Key-Schedule Security for the TLS 1.3 Standard

Abstract

Transport Layer Security (TLS) is the cryptographic backbone of secure communication on the Internet. In its latest version 1.3, the standardization process has taken formal analysis into account both due to the importance of the protocol and the experience with conceptual attacks against previous versions. To manage the complexity of TLS (the specification exceeds 100 pages), prior reduction-based analyses have focused on some protocol features and omitted others, e.g., included session resumption and omitted agile algorithms or vice versa.

This article is a major step towards analysing the TLS 1.3 key establishment protocol as specified at the end of its rigorous standardization process. Namely, we provide a full proof of the TLS key schedule, a core protocol component which produces output keys and internal keys of the key exchange protocol. In particular, our model supports all key derivations featured in the standard, including its negotiated modes and algorithms that combine an optional Diffie-Hellman exchange for forward secrecy with optional pre-shared keys supplied by the application or recursively established in prior sessions.

Technically, we rely on state-separating proofs (Asiacrypt ’18) and introduce techniques to model large and complex derivation graphs. Our key schedule analysis techniques have been used subsequently to analyse the key schedule of Draft 11 of the MLS protocol (S &P ’22) and to propose improvements.

1 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 [9], LogJam [2] for export Diffie-Hellman, WeakDH for ill-chosen groups, and exploits against Mantin biases of RC4 [21]); the RSA key encapsulation (e.g. the ROBOT [19] 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 [38], Lucky13 [3]); the weak signature over nonces allowing protocol version downgrades (e.g. DROWN [5] and POODLE); attacks on other negotiated parameters [11], the key exchange logic (e.g. the cross-protocol attack of [49] and 3SHAKE [12]); exploitations of collisions on the hash transcript (e.g. SLOTH [15]). 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 [51]. For TLS 1.3, it decided to address security upfront by welcoming feedback from various cryptographic efforts, including symbolic [29, 30] and computational protocol models [34, 35, 48], 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 [47], 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 Sect. 6 for a more detailed discussion of related work. Since final adoption, further questions have been raised about pre-shared keys, potential reflection attacks [37], 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 [42], 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. [52] (extending the work of Fischlin et al. [40] on stream-based channels), Badertscher et al. [6], and Bhargavan et al. [32], 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 $\tau _ c$ are derived from $k_{ cht }$, $k_{ ae2 }$ and $\tau _ s$ are derived from $k_{ sht }$, and $k_{ ae3 }$ is derived from $k_{ sat }$. We color digests and keys in alternating and to clarify digest-key dependency. E.g., label and digest is used to derive . (Color figure online)

1.1 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_i^{x_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_{i_0}^y$ (including the group description) and the label $label _{j_0}$ of the chosen PSK. The remaining messages consist of server certificate, signature ($\text {C}(pk),\text {CV}(\sigma )$), key confirmation messages in the forms of messages authentication codes (MACs) $\tau _s$ and $\tau _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 [45], which uses HMAC [7] to implement extract ($\textsf{xtr}$) and expand ($\textsf{xpd}$) operations. In addition, the key schedule makes calls to $\textsf{xpd}$ to expand keys into further subkeys. The key schedule thus consists of a collection of $\textsf{xtr}$ an $\textsf{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 $\textsf{xtr}$ in the early phase and $k_{ dh }$ in the $\textsf{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.

1.2 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 [25], 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 [29].

Outline. We introduce our overall technical approach in Sect. 2. We define our assumptions for collision-resistance, pseudorandomness and pre-image resistance in Sect. 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 [23]. Finally, Sect. 7 includes proposals for (late) changes to the TLS 1.3 standard.

2 Technical Approach

2.1 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 $\textsf{xtr}$ and $\textsf{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$.

$$\begin{aligned} \begin{array}{ll} \mathsf {\textsf{dh}}\langle {\textsf{sort}(X,Y)}\rangle &{} \text {Diffie-Hellman secret}\\ h=\textsf{psk}\langle ctr , alg \rangle &{} \text {application PSK}\\ \textsf{noDH}\langle alg \rangle &{} \text {fixed }0^{\textsf{len}( alg )}\text { Diffie-Hellman secret}\\ \mathsf {\textsf{noPSK}}\langle { alg }\rangle &{} \text {fixed }0^{\textsf{len}( alg )}\text { PSK}\\ \textsf{0salt} &{} \text {fixed }0\text { salt}\\ \textsf{0ikm}\langle {alg}\rangle &{} \text {fixed }0^{\textsf{len}( alg )}\text { initial key material (IKM)} \\ \end{array} \end{aligned}$$

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

$$\begin{aligned} \;\mathsf {\textsf{xtr}}\langle {\textit{name}, \textit{left parent handle},\textit{right parent handle}}\rangle .\\ \mathsf {\textsf{xpd}}\langle {\textit{name}, \textit{label}, \textit{parent handle},\textit{other arguments}}\rangle . \end{aligned}$$

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 } = \textsf{xpd}\langle {cet,{{\texttt {c e traffic}}},h_{ es }, t _{ es }}\rangle $$

where $t _{ es }$ is the transcript of the protocol messages exchanged so far, and ‘${{\texttt {c e traffic}}}$’ is the constant byte string label prescribed in the RFC [53] for this derivation step.

Agility. Our model is agile, i.e., it supports multiple algorithms. Thus, we tag the handles $h=\textsf{psk}\langle ctr , alg \rangle$, $\mathsf {\textsf{noPSK}}\langle { alg }\rangle$ and $\textsf{0ikm}\langle {alg}\rangle$ 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 } = \textsf{xpd}(k_{ es },{{\texttt {c e traffic}}}, d _{ es }),$$

the agile $\textsf{xpd}$ function can retrieve the correct hash algorithm $alg$ to use within $\textsf{hmac}$ from the key’s tag. We write $\textsf{alg}(h_{ cet })$ for the algorithm descriptor of $h_{ cet }$ and $\textsf{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 $\textsf{len}(h_{ cet })$ as an alias for $\textsf{len}(\textsf{alg}(h_{ cet }))$.

Note that we introduced handles $\textsf{0ikm}\langle {alg}\rangle$ for the dummy key value $0^{\textsf{len}(alg)}$ as well as $\textsf{0salt}$ for the 1-bit-long 0-key. This is because $\textsf{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 ${{\texttt {resumption}}}$ label. We write $\textsf{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 $\textsf{prntn}(n)$. In the case of $\textsf{xpd}$, the key is only derived from one key and thus, in this case, $\textsf{prntn}(n)=(n_1,\bot )$. Conversely, we refer by $\textsf{chldrnn}(n_1)$ to the set of all key names which are derived from $n_1$. In particular, if $\textsf{prntn}(n)=(n_1,\bot )$, then $n\in \textsf{chldrnn}(n_1)$. We refer to all names which share a parent with n as $\textsf{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 $\textsf{noDH}\langle alg \rangle$ Diffie-Hellman handle signals a psk_ke mode, while a $\mathsf {\textsf{noPSK}}\langle { alg }\rangle$ PSK handle signals a dh_ke mode.

2.2 Application Key Registration and 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.

2.3 State-Separating Proofs (SSPs)

Fig. 2.

Game $\texttt{Gxpd}^b_{ n ,\ell }$ for $b\in \{0,1\}$

In the following we use the the pseudorandomness game $\texttt{Gxpd}^0_{ n ,\ell }$ for the $\textsf{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 $\mathcal {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 $\texttt{G}^0$ and $\texttt{G}^1$ with identical interfaces and we measure the success probability of any such adversary $\mathcal {A}$ and call it advantage.

Definition 1 (Advantage)

For adversary $\mathcal {A}$, we define the advantage

$$\begin{aligned} \textsf{Adv}(\mathcal {A};\texttt{G}^0,\texttt{G}^1):=\left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{G}^0\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{G}^1\right] \right|. \end{aligned}$$

In particular, for the pseudorandomness game $\texttt{Gxpd}^b_{ n ,\ell }$ for $\textsf{xpd}$, the analogous definition is as follows.

Definition 2 (XPD)

For adversary $\mathcal {A}$, we define the $\textsf{xpd}$ pseudorandomness advantage $\textsf{Adv}(\mathcal {A},\texttt{Gxpd}^0_{ n ,\ell },\texttt{Gxpd}^1_{ n ,\ell })$ as

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^0_{ n ,\ell }\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^1_{ n ,\ell }\right] \right|, \end{aligned}$$

where Fig. 2 defines $\texttt{Gxpd}^0_{ n ,\ell }$.

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 $\texttt{Gxpd}^b_{ n ,\ell }$ consists on first registering input values using the $\textsf{SET}_{n_1,\ell }$ oracle, executing key derivation using the $\textsf{XPD}_{ CN ,\ell }$ oracle and finally retrieving and testing the output using the $\textsf{GET}_{n,\ell }$ oracle. In addition, the adversary gets access to auxiliary oracles, namely the $\textsf{HASH}$ oracle modeling a cryptographic hash function as well as the $\textsf{Q}$ and $\textsf{UNQ}$ oracles.¹ Finally, $\texttt{Gxpd}^b_{ n ,\ell }$ is structured in individual components which we call packages.

Definition 3 (Package)

A package $\texttt{M}$ consists of a set of oracles $[\rightarrow \texttt{M}]=\{\textsf{O1},..,\textsf{Ot}\}$, specified by pseudo-code and operating on a set of state variables $\varSigma$, 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 $\texttt{M}$ may depend on oracles $[\texttt{M}\rightarrow ]=\{\mathsf {O'1},..,\mathsf {O't'}\}$, i.e., make calls to oracles in $[\texttt{M}\rightarrow ]$. We say that a package $\texttt{M}$ is stateless if $\varSigma =\emptyset$. We say that a package $\texttt{M}$ is a game if $[\texttt{M}\rightarrow ]=\emptyset$.

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 $\texttt{Gxpd}^b_{ n ,\ell }$ can be obtained by inlining all internal oracle calls. With the concept of packages we can now discuss the individual parts of $\texttt{Gxpd}^b_{ n ,\ell }$. $\texttt{Xpd}_{ CN ,\ell }$ is a parallel composition of $\texttt{Xpd}$$_{ n ,\ell }$ for all children of $n_1$ exposing the oracles $\textsf{XPD}_{ n ,\ell }$ for $n \in CN$, we write $\textsf{XPD}_{ CN ,\ell }$ as shorthand for these oracles. The $\texttt{Xpd}_{ CN ,\ell }$ packages are the only stateless packages in the game, indicated by the white color as opposed to the gray of stateful packages (Fig. 2).

Fig. 3.

$\texttt{Xpd}$ package

The $\textsf{XPD}_{ n ,\ell }$ oracle of package $\texttt{Xpd}$$_{ n ,\ell }$ (Fig. 3) computes a new handle $h\leftarrow \textsf{xpd}\langle n, label ,h_1, args \rangle$ alongside a new key $k\leftarrow \textsf{xpd}(k_1,( label ,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 $\texttt{Key}$$^b_{n,\ell }$ packages using the $\textsf{GET}$ and $\textsf{SET}$ oracles. Here we can distinguish the upper $\texttt{Key}$$^1_{n_1,\ell }$ package and the lower $\texttt{Key}$$^b_{ CN ,\ell }$ packages (for all n in $CN$). We defer discussion about the $\textsf{Q}$ and $\textsf{UNQ}$ oracle calls to the description of the $\texttt{Log}$ package.

The upper $\texttt{Key}$$^1_{n_1,\ell }$ package offers oracle $\textsf{SET}_{n_1,\ell }(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 $\ell$ of this key package and—modeling algorithmic agility—verifies that the algorithm tag matches the value of the key, and else, $\textsf{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 $\leftarrow$ used for assignments. Finally the key is stored in this package’s state and the handle returned to the caller. The $\textsf{GET}$ oracle simply restores algorithm tagging on the key value and returns it to the caller (in this case the $\texttt{Xpd}$ package). The lower $\texttt{Key}$$^b_{ CN ,\ell }$ packages work the other way round in that they expose the $\textsf{GET}$ oracle to the adversary while the $\textsf{SET}$ oracle is used by $\texttt{Xpd}$. We encode the distinguishing task for the adversary in the $\texttt{Key}_{ CN ,\ell }^b$ package: In $\texttt{Gxpd}^0_{ n ,\ell }$ ($b=0$), the keys returned from the $\textsf{GET}$ oracle of the $\texttt{Key}$$^0_{ CN ,\ell }$ is honestly computed based on the input keys while in the ideal game $\texttt{Gxpd}^1_{ n ,\ell }$ the values of honest keys are sampled in the $\texttt{Key}$ package ignoring the value computed by $\texttt{Xpd}$.

Fig. 4.

Code for the $\texttt{Key}$ and $\texttt{Log}$. In addition we use $\texttt{Nkey}$ for a single key package that answers queries for all levels from the same table and $\texttt{0key}$ for a $\texttt{NKey}$ package which consistently answers with the constant all-zeros key.

Finally, queries $\textsf{Q}_n$ and $\textsf{UNQ}_n$ to the $\texttt{Log}$$_n$ package (Fig. 4) model collisions. The $\textsf{Q}$ query simply returns if a handle is re-used while $\textsf{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. Sect. 5.3 for their use. We use the ${\textbf {throw }}$ notation here to allow special symbols in addition to $abort$ which is also used by $\textsf{assert}$. In the game $\texttt{Gxpd}^b_{ n ,\ell }$, 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. $\infty$ allows collisions between Diffie-Hellman secrets (the adversary can construct colliding values via $X^zY = 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.

3 Assumptions

3.1 Collision-Resistance

Fig. 5.

$\texttt{Gcr}^{\textsf{f}\text {-} alg , b}$ code.

Figure 5 defines the collision-resistance game $\texttt{Gcr}^{\textsf{f}\text {-} alg ,b}$ for a given function $\textsf{f}\text {-} alg$, where $\textsf{f}\in \{\textsf{hash},\textsf{xtr},\textsf{xpd}\}$ and $alg \in \mathcal{H}$ which TLS 1.3 currently defines as

$$\begin{aligned} \mathcal{H}= \{\texttt {sha256} ,\texttt {sha384},\texttt {sha512}\} \end{aligned}$$

(see FIPS 180-2). The $\textsf{HASH}$ oracle takes as input a text t from the domain of $\textsf{f}\text {-} 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.

Definition 4 (Collision-Resistance)

For an adversary $\mathcal {A}$, a function $\textsf{f}\in \{\textsf{hash},\textsf{xtr},\textsf{xpd}\}$ and algorithm $alg \in \mathcal{H}$, define collision-resistance advantage $\textsf{Adv}(\mathcal {A},\texttt{Gcr}^{\textsf{f}\text {-} alg ,0},\texttt{Gcr}^{\textsf{f}\text {-} alg ,1})$ is

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gcr}^{\textsf{f}\text {-} alg ,0}\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gcr}^{\textsf{f}\text {-} alg ,1}\right] \right|. \end{aligned}$$

Agile Collision-Resistance. It is convenient to define the agile collision-resistance game $\texttt{Gacr}^{\textsf{f},b}$ as well, where $\textsf{f}\in \{\textsf{hash},\textsf{xtr},\textsf{xpd}\}$ takes tagged inputs, i.e., $\textsf{hash}$ takes a single input, tagged with the algorithm to use, $\textsf{xpd}$ takes three inputs $(k, label , args )$, where k is tagged, and $\textsf{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 $\textsf{HASH}$ with values in the domain of the agile functions. We write $\texttt{Hash}^b:=\texttt{Gacr}^{\textsf{hash},b}$. See Sect. 2.1 for further discussion of tagging.

3.2 Pseudorandomness of $\textsf{xpd}$

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

Fig. 6.

$\textsf{xpd}$ assumptions

XPD to Derive PSK. For $n = psk$ (cf. Fig. 6a), the layer index increases from $\ell$ to $\ell +1$. Thus, the $\textsf{XPD}_{ psk ,\ell }$ oracle reads keys via $\textsf{GET}_{ rm ,\ell }$ queries, but writes keys using the level $\ell +1$ query $\textsf{SET}_{ psk ,\ell +1}$. Another difference in $\texttt{Gxpd}^b_{ psk ,\ell }$ compared to the general $\texttt{Gxpd}^b_{ n ,\ell }$ is that the lower $\texttt{Log}$$^{D1}_{ psk }$ package uses a D1 pattern for logging which ignores level 0 $\textsf{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 $\textsf{XPD}_{ psk ,\ell }$ writes only on level $\ell +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. Sect. 4.1. Finally, for deriving the psk, no hash-operation is performed.

Definition 5 (XPD for psk)

For an adversary $\mathcal {A}$, we define the $\textsf{xpd}$ pseudorandomness advantage for $psk$ derivation $\textsf{Adv}(\mathcal {A},\texttt{Gxpd}^0_{ psk ,\ell },\texttt{Gxpd}^1_{ psk ,\ell })$ as

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^0_{ psk ,\ell }\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^1_{ psk ,\ell }\right] \right| \end{aligned}$$

XPD to Derive Esalt. For $n = esalt$, the lower $\texttt{Log}$$_{ esalt }^{R}$ 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 $\mathcal {A}$, we define the $\textsf{xpd}$ pseudorandomness advantage for $esalt$ derivation $\textsf{Adv}(\mathcal {A},\texttt{Gxpd}^0_{ esalt ,\ell },\texttt{Gxpd}^1_{ esalt ,\ell })$ as

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^0_{ esalt ,\ell }\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gxpd}^1_{ esalt ,\ell }\right] \right|. \end{aligned}$$

Fig. 7.

$\textsf{xtr}$ Pseudorandomness Assumption

3.3 Pseudorandomness of $\textsf{xtr}$

The TLS 1.3 key schedule performs three $\textsf{xtr}$ operations (cf. Fig. 1), and the modeling is analogous to the XPD assumptions, except that for the early secret $es$, $\textsf{xtr}$ security relies on the $psk$ which is the right input to $\textsf{xtr}$, and for the application secret $as$, $\textsf{xtr}$ security relies on $esalt$ which is the left input to $\textsf{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 $\textsf{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 $\texttt{Xtr}$$^b_{hs,\ell }$ 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 $\mathcal {A}$, level $\ell \in \mathbb {N}_0$, we define the $\textsf{xtr}$ pseudorandomness advantage for $es$ as $\textsf{Adv}(\mathcal {A},\texttt{Gxtr1}^0_{ es ,\ell },\texttt{Gxtr1}^1_{ es ,\ell })$, the pseudorandomness advantage for $hs$ as $\textsf{Adv}(\mathcal {A},\texttt{Gxtr2}^0_{ hs ,\ell },\texttt{Gxtr2}^1_{ hs ,\ell })$ and the pseudorandomness advantage for $as$ as $\textsf{Adv}(\mathcal {A},\texttt{Gxtr3}^0_{ as ,\ell },\texttt{Gxtr3}^1_{ as ,\ell })$, where Fig. 7b–7d define the games $\texttt{Gxtr1}^b_{ es }$, $\texttt{Gxtr2}^b_{ hs }$ and $\texttt{Gxtr}^b_{ as }$ and Definition 1 defines advantage.

Fig. 8.

Game $\texttt{Gsodh}^b$ (top), package $\texttt{Dh}$ (bottom)

3.4 Salted ODH

Our salted oracle Diffie-Hellman assumption (SODH) is a stronger variant of the oracle Diffie-Hellman assumption introduced by Abdalla et al. [1] and the PRF oracle Diffie-Hellman assumption studied by Brendel et al. [20]. 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 hash-functions 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 $\texttt{Gsodh}^b$ game (cf. Fig. 8) allows the adversary to generate honest Diffie-Hellman shares via $\textsf{DHGEN}$, to combine them (or an honest and a dishonest share) into a Diffie-Hellman secret via $\textsf{DHEXP}$ and to derive keys from them via $\textsf{XTR}_{n,\ell }$ for an arbitrary level $\ell \in \{0,..,d\}$. Oracle $\textsf{GET}_{n,\ell }$ then allows to retrieve the derived keys. Note that pseudorandomness is modeled, this time, by a bit in the $\texttt{Xtr}^b_{n,\ell }$ package (Fig. 7a).

Definition 8 (SODH)

For an adversary $\mathcal {A}$, we define the Salted Oracle Diffie Hellman (SODH) advantage $\textsf{Adv}(\mathcal {A},\texttt{Gsodh}^0,\texttt{Gsodh}^1):=$

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gsodh}^0\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gsodh}^1\right] \right|, \end{aligned}$$

3.5 Pre-image Resistance for $\textsf{xpd}$

Pseudorandomness and collision resistance of $\textsf{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 [23, Lemma E.7] and in this conference version rely on pre-image resistance as a separate assumption for convenience.

Fig. 9.

Pre-image resistance assumptions

Definition 9 (Pre-image resistance advantages)

For an adversary $\mathcal {A}$ and level $\ell \in \mathbb {N}_0$ we define the pre-image resistance advantage for deriving keys in $O^*$ (a set to be specified later) $\textsf{Adv}(\mathcal {A},\texttt{Gpi}^D_{O^*},\texttt{Gpi}^F_{O^*}):=$

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gpi}^D_{O^*}\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gpi}^F_{O^*}\right] \right|, \end{aligned}$$

the pre-image resistance advantage for deriving keys with the same parent as $esalt$ by $\textsf{Adv}(\mathcal {A},\texttt{Gpi}^D_{ esalt },\texttt{Gpi}^F_{ esalt }):=$

$$\begin{aligned} \left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gpi}^D_{ esalt }\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gpi}^F_{ esalt }\right] \right|. \end{aligned}$$

Figure 9b and Fig. 9b define $\texttt{Gpi}^P_{O^*}$ and $\texttt{Gpi}^P_{ esalt }$.

Our modular assumptions for $\textsf{xpd}$ and $\textsf{xtr}$ are agile, multi-instance security assumptions with registration of dishonest keys. They reduce to their non-agile, single-instance, monolithically written counterparts with a security loss equal to the number of honest keys. Since TLS 1.3 currently only supports hash-algorithms of different length, indeed, our agile assumptions for $\textsf{xtr}$ and $\textsf{xpd}$ reduce to non-agile assumptions. In turn, we can only reduce our modular agile SODH assumption to an agile monolithic SODH assumption, because TLS 1.3 indeed requires such a strong, agile SODH assumption (cf. Sect. 3.4 and Sect. 7) for further discussion. See full version [23, Appendix E] for the reduction proofs.

4 Key Schedule

We reason about the TLS 1.3 key schedule in terms of its three elementary operations extract ($\textsf{xtr}$), expand ($\textsf{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.

4.1 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 $\textsf{prntn}$ function, cf. Sect. 2.1), a key schedule has a function $\textsf{label}$ which maps the name and a resumption bit to a derivation label. We conveniently model $\textsf{hmac}$ operations by using $\textsf{xpd}$ with empty label as an alias for $\textsf{hmac}$. By sound cryptographic practice, a key should be either used for $\textsf{xpd}$ or for $\textsf{hmac}$ but not both, so if a node has an empty label, it is not allowed to have siblings. Similarly, $\textsf{xtr}$ operations only yield a single child, and the multiple children of $\textsf{xpd}$ operations are derived using distinct labels.

Definition 10 (Key Schedule Syntax)

A key schedule $ks = (N, \textsf{label}, \textsf{prntn})$ consists of a set of names N and two functions

$$\begin{aligned}&\textsf{label}:&N\times \{0,1\}&\rightarrow \{0,1\}^{96} \cup \;\left\{ \bot \right\} \\&\textsf{prntn}:&N&\rightarrow (N \cup \bot ) \times (N \cup \bot ) \end{aligned}$$

with the previously described restrictions.

Fig. 10.

Parent names $\textsf{prntn}$ in TLS 1.3

Figure 10 describes the $\textsf{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 $\textsf{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 $\textsf{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 TLS-like 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, \textsf{label}, \textsf{prntn})$ is TLS-like if its $\textsf{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 $\textsf{prntn}$ function maps 0salt, $dh$ and $0ikm$ to $(\bot ,\bot )$, maps $es$, $hs$ and $as$ according to Fig. 10, maps $psk$ to $( rm ,\bot )$ and each of the remaining names $n$ to some pair $( n _1,\bot )$ with $n _1\ne \bot$.

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

4.2 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 [26] approach to key exchange), where the ideal game is defined as a composition of a simulator $\mathcal {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).

Fig. 11.

Key schedule security games with internal keys $I^*$, output keys $O^*$ and $XPN$, the set of key names produced by $\textsf{xpd}$. We write $\texttt{0K}_n$ as an abbreviation for $\texttt{Nk}_n\rightarrow \texttt{L} _n^Z$. We initialize $\texttt{K}$ and $\texttt{Nk}_n$ with suitable 0 values (cf. Sect. 2.1).

Table 1. Notation

Concretely, in our ideal game $\texttt{Gks}^1(\mathcal {S})$ (Fig. 11b), the simulator $\mathcal {S}$ is a parameter and the $\texttt{Key}$$^1_{O^*,0..d}$ and $\texttt{Log}$$_{O^*}$ packages (cf. Sect. 2.3) constitute the ideal functionality. Namely, the $\texttt{Key}$$^1_{O^*,0..d}$ package samples a uniformly random key for handles which correspond to honest keys with a name $n\in O^*$ and some level $0\le \ell \le d$. The $\texttt{Log}$$_{O^*}$ package, in turn, ensures that each handle corresponds to a different key, modeling key uniqueness for both honest and dishonest keys.

Similarly, we describe the real execution of the key schedule as a game $\texttt{Gks}^0$, written in pseudocode. Following the SSP methodology outlined in Sect. 2.3, we split the pseudocode of the game $\texttt{Gks}^0$ into several packages most of which ($\texttt{Xpd}$, $\texttt{Xtr}$, DH, $\texttt{Key}$, and $\texttt{Log}$) have been introduced before and $\texttt{Check}$ is described in Sect. 4.3. Figure 11a depicts the composed game $\texttt{Gks}^0$—recall that this graph is not merely an illustration, it is part of the formal definition of $\texttt{Gks}^0$.

The game $\texttt{Gks}^0$ exposes $\textsf{SET}_{ psk ,0}$ and $\textsf{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 $\textsf{XTR}$ and $\textsf{XPD}$ oracles trigger key derivations. Finally, the adversary can access output keys via the $\textsf{GET}$ oracle on the (real) key package $\texttt{Key}$$^0_{O^*,0..d}$.

Definition 12 (Key Schedule Advantage)

For a key schedule $ks = (N, \textsf{label},\textsf{prntn})$, a natural number d, a simulator $\mathcal {S}$ and an adversary $\mathcal {A}$ which makes queries for at most d levels we define the advantage $\textsf{Adv}(\mathcal {A},\texttt{Gks}^0,\texttt{Gks}^1(\mathcal {S})):=$

$$\begin{aligned} \big |&{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^0\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^1(\mathcal {S})\right] \big |, \end{aligned}$$

where Fig. 11b defines $\texttt{Gks}^1(\mathcal {S})$ and Fig. 11a defines $\texttt{Gks}^0$.

4.3 Front-End Checks

Fig. 12.

Code of $\texttt{Check}$

The $\texttt{Check}$ package acts as a restriction on the adversary since the $\textbf{assert}$ conditions in the $\texttt{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 $\textbf{assert}$ conditions in $\texttt{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.

In addition to enforcing the use of consistent shares in the transcript, the $\textsf{XPD}$ oracle of the $\texttt{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 $\textsf{xpd}$ derivations, but only once on the path from $psk$ to output key, and $\texttt{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, \textsf{label}, \textsf{prntn})$, we call $S\subseteq N$ a set of separation points, if it satisfies the following two requirements:

• $\forall \;n \in O$: the path from $psk$ to n contains an $n'\in S$.

• If there exists a path from $dh$ to an $n \in O$, then it contains an $n'\in S$.

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

5 Key Schedule Theorem

Theorem 1

Let $ks$ be a TLS-like key schedule with representative set $XPR$ and separation points S. Let $d\in \mathbb {N}$. There is an efficient simulator $\mathcal {S}$ such that for all adversaries $\mathcal {A}$ which make queries for at most d resumption levels,

$$\begin{aligned} \textsf{Adv}(\mathcal {A},\texttt{Gks}^0,\texttt{Gks}^1(\mathcal {S})) \le \;&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^\text {main}_\text {cr},\texttt{Gacr}^{\textsf{hash},b})\\ + \sum _{j\in \{Z,D\},\textsf{f}\in \{\textsf{xtr},\textsf{xpd}\}}&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^\text {main}_{j,\textsf{f}},\texttt{Gacr}^{\mathsf f,b}) \\ +\max _{i\in \{0,1\}}\big [&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {sodh}},\texttt{Gsodh}^b)\\ \sum _{\ell =0}^{d-1}\big (&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {es,}\ell },\texttt{Gxtr}_{ es ,\ell }^b)\\ +&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {hs,}\ell },\texttt{Gxtr}_{ hs ,\ell }^b)\\ +&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {as}, \ell },\texttt{Gxtr}_{ as ,\ell }^b)\\ +\sum _{ n \in { XPR }}\big (&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {n},\ell },\texttt{Gxpd}_{ n ,\ell }^b)\big )\big )\\ +&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{ esalt,pi },\texttt{Gpi}^{b}_{ esalt })\\ +&\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{ O^*,pi },\texttt{Gpi}^{b}_{ O^* })\big ], \end{aligned}$$

where $\mathcal {A}_i$ behaves as $\mathcal {A}$ except that it returns bit i on a so-called win abort (cf. [23, Lemma D.4]); $\mathcal {R}_{*}^{\text {main}}:=\mathcal {R}^{\text {ch-map}}\rightarrow \mathcal {R}_{*}$ when replacing $*$ by $\text {cr}$, $\text{( }{Z},\textsf{f})$, $(\text {D},\textsf{f})$, $\text {sodh}$, $\text {es}$, $\text {hs}$, $\text {as}$, $\text {n}$, $O^*,pi$ or $esalt,pi$, the simulator $\mathcal {S}$ is marked in grey in [23, Fig. 26b], [23, Fig. 32a] defines $\mathcal {R}_{\text {sodh}}$, [23, Fig. 34a] defines $\mathcal {R}_{\text {es,}\ell }$, $\mathcal {R}_{\text {hs,}\ell }$ and $\mathcal {R}_{\text {as,}\ell }$ are defined analogously, and [23, Fig. 34b] defines $\mathcal {R}_{\text {n,}\ell }$ for $n \in XPR$, $0\le \ell \le d$, [23, Fig. 32c] defines $\mathcal {R}_{ esalt,pi }$ and [23, Fig. 32d] defines $\mathcal {R}_{ O^*,pi }$.

Fig. 13.

Proof structure

5.1 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 $\mathcal {A}$ which successfully distinguishes between two games $\texttt{G}_{\text {big}}^0$ and $\texttt{G}_{\text {big}}^1$, then based on $\mathcal {A}$, we can construct an adversary $\mathcal {B}$ of similar complexity as $\mathcal {A}$ which successfully distinguishes between two games $\texttt{G}_{\text {sml}}^0$ and $\texttt{G}_{\text {sml}}^1$. Our reductions will have the following form.

Lemma 1 (Reduction Technique)

If we can define a reduction $\mathcal {R}$ such that

then

$$\begin{aligned} \textsf{Adv}(\mathcal {A};\texttt{G}_{\text {big}}^0,\texttt{G}_{\text {big}}^1)=\textsf{Adv}(\mathcal {B};\texttt{G}_{\text {sml}}^0,\texttt{G}_{\text {sml}}^1), \end{aligned}$$

(3)

where

$$\begin{aligned} \mathcal {B}:=\mathcal {A}\rightarrow \mathcal {R}. \end{aligned}$$

(4)

Proof

Assuming Eq. 1,  2 and 4, we deduce Eq. 3 as follows:

$$ \begin{aligned} \textsf{Adv}(\mathcal {A},&\texttt{G}_{ big }^0,\texttt{G}_{ big }^1)\\ {\mathop {=}\limits ^{\text {def.}}}\,&\left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{G}_{ big }^0\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \mathcal {R}\rightarrow \texttt{G}_{ big }^1\right] \right|\\ {\mathop {=}\limits ^{\text {Eq.}1 \& 2}}&\left|{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow (\mathcal {R}\rightarrow \texttt{G}_{ sml }^0)\right] -{\text {Pr}}\left[ 1=\mathcal {A}\rightarrow (\mathcal {R}\rightarrow \texttt{G}_{ sml }^1)\right] \right|\\ =\;\,&\left|{\text {Pr}}\left[ 1=(\mathcal {A}\rightarrow \mathcal {R})\rightarrow \texttt{G}_{ sml }^0)\right] -{\text {Pr}}\left[ 1=(\mathcal {A}\rightarrow \mathcal {R})\rightarrow \texttt{G}_{ sml }^1\right] \right|\\ {\mathop {=}\limits ^{\text {def.}}}\,&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R},\texttt{G}_{ sml }^0,\texttt{G}_{ sml }^1){\mathop {=}\limits ^{\text {Eq.}~4}}\textsf{Adv}(\mathcal {B},\texttt{G}_{ sml }^0,\texttt{G}_{ sml }^1) \end{aligned}$$

Fig. 14.

Oracles of $\texttt{Map}$. Here, $\ell \in \left\{ 0\dots d\right\}$. $\ell ' {\mathop {\leftarrow }\limits ^{\text {choose}}}\textsf{level}( M _{n_1}[h_1]), \textsf{level}( M _{n_2}[h_2])$ assigns to $\ell '$ the value $\textsf{level}( M _{n_1}[h_1])$ if it is not $\bot$ and $\textsf{level}( M _{n_2}[h_2])$, else.

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 result, we can argue Eqs. 1 and 2 graphically. E.g., in [23, Fig. 31a] we highlight the reduction in gray and observe that the only change from Fig. 15a is the collision resistance assumption—the $\texttt{G}_{\text {sml}}^b$ in this case. Observing the graph of $\texttt{Gks}^0$ (cf. Fig. 11a) closely and comparing it with the graphs of the assumptions introduced in Sect. 3, one can identify that the assumptions are almost sub-graphs of $\texttt{Gks}^0$, and by an appropriately chosen sequence of reduction arguments, the graphs of the assumptions will appear as actual subgraphs.

5.2 Proof of Theorem 1

We need to show the indistinguishability of the real game $\texttt{Gks}^0$ and the ideal game $\texttt{Gks}^1(\mathcal {S})$. [23, Fig. 25a] depicts the real game $\texttt{Gks}^0$ (cf. Fig. 11a), with slightly different graph layouting. [23, Fig. 26b] depicts the ideal game $\texttt{Gks}^1(\mathcal {S})$ (cf. Fig. 11b) where the simulator $\mathcal {S}$ is described in concrete code. To show the indistinguishability between $\texttt{Gks}^0$ ([23, Fig. 25a]) and $\texttt{Gks}^1(\mathcal {S})$ ([23, Fig. 26b]), we make 4 game hops, depicted as the sequence of the five games depicted in [23, Fig. 25a], [23, Fig. 25b], [23, Fig. 25c], [23, Fig. 26a] and [23, Fig. 26b]. We now describe each of the game hops and state the corresponding lemma, see Fig. 13 for a proof overview.

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 $(\textsf{level}(h)>0$) and an adversarially registered application psk $(\textsf{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 $\texttt{Map}$ package (see [23, Fig. 25b] for the game and the left column of Fig. 14 for the code of $\texttt{Map}$) to remove the redundantly stored keys—note that the $\texttt{Log}_{ psk }^{ A1 }$ and the $\texttt{Log}_{ dh }^{ Z \infty }$ package now use the $map =1$ and the $map =\infty$ code of $\texttt{Log}$ (see Fig. 4 for its code). As a result, any adversary playing against $\texttt{Gcore}^0$ (defined in [23, Fig. 25b]) cannot create (this particular) redundancy anymore since the $\texttt{Key}_{ psk ,\ell }$ and $\texttt{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 [23]. It relies on proving the invariant that whenever $\texttt{Gks}^{0}$ stores key k with honesty ${hon}$ under handle h, then game $\texttt{Gks}^{0\text {Map}}$ 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 $\mathcal {A}$ which make queries for at most d resumption levels,

$$\begin{aligned} {\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^{0}\right] ={\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^{0\text {Map}}\right] . \end{aligned}$$

In particular $\texttt{Gks}^{0}{\mathop {\equiv }\limits ^{\text {func}}}\texttt{Gks}^{0\text {Map}}$.

Lemma 3 then reduces the indistinguishability of $\texttt{Gks}^{0\texttt{Map}}$ ([23, Fig. 25b]) and $\texttt{Gks}^{1\texttt{Map}}$ ([23, Fig. 25c]) to the indistinguishability of $\texttt{Gcore}^0$ and $\texttt{Gcore}^1(\mathcal {S}^{\text {core}})$ using reduction $\texttt{R}^{\text {core}}$. The indistinguishability of $\texttt{Gcore}^0$ and $\texttt{Gcore}^1(\mathcal {S}^{\text {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 $\mathcal {A}$ which make queries for at most d resumption levels,

$$\begin{aligned}&\textsf{Adv}(\mathcal {A},\texttt{Gks}^{0\text {Map}},\texttt{Gks}^{1\text {Map}})\\ =&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^{\text {ch-map}},\texttt{Gcore}^{0},\texttt{Gcore}^{1}(\mathcal {S}^{\text {core}})), \end{aligned}$$

where [23, Fig. 25b] defines $\texttt{Gks}^{0\text {Map}}$, [23, Fig. 25c] defines $\texttt{Gks}^{1\text {Map}}$, $\mathcal {R}^{\text {ch-map}}$ and $\mathcal {S}^{\text {core}}$ are marked in grey in [23, Fig. 25c], and Fig. 15a and Fig. 15b define $\texttt{Gcore}^{0}$ and $\texttt{Gcore}^{1}(\mathcal {S}^{\text {core}})$, respectively.

Proof

The proof of Lemma 3 is an instance of Lemma 1 with $\texttt{G}_{\text {big}}^0=\texttt{Gks}^{0\text {Map}}$, $\texttt{G}_{\text {big}}^1=\texttt{Gks}^{1\text {Map}}$, $\texttt{G}_{\text {sml}}^0=\texttt{Gcore}^{0}$, $\texttt{G}_{\text {sml}}^1=\texttt{Gcore}^{1}(\mathcal {S}^{\text {core}})$ and $\mathcal {R}=\mathcal {R}^{\text {ch-map}}$.

By Lemma 1, it suffices to show that

$$\begin{aligned} \texttt{Gks}^{0\text {Map}}&{\mathop {\equiv }\limits ^{\text {code}}} \mathcal {R}^{\text {ch-map}}\rightarrow \texttt{Gcore}^0 \end{aligned}$$

(5)

$$\begin{aligned} \texttt{Gks}^{1\text {Map}}&{\mathop {\equiv }\limits ^{\text {code}}} \mathcal {R}^{\text {ch-map}}\rightarrow \texttt{Gcore}^1(\mathcal {S}^{\text {core}}) \end{aligned}$$

(6)

Equation 5 follows by definition, since [23, Fig. 25b] defines $\texttt{Gks}^{0\text {Map}}$ as the composition of $\mathcal {R}^{\text {ch-map}}$ and $\texttt{Gcore}^0$. Similarly, for Eq. 6, [23, Fig. 25c]

In Lemma 4, we inline the $\texttt{Xpd}_{ n ,0..d}$ code into $\texttt{Map}$ for $n\in O^*$ and call the result $\mathtt{Map-Xpd}$ (see [23, Fig. 25c] and [23, Fig. 26a] for the two games). The proof is a simple inlining argument and included into the full version [23] for completeness.

Lemma 4 (Xpd-Inlining)

For all PPT adversaries $\mathcal {A}$ which make queries for at most d resumption levels,

$$\begin{aligned} {\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^{1\text {Map}}\right] ={\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^{\text {Mapxpd}}\right] . \end{aligned}$$

In particular $\texttt{Gks}^{1\text {Map}}{\mathop {\equiv }\limits ^{\text {code}}}\texttt{Gks}^{\text {Mapxpd}}$.

Finally, Lemma 5 establishes the (perfect) indistinguishability of $\texttt{Gks}^{\mathtt{Map-Xpd}}$ and $\texttt{Gks}^1(\mathcal {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 $\texttt{Gks}^1(\mathcal {S})$.

Lemma 5 (Map-Outro)

For all PPT adversaries $\mathcal {A}$ which make queries for at most d resumption levels,

$${\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^{\text {Mapxpd}}\right] = {\text {Pr}}\left[ 1=\mathcal {A}\rightarrow \texttt{Gks}^1(\mathcal {S})\right] .$$

In particular, $\texttt{Gks}^{\text {Mapxpd}}{\mathop {\equiv }\limits ^{\text {func}}}\texttt{Gks}^1(\mathcal {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 Sect. 5.3).

$$\begin{aligned} \textsf{Adv}(\mathcal {A},\texttt{Gks}^0,\texttt{Gks}^1(\mathcal {S})) {\mathop {=}\limits ^{\text {Lm.}~2}}&\textsf{Adv}(\mathcal {A},\texttt{Gks}^{0\text {Map}},\texttt{Gks}^1(\mathcal {S}))\\ {\mathop {=}\limits ^{\text {Lm.}~5}}&\textsf{Adv}(\mathcal {A},\texttt{Gks}^{0\text {Map}},\texttt{Gks}^{\text {Mapxpd}})\\ {\mathop {=}\limits ^{\text {Lm.}~4}}&\textsf{Adv}(\mathcal {A},\texttt{Gks}^{0\text {Map}},\texttt{Gks}^{1\text {Map}}) \end{aligned}$$

$$\begin{aligned} {\mathop {=}\limits ^{\text {Lm.}~3}}&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^{\text {ch-map}},\texttt{Gks}^{0\text {core}},\texttt{Gks}^{1\text {core}}(\mathcal {S}^{\text {core}}))\\ {\mathop {\le }\limits ^{\text {Th.}~2}}&\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^\text {main}_\text {cr},\texttt{Gacr}^{\textsf{hash},b})\\&+ \sum _{j\in \{Z,D\},\textsf{f}\in \{\textsf{xtr},\textsf{xpd}\}} \textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R}^\text {main}_{j,\textsf{f}},\texttt{Gacr}^{\textsf{hash},b})\\&+\max _{i\in \{0,1\}}\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {sodh}},\texttt{Gsodh}^b)\\&+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{ esalt,pi },\texttt{Gpi}^{b}_{ esalt })\\&+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{ O^*,pi },\texttt{Gpi}^{b}_{ O^* })\\&+\sum _{\ell =0}^{d-1}\big (\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {es,}\ell },\texttt{Gxtr}_{ es ,\ell }^b)\\&\;\;\;\;\;\;\;\;+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {hs,}\ell },\texttt{Gxtr}_{ hs ,\ell }^b)\\&\;\;\;\;\;\;\;\;+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {as}},\texttt{Gxtr}_{ as ,\ell }^b)\\&\;\;\;\;\;\;\;\;+\sum _{ n \in { XPR }}\big (\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}^\text {main}_{\text {n},\ell },\texttt{Gxpd}_{ n ,\ell }^b)\big )\big ), \end{aligned}$$

where $XPR$ is the representative set required by the theorem, $\mathcal {R}_{*}^{\text {main}}:=\mathcal {R}^{\text {ch-map}}\rightarrow \mathcal {R}_{*}$ when replacing $*$ by $\text {cr}$, $(\text {Z},\textsf{f})$, $(\text {D},\textsf{f})$ $\text {sodh}$, $\text {es}$, $\text {hs}$, $\text {as}$, $\text {n}$, $O^*,pi$ or $esalt,pi$.

Fig. 15.

Games for Theorem 2

5.3 Core Key Schedule Theorem

It remains to show that the core key schedule game $\texttt{Gcore}^0$ without the $\texttt{Map}$ and $\texttt{Check}$ package in front (Fig. 15a is indistinguishable from an ideal game $\texttt{Gcore}^1(\mathcal {S}^\text {core})$ which consists of an ideal functionality with a simulator $\mathcal {S}^\text {core}$ (Fig. 15b). The proof of Theorem 2 can be found in the full version [23, Appendix D]

Theorem 2 (Core)

Let $ks$ be a TLS-like key schedule with ${ XPR }$. Let d be an integer. Let $\mathcal {S}^\text {core}$ be the efficient simulator defined in [23, Fig. 26b]. Then, for all adversaries $\mathcal {A}$ which make queries for at most d resumption levels, we have that

$$\begin{aligned}&\textsf{Adv}(\mathcal {A},\texttt{Gcore}^0,\texttt{Gcore}^1(\mathcal {S}^\text {core}))\\ \le&\sum _{\mathcal {R}\in \{\mathcal {R}_{\text {cr}},\mathcal {R}_{Z},\mathcal {R}_{D}\}}\textsf{Adv}(\mathcal {A}\rightarrow \mathcal {R},\texttt{Gacr}^b) \\ {}&+\max _{i\in \{0,1\}}\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{\text {sodh}},\texttt{Gsodh}^b)\\&+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{ esalt,pi },\texttt{Gpi}^{b}_{ esalt }) \\ {}&+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{ O^*,pi },\texttt{Gpi}^{b}_{ O^* })\\&+\sum _{\ell =0}^{d-1}\big (\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{\text {es,}\ell },\texttt{Gxtr}_{ es ,\ell }^b) \\ {}&\;\;\;\;\;\;\;\;+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{\text {hs,}\ell },\texttt{Gxtr}_{ hs ,\ell }^b)\\&\;\;\;\;\;\;\;\;+\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{\text {as}},\texttt{Gxtr}_{ as ,\ell }^b) \\ {}&\;\;\;\;\;\;\;\;+\sum _{ n \in { XPR }}\big (\textsf{Adv}(\mathcal {A}_i\rightarrow \mathcal {R}_{\text {n},\ell },\texttt{Gxpd}_{ n ,\ell }^b)\big )\big ), \end{aligned}$$

where $XPR$ is the required representation set (cf. Table 1), Fig. 15a defines $\texttt{Gcore}^0$ and Fig. 15b defines $\texttt{Gcore}^1(\mathcal {S}^\text {core})$, [23, Fig. 31a] defines $\mathcal {R}_{\text {cr}}$, [23, Fig. 32a] defines $\mathcal {R}_{\text {sodh}}$, [23, Fig. 34a] defines $\mathcal {R}_{\text {es,}\ell }$, $\mathcal {R}_{\text {hs,}\ell }$ and $\mathcal {R}_{\text {as,}\ell }$ are defined analogously, and $\mathcal {R}_{\text {n,}\ell }$ for $n \in XPR$ and $0\le \ell \le d$ is defined in [23, Fig. 34b], $\mathcal {R}_{ esalt,pi }$ is defined in [23, Fig. 32c] and $\mathcal {R}_{ O^*,pi }$ is defined in [23, Fig. 32d].

6 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. [34,35,36] 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. [48] 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. [29, 30] 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. [10] 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 [18] and CryptoVerif [16]. 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 [17] introduces a new proof modularization framework in CryptoVerif, which bears significant similarities with the state-separating proof framework [24] 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. [41] analyse the draft-06 TLS 1.3 handshake, and show that its modes achieve key confirmation in isolation. Fischlin et. al. [39] 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 [27, 37, 46].

The idea of analyzing a key schedule (rather than a key exchange protocol) is conceptually similar to the SIGMA-I pattern of Krawczyk [44] and Krawczyk and Wee [47]. These works prove a reduction from key exchange security to key schedule security analogously to our companion paper [25].

Recent work also looked at the tightness of TLS 1.3 security proofs [31, 33]. 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 [22] uses our methodology, e.g., our recursive handle structure and the style of encoding security guarantees in $\texttt{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., [28]. In the present paper, in addition to key techniques which were picked up by [22], 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 $\texttt{Check}$ component introduced in Sect. 4.3. In a similar way, the additional mapping step (Lemma 2, 4 and 5) handle redundancy not present in MLS. See Sect. 7 for simplifications of the TLS protocol which would allow for a much simpler analysis than the one presented in this article.

7 Lessons Learned and 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 [14]). 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 [37]. 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 [13] 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 [8] security model [43]. 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.