Bruno Blanchet
email: bruno.blanchet@inria.fr

Composition Theorems for CryptoVerif and Application to TLS 1.3

We present composition theorems for security protocols, to compose a key exchange protocol and a symmetrickey protocol that uses the exchanged key. Our results rely on the computational model of cryptography and are stated in the framework of the tool CryptoVerif. They support key exchange protocols that guarantee injective or non-injective authentication. They also allow random oracles shared between the composed protocols. To our knowledge, they are the first composition theorems for key exchange stated for a computational protocol verification tool, and also the first to allow such flexibility.

As a case study, we apply our composition theorems to a proof of TLS 1.3 Draft-18. This work fills a gap in a previous paper that informally claims a compositional proof of TLS 1.3, without formally justifying it.

Introduction

The proof of security protocols is notoriously difficult. In particular, when security protocols grow in size, the complexity of their proof increases, and quickly becomes unmanageable. Composition theorems are essential to tackle this problem: they allow one to prove small pieces of the considered protocol, and to compose these results in order to obtain a proof of the full protocol.

In this paper, we consider the standard game-based computational model of cryptography, and we focus on the composition between a key exchange protocol and a symmetric key protocol that uses the key provided by the key exchange. We assume that the key exchange protocol runs between two participants A and B and is secure: the provided key is secret in the sense that keys provided in several sessions are indistinguishable from independent random keys; the protocol provides authentication of A to B, defined based on session identifiers; and A executes at most one session with a given session identifier. Then, we prove that the security properties of the symmetric key protocol carry over to the composed protocol. Moreover, we also prove that the security properties of the key exchange protocol are preserved in the composed protocol (except for the secrecy of the key on which we perform the composition). This point is important to be able to perform several compositions one after the other. We have two variants of our composition theorem: one in which authentication is injective, that is, each execution of B corresponds to a distinct execution of A; and one in which authentication is non-injective, that is, several executions of B may correspond to the same execution of A.

An originality of our composition theorems is that they are stated within the framework of a protocol verification tool, CryptoVerif [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF], [START_REF]A computationally sound mechanized prover for security protocols[END_REF], [START_REF]CryptoVerif: A computationally-sound security protocol verifier[END_REF], available at http: //cryptoverif.inria.fr. We use the language of CryptoVerif to represent the cryptographic games; we use security properties proved by CryptoVerif as assumptions of our composition theorems. Therefore, we can easily use CryptoVerif to mechanize the proof of the protocol pieces that we compose.

Using such a framework to state composition theorems has several advantages. It strengthens the abilities of Cryp-toVerif: thanks to the composition theorems, we can obtain security proofs for bigger protocols. Moreover, CryptoVerif does not support loops. If we can break a protocol with loops into pieces without loops, we can verify them using Cryp-toVerif, and prove security of the whole protocol with loops by iteratively composing these pieces. Finally, CryptoVerif provides a rigorous framework for stating the composition theorems: it provides a formal language for games and for security properties, with a formal semantics. The hypotheses and conclusions of the composition theorems can then be stated precisely and concisely in that framework.

As a case study, we apply our composition theorems to TLS 1.3. More precisely, we revisit a previous analysis of TLS 1.3 Draft 18 by Bhargavan et al. [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF], [START_REF]Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF]. This analysis splits TLS 1.3 into 3 pieces: the initial handshake, the handshake with pre-shared key, and the record protocol, and claims that security of TLS 1.3 can be obtained by composing these 3 pieces. However, it does not justify this composition formally. Our work fills this gap. TLS 1.3 is particularly well-suited as a case study to illustrate the power of our composition results. First, it is an important protocol, which is currently being standardized. The current draft, Draft 28 [START_REF] Rescorla | The Transport Layer Security (TLS) protocol version 1.3, draft-ietf-tls-tls13-28[END_REF], is now final, and not very different from Draft 18. We expect that our composition results would apply in the same way to Draft 28, though the CryptoVerif models of the protocol pieces would require minor changes. Second, TLS 1.3 is well-designed to allow composition: the handshake produces traffic secrets used by the record protocol as well as a resumption secret used as a pre-shared key by the next handshake. The protocol pieces are cleanly separated, so that the only common secret between them is the symmetric key on which we perform the composition. Third, TLS 1.3 includes loops: it allows an unbounded number of handshakes with pre-shared key and an unbounded number of key updates in the record protocol. Therefore, it cannot be analyzed as a whole by CryptoVerif. The composition results allow us to break these loops and obtain security results for the full protocol. Finally, TLS 1.3 includes a variety of compositions, and we provide theorems for all of them. While most compositions use a key exchange that provides injective authentication, TLS also includes 0-RTT (Round Trip Time) data, that is, data that the client sends to the server immediately after the first message of TLS (ClientHello). Such data can be replayed, and the corresponding key exchange only provides non-injective authentication. Furthermore, we also have to deal with altered ClientHello messages; in this case, only the server has the corresponding key, and that requires a variant of the composition result. Finally, for key updates in the record protocol, the key is simply computed from the previous key without a proper key exchange, so we can use a much simpler composition theorem in this case.

Related Work

The line of work closest to ours is that of [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF]. Brzuska et al. [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF] prove a composition result similar to ours, in an informal game-based framework. Fischlin et al. [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] extend this framework to multi-stage key exchange protocols, in which parties can establish multiple keys in different stages and use these keys between stages. They apply their results to the proof of QUIC [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] and of TLS 1.3 Draft 05, Draft DH [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], and Draft 10 [29]. In addition to recasting the composition result in CryptoVerif, we extend it in several ways. We prove that security properties of the key exchange protocol are preserved in the composition, so we can compose again using other keys. This point appears in [30, Remark, page 16 of the full version] without proof. We allow the composed protocols to share random oracles; this point does not appear in [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF]. We prove a composition theorem for protocols that provide non-injective authentication, used for 0-RTT data in TLS 1.3. Although we do not consider several stages explicitly, our composition theorems support most compositions allowed by the multi-stage framework. (We detail the comparison in Section 5.4.) Brzuska et al. [START_REF] Brzuska | Less is more: relaxed yet composable security notions for key exchange[END_REF] prove a composition theorem that allows the key exchange protocol to already use the key provided to the symmetric-key protocol, for example for key confirmation. TLS 1.3 is designed so that the same key is never both used in the key exchange and provided to the next protocol, so we did not need such a composition result in our case study. We believe that such a result could also be proved in our framework if desired.

Canetti and Krawczyk [START_REF] Canetti | Analysis of key-exchange protocols and their use for building secure channels[END_REF] prove security of the composition of a key exchange protocol with specific symmetrickey protocols that use MACs to achieve an authenticated channel or encrypt-then-MAC to achieve a secure channel. Barthe et al. [4] develop generic proofs of reduction for one-round key-exchange protocols, such as Naxos and HMQV, in EasyCrypt. EasyCrypt is an interactive theorem prover specialized for building game-based security proofs. Thus, their approach provides another way of introducing modularity in machine-checked proofs of security.

Universal composability (UC) [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF], [START_REF] Canetti | Universally composable symbolic analysis of mutual authentication and key exchange protocols[END_REF], [START_REF] Canetti | Universal composition with joint state[END_REF], [START_REF] Küsters | Composition theorems without preestablished session identifiers[END_REF] is a framework that allows to compose protocols. However, proving UC-security requires stronger properties than the game-based framework that we use ( [17, Appendix A] details limitations of the UC framework). Delaune et al. [START_REF] Delaune | Simulation based security in the applied pi calculus[END_REF] present a simulation-based framework that is an analogue of UC in the symbolic (Dolev-Yao) model of cryptography.

Composition theorems have also been proved in the Dolev-Yao model. Many of these theorems deal with the parallel composition of protocols that share secrets, for trace properties [START_REF] Cortier | Safely composing security protocols[END_REF], [START_REF] Guttman | Protocol independence through disjoint encryption[END_REF], for resistance against guessing attacks for protocols that share passwords [START_REF] Delaune | Composition of passwordbased protocols[END_REF], and for privacy properties [START_REF] Arapinis | Verifying privacy-type properties in a modular way[END_REF], using disjointness assumptions such as tagging or disjoint primitives to guarantee the independence of the protocols. Other results [START_REF]Composing security protocols: from confidentiality to privacy[END_REF], [START_REF] Ciobâcȃ | Protocol composition for arbitrary primitives[END_REF] allow sequential composition, in particular the composition of a key exchange protocol with a symmetric-key protocol that uses the exchanged key. Ciobâcȃ et al. [START_REF] Ciobâcȃ | Protocol composition for arbitrary primitives[END_REF] consider trace properties, while Arapinis et al. [START_REF]Composing security protocols: from confidentiality to privacy[END_REF] extend the result to processes with else branches, to private channels, and to privacy properties. Mödersheim et al. [START_REF] Groß | Vertical protocol composition[END_REF], [START_REF] Mödersheim | Secure pseudonymous channels[END_REF], [START_REF]Sufficient conditions for vertical composition of security protocols[END_REF] define notions of security for channels (insecure, authentic, confidential, secure), and prove composition results between protocols that establish such channels and protocols that use them. They also rely on the Dolev-Yao model and use disjointness assumptions. We believe that the computational model has two advantages: it is more realistic than the Dolev-Yao model and the computational definitions compose nicely, so that we can avoid disjointness assumptions.

Protocol composition logic [START_REF] Datta | Protocol composition logic (PCL)[END_REF], [START_REF] Datta | Computationally sound compositional logic for key exchange protocols[END_REF] is a logic for proving security protocols that allows sequential and parallel composition. It was initially designed in the Dolev-Yao model [START_REF] Datta | Protocol composition logic (PCL)[END_REF] and adapted to the computational model [START_REF] Datta | Computationally sound compositional logic for key exchange protocols[END_REF].

Outline

The next section provides a minimal reminder of the CryptoVerif framework. Section 3 presents the structure of our proof of TLS, so that we can use it as a motivation for the composition theorems. Section 4 presents a very simple composition theorem, used for key updates in TLS 1.3, as a warm-up. Section 5 presents our main composition theorems. CryptoVerif has a notion of tables. For simplicity, all the previous results are presented in a language without tables. Section 6 explains how to extend them to tables. Section 7 summarizes their application to TLS, and Section 8 concludes. The proofs of all results and details on the TLS case study can be found in [START_REF]Composition theorems for CryptoVerif and application to TLS 1.3[END_REF].

A Short Reminder on CryptoVerif

This section provides a short reminder of the CryptoVerif framework.

Processes, Contexts, Adversaries

CryptoVerif mechanizes proofs by sequences of games, similar to those written on paper by cryptographers [START_REF] Bellare | The security of triple encryption and a framework for code-based game-playing proofs[END_REF], [START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF]. It represents protocols and cryptographic games in a probabilistic process calculus. We refer the reader to [START_REF]A computationally sound mechanized prover for security protocols[END_REF], [START_REF]CryptoVerif: A computationally-sound security protocol verifier[END_REF] for details on this process calculus. We explain the necessary constructs as they appear.

We use P , Q for processes. A context C is a process with one or several holes [ ]. We write C[P 1 , . . . , P n ] for the process obtained by replacing the holes of C with P 1 , . . . , P n respectively. An evaluation context is a context with one hole, generated by the following grammar:

C ::= evaluation context [ ] hole newChannel c; C channel restriction Q | C parallel composition C | Q parallel composition
The channel restriction newChannel c; Q restricts the channel name c, so that communications on this channel can occur only inside Q, and cannot be received outside Q or sent from outside Q. The parallel composition Q 1 | Q 2 makes simultaneously available the processes defined in Q 1 and Q 2 . We use evaluation contexts to represent adversaries.

Indistinguishability

A process can execute events, by two constructs: event e(M 1 , . . . , M n ) executes event e with arguments M 1 , . . . , M n , and event abort e executes event e without argument and aborts the game. After finishing execution of a process, the system produces two results: the sequence of executed events E, and the information whether the game aborted (a = abort, that is, executed event abort) or terminated normally (a = 0). These events and result can be used to distinguish games, so we introduce an additional algorithm, a distinguisher D that takes as input the sequence of events E and the result a, and returns true or false. We write Pr[Q : D] for the probability that the process Q executes events E and returns a result a such that D(E, a) = true. Definition 1 (Indistinguishability). We write Q ≈ V p Q when, for all evaluation contexts C acceptable for Q and Q with public variables V and all distinguishers D that run in time at most

t D , | Pr[C[Q] : D] -Pr[C[Q ] : D]| ≤ p(C, t D ).
Intuitively, Q ≈ V p Q means that an adversary has probability at most p of distinguishing Q from Q , when it can read the variables in the set V . When V is empty, we omit it. The probability p may depend on many parameters coming from the context C, that is why p takes as arguments the whole context C and the runtime of D. CryptoVerif always expresses the probabilities as formulas in which the only parameters that come from the context C are the maximum runtime of C, the maximum number of times C may send a message to each subprocess in Q (resp. Q ), and the lengths of bitstrings. This property allows us to simplify probability formulas by abstracting away the precise context they use and retaining only the useful parameters. We denote by t C the maximum runtime of C, and use the same notation for processes P , Q, terms M , and functions f . As usual in cryptographic proofs, we ignore very small runtimes.

The condition that C is acceptable for Q and Q with public variables V is a technical condition that ensures that C[Q] and C[Q ] are well-formed. The public variables V are the variables of Q and Q that C is allowed to read.

Indistinguishability is reflexive (

Q ≈ V 0 Q), symmetric (if Q ≈ V p Q , then Q ≈ V p Q) and transitive (if Q ≈ V p Q and Q ≈ V p Q , then Q ≈ V p+p Q ). Moreover, Q ≈ V p Q implies C[Q] ≈ V p C[Q ]
for all evaluation contexts C acceptable for Q and Q with public variables V and all V ⊆ V ∪ var(C), where var(C) is the set of variables of C and p (C

, t D ) = p(C [C[ ]], t D ).

Secrecy

Intuitively, in CryptoVerif, secrecy means that the adversary cannot distinguish between the secrets and independent random values. This definition corresponds to the "real-orrandom" definition of security [START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF]. As shown in [START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF], this notion is stronger than the one in which the adversary performs a single test query and some reveal queries. We recall the definition of secrecy in CryptoVerif given in [START_REF]Automatically verified mechanized proof of one-encryption key exchange[END_REF], [START_REF]CryptoVerif: A computationally-sound security protocol verifier[END_REF]. Let us first explain CryptoVerif constructs used in this definition. The replication ! i≤n Q represents n copies of the process Q in parallel, indexed by i ∈ [1, n], where n is named a replication bound. The current replication indices at a certain program point are the indices i of replications above that program point. In CryptoVerif, all variables defined under a replication are implicitly arrays indexed by the current replication indices: if Q defines a variable x under ! i≤n , the value of x is in fact stored in x[i]. The definition of x is executed at most once for each i, so that all values of x are stored in distinct array cells. When a variable is accessed with current replication indices, we omit the indices, writing x for x[i]. The find construct reads these array cells:

find u = i ≤ n suchthat defined(x 1 [i ], . . . , x m [i ]) ∧ M then P else P looks for an index i ∈ [1, n] such that x 1 [i ], . . . , x m [i ]
are defined and M is true. When such an index is found, it is stored in u, and process P is executed. Otherwise, process P is executed. The term M may refer to x 1 [i ], . . . , x m [i ] and the process P may refer to x 1 [u], . . . , x m [u] since these variables are guaranteed to be defined. The input c[i](x : T ); P receives a message on channel c[i]. If this message is in the set of bitstrings T (T stands for "type"), it is stored in x, and P is executed. Otherwise, the process blocks. The channel c[i] consists of a channel name c and indices, here i. Very often, these indices are the current replication indices at the input: the sender can then tell precisely to which copy of the process the message should be sent. Similarly, the output c[i] M ; Q sends message M on channel c[i]. After the output, the control is passed to the receiver process, which continues execution.

The process Q that follows the output consists of inputs, possibly under replications and parallel compositions; these inputs will be executed when a message is sent to them. Finally, the restriction new y : T ; P chooses uniformly a random element of T , stores it in y, and executes P .

We use u as an abbreviation for a sequence of variables: u = u 1 , . . . , u m . We write u ≤ n for u 1 : [1, n 1 ], . . . , u m : [1, n m ] when u = u 1 , . . . , u m and n = n 1 , . . . , n m . We say that a variable is defined under replications ! i≤ n when i = i 1 , . . . , i m , n = n 1 , . . . , n m , and it is defined under replications ! i1≤n1 . . . ! im≤nm . (There may be other instructions between these replications.) We define that a context has replications ! i≤ n above the hole in a similar way. When

n = n 1 , . . . , n m , we define n = n 1 × • • • × n m .
Definition 2 (Secrecy). Let x and V be such that x / ∈ V . Suppose that the variable x has type T and is defined under replications

! i≤ n in Q. Let R x = c s0 (); new b : bool ; c s0 ; (! is≤ns c s [i s ]( u ≤ n); if defined(x[ u]) then if b then c s [i s ] x[ u] else find u s = i s ≤ n s suchthat defined(y[i s ], u[i s ]) ∧ u[i s ] = u then c s [i s ] y[u s ] else new y : T ; c s [i s ] y | c s (b : bool ); if b = b then event abort S else event abort S)
where the channels c s0 , c s , c s , the variables u, u s , y, b, b , and the events S, S do not occur in Q. The process Q preserves the secrecy of x with public variables V up to probability p when, for all evaluation contexts C acceptable for

Q | R x with public variables V that do not contain S nor S, Pr[C[Q | R x ] : S] - Pr[C[Q | R x ] : S] ≤ p(C).
The process R x chooses a random bit b, and then allows the adversary to query the variable x: if the adversary sends indices u on channel c s [i s ], and x[ u] is defined, then the process R x replies with the value of x[ u] when b is true, and with a random value when b is false. The find in R x makes sure that, if the indices u have already been queried, then the previous reply is sent; otherwise, a fresh random value y is chosen in the type T of x by new y : T , and sent as a reply. The replication ! is≤ns in R x allows the adversary to perform at most n s such queries; n s is chosen large enough so that it is not a limitation. Finally, the adversary sends on channel c s its guess b for the bit b. If the guess is correct (b = b), then the process R x executes event S; otherwise, it executes event S. Intuitively, Q preserves the secrecy of x when the adversary cannot guess b, that is, it cannot distinguish whether the process outputs the value of the secret (b = true) or outputs independent random numbers (b = false).

Correspondences

Correspondences [START_REF] Woo | A semantic model for authentication protocols[END_REF] are properties of executed sequences of events, such as "if some event has been executed, then some other event has been executed". They are typically used for formalizing authentication. Given a correspondence corr , we define a distinguisher D such that D(E, a) = true if and only if the sequence of events E satisfies the correspondence corr . We write this distinguisher simply corr , and write ¬corr for its negation. Definition 3 (Correspondence). The process Q satisfies the correspondence corr with public variables V up to probability p if and only if, for all evaluation contexts C acceptable for Q with public variables V that do not contain events used in corr ,

Pr[C[Q] : ¬corr ] ≤ p(C).
We refer the reader to [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF] for more details on the verification of correspondences in CryptoVerif. We have: Lemma 1. If Q preserves the secrecy of x with public variables V up to probability p and C is an acceptable evaluation context for Q with public variables V , then for all

V ⊆ V ∪ var(C), C[Q] preserves the secrecy of x with public variables V up to probability p such that p (C ) = p(C [C]).
If Q satisfies a correspondence corr with public variables V up to probability p and C is an acceptable evaluation context for Q with public variables V that does not contain events used in corr , then for all

V ⊆ V ∪var(C), C[Q] satisfies corr with public variables V up to probability p such that p (C ) = p(C [C]). If Q ≈ V ∪{x} p
Q and Q preserves the secrecy of x with public variables V up to probability p , then Q preserves the secrecy of x with public variables V up to probability

p such that p (C) = p (C) + 2 × p(C[[ ] | R x ], t S ). If Q ≈ V p Q
and Q satisfies a correspondence corr with public variables V up to probability p , then Q satisfies corr with public variables V up to probability p such that p (C) = p (C) + p(C, t corr ).

Structure of the proof of TLS 1.3

Our proof of TLS 1.3 relies on a previous analysis of the pieces that we compose [START_REF] Bhargavan | Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF], [START_REF]Verified models and reference implementations for the TLS 1.3 standard candidate[END_REF]. Figure 1 summarizes the structure of the composition. We provide a brief sketch of those previous results here.

The initial handshake, without pre-shared key, provides 4 keys at the end of the protocol: the client traffic secret cats, used by the record protocol for messages from the client to the server; the server traffic secret sats, used by the record protocol for messages from the server to the client; the exporter master secret ems, used to compute exporters (secrets generated by TLS that can be used by applications or other protocols); and the resumption secret resumption secret, used as pre-shared key in the next handshake. For all these keys, CryptoVerif proves in particular secrecy, forward secrecy (with respect to the compromise of long-term client and server keys), and authentication. In this model, the adversary has access to oracles that allow him to compromise the long-term client and server keys. The security properties are proved provided the longterm key of the peer is not compromised yet at the end of the handshake. As explained in the definition of secrecy (Section 2), this model does not include reveal queries for session keys; instead, CryptoVerif proves that all keys of the various sessions are indistinguishable from independent random keys, which is a stronger model [START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF].

The handshake with pre-shared key uses a pre-shared key and provides the same keys as above, with the same security properties. Additionally, it provides a client early traffic secret cets, computed after the first message of the protocol (ClientHello). The record protocol uses this traffic secret to send messages from the client to the server immediately after the ClientHello message, so-called 0-RTT data. The ClientHello message may be replayed and the server may also accept an altered ClientHello message, so CryptoVerif proves weaker properties about cets. When the ClientHello message is not altered, it proves in particular secrecy and non-injective authentication, since replays are possible. When the ClientHello message is altered, it essentially proves that the server has a value of cets that no one else has. In this case, the goal is to show that the record protocol that uses this value of cets never accepts messages.

Due to limitations of CryptoVerif, we cannot prove forward secrecy with respect to the compromise of the pre-shared key in the case of a handshake with pre-shared key and Diffie-Hellman key exchange. Hence, all properties that we prove for the handshake with pre-shared key rely on the secrecy of the pre-shared key. In the analysis of this part of the protocol, we can then consider that the long-term signature keys of the client and the server are compromised, and let the adversary deal with certificates and signatures if they appear. Therefore, the only common secret between our models of the initial handshake and of the handshake with pre-shared key is the pre-shared key. Furthermore, the analysis of the initial handshake allows the compromise of these long-term signature keys at the end of the handshake, so the security properties that we prove for the initial handshake remain valid.

Finally, the record protocol uses a traffic secret to derive an updated traffic secret, used for key updates, and a key and an initialization vector, used for encrypting and decrypting messages with an authenticated encryption scheme. Cryp-toVerif proves secrecy of the updated traffic secret, injective message authentication, and message secrecy. (The adversary cannot distinguish which one of two sets of messages is encrypted, similarly to the property we mentioned for S b 1 in Example 1.) We also consider two variants of the record protocol for 0-RTT. In the first variant, the receiver is replicated, so we have non-injective message authentication instead of the injective one. This variant is useful to support replays of unaltered ClientHello messages. In the second variant, the sender is additionally removed, and we show that the receiver never accepts a message. This variant is useful for altered ClientHello messages. The only common secret between the handshakes and the record protocol is the traffic secret.

The goal of our case study is to combine all these results in order to obtain security results for the full TLS 1.3 protocol.

The Most Basic Composition Theorem

As a warm-up, we present a very simple composition theorem, stated and further explained below. In this theorem, illustrated in Figure 2, we compose a system S 1 that establishes a key k with a system S 2 that runs Q 2 using a fresh random key k. The composed system runs S 1 and Q 2 using the key k provided by S 1 . (The letters Q and S both represent CryptoVerif processes, in the same grammar. We use S for the systems that we compose and for the composed system, and Q for other processes.) Intuitively, the composition works because the secrecy of k allows us to replace k with a fresh random key. (An adversary cannot distinguish k from a fresh random key.) In contrast to the theorems of Section 5, in this theorem, S 1 is not a key exchange protocol: a single participant establishes the key k, so the composition is a lot easier. Theorem 1. Let C be any context with one hole, without replications above the hole and without event abort.

Let Q 1 be a process without event abort. Let M be a term of type T . Let

S 1 = C[let k = M in c 1 ; Q 1 ] S 2 = c 2 (); new k : T ; c 3 ; Q 2
where c 1 , c 2 , c 3 do not occur elsewhere in S 1 , S 2 ; k is the only variable common to S 1 and S 2 ; S 1 and S 2 have no common channel and no common event; and k does not occur in C and Q 1 . Let c 1 be a fresh channel. Let

S composed = C[let k = M in c 1 ; (Q 1 | Q 2 )]
Let S • composed be obtained from S composed by removing all events of S 1 .

1 : k (secret) S 2 : new k : T Q 2 S composed : k Q 2 Figure 2. Illustration of Theorem 1
1) If S 1 preserves the secrecy of k with public variables V (k / ∈ V ) up to probability p, then there exists an evaluation context C such that, for any The assumption that S 1 does not contain event abort is useful because, in the definition of secrecy, when S 1 aborts before a message is sent on c s , neither S nor S is executed, so the adversary gets no advantage against the secrecy of k for these traces. However, these traces could still leak information on k that would break the composition. So we prevent S 1 from aborting. This is not a limitation in practice, because event abort is typically introduced during security proofs, using Shoup's lemma [START_REF]Automatically verified mechanized proof of one-encryption key exchange[END_REF], [START_REF] Shoup | Sequences of games: a tool for taming complexity in security proofs[END_REF], but does not occur in the initial protocol model.

V 1 ⊆ V ∪ (var(S 1 ) \ {k}), we have S • composed ≈ V1 p C [S
The assumption that c 1 , c 2 , c 3 do not occur elsewhere in S 1 , S 2 guarantees that messages sent to channel c 2 (resp. received from c 1 , c 3 ) really go to the input (resp. come from the output) shown in the definitions of S 1 and S 2 . The assumption that k does not occur in C and Q guarantees that S 1 defines k but does not use it. The other assumptions on S 1 and S 2 can easily be obtained by renaming if necessary.

The first conclusion of Theorem 1,

S • composed ≈ V1 p C [S 2 ],
allows us to transfer security properties from S 2 to the composed system S composed using Lemma 1. In this property, we need to remove the events of S 1 , because

A (share a key k) B (m0,m1) -----→ event send(m b ) enc(m b ,k,r) -------→ event recv(m b ) Figure 3. A picture of system S b 2
events can leak information on k even when S 1 preserves the secrecy of k according to Definition 2.

Similarly, the second conclusion of Theorem 1,

S composed ≈ V 0 C [S 1 ],
allows us to transfer security properties from S 1 to the composed system S composed , provided these properties are proved with public variable k, because C uses k. These properties may allow us to compose again S composed with another protocol.

In our TLS case study, we use this composition theorem to deal with key updates in the record protocol. The system S 1 runs the record protocol and computes an updated traffic secret from a traffic secret. This updated traffic secret is the key k in the composition theorem. The system S 2 uses this key k to run the record protocol again. The composition theorem allows us to obtain security properties for a record protocol that performs a key update. We compose again recursively to allow any number of key updates. The next example presents a simplified version of this situation, to illustrate the theorem more formally. where all bitstrings in T m have the same length. This system is illustrated in Figure 3. The system S b 2 chooses a key k, and then runs two participants, say A and B, in parallel. When A receives two messages m 0 , m 1 of the same length on channel c 4 , it sends the encryption of m b under k on channel c 5 and records this emission with the event send(m b ). When B receives a ciphertext on channel c 6 , it decrypts that ciphertext, stores the plaintext in m, and executes event recv(m). (The decryption function dec returns ⊥ when it fails, and the function i ⊥ is the natural injection from bitstring to bitstring∪{⊥}, so that the equality i ⊥ (m) = dec(y, k) holds when the decryption succeeds and m is the corresponding cleartext.) When (enc, dec) is an authenticated encryption scheme, we have S 0 2 ≈ p1 S 1 2 , which means that the adversary can distinguish whether m 0 or m 1 was encrypted with probability at most p 1 , and for b ∈ {0, 1}, S b 2 satisfies the correspondence corr = inj-event(recv(m)) =⇒ inj-event(send(m))

(1) up to probability p 2 without public variables, which means that each execution of event recv(m) is preceded by a distinct execution of event send(m), up to cases of probability at most p 2 . (The probabilities p 1 and p 2 come from the probabilities of breaking the security properties of the encryption scheme.) By composing S 1 with S b 2 , we obtain

S b composed = C[let k = M in c 1 ; (Q 1 | c 4 ((m 0 : T m , m 1 : T m )); new r : T r ; event send(m b ); c 5 enc(m b , k, r) | c 6 (y : bitstring); let i ⊥ (m) = dec(y, k) in event recv(m))]
Let S b,• composed be obtained from S b composed by removing all events of S 1 . Let

V 1 = var(S 1 ) \ {k}. By Theo- rem 1, we have S b,• composed ≈ V1 p C [S b 2 ] for b ∈ {0, 1}. (The context C does not depend on b because C is independent of Q 2 in Theorem 1.) By Lemma 1, C [S b
2 ] satisfies the correspondence (1) up to probability p 2 with public variables V 1 , where p 2 (C 1 ) = p 2 (C 1 [C ]), and so S b,• composed satisfies (1) up to probability p 2 , where composed also satisfies (1) up to probability p 2 , since S 1 does not contain the events send and recv. Moreover, assuming S 1 does not contain events, we have

p 2 (C 1 ) = p (C 1 , t corr ) + p 2 (C 1 ) = p(C 1 ) + p 2 (C 1 ), C 1 runs in time at most t C1 +t enc +t dec +t corr , C 1 = C 1 [C ] runs in time at most t C1 +t C = t C1 +t C +t Q1 ,
S 0 composed = S 0,• composed ≈ V1 p C [S 0 2 ] ≈ V1 p 1 C [S 1 2 ] ≈ V1 p S 1,• composed = S 1 composed where p 1 (C 1 , t D ) = p 1 (C 1 [C ], t D ), so by transitivity, S 0 composed ≈ V1 2p +p 1 S 1
composed : in the composed system, the adversary can distinguish whether m 0 or m 1 was encrypted with probability at most 2p + p 1 .

Main Composition Results

This section presents our main composition theorems. We first need to introduce preliminary notions and lemmas.

Transferring Security Properties

We first generalize the notion of indistinguishability. The more general notion still allows us to transfer security properties from a process to another, as indistinguishability does by Lemma 1.

Definition 4. We write

Q ∼ → V,V f,p
Q if, and only if, for all evaluation contexts C acceptable for Q with public variables V and all distinguishers D that run in time at Indistinguishability corresponds to the particular case in which f is the identity: f (C) = C. Being able to transform the context C by the function f is useful in composition proofs, in particular because the variables are not always numbered in the same way in the symmetric key protocol and in the composed system. In this case, f performs the renumbering of the variables.

most t D , C = f (C) is an evaluation context acceptable for Q with public variables V such that | Pr[C[Q] : D] -Pr[C [Q ] : D]| ≤ p(C, t D ). Intuitively, Q ∼ → V,V f,p Q means that,
The rest of this section shows that

Q ∼ → V,V
f,p Q allows us to transfer indistinguishability, correspondence, and secrecy properties from

Q to Q. Lemma 2. If Q 1 ≈ V p Q 2 , Q 1 ∼ → V,V f,p1 Q 1 , and Q 2 ∼ → V,V f,p2 Q 2 , then Q 1 ≈ V p Q 2 , where p (C, t D ) = p 1 (C, t D ) + p (f (C), t D ) + p 2 (C, t D ).
Intuitively, if there is an adversary (represented by the context C), that can distinguish

Q 1 from Q 2 with probability p , then the properties Q 1 ∼ → V,V f,p1 Q 1 and Q 2 ∼ → V,V f,p2 Q 2 guarantee that there is a modified adversary (represented by the context C = f (C)) that can distinguish Q 1 from Q 2 with probability at least p (C, t D ) -p 1 (C, t D ) -p 2 (C, t D ). Since Q 1 ≈ V p Q 2 ,
this probability is at most p (f (C), t D ), so we obtain Lemma 2. Lemma 3 is a similar result for correspondences. Lemma 3. If Q satisfies a correspondence corr with public variables V up to probability p and

Q ∼ → V,V f,p Q
, where f is such that when C does not contain events used by corr , neither does f (C), then Q satisfies corr with public variables V up to probability p , where p (C) = p(C, t corr ) + p (f (C)).

Definition 5. Assuming

Q ∼ → V,V f,p
Q , we say that f is secrecy-preserving for x → (x, f sec ) when we have: If Q preserves the secrecy of x with public variables V \ {x } up to probability p , x ∈ V , and x ∈ V , then Q preserves the secrecy of x with public variables V \{x} up to probability p , where p

(C 0 ) = 2p(C 0 [[ ] | R x ], t S ) + p (f sec (C 0 )).
Definition 5 just defines that function f allows us to transfer secrecy properties. This property holds in particular when, for every evaluation context C 0 acceptable for

Q | R x with public variables V \ {x}, there exist C 0 and C 0 such that f (C 0 [[ ] | R x ]) = C 0 [C 0 [ ] | R x ].
This condition guarantees that f preserves the form of contexts that we use to test secrecy

C 0 [[ ] | R x ],
just allowing the addition of a context C 0 before the secrecy test; this addition preserves secrecy by Lemma 1. (This result is detailed in [15, Appendix A.5, Lemma 10].) In our composition proofs, we use this condition, as well as others detailed in the proofs themselves.

Hash Oracles

The systems S 1 and S 2 that we compose may use hash oracles. In this paper, we consider only non-programmable random oracles. The systems S 1 and S 2 may share the same hash oracles, which appear once in the composed system. To allow the sharing of oracles between S 1 and S 2 , we must treat these oracles specially. In this section, we introduce notations and a lemma that allow us to do that.

We assume that there are L hash oracles (L ≥ 1), and use the following notations: for each l ≤ L, h l is a function of type T hk h,l × T h,l → T h,l ,

Q h = L l=1 ! i h,l ≤n h,l c h3,l [i h,l ](x h,l : T h,l ); c h4,l [i h,l ] h l (hk h,l , x h,l ) C h = c h1 (); new hk h,1 : T hk h,1 ; . . . new hk h,L : T hk h,L ; c h2 ; ([ ] | Q h )
The context C h first chooses the keys hk h,l (l ≤ L). This choice models the choice of the random oracles themselves.

It is triggered by the reception of a message on c h1 and followed by an output on c h2 . Then, C h runs the process Q h in parallel with the hole. The process Q h represents L hash oracles: the l-th hash oracle can be called at most n h,l times; it receives its argument x h,l on channel c h3,l [i h,l ] (i h,l ≤ n h,l ) and returns the hash of x h,l on channel c h4,l [i h,l ]. We use

L l=1 Q l to denote the parallel compo- sition Q 1 | . . . | Q L .
The context C h is not an evaluation context (because it always chooses the keys hk h,l before running the process in the hole). Let Q h and C h be obtained from Q h and C h by renaming the replication bounds n h,l into n h,l and the channels c h1 , c h2 , c h3,l , c h4,l into c h1 , c h2 , c h3,l , c h4,l respectively. Similarly, let Q h and C h be obtained from Q h and C h by renaming the replication bounds n h,l into n h,l and the channels c h1 , c h2 , c h3,l , c h4,l into c h1 , c h2 , c h3,l , c h4,l respectively. We say that a process is hash-wellformed when, for all l ≤ L, it uses hk h,l only in terms of the form h l (hk h,l , M ) for some term M , it does not use the channels c h1 , c h2 , c h3,l , c h4,l , c h1 , c h2 , c h3,l , c h4,l , c h1 , c h2 , c h3,l , c h4,l , and it does not use the variables x h,l .

In the particular case in which there is no hash oracle (L = 0), we define

C h = C h = C h = [ ], the empty context.
Given a process Q, we write n h,l,Q for the maximum number of evaluations of h l (hk h,l , . . . ) in Q. The same notation applies to contexts C and terms M .

The next lemma is the main technical tool that we use to deal with hash oracles. It allows us to move the hash oracles under an evaluation context. Lemma 4. If C is an evaluation context and C[Q] is hashwell-formed, then there exists an evaluation context C such that for all V such that V ∩ var(C h ) = ∅,

C h [C[Q]] ≈ V 0 C [C h [Q]]
where the context C is independent of Q, runs in time at most t C , and for all l ≤ L, C calls the l-th hash oracle in C h at most n h,l,C times, so n h,l = n h,l + n h,l,C . (The symbol n h,l occur in C h and n h,l occurs in C h .) The other parameters of C are the same as those of C.

In this lemma, the context C directly calls the hash functions h l , while the context C performs the same hash evaluations by calling the hash oracles defined by Q h inside C h . (The context C cannot call h l directly, because it does not have access to the keys hk h,l . The context C cannot call the hash oracles of C h because it is hash-well-formed, so it does not use the channels c h3,l and c h4,l .)

Replication

When we compose a key exchange protocol S 1 with a protocol S 2 that uses the key, we typically run n sessions of the key exchange, and each session produces a fresh key. Therefore, we need to consider n independent sessions of S 2 , each with a different fresh key. In this section, we show how to infer security properties (indistinguishability, secrecy, correspondences) of a protocol that runs n independent sessions from the properties of a protocol that runs a single session. (In the vocabulary of [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], we consider that the protocol that uses the key is single-session reducible, and we obtain results similar to theirs for the reduction to a single session [17, Appendix B], but in the context of CryptoVerif.)

Let us consider a protocol Q that runs a single session. We can model a protocol that runs n sessions of Q by adding a replication at the top of Q: ! i≤n Q. Then all variables defined in Q implicitly have one more index, i, because they are defined under ! i≤n . That allows us to distinguish the variables used in different sessions. However, this is not sufficient: we want the adversary to be able to know to (resp. from) which session it sends (resp. receives) messages, so we add the replication index i to the channels of inputs and outputs in Q. Similarly, we can add the replication index i as argument of events in Q, to be able to relate events that belong to the same session. Considering the process S b 2 of Example 1, that yields:

! i≤n c 2 [i](); new k : T ; c 3 [i] ; (c 4 [i]((m 0 : T m , m 1 : T m )); new r : T r ; event send(i, m b ); c 5 [i] enc(m b , k, r) | c 6 [i](y : bitstring); let i ⊥ (m) = dec(y, k) in event recv(i, m))
and this process satisfies the correspondence

inj-event(recv(i, m)) =⇒ inj-event(send(i, m))
that is, each execution of recv(i, m) is preceded by a distinct execution of send(i, m), up to cases of negligible probability. In this process, partnered sessions (which use the same key k) have the same replication index i. However, this property is not preserved by composition: in a key exchange protocol, partnered sessions are typically the ones that exchange the same messages, and they do not necessarily have the same replication index. This will also be true in the composed system. Partnered sessions can then be determined by a session identifier computed from the messages exchanged in the protocol, as in [START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF], [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF], [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Canetti | Analysis of key-exchange protocols and their use for building secure channels[END_REF]: partnered sessions have the same session identifier. In the composition, the session identifier will be determined by the key exchange protocol. Therefore, we consider that the protocol that uses the key receives the session identifier in a variable x, as follows:

! i≤n c 2 [i](x : T sid ); new k : T ; c 3 [i] ; (c 4 [i]((m 0 : T m , m 1 : T m )); new r : T r ; event send(x, m b ); c 5 [i] enc(m b , k, r) | c 6 [i](y : bitstring); let i ⊥ (m) = dec(y, k) in event recv(x, m))
We use the session identifier x instead of the replication index i in events. The only missing ingredient in the above process is that the same session identifier should never be used twice, to avoid confusions between several sessions. The find construct allows us to verify that, by comparing x to the previously received session identifiers. This explanation leads us to the following definition: Definition 6. Given a process P , and replication indices i and a variable x that do not occur in P , we write AddIdxSid( i ≤ n, x : T sid , P ) for the process obtained by adding indices i at the beginning of each sequence of indices of channels in inputs and outputs and at the beginning of the indices of each variable defined in P (implicit when current replication indices are omitted), and adding variable x at the beginning of each event.

Given a correspondence corr , we write AddSid(T sid , corr ) for the correspondence obtained by choosing a fresh variable x of type T sid and adding it at the beginning of each event in corr . When Q is of the form Q = c(); P and the channels c and c and the replication indices i do not occur in P , we define

AddReplSid( i ≤ n, c , T sid , Q) = ! i≤ n c [ i](x : T sid ); find u = i ≤ n suchthat defined(x[ i ], x [ i ]) ∧ x = x[ i ] then yield else let x = cst in AddIdxSid( i ≤ n, x : T sid , P )
where x, x , and u are fresh variables.

The process AddReplSid( i ≤ n, c , T sid , Q) is the replicated version of process Q = c(); P : it corresponds to n copies of Q indexed by i ≤ n, as shown by the replication ! i≤ n . However, it additionally manages the session identifier and replication indices as detailed in the explanation above. The first input in AddReplSid( i ≤ n, c , T sid , Q) receives the session identifier x, the subsequent find checks that the same x is never used twice, so that there is a bijection between the value of x and the replication indices i. (When the received session identifier x is equal to a previous one x[ i ] with which P was run, it just executes yield, which returns control to the adversary. We record that P is run in session i by defining the variable x [ i] as a constant value cst. The find requires that x [ i ] be defined, which means that P was run in session i . In particular, i = i, because x [ i] is not defined yet when the find is executed.) Finally, the process P that follows the input is executed, with the appropriate additions of the replication indices i or the session identifier x to channels, variables, and events, as defined by AddIdxSid( i ≤ n, x : T sid , P ).

Lemmas 5 and 6 below show that indistinguishability, secrecy, and correspondence properties are preserved by adding a replication. The hash oracles, when present, are left outside the replication. Lemma 5. Suppose that V ∩ var(C h ) = ∅, Q = c(); P , Q = c(); P , Q and Q are hash-well-formed and do not contain events,

Q ! = AddReplSid( i ≤ n, c , T sid , Q),
and

Q ! = AddReplSid( i ≤ n, c , T sid , Q ). If C h [Q] ≈ V p C h [Q ], then C h [Q ! ] ≈ V p C h [Q ! ] where p (C, t D ) = n × p(C , t D ) and the context C runs in time at most t C + ( n -1) × max(t Q , t Q ), calls the l-th hash oracle at most n h,l = n h,l + ( n -1) × max(n h,l,Q , n h,l,Q )
times where C calls the l-th hash oracle at most n h,l times, and the other parameters of C are the same as those of C. Lemma 6. Suppose that V ∩ var(C h ) = ∅, Q is a hashwell-formed process, and up to probability p 2 without public variables, where

Q ! = AddReplSid( i ≤ n, c , T sid , Q).

1) If

C h [Q] preserves
p 1 (C, t D ) = n × p 1 (C , t D ), p 2 (C) = n × p 2 (C )

Main Composition Theorem

Finally, we obtain our main composition theorem. In this theorem, stated below and illustrated in Figure 4, the system S 1 is a key exchange protocol that provides a key to two participants: A executes event e A and stores the key in k A and k A , and B executes event e B and stores the key in k B . The system S 2 creates a fresh key, and also involves two participants:

A executes Q 2A and B executes Q 2B . The S 1 : A B k A k B S 2 : replicated version of new k : T A Q 2A B Q 2B S composed : A B A Q 2A B Q 2B k A k B
(S 1 may run several sessions of A and B.) Theorem 2 (Main composition theorem). Let C be any context with two holes, with replications ! i≤ n above the first hole and ! i ≤ n above the second hole and without event abort. Let Q 1A and Q 1B be processes without event abort. Let k, k A , k B be variables of type T . Let

Q 1 = C[event e A (sid( msg A ), k A , i); let k A = k A in c A [ i] M A ; Q 1A , event e B (sid( msg B ), k B ); c B [ i ] M B ; Q 1B ] Q 2 = c 1 (); new k : T ; c 2 ; (Q 2A | Q 2B ) S 1 = C h [Q 1 ] S 2 = C h [AddReplSid( i ≤ n, c 1 , T sid , Q 2 )]
where Q 1 and Q 2 are hash-well-formed; msg A is a sequence of variables defined in C above the first hole and input or output by C above the first hole or by the output c A [ i] M A ; msg B is a sequence of variables input or output by C above the second hole; sid is a function that takes a sequence of messages and returns a session identifier of type T sid ; C, Q 1A , Q 1B , Q 2A , and Q 2B make all their inputs and outputs on pairwise distinct channels with indices the current replication indices; c A , c B , c 1 , c 1 , c 2 , k A , e A , e B do not occur elsewhere in S 1 , S 2 ; S 1 and S 2 have no common variable, no common channel, and no common event; S 1 and S 2 do not contain newChannel; and there is no defined condition in

Q 2 . Let Q 2A = AddIdxSid( i ≤ n, x : T sid , Q 2A ) and Q 2B = AddIdxSid( i ≤ n , x : T sid , Q 2B ). Let c A , c B be fresh channels. Let Q composed = C[event e A (sid( msg A ), k A , i); c A [ i] M A ; (Q 1A | Q 2A {k A /k, sid( msg A )/x}), event e B (sid( msg B ), k B ); c B [ i ] M B ; (Q 1B | Q 2B {k B /k, sid( msg B )/x})] S composed = C h [Q composed ]
Let S • composed be obtained from S composed by removing all events of S 1 .

Let

t 1 = t C + n×(t M A +t Q 1A )+ n ×(t M B +t Q 1B ) be an upper bound on the runtime of Q 1 , t 2 = n × t Q 2A + n × t Q 2B be an upper bound on the runtime of Q 2A and Q 2B in Q composed , n h,l,1 = n h,l,C + n × (n h,l,M A + n h,l,Q 1A ) + n × (n h,l,M B + n h,l,Q 1B ), and n h,l,2 = n × n h,l,Q 2A + n × n h,l,Q 2B . 1) If S 1 preserves the secrecy of k A with public vari- ables V (V ⊆ var(S 1 ) \ ({k A , k A } ∪ var(C h ))) up
to probability p and satisfies the correspondences

inj-event(e B (sid , k)) =⇒ inj-event(e A (sid , k, i)) (2)
event(e A (sid , k

1 , i 1 )) ∧ event(e A (sid , k 2 , i 2 )) =⇒ i 1 = i 2 (3)
with public variables V ∪{k A } up to probabilities p and p respectively, then there exists f such that, for any

V 1 ⊆ V ∪ (var(Q 2 ) \ ({k} ∪ var(C h ))), we have S • composed ∼ → V1,V2 f,p3 S 2 where V 2 = V 1 ∩ var(Q 2 ); p 3 (C 3 , t D ) = p(C 3 + t D ) + p (C 3 , t D ) + p (C 3 , t D )
and, assuming C 3 calls the l-th hash oracle n h,l times, the context C 3 runs in time at most t C3 + t 2 , calls the l-th hash oracle at most n h,l = n h,l + n h,l,2 times, and its other parameters are the same as those of C 3 ; f (C 3 ) contains the same events as C 3 , runs in time at most t C3 + t 1 , calls the l-th hash oracle at most n h,l = n h,l +n h,l,1 times, and its other parameters are the same as those of C 3 ; if y ∈ V 2 , then f is secrecy-preserving for y → (y, f sec ) where f sec (C 3 ) has the same parameters as f (C 3 ).

2) There exists an evaluation context C 4 such that, for any

V ⊆ var(S composed ) \ ({k A } ∪ var(C h )), we have S composed ≈ V 0 C 4 [S 1
] and C 4 is acceptable for S 1 with public variables k A , k B , contains the events of S 2 , runs in time at most t 2 , calls the l-th hash oracle at most n h,l,2 times, so n h,l = n h,l + n h,l,2 , and does not alter the other parameters. Moreover, f is independent of the details of Q 2A and Q 2B : it depends only on the channels of Q 2B , whether

A B n fresh nonce n ← - k A fresh key event e A ((n, m 2 ), k A , i) m2 --→ event e B ((n, m 2 ), k A )
where m 2 = enc(concat(k A , n), k lt , r ).

Figure 5. A simple key exchange protocol they are for input or for output, under which replications and with which type of data;

C 4 is independent of Q 1A and Q 1B .
This theorem requires the key exchange to satisfy the following security properties. It must guarantee the secrecy of the key obtained by A, k A , and injective authentication of A and B, as formalized by the correspondence (2). This correspondence means that each execution of event e B ( msg, k) is preceded by a distinct execution of event e A ( msg, k, i) for some i, except in cases of probability at most p . These two properties imply secrecy of the obtained key on B's side, since all keys that B has are also keys that A has. The correspondence (3) means that the event e A is executed at most once for each session identifier sid , since all such executions must have the same replication indices i. It allows us to use the session identifier sid as argument x to identify the session in the system S 2 . It is easy to prove in practice, both using CryptoVerif and manually: it is sufficient to notice that sid contains fresh randomness in each execution of e A , for instance a nonce or an ephemeral public key.

The assumption that S 1 and S 2 do not contain newChannel guarantees that all channels are public. It is not a limitation in practice, because CryptoVerif does not support newChannel in protocol specifications; newChannel is used only in manual proofs. We require that the inputs and outputs use distinct channels with indices the current replication indices, to identify channels unambiguously. The assumption that there is no defined condition in Q 2 facilitates a renumbering of variables: the variables of

Q 2B have indices i in S 2 but i in S composed .
Like Theorem 1, the first conclusion of Theorem 2 allows us to transfer security properties proved on S 2 to S composed , this time by relying on Section 5.1. We cannot prove indistinguishability here, because the variables of Q 2B are renumbered as mentioned above: since these variables may be public, the renumbering may affect the context as well. The second conclusion allows us to transfer security properties proved on S 1 to S composed by Lemma 1, provided they are proved with public variables including k A and k B , since C 4 uses k A and k B .

In our TLS case study, we apply this theorem to perform most compositions: the handshakes with the record protocol, using a traffic secret as common key, as well as the handshake with pre-shared key with itself and the initial handshake with the handshake with pre-shared key, using the pre-shared key as common key. However, this theorem does not apply for the client early traffic secret cets, because of the possibility of replays. (Theorem 3 deals with this case.) The next example illustrates the theorem on a simpler case. Example 3. Let us suppose that there are no hash oracles and consider the following very simple key exchange protocol, also shown in Figure 5:

S 1 = c 7 (); new k lt : T ; c 8 ; ((! i A ≤n A c 9 [i A ](n : T nonce ); new k A : T ; new r : T r ; let m 2 = enc(concat(k A , n), k lt , r ) in event e A ((n, m 2 ), k A , i A ); let k A = k A in c A [i A ] m 2 ) | (! i B ≤n B c 10 [i B ](); new n : T nonce ; c 11 [i B ] n ; c 12 [i B ](m 2 : bitstring); let i ⊥ (concat(k B , =n)) = dec(m 2 , k lt ) in event e B ((n, m 2 ), k B ); c B [i B ] ))
After an input on channel c 7 , this process generates a long-term key k lt shared between A and B, returns control to the adversary by outputting on channel c 8 , and runs the participants A and B in parallel. The participant B (at the bottom) is run at most n B times. It waits for an input on channel c 10 [i B ], generates a fresh nonce n and sends it to A on channel c 11 [i B ]. If the session runs normally, the adversary forwards this nonce to channel c 9 [i A ] for some i A , so that A receives it, generates a fresh key k A , and computes the message m 2 that is the encryption of k A and n under k lt . (The function concat is concatenation.) Then, A executes the event e A to record that it accepts the key k A , in a session of session identifier (n, m 2 ). (In this example, the function sid is the pair.) It stores k A in k A and sends message m 2 on channel c A [i A ]. If the session runs normally, the adversary forwards this message to channel c 12 [i B ], so that B receives it, decrypts it, and in case of success, executes event e B to record that it terminates with key k B = k A , in a session of session identifier (n, m 2 ). Assuming that (enc, dec) is an authenticated encryption scheme, CryptoVerif shows that S 1 preserves the secrecy of k A up to probability p and satisfies (2) and (3) with public variables k A , k B up to probabilities p and p respectively, which depend on the probability of breaking the encryption scheme. We compose S 1 with the system S b 2! of Example 2. The syntactic assumptions are easy to check, and the composed system is

S b composed = c 7 (); new k lt : T ; c 8 ; ((! i A ≤n A c 9 [i A ](n : T nonce ); new k A : T ; new r : T r ; let m 2 = enc(concat(k A , n), k lt , r ) in event e A ((n, m 2 ), k A , i A ); c A [i A ] m 2 ; c 4 [i A ]((m 0 : T m , m 1 : T m )); new r : T r ; event send((n, m 2 ), m b ); c 5 [i A ] enc(m b , k A , r) ) | (! i B ≤n B c 10 [i B ](); new n : T nonce ; c 11 [i B ] n ; c 12 [i B ](m 2 : bitstring); let i ⊥ (concat(k B , =n)) = dec(m 2 , k lt ) in event e B ((n, m 2 ), k B ); c B [i B ] ; c 6 [i B ](y : bitstring); let m = dec(y, k B ) in event recv((n, m 2 ), m)))
The composed protocol runs the key exchange as before, then it sends m b encrypted, as in S 2 . However, in A, it executes event send with session identifier (n, m 2 ) and encrypts with key k A . In B, it executes event recv with session identifier (n, m 2 ) and decrypts with key k B . These values are provided by the key exchange protocol. (The processes Q 1A and Q 1B are the process 0 that does nothing, so we simply omit them.) Let S b,• composed be obtained from S b composed by removing events e A and e B . Let t 1 = t 2 = n A t enc + n B t dec . By Theorem 2, item 1), for b ∈ {0, 1}, there exists

f such that S b,• composed ∼ → ∅,∅ f,p3 S b 2! where p 3 (C 3 , t D ) = p(C 3 + t D ) + p (C 3 , t D ) + p (C 3 , t D ), C 3 runs in time at most t C3 + t 2 , f (C 3 )
runs in time at most t C3 + t 1 , and their other parameters are the same as those of C 3 . Since f does not depend on the details of S b 2 , f does not depend on b. ) respectively. Therefore, we transferred security properties from S 1 and S b 2! to the composed system. The properties required on S 1 are closely related to the security of a key exchange protocol as defined in CryptoVerif [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF]. As in [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF], we require secrecy of the key obtained by A and injective authentication of A to B [START_REF] Arapinis | Verifying privacy-type properties in a modular way[END_REF]. The security of a key exchange includes mutual authentication, which is not needed for the composition. The correspondence (3) does not appear in [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF]. Combined with (2), it implies that sessions that share the same session identifier have the same key:

Since S 0 2! ≈ p 1 S 1 2! , by Lemma 2, S 0,• composed ≈ p4 S 1,• composed where p 4 (C, t D ) = 2p 3 (C, t D ) + p 1 (f (C), t D ).
event(e A (sid , k A , i 1 )) ∧ event(e B (sid , k B )) =⇒ k A = k B (4)
a property included in the definition of a key exchange in CryptoVerif [START_REF] Blanchet | Computationally sound mechanized proofs of correspondence assertions[END_REF]. Indeed, if e A (sid , k A , i 1 ) and e B (sid , k B ) are executed, then e A (sid , k B , i 2 ) is also executed for some i 2 by (2), which implies i 1 = i 2 by (3), so the two events e A (sid , k A , i 1 ) and e A (sid , k B , i 2 ) are actually the same event, so k A = k B . The converse is not true in general, because (2) and ( 4) put no constraints in case event e B is not executed with the considered session identifier. These properties are also closely related to the properties used in previous composition results [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF]. These results require key secrecy, as well as partnering or match security, which provides guarantees similar to (2) and (3). In particular, [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] require a public session matching algorithm, that is, the adversary knows which sessions are partnered. We also have this property: sessions are partnered when they have the same session identifier, and the session identifier is computed from public messages msg A and msg B by the function sid. This property is relaxed in [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF]: they allow to use keys of early stages (which are virtually revealed) in the session matching. In TLS 1.3, the handshake is encrypted, and the session matching should be done on the plaintext, so the handshake keys are indeed needed for the session matching. In the model we consider, instead of encrypting the handshake, the handshake keys are given to the adversary, so that it can encrypt and decrypt messages. The session matching can then be done with public data. We do not establish any security property that would rely on the encryption of the handshake.

However, the required properties still differ from [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] in their presentation. We make explicit the distinction between the two participants of the protocol, and (3) requires that A executes at most one session with a given session identifier. By (2), we obtain that B also executes at most one session with a given identifier. In contrast, [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] require that there are at most two sessions with the same identifier, without distinguishing A and B. The correspondence (2) guarantees that these two sessions have the same key, which is also required by [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF].

Our definition of the key exchange protocol S 1 allows much flexibility:

• In contrast to [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF], we do not assume that the key exchange protocol is a public-key protocol. In TLS 1.3, the handshake with pre-shared key indeed relies on a shared key, and may not need a long-term public key.

•

We encode "corrupt" queries, used to corrupt longterm keys, for instance to model forward secrecy, inside the context C. That allows us to deal with protocols that satisfy forward secrecy or not, without explicit distinction, in contrast to what [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] do. That also allows us to support keys that are forward secret only from a certain stage, as well as temporary keys, used in several sessions but not leaked by "corrupt" queries because their lifetime is short, as in the multi-stage framework of [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF].

•

As in [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF], the key exchange may continue running after accepting a key: it may send messages M A and M B and execute Q 1A and Q 1B . We allow composition with keys that are established before the last key exchange message, provided they are not used in the key exchange protocol. However, we cannot perform test queries on a stage-i key and still use it in the key exchange protocol; while [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] allow that, they do not allow composition for such keys. (In their vocabulary, these keys are not final.)

•

As in [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], the communication partner does not need to be known at the start of the protocol.

• Finally, we support key exchange protocols that guarantee mutual authentication, unilateral authentication, or no authentication, as [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF]. This point may seem counter-intuitive, since (2) requires unilateral authentication. However, the security properties are obviously proved only when the partner is honest. Therefore, the system S 1 executes the events e A , e B and stores the key in k A only when the partner is honest. (That can be tested using find when the partner is not authenticated.) Then, the correspondence (2) holds, and we can apply Theorem 2. When the partner is dishonest, we simply leak the key. Since no security property is desired in this case, we can trivially compose with any protocol that uses this key. This situation appears in TLS, when the client is not authenticated. In this case, the server considers that its partner is honest when the Diffie-Hellman share it receives has been sent by the honest client. This condition replaces client authentication and allows CryptoVerif to prove (2).

Non-injective Variant

The next theorem is a variant of Theorem 2 with noninjective authentication. In this case, the process Q 2B may be executed several times for each key. Previous work [START_REF] Brzuska | Composability of Bellare-Rogaway key exchange protocol[END_REF], [START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF], [START_REF] Fischlin | Multi-stage key exchange and the case of Google's QUIC protocol[END_REF] did not consider this case. Theorem 3 (Non-injective variant). The conclusion of Theorem 2 still holds with the following changes in the hypotheses:

Q 2 = c 1 (); new k : T ; c 2 ; (Q 2A | ! i ≤ n Q 2B ), Q 2B = AddIdxSid(∅ ≤ ∅, x : T sid , Q 2B )
where the notation ∅ designates the empty sequence, and the correspondence event(e B (sid , k)) =⇒ event(e A (sid , k, i))

instead of (2).

In the theorem above, the system S 1 satisfies noninjective authentication: the correspondence (5) means that for each execution of e B (sid , k), there is an execution of e A (sid , k, i). However, event e B (sid , k) can be executed several times for each execution of e A (sid , k, i). To compensate for that, the process Q 2B in Q 2 , inside the system S 2 , is replicated: it is under the replication ! i ≤ n , with the same indices as those above e B , so that it can also be executed several times for each shared key k. In the construction of the composed system, in Q 2B , we do not need to add replication indices to Q 2B , since Q 2B already contains the replication indices i ≤ n , because Q 2B is under the replication ! i ≤ n . Hence, the construction of Q 2B from Q 2B just adds the session identifier x.

In our TLS case study, we use this theorem to compose the handshake with pre-shared key with the record protocol using the client early traffic secret cets as common key. This theorem is needed because, in case ClientHello messages are replayed, several sessions of the server may obtain the same client early traffic secret, so the handshake does not guarantee injective authentication.

Extension to Tables

CryptoVerif also supports tables. Tables are lists of tuples shared between all honest participants of the protocol. The construct insert T bl(M 1 , . . . , M n ); P inserts element (M 1 , . . . , M n ) in table T bl, then runs P . The construct get T bl(x 1 , . . . , x l ) suchthat M in P else P tries to retrieve an element (x 1 , . . . , x l ) in the table T bl such that M is true. When such an element is found, it executes P with (x 1 , . . . , x l ) bound to that element. When no such element is found, it executes P . Equality tests = M i are also allowed instead of variables x i ; in this case, the table element must contain the value of M i at the i-th position.

The definition of AddIdxSid( i ≤ n, x : T sid , P ) (Definition 6) is extended to tables by adding variable x at the beginning of each insertion in a table, and adding the test = x at the beginning of each get in a table.

Theorems 1 and 2 require that S 1 and S 2 have no common table. In Theorem 2, the assumption that there is no defined condition in Q 2 is not a strong limitation since most usages of find with defined conditions can also be encoded using tables, and tables are allowed.

Application to TLS 1.3

In this section, we sketch the application of our composition theorems in order to compose the protocol pieces of TLS 1.3 as outlined in Figure 1. More details are given in [START_REF]Composition theorems for CryptoVerif and application to TLS 1.3[END_REF]Appendix B]. The composition theorems are generally easy to apply: their assumptions are either proved by CryptoVerif or syntactic and easy to verify, and the composed protocol is syntactically built from the two pieces that we compose. The TLS case study still presents two additional difficulties:

•

We compose protocols recursively an arbitrary number of times, in case there are successive handshakes with pre-shared keys or key updates in the record protocol, so we perform proofs by induction.

•

The secrecy of payload messages is expressed by the secrecy of a bit b in a process that sends message m b encrypted. We translate that into an indistinguishability between the process that sends m 0 and the one that sends m 1 (as S 0 2 ≈ p1 S 1 2 in Example 1). Then we perform compositions on these two processes and combine the obtained results in order to prove secrecy of messages for composed processes. The length of the composition proof is mostly due to the number of compositions that we perform between the various protocol pieces and the number of properties that we prove about these protocols.

In the composition, we first compose the record protocol with itself recursively by Theorem 1, using the secrecy of the updated traffic secret, to show that the security properties of the record protocol are preserved by key updates. We obtain a model of the record protocol that performs at most m key updates, for any m. We perform similar compositions for the 0-RTT variants. We put these protocols under replication by Lemmas 5 and 6, to model several sessions of the record protocol with independent traffic secrets.

Second, we compose the handshake with pre-shared key with the record protocol, using secret keys cats and sats, by Theorem 2. We also compose them with secret key cets, using Theorem 3 and the first 0-RTT variant of the record protocol, mentioned in Section 3, when the ClientHello message is unaltered, and using the theorem shown in [START_REF]Composition theorems for CryptoVerif and application to TLS 1.3[END_REF]Appendix A.12] by lack of space and the second 0-RTT variant when the ClientHello message is altered. We also compose the obtained process with itself recursively, using the resumption secret resumption secret as pre-shared key in the next handshake, by Theorem 2, and put it under replication by Lemmas 5 and 6. These compositions yield processes that perform at most l successive handshakes with pre-shared key and m key updates.

Third, we compose the initial handshake with the record protocol, using secret keys cats and sats, by Theorem 2. We also compose the initial handshake with the process that runs handshakes with pre-shared key, using the resumption secret resumption secret as pre-shared key, by Theorem 2.

In all these compositions, CryptoVerif proves all secrecy and correspondence properties required by the theorems. The composed protocol inherits security properties from the components we compose. Therefore, these compositions allow us to infer security properties of the TLS protocol from properties of the handshakes and the record protocol. In particular, we obtain message secrecy, message forward secrecy (with respect to the compromise of long-term client and server keys), and injective message authentication for non-0-RTT application messages in both directions. For 0-RTT messages, since the handshake does not prevent replays for cets, we obtain non-injective authentication instead of the injective one. The correspondence properties of the handshakes are inherited by the composition and we also obtain secrecy of the exported master secrets ems provided by the various handshakes.

Conclusion

This paper presents several composition theorems, to compose a protocol that provides a key (e.g., a key exchange protocol) with a protocol that uses this key. These theorems rely on the computational model of cryptography. They are expressed in the framework of the tool CryptoVerif, so they are easily applicable when each protocol to compose is proved secure by CryptoVerif. They provide great flexibility. In particular, they allow the composed protocols to share hash oracles, and they support non-injective as well as injective authentication.

We apply these theorems to TLS 1.3. This is an important case study, which illustrates well the power of our results. It allows us to prove security for any number of successive handshakes and key updates, a result that would be out of scope of CryptoVerif without composition, because this tool does not support loops. However, our theorems are of much more general interest, and we expect them to be applied to other protocols in the future. For instance, they apply as soon as a key exchange protocol provides a key to a cleanly separated transport protocol, a situation desirable in the design of many protocols.

Our results are specific to the CryptoVerif tool. We see no obstacle to recasting them in the framework of other tools that perform proofs in the computational model, such as EasyCrypt [START_REF] Barthe | EasyCrypt: A tutorial[END_REF], [START_REF] Barthe | Computeraided security proofs for the working cryptographer[END_REF]. However, although the general approach would be the same, a lot of our work would probably have to be redone to adapt the result to the language and formalism of each new tool. The assumptions of our theorems are either proved by CryptoVerif or syntactic and easy to verify. If desired, it would not be difficult to automate their verification and the application of the theorems in CryptoVerif. However, automating the application to TLS 1.3 would be more complicated, due to the additional difficulties mentioned at the beginning of Section 7. An interesting future work would also be to prove composition results with a key exchange protocol that already uses the key, for instance for key confirmation, in the line of [START_REF] Brzuska | Less is more: relaxed yet composable security notions for key exchange[END_REF].

Figure 1 .

 1 Figure 1. Structure of the composition

S

Example 1 .

 1 Consider the system S b 2 defined by S b 2 = c 2 (); new k : T ; c 3 ; (c 4 ((m 0 : T m , m 1 : T m )); new r : T r ; event send(m b ); c 5 enc(m b , k, r) | c 6 (y : bitstring); let i ⊥ (m) = dec(y, k) in event recv(m))

  and their other parameters are the same as those of C 1 . (The other parameters of C 1 = C 1 [C ] are the same as those of C 1 because C does not alter these parameters.) Therefore, S b

  for each adversary against Q (represented by the context C), there exists a modified adversary against Q (represented by the context C = f (C)) such that C[Q] and C [Q ] behave similarly. (The difference between the probabilities Pr[C[Q] : D] and Pr[C [Q ] : D] is at most p(C, t D ).)

Figure 4 .

 4 Figure 4. Illustration of Theorem 2

Since S b 2 !

 2 satisfies (1) up to probability p 2 , by Lemma 3, S b,• composed satisfies (1) up to probability p 5 (C) = p 3 (C, t corr ) + p 2 (f (C)), and so does S b composed . By Theorem 2, item 2), there exist evaluation contexts C b 4 such that S b composed ≈ 0 C b 4 [S 1 ] and C b 4 is acceptable for S 1 with public variables k A , k B , runs in time at most t 2 , and does not alter the other parameters. Since S 1 satisfies (2) and (3) with public variables k A , k B up to probabilities p and p respectively, by Lemma 1, C b 4 [S 1 ] and S b composed satisfy (2) and (3) up to probabilities p 1 (C) = p (C[C b 4 ]) and p 1 (C) = p (C[C b 4 ]

  the secrecy of x with public variables V up to probability p with x / ∈ var(C h ) and Q does not contain event abort, then C h [Q ! ] preserves the secrecy of x with public variables V up to probability p ; and 2) if C h [Q] satisfies the correspondence corr with public variables V up to probability p, then C ) and the context C runs in time at most t C + ( n -1)t Q , calls the l-th hash oracle at most n h,l = n h,l +( n-1)n h,l,Q times where C calls the l-th hash oracle at most n h,l times, and the other parameters of C are the same as those of C.

	Example 2. Letting S b 2! = AddReplSid(i ≤ n, c 2 , T sid , S b 2 ), by Lemma 5, we obtain S 0 2! ≈ p 1 S 1 2! and by Lemma 6, S b 2! satisfies the correspondence

h [Q ! ] satisfies the correspondence AddSid(T sid , corr ) with public variables V up to probability p ; where p (C) = n × p(C inj-event(recv(x, m)) =⇒ inj-event(send(x, m))

  , and C runs in time at most t C + (n -1) × t S b 2 and its other parameters are the same as those of C. (Note that

	t S 0 2 = t S 1 2 .)

  composed system S composed combines S 1 and S 2 so that A executes Q 2A with the key k A and B executes Q 2B with the key k B , after the key exchange S 1 provides the key. These systems may share hash oracles, included in C h , C h , and C h . (These contexts use the same hash functions. The hash oracles are omitted in Figure4.)We write P {M/x} for the process obtained from P by substituting M for x. We denote by C + t D a context that runs in time at most t C + t D and such that the other parameters of C + t D are the same as those of C.

Acknowledgements. This work was partly supported by ANR TECAP (decision number ANR-17-CE39-0004-03) and H2020 NEXTLEAP.