Chris Brzuska
email: chris.brzuska@aalto.fi

Antoine Delignat-Lavaud

Christoph Egger
email: christoph.egger@alumni.fau.de

Cédric Fournet
email: fournet@microsoft.com

Konrad Kohbrok
email: konrad.kohbrok@aalto.fi

Markulf Kohlweiss
email: mkohlwei@ed.ac.uk

Key-Schedule Security for the TLS 1.3 Standard

Keywords: XPD XPN, 0..d C N*, 0. C +1..d Key C N*, ..d Key c 0.. +1 Key c eN*, 0.. Key eN* c +2..d Key c eN*, +1..d Key es, 0.. -1 Key es, +1..d c 0.. Keyc eN*, 0.. -

ideas of the proof.

Introduction

Transport Layer Security (TLS) is the most widely used authenticated secure channel protocol on the Internet, protecting the communications of billions of users. Previous versions of TLS have suffered from impactful attacks against weaknesses in their design, including legacy algorithms (e.g. FREAK for export RSA [START_REF] Beurdouche | A messy state of the union: Taming the composite state machines of TLS[END_REF], LogJam [START_REF] Adrian | Imperfect forward secrecy: How Diffie-Hellman fails in practice[END_REF] for export Diffie-Hellman, WeakDH for ill-chosen groups, and exploits against Mantin biases of RC4 [START_REF] Bricout | Analysing and exploiting the mantin biases in RC4[END_REF]); the RSA key encapsulation (e.g. the ROBOT [START_REF] Böck | Return of bleichenbacher's oracle threat (ROBOT)[END_REF] variant of Bleichenbacher's PKCS1 padding oracle); the fragile MAC-encode-encrypt construction leading to many variants of Vaudenay's padding oracles against CBC cipher suites (e.g. BEAST [START_REF] Duong | Here come the ⊕ ninjas[END_REF],

Lucky13 [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF]); the weak signature over nonces allowing protocol version downgrades (e.g. DROWN [START_REF] Aviram | DROWN: Breaking TLS using SSLv2[END_REF] and POODLE); attacks on other negotiated parameters [START_REF] Bhargavan | Downgrade resilience in key-exchange protocols[END_REF], the key exchange logic (e.g. the cross-protocol attack of [START_REF] Mavrogiannopoulos | A crossprotocol attack on the TLS protocol[END_REF] and 3SHAKE [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over tls[END_REF]); exploitations of collisions on the hash transcript (e.g. SLOTH [START_REF] Bhargavan | Transcript collision attacks: Breaking authentication in TLS, IKE and SSH[END_REF]). TLS 1.3 intends both to fix the weaknesses of previous versions and to improve the protocol performance, notably by lowering the latency of connection establishment from two roundtrips down to one, or even zero when resuming a connection.

Historically, the IETF process to adopt a standard involves an open consortium of contributors mostly coming from industry, with a bias towards early implementers. The TLS working group at the IETF acknowledged that this process puts too much emphasis on deployment and implementation concerns, and tends to address security issues reactively [START_REF] Paterson | Reactive and proactive standardisation of TLS[END_REF]. For TLS 1.3, it decided to address security upfront by welcoming feedback from various cryptographic efforts, including symbolic [START_REF] Cremers | Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication[END_REF][START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF] and computational protocol models [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF][START_REF] Dowling | A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol[END_REF][START_REF] Li | Multiple handshakes security of TLS 1.3 candidates[END_REF], both on paper and implemented in tools such as Tamarin or CryptoVerif. Early drafts of TLS 1.3 also drew much inspiration from Krawczyk's OPTLS protocol [START_REF] Krawczyk | The OPTLS protocol and TLS 1.3[END_REF], which comes with a detailed security proof, although later versions diverged from it (in particular in the design of resumption). This proactive approach has certainly improved the overall design of TLS 1.3, and uncovered flaws along its 28 intermediate drafts. However, many of these efforts are incomplete (focusing, e.g., on fixed protocol configurations) or do not account for the final version published in RFC 8446, see Section 6 for a more detailed discussion of related work. Since final adoption, further questions have been raised about pre-shared keys, potential reflection attacks [START_REF] Drucker | Selfie: reflections on TLS 1.3 with PSK[END_REF], and difficulties in separating resumption PSKs (produced internally by the key exchange) from external ones installed by the application. In short: we still miss provable security for the final Internet standard.

TLS can be decomposed into sub-protocols: the record layer manages the multiplexing, fragmentation, padding and encryption of data into packets (also called records) from three separate streams of handshake, alert, and application data. Incoming handshake messages are passed to the handshake sub-protocol, which in turn produces fresh record keys and outgoing handshake messages. Taking advantage of this well-understood modularity, other protocols re-use the TLS 1.3 handshake with different record layers: for instance, DTLS 1.3 is a variant based on UDP datagrams instead of TCP streams, while the IETF version of QUIC replaces the record layer with a much extended transport [START_REF] Iyengar | QUIC[END_REF], adding features such as dynamic application streams and fine-grained flow control. Detailed security proofs for the TLS 1.3 record layer have been proposed by Patton et al. [START_REF] Patton | Partially specified channels: The TLS 1.3 record layer without elision[END_REF] (extending the work of Fischlin et al. [START_REF] Fischlin | Data is a stream: Security of stream-based channels[END_REF] on stream-based channels), Badertscher et al. [START_REF] Badertscher | Augmented secure channels and the goal of the TLS 1.3 record layer[END_REF], and Bhargavan et al. [START_REF] Delignat-Lavaud | Implementing and proving the TLS 1.3 record layer[END_REF], who also provide a verified reference implementation. Therefore, we defer to these works for the record layer, and focus on the handshake protocol. Fig. 1: Overview over the TLS 1.3 Handshake (left) and its key schedule (right).

[m] k denotes encryption of message m under key k. k ae1 and τ c are derived from k cht , k ae2 and τ s are derived from k sht , and k ae3 is derived from k sat . We color digests and keys in alternating pink and blue to clarify digest-key dependency. E.g., label c e traffic and digest d as is used to derive k cet .

TLS 1.3 Handshake and Key Schedule

The top of Fig. 1 gives an abstract view of the TLS 1.3 protocol message flow.

In the client hello message, the client sends a nonce n c , its Diffie-Hellman (DH) share g x , a PSK label and a binder value for domain separation and session resumption. As a means of negotiation, the client may offer shares for different groups and different PSK options (thus the indices i, j in g xi i , label j , binder j ). The server communicates its choice of the DH group and the PSK when sending the server hello message which contains the server nonce n s , its share g y i0 (including the group description) and the label label j0 of the chosen PSK. The remaining messages consist of server certificate, signature (C(pk), CV(σ)), key confirmation messages in the forms of messages authentication codes (MACs) τ s and τ c computed over the transcript, and a ticket which is used on the client side to store a resumption key (later referred to as resumption PSK ) derived from the key material of the current key exchange session.

The key schedule is the core part of the handshake that performs all key computations. It takes as main input PSK and DH key materials and, at each phase of the handshake, it derives keys, e.g., to encrypt client early traffic (k cet ), to compute the binder value (k binder ), to encrypt server handshake traffic (k sht ) and to encrypt client handshake traffic (k cht ).

The key schedule relies on the hashed key derivation function (HKDF) standard [START_REF] Krawczyk | Cryptographic extraction and key derivation: The HKDF scheme[END_REF], which uses HMAC [START_REF] Bellare | New proofs for NMAC and HMAC: Security without collision resistance[END_REF] to implement extract (xtr) and expand (xpd) operations. In addition, the key schedule makes calls to xpd to expand keys into further subkeys. The key schedule thus consists of a collection of xtr an xpd operations, organized in a graph. Each of the operations takes as input a chaining key and/or new key material, (k psk in the xtr in the early phase and k dh in the xtr in the in the handshake phase), together with the latest digest and auxiliary inputs such as a resumption status r and a ticket nonce tn.

In this article, we consider eight output keys of the TLS key schedule: k cet , k eem , k binder , k cht , k sht , k cat , k sat , k eam . They constitute a natural boundary, inasmuch as all other TLS keys and IVs are further derived from them in a transcript-independent manner.

Key Schedule Model and Key Exchange Model

We model the security of the key schedule as an indistinguishability game between a real and an ideal game. The real game allows the adversary to use their own dishonest application PSKs and Diffie-Hellman shares. In addition, it allows the adversary to instruct the game to sample honest PSKs and Diffie-Hellman shares. From these base keys, the adversary can then instruct the model to derive further keys. The adversary cannot see internal keys, but it can obtain the 8 output keys from the model. In turn, in the ideal game, the output keys are replaced by unique, random keys which are sampled independently from the input key material.

The interface of this model captures how the key exchange protocol uses the key schedule. The key exchange protocol should, indeed, not use the internal keys, but instead only use the output keys. Moreover, the final session keys are to be used only by the Record Layer to implement a secure channel. In a companion paper [START_REF] Brzuska | Key exchange to key schedule reduction for TLS 1[END_REF], we show that key exchange security of the TLS 1.3 handshake protocol reduces to the key schedule security established in this paper. Note that authentication is proved based on keys and does not capture binding between keys and identities, as needed, e.g., for reflection attacks [START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF].

Outline We introduce our overall technical approach in Section 2. We define our assumptions for collision-resistance, pseudorandomness and pre-image resistance in Section 3. Section 4 defines syntax and security of the TLS key schedule. Section 5 states the main key schedule theorem and provides its proof. This article gives proof sketches of all lemmata, highlighting their conceptual insights. The complete proofs are provided in the full version [START_REF] Brzuska | Key-schedule security for the tls 1.3 standard[END_REF]. Finally, Section 7 includes proposals for (late) changes to the TLS 1.3 standard.

Technical Approach

Handles

Complex derivation steps make it crucial to maintain administrative handles in the model state, both for internal bookkeeping and security modeling as well as for communication with the adversary. Namely, to instruct the model to perform further computations on keys, the adversary can point to the keys to be used via handles. Such handles are particularly important for honest keys, i.e., honest psks, honest Diffie-Hellman shares and honest internal keys derived via xtr and xpd from honest base keys, because the model cannot provide the adversary with the actual values of these secrets.

Our model constructs handles as nested data records where each nesting step keeps track of the inputs which were used to compute the associated key. We have base handles for PSKs and DH secrets, including handles for dummy zero values to be used in noDH and noPSK mode as well as base handles for a fixed 0salt and fixed 0ikm.

dh sort(X, Y )
Diffie-Hellman secret h = psk ctr , alg application PSK noDH alg fixed 0 len(alg) Diffie-Hellman secret noPSK alg fixed 0 len(alg) PSK 0salt fixed 0 salt 0ikm alg fixed 0 len(alg) initial key material (IKM)

The model then inductively applies the following constructors to build all other handles from the base handles:

xtr name, left parent handle, right parent handle .

xpd name, label, parent handle, other arguments .

For example, given a handle to the early master secret h es , the handle h cet to the client early transport secret is defined as

h cet = xpd cet, c e traffic, h es , t es
where t es is the transcript of the protocol messages exchanged so far, and 'c e traffic' is the constant byte string label prescribed in the RFC [START_REF] Rescorla | The Transport Layer Security (TLS) Protocol Version 1[END_REF] for this derivation step.

Agility Our model is agile, i.e., it supports multiple algorithms. Thus, we tag the handles h = psk ctr , alg , noPSK alg and 0ikm alg with the algorithm alg for which the keys are intended. Jumping ahead, we note that we also tag keys with their intended algorithm so that in the key derivation

k cet = xpd(k es , c e traffic, d es ),
the agile xpd function can retrieve the correct hash algorithm alg to use within hmac from the key's tag. We write alg(h cet ) for the algorithm descriptor of h cet and tag h (k) for key k tagged with this algorithm.

Length The handle determines the algorithm, and the algorithm determines the length of keys and outputs of a hash-algorithm alg. For convenience, we write len(h cet ) as an alias for len(alg(h cet )).

Note that we introduced handles 0ikm alg for the dummy key value 0 len(alg) as well as 0salt for the 1-bit-long 0-key. This is because hmac pads keys with zeroes up to their block length and thus, storing multiple zero values would introduce redundancy in the model without a correspondence in real-life.

Name and level In addition to the algorithm and its key length, the handle determines the key name (cet) and a level. The level is the number of resumptions the handle records, counting from 0 and adding one for each node with a resumption label. We write level(h cet ) for this level. We will often need to refer to the parent names of a particular key (name) n, and write the pair of parent names as prntn(n). In the case of xpd, the key is only derived from one key and thus, in this case, prntn(n) = (n 1 , ⊥). Conversely, we refer by chldrnn(n 1 ) to the set of all key names which are derived from n 1 . In particular, if prntn(n) = (n 1 , ⊥), then n ∈ chldrnn(n 1 ). We refer to all names which share a parent with n as sblngn(n).

Handshake mode Jumping ahead, we note that we use handle data also to communicate the handshake mode to the key schedule model. A noDH alg Diffie-Hellman handle signals a psk_ke mode, while a noPSK alg PSK handle signals a dh_ke mode.

Application Key Registration & Honesty

Honesty of a handle is a crucial concept to model that the key associated with the handle, when returned to the adversary, looks pseudorandom. Honesty is inductively computed, starting from the base keys: All zero keys have dishonest handles. Handles of application PSKs are honest if their key was sampled by the security model and dishonest if their key was sampled by the security model. Diffie-Hellman handles are honest if both shares are honest. Derived handles are honest if and only if at least one of their input handles are honest. Considering the derivation graph (cf. right side of Fig, 1), we obtain that the h esalt handles and the handles which appear before have the same honesty as the last PSK handle, while the handles after h esalt are honest if the last PSK handle was honest or the last Diffie-Hellman handle was honest. In the following we use the the pseudorandomness game Gxpd 0 n, for the xpd function (depicted in Fig. 2) as a running example to introduce core concepts. As is common in cryptography, security is modeled as an interaction between an adversary A (which can be thought of as sitting left of the picture) and a program which we call the game. This interaction happens via so-called oracles-which we describe in pseudo-code-corresponding to the arrows from the left side of the picture. The task of the adversary consists in distinguishing two variants of the game G 0 and G 1 with identical interfaces and we measure the success probability of any such adversary A and call it advantage.

State-Separating Proofs (SSPs)

Q CN , UNQ CN Q n1 , UNQ n1 GET n1, HASH Xpd CN, Q n1 UNQ n1 Key n1, Q CN UNQ CN Key CN, SET CN, GETCN, SET n1, XPD CN,
Definition 1 (Advantage). For adversary A, we define the advantage

Adv(A; G 0 , G 1 ) := Pr 1 = A → G 0 -Pr 1 = A → G 1 .
In particular, for the pseudorandomness game Gxpd b n, for xpd, the analogous definition is as follows.

Definition 2 (XPD). For adversary A, we define the xpd pseudorandomness advantage Adv(A, Gxpd 0 n, , Gxpd 1 n, ) as

Pr 1 = A → Gxpd 0 n, -Pr 1 = A → Gxpd 1 n,
, where Fig. 2 defines Gxpd 0 n, . The graphs specifying such a security game suggest a natural flow downwards. While we discuss the details of the game later in this section, one can extract a conceptual picture already from the graph alone. Concretely the intended usage (by the adversary) of Gxpd b n, consists on first registering input values using the SET n1, oracle, executing key derivation using the XPD CN , oracle and finally retrieving and testing the output using the GET n, oracle. In addition, the adversary gets access to auxiliary oracles, namely the HASH oracle modeling a cryptographic hash function as well as the Q and UNQ oracles. 5

= ∅. We say that a package M is a game if [M →] = ∅.
While some oracles of a package are exposed to the adversary, others are used only internally within the game. A monolithic version of a game such as Gxpd b n, can be obtained by inlining all internal oracle calls. With the concept of packages we can now discuss the individual parts of Gxpd b n, . Xpd CN , is a parallel composition of Xpd n, for all children of n 1 exposing the oracles XPD n, for n ∈ CN , we write XPD CN , as shorthand for these oracles. The Xpd CN , packages are the only stateless packages in the game, indicated by the white color as opposed to the gray of stateful packages.

Xpd n,

Parameters

n : name ,d)) based on the parent handle h 1 , the arguments (e.g. transcript) and the bit r indicating whether this is a resumption session. The evaluation also includes a label which depends on the name of the package as well as the resumption bit. Note that the oracle only receives the handle of the input key from the adversary and only returns the newly constructed handle of the newly derived key. Concrete secrets are passed to Key b n, packages using the GET and SET oracles. Here we can distinguish the upper Key 1 n1, package and the lower Key b CN , packages (for all n in CN ). We defer discussion about the Q and UNQ oracle calls to the description of the Log package.

: level prntn : N → (N ⊥ × N ⊥ ) label : N × {0, 1} → {0, 1} 96 State no state XPD n, (h 1 , r, args) n1, _ ← prntn(n) label ← label(n, r) h ← xpd n, label , h1, args (k1, hon) ← GET n 1 , (h1) if n = psk : ← + 1 k ← xpd(k1, (label , args))
The upper Key 1 n1, package offers oracle SET n1, (h, hon, k) to the adversary which allows it to register a key. The oracle first verifies that the handle h matches the name n and level of this key package and-modeling algorithmic agilityverifies that the algorithm tag matches the value of the key, and else, assert throws an abort. As this is an ideal key package (indicated by superscript b=1 ) for honest keys, instead of using the value provided by the adversary a fresh value is sampled-as indicated by using ←$ in contrast to ← used for assignments. Finally the key is stored in this package's state and the handle returned to the caller. The GET oracle simply restores algorithm tagging on the key value and returns it to the caller (in this case the Xpd package). The lower Key b CN , packages work the other way round in that they expose the GET oracle to the adversary while the SET oracle is used by Xpd. We encode the distinguishing task for the adversary in the Key b CN , package: In Gxpd 0 n, (b = 0), the keys returned from the GET oracle of the Key 0 CN , is honestly computed based on the input keys while in the ideal game Gxpd 1 n, the values of honest keys are sampled in the Key package ignoring the value computed by Xpd.

Finally, queries Q n and UNQ n to the Log n package (Fig. 4) model collisions. The Q query simply returns if a handle is re-used while UNQ concerns itself with collisions between keys via an abort pattern and a mapping method. In slightly nonstandard notation, we use existential quantors here to express searching for indices into tables. The pattern models conditions on states where the game aborts (i.e. terminates and outputs a special symbol), cf. Section 5.3 for their

Key b n, Parameters n : name : level State K n, : Keytable SET n, (h, hon, k ) assert name(h) = n assert level(h) = assert alg(k ) = alg(h) k ← untag(k ) assert len(h) = |k| if Qn (h) = ⊥ : return Qn (h) if b : if hon : k ←$ {0, 1} len(h) h ← UNQ n (h, hon, k) if h = h : return h K n, [h] ← (k, hon) return h GET n, (h) assert K n, [h] = ⊥ (k * , hon) ← K n, [h] k ← tag h (k * ) return (k, hon) Log P,map n Parameters n : name State Ln : Log Qn (h) if Ln[h] = ⊥ : return ⊥ else (h , _, _) ← Ln[h] return h UNQ n (h, hon, k) if (∃ h : Ln [h ] = (h , hon , k) ∧ level(h) = r ∧ level(h ) = r ) : if map(r, hon, r , hon Jn[k]) : Ln [h] ← (h , hon, k) Jn [k] ← 1 return h if (∃ h : Ln [h ] = (h , hon , k) ∧ level(h) = r ∧ level(h ) = r ) : P (r, hon, r , hon ) Ln [h] ← (h, hon, k) return h P the command P (r, hon, r , hon ) is Z ∅ A if hon = hon = 0 ∧ r = r = 0 : throw abort D if hon = hon = 0 : throw abort R if hon = hon = 0 : throw abort else throw win F throw abort map the command map(r, hon, r , hon , Jn [k]) is 0 0 1 hon = hon = 0 ∧ r = r ∧ 0 ∈ {r, r } ∧ Jn [k] = 1 ∞ hon = hon = 0
Fig. 4: Code for the Key and Log. In addition we use Nkey for a single key package that answers queries for all levels from the same table and 0key for a NKey package which consistently answers with the constant all-zeros key.

use. We use the throw notation here to allow special symbols in addition to abort which is also used by assert. In the game Gxpd b n, , the D pattern aborts on collisions between dishonest keys. The F and R pattern abort if there is a collision between key values, regardless of their honesty, and they return different abort messages. Z does not abort at all, and A aborts upon a collision of two dishonest level 0 keys (which we use to constrain the adversary's psk registrations in the key schedule model).

Mapping methods filter certain collisions (preventing an abort event. ∞ allows collisions between Diffie-Hellman secrets (the adversary can construct colliding values via X z Y = XY z ) and the 1 method allows the adversary to register a dishonest application PSK colliding with an dishonest resumption PSK. The mapping methods are only used in the proof and not in the security model. (see FIPS 180-2). The HASH oracle takes as input a text t from the domain of f-alg and returns its digest d. If that text t has not been queried before, the digest is stored in table H at index t. In the ideal game (b = 1), the oracle first checks whether d already occurs in H , and if so, throws an abort. Hence, the adversary can distinguish between the real and the ideal game if and only if it can submit two different texts with the same digest. Our definition generalizes to n-ary functions by letting the text t be the tuple of their arguments.

Assumptions

Collision-Resistance

Gcr f-alg,b HASH(t) assert t ∈ dom(f-alg) d ← f-alg(t) if H [t] = ⊥ : if b ∧ d ∈ range(H ) : throw abort H [t] ← d return d
Definition 4 (Collision-Resistance). For an adversary A, a function f ∈ {hash, xtr, xpd} and algorithm alg ∈ H, define collision-resistance advantage Adv(A, Gcr f-alg,0 , Gcr f-alg,1 ) is

Pr 1 = A → Gcr f-alg,0 -Pr 1 = A → Gcr f-alg,1 .
Agile Collision-resistance It is convenient to define the agile collision-resistance game Gacr f,b as well, where f ∈ {hash, xtr, xpd} takes tagged inputs, i.e., hash takes a single input, tagged with the algorithm to use, xpd takes three inputs (k, label , args), where k is tagged, and xtr takes inputs (k 1 , k 2 ) where one is tagged, and if both are tagged, they are tagged consistently. The adversary can then make queries to HASH with values in the domain of the agile functions. We write Hash b := Gacr hash,b . See Section 2.1 for further discussion of tagging.

Pseudorandomness of xpd

For most key names n, Definition 2 already captures pseudorandomness of xpd. We now cover two special cases.

XPD to derive PSK For n = psk (cf. Fig. 6a), the layer index increases from to + 1. Thus, the XPD psk , oracle reads keys via GET rm, queries, but writes keys using the level + 1 query SET psk , +1 . Another difference in Gxpd b psk , compared to the general Gxpd b n, is that the lower Log D1 psk package uses a D1 pattern for logging which ignores level 0 UNQ psk (h, hon, k) queries with hon = 0 whenever there already exists a dishonest handle h for key value k at level 0. Since XPD psk , writes only on level + 1 > 0, this difference in logging does not affect the strength of the assumption, but it makes the assumption code align with the key schedule game, cf. Section 4.1. Finally, for deriving the psk, no hash-operation is performed.

Definition 5 (XPD for psk). For an adversary A, we define the xpd pseudorandomness advantage for psk derivation Adv(A, Gxpd 0 psk , , Gxpd 1 psk , ) as

Pr 1 = A → Gxpd 0 psk , -Pr 1 = A → Gxpd 1 psk ,
XPD to derive esalt For n = esalt, the lower Log R esalt package uses an R pattern instead of a D pattern, sending abort messages whenever the same key value k is registered as an esalt under two distinct handles h and h (across all levels and regardless of honesty). Note that the adversary could simulate the R pattern itself (by retrieving all keys and checking for equality) and thus, the R pattern only weakens the adversary since it can no longer query the game after triggering an R abort and since the adversary does not learn the value of the collision which caused the abort. Definition 6 (XPD for esalt). For an adversary A, we define the xpd pseudorandomness advantage for esalt derivation Adv(A, Gxpd 0 esalt, , Gxpd 1 esalt, ) as

Pr 1 = A → Gxpd 0 esalt, -Pr 1 = A → Gxpd 1 esalt, . Q psk ,UNQ psk Q rm ,UNQ rm GET rm,

State no state

XTRn, (h1, h2)

n1, n2 ← prntn(n) if alg(h1) = ⊥ ∧ alg(h2) = ⊥ : assert alg(h1) = alg(h2) h ← xtr n, h1, h2 (k1, hon1) ← GETn 1 , (h1) (k2, hon2) ← GETn 2 , (h2) k ← xtr(k1, k2) hon ← hon1 ∨ hon2 if b ∧ hon2 : k ←$ {0, 1} len(k) k ← tag alg(k) (k ) h ← SETn, (h,

Pseudorandomness of xtr

The TLS 1.3 key schedule performs three xtr operations (cf. Fig. 1), and the modeling is analogous to the XPD assumptions, except that for the early secret es, xtr security relies on the psk which is the right input to xtr, and for the application secret as, xtr security relies on esalt which is the left input to xtr.

The derivation of the handshake secret hs is a special case, because its security is an OR of the honesty of its left and right input. We here state the xtr security assumption required for hs security based on its left input esalt and turn to the security based in its right input (the Diffie-Hellman (DH) secret) shortly. Note that the security of esalt will be applied after the security of the DH secret and thus, the bit b in the Xtr b hs, is already set to 1 and samples output keys uniformly at random whenever the Diffe-Hellman secret is honest. The security of esalt thus only increases security for those keys where the Diffie-Hellman secret is dishonest.

Definition 7 (XTR advantages).

For adversary A, level ∈ N 0 , we define the xtr pseudorandomness advantage for es as Adv(A, Gxtr1 0 es, , Gxtr1 1 es, ), the pseudorandomness advantage for hs as Adv(A, Gxtr2 0 hs, , Gxtr2 1 hs, ) and the pseudorandomness advantage for as as Adv(A, Gxtr3 0 as, , Gxtr3 Our salted oracle Diffie-Hellman assumption (SODH) is a stronger variant of the oracle Diffie-Hellman assumption introduced by Abdalla et al. [START_REF] Abdalla | The oracle Diffie-Hellman assumptions and an analysis of DHIES[END_REF] and the PRF oracle Diffie-Hellman assumption studied by Brendel et al. [START_REF] Brendel | PRF-ODH: Relations, instantiations, and impossibility results[END_REF]. Most importantly, SODH is an agile, i.e., it requires pseudorandomness of the derived keys even when the adversary can see hash-values of the same Diffie-Hellman secret under different hashfunctions and different, possibly adversarially chosen salts. In practice, different salts can emerge from disagreement between server and client about the PSK to use since the early salt esalt (and possibly also the alg) changes when the PSK changes (see Fig. 1). The Gsodh b game (cf. Fig. 8) allows the adversary to generate honest Diffie-Hellman shares via DHGEN, to combine them (or an honest and a dishonest share) into a Diffie-Hellman secret via DHEXP and to derive keys from them via XTR n, for an arbitrary level ∈ {0, .., d}. Oracle GET n, then allows to retrieve the derived keys. Note that pseudorandomness is modeled, this time, by a bit in the Xtr b n, package (Fig. 7a). Definition 8 (SODH). For an adversary A, we define the Salted Oracle Diffie Hellman (SODH) advantage Adv(A, Gsodh 0 , Gsodh 1 ) :=

DHGEN(grp) assert grp ∈ G g ← gen(grp) x ←$ Z ord(grp) X ← g x E[X] ← x return X DHEXP(X, Y ) assert grp(X) = grp(Y ) h ← dh sort(X, Y ) honX ← E[X] = ⊥ honY ← E[Y ] = ⊥ assert honX = 1 x ← E[X]; k ← Y x hon ← honX ∧ honY h ← SETdh (h, hon, k) return h
Pr 1 = A → Gsodh 0 -Pr 1 = A → Gsodh 1 ,

Pre-image resistance for xpd

Pseudorandomness and collision resistance of xpd also imply that it is hard to find pre-images for honest output keys. We prove this implication in the full version of this article [START_REF] Brzuska | Key-schedule security for the tls 1.3 standard[END_REF]Lemma E.7] and in this conference version rely on pre-image resistance as a separate assumption for convenience.

Key Schedule

We reason about the TLS 1.3 key schedule in terms of its three elementary operations extract (xtr), expand (xpd) and computation of Diffie-Hellman secrets. This section first introduces an abstract key schedule syntax and refines it to capture TLS 1.3 as part of a bigger class of TLS-like key schedules. We then define key schedule security and state our theorem for all TLS-like key schedules.

Key Schedule Syntax

Our formalization interprets the key schedule as a directed graph where nodes describe key names (cf. Fig. 10 for the case of TLS 1.3). In addition to the set of names N and the graph description (encoded as prntn function, cf. Section 2.1), a key schedule has a function label which maps the name and a resumption bit to a derivation label. We conveniently model hmac operations by using xpd with empty label as an alias for hmac. By sound cryptographic practice, a key should be either used for xpd or for hmac but not both, so if a node has an empty label, it is not allowed to have siblings. Similarly, xtr operations only yield a single child, and the multiple children of xpd operations are derived using distinct labels.

Definition 10 (Key Schedule Syntax).

A key schedule ks = (N, label, prntn) consists of a set of names N and two functions

label : N × {0, 1} → {0, 1} 96 ∪ {⊥} prntn : N → (N ∪ ⊥) × (N ∪ ⊥)
with the previously described restrictions.

Fig. 10 describes the prntn function of the TLS 1.3 key schedule as a graph.

Stating and proving our theorem in terms of the concrete TLS key schedule would require listing and treating each xpd operation individually. Instead, we prove our theorem for all TLS-like key schedules (of which the TLS key schedule is an instance). We consider a key schedule as TLS-like if it aligns with TLS in terms of base keys and xtr operations and treats the psk name as the main root from which all keys except for the base keys can be reached. Moreover, a TLSlike key schedule only has a single loop. This loop contains the edge from rm to psk and models resumptions. This edge has the special property of increasing the associated level as the psk is computed in an earlier session to be used in a later key schedule session. As such the cycle does not contradict an ordering on key computations.

Definition 11 (TLS-like Key Schedule Syntax).

A key schedule ks = (N, label, prntn) is TLS-like if its prntn graph satisfies the above restrictions, its set of names N contains at least the names 0salt, psk , es, esalt, dh, hs, hsalt, 0ikm, as, rm and the prntn function maps 0salt, dh and 0ikm to (⊥, ⊥), maps es, hs and as according to Fig. 10, maps psk to (rm, ⊥) and each of the remaining names n to some pair (n 1 , ⊥) with n 1 = ⊥.

We use several subsets of N which we summarize in Table 1.

Key Schedule Security Model

Our key schedule security model captures that the key schedule produces keys which are pseudorandom and unique. We formulate security as indistinguishability between a real and an ideal game where the real game implements the actual key schedule derivations, while in the ideal game, output keys are unique, and honest keys are sampled uniformly at random. Concretely, we follow a simulation approach (somewhat similar to the Canetti and Krawczyk [START_REF] Canetti | Universally composable notions of key exchange and secure channels[END_REF] approach to key exchange), where the ideal game is defined as a composition of a simulator S and an ideal functionality. The simulator instructs the ideal functionality to produce output keys of certain length, however the value of the output keys is sampled independently from the simulator. As we require that no adversary can distinguish these two settings this captures security: The protocol determines when an output key becomes available and which type of key but no information about the concrete value is disclosed in the protocol (as the simulator does not have such information). Concretely, in our ideal game Gks 1 (S) (Fig. 11b), the simulator S is a parameter and the Key Similarly, we describe the real execution of the key schedule as a game Gks 0 , written in pseudocode. Following the SSP methodology outlined in Section 2.3, we split the pseudocode of the game Gks 0 into several packages most of which (Xpd, Xtr, DH, Key, and Log) have been introduced before and Check is described in Section 4.3. Fig. 11a depicts the composed game Gks 0 -recall that this graph is not merely an illustration, it is part of the formal definition of Gks 0 .

N

The set of all (key) names

N * N \ {psk , dh } I * The set of internal keys {n ∈ N * | chldrnn(n) = ∅} O * : The set of output keys {n ∈ N * | chldrnn(n) = ∅} O: O * ∪ {psk } S:
The set of separation points (Definition 13) XPN : The set of expand names {n ∈ N : prntn(n) = (_, ⊥)} XPR: The set of representatives (Section 4.3)

Table 1: Notation

The game Gks 0 exposes SET psk ,0 and DHGEN oracles which sample honest Diffie-Hellman shares, honest application PSKs and enable the adversary to register dishonest application PSKs with a chosen value. The XTR and XPD oracles trigger key derivations. Finally, the adversary can access output keys via the GET oracle on the (real) key package Key 0 O * ,0..d .

Definition 12 (Key Schedule Advantage). For a key schedule ks = (N, label, prntn), a natural number d, a simulator S and an adversary A which makes queries for at most d levels we define the advantage Adv(A, Gks 0 , Gks 1 (S)) :=

Pr 1 = A → Gks 0 -Pr 1 = A → Gks 1 (S) ,
where Fig. 11b defines Gks 1 (S) and Fig. 11a defines Gks 0 .

Front-End Checks

Check XPD n, (h 1 , r, args) The Check package acts as a restriction on the adversary since the assert conditions in the Check code force the adversary to use the correct Diffie-Hellman shares and binder value in its transcript when the transcript is included in a derivation step. In terms of composability, the assert conditions in Check force the key exchange to call the key schedule with consistent values, i.e., derive the Diffie-Hellman secret from a pair of shares that is included in the transcript and not from an unrelated pair of shares. The TLS 1.3 specification ensures these innocent conditions, and requiring them formally means that the proof breaks down when session memory in TLS 1.3 is unsafely implemented.

if n = bind : if r = 0, assert level(h1) = 0 if r = 1, assert level(h1) > 0 elseif n ∈ S ∩
In addition to enforcing the use of consistent shares in the transcript, the XPD oracle of the Check package (Fig. 12) ensures that the resumption flag is consistent with the level of the PSK; and that the binder tag included in the transcript of later stages (at the end of the last ClientHello message) is the same that was computed and checked in the early stage. The transcript is not included into all xpd derivations, but only once on the path from psk to output key, and Check only filters queries on these particular derivation steps. Since including the transcript ensures domain separation between different protocol runs and derivation pathes, we refer to the derivation steps which include the transcript as a separation point.

Definition 13 (Separation Points).

For a key schedule ks = (N, label, prntn), we call S ⊆ N a set of separation points, if it satisfies the following two requirements:

-∀ n ∈ O: the path from psk to n contains an n ∈ S.

-If there exists a path from dh to an n ∈ O, then it contains an n ∈ S.

In addition, for each xpd operation, we choose one representative child. I.e., XPR ⊆ N is a representative set for ks if psk , esalt ∈ XPR and for each name n ∈ N with only a single parent (these are the xpd nodes), either n or exactly one sibling of n is contained in XPR.

Key Schedule Theorem

Theorem 1. Let ks be a TLS-like key schedule with representative set XPR and separation points S. Let d ∈ N. There is an efficient simulator S such that for all adversaries A which make queries for at most d resumption levels,

Adv(A, Gks 0 , Gks 1 (S)) ≤ Adv(A → R main cr , Gacr hash,b ) + j∈{Z,D},f∈{xtr,xpd} Adv(A → R main j,f , Gacr f,b ) + max i∈{0,1} Adv(A i → R main sodh , Gsodh b ) d-1 =0 Adv(A i → R main es, , Gxtr b es, ) +Adv(A i → R main hs, , Gxtr b hs, ) +Adv(A i → R main as, , Gxtr b as, ) + n∈XPR Adv(A i → R main n, , Gxpd b n, ) +Adv(A i → R main esalt,pi , Gpi b esalt ) +Adv(A i → R main O * ,pi , Gpi b O * ) ,
where A i behaves as A except that it returns bit i on a so-called win abort (cf. Lemma 8); R main * := R ch-map → R * when replacing * by cr, (Z, f), (D, f), sodh, es, hs, as, n, O * , pi or esalt, pi , the simulator S is marked in grey in Fig. 16b, Fig. 18a defines R sodh , Fig. 18e defines R es, , R hs, and R as, are defined analogously, and Fig. 18f defines R n, for n ∈ XPR, 0 ≤ ≤ d, Fig. 18b defines R esalt,pi and Fig. 18c defines R O * ,pi .

Proof Technique

A recurrent proof technique which we use are reductions, written in SSP style. As usually, we want to show that if there is an adversary A which successfully Mapping Core Key-Schedule Fig. 13: Proof Structure distinguishes between two games G 0 big and G 1 big , then based on A, we can construct an adversary B of similar complexity as A which successfully distinguishes between two games G 0 sml and G 1 sml . Our reductions will have the following form.

Lemma 1 (Reduction Technique). If we can define a reduction R such that

G 0 big code ≡ R → G 0 sml (1) and G 1 big code ≡ R → G 1 sml (2) then Adv(A; G 0 big , G 1 big ) = Adv(B; G 0 sml , G 1 sml ), (3)
where

B := A → R. (4)
Proof. Assuming Equation 1, 2 and 4, we deduce Equation 3 as follows:

Adv(A,G 0 big , G 1 big ) def. = Pr 1 = A → G 0 big -Pr 1 = A → R → G 1 big Eq.1&2 = Pr 1 = A → (R → G 0 sml ) -Pr 1 = A → (R → G 1 sml ) = Pr 1 = (A → R) → G 0 sml ) -Pr 1 = (A → R) → G 1 sml def. = Adv(A → R, G 0 sml , G 1 sml ) Eq. 4 = Adv(B, G 0 sml , G 1 sml )
Importantly, throughout this article, we define reductions graphically as composition of previously defined packages so that the reduction re-uses code, as opposed to the usual technique which introduces new code for a reduction. As a Map SETpsk,0(h, hon, k) h ← SETpsk,0(h, hon, k)

Mpsk[h] ← h return h GETn∈O * , (h) assert Mn, [h] = ⊥ h ← Mn, [h] return GET n,level(h ) (h ) XPDn∈XPN, (h1, r, args) i1, _ ← prntidx(n, ) assert Mi 1 [h1] = ⊥ label ← label(n, r) 1 ← level(Mi 1 [h1]) h ← xpd n, label, h1, args h ← XPDn, 1 Mi 1 [h1], r, args if n = psk : ← + 1 Mn, [h] ← h return h DHGEN() return DHGEN() DHEXP(X, Y ) h ← dh sort(X, Y ) h ← DHEXP(X, Y ) if Mdh[h] = ⊥ : Mdh[h] ← h return h XTR n∈{es,hs,as }, (h1, h2) i1, i2 ← prntidx(n, ) assert Mi 1 [h1] = ⊥ assert Mi 2 [h2] = ⊥ choose ← level(Mi 1 [h1]), level(Mi 2 [h2]) h ← xtr n, h1, h2 h ← XTR n, Mi 1 [h1], Mi 2 [h2] Mn, [h] ← h return h
Fig. 14: Oracles of Map. Here, ∈ {0 . . . d}.

choose ← level(M n1 [h 1 ]), level(M n2 [h 2 ]) assigns to the value level(M n1 [h 1 ]) if it is not ⊥ and level(M n2 [h 2 ]), else.
result, we can argue Equations 1 and 2 graphically. E.g., in Fig. 17b we highlight the reduction in gray and observe that the only change from Fig. 17a is the collision resistance assumption-the G b sml in this case. Observing the graph of Gks 0 (cf. Fig. 11a) closely and comparing it with the graphs of the assumptions introduced in Section 3, one can identify that the assumptions are almost sub-graphs of Gks 0 , and by an appropriately chosen sequence of reduction arguments, the graphs of the assumptions will appear as actual subgraphs.

Proof of Theorem 1

We need to show the indistinguishability of the real game Gks 0 and the ideal game Gks 1 (S). Fig. 15a depicts the real game Gks 0 (cf. Fig. 11a), with slightly different graph layouting. Fig. 16b depicts the ideal game Gks 1 (S) (cf. Fig. 11b) where the simulator S is described in concrete code. To show the indistinguishability between Gks 0 (Fig. 15a) and Gks 1 (S) (Fig. 16b), we make 4 game hops, depicted as the sequence of the five games depicted in Fig. 15a, 15b, 15c, 16a and 16b. We now describe each of the game hops and state the corresponding lemma.

First, recall that the key schedule security model stores keys in a redundant fashion (a) due to possible equal values of a dishonest resumption psk (level(h) > 0) and an adversarially registered application psk (level(h) = 0) and (b) due to the equal values of the (dishonest) DH keys corresponding to (X a , Y ) and (X, Y a ).

Lemma 2 introduces a Map package (see Fig. 15b for the game and the left column of Fig. 14 for the code of Map) to remove the redundantly stored keysnote that the Log A1 psk and the Log Z ∞ dh package now use the map = 1 and the map = ∞ code of Log (see Fig. 4 for its code). As a result, any adversary playing against Gcore 0 (defined in Fig. 15b) cannot create (this particular) redundancy anymore since the Key psk , and DHKey dh packages do not store the key again when the mapping code is triggered. We defer the proof of code equality proof of Lemma 2 to the full version [START_REF] Brzuska | Key-schedule security for the tls 1.3 standard[END_REF]. It relies on proving the invariant that whenever Gks 0 stores key k with honesty hon under handle h, then game Gks 0Map stores key k with honesty hon under the mapped handle h = M [h]. The proof proceeds by induction over the oracle calls.

Lemma 2 (Map-Intro). For all adversaries A which make queries for at most d resumption levels,

Pr 1 = A → Gks 0 = Pr 1 = A → Gks 0Map .
In particular Gks 0 func ≡ Gks 0Map .

Lemma 3 then reduces the indistinguishability of Gks 0Map (Fig. 15b) and Gks 1Map (Fig. 15c) to the indistinguishability of Gcore 0 and Gcore 1 (S core ) using reduction R core . The indistinguishability of Gcore 0 and Gcore 1 (S core ) will be established in Theorem 2 in Appendix 5.3 and contains the main technical argument of this article.

Lemma 3 (Main). For all PPT adversaries A which make queries for at most d resumption levels,

Adv(A, Gks 0Map , Gks 1Map ) =Adv(A → R ch-map , Gcore 0 , Gcore 1 (S core )),
where Fig. 15b defines Gks 0Map , Fig. 15c defines Gks 1Map , R ch-map and S core are marked in grey in Fig. 15c, and Fig. 17a and Fig. 17i define Gcore 0 and Gcore 1 (S core ), respectively.

Proof. The proof of Lemma 3 is an instance of Lemma 1 with G 0 big = Gks 0Map , G 1 big = Gks 1Map , G 0 sml = Gcore 0 , G 1 sml = Gcore 1 (S core ) and R = R ch-map . By Lemma 1, it suffices to show that

Gks 0Map code ≡ R ch-map → Gcore 0 (5)
Gks 1Map code ≡ R ch-map → Gcore 1 (S core ) (6)
Equation 5 follows by definition, since Fig. 15b defines Gks 0Map as the composition of R ch-map and Gcore 0 . Similarly, for Equation 6, Fig. 15c defines Gks 1Map as the composition of R ch-map and Gcore 1 (S core ).

In Lemma 4, we inline the Xpd n,0..d code into Map for n ∈ O * and call the result Map-Xpd (see Fig. 15c and Fig. 16a for the two games). The proof is a simple inlining argument and included into the full version [START_REF] Brzuska | Key-schedule security for the tls 1.3 standard[END_REF] for completeness.

Lemma 4 (Xpd-Inlining). For all PPT adversaries A which make queries for at most d resumption levels,

Pr 1 = A → Gks 1Map = Pr 1 = A → Gks Mapxpd .
In particular Gks 1Map code ≡ Gks Mapxpd .

Finally, Lemma 5 establishes the (perfect) indistinguishability of Gks Map-Xpd and Gks 1 (S). The proof of Lemma 5, essentially, removes or rather inverts the mapping on the output keys in order to recover the ideal functionality. Inverting the handle mapping, however, requires that it is injective. Conceptually, it is also clear that injectivity of the handle mapping needs to play a role in the proof: We prove uniqueness of output keys which means that equal keys imply equal handles. The injectivity proof ensures that the mapping did not introduce additional collisions and that the proof of Theorem 2 indeed suffices to establish the uniqueness of output keys in Gks 1 (S).

Lemma 5 (Map-Outro). For all PPT adversaries A which make queries for at most d resumption levels,

Pr 1 = A → Gks Mapxpd = Pr 1 = A → Gks 1 (S) .
In particular, Gks Mapxpd func ≡ Gks 1 (S).

In summary, Lemma 3 is the core argument, Lemma 2 is proven via a mechanical invariant proof, Lemma 5 is proven via a conceptually interesting invariant proof and Lemma 4 is a straightforward inlining argument.

Theorem 1 directly follows from Lemma 2-Lemma 5 and Theorem 2 (stated in Section 5.3).

Adv(A, Gks 0 , Gks 1 (S))

Lm. 2 = Adv(A, Gks 0Map , Gks 1 (S)) Lm. 5 = Adv(A, Gks 0Map , Gks Mapxpd ) Lm. 4 = Adv(A, Gks 0Map , Gks 1Map ) Lm. 3 = Adv(A → R ch-map , Gks 0core , Gks 1core (S core )) Th. 2 ≤ Adv(A → R main cr , Gacr hash,b ) + j∈{Z,D},f∈{xtr,xpd} Adv(A → R main j,f , Gacr hash,b ) + max i∈{0,1} Adv(A i → R main sodh , Gsodh b ) + Adv(A i → R main esalt,pi , Gpi b esalt ) + Adv(A i → R main O * ,pi , Gpi b O * ) + d-1 =0 Adv(A i → R main es, , Gxtr b es, ) + Adv(A i → R main hs, , Gxtr b hs, ) + Adv(A i → R main as , Gxtr b as, ) + n∈XPR Adv(A i → R main n, , Gxpd b n, ) ,
where XPR is the representative set required by the theorem, R main * := R ch-map → R * when replacing * by cr, (Z, f), (D, f) sodh, es, hs, as, n, O * , pi or esalt, pi .

Core Key Schedule Theorem

It remains to show that the core key schedule game Gcore 0 without the Map and Check package in front (Fig. 17a is indistinguishable from an ideal game Gcore 1 (S core ) which consists of an ideal functionality with a simulator S core (Fig. 17i). We prove Theorem 2 in Appendix A.

Theorem 2 (Core). Let ks be a TLS-like key schedule with XPR. Let d be an integer. Let S core be the efficient simulator defined in Fig. 16b. Then, for all adversaries A which make queries for at most d resumption levels, we have that

Adv(A, Gcore 0 , Gcore 1 (S core )) ≤ R∈{Rcr,R Z ,R D } Adv(A → R, Gacr b ) + max i∈{0,1} Adv(A i → R sodh , Gsodh b ) + Adv(A i → R esalt,pi , Gpi b esalt ) + Adv(A i → R O * ,pi , Gpi b O * ) + d-1 =0 Adv(A i → R es, , Gxtr b es, ) + Adv(A i → R hs, , Gxtr b hs, ) + Adv(A i → R as , Gxtr b as, ) + n∈XPR Adv(A i → R n, , Gxpd b n, ) ,
where XPR is the required representation set (cf. Table 1), Fig. 17a defines Gcore 0 and Fig. 17i defines Gcore 1 (S core ), Fig. 17b defines R cr , Fig. 18a defines R sodh , Fig. 18e defines R es, , R hs, and R as, are defined analogously, and R n, for n ∈ XPR and 0 ≤ ≤ d is defined in Fig. 18f, R esalt,pi is defined in Fig. 18b and R O * ,pi is defined in Fig. 18c.

Related Work

The following discussion focuses on attacker capabilities and security guarantees, and glosses over the exact encoding into security games and the use of multiple keys and stages. Dowling et al. [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF][START_REF] Dowling | A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol[END_REF][START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol[END_REF] present a multi-stage security model of draft-05, draft-10, and the final version of the standard. Their multi-stage model considers psk_ke, dh_ke, and psk_dhe_ke modes in isolation. Li et al. [START_REF] Li | Multiple handshakes security of TLS 1.3 candidates[END_REF] adapt the multi-stage security model to also capture the recursive nature of the TLS 1.3 key schedule, by accounting for the re-use of resumption secrets between different modes (psk_ke, psk_dhe_ke, and the now removed semi-static share 0-RTT).

Cremers et al. [START_REF] Cremers | Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication[END_REF][START_REF] Cremers | A comprehensive symbolic analysis of TLS 1[END_REF] investigate the security of draft-10 and draft-21, using the automated Tamarin prover (in the symbolic model). Their work investigates the proposed post-handshake client authentication and finds an attack that exploited a missing binding between PSKs and transcripts that led to the addition of binders to the standard. To our knowledge ours is the first reduction proof that models the additional security afforded by binder values.

Bhargavan et al. [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF] also model TLS 1.3, decomposed into 3 separate pieces: dh_ke 1-RTT handshake, the 0-RTT handshake, and the record protocol. They verify these models using both ProVerif [START_REF] Blanchet | ProVerif 2.00: automatic cryptographic protocol verifier[END_REF] and CryptoVerif [START_REF] Blanchet | CryptoVerif: Computationally sound mechanized prover for cryptographic protocols[END_REF]. A limitation of their model is the informal way in which the separate guarantees for the three components are combined to justify the overall security of the protocol.

Blanchet [START_REF] Blanchet | Composition theorems for CryptoVerif and application to TLS 1.3[END_REF] introduces a new proof modularization framework in Cryp-toVerif, which bears significant similarities with the state-separating proof framework [START_REF] Brzuska | State separation for code-based game-playing proofs[END_REF] that our work is based on. The work also updates some of the model from draft-18 to draft-28; however, the model still assumes that all pre-shared keys are derived from resumption secrets and does not capture adaptively-created dishonest application PSKs, or the security of PSK binders.

Many other works focus on analysing certain properties of the TLS 1.3 handshake protocol. For instance, Arfaou et al. [4] specifically analyse the privacy of the TLS 1.3 psk_ke, dh_ke, and psk_dhe_ke handshakes. Fischlin et. al. [START_REF] Fischlin | Key confirmation in key exchange: A formal treatment and implications for TLS 1[END_REF] analyse the draft-06 TLS 1.3 handshake, and show that its modes achieve key confirmation in isolation. Fischlin et. al. [START_REF] Fischlin | Replay attacks on zero round-trip time: The case of the TLS 1.3 handshake candidates[END_REF] considers replay attacks against various drafts of TLS 1.3 0-RTT handshakes such as draft-14's psk_ke mode, similarly considering versions and modes in isolation. Other relevant papers on TLS handshake analysis are [START_REF] Krawczyk | A unilateral-to-mutual authentication compiler for key exchange (with applications to client authentication in TLS 1.3)[END_REF][START_REF] Drucker | Selfie: reflections on TLS 1.3 with PSK[END_REF][START_REF] Chen | Secure communication channel establishment: TLS 1.3 (over TCP fast open) vs. QUIC[END_REF].

The idea of analyzing a key schedule (rather than a key exchange protocol) is conceptually similar to the SIGMA-I pattern of Krawczyk [START_REF] Krawczyk | SIGMA: The "SIGn-and-MAc" approach to authenticated Diffie-Hellman and its use in the IKE protocols[END_REF] and Krawczyk and Wee [START_REF] Krawczyk | The OPTLS protocol and TLS 1.3[END_REF]. These works prove a reduction from key exchange security to key schedule security analogously to our companion paper [START_REF] Brzuska | Key exchange to key schedule reduction for TLS 1[END_REF].

Recent work also looked at the tightness of TLS 1.3 security proofs [START_REF] Diemert | On the tight security of TLS 1.3: Theoretically sound cryptographic parameters for real-world deployments[END_REF][START_REF] Davis | Tighter proofs for the SIGMA and TLS 1.3 key exchange protocols[END_REF]. Besides natural birthday bounds for collision resistance, our reductions avoid the common quadratic loss in the number of sessions. We remark however, that tightness was not the principal focus of our analysis.

Subsequent work to the present article [START_REF] Brzuska | Security analysis of the mls key derivation[END_REF] uses our methodology, e.g., our recursive handle structure and the style of encoding security guarantees in Log packages to analyse the key schedule security of the Messaging Layer Security (MLS) protocol whose conclusions were integrated into the IETF standard, e.g., [START_REF] Cornelissen | Pull request 453: Use the GroupContext to derive the joiner_secret[END_REF]. In the present paper, in addition to key techniques which were picked up by [START_REF] Brzuska | Security analysis of the mls key derivation[END_REF], we introduce a plethora of techniques to tackle indirect domain separation by late hashing of Diffie-Hellman shares and binders such as the notion of separation points and the Check component introduced in Section 4.3. In a similar way, the additional mapping step (Lemma 2, 4 and 5) handle redundancy not present in MLS. See Section 7 for simplifications of the TLS protocol which would allow for a much simpler analysis than the one presented in this article.

Lessons Learned & Afterthoughts on the Key Schedule

We now discuss changes to the key schedule that would improve its security and simplify its analysis and may be of independent interest for other protocols.

Simplify SODH The salted Diffie-Hellman computation extracts entropy from the DH secret and mixes it with the PSK-derived salt (which is under adversarial influence). A separate DH extraction, preferably hashing the (sorted) public shares together with the secret, followed by a dual PRF, would enable a proof based on the simpler and better understood Oracle Diffie-Hellman assumption. The hashing of shares would also remove the need to map DH secrets (currently computable from multiple pairs of shares), and would enable the use of a more abstract functionality such as a CCA-secure KEM (as in TLS 1.2 [START_REF] Bhargavan | Proving the TLS handshake secure (as it is)[END_REF]). These changes would thus also ease the integration of post-quantum secure primitives.

Eliminate PSK mapping Similarly, directly applying domain-separation for computations based on application and resumption PSKs via distinct labels would remove the need to map PSKs and argue via inclusion of binders at separation points indirectly. Both proposals follow the same design pattern: first sanitize input key materials to prevent malleability (DH secrets) and collisions (dishonest resumption PSKs and adversarially-chosen application PSKs).

Avoid Agile Assumptions Our development supports multiple hash algorithms without requiring any hash-agile assumptions, by observing that the hash functions currently used by TLS 1.3 have pairwise-distinct digest lengths. This is brittle, e.g. adding support for SHA3 with the same lengths as SHA2 would require to formally account for cross-algorithm collisions. This may be prevented by tagging the outputs of all extractors and KDFs with hash algorithms. Similarly, we may avoid the current need for agile (S)ODH assumptions by tagging group elements with both a group descriptor and a single extraction algorithm.

Prevent PSK Reflections Drucker and Gueron note that TLS 1.3 is subject to reflection attacks due to its symmetric use of PSKs [START_REF] Drucker | Selfie: reflections on TLS 1.3 with PSK[END_REF]. Hence, in our model, the same PSK handle may either be used by two parties, as intended, or by the same party acting both as a client and as a server. This is a security risk, inasmuch as applications may embed identity information in PSK identifiers to benefit from their early authentication. It may also enable key synchronization attacks and other variants of key compromise impersonation [START_REF] Bhargavan | Verified contributive channel bindings for compound authentication[END_REF] when identities are also symmetrical. When using PSKs, the standard unfortunately forbids certificate-based authentication, which would otherwise provide more detailed, role-specific identity information. At the key schedule level, it may be possible to enforce better separation by tagging PSK identifiers with roles.

Enforce Stronger Modularity Applied cryptographers often complain that, in TLS 1.2, the subtle interleaving of the handshake with the record layer hinders its analysis based on the well-established Bellare-Rogaway [START_REF] Bellare | Entity authentication and key distribution[END_REF] security model [START_REF] Jager | Authenticated confidential channel establishment and the security of TLS-DHE[END_REF]. While TLS 1.3 tries to enforce cleaner separation between handshake and record keys, it still fails in some important places. Notably, the handshake traffic secrets, meant to be released to the record layer (be it TLS, DTLS, or QUIC) are also used by the handshake to derive finished keys. Similarly, some handshake messages are encrypted under keys derived from application traffic secrets (e.g. New Session Ticket, carrying resumption PSKs, late client authentication, and key updates). This complicates the modeling of data stream security, as application data may be interleaved with handshake messages (e.g. the same QUIC packet may contain both data and session tickets). To prevent such issues, and many others, we suggest the RFC documents more explicitly its application interface and, in particular, recommends not to derive keys from keys released to the record layer.

A Proof of Theorem 2

Fig. 17 provides and overview over the proof of Theorem 2, which consists of 5 game-hops: From Gcore 0 (Fig. 17a) to Gcore Hash (Fig. 17b), to Gcore D (Fig. 17c), to Gcore Resalt (Fig. 17d) and finally to Gcore 1 (S) (Fig. 17i), as required by Theorem 2. The last step from Gcore Resalt and to Gcore 1 (S) is implemented by a hybrid argument which we prove in Appendix A, the hybrid games are illustrated in Fig. 17f, Fig. 17g and Fig. 17h. The first game hop (Lemma 6) idealizes collision resistence of the Hash b H package (which is used to hash transcripts).

Lemma 6 (Collision-Resistance).

Adv(A, Gcore 0 , Gcore Hash ) ≤Adv(A → R cr , Hash 0 H , Hash 1 H ),

where Fig. 17a and Fig. 17b define Gcore 0 and Gcore Hash , respectively, and R cr is marked in grey in Fig. 17b.

Proof. The proof of Lemma 6 is an instance of Lemma 1 with G 0 big = Gcore 0 , G 1 big = Gcore Hash , G 0 sml = Gacr hash,0 , G 1 sml = Gacr hash,1 and R = R cr . By Lemma 1, it suffices to show that Gcore 0 code ≡ R cr → Gacr hash,0

Gcore Hash code ≡ R cr → Gacr hash,1 )

Equation 7 follows by definition, since Fig. 15b defines Gks 0Map as the composition of R ch-map and Gcore 0 . Similarly, for Equation 6, Fig. 15c defines Gks 1Map as the composition of R ch-map and Gcore 1 (S core ).

The second game hop (Lemma 7) changes the pattern in the Log packages from Z to D and reduces to collision-resistance.

Lemma 7 (D-Pattern).

Adv(A, Gcore Hash , Gcore D ) ≤

Adv(A → R Z,xtr , Gacr xtr,b ) + Adv(A → R Z,xpd , Gacr xpd,b )+ Adv(A → R D,xtr , Gacr xtr,b ) + Adv(A → R D,xpd , Gacr xpd,b ),
where Gcore Hash is defined in Fig. 17b, Gcore D is defined in Fig. 17c, and the reductions R Z,xtr , R Z,xpd , R D,xpd and R D,xtr are provided in the full version [START_REF] Brzuska | Key-schedule security for the tls 1.3 standard[END_REF].

Proof (Proof Sketch). We (a) first idealize collision-resistance for xtr and xpd using the Rxtr and Rxpd implementation (cf. Step (b) relies on an inductive argument which we refer to as the co-dependance lemma. Namely, we show that once collisionresistance of the hash-function is idealized, a D abort on one key requires that there has been a collision before and therefore, since every collision requires a previous collision, no collision can occur. We defer the details of this argument to the full version.

The third game-hop (Lemma 8) now introduces a special abort symbol win whenever two different esalt handles point to the same key value, regardless of the honesty of the handles.

We show that the introduction of this special win abort can only increase the success probability of an adversary A by providing two adversaries A 0 and A 1 which behave almost identically to A, but in addition to the advantage which A has anyway, at least one out of A 0 and A 1 succeeds in benefitting from the win aborts. We defer the details of this proof to the full version. In a later game hop, we show that win aborts can be removed. Note that in this lemma, we do not bound the difference of an adversary between Gcore D and Gcore Resalt , but instead bound the difference between advantages, when comparing either of the games to Gcore 1 (S core ).

Lemma 8 (Resalt). For every adversary A and i ∈ {0, 1}, let A i be the adversary which behaves as A, but returns i when receiving a win abort. Then, Adv(A, Gcore D , Gcore 1 (S core ))

≤ max i∈{0,1}

Adv(A, Gcore Resalt , Gcore 1 (S core ))

where Gcore Resalt is defined in Fig. 17c.

Proof. First, observe that

Pr 1 = A → Gcore D ≤ Pr 1 = A 1 → Gcore Resalt (10)
because A 1 returns 1 whenever A returns 1 plus when receiving a win abort. Moreover,

Pr 1 = A → Gcore 1 (S) = Pr 1 = A 1 → Gcore 1 (S) , (11)
because Gcore 1 (S) never returns win. From here, the proof proceeds by case distinction. Case I.

Pr 1 = A → Gcore D ≥ Pr 1 = A → Gcore 1 (S core ) (12)
Inequality 9 holds because Adv(A, Gcore D , Gcore 1 (S core ))

Eq. 12 = Pr 1 = A → Gcore D -Pr 1 = A → Gcore 1 (S core )

Eq. 10&11

≤ Pr 1 = A 1 → Gcore D -Pr 1 = A 1 → Gcore 1 (S core )
Case II consists of Inequality 12 being the other way round. The proof is analogous.

With the collision-freeness of esalt at hand, we can (globally) apply the Gsodh assumption to idealize Diffie-Hellman secrets (Lemma 9). The proof is brief and straightforward and included after the lemma statement.

Lemma 9 (SODH Lemma).

Adv(A, Gcore Resalt , Gcore SODH ) = Adv(A → R sodh , Gsodh b ),

where Fig. 17c and Fig. 17d define Gcore Resalt and Gcore SODH , respectively, and R sodh is marked in grey in Fig. 18a.

Proof. The proof of Lemma 9 is an instance of Lemma 1 with G 0 big = Gcore Resalt , G 1 big = Gcore SODH , G 0 sml = Gsodh 0 , G 1 sml = Gsodh 1 and R = R sodh . By Lemma 1, it suffices to show that Gcore Resalt code ≡ R sodh → Gsodh 0 (13)

Gcore SODH code ≡ R sodh → Gsodh 1 (14)
Equation 13 follows by observing that the graph of R sodh → Gsodh 0 (Fig. 18a with b = 0) is identical to the graph of Gcore Resalt (Fig. 17c) by inspecting the different layouts of the graphs chosen in the two figures represengint them.

Similarly, for Equation 14, one can observe that the graph of R sodh → Gsodh 1 (Fig. 18a with b = 1) is equal to the graph of Gcore SODH (Fig. 17d).

At this point we use a hybrid argument (Lemma 10) to idealize pseudorandomness of all xtr and xpd blocks. We provide the proof of Lemma 10 in Appendix B.

Lemma 10 (Hybrid Lemma).

Adv(A, Gcore SODH , Gcore ki ) ≤

where Fig. 18f defines R n, for n ∈ XPN \ {psk , esalt} and Fig. 18e defines R es, .

Finally, we use preimage-resistance (Lemma 11) to remove the rewarding aborts introduced in Lemma 8.

Lemma 11 (Pre-image-resistance).

Adv(A, Gcore ki , Gcore 1 (S core )) ( 16)

≤Adv(A → R esalt,pi , Gpi R esalt , Gpi D esalt ) + Adv(A → R O * ,pi , Gpi D O * , Gpi F O * ),
where R esalt,pi is defined in Fig. 18b and R O * ,pi is defined in Fig. 18c. From Eq. 17

Fig. 2 :

 2 Fig. 2: Game Gxpd b n, for b ∈ {0, 1}

  Finally, Gxpd b n, is structured in individual components which we call packages. Definition 3 (Package). A package M consists of a set of oracles [→ M] = {O1, .., Ot}, specified by pseudo-code and operating on a set of state variables Σ, specified on the top of each package description. All other variables used by oracles are temporary and their values are forgotten after each call. The oracles of M may depend on oracles [M →] = {O 1, .., O t }, i.e., make calls to oracles in [M →]. We say that a package M is stateless if Σ

Fig. 3 :

 3 Fig. 3: Xpd package

Fig. 5 :

 5 Fig. 5: Gcr f-alg,b code.

Fig. 5

 5 Fig. 5 defines the collision-resistance game Gcr f-alg,b for a given function f-alg, where f ∈ {hash, xtr, xpd} and alg ∈ H which TLS 1.3 currently defines as

Fig. 6 :

 6 Fig. 6: xpd assumptions

Fig. 7 :

 7 Fig. 7: xtr Pseudorandomness Assumption

  1 as, ), where Fig. 7b-7d define the games Gxtr1 b es , Gxtr2 b hs and Gxtr b as and Definition 1 defines advantage. 3.4 Salted ODH GET esalt,0..d Xtr hs,0..d Q dh UNQ dh NKey dh Q hs UNQ hs Key hs,0..d SET hs,0..d GET hs,0..d XTR hs,0..

Fig. 8 :

 8 Fig. 8: Game Gsodh b (top), package Dh (bottom)

Fig. 9 :levelFig. 10 :

 910 Fig. 9: Pre-image resistance assumptions

Fig. 11 :

 11 Fig.11: Key schedule security games with internal keys I * , output keys O * and XPN , the set of key names produced by xpd. We write 0K n as an abbreviation for Nk n → L Z n . We initialize K and Nk n with suitable 0 values (cf. Section 2.1).

Fig. 12 :

 12 Fig. 12: Code of Check

  Fig. 18d) instead of Xtr and Xpd to construct reductions R Z,xtr and R Z,xpd to agile collision-resistance (cf. Section 3.1) of xtr and xpd, respectively. (b) Then, we introduce D abort patterns in a perfect equivalence step and then (c) de-idealize collision-resistance of xtr and xpd analogously to (a).

  → R es, , Gxtr b es, ) + Adv(A → R hs, , Gxtr b hs, ) + Adv(A → R as, , Gxtr b as, ) + n∈XPR Adv(A → R n, , Gxpd b n, ) ,

Proof.

  The proof of Lemma 11 consists of two instances of Lemma 1. For the first part of the proof, we useG 0 big = Gcore ki , G 1 big = R esalt,pi → Gpi D esalt , G 0 sml = Gpi R esalt , G 1 sml = Gpi D esalt and R esalt,pi . Now, Gcore ki code ≡ R esalt,pi → Gpi Resalt follows by carefully inspecting the graph layouts in Fig.17hand Fig.18b.G 1 big code ≡ R → G 1sml is true by definition. By Lemma 1, we thus obtainAdv(A, Gcore ki , R esalt,pi → Gpi D esalt )(17)=Adv(A → R esalt,pi , Gpi R esalt , Gpi D esalt )For the second instance of Lemma 1, we useG 0 big = R esalt,pi → Gpi R esalt , G 1 big = Gcore 1 (S core ), G 0 sml = Gpi D O * , G 1 sml = Gpi F O * and R O * ,pi . R esalt,pi → Gpi D esalt is code equivalent to R O * ,pi → Gpi FO * by carefully comparing Fig.18b(with P = D) and Fig.18c (with P= D). Gcore 1 (S core ) is code-equivalent to R O * ,pi → Gpi DO * by comparing Fig.18c(with P = F) and Fig.17i. By Lemma 1, we obtain Adv(A, R esalt,pi → Gpi D esalt , Gcore 1 (S core )) (18)=Adv(A → R O * ,pi , Gpi D O * , Gpi F O * )

6 ≤ 7 ≤R 8 ≤R 1 =0 11 ≤R 1 =0

 6781111 and 18, we obtain Inequality 16 via triangle inequality.From Lemma 6-11, we obtain Theorem 2 by triangle inequalities, included below for completeness. All sums over R sum over R ∈ {R cr , R Z,xtr , R Z,xpd , R D,xtr , R D,xpd } and use matching f ∈ {hash, xtr, xpd} Adv(A, Gcore 0 , Gcore 1 (S core ))Lm. Adv(A → R cr , Gacr hash,b ) + Adv(A, Gks Hash , Gcore 1 (S core )) Lm. Adv(A → R, Gacr f,b ) + Adv(A, Gcore D , Gcore 1 (S core )) Lm. Adv(A → R, Gacr f,b ) + max i∈{0,1} Adv(A i , Gcore Resalt , Gcore 1 (S core )) Lm. 9 = R Adv(A → R, Gacr f,b ) + max i∈{0,1} Adv(A i → R sodh , Gsodh b ) + Adv(A i , Gcore SODH , Gcore 1 (S core )) Lm. 10 ≤ R Adv(A → R, Gacr f,b ) + max i∈{0,1} Adv(A i → R sodh , Gsodh b ) + Adv(A i , Gcore ki , Gcore 1 (S core ))+ d-Adv(A i → R es, , Gxtr b es, ) + max i∈{0,1} Adv(A i → R hs, , Gxtr b hs, )+ Adv(A i → R as , Gxtr b as, ) + n∈XPR Adv(A i → R n, , Gxpd b n, ) Lm. Adv(A → R, Gacr f,b ) + max i∈{0,1} Adv(A i → R sodh , Gsodh b ) + Adv(A i → R esalt,pi , Gpi b esalt ) + Adv(A i → R O * ,pi , Gpi b O * )+ d-Adv(A i → R es, ,Gxtr b es, ) + Adv(A i → R hs, , Gxtr b hs, )+ Adv(A i → R as , Gxtr b as, ) + n∈XPR Adv(A i → R n, , Gxpd b n, ) ,

  1 O * ,0..d and Log O * packages (cf. Section 2.3) constitute the ideal functionality. Namely, the Key 1 O * ,0..d package samples a uniformly random key for handles which correspond to honest keys with a name n ∈ O * and some level 0 ≤ ≤ d. The Log O * package, in turn, ensures that each handle corresponds to a different key, modeling key uniqueness for both honest and dishonest keys.

These two oracles in particular are necessary for composition: Note that the main oracles the adversary interacts with are subscripted by a name n and a level while the Q and UNQ oracles only take the name n as subscript. We will share the same

XTRn, (h1, h2) IdealizationOrder(ks, <)

Fig. 19: Idealization Order

The proof of Lemma 10 is a hybrid argument over all levels as well as over the derivation graph.

Here, we need to specify the order in which keys are idealized, i.e., replaced by random keys. This order needs to satisfy the (a) all parents have been idealized before and (b) that when n is idealized in a step then all siblings are idealized, too. We refer to such an order as idealization order and show that each TLS-like key schedule indeed has an idealization order (as is required for the proof of Lemma 10). Definition 14 (Idealization Order). Let ks = (N, label, prntn) be a TLS-like key schedule and m ∈ N. An Idealization Order io for ks is a total order on m subsets of N together with a sequence of names n 1 , . . . , n m-1 such that Claim (Idealization Order). Every TLS-like key schedule has an idealization order.

Proof. Let < be a total order on N and consider the algorithm in Fig. 19 which constructs the idealization computing min with respect to <. Firstly, the assignment in line 4 is well-defined: Let n be in N \ io[c]. Since n is reachable from psk (Definition 11), there is a path from psk to n. As there is a first element on this path not in io Using the existence of idealization order Claim B.1, the proof of Lemma 10 consists of the following lemmata whose proofs are a direct application of Lemma 1.

Lemma 12 (XTR1).

For n c = psk , we have that Adv(A, Gcore hyb: ,c , Gcore hyb: ,c+1 ) ≤ Adv(A → R es, , Gxtr b es, ),

where R es, is defined in Fig. 18e.

Lemma 13 (XTR2). For n c = esalt Adv(A, Gcore hyb: ,c , Gcore hyb: ,c+1 ) ≤ Adv(A → R hs, , Gxtr b hs, ),

where R hs, is defined analogously to reduction R es, in Fig. 18e.

Lemma 14 (XTR3). For n c = hsalt, we have that Adv(A, Gcore hyb: ,c , Gcore hyb: ,c+1 ) ≤ Adv(A → R as, , Gxtr b as, ),

where R as, is defined analogously to reduction R es, in Fig. 18e.

Lemma 15 (XPD). For chldrnop(n c ) = xpd, we have that Adv(A, Gcore hyb: ,c , Gcore hyb: ,c+1 )

where Game Gxpd b n, for b ∈ {0, 1} is defined in Fig. 2 for n / ∈ {psk , esalt}, in Fig. 6b for n = esalt and in Fig. 6a for n = psk . For n / ∈ {esalt, esalt}, where R n, is defined in Fig. 18f. The reductions for n ∈ {psk , esalt} are defined analogously.

From Lemma 12, Lemma 13, Lemma 14, and Lemma 15 we obtain Lemma 10 by a 2-dimensional hybrid argument. First observe:

Gcore SODH = Gcore hyb:0 Gcore hyb:d = Gcore ki

Gcore hyb: = Gcore hyb: ,1 Gcore hyb: +1 = Gcore hyb: ,m

From there, we obtain Adv(A, Gcore SODH , Gcore ki )

Eq. 19

= Adv(A, Gcore hyb:0 , Gcore hyb:d ) tele.sum.