Karthikeyan Bhargavan
email: karthikeyan.bhargavan@inria.fr

Antoine Delignat-Lavaud

Cédric Fournet
email: fournet@microsoft.com

Markulf Kohlweiss
email: markulf@microsoft.com

Jianyang Pan

Jonathan Protzenko

Aseem Rastogi
email: aseemr@microsoft.com

Nikhil Swamy
email: nswamy@microsoft.com

Santiago Zanella-Béguelin
email: santiago@microsoft.com

Jean Karim Zinzindohoué
email: jean-karim.zinzin-dohoue@inria.fr

Implementing and Proving the TLS 1.3 Record Layer

Keywords:

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Transport Layer Security (TLS) is the main protocol for secure communications over the Internet. With the fast growth of TLS traffic (now most of the Web [START_REF] Swire | Online privacy and ISPs: ISP access to consumer data is limited and often less than access by others[END_REF]), numerous concerns have been raised about its security, privacy, and performance. These concerns are justified by a history of attacks against deployed versions of TLS, often originating in the record layer.

History and Attacks Wagner and Schneier [START_REF] Wagner | Analysis of the SSL 3.0 protocol[END_REF] report many weaknesses in SSL 2.0. The MAC construction offers very weak security regardless of the encryption strength. The padding length is unauthenticated, allowing an attacker to truncate fragments. Stream closure is also unauthenticated; although an end-ofstream alert was added in SSL 3.0, truncation attacks persist in newer TLS versions [START_REF] Bhargavan | Triple handshakes and cookie cutters: Breaking and fixing authentication over TLS[END_REF][START_REF] Smyth | Truncating TLS connections to violate beliefs in web applications[END_REF].

The original MAC-pad-encrypt mode is not generically secure [START_REF]The order of encryption and authentication for protecting communications (or: how secure is SSL?)[END_REF] and is brittle in practice, despite encouraging formal results for specific algorithms [START_REF] Almeida | Verifiable side-channel security of cryptographic implementations: Constant-time MEE-CBC[END_REF][START_REF] Bhargavan | Implementing TLS with verified cryptographic security[END_REF][START_REF] Paterson | Tag size does matter: Attacks and proofs for the TLS record protocol[END_REF]. Many padding oracle attacks have surfaced over the years, ranging from attacks exploiting straightforward issues (such as implementations sending padding error alerts after decryption) to more advanced attacks using side channels (such as Lucky13 [START_REF] Alfardan | Lucky thirteen: Breaking the TLS and DTLS record protocols[END_REF] or POODLE [START_REF] Möller | This POODLE Bites: Exploiting The SSL 3.0 Fallback[END_REF]). Even though padding oracle attacks are well known, they remain difficult to prevent in TLS implementations and new variants tend to appear regularly [START_REF] Somorovsky | Systematic fuzzing and testing of TLS libraries[END_REF]. The CBC mode of operation is also not secure against chosen-plaintext attacks when the IV is predictable (as in TLS 1.0), which is exploited in the BEAST attack [START_REF] Duong | Here come the ⊕ ninjas[END_REF]. Random explicit IVs [START_REF] Böck | Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS[END_REF] and CBC mode for 64-bit block ciphers [START_REF] Bhargavan | On the practical (in-)security of 64-bit block ciphers: Collision attacks on HTTP over TLS and OpenVPN[END_REF] are also vulnerable to birthday attacks. Finally, fragment compression can be exploited in adaptive chosen-plaintext attacks to recover secrets [START_REF] Rizzo | The CRIME Attack[END_REF].

Even with provably-secure algorithms, functional correctness and memory safety are essential, inasmuch as implementation bugs can easily nullify security guarantees. For instance, the OpenSSL implementation of ChaCha20-Poly1305 has been found to contain arithmetic flaws [START_REF] Böck | Wrong results with Poly1305 functions[END_REF] and more recently, a high severity buffer overflow vulnerability [START_REF] Święcki | ChaCha20/Poly1305 heap-buffer-overflow[END_REF].

Changes in TLS 1. [START_REF] Badertscher | Augmented secure channels and the goal of the TLS 1.3 record layer[END_REF] The IETF aims to robustly fix the weaknesses of the record layer by adopting a single AEAD mode for all ciphersuites, thus deprecating all legacy modes (MAC-only, MAC-pad-encrypt, RFC 7366 [START_REF] Gutmann | Encrypt-then-MAC for Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS)[END_REF] encrypt-then-MAC, compress-then-encrypt). The new AEAD mode is designed to be provablysecure and modular, supporting algorithms such as AES-GCM, AES-CCM, and ChaCha20-Poly1305 within the same framework. The usage of AEAD has also been improved: authentication no longer relies on associated data, whereas implicit nonces derived from initialization vectors (IV) and sequence numbers yield better security and performance.

What is the Record Layer? TLS involves establishing and using many encryption keys. In the key exchange literature, a common viewpoint is to treat each key generated in the handshake as belonging to a specific, independent application. Under this model, the handshake encryption key is used only by the handshake to encrypt its own messages, and must be separate from the application data key used only to encrypt application data fragments. This model does not fit the actual use of keys in TLS: it fails to capture TLS 1.2 renegotiation (where handshake messages are interleaved with the application data stream), TLS 1.3 post-handshake authentication and re-keying, or even alerts in any TLS version. In our modularization of TLS, following Bhargavan et al. [START_REF] Bhargavan | Implementing TLS with verified cryptographic security[END_REF], we consider that each sub-protocol of TLShandshake, change cipher spec (CCS), alert and application data (AppData)-defines its own data stream. The role of the record is to multiplex all of these streams into one, corresponding to network messages after fragmentation, formatting, padding, and optional record-layer encryption. Under this model, the record layer is the exclusive user for all non-exported keys generated by the handshake, and there is no need to assign keys to any given sub-protocol stream. Figure 1 illustrates the stream multiplexing for a TLS 1.3 connection with 0-RTT data and one rekeying from the point of view of the client. Separate channels are used for writing and reading. Within each channel, a band in the figure represents a stream, and arrows represent message fragments (incoming for left arrows, outgoing for right arrows) over time (flowing from left to right). Dashed arrows represent fragments used to signal key changes to the record layer. In TLS 1.2, CCS messages signal key changes; in TLS 1.3 this function is taken over by handshake messages. Related Work Since the first draft of TLS 1.3 in April 2014, the handshake and key schedule have undergone significant analysis efforts [START_REF] Cremers | Automated analysis and verification of TLS 1.3: 0-RTT, resumption and delayed authentication[END_REF][START_REF] Dowling | A cryptographic analysis of the TLS 1.3 handshake protocol candidates[END_REF][START_REF] Fischlin | Key confirmation in key exchange: A formal treatment and implications for TLS 1.3[END_REF][START_REF] Jager | On the security of TLS 1.3 and QUIC against weaknesses in PKCS#1 v1.5 encryption[END_REF][START_REF] Kohlweiss | de-) constructing TLS 1.3[END_REF][START_REF] Krawczyk | The OPTLS protocol and TLS 1.3[END_REF] as their design evolved over 19 iterations (at the time of writing). In contrast, few authors have analyzed changes to the record layer: Fischlin et al. [START_REF] Fischlin | Data is a stream: Security of stream-based channels[END_REF] and Badertscher et al. [START_REF] Badertscher | Augmented secure channels and the goal of the TLS 1.3 record layer[END_REF] analyze an early draft that did not feature many of the current changes (for instance, it still relied on associated data to authenticate record meta-data), and Bellare and Tackmann [START_REF] Bellare | The multi-user security of authenticated encryption: AES-GCM in TLS 1.3[END_REF] specifically focus on the way nonces are derived from IVs. This focus on the handshake protocol may be explained by the difficulty of analyzing the record independently of the handshake, and more generally, of defining the precise scope of its functionality.

As noted by several authors [START_REF]A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol[END_REF][START_REF] Jager | On the security of TLS-DHE in the standard model[END_REF], TLS occasionally uses the same keys to encrypt handshake messages and application data, e.g., for finished and post-handshake messages. This, unless carefully modeled in a custom security model [START_REF] Bhargavan | Implementing TLS with verified cryptographic security[END_REF] breaks key-indistinguishability. Authenticated and Confidential Channel Establishment (ACCE) [START_REF] Jager | On the security of TLS-DHE in the standard model[END_REF][START_REF] Krawczyk | On the security of the TLS protocol: A systematic analysis[END_REF] is a game-based model that combines the handshake and the record protocols to preempt these composition problems. While ACCE models capture complex features of TLS 1.2 such as renegotiation [START_REF] Giesen | On the security of TLS renegotiation[END_REF], its focus is primarily on the handshake, and it is unclear how to capture features such as post-handshake authentication [START_REF]A cryptographic analysis of the TLS 1.3 draft-10 full and pre-shared key handshake protocol[END_REF]. Other limits of ACCE models are discussed in [START_REF] Badertscher | Augmented secure channels and the goal of the TLS 1.3 record layer[END_REF]. A recent paper by Krawczyk [START_REF]A unilateral-to-mutual authentication compiler for key exchange[END_REF] proposes a new security definitions based on a key usability [START_REF] Datta | Computationally sound compositional logic for key exchange protocols[END_REF] rather than key indistinguishability to address this challenge. Our contributions We provide a reference implementation of the TLS record layer and its underlying cryptographic algorithms using the F programming language. We define security as an indistinguishability game and show a reduction with concrete bounds (Table 1) for any distinguisher to standard, low-level cryptographic assumptions. Our proof structure is depicted in Figure 2; from the bottom up:

1. We build a generic library for one-time message authentication codes (MAC) based on the Wegman-Carter-Shoup construction. We implement the GHASH and Poly1305 algorithms, and we prove the functional correctness (with regards to mathematical specifications), memory safety, and encoding injectivity of the resulting low-level code ( §3). Similarly, we build a library for pseudo-random functions (PRF), and provide functionally-correct, memory-safe implementations for AES and ChaCha20 ( §4). We express the security guarantees of these libraries using cryptographic idealizations backed by game-based assumptions.

2. We describe a generic AEAD construction that captures both RFC 5288 [START_REF] Salowey | AES Galois Counter Mode (GCM) cipher suites for TLS[END_REF] for AES-GCM (as described in NIST SP800-38D [START_REF] Dworkin | Recommendation for block cipher modes of operation: Galois/Counter mode (GCM) and GMAC[END_REF]) and RFC 7539 [START_REF] Nir | ChaCha20 and Poly1305 for IETF protocols[END_REF] for ChaCha20-Poly1305 through an interface compatible with RFC 5116 [START_REF] Mcgrew | An interface and algorithms for authenticated encryption[END_REF]. We show that this construction satisfies a standard notion of AEAD security ( §5) that combines indistinguishability under chosen-plaintext attacks (IND-CPA) with ciphertext integrity (INT-CTXT). Our proof applies to our F implementation and, based on the idealizations of our two libraries, is verified by typing-as are the following three steps:

3. From AEAD, we build and verify stream encryption, which uses AEAD nonces and record sequence numbers according to the TLS version-specific format ( §6).

4. From stream encryption, we build a length-hiding encryption interface by adding padding, the TLSspecific content type multiplexing, and version-specific associated data ( §7).

5. From length-hiding stream encryption with multiplexing, we implement the TLS record layer by adding interfaces to the handshake and alert sub-protocols that extend streams to sequences of streams by installing and enabling keys ( §8). This captures novel protocol features of TLS 1.3 such as early application data (0-RTT and 0.5 RTT), late handshake messages, and re-keying. Based on our security bound, we propose a re-keying strategy that compensates for potential weaknesses in AES-GCM.

6. We evaluate our implementation of the TLS record layer ( §9) by linking our AES-GCM and ChaCha20-Poly1305 ciphersuites to the handshake implementation of miTLS [START_REF] Bhargavan | Implementing TLS with verified cryptographic security[END_REF]. We confirm network interoperability with other TLS libraries both for TLS 1.2 and TLS 1.3 draft-14 and draft-18. Our code and formal development maximize reuse between TLS 1.2 and 1.3.

Additional Materials

The latest version of the paper is available from a companion website https://project-everest.github.io/record/. This website also provides links to online repositories that include all verified code we report on in the paper, as well as instructions on how to verify, extract and run the code. The code encompases several open-source projects, namely:

• The F programming language: https://github.com/FStarLang/FStar/, including libraries for fixed-size integer arithmetic and buffers.

• The kreMLin compiler from F to C, available at https://github.com/FStarLang/kremlin/.

• The development version of miTLS, extended to TLS 1.3, implemented in F : https://github.com/ mitls/mitls-fstar/. While verification of the full codebase is in progress, the repository contains verified protocol-specific code for the record layer fragment reported in this paper.

• The HACL cryptographic library: https://github.com/mitls/hacl-star/, notably including our verified code for cryptographic algorithms and the AEAD construction.

Compositional Verification by Typing

To implement and verify the record layer, we adopt a compositional approach to functional correctness and cryptographic security based on F [START_REF] Swamy | Dependent types and multimonadic effects in F*[END_REF], a dependently-typed programming language. This section explains our approach on two examples: arithmetic in a prime field for the Poly1305 algorithm, and basic authenticated encryption. We refer the reader to Fournet et al. [START_REF] Fournet | Modular code-based cryptographic verification[END_REF] for a general presentation of our approach and Barthe et al. [START_REF] Barthe | Probabilistic relational verification for cryptographic implementations[END_REF] for a probabilistic semantics of F and additional cryptographic examples. We use F not only to implement cryptographic constructions, but also as the formal syntax for their game-based security definitions. This is akin to the approach taken by Bhargavan et al. [START_REF] Bhargavan | Proving the TLS handshake secure (as it is)[END_REF] in their proof of a TLS 1.2 handshake implementation using F7, an ancestor of F . In contrast to F7, F supports an imperative programming style that is closer to pseudo-code used by cryptographers in code-based games [START_REF] Bellare | The security of triple encryption and a framework for code-based gameplaying proofs[END_REF]. For most of the paper, we use such pseudo-code instead of more precise and verbose F code. We do not assume familiarity with F and elide details of its syntax, such as type annotations, that are not relevant for the developments in this paper.

Functional Correctness of Poly1305

As a first example in F syntax, we specify arithmetic in the field GF (2 130 -5) for the Poly1305 MAC algorithm as follows: let p = 2^130 -5 ( * the prime order of the field * ) type elem = n:nat {n < p} ( * the type of field elements * ) let x +@ y : Tot elem = (x + y) % p ( * field addition * ) let x * @ y : Tot elem = (x * y) % p ( * field multiplication * )

This code uses F mathematical (unbounded) natural numbers to define the prime order p of the field and the type of field elements. (The formula {n < p} line 2 states that this type is inhabited by natural numbers n smaller than p.) The code also defines two infix operators +@ and * @ for addition and multiplication in the field, relying on primitive, unbounded integer arithmetic. Their result is annotated with types Tot elem, to indicate that these operations are pure total functions that return field elements. Hence, the F typechecker automatically checks that their result is in the field; it would report an error if e.g. we omitted the reduction modulo p. These operations are convenient to specify polynomial computations (see §3.2) but highly inefficient.

Instead, typical 32-bit implementations of Poly1305 represent field elements as mutable arrays of 5 unsigned 32-bit integers, each holding 26 bits. This low-level representation evenly spreads out the bits across the integers, so that carry-overs during arithmetic operations can be delayed. It also enables an efficient modulo operation for p. We show below an excerpt of the interface of our lower level verified implementation, relying on the definitions above to specify its correctness. The type repr defines the representation of field elements as F buffers (i.e., mutable arrays) of 5 32-bit integers. It is marked as abstract, to hide this representation from the rest of the code. Functions are declared with a series of argument types (separated by → ) ending with a return type and an effect (e.g. Tot or ST). Functions may have logical pre-and post-conditions that refer to their arguments, their result, and their effects on the memory. If they access buffers, they typically have a pre-condition requiring their caller to prove that the buffers are 'live' in the current memory (that is, they have been allocated and haven't been de-allocated yet) and they also explicitly state which buffers they modify.

The total function select is used only in specifications; it reads the value of an element from the program memory. We use it, for example, in the stateful specification of multiply. In the types above, we keep the memory argument implicit, writing select e0 and select e0 for the values of e0 in initial and final memories, respectively. (In real F code, pre-and post-conditions take these memories as explicit arguments.)

The multiply function is marked as ST, to indicate a stateful computation that may use temporary stackbased allocations. It requires that its arguments e0 and e1 be live and disjoint; it computes the product of its two arguments and overwrites e0 with the result. Its post-condition specifies the result in terms of the abstract field multiplication of the arguments.

Implementing and proving that multiply meets its mathematical specification involves hundreds of lines of source code, relying on a custom Bignum library with lemmas on integer representations and field arithmetic (see §9). Such code is easy to get wrong, but once F typechecks it, we are guaranteed that our low-level code is safe (e.g. it never accesses buffers out of bound, or de-allocated buffers) and functionally correct (since their results are fully specified). All F types and specifications are then erased, so that the compiled code only performs efficient low-level operations.

Authenticated Encryption: Real Interface Let us consider a simplified version of the authenticated encryption (AE) functionality at the core of the TLS record layer. In F , we may write an AE module with the following interface: Plaintexts and ciphertexts are represented here as immutable bytestrings of fixed lengths p and c . We frequently rely on type abbreviations to statically enforce length checks for fixed-length bytestrings using lbytes , and for bounded-length bytestrings using bbytes . (Our presentation uses immutable bytestrings for simplicity, whereas our record-layer implementation also uses mutable buffers of bytes.)

Next, our interface defines an abstract type key; values of this type can only be generated via keygen and accessed via encrypt and decrypt. The internal representation of keys is hidden from all other modules to protect their integrity and secrecy. The function keygen needs to generate randomness by calling an effectful external function; so we give this function the ST effect to indicate that the computation is impure and stateful (even though it does not explicitly modify the memory). In particular, two calls to keygen may yield different results. The function encrypt would typically generate a nonce for use in the underlying AE construction, and hence is also marked as stateful. In contrast, decrypt is deterministic, so is marked with the Tot effect. Its result is an optional plain value: either Some p if decryption succeeds, or None otherwise. In pseudo-code we write ⊥ for brevity.

Our interface does not express any security guarantees yet, but it does require a functional correctness guarantee, namely that decryption undoes encryption. Authenticated Encryption: Security Given an AE scheme, one usually measures its concrete security as the advantage of an adversary A that attempts to guess the value of b in the following game:

Game Ae(A, AE) b $ ← {0, 1}; L ← ∅; k $ ← AE.keygen() b ← A Encrypt,Decrypt (); return (b ? = b ) Oracle Encrypt(p) if b then c $ ← byte c ; L[c] ← p else c ← AE.encrypt k p return c Oracle Decrypt(c) if b then p ← L[c] else p ← AE.decrypt k c return p
The adversary A is a program that can call the two oracle functions to encrypt and decrypt using a secret key k. In the real case (b = 0) they just call the real AE implementation. In the ideal case (b = 1), Encrypt returns a randomly sampled ciphertext and stores the associated plaintext in a log L, while Decrypt performs decryption by looking up the plaintext in the log, returning ⊥ when there is no plaintext associated with the ciphertext. (In devising the Decrypt oracle we had a choice: we could instead have returned ⊥ when queried on a challenge ciphertext already recorded in L regardless of b. This strategy of rejecting challenge ciphertexts is idiomatic in cryptographic definitions in which Decrypt always returns ⊥ when b = 1. We decided to allow decryption of challenge ciphertexts when b = 0 and implement the ideal behavior when b = 1 using table lookup. This allows us to more closely align game-based definitions with idealized cryptographic libraries.) Ideal AE is perfectly secure, inasmuch as the ciphertext does not depend on the plaintext. Thus, we define AE security by saying that the attacker cannot easily distinguish between the real and ideal cases.

For this game, we define A's advantage probabilistically as |2 Pr[Ae(A, AE)] -1|, e.g. an adversary flipping a coin to guess b will succeed with probability 1 2 and has 0 advantage. In this paper, we adopt a more flexible notation for indistinguishability games: we keep the sampling of b and the call to the adversary implicit, and instead indicate the oracles available to this adversary. Hence, we write the game above (with the same oracles) equivalently as

Game Ae b (AE) L ← ∅ ; k $ ← AE.keygen(); return {Encrypt, Decrypt}
This notation facilitates the re-use of oracles for building other games, much like F modules. In general, we write G b to refer to an indistinguishability game G where the adversary A tries to guess the value of the random bit b by calling the oracles returned by G. For all such games, we equivalently define the advantage as

Pr[A G 1 = 1] -Pr[A G 0 = 1] .
Embedding games in F modules Although we wrote the game Ae b above in pseudo-code, each game in this paper reflects a verified F module, written e.g. AE b , that uses a boolean flag b to select between real and ideal implementations of the underlying cryptographic module AE. For example, AE b may define the key type and encrypt function as The interface declares keys as abstract, hiding both the real key value and the ideal log, and relies on the log to specify the effects of encryption and decryption. To this end, it provides a log function that reads the current content of the log-a sequence of ciphertexts and plaintexts. This function is marked as Spec, indicating that it may be used only in specification and will be discarded by the compiler after typechecking.

Each of the 3 ensures clauses above uses this proof-only function to specify the state of the log before (log k) and after the call (log k ). Hence, the interface states that, in the ideal case, the function keygen creates a key with an empty log; encrypt k p returns a ciphertext c and extends the log for k with an entry mapping c to p; and decrypt k c returns exactly the result of looking up for c in the current log. This post-condition formally guarantees that decrypt succeeds if and only if it is passed a ciphertext that was generated by encrypt; in other words it guarantees both functional correctness and authentication (a notion similar to INT-CTXT).

AE b is also parametrized by a module Plain b that defines abstract plaintexts, with an interface that allows access to their concrete byte representation only when b = 0 (for real encryption). By typing AE b , we verify that, when b = 1, our idealized functionality is independent (information-theoretically) from the values of the plaintexts it processes.

From the viewpoint of the application, the plaintext abstraction guarantees that AE 1 preserves the confidentiality and integrity of encrypted data (as in classic information flow type systems). An application can rely on this fact to prove application-level guarantees. For instance, an application may prove, as an invariant, that only well-formed messages are encrypted under a given key, and thus that parsing and processing a decrypted message always succeeds.

Probabilistic Semantics We model randomness (e.g. random_bytes) using primitive sampling functions. Two Boolean terminating F programs A 0 and A 1 are equivalent, written A 0 ≈ A 1 , when they return true with the same probability. They are -equivalent, noted

A 0 ≈ A 1 , when | Pr[A 1 ⇓ true] -Pr[A 0 ⇓ true]| ≤
where Pr[A ⇓ v] denotes the probability that program A evaluates to value v according to the probabilistic semantics of F . These definitions extend to program evaluation contexts, written A b [_], in which case depends on the program plugged into the context, which intuitively stands for the adversary. Equipped with these definitions, we can develop code-based game-playing proofs following the well-established approach of Bellare and Rogaway [START_REF] Bellare | The security of triple encryption and a framework for code-based gameplaying proofs[END_REF] directly applied to F programs rather than pseudo-code. For example, we can reformulate AE security as

AE 1 [A] ≈ AE 0 [A],
where A now ranges over well-typed Boolean programs parameterized by the two functions encrypt and decrypt defined by AE b . Our definition of -equivalence between real and ideal implementations of AE b matches the definition of A's advantage in the Ae b game.

Concrete security definitions and reductions

As illustrated for AE below, our security definitions will consist of a game and a notation for the adversary advantage, parameterized by a measure of oracle use (e.g. how many times an adversary calls an oracle is called). We intend to provide concrete bounds on those advantages, as a function of their parameters. To this end, our reduction theorems will relate the advantage for a given construction to the advantages of its building blocks.

Definition 1 (AE-security). Given AE, let Ae (A[q e , q d ]) be the advantage of an adversary A that makes q e queries to Encrypt and q d queries to Decrypt in the Ae b (AE) game.

Equipped with this definition and our idealized interface for AE, we can prove the security of programs using ideal AE (b = 1), say with advantage , and then bound the advantage of the same programs using real AE (b = 0) to + Ae (A[q e , q d ]).

We can either assume that this definition holds for our real AE module with an Ae that is small for realistic adversaries (possibly relying on functional correctness and some prior proof of security), or we can prove that our AES-GCM module (say) achieves some bound on Ae by reduction to a simpler assumptions on the AES cipher module. In later sections, we will show how we can precisely compute the adversary A's advantage in the game above from a related adversary B's advantage in winning the PRF game on the underlying cipher (e.g. AES). The proof relies on standard cryptographic game transformations that are applied, on paper, at the level of F code, combined with functional correctness proofs about the real and ideal code, verified automatically by F .

Games vs Idealized Modules

We conclude this presentation of our approach by discussing differences between the games on paper and the modules of our implementation.

Standard-compliant modules include many details elided in informal games; they also use lower level representations to yield more efficient code, and require additional type annotations to keep track of memory management.

These modules are part of a general-purpose verified cryptographic libraries, providing real functionality (when idealizations flags are off) so they always support multiple instances of their functionality. Here for instance, AE b has a function to generate keys, passed as parameters to the encrypt function, whereas the game oracle uses a single, implicit key. (This difference can usually be handled by a standard hybrid-argument reduction.)

Modules rely on the F type system to enforce the rules of the games. Hence, dynamic checks in games (say, to test whether a nonce has already been used) are often replaced with static pre-conditions on typed adversaries. Similarly, types enforce many important but trivial conditions, such as the length of oracle arguments, and are often kept implicit in the paper.

One-Time MACs

Anticipating on §5, the AEAD construction uses fresh key materials for each message, so we consider authentication when keys are used to compute at most one MAC.

We treat two main constructions, GHASH and Poly1305, using the same definitions, code, and proofs, inasmuch as possible. We initially suppose that the whole key is freshly generated for each MAC (as in ChaCha20-Poly1305) before presenting the general case where a part of the key is shared between multiple MACs (as in AES-GCM).

One-time MAC functionality and security

We outline below our interface for message authentication code (MAC), omitting its functional specification (see §9). This interface defines concrete byte formats for keys, tags, and messages. Authenticated messages are strings of at most m bytes that comply with an implementation-specific well-formedness condition. (We need such a condition for GHASH.) We let m range over well-formed messages.

Key-generation functions are marked as stateful (ST) to reflect their use of random sampling. Static keys of type key 0 may be used to generate multiple one-time keys of type key. (For example, keygen may concatenate the static key with kk 0 random bytes.) To begin with, we assume k 0 = 0 so that k 0 is the empty string ε.

The two main functions produce and verify MACs. Their correctness is captured in the verify postcondition of mac: verification succeeds at least on the tags correctly produced using mac with matching key and message.

One-Time Security MAC security is usually defined using computational unforgeability, as in the fol-lowing game:

Game UF-1CMA(A, MAC) k $ ← MAC.keygen(ε); log ← ⊥ (m , t ) ← A Mac return MAC.verify(k, m , t ) ∧ log = (m , t ) Oracle Mac(m) if log = ⊥ return ⊥ t ← MAC.mac(k, m) log ← (m, t) return t
The oracle permits the adversary a single chosen-message query (recorded in log) before trying to produce a forgery. The advantage of A playing the UF-1CMA game is defined as

UF-1CMA (A[ m ]) Pr[UF-1CMA(A, MAC) = 1].
We seek a stronger property for AEAD-the whole ciphertext must be indistinguishable from random bytes-and we need a decisional game for type-based composition, so we introduce a variant of unforgeability that captures indistinguishability from a random tag (when r is set).

Definition 2 (IND-UF-1CMA). Let Mac1 (A[ m , q v ]
) be the advantage of an adversary A that makes q v Verify queries on messages of length at most m in the following game:

Game Mac1 b (MAC) k $ ← MAC.keygen(ε); log ← ⊥ return {Mac, Verify} Oracle Verify(m , t ) if b return log = (m , t ) return MAC.verify(k, m , t ) Oracle Mac(m) if log = ⊥ return ⊥ t ← MAC.mac(k, m) if b ∧ r t $ ← byte MAC. t log ← (m, t) return t
In this game, the MAC oracle is called at most once, on some chosen message m; it returns a tag t and logs (m, t). Conversely, Verify is called q v times before and after calling MAC. When b is set, the game idealizes MAC in two ways: verification is replaced by a comparison with the log; and (when r is also set) the tag is replaced with random bytes.

We show (in the appendix) that our definition implies UF-1CMA when q v ≥ 1 and that random tags are neither necessary nor sufficient for unforgeability. We are not aware of much prior work on Mac1 with r set; a pairwise independent hash function would satisfy our IND-UF-1CMA definition but may require longer keys [START_REF] Sarkar | A trade-off between collision probability and key size in universal hashing using polynomials[END_REF].

Multi-Instance Security with a Shared Key In the AEAD construction, we instantiate a one-time MAC for every encryption and decryption. AES-GCM uses a static MAC key derived from the AEAD key and shared between all MAC instances. This state sharing is not captured by the games above. To this end, we extend the Mac1 b game into a multi-instance version MMac1 b with a setup that invokes the keygen 0 function to generate any key materials reused across instances.

In the multi-instance case it is convenient to support two kinds of instances: honest instances are created with Keygen and idealized as in Mac1 b ; dishonest instances are created with Coerce and use the real implementation regardless of b. (Formally Coerce does not make the model stronger, as an adversary can run all algorithms on his own. However, the finer model is useful in hybrid arguments and for composition with a PRF in §4.)

Definition 3 (m-IND-UF-1CMA). Let MMac1 (A[ m , q v , q i ]
) be the advantage of an adversary A that creates q i instances and makes q v Verify queries overall on messages of length at most m in the game:

Game MMac1 b (MAC) log ← ∅; k ← ∅; H ← ∅ k 0 $ ← MAC.keygen 0 () return {MAC, Verify, Coerce, Keygen} Oracle Mac(n, m) if k[n] = ⊥ return ⊥ if log[n] = ⊥ return ⊥ t ← MAC.mac(k[n], m) if b ∧ n ∈ H t $ ← byte MAC. t log[n] ← (m, t) return t Oracle Keygen(n) if k[n] = ⊥ return ⊥ k[n] ← MAC.keygen(k 0 ) H ← H ∪ n Oracle Coerce(n, k) if k[n] = ⊥ return ⊥ k[n] ← k Oracle Verify(n, m, t) if k[n] = ⊥ return ⊥ v ← MAC.verify(k[n], m, t) if b ∧ n ∈ H v ← log[n] = (m, t) return v
We confirm that Mac1 is a special case of MMac1 security and that, even with a static key, it suffices to consider a single verification query. (The proofs are in the appendix.)

Lemma 1 (MMac1 reduces to Mac1). Given A against MMac1 b , when k 0 = 0, we construct B against Mac1 b (linearly in q i ) such that:

MMac1 (A[ m , q v , q i ]) ≤ q i Mac1 (B[ m , q v ]).
Lemma 2. Given A against MMac1 b we construct B such that:

MMac1 (A[ m , q v , q i ]) ≤ q v MMac1 (B[ m , 1, q i ]).
Verified Implementation m-IND-UF-1CMA security reflects the type-based security specification of our idealized module MMac1 b , which has an interface of the form val log: memory → key → Spec (option (message × tag)) val mac: k:key → m:message → ST (t:tag) (requires log k = None) (ensures log k = Some(m,t)) val verify: k:key → m:message

→ t:tag → ST (v:bool) (ensures b ⇒ v = (log k = Some(m,t)))
The types of mac and verify express the gist of our security property: the specification function log gives access to the current content of the log associated with a one-time key; mac requires that the log be empty (None in F ) thereby enforcing our one-time MAC discipline; verify ensures that, when b is set, verification succeeds if and only if mac logged exactly the same message and tag. Their implementation is automatically verified by typing MMac1 b . However, recall that typing says nothing about the security loss incurred by switching b-this is the subject of the next subsection.

Our verified implementation of MMac1 b supports the two constructions described next, including code and functional correctness proofs for their algorithms. It also provides a more efficient interface for computing MACs incrementally. Instead of actually concatenating all authenticated materials in a message, the user creates a stateful hash, then repeatedly appends 16-byte words to the hash, and finally calls mac or verify on this hash, with a type that binds the message to the final hash contents in their security specifications. Our code further relies on indexed abstract types to separate keys and hashes for different instances of the functionality, and to support static key compromise.

Wegman-Carter-Shoup (WCS) Constructions

Next, we set up notations so that our presentation applies to multiple constructions, including GHASH and Poly1305; we factor out the encodings to have a core security assumption on sequences of field elements; we verify their injectivity; we finally prove concrete bounds in general, and in particular for GHASH and Poly1305.

From bytes to polynomials and back In addition to fixed lengths for keys and tags, the construction is parameterized by

• a field F;
• an encoding function • from messages to polynomials in F, represented as sequences of coefficients m ∈ F * .

• a truncation function from e ∈ F to tag(e) ∈ byte t ;

The key consists of two parts: an element r ∈ F and a one-time pad s ∈ byte t . We assume that r and s are sampled uniformly at random, from some R ⊆ F and from byte t , respectively. We write r s ← k for the parsing of key materials into r and s, including the encoding of r into R.

Generic Construction

Given a message m encoded into the sequence of

d coefficients m 0 , . . . , m d-1 of a polynomial m(x) = i=1..d m d-i x i in F, the tag is computed as: hash r (m) ← tag(m(r)) in F before truncation mac(r s, m) ← hash r (m) s in byte t
where the blinding operation is related to addition in F (see specific details below). We refer to hash r (m), the part of the construction before blinding, as the hash.

Next, we describe the two instantiations employed in TLS.

GHASH [START_REF] Dworkin | Recommendation for block cipher modes of operation: Galois/Counter mode (GCM) and GMAC[END_REF] uses the Galois field GF (2 128 ), defined as the extension GF (2)[x]/x 128 + x 7 + x 2 + x + 1, that is, the field of polynomials with Boolean coefficients modulo the irreducible polynomial x 128 + x 7 + x 2 + x + 1. Such polynomials are represented as 128-bit vectors. Conveniently, polynomial addition, the blinding operation , and its inverse simply correspond to 128-bit XOR. Polynomial multiplication is also efficiently supported on modern processors. The message encoding • splits the input message into 16-byte words, seen as integers in 0..2 128 -1; and the tag truncation is the identity. For AES-GCM, GHASH has a keygen0 function that samples a single r

$ ← GF (2 128
) shared across all MAC instances.

Poly1305 [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF] uses the field GF (p) for p = 2 130 -5, that is, the prime field of integer addition and multiplication modulo p, whose elements can all be represented as 130-bits integers. Its message encoding • similarly splits the input message into 16-byte words, seen as integers in 0..2 128 -1, then adds 2 to each of these integers, where is the word length in bits. (Hence, the encoding precisely keeps track of the length of the last word; this feature is unused for AEAD, which applies its own padding to ensure = 128.) The truncation function is tag(e) = e mod 2 128 . The blinding operation and its inverse are addition and subtraction modulo 2 128 . For ChaCha20-Poly1305, both r and s are single-use ( k 0 = 0) but our proof also applies to the original Poly1305-AES construction [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF] where r is shared.

Injectivity Properties

We intend to authenticate messages, not just polynomial coefficients. To this end, we instantiate our wellformed predicate on messages and show (in F ) that ∀ (m0: bytes) (m1: bytes).

( wellformed m0 ∧ wellformed m1 ∧ Poly.equals m0 m1 ) ⇒ m0 = m1

where Poly.equals specifies the equality of two formal polynomials by comparing their sequences of coefficients, extending the shorter sequence with zero coefficients if necessary. This enables the (conditional) composition of MACs with suitable well-formedness predicates for AEAD in TLS. This is required for GHASH as it is otherwise subject to 0-message truncations. We verify that the property above suffices to prove that both encodings are secure, and also that it holds in particular once we define wellformed as the range of formatted messages for AEAD (which are 16-byte aligned and embed their own lengths; see §5). We also confirm by typing that, with Poly1305, there is no need to restrict messages: its encoding is injective for all bytestrings [9, Theorem 3.2].

Security We give a theorem similar to those in prior work [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF][START_REF] Krawczyk | LFSR-based hashing and authentication[END_REF]46] but parameterized by the underlying field F, encoding • , truncation tag, and blinding operation . The theorem covers all uses of AES-GCM and ChaCha20-Poly1305 in TLS.

Consider the MMac1 definition, covering both shared and fresh values for r. Let q v be the number of oracle calls to Verify (for which log[n] = (m , t )) and d a bound on the size (expressed in number of field elements) of the messages in calls to Mac and Verify.

Theorem 1. The Wegman-Carter-Shoup construction for messages in

F d-1 is m-IND-UF-1CMA secure with concrete bound MMac1 (A[ m , q v , q i ]) = d.τ.qv
|R| with d = m /16, and τ = 1 for GHASH and τ = 8 for Poly1305.

The proof (in the appendix) uses Lemma 2 and establishes a bound d•τ

|R| for an adversary that makes a single Verify query. This bound follows from an d•τ

|R| -almost--universal property, which has been separately proved for GHASH [START_REF] Mcgrew | Flexible and efficient message authentication in hardware and software[END_REF] and Poly1305 [START_REF] Bernstein | The Poly1305-AES message-authentication code[END_REF]; the appendixalso includes its proof for all instantiations of hash r for TLS.

Concrete bounds for GHASH The range size for r is 2 128 and there is no tag truncation, hence by Lemma 2 we get a straight = d•qv 2 128 , so for TLS the main risk is a failure of our PRF assumption on AES, discussed in §7.

Concrete bound for Poly1305

The effective range R of r is reduced, first by uniformly sampling in 0..2 128 -1, then by clamping 22 bits, to uniformly sampling one element out of | R |= 2 106 potential values. We lose another 3 bits of security from the truncation of F to byte t and by applying Lemma 2 we arrive at

= d•qv 2 103 .
4 Pseudo-Random Functions for AEAD

We now consider the use of symmetric ciphers in counter mode, both for keying one-time MACs and for generating one-time pads for encryption. We model ciphers as PRFs. For TLS, we will use AES or ChaCha20, and discuss PRF/PRP issues in §7. A pseudo-random function family PRF implements the following interface:

type key val keygen: unit → ST key This interface specifies an abstract type for keys and a key-generation algorithm. (Type abstraction ensures that these keys are used only for PRF computations.) It also specifies concrete, fixed-length bytestrings for the domain and range of the PRF, and a function to compute the PRF. We refer to the PRF outputs as blocks. As usual, we define security as indistinguishability from a uniformly random function with lazy sampling.

Definition 4 (PRF security). Let Prf (A[q b ]) be the advantage of an adversary A that makes q b Eval queries in the game:

Game Prf b (PRF) T ← ∅ k $ ← PRF.keygen() return {Eval} Oracle Eval(m) if T [m] = ⊥ if b then T [m] $ ← byte b else T [m] ← PRF.eval(k, m) return T [m]
The AEAD constructions we consider use PRFs both to generate keys for the one-time MAC used to authenticate the ciphertext and to generate a one-time pad for encryption and decryption. Accordingly, we partition the domain and use a specialized security definition, with a separate eval function for each usage of the PRF. (This will enable us to give more precise types to each of these functions.)

We assume the PRF domain consists of concatenations of a fixed-sized counter j and a nonce n, written j n. This notation hides minor differences between AEAD algorithm specifications, e.g. AES-GCM uses n j instead j n. Our implementation handles these details, and verifies that j n is injective for all admissible values of j and n.

For key generation, AES-GCM uses the PRF to derive both a static MAC key k 0 generated from the PRF (with nonce and counter 0) and a 1-time MAC key for each nonce (with counter 1) whereas Poly1305 uses a pure 1-time MAC key for each nonce (with counter 0). To handle both cases uniformly, we introduce a parameter j 0 ∈ {0, 1} to shift the counter before concatenation with the nonce. In the following, we assume a compatible MAC, meaning that either

j 0 = 0 ∧ k 0 = 0 ∧ k ≤ b or j 0 = 1 ∧ k 0 ≤ b ∧ k -k 0 ≤ b .
For pad generation, counter mode encrypts plaintext blocks as p ⊕ eval(j n) and decrypts by applying the same pad to the ciphertext. In the PrfCtr game below, we separate encryption and decryption, and we fuse the block generation and the XOR, so that we can give separate types to plaintexts and ciphertexts. (We truncate the block in case it is smaller than the input, as required for the last block in counter-mode.) Definition 5 (PrfCtr security). Given PRF and MAC, let PrfCtr (A[q b , q g ]) be the advantage of an adversary A that makes q b queries to either EvalEnx or EvalDex and q g queries to EvalKey in the following game:

Game PrfCtr b (PRF, MAC) T ← ∅; R ← ∅ k $ ← PRF.keygen() k 0 $ ← MAC.keygen0() if j 0 ∧ ¬b o ← PRF.eval(k, 0 b ) k 0 ← truncate(o, MAC. k0 ) return {EvalKey, EvalEnx, EvalDex} Oracle EvalKey(j n) if j = j 0 return ⊥ if T [j n] = ⊥ if b k m $ ← MAC.keygen(k 0 ) else o ← PRF.eval(k, j n) k m ← truncate(k 0 o, k ) T [j n] ← k m return T [j n] Oracle EvalEnx(j n, p) if j ≤ j 0 return ⊥ o $ ← Eval(j n) c ← p ⊕ truncate(o, |p|) return c Oracle EvalDex(j n, c) if j ≤ j 0 return ⊥ o $ ← Eval(j n) p ← c ⊕ truncate(o, |c|) return p
Lemma 3 (PrfCtr b reduces to Prf b ). Given PRF, MAC, and A against PrfCtr b (PRF, MAC), we construct B against Prf b (PRF) such that:

PrfCtr (A[q b , q g ]) = Prf (B[q b + q g + j 0 ]).
The proof is in the appendix. Intuitively, we have a perfect reduction because, in all cases, the specialized game still samples a single fresh block for each j n for a single purpose, and returns a value computed from that block.

In the next section, once b holds and the MAC has been idealized, we will use two oracles that further idealize encryption and decryption:

Oracle EvalEnx (j n, p) if j ≤ j 0 return ⊥ if T [j n] = ⊥ return ⊥ if b c $ ← byte |p| else c $ ← EvalEnx(j n, p) T [j n] ← (p, c) return c
Oracle EvalDex (j n, c) if j ≤ j 0 return ⊥ if T [j n] = (p, c) for some p return p else return ⊥ When b holds, encryption samples c instead of o = p ⊕ c, and records the pair (p, c) instead of just p ⊕ c; and decryption simply performs a table lookup. This step is valid provided the block at j n is used for encrypting a single p and decrypting the resulting c. The oracles enforce this restriction dynamically (on their second lines) whereas our code enforces it statically, using type-based preconditions on EvalEnx or EvalDex implied by the AEAD invariant of §5. Verified Implementation Lemma 3 and the subsequent step are not currently verified by typing. (Still, note that the sampling of c instead of o is justified by F 's probabilistic semantic and could be verified using the relational typing rule for sample in RF [START_REF] Barthe | Probabilistic relational verification for cryptographic implementations[END_REF])

We use an idealized PRF module with two idealization flags (for b and for b ) that directly corresponds to the specialized game PrfCtr b,b parametrized by a Cipher module that implements real AES128, AES256, and ChaCha20 (depending on an algorithmic parameter alg) and by a MAC module. The separation of the PRF domain is enforced by typing: depending on alg, j 0 , j, b, and b , its range includes keys, blocks, and pairs (p, c).

From MAC and PRF to AEAD

We implement the two main AEAD constructions used by TLS 1.3 and modern ciphersuites of TLS 1.2. We show that their composition of a PRF and a one-time MAC yields a standard notion of AEAD security. Our proof is generic and carefully designed to be modular and TLS-agnostic: we share our AEAD code between TLS 1.2 and 1.3, and plan to generalize it for other protocols such as QUIC.

AEAD functionality Our authenticated encryption with associated data (AEAD) has a real interface of the form with two functions to encrypt and decrypt messages with associated data of variable lengths, and types that specify the cipher length as a function of the plain length. (We omit declarations for keys, similar to those for PRFs in §4.)

Definition 6 (Aead security). Let Aead (A[q e , q d , p , a ]) be the advantage of an adversary that makes at most q e Encrypt and q d Decrypt queries on messages and associated data of lengths at most p and a in the game:

Game Aead b (AEAD) C ← ∅ k $ ← AEAD.keygen() return {Encrypt, Decrypt} Oracle Encrypt(n, a, p) if C[n] = ⊥ return ⊥ if b c $ ← byte cipherlen(|p|) else c ← AEAD.encrypt(k, n, a, p) C[n] ← (a, p, c) return c Oracle Decrypt(n, a, c) if b if C[n] = (a, p, c) for some p return p return ⊥ else p ← AEAD.decrypt(k, n, a, c) return p
Our definition generalizes AE in §2; it has a richer domain with plaintext and associated data of variable lengths; a function cipherlen from plaintext lengths to ciphertext lengths; and nonces n. It similarly maintains a log of encryptions, indexed by nonces. Crucially, Encrypt uses the log to ensure that each nonce is used at most once for encryption.

Generic AEAD Construction Given a PRF and a compatible MAC, AEAD splits plaintexts into blocks which are then blinded by pseudo-random one-time pads generated by calling PRF on increasing counter values, as shown in §4. (Blocks for MAC keys and the last mask may require truncation.)

To authenticate the ciphertext and associated data, the construction formats them into a single 16-bytealigned buffer (ready to be hashed as polynomial coefficients as described in §3) using an encoding function declared as val encode: bbytes p × bbytes a → Tot bbytes ( p + a + 46) and implemented (in pseudo-code) as where the auxiliary function split (b) splits the bytestring b into a sequence of r non-empty bytestrings, all of size , except for the last one which may be shorter.

(that is, if r, b 1 , . . . b r ← split b ( ), then b = b 1 • • • b r .);
where zeros( ) is the bytestring of zero bytes; and where length 8 (n) is the 8-byte representation of the length of n. Thus, our encoding adds minimal zero-padding to a and c, so that they are both 16-bytes aligned, and appends a final 16-byte encoding of their lengths.

Recall that the domain of MAC messages is restricted by the wellformed predicate. We now define wellformed b = ∃ (c:cipher) (a:ad). b = encode c a and typecheck the property listed in §3 that ensures injectivity of the polynomial encoding.

The rest of the AEAD construction is defined below, using an operator otp ⊕ p that abbreviates the expression truncate(otp, |p|) ⊕ p, and a function untag 16 that separates the ciphertext from the tag.

Function keygen() k $ ← PRF.keygen(); k 0 ← ε if j 0 o ← PRF.eval(k, 0 b ) k 0 ← truncate(o, MAC. k0 ) return k 0 k Function encrypt(K, n, a, p) (k 0 , k) ← split k 0 (K); c ← ε k 1 ← PRF.eval(k, j 0 n) k m ← truncate(k 0 k 1 , MAC. k ) r, p 1 , . . . , p r ← split b (p); for j = 1..r otp ← PRF.eval(k, j 0 + j n) c ← c (otp ⊕ p j ) t ← MAC.mac(k m , encode(c, a)) return c t Function decrypt(K, n, a, c) (k 0 , k) ← split k 0 (K); p ← ε k 1 ← PRF.eval(k, j 0 n) k m ← truncate(k 0 k 1 , MAC. k ) (c, t) ← untag 16 (c) m ← encode(c, a) if ¬MAC.verify(k m , m, t) return ⊥ r, c 1 , . . . , c r ← split b (c); for j = 1..r otp ← PRF.eval(k, j 0 + j n) p ← p (otp ⊕ c j ) return p
The main result of this section is that it is Aead-secure when PRF is Prf-secure and MAC is MMac1secure:

Theorem 2 (AEAD construction). Given A against Aead, we construct B against Prf and C against MMac1, with:

Aead(AEAD) (A[q e , q d , p , a ]) ≤ Prf(PRF) (B[q b ]) + MMac1(MAC) (C[ p + a + 46, q d , q e + q d ])
where q b (the number of distinct queries to the PRF) satisfies:

q b ≤ j 0 + q e 1 + p b + q d
Proof sketch. The proof is in the appendix; it relies on the PrfCtr b,b and MMac1 b idealizations; it involves a sequence of transformations from Aead 0 to Aead 1 that inline successively more idealizations. Therefore, we introduce a parametric game AeadCtr(X) for any game X that returns EvalKey, EvalEnx, EvalDex, Mac, and Verify oracles:

Game AeadCtr(X) (EvalKey, EvalEnx, EvalDex, Mac, Verify) ← X() return {Encrypt, Decrypt} Oracle Encrypt(n, a, p) if C[n] = ⊥ return ⊥ EvalKey(n); c ← ε r, p 1 , . . . , p r ← split b (p) for j = 1..r c ← c EvalEnx(j 0 + j n, p j ) c ← c Mac(n, encode(c, a)) C[n] ← (a, p, c) return c Oracle Decrypt(n, a, c) c, t ← untag 16 (c) EvalKey(n) if ¬Verify(n, encode(c, a), t) return ⊥ r, c 1 , . . . , c r ← split b (c); p ← ε for j = 1 . . . r p ← p EvalDex(j 0 + j n, c j ) return p
When X is obtained from PrfCtr 0 and MMac1 0 we have a game that is equivalent to Aead 0 . We first switch to PrfCtr 1 to get random MAC keys and then idealize MMac1 1 . When X is obtained from PrfCtr 1 and MMac1 1 ciphertexts are authenticated and we can switch to PrfCtr 1,0 and then to PrfCtr 1,1 . At this stage the PRF table contains randomly sampled ciphertext blocks and decryption corresponds to table lookup in this table. This is ensured on the code by our AEAD invariant.

Verified Implementation We outline below the idealized interface of our main AEAD b module built on top of (the idealized interfaces of) PrfCtr b,b and MMac1 b , both taken as cryptographic assumption, and documented by the games with the same names on paper. We focus on types for encryption and decryption: As in §2, we have a multi-instance idealization, with a log for each instance stored within an abstract, stateful key; and we provide a proof-only function log to access its current contents in logical specifications. Hence, key generation allocates an empty log for the instance; encryption requires that the nonce be fresh and records its results; and decryption behaves exactly as a table lookup, returning a plaintext if, and only if, it was previously stored in the log by calling encryption with the same nonce and additional data.

This step of the construction is entirely verifiable by typing. To this end, we supplement its implementation with a precise invariant that relates the AEAD log to the underlying PRF table and MAC logs. For each entry in the log, we specify the corresponding entries in the PRF table (one for the one-time MAC key, and one for each block required for encryption) and, for each one-time MAC key entry, the contents of the MAC log (an encoded message and the tag at the end of the ciphertext in the AEAD log entry). By typing the AEAD code that implements the construction, we verify that the invariant is preserved as it completes its series of calls to the PRF and MAC idealized interfaces. Hence, although our code for decryption does not actually decrypt by a log lookup, we prove that (when b holds) its results always matches the result of a lookup on the current log. As usual, by setting all idealization flags to false, the verified code yields our concrete TLS implementation.

Security bounds Theorem 2 can be specialized to provide precise security bounds for the various AEAD ciphersuites:

Construction Aead (A[q e , q d , p , a ]) ≤ AES128- GCM, AES256- GCM Prf B q e 1 + p 16 + q d + 1 + q d 2 128 • p+ a+46 16 ChaCha20- Poly1305 Prf B q e 1 + p 64 + q d + q d 2 103 • p+ a+46 16
In this paper, we only consider MAC schemes that provide information theoretic security although we do not rely on this fact in the proof of AEAD.

6 From AEAD to Stream Encryption (StAE)

TLS requires stream encryption: message fragments must be received and processed in the order they were sent, thereby defeating attempts to delete or re-order network traffic. To this end, encryption and decryption use a local sequence number to generate distinct, ordered nonces for AEAD.

In practice, it is difficult to prevent multiple honest servers from decrypting and processing the same 0-RTT encrypted stream. Since decryption is now stateful, we must generalize our model to support multiple parallel decryptors for each encryptor. In our security definitions, we thus add a genD oracle to generate new decryptors (with local sequence numbers set to zero) from a given encryptor.

Otherwise, the stateful construction is quite simple: TLS 1.3 combines the sequence number with a static, random 'initialization vector' (IV) in the key materials to generate pairwise-distinct nonces for encrypting fragments using AEAD. In contrast, TLS 1.2 nonces concatenate the static IV with a perfragment explicit IV that is sent alongside the ciphertext on the network (except for ciphersuites based on ChaCha20-Poly1305 which follow the TLS 1.3 nonce format). Some TLS 1.2 implementations incorrectly use uniformly random explicit IVs [START_REF] Böck | Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS[END_REF]. This is much inferior to using the sequence number because of the high collision risk on 64 bits. Therefore, in our implementation, we use the following nonce construction: n = bigEndian 8 (seqn) iv 4 for AES-GCM in TLS 1.2 bigEndian 12 (seqn) ⊕ iv 12 otherwise where the indices indicate lengths in bytes. We discuss at the end of the section the impact of random explicit IVs in TLS 1.2 on the concrete security bound. The use of longer static IVs in TLS 1.3 is a practical improvement, as (informally) it acts as an auxiliary secret input to the PRF and may improve multi-user security [START_REF] Bellare | The multi-user security of authenticated encryption: AES-GCM in TLS 1.3[END_REF]. This is particularly clear for ChaCha20, where the key, nonce, and counter are just copied side by side to the initial cipher state. We easily verify (by typing) that both constructions are injective for 0 ≤ seqn < 2 64 , which is required (also by typing) to meet the 'fresh nonce' pre-condition for calling AEAD encryption. Formally, the state invariant for StAE encryption is that 0 ≤ seqn < 2 64 and the underlying AEAD log has an entry for every nonce n computed from a sequence number smaller than seqn. StAE functionality A stream authenticated encryption functionality StAE implements the following interface: We omit type declarations for plain, cipher and ad as they are similar to AEAD. For TLS, the length of additional data a can be 0 (TLS 1.3) or 13 (TLS 1.2) and the length of IVs iv is 12. Compared to previous functionalities, the main change is that keys are replaced by states that embed a 64-bit sequence number. Accordingly, in this section we assume that at most 2 64 fragments are encrypted. The stateful function gen initializes the encryptor state used by the encryption algorithm, while genD initializes a decryptor state used by the decryption algorithm. The stateful encrypt and decrypt functions require that the sequence number in the key state does not overflow (seqn s < q e ) and ensure that it is incremented (only on success in the case of decryption). In pseudo-code, authenticated stream encryption is constructed as follows: We are now ready to use stream encryption for protecting TLS 1.3 traffic, which consists of a sequence of protocol-message fragments, each tagged with their content type, while hiding their content, their type, and their actual size before padding. The steps taken by the record layer to construct encrypted fragments are depicted in Figure 3, with apparent size after padding. The last line adds the (unprotected) record header; for backward compatibility, it pretends to be a TLS 1.0 AppData record irrespective of its actual encrypted content type. On the other hand, TLS does not attempt to hide the record boundaries (as e.g. SSH) so we do not expect indistinguishability from random for the resulting record.

Function gen() k $ ← AEAD.keygen() iv $ ← byte iv return {k ← k; iv ← iv; seqn ← 0}
Formatting: Content Type and Length Hiding Encryption and decryption rely on formatting and padding functions over a type fragment indexed by a length indicating the public maximal length of its content, specified as follows:

type len = n:nat {n ≤ 2 14 } ( * valid record length in TLS * ) type fragment ( :len) = {ct:byte; data:bbytes } val parse: :len → lbytes ( +1) → Tot (option (fragment )) val format: :len → f:fragment → Tot (p:lbytes ( +1)) (ensures parse p = Some f)

These functions must be carefully implemented to prevent any side channel. We also construct and parse records into headers and payloads using functions These function specifications suffice to establish our theorems below. We now give the concrete format function for TLS 1.3:

Function format( : len, f : fragment ) f.data [f.ct] pad 0 ( -|f.data|)
where pad 0 n is the string of n 0x00 bytes. We verify the post-condition of format by typing. We omit the corresponding parse function and the code for processing headers. The implementation of parse and format, and the converse function for parsing a bytestring into a fragment value, require precautions to avoid leaking the actual contents length using side-channels. The code for processing headers does not depend on the fragment, only on its length after padding.

The game logs the encryption stream in F , indexed by fragment sequence numbers and ciphertexts. It has an oracle for creating decryptors; it stores their state in a table D, indexed by some abstract d chosen by the adversary. It does not model stream termination, enforced purely by typing the stream content.

Theorem 4 (Lhse perfectly reduces to Stae). Given A against Stae, we construct B against Aead with

Lhse (A[q e , q d ]) = Stae (B[q e , q d , 2 14 + 1, a ])
where a is 0 for TLS 1.3 and 13 for TLS 1.2.

Proof. We build B by composing A with a variant of the construction given above that calls Stae oracles instead of its functions. The 1.3 record does not use authenticated data, a = 0, (while in TLS 1.2 it was a = 13). The maximum fragment size is p = 2 14 + 1. We encrypt one additional byte for the content type.

Multi-Stream LHSE In the next section (as in our interface above), we use a multi-instance Lhse game, defined below.

Game Multi(Lhse b ) E ← ∅; return {Gen, GenD, Encrypt, Decrypt} Oracle Gen(i) if (E[i] = ⊥) E[i] $ ← Lhse b () Oracle GenD(i, d) if (E[i] = ⊥) E[i] $ ← Lhse b () E[i].GenD(d) Oracle Encrypt(i, , f ) if (E[i] = ⊥) return ⊥ return E[i].Encrypt( , f ) Oracle Decrypt(i, d, v) if (E[i] = ⊥) return ⊥ return E[i].Decrypt(d, v)
For every fresh index i passed to Gen, we spawn an instance of Lhse and we record its state and oracle in table E. In all other cases, the oracles above now look up the shared instance at i and forward the call to the instance oracle.

Security bounds for TLS Table 1 gives the concrete bounds by ciphersuites, setting p to 2 14 + 1 and a to 0 (or 13 for TLS 1.2). ChaCha20 uses a Davies-Meyer construction and is considered a good PRF. For AES-GCM ciphersuites, blocks are relatively small (16 bytes) so we incur a loss of q 2 b 2 129 by the PRP/PRF switching lemma [START_REF]Code-based game-playing proofs and the security of triple encryption[END_REF], intuitively accounting for the probability of observing collisions on ciphertext blocks and inferring the corresponding plaintext blocks are different. As observed e.g. by Luykx and Paterson [START_REF] Luykx | Limits on authenticated encryption use in TLS[END_REF], this factor limits the amount of data that can be sent securely using AES-GCM.

Based on their suggestion to send at most 2 24.5 fragments with the same key (itself based on a proof by [START_REF]Stronger security bounds for Wegman-Carter-Shoup authenticators[END_REF] for the UF-1CMA security of GHASH that avoids the full PRF-PRP switching loss), our implementation may automatically trigger TLS re-keying after sending 2 24.5 fragments. This strategy results in the bound in the last row, which no longer depends quadratically on q e and thus achieves a poor man's form of beyond birthday bound security.

The Luykx and Paterson bound shows that when q e ≤ 2 50 and q d ≤ 2 60 then the success probability of any attacker breaking the integrity of AES-GCM is bounded by 2 -56 . Conditioned on all decryption queries having failed, they can then assume q d = 0 when considering the bound for confidentiality.

Ciphersuite

Lhse (A[q e , q d ]) ≤ General bound Prf (B[q e (1 + (2 14 + 1)/ b ) + q d + j 0 ]) + MMac1 (C[2 14 + 1 + 46, q d , q e + q d ])

ChaCha20-Poly1305

Prf (B q e 1 + (2 14 +1) 64

+ q d ) + q d 2 93 AES128- GCM AES256- GCM Prp (B[q b ]) + q 2 b 2 129 + q d 2 118
where q b = q e (1+ (2 14 +1)/16 )+q d +1 AES128-GCM AES128-GCM qe 2 24.5 Prp (B 2 34.5 )

+ 1 2 60 + 1 2 56
with re-keying every 2 24.5 records (counting q e for all streams, and q d ≤ 2 60 per stream)

Table 1: Summary of security bounds for the TLS AEAD ciphersuites.

To tolerate an attacker success probability of at most , they compute the maximum number of encrypted fragments q e such that q e ≤ √ 2 129 -1 (1+(2 14 +1)/16) . For instance as long as at most 2 24.5 records are encrypted they bound the success probability by = 2 -60 .

Let us now consider the bound for simultaneously achieving confidentiality and integrity. By solving

for q e we have:

q e ≤ √ 2 129 -2 11 q d -q d -1 1+ 2 14 +1 /16
. For q d = 2 34 we have q e ≤ 2 22.72 , while for q d = 2 35 we no longer get a meaningful security bound. For q d = 2 32 one can send a more satisfying q e ≤ 2 24.21 records. If as in 1-RTT only a single failed decryption query is accepted, then q d = 1 and we get q e = 2 24.49 , essentially the same bound as Luykx and Paterson [START_REF] Luykx | Limits on authenticated encryption use in TLS[END_REF].

Exhaustive key search To better understand the terms Prp and Prf above, let us recall an exhaustive, ideal-cipher attack. Assume the adversary can search for q K keys (each time encrypting a known plaintext block and comparing it with an oracle encryption of that block). The attack succeeds with probability q K 2 K . With AES128 exhaustive key search is the best attack when this term dominates the quadratic term (q K ≥ 2q 2 b ), and the third term (q K ≥ 2 11 q d ).

8 The TLS 1.3 Record Protocol Figure 4 presents the TLS 1.3 protocol from draft-19, focusing only on how it drives the record layer. In particular, this presentation ignores most of the details of the handshake. Figure 1 in Section 1 illustrates the sub-protocol streams from the point of view of the client. The client sends the ClientHello message in cleartext, and may then immediately install a fresh 0-RTT key k c 0 in the record layer and use it to encrypt a stream of early data. The server receives this message and, if it accepts 0-RTT, also installs the 0-RTT key k c 0 and decrypts the client's data. Otherwise, it discards this first stream. In parallel, the server sends a ServerHello message that allows both parties to derive encryption keys k c h and k s h for the handshake messages, and k c 1 and k s 1 for application data. The server installs k s h in the record and uses it to encrypt a first stream of handshake messages, ending with a finished message that triggers the installation of key k s 1 . If the server supports 0.5-RTT, it may immediately start using k s 1 for sending application data. Once 0-RTT stream is complete (signaled by an end-of-early-data message) and after processing the ServerHello, the client installs the handshake keys k c h and k s h for encryption and decryption. It completes the handshake by sending its own encrypted stream, ending with a finished message, and installs the application traffic keys k c 1 and k s 1 . Upon completing the handshake, the server also installs k c 1 for decryption. After this point, the connection is fully established and both parties use the installed application traffic keys for all content types: AppData, Alert, and even Handshake messages (such as KeyUpdate).

Later, the client (or the server) can terminate their current output stream by sending either a KeyUpdate handshake message or a close-notify alert message. In the first case, it installs and starts using the next application traffic key k c 2 (then k c 3 , etc.). The server (or the client) responds accordingly, with a KeyUpdate or a close-notify. In the first case, it installs and starts using the next traffic keys k c 2 and k s 2 . In the second case, the connection is closed.

In all cases, each party uses a single stream at a time in each direction, for sending and receiving all content types, and each stream ends with a distinguished message that clearly indicates its final fragment. 0-RTT data ends with an end-of-early-data message; encrypted handshake messages in both directions end with the finished message; 0.5 and 1-RTT data streams end with a key update or a close-notify alert. This precaution ensures that any truncations at the end of a stream will cause a connection failure, rather than continuing with the next stream.

Performance/Security Trade-Offs. 0-RTT and 0.5-RTT significantly decrease communications latency, but they yield weaker application security. 0-RTT traffic has weaker forward secrecy and is subject to replays: if multiple servers may accept the connection and (as usual) do not share an anti-replay cache, then they may all receive and process (prefixes of) the same early traffic data. This motivates our model with multiple decryptors, and also requires the server application to defer some effects of early-data processing till handshake completion. Also, since data is sent before ciphersuite negotiation, the client may use relatively weak algorithms (or broken implementations) that the server would otherwise have a chance to refuse. 0.5-RTT incurs similar, lesser risks as the server sends data before the handshake completes. The server is subject to 0-RTT truncation attacks if it starts sending data before receiving the client's end of early data. Also, if the server relies on a client signature, it should not send sensitive data before handshake completion. In contrast with 0-RTT, sending 0.5-RTT traffic is a local configuration issue for the server; the client receives 0.5-RTT data after completing the handshake and does not distinguish it from 1-RTT data.

TLS 1.2 is routinely deployed with 'FalseStart', which is similar to 0.5-RTT but in the other direction, the client may locally decide to start sending encrypted application data as soon as it can compute the keys, before handshake completion. This places additional trust in the client's ciphersuite whitelist, inasmuch as sensitive data may be sent before confirming their correct negotiation with the server.

A Minimal Record Game Next, we present a simplified, more liberal model of the Record that seeks to abstract away from the details of how the connection evolves. This facilitates the statement of a standalone 'record-layer' theorem, but our approach similarly applies to our full F implementation integrated with miTLS, which carefully keeps track of the sequence of keys, as outlined at the end of this section.

We abstract the state of the connection by a context bitstring; as the handshake progresses, we concatenate more relevant handshake parameters to the context. For instance, after ClientHello, the context consists of the client's nonce n C and its proposed ciphersuites and key exchange values; after ServerHello, it additionally contains the server nonce n S , algorithm choice, key exchange value, etc.

Instead of modeling duplex channels between clients and servers, we consider separate sequences of streams in each direction. Our game (Figure 6) models re-keying and context extension for a sequence of streams (all in the same direction), covering 0-RTT, 0.5-RTT, and 1-RTT traffic, relying on the multiinstance game SE = Multi(Lhse) (see §7).

The game has oracles Init and InitD for generating multi-stream encryptors and decryptors in their initial state, indexed by n and m, respectively. We assume that their arguments determine the record algorithm. Their state consist of a current context, a current stream number j, and a local map I from stream numbers to the value of the context when they were installed. We use variables ctx, j, and I to refer to the fields of E[m] and D[n], respectively.

Oracles Extend and ExtendD allow the local context to be extended (concatenated) with new information at any time.

Oracles Install and InstallD install an LHSE instance (allocating it if it does not exist) for encryption and decryption, respectively. Recall that calls to SE.Gen are memoized, so that an encryptor and a decryptor share the same stream if and only if they agree on the stream sequence number and context.

Oracles Encrypt and Decrypt apply encryption and decryption to the currently-installed stream. Some fragments are final: they terminate the stream and signal the need to install a new stream before continuing. Definition 9 (Record). Let Record (A[q e , q d , q i ]) be the advantage of an adversary A that makes at most q e encryption queries and q d decryption queries for each of the q i LHSE instances created using install queries in the game of Figure 6.

Theorem 5 (Record reduces to Lhse).

Record (A[q e , q d , q i ]) ≤ q i Lhse (B[q e , q d ]).

Our game complies with the idealized interface for LHSE and relies on its conditional idealization. If b = 0, then the oracles operate purely on local state, and simply implement a real sequence of encrypted streams, under the control of the record state machine. If b = 1, then we get perfect authentication of (a prefix of) the whole sequence of streams of fragments. (This property is verified by typing our idealized record implementation.) The ctx field of encryptors and decryptor represents their implicitly authenticated shared context: unless there is an encryptor with a matching context, the ideal encryption log is empty hence decryption will fail. In particular, as soon as the context includes ServerCert-Finished, and thus the fresh TLS nonces n C and n S , we know that there is at most one encryptor and one decryptor.

More precisely, consider encryptor and decryptor states E

[n] and D[m]. If E[n].I[j] = D[m].I[j] then also E[n].I[j ] = D[m].I[j ]
for any j < j. Thus, for instance, when D[m] receives a final fragment, we know that E[n] and D[m] agree on the whole sequence of communicated fragment for the first j streams. By Theorem 5 these guarantees also hold for the real record for any game adversary A, except with probability Record (A). Application to 0-RTT We briefly show how to control our game to model 0-RTT and 0.5-RTT. For 0-RTT, the client is the encryptor and the server is the decryptor. Both use the encryptor index n as initial context, representing the content of ClientHello, notably the fresh client random n C . Conversely, the decryptor index m (including the fresh server random n S ) is not included in the initial context of InitD. As both parties install their first stream (j = 0) for 0-RTT, this reflects that the underlying TLS key derivation (k c 0 in Figure 4) depends only on client-side information. Thus, although 0-RTT traffic is protected, it may be decrypted by multiple server instances with different indexes m.

Calls to ExtendD and Extend reflect handshake communications in the other direction, as the ServerCert-Finished stream is sent and received, causing ctx to be extended with (at least) m. Afterwards, as the two parties successively install streams for the TLS keys k c h , k c 1 , k c 2 , . . . , successful decryption guarantees agreement on a context that includes the pair n, m. Thus, in this usage of our Record game at most one server will successfully decrypt the first encrypted handshake fragment from the client, and from this point all streams are one-to-one.

Application to 0.5-RTT The server is the encryptor, the client the decryptor and, since they both have initial access to the first message exchange, we may select as index n that includes the client hello and server hello messages and implicitly authenticate the pair n C , n S . Thus, there is at most one honest client decryptor for 0.5-RTT and, from the client's viewpoint, successful decryption of the first handshake fragment ensures agreement on this context. Still (at least from the record's viewpoint) the server is not guaranteed there is a matching decryptor until it receives ClientCert-Finished in the other direction and transitions to 1-RTT.

Verified Implementation for miTLS (Outline) Our TLS Record implementation supports sequences of streams for the full protocol described in Figure 4 and its TLS 1.2 counterpart.

Stream Sequences As described in the game above, it maintains a current stream for each direction, and it receives 'extend' and 'install' commands from the handshake protocol as the connection gets established. Its indexes (ctx in the game) consist of a summary of the handshake context available at the time of key derivation (always including the algorithms to use). In contrast with our game, which models all communications in a single direction, our code supports 'duplex' communications. This is necessary, for instance, for synchronizing key updates and connection closure between clients and servers. Our code also maintains a small (type-based) state machine that controls the availability of the current streams for sending application data.

Re-keying and Corruption The state machine enforces a limit on the maximum number of fragments that can be sent with one key to prevent sequence number overflows and account for the birthday bound weakness of AES-GCM. On key updates we delete old keys and model the corruption of individual streams using leak and coerce functions for keys. This is in keeping with the static corruption modeling of miTLS, e.g. to account for insecure handshake runs.

Fragment API Our code for the record is parameterized by a type of abstract application-data plaintexts, indexed by a unique stream identifier and an apparent fragment length. Type abstraction guarantees that, if the stream identifier is safe (a property that depends on the handshake and key derivation process), the idealized TLS implementation never actually accesses their actual length and contents, a strong and simple confidentiality property.

Our API has a configuration to control 0-RTT and 0.5-RTT as the connection is created. In particular, 0-RTT plaintexts have their own type, (indexed by an identifier that describe their 0-RTT context) which should help applications treat it securely. Conversely, 0.5-RTT is modeled simply by enabling earlier encryption of 1-RTT traffic.

Message API Our code also has a higher-level API with messages as (potentially large) bytestrings instead of individual fragments. As usual with TLS, message boundaries are application specific, whereas applications tend to ignore fragment boundaries. Nonetheless, our code preserves apparent message boundaries, never caches or fragments small messages, and supports message length-hiding by taking as inputs both the apparent (maximal) size max of the message and its private (actual) size m . It has a simple fragmentation loop, apparently sending up to 2 14 bytes at each iteration, starting with maxm bytes of padding follows by the actual data. (This ensures that an application that waits for the whole message never responds before receiving the last fragment.) We do not model de-fragmentation on the receiving end; our code delivers fragments as they arrive in a buffer provided by the application for reassembling its messages. The correctness and security of this construction on top of the fragment API is verified by typing, essentially abstracting sequences of fragments into sequences of bytes for the benefit of the application, and turning close-notify alert fragments into end-of-files. (See also [START_REF] Fischlin | Data is a stream: Security of stream-based channels[END_REF] for a cryptographic treatment of fragmentation issues.)

Experimental evaluation

We evaluate our reference implementation of the TLS record layer both qualitatively (going over the verified goals of the various modules and how they relate to the games presented in the paper, and checking that our implementation interoperates with other TLS libraries) and quantitatively (measuring the verification and runtime performance).

Verification evaluation Table 2 summarizes the modular structure of our code, and evaluates the verification costs and the extracted OCaml and C implementations. Since proofs and implementations are tightly interleaved in F source code, it is difficult to accurately measure a precise source overhead. The reported annotation percentages figure in the table are rough manual estimates, but they can be compared to the size of extracted implementations.

Most of the verification burden comes from the security proof of AEAD (totaling approximately 4,500 lines of annotation out of a total of about 5,500 lines of F ) and the functional correctness proof of the MAC implementations (totaling over 4,000 lines of annotations and lemmas). For the latter, we extended F with a new big number library to verify the low-level implementations of various mathematical operations (such as point multiplication on elliptic curves or multiplication over finite fields) using machine-sized integers and buffers. We use it to prove the correctness of the polynomial computations for Poly1305 and GHASH.

Current limitations Our record layer implementation is part of miTLS in F : a larger, partially verified codebase that intends to provide a secure, efficient implementation for both TLS 1.2 and TLS 1.3. We leave a complete verification of the TLS 1.3 handshake and its integration with our code as future work.

Our implementation also includes the first miTLS component implemented in a lower level fragment of F that enables its extraction to C code. In contrast, the rest of miTLS is still extracted to OCaml and, until it is similarly adapted, relies on an unverified OCaml/C wrapper to call our extracted C code. Currently, this runtime transition is done at the level of the AEAD interface, enabling us to switch to other generic cryptographic providers more easily (e.g. to compare performance with OpenSSL). Hence, the TLS-specific stateful encryption in StreamAE is verified on top of an idealized AEAD interface that slightly differs from the one exported by our idealized Crypto.AEAD construction. For instance, the former represents fragments as sequences of bytes, whereas the latter uses a lower level memory model and represents fragments as mutable I/O buffers, hence the transition requires copying fragments between representations.

Interoperability Our record implementation supports both TLS 1.3 and 1.2 and exposes them through a common API. We have tested interoperability for our TLS 1.2 record layer with all major TLS implementations. For TLS 1.3 draft-14, we tested interoperability with multiple implementations, including BoringSSL, NSS, BoGo, and Mint, at the IETF96 Hackathon. For draft-18, we tested interoperability with the latest version of Mint at the time of writing. In all cases, our clients were able to connect to interoperating servers using an ECDHE or PSK_ECDHE key exchange, then to exchange data with one of the following AEAD algorithms: AES256-GCM, AES128-GCM, and ChaCha20-Poly1305. Similarly, our servers were able to accept connections from interoperating clients that support the above ciphersuites.

Performance We evaluate the performance of our record layer implementation at two levels. First, we compare our implementation of AEAD encryption extracted to C using an experimental backend for F to OpenSSL 1.1.0 compiled with the no-asm option, disabling handwritten assembly optimizations. Our test encrypts a random payload of 2 14 bytes with 12 bytes of constant associated data. We report averages over 3,000 runs on an Intel Core E5-1620v3 CPU (3.5GHz) Our implementation is 17 to 18 times slower than OpenSSL for AES-GCM and about 30% slower for ChaCha20-Poly1305. Note that the performance of custom assembly implementations can be significantly better. OpenSSL with assembly can perform ChaCha20-Poly1305 in about one cycle per byte and can do AES128-GCM and AES256-GCM in less than half a cycle per byte. Next, we measure the throughput of our record layer integrated into miTLS by downloading one gigabyte of random data from a local TLS server. We compare two different integration methods: first, we extract the verified record layer in OCaml, and compile it alongside the OCaml-extracted miTLS. Then, we build an F interface to the C version of our record implementation and call it from miTLS. We compare these results with the default AEAD provider of miTLS (based on OpenSSL 1.1.0 with all optimizations, including hardware-accelerated AES), and curl (which uses OpenSSL for the full TLS protocol). We observe that miTLS is not a limiting factor in these benchmarks as its performance using the OpenSSL implementation of AEAD encryption is comparable to that of libcurl. Unsurprisingly, the OCaml version of our verified implementation performs very poorly. This is due to the high overhead of both memory operations and arithmetic computations in the OCaml backend of F (which uses garbage-collected lists for buffers, and arbitrary-precision zarith integers). The C extracted version is over 30,000 times faster, but remains two orders of magnitude slower than the hardware-optimized assembly implementations in OpenSSL for AES. For ChaCha20-Poly1305, we achieve 50% of the assemblyoptimized OpenSSL throughput.

Although our code is optimized for verification and modularity rather than performance, we do not believe that we can close the performance gap only by improving F code for hardware-accelerated algorithms such as AES-GCM-instead, we intend to selectively link our F code with assembly code proven to correctly implement a shared functional specification. We leave this line of research for future work.

Security Proofs for Section 3

Claim 1. IND-UF-1CMA implies UF-1CMA when q v ≥ 1 and random tags are neither necessary nor sufficient for unforgeability.

(i) To see the latter, consider the mac(k, m) function that just returns the random key k as its tag for every message. Returning k for t * break UF-1CMA but the scheme nevertheless satisfies the randomness requirement for A[ m , 0] adversaries. (ii) To see the former, consider the Mac1 b game with r = 0 (denoted Mac1 b 0 ). We can relate Mac1 b 0 to the standard unforgeability definition as follows: clearly, an adversary who wins the UF-1CMA game can win the Mac1 b 0 game by submitting his forgery (m, t) to Verify, which returns false if and only if b = 1. Conversely, an adversary that wins the Mac1 b 0 game with advantage Mac1 0 (A[ m , q v ]) must query Verify on at least one forgery with the same probability, since the adversary's view is otherwise independent of b. In the reduction, B[ m ] guesses in which of the q v Verify queries A submits his first forgery and return false for all prior queries.1 It follows that:

Mac1 0 (A[ m , q v ]) ≤ q v UF-1CMA (B[ m ]).

Figure 1 :

 1 Figure 1: Multiplexing of sub-protocol streams by the record layer, depicting a TLS 1.3 draft-19 0-RTT handshake with re-keying.

Figure 2 :

 2 Figure 2: Modular structure of our proof. Green arrows denote security reductions proved by typing.

  abstract type repr = buffer UInt32.t 5 ( * 5-limb representation * ) val select: memory → r:repr → Tot elem ( * current value held in r * ) val multiply: e0:repr → e1:repr → ST unit (requires live e0 ∧ live e1 ∧ disjoint e0 e1) (modifies e0) (ensures select e0 = select e0 * @ select e1)

  val p : nat val c : nat type lbytes ( :nat) = b:bytes{length b = } type bbytes ( :nat) = b:bytes{length b ≤ } type plain = lbytes p type cipher = lbytes c abstract type key val keygen: unit → ST key val decrypt: key → cipher → Tot (option plain) val encrypt: k:key → p:plain → ST (c:cipher{decrypt k c = Some p})

  abstract type key = {key: AE.key; log: encryption_log} let encrypt (k:key) (p:plain) = if b then let c = random_bytes c in k.log ← k.log ++ (c,p); c else AE.encrypt k.key p where the (private) key representation now includes both the real key and the ideal encryption log. The encrypt function uses k.log to access the current log, and ++ to append a new entry, much as the Encrypt oracle. Idealization Interfaces The idealized module AE b can be shown to implement the following typed interface that reflects the security guarantee of the Ae b game: abstract type key val log: memory → key → Spec (seq (cipher × plain)) val keygen: unit → ST k:key (ensures b ⇒ log k = ∅) val encrypt: k:key → p:plain → ST (c:cipher) (ensures b ⇒ log k = log k ++ (c,p)) val decrypt: k:key → c:cipher → ST (o:option plain) (ensures b ⇒ o = lookup c (log k) ∧ log k' = log k)

  val k0 : nat ( * static key length, may be 0 * ) val k : n:nat { k0 ≤ k } ( * total key length * ) val t : nat ( * tag length * ) val m : nat ( * maximal message length * ) type key 0 = lbytes k0 ( * static key shared between MACs * ) type key = lbytes k ( * one-time key (including static key) * ) type tag = lbytes t ( * authentication tag * ) type message = b:bbytes b {wellformed b} val keygen 0 : unit → ST key 0 val keygen: key 0 → ST key val verify: key → message → tag → Tot bool val mac: k:key → m:message → Tot (t:tag{verify k m t})

  val d : nat ( * fixed domain length * ) val b : nat ( * fixed block length * ) type domain = lbytes d type block = lbytes b val eval: key → domain → Tot block ( * functional specification * )

  val n : nat ( * fixed nonce length * ) val a : n:nat{n < 2 32 } ( * maximal AD length * ) val p : n:nat{n < 2 32 } ( * maximal plaintext length * ) val cipherlen: n:nat{n ≤ p } → Tot nat type nonce = lbytes n type ad = bbytes a type plain = bbytes p type cipher = bytes val decrypt: key → nonce → ad → c:cipher → ST (option (p:plain{length c = cipherlen (length p)})) val encrypt: k:key → n:nonce → a:ad → p:plain → ST (c:cipher{length c = cipherlen (length p))

Function

  encode(c, a) return pad 16 (a) pad 16 (c) length 8 (a) length 8 (c) Function pad 16 (b) r, b 1 , . . . , b r ← split 16 (b) return b zeros(16 -|b r |)

  abstract type key ( * stateful key, now containing the log * ) val log: memory → key → Spec (seq (nonce × ad × cipher × plain) val keygen : unit → ST (k:key) (ensures b ⇒ log k = ∅) val encrypt: k:key → n:nonce → a:ad → p:plain → ST (c:cipher) (requires b ⇒ lookup_nonce n (log k) = None) (ensures (b ⇒ log k = log k ++ (n,a,c,p))) val decrypt: k:key → n:nonce → a:ad → c:cipher → ST (o:option plain) (ensures b ⇒ o = lookup (n,a,c) (log k))

  type seqn_t = UInt64.t val q e : seqn_t ( * maximal number of encryptions * ) val cipherlen: n:nat{ n ≤ p } → Tot nat ( * e.g. p + MAC. t * ) type role = E | D abstract type state (r:role) val seqn: mem → state r → Spec seqn_t val gen: unit → ST (s:state E) (ensures seqn s = 0) val genD: state E → ST (s:state D) (ensures seqn s = 0) val encrypt: s:state E → ad → p:plain → ST (c:cipher{length c = cipherlen (length p)) (requires seqn s < q e ) (ensures seqn s = seqn s + 1) val decrypt: s:state D → ad → c:cipher → ST (o:option (p:plain{length c = cipherlen (length p)})) (requires seqn s < q e ) (ensures seqn s = if o = None then seqn s else seqn s + 1)

Figure 3 :

 3 Figure 3: Constructing a TLS 1.3 record fragment

  val parse_record: r:record → Tot (option (n:nat × c:lbytes n)) val format_record: n:nat → c:lbytes n → Tot (r:record) (ensures parse_record r = Some (n,c))

Table 2 :

 2 Modules in our verified record layer implementation

  on Windows 64-bit.

		Crypto.AEAD	OpenSSL
	ChaCha20-Poly1305	13.67 cycles/byte	9.79 cycles/byte
	AES256-GCM	584.80 cycles/byte 33.09 cycles/byte
	AES128-GCM	477.93 cycles/byte 28.27 cycles/byte

See[START_REF] Bellare | The power of verification queries in message authentication and authenticated encryption[END_REF] for a detailed discussion of this proof strategy, and the reason why strong unforgeability, i.e. log = (m , t ) and not just ∀t. log = (m , t), is necessary.

Acknowledgements

This research received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement no. 683032 -CIRCUS)

Definition 7 (Stae). Let Stae (A[q e , q d , p , a ]) be the advantage of an adversary A that makes q e encryption queries and q d decryption queries in the game below. The game involves a single encryptor, a table of decryptors D, and a log of encryptions E. For brevity, it relies on the stateful encryptor and decryptors specified above, e.g. encrypts increments s.seqn and Encrypt records the encryption with sequence number s.seqn -1. (Equivalently, it could keep its own shadow copies of the sequence numbers.) In contrast with AEAD, decryption only succeeds for the current sequence number of the decryptor.

Our definition corresponds most closely to level-4 (stateful) LHAE of [START_REF] Boyd | From stateless to stateful: Generic authentication and authenticated encryption constructions with application to TLS[END_REF]. In both definitions the requirement is that decrypt only successfully decrypted a prefix of what was sent. We discuss minor differences: in their game the adversary needs to distinguish m 0 from m 1 , while in our game he has to distinguish ciphertexts from random. Also, instead of rejecting all decryptions when b = 0 and forbidding in-sync challenge ciphertexts when b = 1 we return in-sync challenge plaintexts in both cases. These changes are superficial; the rational behind them is to keep our game close to our idealizing modules in the implementation. Another difference is that we do not require real decryption to continue rejecting ciphertexts upon decryption failure. We also leave length-hiding and stream termination to §7. So our definition compares to their definitions with the maximal plaintext length set to |p|.

Theorem 3 (Stae perfectly reduces to Aead). Given A against Stae, we construct B against Aead with

Proof. We build B by composing A with a variant of the construction given above that calls Aead oracles instead of AEAD functions.

In TLS 1.2 with AES-GCM, there is a probability p(q e ) ≈ q 2 e 2 65 of collision when the IVs are randomly sampled. This probably already exceeds 2 -32 after less than 2 17 fragments. This is more than sufficient to mount practical attacks against HTTPS websites, as demonstrated in [START_REF] Böck | Nonce-disrespecting adversaries: Practical forgery attacks on GCM in TLS[END_REF]. Therefore, random explicit IVs must not be used in TLS 1.2.

Stream Closure As explained in §6, stream integrity ensures that decrypted traffic is a prefix of encrypted traffic. Complementarily, the TLS record layer relies on well-defined final fragments, specified as a predicate val final: fragment → Tot bool, to ensure that no further encryptions are performed on a stream after sending such a fragment.

For LHAE, we extend the stateful key of StAE to record the termination status of the stream, which can be queried with the predicate val closed: mem → state r → Spec bool. Furthermore, we extend the postcondition of encryption to ensure that the state s after encrypting fragment f satisfies closed s = final f. Therefore, upon receiving a final fragment, the decryptor is guaranteed to have received the whole data stream. This control-flow mechanism only depends on stream integrity; it does not involve additional cryptography, but provides a useful additional guarantee to the application, and may help achieve forward secrecy by erasing the stream key immediately after closure.

LHSE Construction and Game

The construction is:

with the same state as StAE-we omit the unmodified functions for generating encryptors and decryptors. When a final fragment is sent or received, we erase the StAE state. The TLS 1.3 construction uses empty associated data, relying on implicit authentication of the underlying key and sequence number. (Our code also supports the older TLS 1.2 construction, which uses 13 bytes of associated data in total, obtained by appending the protocol version and the content type to the sequence number of stream encryption.) Definition 8 (Lhse). Given LHSE, let Lhse (A[q e , q d ]) be the advantage of an adversary A that makes q e encryption queries and q d decryption queries in the game below.

where f 0 (respectively, f 1 ) is a fragment (respectively, a final fragment), with fixed content type and data 0 .

Proof of Lemma 1. Let H i , i ∈ [0, q i ] be hybrids of MMac1 1 that only idealize the first i instances: that is, the first i queries to H i .Keygen behave as MMac 1 .Keygen while later queries behave as MMac 1 .Coerce(n, k $ ← byte k ). In particular, H q i is equivalent to MMac 1 as all keys are idealized, and H 0 is equivalent to MMac 0 as no key is idealized.

By the triangle inequality:

In the reduction, B picks i at random between 1 and q i and uses its oracles to Mac1 b such that A either interacts with H i or H i-1 depending on b. B returns the output of A.

By definition, Mac1 (B[ m , q v ]) is:

Note that we could express a tighter bound in case we had an upper bound for the number of verification queries that A makes per instance, which could be as low as q v /q i . We directly prove MMac1 security for GHASH and Poly1305, so this has no effect on our main result.

Proof of Lemma 2. In the reduction, B guesses in which Verify query A might make its first forgery (say, query number q). This guess is correct with probability 1/q v . Note that a successful A may distinguish purely based on the tag and never submit a forgery; in that case, the simulation provided by B is perfect until the end of the experiment. B simulates the q v verification queries by returning 0 or 1 depending on whether the tag-message pair was generated using a query to Mac. If B guessed correctly, the simulation is perfect up to the submission of the forgery. Now B submits the message-tag pair of the query q to its single-call Verify oracle. Let b be the result of this query, and b be the output of A after running to completion with all further Verify oracles simulated as before.

B output b ∧ ¬b as its guess. If the q th query result indicates a forgery, then clearly b = 0, otherwise we either guessed q wrongly or the adversary did not query on a forgery and so b is the result of a perfect simulation.

In both cases, conditioned on having guessed correctly, the success probability of B is greater equal the success probability of A and thus

Proof of Theorem 1. We make use of Lemma 2 and first prove the bound d•τ

|R| for an adversary that makes only a single Verify query. We refer to the instance in which the Verify query is made as the target instance.

Game 0 For a given r and message m, we can compute s and t from one another. Thus, we first perform the following game transformation (with no security loss):

When answering Mac before Verify, instead of sampling the one-time pad s and adding it to finalize the WCS MAC, we sample instead the tag t that will be released. For verification we compute s from t, m and r.

When answering Verify before Mac, we verify as before, but store (v , t , m ) in an additional table. For Mac we sample the tag t at random, and compute its s from t, m and r. Only if the answer we would have given in verification differs between s and s , we recompute the tag using s.

Game 1 For the target instance, we can distinguish two cases: either the Mac oracle or the Verify oracle gets queried first. Consider the following game in which idealizations are marked by ( * # * ):

We separately bound the probabilities for the following two events: ( * 1 * ) The oracle call to Verify(n, m , t ) accepts a forgery after calling Mac(n, m), ( * 2 * or * 3 * ) The oracle call to Verify(n, m * , t ) accepts a forgery before calling Mac(n, m) or the Mac query has to correct its tag t, because v = v . This second event requires the adversary to guess either the value s or the value t, both sampled at random, to set v or v to 1 respectively. We bound this probability by 2 -t+1 .

The first event dominates the probability. The adversary wins if and only if t t = hash r (m ) hash r (m) for m = m . This probability is bound by the -almost--universal property of GHASH and Poly1305. Proof. The hypothesis is equivalent to (a mod 2 128 ) -(a mod 2 128 ) = y + γ • 2 128 for some γ ∈ -1..0, so we can use δ = γ + a /2 128 -a/2 128 .

We have that hash r (x) hash r (x ) = y if and only if

for some y δ = y + δ • 2 128 with δ ∈ -4..3 for Poly1305 0 for GHASH Equation 1, defines a non-null polynomial of degree at most d and tests whether r is a root of that polynomial. Since each polynomial is not null, it has at most d roots, and the equality holds with probability at most d/|R|. We arrive at the bound stated in the theorem by multiplying by the number of possible polynomials in the construction-specific step.

Security Proofs for Section 4

Proof of Lemma 3. When A queries EvalEnx or EvalDex (they are exactly the same except for parameter names), B calls Prf b .Eval, XORs the value provided by A, and truncates. To compute k 0 when j 0 = 1, B queries Prf.Eval on 0 b . Whenever A queries PrfCtr.EvalKey on nonce j 0 n, B queries Prf.Eval on the same input, prepends k 0 , and truncates.

Analysis The requirement j > j 0 in EvalEnx and EvalDex, guarantees that EvalKey uses disjoint parts of the PRF's domain regardless of j 0 . The use of j 0 n in EvalKey also guarantees that k 0 is computed using a disjoint element of the domain. As the simulation is perfect B can forward the output of A as its own guess, making in total q b + q g + j 0 queries to Prf.

Security Proofs for Section 5

Proof of AEAD construction. As a first step of the proof of AEAD security we model the composition of cryptographic functionalities in our implementation using abstract keys with state.

Composing auxiliary games We introduce the following composed game PrfCtr b (PRF, MMac1 b (MAC)) that restrict adversaries from accessing the real MAC keys. This will allow us to idealize both the PRF and the MAC functionalities in order to idealize the authentication of ciphertexts:

with the same EvalEnx and EvalDex oracles as in §4. Thus, the adversary has access to the oracles EvalKey, EvalEnx and EvalDex of the PrfCtr b game; in addition, for every nonce n queried to EvalKey, the adversary is given access to oracles Mac and Verify of the MMac1 game. In the composed game, the adversary is not given direct access to the MAC keys; instead the game calls MMac1.Coerce to turn PRF blocks into MAC keys.

When it is clear from the context we will omit the game parameters PRF, MAC and instead write PrfCtr b (MMac1 b ). Both the PrfCtr b and the MMac1 b components of the game use the same random bit b to determine the winning condition. However, we commonly use composed games in reduction proofs where some component uses a fixed value of b, which we write as superscript. For instance, we may write PrfCtr b (MMac1 0 ) to compose PrfCtr with only the real variant of MMac1 b . Lemma 5 (PrfCtr(MMac1) reduces to MMac1 and Prf). Given A against PrfCtr(MMac1), we construct B against Prf and C against MMac1 such that:

Proof. We write A PrfCtr b (MMac1 b )) to refer to the adversary's output bit when interacting with such a game. By definition, PrfCtr(MMac1) (A[q b , q i , m , q v ]) is:

By the triangle inequality:

This justifies the game transformation that first switches from PrfCtr b (MMac1 0 ) to PrfCtr b (MMac1 1 ). We bound the difference:

, where C runs A against the game PrfCtr 1 (MMac1 b ) by simulating PrfCtr 1 and returning the output of A. Similarly, we bound the difference:

, where B runs A against the game PrfCtr b (MMac1 0 ) by simulating MMac1 0 and returning the output of A. We conclude by applying Lemma 3.

We can similarly define a composed game PrfCtr b,b (MMac1 b ) for the specialized game PrfCtr b,b . Our proof uses the following lemma about PrfCtr 1,b , which can be lifted to PrfCtr 1,b (MMac1 1 ).

Main proof

The proof proceeds in a sequence of game steps.

Game 0 is defined as G0 = AeadCtr(PrfCtr 0 (MMac1 0 )): by inlining the real versions of EvalPad, Mac and Verify from PrfCtr 0 (MMac1 0 ), one can easily see that this game is identical to Aead 0 (AEAD), hence we have that Pr[

Game 1 is defined as G1 = AeadCtr(PrfCtr 1 (MMac1 1 )). Game 0 and Game 1 are the same game except for the bit b of PrfCtr, so a reduction A can simply simulate the game and returns the output of A as its guess. Therefore:

, q e + q d , p + a + 46, q d ])

The implementation inlined into Game 1 has random tags and one-time-pads and the MAC is perfectly unforgeable. We could now conclude that in this implementation, not only the pads, but the full ciphertexts are random. This, however, requires us to reason about the various encoding steps (splitting the plaintext and splicing the ciphertext taking into account the truncated block), to check that we never apply the same pad twice, and to show that decryption is not revealing information about the plaintext blocks. We implement this information-theoretic step of the proof in F , where we can get assurance that we capture the correct implementation details in the real implementation (by running it on known test vectors).

Game 2 is defined as G2 = AeadCtr(PrfCtr 1,0 (MMac1 1 )). Game 1 and Game 2 are perfectly equivalent.

Proof. EvalEnx calls EvalEnx after checking T [j n] = ⊥. We will show that this restriction is already enforced by AeadCtr.

Similarly for every call to EvalDec we will show that the restriction T [j n] = (p, c) is already enforced by AeadCtr when the bit b of PrfCtr is set. In this case decryption using ⊕ in G1 already leads to the same result as the lookup in T of G2.

We prove both restrictions on AeadCtr using an F invariant that relates the content of the table C of AeadCtr to the log of MMac1:

For the first restriction, the AeadCtr game guarantees that C[n] = ⊥ upon calling Encrypt, consequently, T [j n] = ⊥ upon calling EvalEnx.

For the second restriction, the MMac1 game guarantees that Verify only succeeds, if encode([c j∈ [1,r] ], a) was recorded in log by a call to Encrypt. We can thus conclude by the injectivity of encode that the restriction holds.

Game 3 is defined as G3 = AeadCtr(PrfCtr 1,1 (MMac1 1 )). Game 2 and Game 3 are perfectly equivalent by Lemma 6. Together we have P r

Note that the condition T [j n] = (p, c) in EvalDex (j n, c) restricts decryption to those cases where decryption using ⊕ when b = 0 would already lead to the same result as the table lookup.

From the invariant we also infer that Pr

Ciphertexts thus consists of random PRF blocks that are never repeated. Consequently, they are themselves indistinguishable from random. Summarizing the game steps

, q e + q d , p + a + 46, q d ])

Server S Knows sk C , psk Knows sk S , psk log 0 log 0 ClientHello(n C , g x , a 0 , . . .) 0-RTT Keys (encrypt-only):

ServerHello(n S , g y , a 1 , . . .)

Handshake Keys:

Handshake Keys: