channels). This is in particular interesting for non-cryptographic assumptions that the CryptoVerif model contains about functions, e. g., message encoding functions and (de) serialization functions that are assumed to be correctly encoding and decoding, and encryption and decryption functions that are assumed to be correctly implemented. In $F^*$, we can implement these functions and prove that they actually have the correctness property assumed in the CryptoVerif model. The cv2fstar compiler translates the equations and non-cryptographic assumptions included in the CryptoVerif model to proof obligations – lemmas – in $F^*$, which can then be proved to hold for the actual implementation. This is the first motivation for the link between CryptoVerif and $F^*$, and it has been put in place for this first iteration of the cv2fstar project, and has been tested on the NSL case study.

Second, we would like to express the cryptographic theorems proved by CryptoVerif in $F^*$, as assumed lemmas, or pre- and post-conditions of functions. Then, we could reason further with them, i. e., use them to prove other theorems. This can be interesting for larger systems that cannot be treated in CryptoVerif but where $F^*$'s capabilities could be useful. This second motivation has not yet been implemented and remains for future work. The kinds of theorems that we need to translate are (1) correspondence properties between events, (2) secrecy properties, and (3) equivalence properties. While the translation of correspondence properties should be relatively straightforward with lemmas about lists of events, for secrecy and equivalence properties we need to relate program codes which is not straightforward in $F^*$.

The cv2fstar project is joint work together with my PhD advisors Bruno Blanchet and Karthik Bhargavan. There is no publication or ongoing submission of this work yet, at the moment of thesis submission – this is planned for after submission when we did some finishing touches. Some of them are laid out in the section on future work. Future readers might want to watch out for a peer-reviewed publication of this work, or a preprint version.

## 6.2 RELATED WORK

This work integrates in a long line of research considering different approaches to ensure cryptographic guarantees of implementations. We present work in the computational model and in the symbolic model. For both, we group by (1) extraction of an implementation from a model, (2) extraction of a model from an implementation, and (3) proofs done directly on an implementation.

**COMPUTATIONAL MODEL, EXTRACTING IMPLEMENTATIONS.** A translation from CryptoVerif models to OCaml has been developed during David Cadé's thesis [CB13; CB15]. It is accompanied by a soundness proof, assuring that for each cryptographic attack successfully executed against the OCaml code, there exists an attack against the CryptoVerif model. A detailed comparison between cv2ocaml and cv2fstar is provided in Section 6.14. CertiCrypt [BGZB09] is built on top of Coq and can generate OCaml, Haskell, and Scheme implementations of its deeply embedded pWhile language through Coq's built-in extraction mechanism. The Foundational Cryptogra-

<footnote>[CB13] Cadé and Blanchet, “From Computationally-Proved Protocol Specifications to Implementations and Application to SSH”</footnote>

<footnote>[CB15] Cadé and Blanchet, “Proved Generation of Implementations from Computationally Secure Protocol Specifications”</footnote>

<footnote>[BGZB09] Barthe et al., “Formal Certification of Code-Based Cryptographic Proofs”</footnote>
phy Framework (FCF) [PM15] allows to write security proofs with concrete bounds in the computational model. It is formalized in Coq, which again allows to extract executable code.

### EXTRACTING MODELS.
The Jasmin [Alm+17] framework and programming language together with the EasyCrypt proof assistant [Bar+11] form an ecosystem that links verified and executable code to cryptographic proofs. Jasmin code can be compiled to assembly for execution in production, and to EasyCrypt for proofs of functional correctness, cryptographic properties, and constant timeness. The toolchain has been used to prove indifferen- tiability, correctness, and constant timeness of a Jasmin SHA-3 implemen- tation [Alm+19]. A tool taking the opposite approach of our cv2fstar is fs2cv [Bha+08a], extracting a CryptoVerif model from an F# protocol im- plementation. F# is a general-purpose programming language from the ML family and is part of the .NET Framework. An approach extracting CryptoVerif models from C via symbolic execution [AGJ12], started by ex- tracting ProVerif models [AGJ11] and using a computational soundness result [BHU09].

### PROOFS ON CODE.
The Verified Software Toolchain (VST) Coq library has been used with FCF to verify the correctness and security of OpenSSL's HMAC implementation in C, using symbolic execution of the actual source code [Ber+15]. The F7 typechecker and its underlying methodology have been extended to support modular verification in the computational model of F# implementations [FKS11]. This allows to ensure asymptotic crypto- graphic guarantees by typing, and has been applied to the miTLS verified TLS implementation [Bha+13; Bha+14b]. The ideas have been further devel- oped for use in F\*, applied to the Record Layer of TLS 1.3 [DL+17]. [Bar+14] and [Gri+19] present frameworks for probabilistic relational verification in F\*. Küsters, Truderung, and Graf present a framework to prove computa- tional indistinguishability properties for Java-like programs [KTG12].

### SYMBOLIC MODEL, EXTRACTING IMPLEMENTATIONS.
Piromonti and Sisto gen- erate Java implementations from models written in spi calculus [PS10]. Sisto, Avalle, Piromonti, and Pozza go further and implement spi calculus in Java, using Java both for modeling and implementation, and generating an implementation from the model with the help of annotations [Sis+11]. Chevalier and Rusinowitch generate OCaml implementations [CR10] from analyses done with CPPL [Gut+05]. Corin, Denielou, Fournet, Bhargavan, and Leifer show how to compile session types to cryptographic protocols in F\# [Cor+08]. Fournet, Le Guernic, and Rezk present a methodology to generate F\# implementations from information flow specifications [FGR09]. Noise Explorer generates ProVerif models as well as Go and Rust imple- mentations from Noise protocol patterns [KNB19]. The symbolic analy- sis framework Dolev-Yao\* (DY\*) in F\* "bridg[es] the gap between trace- based and type-based protocol analyses" [Bha+21], with executable models. Noise\* [Ho+22] uses DY\* in a development of a once-and-for-all verified generator of Noise protocol implementations, linking all the way down to efficient implementations in C.

[PM15] Petcher and Morrisett, "The Founda- tional Cryptography Framework"

[Alm+17] Almeida et al., "Jasmin: High- Assurance and High-Speed Cryptography"

[Bar+11] Barthe et al., "Computer-Aided Security Proofs for the Working Cryptogra- pher"

[Alm+19] Almeida et al., "Machine-Checked Proofs for Cryptographic Standards: Indif- ferentiability of Sponge and Secure High- Assurance Implementations of SHA-3"

[Bha+08a] Bhargavan et al., "Cryptographi- cally verified implementations for TLS"

[AGJ12] Aizatulin et al., Computational Ver- ification of C Protocol Implementations by Symbolic Execution

[AGJ11] Aizatulin et al., "Extracting and Ver- ifying Cryptographic Models from C Protocol Code by Symbolic Execution"

[BHU09] Backes et al., "CoSP: A General Framework for Computational Soundness Proofs"

[Ber+15] Beringer et al., "Verified Correct- ness and Security of OpenSSL HMAC"

[FKS11] Fournet et al., "Modular code-based cryptographic verification"

[Bha+13] Bhargavan et al., "Implementing TLS with Verified Cryptographic Security"

[Bha+14b] Bhargavan et al., "Proving the TLS Handshake Secure (As It Is)"

[DL+17] Delignat-Lavaud et al., "Imple- menting and Proving the TLS 1.3 Record Layer"

[Bar+14] Barthe et al., "Probabilistic Rela- tional Verification for Cryptographic Imple- mentations"

[Gri+19] Grimm et al., A Monadic Frame- work for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations

[KTG12] Küsters et al., "A Framework for the Cryptographic Verification of Java-Like Programs"

[PS10] Piromonti and Sisto, "Provably correct Java implementations of Spi Calculus secu- rity protocols specifications"

[Sis+11] Sisto et al., "JavaSPI: A Framework for Security Protocol Implementation"

[CR10] Chevalier and Rusinowitch, "Com- piling and securing cryptographic protocols"

[Gut+05] Guttman et al., "Programming Cryptographic Protocols"

[Cor+08] Corin et al., "A Secure Compiler for Session Abstractions"

[FGR09] Fournet et al., "A Security- Preserving Compiler for Distributed Pro- grams"
**EXTRACTING MODELS.** Bhargavan, Fournet, Gordon, and Tse compile protocol implementations written in F# to ProVerif models [Bha+08b].

**PROOFS ON CODE.** The F7 tool has originally been developed to typecheck interfaces with refinement and dependent types for F# implementations, in a work by Bengtson, Bhargavan, Fournet, Gordon, and Maffeis [Ben+08]. The F5 typechecker is an advancement on the F7 work adding union, intersection, and polymorphic types [BHM14]. ASPIER [CD09] has been used to analyze authentication and secrecy properties of parts of the OpenSSL source code. Dupressoir, Gordon, Jürjens, and Naumann use the general-purpose verifier VCC and Coq to analyse C programs in the symbolic model [Dup+11].

## 6.3 THE OUTPUT LANGUAGE

In this section, we briefly present some language elements of $F^*$. The syntax of $F^*$ is mostly the same as in OCaml. $F^*$ supports algebraic data types, too. This includes product types like tuples and records, and sum types like tagged unions. Like OCaml, $F^*$ has pattern matching in let bindings and match statements, and supports higher-order functions.

For example, a custom type of natural numbers can be defined as follows in $F^*$, as a tagged union:

1. `type natural =`
2. `| Zero`
3. `| Succ: natural → natural`

The constructor `Zero` does not have parameters, and `Succ` has one parameter, indicating the previous natural number. We can implement a predicate determining if an element of this type is non-zero with a match statement:

1. `let nonzero n =`
2. `match n with`
3. `| Zero → false`
4. `| Succ _ → true`

Here, the underscore stands for an arbitrary value.

Comparing $F^*$ to OCaml, the main difference is that $F^*$'s types are richer, and in particular can be dependent. The definition of a *dependent type* can depend on parameters. For example, using $F^*$'s built-in type for natural numbers, `nat`, we can define a type of bounded natural numbers as follows:

1. `type bounded l = n:nat{n < l}`

The dependent type `bounded` has a parameter `l` that is used in the *refinement* `{n < l}` to define that this type contains all $n \in \mathbb{N}$ for which the condition $n < l$ holds. Generally, a refinement restricts the elements of the type to those that fulfill the predicate given inside the braces. Then, we can define a constant `t` as follows:

1. `let t:bounded 3 = 2`

Functions can also use dependent types, as in the following example for a subtraction function defined for our example type:

[Bha+08b] Bhargavan et al., "Verified Interoperable Implementations of Security Protocols"

[Ben+08] Bengtson et al., *Refinement Types for Secure Implementations*

[BHM14] Backes et al., "Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations"

[CD09] Chaki and Datta, "ASPIER: An Automated Framework for Verifying Security Protocol Implementations"

[Dup+11] Dupressoir et al., *Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols*
1 let bounded_sub
2 (#l:nat)
3 (a:bounded l)
4 (b:bounded l{b ≤ a})
5 : (bounded (l-b))
6 = a - b

The function has three parameters: the lower bound `l`, a natural number `a` bounded by `l`, and a natural number `b` bounded by `l` that we additionally restrict with a refinement to being at most as large as `a`. In the function's return type, we use both the parameters `l` and `b`, to indicate that the result has a lower bound. The parameter `l` is prefixed with a `#`. This indicates that the parameter is implicit, which means that it can be omitted in case the F\* typechecker can infer it from the remaining parameters. In this case, the value of `l` can be inferred from the types of both `a` and `b`.

Coming back to our example of a custom type for natural numbers, we can define the following decrease function to showcase pattern matching in let bindings:

1 let decr (n:natural{nonzero n}) =
2 let Succ m = n in
3 m

Here, we restrict the parameter to non-zero natural numbers using the predicate defined earlier. Then, `F\*` understands that `n` can only be an element built with the `Succ` constructor of the tagged union, and we can use a let pattern matching to destruct it.

An important dependent type from the HACL\* library that we use in `cv2fstar` is `lbytes len` from the HACL\* module `Lib ByteSequence`. This type implements fixed-length bytestrings, where `len` is the length in bytes. The parameter `len` is of type `sizeNat`, which is the type of natural numbers up to a maximum of `max_sizeNat = 2^32 - 1`. The definition of the type `lbytes len` is as follows:

1 let lbytes (len:sizeNat) =
2 s:Seq.seq uint8{Seq.length s == len}

The type `Seq.seq` is from `F\*`'s standard library and implements arbitrary-length sequences of a type given as parameter. Here, the parameter is `uint8`, which implements unsigned machine integers of size 8 bits.

`F\*` functions can have pre- and post-conditions that the typechecker enforces. The subtraction function on bounded natural numbers can be written as follows, using pre- and post-conditions:

1 val bounded_sub2: l:nat → a:nat → b:nat
2 → Pure (nat)
3 (requires a < l ∧ b ≤ a)
4 (ensures λc → c < l-b)
5
6 let bounded_sub2 l a b = a - b

Here, we use a function declaration with the `val` keyword. The `requires` clause states the pre-condition, and the `ensures` clause the post-condition that is a function of the return value of the function. With the effect `Pure`, `F\*` checks that the function has no side effects and that it terminates. We did not indicate an effect for the previous functions. The standard effect in `F\*` is
Tot, which is like Pure, just without pre- and post-conditions: it indicates a function without side effects that terminates.

Lemmas are a special kind of functions in $F^*$, and can be used to record provable facts. Like with generic functions, different styles are available to write down lemmas and their pre- and post-conditions. We introduce the style that we use most in `cv2fstar`. Consider the following third implementation of our subtraction function:

1 let bounded_sub3 a b = a - b

Here, we removed all pre- and post-conditions, and refinements on types. We instead move them to a separate lemma:

1 let lemma_bounded_sub3
2 (l:nat)
3 (a:nat{a < l})
4 (b:nat{b ≤ a})
5 : Lemma (bounded_sub3 a b < l - b) = ()

The parameters of the lemma correspond to the parameters of our first implementation, and express the pre-conditions. The post-condition in parentheses behind the keyword `Lemma` expresses what we put into the result type or the post-condition of the other implementations of the function. $F^*$ is able to prove this lemma without further help, which is why the lemma's function body contains only `()`. Besides the interest in their own proof, lemmas can be used to guide `F^*`'s typechecker in other proofs, by instantiating them with particular parameters, as needed.

To structure an $F^*$ development, it can be split into separate files, called *modules*. Other modules can be used within a module, by importing them, called *opening*. A module's interface and implementation can be separated into an *fsti* and *fst* file, respectively. By default, when a module A opens a module B, only the interface of B is visible inside A, while the implementation of B stays hidden. In $F^*$, as a reminder, declarations without implementation begin with the *val* keyword. The implementation of a type begins with the *type* keyword, and implementations of functions, and proofs of lemmas begin with *let*. If an interface contains a *val* declaration but no implementation, the implementation must be provided in the *fst* file of the same module.

## 6.4 THE INPUT LANGUAGE

Starting from CryptoVerif's standard input language, we make two modifications: (1) We restrict it to a subset that is supported by `cv2fstar`; (2) We extend it to allow for annotations that guide the extraction.

### 6.4.1 Annotations For Extraction

There are two kinds of annotations. The first kind is marking blocks of code for extraction. Parts that shall be extracted must be wrapped in a block starting with `module_name {` and ending with `}`, and we call such a block a *module*. Each module will be extracted to a module in $F^*$, with an *fsti* file for the interface and an *fst* file for the implementation.
The following code snippet shows an excerpt of the NSL case study as an example. Here, the `Initiator` module is defined inside the initiator process. We see that the oracle inside the process is replicated, through usage of the `foreach` keyword. We will discuss later that this replication is a requirement.

```python
1 let initiator() =
2
3 Initiator {
4   foreach i_init ≤ Qinit do
5     initiator_sendMsg1 (...) :=
6     ...
7     return (...);
8   ...
9
10
11
12
13 }.
```

The second kind of annotations is for each type, constant, function, and table that is used within an extracted module. The required annotation differs for each of these:

* **type** Types must be annotated with at least the name to be used in `F*`. If terms of the type are used in equality tests, then an indication of an equality test function is required.

There are many conditions under which an indication of a name for a serialization and deserialization function is required for a type. From CryptoVerif's point of view, it is required if terms of this type are cast to a bitstring, e. g., because they are assembled to a tuple or used directly within an out process (return of an oracle). From the point of view of the `cv2fstar` framework, a serialization function is also required if terms of this type appear in a table, an event, or a session entry: The framework defines printing helper functions that use the serialization function of a type to print tables, events, and session entries. We describe in Section 6.13.2 how we extract correctness assumptions on (de) serialization to `F*` lemmas.

If the type supports random sampling and the model does sample random values of this type, a function sampling random values of this type must be indicated. A type supports random sampling if it is not unbounded.

A specific kind of types receives special treatment: fixed types. These are types marked with `[fixed]` and model bitstrings of fixed length. For these types, all functions are predefined. The only annotation they require is their size in bits. The treatment of fixed types is covered in more detail in Section 6.6.

The predecessor project `cv2ocaml` allows the indication of a predicate function for a type. We explain in Section 6.14 why we do not need this in `cv2fstar`.

For a type `t`, the syntax of the annotations is as follows:

1. implementation type t="G_t(t)" [serial = "Glle ser(t)", "Gd eser(t)"];

2. equal = "Geq(t)";

3. random = "Gs(t)"].
cv2fstar, we decided to inherit this restriction. Both cv2ocaml and cv2fstar support tables, which are a specific form of *find*, and we believe tables should be sufficient to model practically interesting protocols. One might also think that the semantics of *find* is dubious for practical implementations: While read access to variables of other sessions within the same module is straightforward, read access to variables of other modules that might be executed on remote machines is not. However, it would be possible to implement such access, assuming a secure communication channel between remote modules.

Modules marked for extraction are not allowed to contain `event_abort`. The semantics of `event_abort` in CryptoVerif is that the entire game stops as soon as this event is dispatched. In a practical implementation, it is not feasible to abort the entire system: The module that reached an `event_abort` would need to communicate this fact to other modules, and the adversary could easily suppress this.

We restrict the model to a specific top-level structure. It must be a parallel composition of processes under replication, and each process must be extracted as a module, as follows:

1. ( 
2. module₁ { 
3.   foreach i₁ ≤ N₁ do 
4.     Oracle₁(...) := ... 
5.     return (...) 
6.   ... 
7. } 
8. ) 
9. module₂ { 
10.   foreach i₂ ≤ N₂ do 
11.     Oracle₂(...) := ... 
12.     return (...) 
13.   ... 
14. } 
15. ) 
16. ... 
17. )

This restriction is motivated as follows: Extracted to a function in an F\* module, the top-level oracle of a module can be called at any time, and so we do not allow any model code above it (because we would not be able to enforce that this other code is executed before); also, it can be called any number of times, and so we require that it is under replication in the model (effectively preventing an application from calling the top-level function more than once is hard). Thus, it seems sensible to require the CryptoVerif models and thus the cryptographic proof to be written in a way that accounts for that. The restriction to this specific top-level structure also means that all parts of the model must be extracted. The motivation behind this is that an adversary against the F\* code should be able to do everything that an adversary is allowed to do in the CryptoVerif model.

This restriction of the top-level structure means that, in particular, `cv2fstar` does not allow a non-replicated setup oracle, like it is common in Crypto-Verif and ProVerif models. Such an oracle is for example often used to sample a key for a hash function or a random oracle; this key just models the choice of the hash function and could be ignored in an implementation that uses a
specific hash function. In the top-level structure imposed by `cv2fstar`, this could be implemented by a replicated setup oracle that stores the sampled key in a table; oracles in other modules then need to retrieve it from the table and yield if the adversary did not yet call the setup oracle.

Our usage of HACL\* on the $F^*$ side introduces some restrictions, too: First, types declared as fixed-length in CryptoVerif are restricted to at most $2^{32} - 1$ bytes. Second, technically, we translate CryptoVerif bitstrings, including fixed-length types, to HACL\* bytestrings. This affects practical systems that need bitstrings with a length that is not a multiple of eight. Such applications would need to work around this, or extend the framework accordingly, for example by using the `uint1` type instead of the `uint8` type underlying `bytes`. This would entail rewriting equality test functions for bitstrings instead of bytestrings in HACL\*.

Some restrictions that are present in `cv2ocaml` are no longer present in `cv2fstar`. Events are extracted to $F^*$, while they are ignored in `cv2ocaml`. We allow replication indices to occur in events under the condition that the entire hierarchy of replication indices is used together in a tuple. This is because we use a single session identifier in the `cv2fstar` framework, and do not translate the replication indices individually. The translation of replication indices in events is covered in more detail in Section 6.11.

## 6.5 TRANSLATING TO $F^*$: AN OVERVIEW

In the following sections, we describe step-by-step how we translate CryptoVerif models to executable $F^*$ specifications. We say *executable* because the specifications we write are extractable to OCaml code via $F^*$'s built-in toolchain, and that is also how we execute the code of our case study presented in Section 6.15.

The code generated by the `cv2fstar` compiler does not stand on its own, but runs in the context of what we call the *cv2fstar framework*. This framework consists of two parts: First, a collection of $F^*$ modules that define the generic behaviour of tables (Section 6.9), sessions (Section 6.12), events (Section 6.10), and entropy (Section 6.6.1). This concerns the $F^*$ modules `State`, `NatMap`, `Helper` and `RandomHelper`. These form what we call the *state*, see Section 6.8. Second, an $F^*$ module `CVTypes` containing definitions of standard CryptoVerif types and functions, see Section 6.6.

The `cv2fstar` compiler generates several model-specific files from a CryptoVerif model. In the following, we use $M$ to refer to model's name in uppercase letters, derived from the filename of the CryptoVerif model. It is used in the names of the generated $F^*$ modules. We use $m$ to refer to the all-lowercase version, used in type names. The compiler generates $F^*$ interface files with file extension `fsti` and for some modules, $F^*$ implementation files with file extension `fst`. The compiler generates the following model-specific files. They all depend on `CVTypes`, and we indicate additional dependencies in the following. Figure 6.1 gives a visual overview of how the different parts of a CryptoVerif model translation come together with `cv2fstar`.

`M Types fsti`: This file is generated with the declarations of types that are part of the CryptoVerif model, as discussed in Section 6.6.2. It depends
<figure><img src="image_32.png" /><figcaption>FIGURE 6.1: Visual overview of how the different parts of a `cv2fstar` translation project come together. The uppercase letter M stands for `Ml`, the uppercase name of the CryptoVerif model. On the left in green, we show a CryptoVerif model and its parts. The solid box in the background of the entire column represents the fact that all these parts are within one CryptoVerif model file. Module block annotations contain oracle sequences, and each oracle has a body, which is why we regroup them as modules. The security queries stated in the model are proved with CryptoVerif.</figcaption></figure>

On the middle in blue, we show the files generated by the `cv2fstar` compiler. An arrow coming from the left means that this part from the CryptoVerif model contains information needed to generate the part in the middle. For oracle implementations, separate `fsti` and `fst` files are generated for each module, using the name of the module block annotation as `F*` module name. The only part from the left that is not used for any generation is the security queries. On the right in yellow, we show the parts that a user has to manually implement to complete an extracted `F*` specification: types, functions, and proofs of lemmas. This implementation relationship is represented by dotted lines between middle and right. We do not show a user-written application that uses the extracted executable protocol specification.

On the right at the bottom in orange, we show the `cv2fstar` framework that is written and verified once and for all. The two most important parts are `CVTypes` implementing CryptoVerif's built-in types in `F*`, and `State`, providing functions for managing events, tables, sessions, and entropy.

On the right in the middle in red, we show the `HACL*` library that is used by `CVTypes`, and that can be used by the user-written implementations. This relationship is represented by dotted arrows. Likewise, the user-written implementations can use `CVTypes`. The event, table, and session definitions use `State` and other modules visible in the diagram; we do not display these dependencies because this would introduce too many arrows.

The entire `F*` development shown in the middle and the right column is verified using the `F*` typechecker.
on CVTypes. The user has to provide implementations for the types in a manually written file M Types.fst.

M Functions.fsti: This file is generated with the declarations of functions and constants, as presented in Section 6.7. It depends on M Types and CVTypes. The user has to provide implementations for them in a manually written file M Functions.fst.

M Equations.fsti: This file is generated with lemmas expressing the non-cryptographic assumptions made in the CryptoVerif model as described in Section 6.13. It depends on M Types, M Functions, and CVTypes. The user has to provide proofs for them in a manually written file M Equations.fst.

M Events.fsti AND fst: These are the generated files for the types and functions needed for events, as presented in Section 6.10 and by example in Section 6.15.6. It depends on M Types, State, and CVTypes.

M Tables.fsti AND fst: These are the generated files for the types and functions needed for tables, as presented in Section 6.9 and by example in Section 6.15.3. It depends on M Types, State, and CVTypes.

M Sessions.fsti AND fst: These are the generated files for the types and functions needed for sessions, as described in Section 6.12.4 and by example in Section 6.15.7. They depend on M Types, State, and CVTypes.

M Protocol.fst: This small generated file defines the model-specific state type m_state. It depends on M Types, M Tables, M Sessions, M Events, and State.

M Letfun.fsti AND fst: These are the generated files for the interfaces of letfun functions and their implementations, as described at the end of Section 6.11. They depend on M Types, M Functions, M Tables, M Sessions, M Events, M Protocol, State, Helper, and CVTypes.

M Module.fsti AND fst: For each module block annotation, an interface and an implementation file is generated for the sequence of oracles contained in the module, as described in Section 6.12 and by example in Section 6.15.7. The name used in the module block annotation is used instead of Module, in the filename. They depend on M Types, M Functions, M Tables, M Sessions, M Events, M Protocol, State, Helper, and CVTypes.

## 6.6 TRANSLATING TYPES

A type *t* is declared as follows in a CryptoVerif model:

1. type *t*.

A type can be declared with options *o*:

1. type *t* [*o*].

The most common options are fixed or bounded to indicate fixed-length bitstrings, or bitstrings with a maximum length; and large to indicate that the number of elements of this type is large enough such that the probability
that two randomly sampled elements collide is negligible. If two options are used, they are separated by a comma. For more options, we refer to the CryptoVerif manual that is available in the CryptoVerif download.<fnref n="6" />

### 6.6.1 Built-In and Fixed-Length Types

CryptoVerif has three built-in types that are prominently visible: `bitstring`, `bitstringbot`, and `bool`. A type that is not immediately visible as such is the one of replication indices. CryptoVerif uses positive integers which we translate to the built-in `nat` in $F^*$. CryptoVerif's `bool` is translated to $F^*$'s built-in type `bool`. CryptoVerif's `bitstring` is unbounded and we map it to HACL*'s bytes which is unbounded as well. It is defined in the module `Lib 字节序列`. An important kind of not-built-in types in CryptoVerif is the type of fixed-length bitstrings, annotated with the option `[fixed]` in type declarations. We mention it here already because it is translated in a pre-defined way, with limited choice by the author of the CryptoVerif model. Fixed types are translated to `lbytes len` from HACL*'s module `Lib 字节序列`, where `len` is the length of the bitstring in bytes, with a maximum of $max\_size\_nat = 2^{32} - 1$ bytes. This means fixed-length types are limited to this many bytes. This should be enough for any current practical purpose but is, in theory, a restriction compared to CryptoVerif's semantics where there is no such limit. The length is the only parameter that the CryptoVerif model author can choose for a fixed type. As an example, a fixed CryptoVerif type annotated with a size of 64 bits is translated to `lbytes 8`; this should explain why no name annotation is required for fixed types.

CryptoVerif's type `bitstringbot` differs from `bitstring` only in that it adds a failure symbol `bottom`. We translate it as option type `option bytes`, where `bottom` is constructed by `None` on the $F^*$ side, and a `bitstring b` by `Some b`.<fnref n="7" />

EQUALITY TEST FUNCTIONS FOR BUILT-IN TYPES. HACL*'s Lib. `ByteSequence` implements a constant-time equality test function `lbytes_eq` for `lbytes len`. We use it for CryptoVerif's fixed-length types, wrapped into a function named `eq_lbytes` for reasons of consistency with the remainder of the framework.

HACL* does not provide an equality test function for the unbounded type `bytes`. However, CryptoVerif does support equality tests on `bitstring`, and so we wrote our own equality test function `eq_bytes` for the type `bytes` that uses `lbytes_eq` internally for chunks smaller or equal to $max\_size\_nat$ in size. For bytestrings shorter or equal to $2^{32} - 1$ bytes, it directly falls back to `lbytes_eq`.

The equality test function `eq_obytes` for `bitstringbot` is straightforward and returns true either if both `bitstringbot` are `bottom` or if the bitstrings are equal. For `nat` and `bool`, we use $F^*$'s built-in operator for decidable equality (`=`) without wrapper.

CryptoVerif makes several assumptions about equality test functions. One of them is commutativity, and we discuss in Section 6.13 how we translate this as $F^*$ lemma and how we prove it.

<footnote n="6">⁶https://cryptoverif.inria.fr</footnote>

<footnote n="7">⁷An option type is a particular datatype, `sum type`, or `tagged union` predefined in $F^*$. The type `option a` with type `a` as parameter has two constructors: `None`, and `Some a`.</footnote>
For the pre-defined types we go further: We prove that `eq_bytes` and `eq_obytes` are equivalent to F*’s built-in operator for propositional equality (`==`) for all pairs of parameters (bytestrings and optional bytestrings). The operator (`==`) does not extract to executable code because propositional equality is undecidable in F*, it is only usable in logical statements.<fnref n="8" /> The interesting property for us is that it is an equivalence relation. Thus, by our proofs, we establish that `eq_bytes` and `eq_obytes` are equivalence relations, respectively.

### SERIALIZATION AND DESERIALIZATION OF BUILT-IN TYPES.
Generally, a serialization function in `cv2fstar` returns `bytes`, and a deserialization function takes `bytes` as input and returns an option type of the original type. It returns `None` if the input cannot be parsed as an instance of the original type.

Like any type, built-in types can be used within CryptoVerif tuples or as returned term of an oracle, and so we need to define serialization and deserialization functions for built-in types. The target type of serialization is the image of `bitstring`, which is `bytes`. For `bytes` itself, serialization is the identity function and so we do not spell it out explicitly in `CVTypes`. For `lbytes` `len`, serialization is a straightforward type cast to `bytes`. However, for deserialization, we require the expected length `len` of the resulting `lbytes` `len` as a parameter. We return `None` in case the length given as parameter and the actual length of the input `bytes` do not match. Apart from that, it is a straightforward type cast.

For the serialization of `bitstringbot` (option `bytes` in F*), we express `bottom` (`None`) as a null byte `0x00`, and any `bitstring` as the byte `0x01` concatenated with the actual `bitstring`.

For `nat`, we use HACL*’s serialization and deserialization functions `nat_to_bytes_be` and `nat_from_bytes_be` from `Lib 字节Sequence` which encode a `nat` as a big-endian byte sequence. The choice of big-endian is arbitrary but matches the usually used network encoding.

For `bool`, we chose a simple encoding of `false` as `0x00` and `true` as `0xFF`. One bit would be enough, however, the smallest unit of HACL*’s `bytes` is one byte, as `bytes` is implemented as a sequence of bytes. For the sake of not increasing the complexity of the framework, we did not strive for a more efficient serialization of `bool`. As an optimization for future work, the target for serialization could be made a type of bitstrings, based on the `uint1` type instead of the `uint8` type underlying `bytes`.

We prove two correctness lemmas for each pair of `(de) serialization` functions. It is the same kind of lemmas that `cv2fstar` generates as proof obligation for user-defined types that have serialization and deserialization functions. This is described in more detail in Section 6.13.

### PRINTING HELPER FUNCTIONS OF BUILT-IN TYPES.
As helper functions for debugging purposes, we define printing functions for the built-in types, and most importantly for `bytes`. The `print` function for `bytes` is used for printing of user-defined types via the type’s serialization function. This way, the user is only required to implement serialization (and deserialization) and gets printing helpers for free. The `print` function for `bytes` prints a hexadecimal

<footnote n="8">⁸For more details on this, see https://www.fstar-lang.org/tutorial/book/part1/part1_polymorphism.html#equality</footnote>
<caption>Listing 6.1: Interface for entropy in the cv2fstar framework, as defined in CVTypes.fsti.</caption>

```h
1 val entropy: Type0
2
3 val initialize_entropy: Lib.RandomSequence.entropy -> entropy
4 val finalize_entropy: entropy -> Lib.RandomSequence.entropy
5
6 val gen_nat: max: nat{max > 0} -> entropy
7     -> entropy * n: nat{n ≤ max}
8 val gen_lbytes: l: Lib.IntTypes.size_nat -> entropy
9     -> entropy * lbytes l
```

representation of a given bytestring.

### ENTROPY, AND RANDOM SAMPLING FOR BUILT-IN TYPES.
In `cv2fstar`, all functions are pure by design, i. e., they terminate and are in particular without side effects. If a function needs to randomly sample a value, we need to explicitly pass the randomness or at least some representation of entropy to it. In `CryptoVerif`, random sampling can be done in terms with the `<-R` syntax, and it is done implicitly when multiple entries match a table get query, to (almost) uniformly random choose one of the matches.

For `cv2fstar`, we decided to go for an entropy-passing style as follows: At the initialization of the framework, some initial entropy must be passed to the framework. The framework keeps the entropy value and passes it to each function that does random sampling. Such a function internally takes some entropy from the entropy pool, and returns the new state of the entropy pool along with the actual result of the function. The `cv2fstar` framework provides functions for random sampling of built-in types that work this way – they take entropy as parameter, and return entropy and a randomly sampled value. This style avoids side effects and gives us a pure specification. We will discuss in a moment that the actual implementation is not necessarily free from side effects.

There are two layers that we describe in the following. First, we discuss the interface defined for entropy in `cv2fstar`'s module `CVTypes.fsti`. It defines entropy as an abstract type. Second, we explain the implementation of entropy in `CVTypes.fst`, which instantiates entropy and random sampling with specific algorithms. As with all well-designed abstractions, this allows us to replace the implementation of random sampling later, without touching the rest of the framework. We will discuss related future work at the end of this section.

Listing 6.1 shows how the interface of entropy and random sampling is defined in `CVTypes.fsti`. Line 1 shows the definition of entropy as an abstract type. For this first version of `cv2fstar`, we decided to require the entropy variable to be initialised once at the beginning when the framework is set up. The function used for this is shown in Line 3. It takes a value of a specific type of entropy as parameter, and returns the framework's abstract entropy type – which might or might not be the same type, depending on the implementation. This specific type of entropy is HACL*'s entropy as defined in the module `Lib.RandomSequence`. At the end of execution of the framework, the `finalize_entropy` function (Line 4) can be called to
retrieve the new value of the HACL\* type of entropy, to close the circuit.

CryptoVerif samples almost uniformly random integers to choose a table entry among multiple query matches. We define `gen_nat` to support this on the F\* side (Line 7). The function takes a `nat` parameter to define the interval $[0, m]$ in which to sample the integer.

There is no random sampling for `bitstring` in CryptoVerif because this type is unbounded. CryptoVerif allows random sampling for types that are annotated with `[bounded]` or `[fixed]`. `cv2fstar` currently supports random sampling for fixed types with `gen_lbytes` (Line 9). This function takes the desired length in bytes as parameter.

The implementation of the type `entropy` and of the functions `initialize_entropy`, `finalize_entropy`, `gen_nat`, and `gen_lbytes` is outsourced to the `cv2fstar` module `RandomHelper`. Its interface defines the same type and functions. We discuss the implementation in the following.

```
1 noeq type entropy =
2   | Entropy : system_entropy: Lib.RandomSequence.entropy -> entropy
3
4 let initialize_entropy ent =
5   Entropy ent
6
7 let finalize_entropy ent =
8   let Entropy entropy = ent in
9   entropy
```

In Line 2, we define entropy as a type with a single constructor `Entropy` that takes a value of HACL\*'s entropy type as parameter.<fnref n="9" /> Initialization simply creates an instance of entropy with the entropy value passed to it, and finalization unwraps and returns it. Here, it becomes clear that in our current implementation, we just use the same entropy type internally.

For the actual random sampling, we use the `crypto_random` function from HACL\*'s `Lib.RandomSequence` module. It is the only module for random sampling that HACL\* offers for the pure world of specifications written in F\*.<fnref n="10" /> Only the *interface* of `Lib.RandomSequence` is written in F\*:

```
1 val entropy: Type0
2 val entropy0: entropy
3 val crypto_random: entropy -> len=size_nat-> entropy * lbytes len
```

The implementation in a directly executable language has to be linked after extraction of the F\* code. As we extract our case study's code to OCaml for execution, we briefly look at the OCaml implementation: It instantiates entropy as an OCaml integer and uses `0` as initial value. The function `crypto_random` internally uses the OCaml crypto library Cryptokit's function `Random.hardware_rng` that uses the RDRAND CPU instruction to get random bytes<fnref n="11" />. As new entropy value, it always returns `0`. At this point it becomes clear that the entropy-passing style is of merely philosophical interest when using such an implementation as backend. However, the interface defined by `Lib.RandomSequence` is also not giving any information about how the two entropy values relate, and how the returned randomness relates to them. Concluding this brief look to the low-level implementation of HACL\*'s `crypto_random`, we now look at how we use it to sample random bitstrings of fixed length.

<footnote n="9">⁹The keyword `noeq` prevents F\* from generating the decidable equality operator (`=`) for this type, which would otherwise fail with an error.</footnote>

<footnote n="10">¹⁰For efficient implementations in `Low\*`, there is the library `Lib.RandomBuffer`. `System` for random sampling.</footnote>

<footnote n="11">¹¹This code can be found in the file `lib/ml/Lib_RandomSequence.ml` in HACL\*.</footnote>
The implementation of `gen_lbytes` is straightforward, see Listing 6.2: We wrap the entropy value, and then call `crypto_random` with it and the desired length of the bitstring. We construct the new entropy value and return it along the random bitstring.

<caption>Listing 6.2: Implementation of random sampling for fixed-length bitstrings.</caption>

1. `let gen_lbytes num ent =`
2. `let Entropy entropy = ent in`
3. `let entropy, bytes = crypto_random entropy num in`
4. `Entropy entropy, bytes`

Randomly sampling a natural number within an interval $[0, m]$ is more involved, given that we only have `crypto_random` which generates a bytestring of length at most `max_size nat`: First, we need to generate an almost uniformly random natural number from a uniformly random bytestring. Second, we need to support this for an arbitrary large $m$. The second problem is of course mostly a problem of theoretical interest, because most practical systems will not have table queries that match this many entries. We implement the function `crypto_random_unbounded` to solve this – a variant of `crypto_random` that takes a natural number $n$ as parameter and that calls `crypto_random` internally as often as necessary to produce a bytestring of length $n$. In the implementation of `gen nat`, we first compute the minimum number of bytes $n'$ necessary to represent the upper inclusive bound $m$ of the interval:

$$n' = \left\lceil \frac{1 + \log_2 m}{8} \right\rceil.$$

We then add an accuracy parameter $k$ to it to compute the number of random bytes $n$ that we are going to sample:

$$n = n' + k.$$

A higher value for $k$ reduces the skew in the almost uniform distribution. We use `crypto_random_unbounded` to generate $n$ random bytes, and transform them to a natural number $r$ using a built-in HACL* function. Finally, we compute the almost uniformly random number in $[0, m]$ by computing $r \mod (m+1)$. The parameter $k$ is configurable in `cv2fstar`'s code, we set it to 10 for our case study.

Concerning future work on random sampling, we plan to replace the use of `crypto_random`. Currently, we use the hardware random number generator for each random byte. This is less efficient than using a cryptographically secure pseudo-random number generator (CSPRNG) and seeding it in reasonable intervals from the hardware random number generator, or any other high-quality entropy pool offered by the operating system. As a teaser, with the methodology presented above, the implementation of the entropy could look like this, because we need to keep the state of the CSPRNG:

1. `noeq type entropy =`
2. `| Entropy :`
3. `system_entropy: Lib.RandomSequence.entropy`
4. `-> Spec.HMAC_DRBG.state Spec.Agile.Hash.SHA2_512`
5. `-> entropy`
The CSPRNG HMAC-DRBG is implemented in HACL\*, and it is parametrized by a hash function. We would initialize this state within `initialize_entropy` and reseed it from the system's entropy pool whenever necessary. Here, the entropy type's constructor takes two parameters, and it becomes clearer why the use of an explicit constructor makes code more readable: in contrast to simply using a tuple of two elements (e. g. `(a, b)`), the explicit constructor makes it clear from reading alone that we are dealing with entropy (e. g. `Entropy a b`).

### 6.6.2 Other Types

Now that the treatment of built-in and fixed types has been described, we look at how other, user-defined types are translated. `cv2fstar` only translates type declarations for them, and if required and indicated by annotations, declarations of equality test, serialization and deserialization, and random sampling functions. For a type `t`, the following code is generated in `M Types.fsti`:

1. `val G_t(t): Type0`

2. `val G eq (t): G t (t) → G t (t) → bool`

3. `val G ser (t): G t (t) → bytes`

4. `val G deser (t): bytes → option (G t (t))`

5. `val G s (t): entropy → entropy * G t (t)`

The user needs to write a file `M Types.fst` with appropriate implementations of the type and its functions.

## 6.7 TRANSLATING FUNCTIONS AND CONSTANTS

**CONSTANTS.** A constant `c` of type `t` is declared as follows in a CryptoVerif model:

1. `const c: t.`

This declaration is translated in `M Functions.fsti` as follows:

1. `val G_c(c): G_t(t)`

**FUNCTIONS.** A function `f` with parameters of types `t_i`, `1 ≤ i ≤ n` and return type `t` is declared as follows in a CryptoVerif model:

1. `fun f(t_1, ..., t_n): t.`

The optional `[data]` keyword to indicate that `f` has an efficiently computable inverse can be added at the end:

1. `fun f(t_1, ..., t_n): t [data].`

The function declaration in F\* is generated in the following way:

1. `val G_f(f): G_t(t_1) ... → G_t(t_n) → G_t(t)`

If the function is declared `[data]`, and the inverse of the function is used in the model, an additional function declaration for the inverse is generated:

1. `val G inv (f): G_t(t) → option (G_t(t_1) ... * ... * G_t(t_n))`

The return type is an option type because not each element of type `t` might be invertible, i. e., not each element of type `t` might be in the image of `f`.
## 6.8 THE STATE TYPE

In Section 6.6, we introduced entropy as a kind of state of which the `cv2fstar` framework keeps track during its execution. In the following sections, we introduce other kinds of such state. Entropy is generic and not specific to a CryptoVerif model. There are three data types that are specific to a CryptoVerif model and important for the state of the execution: tables, events, and sessions. We introduce them step by step in Section 6.9 (tables), Section 6.10 (events), and Section 6.12 (sessions). What we want to say already now is that we group these three data types into a polymorphic `state_type`. It looks as follows, where we use the data types that we introduce later:

```
1 noeq type state_type =
2 | StateType :
3    tt: table_type
4    → st: session_type
5    → event_type: Type0
6    → state_type
```

We define getters `tt_of`, `st_of`, and `et_of` to access the individual data types of tables, sessions, and events, given a `state_type`. The `cv2fstar` compiler generates code to instantiate `state_type` for a CryptoVerif model, as described in the following sections.

With this, we define a polymorphic type `state` that is parametrized by a `state_type`. An instance of this type holds the state for each of the three model-specific data types (tables, sessions, events), and for the entropy pool:

```
1 noeq type state (stt: state_type) =
2 | State :
3    ent: entropy →
4    tabs: tables (tt_of stt) →
5    sess: sessions (st_of stt) →
6    evs: list (et_of stt)
7    → state stt
```

Internally, the framework provides getters and setters for the state's fields as helper functions.<fnref n="12" /> The getters are called `entropy_of`, `tables_of`, `sessions_of`, and `events_of`, and take a `state` as parameter. The setters are called `state_updTOTP`, `state_upd_tables`, `state_upd_sessions`, and `state_upd_events`. They take a `state` and a new entropy, `tables`, `sessions`, or `events` object as parameter, and return a new `state` with the appropriate field replaced by the new object, and the other fields unchanged.

The framework's idea concerning the state is that the *outside* interface does not allow direct manipulation of state fields. Changes are only possible via functions exposed in `State.fsti`. This way, on the one hand, we hide the implementation details of the state's components, and on the other hand, we control what changes can be made, and can ensure that they are sound.

In Section 6.6, we introduced our handling of entropy and random sampling. An important function exposed by the framework in this context is `call_withTOTP`. We use it as a wrapper to provide functions with entropy. The function `call_withTOTP` takes two parameters: the `state`, and a function to be wrapped. This function must take entropy as input and return a pair of entropy and some other return value. The output of

<footnote n="12">¹²In this case, internally means, that they are not exposed in the interface `State.fsti` but are only present in `State.fst`.</footnote>
`call_with_entropy` is a new state and the return value of the wrapped function. The interface is as follows:

1. `val call_with_entropy:`
2. `#stt: state_type →`
3. `#a: Type→`
4. `st0: state stt →`
5. `(entropy → entropy * a)`
6. `→ state stt * a`

The function has two implicit parameters, marked with `#`, the state type and the return type of the wrapped function. In most cases, `F*` should be able to infer them from the next two parameters, the state and the wrapped function. Then, it is not necessary to provide the implicit parameters. This function is also a good example for a dependent type: Its return type `state stt * a` depends on the parameter `stt`. The implementation of the function is as follows:

1. `let call_with_entropy st0 f =`
2. `let ent0 = entropy_of st0 in`
3. `let ent1, res = f ent0 in`
4. `let stl = state_updates_entropy st0 ent1 in`
5. `stl, res`

This wrapper is used for any random sampling with `gen_nat` and `gen_lbytes`.

## 6.9 TRANSLATING TABLES

As a start, a quick recap about tables in CryptoVerif. In a CryptoVerif model, tables are declared using

1. `table tbl(t₁, ..., tₙ)`.

where `tbl` is the table name and `t₁` to `tₙ` are the types of an entry's fields. In a process, entries can be added to a table by a term

1. `insert tbl(M₁, ..., Mₙ); M`

where `M₁` to `Mₙ` must be terms with types matching the types of the table declaration. A table insert always succeeds in CryptoVerif, so there is no branching, and only one next term `M` that is evaluated. Entries cannot be removed from tables.

A table is queried by a term

1. `get tbl(p₁, ..., pₙ) suchthat M in M' else M''`

where `p₁` to `pₙ` are patterns. The query tries to find an entry with fields matching the patterns such that the term `M` is true. If exactly one matching entry is found, the term evaluates to the result of `M'`. If more than one matching entries are found, one among them is chosen almost uniformly random, and the term evaluates to the result of `M'`. Otherwise, it evaluates to the result of `M''`. The keyword `[unique]` can be added directly after `get` to make it `[unique]`. Then, CryptoVerif tries to prove that there is only ever at most one matching table entry for this query, up to negligible probability.

In the following, we describe by which types CryptoVerif tables are expressed in the `cv2fstar` framework. Then, we line out how `insert` and the different variants of `get` are implemented. As a motivational overview, let us discuss what we need for tables. We want to identify tables by their name,
<table><caption>TABLE 6.1: Common abbreviations used in the cv2fstar framework.</caption><thead><tr><td>Abbreviation</td><td>Meaning</td></tr></thead><tbody><tr><td>tt</td><td>table type</td></tr><tr><td>tn</td><td>table name</td></tr><tr><td>tns</td><td>table names</td></tr><tr><td>te</td><td>table entry</td></tr><tr><td>tft</td><td>table filter type</td></tr><tr><td>rt</td><td>return type</td></tr><tr><td>st</td><td>session type</td></tr><tr><td>se</td><td>session entry</td></tr><tr><td>on</td><td>oracle name</td></tr><tr><td>et</td><td>event type</td></tr></tbody></table>

as in CryptoVerif; for each table, we need a data structure containing the entries, and also a data type for the tables's entries.

We begin with a generic type for tables, `table_type`. It has one constructor, parametrized by two values: a type meant to enumerate table names, and a function type meant to map a table's name to the type of its entries.

```
1 noeq type table_type =
2 | TableType :
3 tn: eqtype (* table names *) →
4 te: (tn → Type0) (* table entries *) → table_type
```

We define two getters: `table_name` to retrieve the type enumerating table names, and `table_entry` to retrieve the type of a table's entries, given a `table_type`.

We introduce a polymorphic type `table`, parametrized by a table type and a table name. A `table` is implemented as a sequence of table entries of the appropriate type:

```
1 type table (#tt: table_type) (tn: table_name tt) =
2 Seq.seq (table_entry #tt tn)
```

We group all tables of a model in a type `tables` parametrized by the table type. We use a function-type mapping from table name to a table:<fnref n="13" />

```
1 type tables (tt: table_type) = tn: table_name tt → table #tt tn
```

For the initialisation of the framework, we provide a function `init_tables` that constructs an empty instance of `tables` for a given table type: it returns a function that maps each table name to the empty sequence. Eventually, we want to implement a functionality to write tables to disk and to read them from disk to allow for persistence. In this first version of `cv2fstar`, the framework always starts with empty tables. The implementation of the types `table_type`, `table_name`, and `table_entry` is model-specific; we will discuss the NSL example in Section 6.15.

We now describe the implementation of `insert` and `get`. Beginning with `insert`: it takes a state, a table name, and a table entry to be added to the table as parameters, and returns a new state with the `tables` field updated accordingly. The function declaration is as follows:

<footnote n="13">¹³This could be implemented more efficiently with a record, as the set of tables in a model is fixed. We scheduled this change for immediate future work.</footnote>
1 val insert:
2   #stt: state_type →
3   st0: state stt →
4   tn: table_name (tt_of stt) →
5   table_entry #(tt_of stt) tn
6   → state stt

The matching condition of a CryptoVerif get query consists of the patterns (one for each field), and an additional condition after the suchthat keyword. In cv2fstar, we express these by one filter function that is provided as a parameter to get and its variants. The filter function is called on each table entry, checks if this particular entry matches, and if yes, returns the values of the variables bound by the patterns. In its simple form, a filter function has the following type:

1   #stt: state_type →
2   rt: Type0 → (* rt for return type *)
3   #tn: table_name (tt_of stt) →
4   table_entry #(tt_of stt) tn
5   → option rt

In this simple form, the filter function does not have access to the state. However, CryptoVerif's semantics allows terms in get patterns and conditions to access state: It is possible to have random sampling or other get queries inside get conditions. For random sampling, read and write access to entropy is needed, and for get, it is read access to tables (and get might also need read and write access to entropy).<fnref n="14" /> Therefore, we need a full form for filter functions that takes state as parameter and returns a new state alongside the result option type. The reason for the separation in a simple and full form is simplification of the generated F\* code for the majority of cases: Most CryptoVerif models will not do random sampling or other get queries inside the conditions of get.

We formalize these two types of filters as follows. We have a type to enumerate the two possibilities

1 type table_filter_type =
2   | TableFilterSimple
3   | TableFilterFull

Then, we have a type table_filter that assigns each type the interface of the appropriate filter function. The interesting lines in the following listing are Line 9 and Lines 11 and 12. They define that the simple case only takes a table entry and returns a result, and the full case additionally passes state through.

1 let table_filter
2   (#stt: state_type)
3   (tft: table_filter_type)
4   (rt: Type0)
5   (tn: table_name (tt_of stt))
6 =
7 match tft with
8   | TableFilterSimple →
9   (table_entry #(tt_of stt) tn → option rt)
10  | TableFilterFull →
11  (st0: state stt → table_entry #(tt_of stt) tn
12  → state stt * option rt)

<footnote n="14">¹⁴The terminology *read and write access* might be confusing here, as state is not a global variable to which functions could write. In our case, a function having write access to entropy or state means that it returns a new entropy or state value that must be used subsequently by the caller.</footnote>
Besides `get` and `get[unique]`, we are introducing a third variant for convenience, like `cv2ocaml` did. It does not exist as such in CryptoVerif, but serves to simplify the generated F\* code. In cases where no values retrieved from the table are actually used within the following terms, `get` and `get[unique]` are just a check if matching entries exist. This is simply a boolean result and so we add an `entry_exists` variant in `cv2fstar`.

The interfaces of the functions implementing the various variants of `get` are similar, so we look at the one for `get` in detail, and discuss only the differences for the others. The non-unique `get` might find multiple matching entries and thus needs read and write access to entropy and thus the state, independently of if the filter function needs write access to state. Thus, we provide only one implementation for the non-unique `get` that always returns a new state. It is parametrized by a table filter type to accomodate for the simple and the full case:

```
1 val get:
2   #stt: state_type →
3   #tft: table_filter_type →
4   #rt: Type0 →
5   st0: state stt →
6   tn: table_name (tt_of stt) →
7   table_filter #stt tft rt tn
8   → state stt * option rt
```

The unique variant of `get` does not always need write access to the state, only the full variant does.<fnref n="15" /> Thus, we have a function `get_unique_full` that differs from `get` only in that it does not take a table filter type as implicit parameter (so we omit Line 3) and that the table filter is always of type `TableFilterFull` (in Line 7). A `get[unique]` query with a simple filter does not use randomness, and thus does not need entropy: for the function `get_unique`, the table filter is hard-coded to a `TableFilterSimple` one, and the return type is only an `option rt`; no new state is returned. For the existence variant of `get`, we provide `entry_exists_full` and `entry_exists` that differ from `get_unique_full` and `get_unique` in that they return `state stt * bool` and `bool`, respectively.

The implementation of `get` iterates recursively through the table entries and accumulates matches, passing the state through the filter function appropriately. If there is more than one match, an almost uniformly random integer in `[0, m)` is sampled using `gen_nat`, where *m* is the number of matches, to choose an entry. The unique variant can stop iterating after the first match is found, as it has been proved by CryptoVerif that it is not possible to have multiple matches. The existence variants of `get` can equally stop iterating after the first successful match.

This concludes the description of the handwritten part of the `cv2fstar` framework concerning tables. The `cv2fstar` compiler generates code for a model's instantiation of the table name and table entry types. We will discuss this by example in Section 6.15.3.

## 6.10 TRANSLATING EVENTS

Events are not translated by `cv2ocaml`; this constitutes an entirely new development in `cv2fstar`. In a CryptoVerif model, an event can be declared

<footnote n="15">¹⁵They always need read access because they read tables, so all `cv2fstar` functions implementing `get` variants take state as parameter.</footnote>
by

1 event e(t₁, ..., tₙ).

where e is the name of the event, and t₁ to tₙ are the types of its parameters.
An event is invoked by a term

1 event e(M₁, ..., Mₙ); M

where e is the name of an event that has been declared in the model, and
M₁ to Mₙ are terms with types matching the event's declaration. An event
does not fail, so there is no branching, and the return value of the term is
the evaluation of the following term M.

In Section 6.8, we introduced the state_type, containing the event_type,
and defined that the state contains a list of values of this type. The frame-
work provides a function for appending an event to the event list: The
function state_add_event takes the state and an event as parameter, and
returns a new state with this event added to the list of events, using the
state_updates function.

The cv2fstar compiler generates a model-specific events type, which will
be described in Section 6.15.6. Events are important in correspondence
queries. cv2fstar is not yet translating these queries, this is left for future
work.

6.11 TRANSLATING TERMS

In the previous sections, we discussed single building blocks and their trans-
lation: types, randomness, tables, and events. The next step, in this section,
are terms. Terms are a building block on our way to translate processes
(oracles). However, on the way, translating terms is already enough to trans-
late letfun s. In CryptoVerif, a letfun is nothing else than a term separated
into a named function. During a proof, CryptoVerif inlines letfun s imme-
diately for the first game transformation such that they will not be visible
anymore as separate functions in any game. For cv2fstar, we decided to keep
them separate as a way to structure the code and to avoid code duplication.
cv2fstar generates an interface M.Letfun s.fst i and an implementation
M.Letfun s.fst for a model M's letfun s. We discuss specifics at the end of
this section. Before, we describe several aspects of the translation of terms.

A major difference to cv2ocaml is that cv2fstar uses a state-passing style to keep track of the execution state. This complicates the translation of terms, because each term possibly becomes a pair: it has *two* important return values instead of only one; the actual return value, *and* a new state. Although, not all terms in CryptoVerif touch the state, so some optimization is possible to keep the generated F\* code readable. Indeed, in our implementation of the cv2fstar compiler inside CryptoVerif, we generate code for (state, value) tuples only if a term needs state. However, in this section, to keep the presentation simple, we explain the translation of terms as if all terms needed state and would possibly change it. This means that in the following, all terms produce a new state.

We denote by $\mathbb{G}_M(M)$ the function that produces the $F^*$ code translating a CryptoVerif term $M$. In the following, we define $\mathbb{G}_M(M)$ step by step for the different kinds of terms.
VARIABLE NAMES, $G_M(x)$. A variable term $x$ is translated as follows:

1. $G_M(x) =$

2. state, $G_{var}(x)$

where $G_{var}(x)$ is a function taking a CryptoVerif variable name and returning an $F^*$ variable name. We use a prefix `var_` and an encoding such that this function is injective, to avoid collisions with other functions that generate names.

CONSTANTS. Constants are translated to their annotated name:

1. $G_M(c) =$

2. state, $G_{const}(c)$

At first sight, it might appear wrong that variables and constants are translated as pairs. However, in the following, it will become clear that before using any term, the pair of state and value is always decomposed.

TUPLES. In CryptoVerif, tuples are constructed by wrapping multiple terms into parentheses, separated by commas, like in this example: `(a, b, c)`. Tuples are of type `bitstring`. When translating a tuple, we feed each element through the serialization function of its type and concatenate the resulting byte sequences. Each element of the tuple might process state, so we first chain the preparation of each individual element. For terms $M_i$ of types $t_i$, $1 \le i \le n$, we generate the following code:

1. $G_M((M_1, \dots, M_n)) =$

2. let state, $v_1 = G_M(M_1)$ in

3. ...

4. let state, $v_n = G_M(M_n)$ in

5. state, compos $[G_{ser}(t_1) v_1; \dots; G_{ser}(t_n) v_n]$

The function `compos` takes a list of byte sequences as input. It uses a 4-byte prefix to encode the number of tuple elements, and a 4-byte prefix in front of each element to encode its length. This makes tuple composition limited to terms that result in a serialization with a maximum length of $2^{32}-1$ bytes. For longer strings, the tuple composition function will instead return an error symbol. This is another practical limitation of `cv2fstar` that could be pushed further if need be.

FUNCTION CALLS WITHOUT ENTROPY. Function calls are generated with the function name from the implementation annotations. As previously, each parameter is translated using $G_M$. For a function $f$, and terms $M_i$, $1 \le i \le n$, we generate:

1. $G_M(f(M_1, \dots, M_n)) =$

2. let state, $v_1 = G_M(M_1)$ in

3. ...

4. let state, $v_n = G_M(M_n)$ in

5. state, $G_f(f) v_1 \dots v_n$

FUNCTION CALLS WITH ENTROPY. If a function $f$ needs entropy because it internally samples random values, we wrap it with `call_with_entropy`. This function is already of the form that it returns a tuple of state and a value, so we do not need an explicit `state` in the last line.
1 $\mathbb{G}_M(f(M_1, \dots, M_n)) =$

2 let state, $v_1 = \mathbb{G}_M(M_1)$ in

3 ...

4 let state, $v_n = \mathbb{G}_M(M_n)$ in

5 call_with_entropy state $(\mathbb{G}_f(f) v_1 \dots v_n)$

For simplicity, we use the same variable names $v_1$ to $v_n$ in this and the other listings; in the actual implementation of the compiler, we use unique names. The function $f$ is required to take entropy as last parameter such that $(\mathbb{G}_f(f) v_1 \dots v_n)$ results in a function with only entropy as parameter.

In Section 6.4, we mentioned that it is possible to provide an annotation for a CryptoVerif letfun such that it is implemented by a function, hiding the CryptoVerif body of the letfun. In this case, the letfun is treated as a non-letfun function and translated as described here, as a function call with or without entropy. The following paragraph describes letfun function calls where the letfun is translated with its body as it is.

**LETFUN FUNCTION CALLS.** Letfun calls are translated to a function call of the appropriate function in the $M$. Letfun module. The generation of this module is described at the end of this section. We are again assuming that each letfun processes state and returns a pair. In the actual implementation, we optimise the case in which a letfun does not process state. For a letfun call that has the terms $M_i$, $1 \le i \le n$ as parameters, we generate:

1 $\mathbb{G}_M(\text{letfun}(M_1, \dots, M_n)) =$

2 let state, $v_1 = \mathbb{G}_M(M_1)$ in

3 ...

4 let state, $v_n = \mathbb{G}_M(M_n)$ in

5 $M$.Letfun.fun_letfun state $v_1 \dots v_n$

The $F^*$ function name of a letfun is its CryptoVerif name prefixed with `fun_`.

**EQUALITY TEST.** For an equality test $M_1 = M_2$, or its negation $M_1 \langle\rangle M_2$, CryptoVerif already ensures that $M_1$ and $M_2$ have the same type $t$. An equality test is translated to a function call as indicated by the implementation annotation of the type $t$:

1 $\mathbb{G}_M(M_1 = M_2) =$

2 let state, $v_1 = \mathbb{G}_M(M_1)$ in

3 let state, $v_2 = \mathbb{G}_M(M_2)$ in

4 state, $\mathbb{G}_{eq}(t) v_1 v_2$

The syntax `<>` from CryptoVerif is translated to the negation of the equality test function of type $t$:

1 $\mathbb{G}_M(M_1 \langle\rangle M_2) =$

2 let state, $v_1 = \mathbb{G}_M(M_1)$ in

3 let state, $v_2 = \mathbb{G}_M(M_2)$ in

4 state, not $(\mathbb{G}_{eq}(t_1) v_1 v_2)$

**IF CONDITIONALS.** The translation of an `if` condition is as follows, for a boolean term $M$, and branches $M'$ and $M''$:

1 $\mathbb{G}_M(\text{if } M \text{ then } M' \text{ else } M'') =$

2 let state, $v = \mathbb{G}_M(M)$ in

3 if $v$ then $\mathbb{G}_M(M')$ else $\mathbb{G}_M(M'')$
## RANDOM SAMPLING.
For a type `t` that allows random sampling, and a following term `M`, we generate the following code:

1. $G_M(x < R t; M) =$

2. `let state, $G_{var}(x) = call_with-probability state G_S(t)$ in`

3. `$G_M(M)$`

## EVENTS.
For an event `e` with parameters $M_i$, $1 \le i \le n$ and a following term `M`, we generate the following code:

1. $G_M(\text{event } e(M_1, \dots, M_n); M) =$

2. `let state, $v_1 = G_{M'}(M_1)$ in`

3. ...

4. `let state, $v_n = G_{M'}(M_n)$ in`

5. `let ev = Event_e v_1 ... v_n in`

6. `let state = state_add_event state ev in`

7. `$G_M(M)$`

Here, $G_{M'}$ is a slightly adapted version of $G_M$ that translates replication indices if they occur in a particular way in the parameters of the event: if the oracle in which the event occurs is under multiple nested replications, the replication indices of all levels must be used within a tuple in the right order, from the innermost to the outermost replication index; if the oracle is under only one replication, the replication index must be used directly; in both cases, this has to be directly as a parameter of the event, not nested inside other terms inside a parameter, e. g., function calls. For example, for an event inside of two nested replications, the following event invocation is supported by `cv2fstar`:

1. `foreach i1 \le Q1 do`

2. ...

3. `foreach i2 \le Q2 do`

4. ...

5. `event e1((i2, i1), ...);`

6. ...

The first parameter of the event `e1` has to be declared as type bitstring. For event `e2` in the following example, inside of only one replication, the type of `e2`'s first parameter must be the replication parameter, in this case `Q1`.

1. `foreach i1 \le Q1 do`

2. ...

3. `event e2(i1, ...);`

4. ...

If these conditions are met, we translate a tuple of replication indices as `( serializes nat sid) because the event's parameter expects a bytes value, and a single replication index as `sid` because the event's parameter expects a nat value. As we describe in detail in the next section, the variable `sid` of type `nat` always contains a current session ID that reflects all replications.

## LET BINDINGS.
The most interesting translation might be the one of `let` bindings, because it includes pattern matching. A pattern matching in `CryptoVerif` generally has the following form:

1. `let PAT = M in M' else M''`

where `PAT` is the pattern, `M` is the term that is being matched to the pattern, $M'$ is the term evaluated in case of success of the pattern matching, and $M''$ is the term evaluated otherwise.
Pattern matching can be split into three cases for PAT: a single variable assignment, a single equality pattern, and finally everything more complex than that. We go through them one by one.

A single variable assignment is translated as such to F\*, it always succeeds and thus, it has no else branch M'':

1. $G_M(\text{let } x = M \text{ in } M') =$

2. $\text{let } \mathit{state}, v = G_M(M) \text{ in}$

3. $\text{let } G_{\mathit{var}}(x) = v \text{ in}$

4. $G_M(M')$

A single equality pattern is translated to an if condition in F\*. The generic case looks like this, with a term $M_1$ of type $t_1$:

1. $\text{let } (=M_1) = M \text{ in } M' \text{ else } M''$

The condition in F\* uses the equality test function of this type. The semantics of CryptoVerif defines that M is evaluated first, and then $M_1$.

1. $G_M(\text{let } (=M_1)=M \text{ in } M' \text{ else } M'') =$

2. $\text{let } \mathit{state}, v = G_M(M) \text{ in}$

3. $\text{let } \mathit{state}, w = G_M(M_1) \text{ in}$

4. $\text{if } G_{\mathit{eq}}(t_1) \text{ v w then } G_M(M') \text{ else } G_M(M'')$

Finally, we look at a more complex pattern with one or more variable assignments and equality patterns, and one ore more function inversions or tuple decompositions, possibly nested. The generic algorithm for this is quite involved, so we describe it only on a high level, and based on an example that contains all the kinds of patterns listed above.

On a high level, when translating a complex pattern, we go through it inwards, starting from the outermost layer. We collect variable assignments, equality patterns, and inversions (function inversions or tuple decomposition). Then, we first generate code for the inversions. Generally, for all failure cases, we generate the code for the else case of the pattern matching, $M''$. After the success case of an inversion, we pass through the variable names of assignments at that layer and continue with the next inversion. After all inversions are done, we translate the equality patterns as an if condition, combining multiple ones with &&. The success case continues with the translation of $M'$, the else case again with $M''$.

Let us look at the example that we are using to showcase the translation algorithm:

1. $\text{let } (=M_1, b: t_2, f(c: t_4, =M_5)) = M \text{ in } M' \text{ else } M''$

On the outermost layer, the pattern is a tuple of three elements. The first one is an equality pattern, and we suppose that the term $M_1$ has type $t_1$. The second one is an assignment to a variable $b$ of type $t_2$. The third one is an application of the function $f$, which must have been declared `[data]` to have an efficiently computable inverse $f^{-1}$. We suppose that $f$ returns a value of type $t_3$. Inside of the function $f$, we have an assignment to a variable $c$ of type $t_4$, and an equality pattern with term $M_5$ of supposed type $t_5$.

Moving on to the code that `cv2fstar` generates for this example. First, the terms $M, M_1$ and $M_5$ need to be processed in the right order. The semantics of CryptoVerif defines that $M$ is evaluated first, and then the terms of the equality patterns $M_1$ and $M_5$:
<caption>Listing 6.3: F\* code generated by cv2fstar for the pattern matching example.</caption>

1 let state, v = G<sub>M</sub>(M) in
2 let state, v<sub>1</sub> = G<sub>M</sub>(M<sub>1</sub>) in
3 let state, v<sub>5</sub> = G<sub>M</sub>(M<sub>5</sub>) in

The next step is the decomposition of the tuple. We use a function decompos of our framework that takes a byte sequence and decomposes it into its parts according to the format used by compos: a first 4-byte prefix encodes the number of parts, and each part is prefixed by 4 bytes encoding its length. If there is an inconsistency with the prefixes, decompos returns None (Line 9 in Listing 6.4), otherwise it returns a list Some [c<sub>1</sub>,...,c<sub>n</sub>], where c<sub>1</sub>,...,c<sub>n</sub> are the byte sequences representing the tuple's elements (Line 5). We then apply the deserialization functions of the appropriate types

<caption>Listing 6.4: Continuation: F\* code generated by cv2fstar for the pattern matching example.</caption>

4 match (λ n₁ → match decompos n₁ with
5 | Some [c₁; c₂; c₃] →
6 (match (G<sub>deser</sub>(t₁) c₁, G<sub>deser</sub>(t₂) c₂, G<sub>deser</sub>(t₃) c₃) with
7 | (Some r₁, Some r₂, Some r₃) → Some (r₁, r₂, r₃)
8 | _ → None)
9 | _ → None) v with
10 | None → G<sub>M</sub>(M'')
11 | Some (r₁, G<sub>var</sub>(b), r₃) →

to these byte sequences (Line 6). If all deserializations succeed, we return the values; otherwise we return None (Lines 7 and 8). For the case that the decomposition of the tuple failed overall (None in Line 10), we generate the code for term M''. If it succeeds, we carry on with the next patterns, and pass on a variable for each element of the tuple that was just decomposed (Line 11). As the second tuple element is a variable assignment, we use the variable's name G<sub>var</sub>(b). The λ function starting in Line 4 in this code listing corresponds to the inversion function G<sub>inv</sub> of the tuple.

Now, it is the turn of the inversion of the function *f*. We use the function name of the inverse function G<sub>inv</sub>(*f*) as indicated by the implementation annotation. It takes the third tuple element *r*<sub>3</sub> as parameter. For the case that inversion fails, we again translate the code of *M''*. For the case that it succeeds, we pass along variable *c* and the second matched parameter *r*<sub>5</sub>:

<caption>Listing 6.5: Continuation: F\* code generated by cv2fstar for the pattern matching example.</caption>

12 match G<sub>inv</sub>(*f*) r<sub>3</sub> with
13 | None → G<sub>M</sub>(M'')
14 | Some (G<sub>var</sub>(*c*), r<sub>5</sub>) →

Finally, we produce the code for the equality pattern's tests. We use the equality test functions of the appropriate types to compare the matched elements r₁, r₅ with the terms v₁, v₅ that have been evaluated at the beginning. For the case that the tests succeed, we translate the code for *M'*, otherwise again the code for *M''*:
<caption>Listing 6.6: End: F\* code generated by cv2fstar for the pattern matching example.</caption>

```
15 if $\mathbb{G}_{\text{eq}}(t_1)$ $r_1$ $v_1$ && $\mathbb{G}_{\text{eq}}(t_5)$ $r_5$ $v_5$
16 then $\mathbb{G}_M(M')$
17 else $\mathbb{G}_M(M'')$
```

In this example throughout the last 4 listings, it is clear that the term $M''$ appears multiple times. If $M''$ translates to multiple lines of code, the repetition can make the generated code quite unreadable. We optimise our compiler for the case of a multiline $M''$ and wrap the pattern matching in an additional match. While translating the original pattern matching, we replace $M''$ by None and $M'$ by the list of variable's assigned. For our example, this results in the following:

```
1 let state, v = $\mathbb{G}_M(M)$ in
2 let state, v_1 = $\mathbb{G}_M(M_1)$ in
3 let state, v_5 = $\mathbb{G}_M(M_5)$ in
4
5 let r = (* the remainder of the above pattern matching code,
6         with "$\mathbb{G}_M(M')$" replaced by "Some ($\mathbb{G}_{\text{var}}(b)$, $\mathbb{G}_{\text{var}}(c)$)"
7         and "$\mathbb{G}_M(M'')$" replaced by "None" *) in
8 match r with
9 | None → $\mathbb{G}_M(M'')$
10 | Some ($\mathbb{G}_{\text{var}}(b)$, $\mathbb{G}_{\text{var}}(c)$) → $\mathbb{G}_M(M')$
11
```

In the last two lines, $\mathbb{G}_M(M')$ and $\mathbb{G}_M(M'')$ are again the original ones. In this style, $\mathbb{G}_M(M'')$ is guaranteed to be translated only once.

**TABLE INSERTS.** For a table tbl, an insert with terms $M_i$, $1 \le i \le n$ as parameters, and a following term M, we generate the following code:

```
1 $\mathbb{G}_M$(insert tbl($M_1$, ..., $M_n$); M) =
2 let state, v_1 = $\mathbb{G}_M(M_1)$ in
3 ...
4 let state, v_n = $\mathbb{G}_M(M_n)$ in
5 let entry = TableEntry-$\mathbb{G}_{\text{tbl}}$(tbl) #Table-$\mathbb{G}_{\text{tbl}}$(tbl) v_1 ... v_n
6 let state = insert state Table-$\mathbb{G}_{\text{tbl}}$(tbl) entry in
7 $\mathbb{G}_M(M)$
```

In the construction of the table entry we need to indicate the table name as implicit parameter with \# because F\* cannot infer it, in general, from the parameters.

**TABLE GET QUERIES.** We remind the generic syntax of a get query:

```
1 get tbl(p_1, ..., p_n) suchthat M then M' else M''
```

The patterns $p_i$, $1 \le i \le n$ can consist of variable assignments, equality tests, tuple decompositions, and function inversions, just like the patterns in let bindings. The term M constitutes an additional boolean condition.

We are now describing how we generate the filter function that was first introduced in Section 6.9. We call it $\mathbb{G}_{\text{filter}}$ in the following and the generated code is shown in Listing 6.7. It is passed as a parameter to the `cv2fstar` functions `get`, `get_unique(_full)`, and `entry_exists(_full)`. The filter function takes two parameters, the state of the model-specific type `m_`state, and a table entry of type `m_`table_entry parametrized by
the table name `Table_Gtbl` (`tbl`). After decomposing the entry into its fields

<caption>Listing 6.7: F\* code for `Gfilter` generated by `cv2fstar`.</caption>

```h
1 (λ (state:m_state) (te:m_table_entry Table_Gtbl (tbl)) →
2 let TableEntry_tbl v₁ ... vₙ = te in
3 (* translate the patterns using the complex case from above,
4 use "None" as M'' and the following as M': *)
5 let state, v = G_M (M) in
6 if v then state, Some (u₁, ..., uₘ) else state, None
7 )
```

$v_i, 1 \le i \le n$, we are matching these $n$ values to the $n$ patterns $p_i$. For this pattern matching, we reuse the pattern matching algorithm of `let` bindings. The difference is that we have $n$ patterns to match to $n$ values, and not only a single one. We adapt to this case by chaining the $n$ pattern matchings one after another. For the $n$-th pattern matching, we use special values for the success and failure cases: `None` for the failure case, and the code for the `suchthat` condition in the success case, see Lines 5 and 6. The $u_i, 1 \le i \le m$ are the variables that appear in variable assignments in the patterns and that are used in $M'$. These are the variables that are returned as answer of the `get` query.

The filter function `Gfilter` is used as follows in the translation of `get` queries. For a non-unique `get` query with a success term $M'$ that uses variables returned from the query, we generate the following code:

```h
1 (* evaluation of terms appearing in equality patterns *)
2 let state, v... = G_M (...) in
3
4 match get state Table_tbl Gfilter with
5 | state, None → G_M (M'')
6 | state, Some (u₁, ..., uₘ) → G_M (M')
```

First, the terms of any equality patterns used in the query need to be evaluated before anything else. Then, we call the function `get` and pass it the state, the table name, and the filter function. Finally, we evaluate the next terms $M'$ and $M''$ according to the query result.

For a `get[unique]` query, the translation is the same except that the function name `get` is replaced by `get_unique_full`. For a `get` query with a success term $M'$ that does not use any variable returned from the query, we call `entry_exists_full` instead. It returns a boolean result, based on which we decide if $M'$ or $M''$ is evaluated:

```h
1 (* evaluation of terms appearing in equality patterns *)
2 let state, v... = G_M (...) in
3
4 let state, b = entry_exists_full state Table_tbl Gfilter
5 if b then G_M (M') else G_M (M'')
```

TRANSLATING LETFUNS. Having seen how terms are translated, we can come back to letfun s and look at how their interfaces and implementations are generated.

For the interface, we generate a `val` declaration in the file `M.Letfun.fsti` for each letfun. As name we use the same name as in the CryptoVerif model,
prefixed with `fun_`. If the `letfun`'s term needs state, the first parameter of the `letfun` is state. If the `letfun` has parameters, their types are appended separated by `→`. Finally, for the return types, if the `letfun`'s term needs state, the `letfun`'s return type is `m_state * a`, where `a` is the original return type, and only `a` if the term does not need state. Assuming a `letfun` that needs state and takes `n` parameters of type `t_i`, `1 ≤ i ≤ n`, and returns a value of type `t`, the declaration is as follows:

$$1 \quad \texttt{val fun\_letfun : m\_state \to G_t(t_1) \to \dots \to G_t(t_n) \to m\_state * G_t(t)}$$

For the implementation, we generate a `let` in the file `M.Letfun.fst` for each `letfun`. We use the same variable names for the parameters as in the CryptoVerif model. If the `letfun`'s term needs state, the first parameter is state. For the body we call into `G_M`. Assuming a `letfun` that needs state, takes `n` parameters `p_i`, `1 ≤ i ≤ n`, and has the body `M`, the generated code is as follows:

$$2 \quad \begin{array}{l} \texttt{let fun\_letfun state G\_var(p_1) \dots G\_var(p_n) =} \\ \qquad G_M(M) \end{array}$$

## 6.12 TRANSLATING ORACLES AS FUNCTIONS

**OVERVIEW.** Oracles, or processes in the channels frontend, are the essential top-level building block of CryptoVerif models. We use the terminology oracles and processes interchangeably, but prefer oracles because this is how they are called in cryptographic proofs. Oracles are identified by a name, can have parameters, and in our context, can end either with a return statement, or a yield statement returning control to the caller without returning values<fnref n="16" />. Oracles are translated to $F^*$ functions, grouped by the module block annotation in which they are contained: The interfaces of a module's oracles are written to the file `M.Module.fsti` and their implementation to the file `M.Module.fst`, where `Module` is the module name used in the module block annotation.<fnref n="17" /> Reusing the translation of terms, we only need to add treatment of `yield` and `return` to translate an oracle's implementation. Oracles can be part of a series of subsequent oracles. We enforce their order and implement the sharing of variables between them through session state identified by a session ID.

### 6.12.1 Session Data Structure and Session IDs

**MOTIVATION.** An oracle following after one or more oracles is allowed to use variables of the preceding oracles. Otherwise said, such a following oracle can have free variables that are neither defined by the oracle's input parameters nor within the oracle itself, but have been defined by a previous oracle or its inputs. In `cv2fstar`, oracles are translated to separate functions and thus, cannot directly share variables. We use a session data structure to overcome this. At the end of an oracle's $F^*$ code, all free variables of following oracles are written into a session entry. At the beginning of a following oracle, these variables are read from the session entry. A session entry is identified by the name of the following oracle, the counter of the return statement within the current oracle, and a session ID. While the

<footnote n="16">¹⁶A third possibility is `event_abort`, which ends execution of the entire system. We do not allow this in `cv2fstar`'s restricted input language. See Section 6.4.2 for details.</footnote>

<footnote n="17">¹⁷As a reminder, `M` is the name of the CryptoVerif model, derived from its filename, converted to all uppercase letters.</footnote>
attribution of session IDs is discussed in the next paragraph, we explain the return counter. An oracle can have multiple return statements, due to the fact that branching is possible through different means (if, get, and let binding with pattern matching), and the fact that CryptoVerif's syntax does not allow to re-merge branches.<fnref n="18" /> This means oracle definitions need to be repeated after each return. We enforce that the structure of oracles is the same after each return: The oracle's names, whether they are replicated, and their input and output types, must be the same after all returns. However, the body of an oracle can be different in each definition. Thus, it can have a different set of free variables that need to be stored in the session entry by the previous oracle.

The reason for this restriction of the oracle structure is the following. Assume we allow for different following oracles after different returns of an oracle O. In general, the adversary does not know which branch and thus which return was taken in O. Thus, the adversary would not know if an oracle that it wants to call after O is actually available. For example, if in the first branch, O₁ is available as a following oracle, and O₂ in the second branch; if the first branch was taken and the adversary calls O₂, this oracle is not available. How do we encode this error? It should be different from a yield, because that is used to encode that an existing oracle did not return. The restriction to the same oracle structure has been made to avoid the need of extending the semantics of CryptoVerif to encodes this type of error. As a side effect, this means that the adversary cannot detect which branch was taken within an oracle only based on the metadata of the following oracles (name, replication, input and output types).<fnref n="19" />

We use the following example to illustrate the restrictions:

```
1  01(...) :=
2    if ... then (
3        return (...);
4        02(...) :=
5        ...
6        return (...);
7        03(...) :=
8        ...
9        return (...)
10    )
```

In this example, the two columns correspond to the then branch (Lines 3 to 9) and the else branch (Lines 13 to 19) of the if condition. Returns at the same place in both branches must have the same number of parameters, and the same types (Lines 3 and 13, 6 and 16, 9 and 19). Oracle definitions at the same place in both branches must have the same name, the same number of input parameters, and the parameters must be of the same types (Oracles 02 and 03). The bodies of Oracles 02 and 03 are allowed to be different in both branches (parts omitted by ... on Lines 5 and 15, and 8 and 18).

ORACLE NAME, SESSION ENTRY, SESSION ID. A session represents which oracles can be called at that stage of execution. Each session is identified by a session ID. Due to replication and parallel composition, multiple oracles

<footnote n="18">¹⁸For example, the following is not allowed to continue with a term $M'$ in both branches after an if condition: `(if M then $M_1$ else $M_2$); $M'$`</footnote>

<footnote n="19">¹⁹Information about the branch taken can be encoded into the return values.</footnote>
might be callable from a given session. We store a list of session entries associated to each session ID in a map. If an oracle has multiple following oracles in parallel composition, the oracle adds a session entry for each of them. Session entries for oracles under replication are never removed.

We use a type `m_oracle_name` to enumerate all oracles:

1. `type m_oracle_name: eqtype =`

2. `| Oracle_Oi`

3. `...`

4. `| Oracle_On`

Here, the $O_i$, $1 \le i \le n$ are the names of the oracles in the CryptoVerif model, over all modules. The value `Oracle_Oi` is used to regroup all session entries valid for this oracle, as we will see later.

Session entries look like this:

1. `noeq type m_session_entry =`

2. `| ...`

3. `| Rj_Oi: v₁:t₁ ... vₘ:tₘ ... m_session_entry`

4. `| ...`

Here, $j$ stands for the counter of the return in the previous oracle, and $O_i$ is the oracle that can be called. The values $v_k$ of type $t_k$, $1 \le k \le m$ are the free variables of oracle $O_i$ or one of its following oracles. The oracle will load these variables from the session entry.

### 6.12.2 The Interface of an Oracle Function

For an oracle $O$ with input types $t_i$, $1 \le i \le n$, and output types $t'_j$, $1 \le j \le m$, we generate the following interface:

1. `val oracle_O: m_state -> nat -> G_t(t₁) ... -> G_t(tₙ)`

2. `-> m_state * option (nat * G_t(t'_1) * ... * G_t(t'_m))`

The input session ID of type `nat` is only present if the oracle is not a top-level oracle: top-level oracles are the entry points to a model, and so there is no session to continue, yet. Non-top-level oracles always continue a session and thus, *always* take a session ID as input. If the oracle takes no input parameters, no types $G_t(t_i)$ are indicated in the interface except `m_state`.

In general, an oracle's function returns `state`, `None` when the oracle terminates by `yield`, and it returns `state`, `Some sid`, $v_1, ..., v_m$) when it terminates by `return(M_1, ..., M_m)`. In more detail, the behaviour is as follows: A new session is started by oracles under replication that have following oracles. Only in this case, a new session ID of type `nat` is returned along with the oracle's other return values. If the oracle has no output, i. e., the return statements are empty, the output types are replaced by a single `unit`. If the oracle does never return in any branch, but always finishes by `yield`, the return type of the function is only `m_state`. Such an oracle cannot have following oracles, so there is never a new session ID.

### 6.12.3 The Implementation of an Oracle Function

We start by discussing the implementation of top-level oracle functions. They are less involved, because there is no need to resume a session. Just like we defined a function $G_M(M)$ to translate a term $M$, we define a function
$G_O(P)$ to translate oracle bodies $P$. It reuses $G_M$ for everything except
yield and return. We define $G_O$ for them in the course of this section.

For an oracle $O$ with input parameters $v_i$, $1 \le i \le n$ of types $t_i$, $1 \le i \le n$,
the implementation starts as follows:

1. let oracle_O state $G_{var}(v_1) ... G_{var}(v_n) =$

There is no session ID parameter.

If there are following oracles after this oracle, we need to write one
or more session entries before returning. Thus, we need a session ID to
which these entries are associated. If the current oracle is under replication,
which is always the case for top-level oracles, we need a new session ID. It
is obtained by the following function call that reserves a new session ID in
the session map:

1. let state, sid = state_reserve_session_id state in

If the current oracle is not under replication, the same session ID is reused.
This is important for non-top-level oracles. The reason why we reserve a
session ID so early within an oracle function is that we might need it for
an event that uses it in its parameters. This is not optimal, as we might
"lose" a session ID in cases where there is no such event and the oracle
ends by yield. This is a tradeoff to keep the code uniform and simple. The
alternative of only reserving the session ID right before it is needed, and
thus possibly in multiple branches of the oracle, is more complex.

CryptoVerif allows pattern matching in oracle inputs:

1. $O(p_1, ..., p_n) := ...$

The depth of the patterns<sup>20</sup> does not influence the type of the input param-
eters: this oracle has $n$ input parameters, and their types are the types of
the patterns $p_i$, $1 \le i \le n$. The pattern matching is evaluated inside the
oracle body before the remaining code of the oracle, to bind the variables
and check the equality patterns. If the pattern matching fails, the call to the
oracle counts regardlessly and the oracle ends with `yield`.<sup>21</sup> We generate
the appropriate code by using the same algorithm as for the complex case of
let binding pattern matching. For the success case, we generate code for the
body of the oracle using $G_O$. For the failure case, we use $G_O(yield)$.

TRANSLATING YIELD. If all branches within an oracle finish by `yield`, the return type of the oracle is (only) `m_state`. Thus, we translate `yield` by just `state`. If not all branches finish by `yield`, we translate it by `state`, `None`. This is the definition of $G_O(yield)$.

TRANSLATING RETURN. In a simple case where there are no following oracles
after a return, we can translate it as follows, considering a return term
return($M_1, ..., M_n$):

1. let state, $v_1 = G_M(M_1)$ in

2. ...

3. let state, $v_n = G_M(M_n)$ in

4. state, Some($v_1, ..., v_n$)

If the oracle has following oracles, we need to create session entries and
return a session ID. We need one session entry for each following oracle, to
provide it with the values of its free variables (and those of its own following

<footnote n="20">20 Each pattern might contain multiple levels of function inversions.</footnote>

<footnote n="21">21 So, pattern matching in oracle parame-
ters is just syntactic sugar for applying the
pattern to the input parameters as first step
inside the oracle body.</footnote>
oracles, possibly). As described above, the definition of the following oracle and its free variables can depend on the branch taken in the current oracle. Thus, it makes sense to create the session entries right before returning.

In the following code, we translate return number *r* of the current oracle, returning a tuple of terms *M*<sub>*i*</sub>, 1 ≤ *i* ≤ *n*. We assume there are *m* following oracles *O*<sub>*j*</sub>, 1 ≤ *j* ≤ *m* that have *n*<sub>*j*</sub> free variables each, called *b*<sub>*j*,k*</sub>, 1 ≤ *k* ≤ *n*<sub>*j*</sub>.

1 G<sub>O</sub>(return(M<sub>1</sub>, ..., M<sub>n</sub>)) =
2 let sel = [Rr<sub>O<sub>1</sub></sub> G<sub>var</sub>(b<sub>1,1</sub>) ... G<sub>var</sub>(b<sub>1,n<sub>1</sub></sub>);
3 ...;
4 Rr<sub>O<sub>m</sub></sub> G<sub>var</sub>(b<sub>m,1</sub>) ... G<sub>var</sub>(b<sub>m,n<sub>m</sub></sub>)] in
5 let state = state_add_to_session state sid sel in
6 let state, v<sub>1</sub> = G<sub>M</sub>(M<sub>1</sub>) in
7 ...
8 let state, v<sub>n</sub> = G<sub>M</sub>(M<sub>n</sub>) in
9 state, Some (sid, v<sub>1</sub>, ..., v<sub>n</sub>)

The function `state_add_to_session` adds the list of session entries `sel` to the already existing session entries of session `sid`. If it is a new session, these will be the only entries.

**NON-TOP-LEVEL ORACLES.** We continue with the implementation of non-top-level oracle functions:

1 let oracle_O state sid G<sub>var</sub>(v<sub>1</sub>) ... G<sub>var</sub>(v<sub>n</sub>) =

We always need the session ID parameter `sid` for non-top-level oracles.

Non-top-level oracles start by retrieving an appropriate session entry from the list of session entries associated with the session ID `sid`.

1 match get_session_entry state Oracle_O sid with
2 | None → G<sub>O</sub>(yield)
3 | Some (se: m_session_entry) →

The session might contain session entries for different oracles, but there can only be one that fits to oracle *O*. The reason for this is that within *one* session, only one return of the previous oracle could have been taken. Taking multiple different return branches is only possible if the previous oracle is under replication, and then the session entries end up in lists for different session IDs. We pass the oracle name to the session retrieval function such that it finds the at most one session entry that fits. The function `get_session_entry` returns `None` in case the session ID does not exist or there is no fitting session entry. In this case, the oracle function fails early. The function `get_session_entry` is used in oracles under replication, as it does not remove the session entry. For oracles not under replication, we use `get_and_remove_session_entry` that removes the session entry. It returns a new state alongside the result.

After retrieving the session entry, we continue with the code for reserving a new session ID if needed, as explained above in the paragraph about top-level oracles. Then, we generate code to match on the different possibilities for the session entry. There is one possibility for each return of the previous oracle *O*<sub>*p*</sub>. Considering a previous oracle with *m* returns, and *n*<sub>*j*</sub> variables transmitted from *O*<sub>*p*</sub> to *O* at return number *j*, we generate the following code:
1 match se with

2 | R1_Op Gvar(u1,1) ... Gvar(u1,n1) →

3 (* code for body of oracle O after return 1 of Op *)

4 ...

5 | Rm_Op Gvar(u_m,1) ... Gvar(u_m,n_m) →

6 (* code for body of oracle O after return m of Op *)

The code within the branches is generated as in top-level oracles: we match the input patterns of the oracle and continue with G<sub>O</sub>(P) in the success case, where P is the oracle's body, and continue with G<sub>O</sub>(yield) in the failure case.

### 6.12.4 Session Type

Before we end the section on the translation of oracles, we give a quick overview of the declaration and implementation of the session type. Like for tables, we define a session type that holds information specific to a CryptoVerif model. It has a single constructor:

1 noeq type session_type =

2 | SessionType :

3 (* oracle name *)

4 on: eqtype →

5 (* session entry *)

6 se: Type0 →

7 (* following oracles *)

8 fo: (on → list on) →

9 (* session_entry_to_name *)

10 se2on: (se → on)

11 → session_type

Similar as with tables, we have one type enumerating all possible oracle names (on), and one type for the actual session entries (se). We define getters `oracle_name` and `session_entry` for these types, returning on and se for a given session type.

The field `fo` must be instantiated by a function mapping an oracle name to the oracle names of all allowed following oracles. The field `se2on` must contain a function mapping session entries to the oracle's name to which they belong. `cv2fstar` generates the appropriate instantiations for a model. The function `se2on` is generated such that for each session entry `Rj_Ok` it returns the oracle name `Oracle_Ok`. It is used by `get_session_entry` and `get_and_remove_session_entry` to determine if a session entry fits to a given oracle name; `se2on` is used to implement an `is_valid_entry` predicate that checks whether an oracle name and a session entry match:

1 let is_valid_entry

2 (#st: session_type)

3 (on: oracle_name st)

4 (se: session_entry st)

5 =

6 match st with | SessionType _ _ _ se2on → (se2on se = on)

We plan to use the function `fo` for future work, when we prove lemmas about the correct treatment of sessions by oracle functions (see Section 6.17).

All sessions of a model are held in a type `sessions` that is refined by the session type. It is implemented as a map from a natural number session ID to a list of session entries defined for this session type:
1 let sessions (st: session_type) = Map.t (list (session_entry st))

Another example of where `is_valid_entry` is used, is the return type of `get_session_entry` and `get_and_remove_session_entry`:

1 val get_and_remove_session_entry
2 (#stt: state_type)
3 (st: state stt)
4 (on: oracle_name (st_of stt))
5 (sid: nat)
6 : (state stt
7 * option (s: (session_entry (st_of stt)){is_valid_entry sn s}))

This refinement is useful for the implementation of the oracle body. When matching on the different possibilities for the session entry, the refinement allows us to only match on the session entries that are actually possible for the oracle's name: The F* typechecker understands that the other session entries are not possible and does not complain about a non-exhaustive pattern matching.

## 6.13 TRANSLATING ASSUMPTIONS AS LEMMAS

Many assumptions are made in a CryptoVerif model: On the one hand, there are cryptographic hypotheses on the cryptographic building blocks. On the other hand, there often are functions for message formats that are assumed to have certain properties, e. g., producing disjoint output for different message types, or having an inverse. Functions for serialization and deserialization are assumed to be inverses, equality test functions are assumed to be equivalence relations.

While we are not hoping to prove the cryptographic assumptions for an implementation in F\*, proving that the non-cryptographic assumptions hold for an implementation is definitely in the realm of F\*'s type system. With `cv2fstar`, we translate many of these assumptions to F\* lemmas. This produces proof obligations for the implementation, that the user has to prove.<fnref n="22" /> This reinforces the link between CryptoVerif models and F\* implementations produced by `cv2fstar`. For the proofs of the lemmas, existing lemmas in F\* and HACL\* can of course be reused; so some lemmas might be straightforward to prove. In the following, we discuss what kind of lemmas `cv2fstar` produces for which kind of assumption in a CryptoVerif model. The generated code is written to the file `M.Equations.fsti`. The user will need to write proofs for the lemmas in the file `M.Equations.fst`.

**SOURCES OF LEMMAS.** There are 4 sources of lemmas from the point of view of `cv2fstar`, at the moment. First, there are equations explicitly defined in the CryptoVerif model. Second, the assumption that the inverses of functions declared with `[data]` are correct. Third, serialization and deserialization functions are assumed to be inverses of each other. Fourth, CryptoVerif allows to declare built-in equational theories for functions, like commutativity, up to forming a group with an inverse function and a neutral element. `cv2fstar` generates lemmas for these kinds of assumptions. We go through them one by one and explain what lemma code we generate for these. Generally, we produce `val` declarations of lemmas, and no proofs.

<footnote n="22">²²The user can also consciously admit these lemmas and thus assume they have a proof, but at this point, `cv2fstar` did all it could by translating the lemmas.</footnote>
### 6.13.1 Explicitly Defined Equations

An equation is defined starting with the equation keyword, followed by a list of universally quantified variables with type indication, then a boolean term $M$ encoding the assumption, and optionally, the keyword if followed by a condition $M'$:

1. equation `forall v₁:t₁, ..., vₙ:tₙ; M if M'`.

We generate the following $F^*$ code for such an equation:<fnref n="23" />

1. `val lemma_i: unit → Lemma (∀ (G_var(v₁):G_t(t₁)) ... (G_var(vₙ):G_t(tₙ)).)`

2. `G_M(M') ⇒ G_M(M)`

Here, $i$ is the number of the lemma: We do not generate speaking lemma names but just numerate them. The lemma does not take any parameters (unit), the universally quantified variables are all defined inside. If $M'$ is left empty, it is implicitly true, and we omit $G_M(M') \Rightarrow$. Equations are not allowed to contain terms that process state. We use the version of $G_M$ that is optimized for terms not processing state. It does not produce code that returns a pair of state and the evaluation of the term, but code that returns only the evaluation of the term.

The cryptographic library shipped with CryptoVerif contains many equation definitions, mostly within the macros that define cryptographic assumptions. If we wanted to translate those, we would need $F^*$ translations for all types, functions, and constants used within the macros. However, a user might not want to translate all the cryptographic internals; most likely they just want to use a ready-made implementation from HACL*. So, we translate only those equations that use only types, functions, and constants that have an implementation annotation in the CryptoVerif model. We skip all other equations.

### 6.13.2 Correctness of Inverses

For a function $f$ with inverse $f^{-1}$, we generate lemmas for two assumptions: First, $f^{-1}$ applied to the output of $f$ for some input $x$, returns exactly this input $x$. Second, if $f^{-1}$ applied to a value $y$ returns $x$, then $f(x) = y$; if $f^{-1}$ cannot compute the inverse of $y$ and returns the error symbol, then there is no $x$ such that $f$ could have returned $y$. These two assumptions are used for functions declared with `[data]`, and for serialization and deserialization functions of a type.

For a function $f$ taking $n$ parameters of types $t_1, 1 \le i \le n$, and returning a value of type $t$, the first assumption translates to the following code for the equation term (so, ignoring how the parameters are quantified for now):

1. `match G_inv(f) (G_f(f) x₁ ... xₙ) with`

2. `| Some (z₁, ..., zₙ) → G_eq(t₁) x₁ z₁ ... ∧ ... ∧ G_eq(tₙ) xₙ zₙ`

3. `| None → ⊥`

The $⊥$ in the `None` case means that we want to prove that this case does not occur.

We use this code to generate code for two lemmas. One of them corresponds closely to the way CryptoVerif defines equations: all variables are universally quantified. Proving such lemmas in $F^*$ is more complex, and so we generate a helper lemma that is easier to prove. This lemma takes

<footnote n="23">²³Indicating unit as a parameter is required in $F^*$ even if the lemma takes no actual parameters.</footnote>
the variables as parameters and thus expresses the assumption just for an
instantiation of the variables. The two lemmas are as follows:

1. val lemma_i_inner (x₁:G<sub>t</sub>(t₁)) ... (x_n:G<sub>t</sub>(t_n)) : Lemma (
2. (* code for the equation term *)
3. ) [SMTPat ( G<sub>inv</sub>(f) (G<sub>f</sub>(f) x₁ ... x_n) )]
4.
5. let lemma_i () : Lemma (∀ (x₁:G<sub>t</sub>(t₁)) ... (x_n:G<sub>t</sub>(t_n)).
6. (* code for the equation term *)
7. ) = ()

The helper lemma is the first one. The code is a val declaration of a lemma, so it still has to be proved in M.Equations.fst. It declares an SMT pattern, which lets F* automatically use the helper lemma to prove the actual lemma, the second one in the above code. This lemma takes no parameters, the universal quantification of the variables is inside. It is a let definition,<fnref n="24" /> meaning it has to have a proof, directly. Here, the proof is just () : F* succeeds in applying the previous lemma automatically thanks to the SMT pattern.

For the same function *f*, the second assumption translates to the following equation term:

1. match G<sub>inv</sub>(f) y with
2. | Some (x<sub>1</sub>, ..., x<sub>n</sub>) → G<sub>eq</sub>(t) (G<sub>f</sub>(f) x<sub>1</sub> ... x<sub>n</sub>) y
3. | None → ¬(∃ (x<sub>1</sub>:G<sub>t</sub>(t<sub>1</sub>)) ... (x<sub>n</sub>:G<sub>t</sub>(t<sub>n</sub>)). G<sub>eq</sub>(t) (G<sub>f</sub>(f) x<sub>1</sub> ... x<sub>n</sub>) y)

We generate the following two lemmas, again with the first one being a
helper lemma that is the one proved by the user:

1. val lemma_i_inner (y:G<sub>t</sub>(t)) : Lemma (
2. (* code for the equation term *)
3. ) [SMTPat ( G<sub>inv</sub>(f) y )]
4.
5. let lemma_i () : Lemma (∀ (y:G<sub>t</sub>(t)).
6. (* code for the equation term *)
7. ) = ()

The code for serialization and deserialization is a special case: *f* is the
 serialization function *G*<sub>ser</sub>(*t*<sub>1</sub>) for type *t*<sub>1</sub> and it takes only one parameter
of this type, so *n* = 1. Its return type *t* is *G*<sub>*t*</sub>(*t*) = bytes. *f*<sup>-1</sup> is the
deserialization function *G*<sub>deser</sub>(*t*<sub>1</sub>) for the type *t*<sub>1</sub> and it takes one parameter
of type bytes. The function's output is an option on one value of type *t*<sub>1</sub>.
The equality test function *G*<sub>eq</sub>(*t*) is always *eq_bytes*.

The reader might wonder why we do not use this style with helper
lemmas for the explicitly defined equations discussed in Section 6.13.1, after
all we said that this makes the proof easier. However, SMT patterns cannot
treat occurrences of negation well, but the explicitly defined equations can
contain negations. In future work, we could try to filter out any negations
when creating the SMT pattern. For now, we decided to only generate the
universally quantified version for the explicitly defined equations.

6.13.3 *Built-in Equational Theories*

Built-in equations are used with the keyword equation builtin, followed
by the name of the equational theory, and its parameters. The signature of
the lemmas that we generate is always the same, so we are not repeating it
each time in the following:

<footnote n="24">²⁴It is allowed to have let definitions in an fsti interface file. It is exposed to the outside just like val declarations.</footnote>
1. `val lemma_i : unit → Lemma ( (* code of the equation *) )`

As with the other kinds of assumptions, we only translate those that only contain functions and constants that are translated, i. e., have an implementation annotation.

equation builtin commut(f). For a binary function f with two inputs of the same type t and return type t', this indicates that f is commutative. We generate the following code for the inside of the lemma:

1. `∀ (a:G_t(t)) (b:G_t(t)). G_{eq}(t') (G_f(f) a b) (G_f(f) b a)`

equation builtin assoc(f). For a binary function f with inputs and return of the same type t, this indicates that f is associative. We generate:

1. `∀ (a:G_t(t)) (b:G_t(t)) (c:G_t(t)).`

2. `G_{eq}(t) (G_f(f) a (G_f(f) b c)) (G_f(f) (G_f(f) a b) c)`

equation builtin AC(f). For a binary function f with inputs and return of the same type t, this indicates that f is commutative and associative. We generate two separate lemmas, one for commutativity, and one for associativity, like above, respectively.

equation builtin assocU(f, n). For a binary function f with inputs and return of the same type t, and a constant n also of type t, this indicates that f is associative and that n is a neutral element for f. We generate one lemma for associativity like above, and one for the neutral element as follows:

1. `∀ (a:G_t(t)). (G_{eq}(t) (G_f(f) a G_c(n)) a) ∧ (G_{eq}(t) (G_f(f) G_c(n) a) a)`

equation builtin ACU(f, n). This is like assocU, adding that f is also commutative. We generate three lemmas like above, for commutativity, associativity, and the neutral element.

equation builtin ACUN(f, n). This is like ACU, adding that the equation $f(a, a) = n$ holds for all a of type t. We generate three lemmas like above, for commutativity, associativity, and the neutral element, and a fourth one for the cancellation equation:

1. `∀ (a:G_t(t)). G_{eq}(t) (G_f(f) a a) G_c(n)`

equation builtin group(f, inv, n). For a binary function f with inputs and return of the same type t, and a constant n also of type t, and a unary function inv with input and return type t, this indicates that f forms a group in type t, where n is the neutral element and inv computes the inverse of an element. We generate an associativity lemma, one for the neutral element, and the following for the inverse:

1. `∀ (a:G_t(t)).`

2. `(G_{eq}(t) (G_f(f) a (G_f inv) a) G_c(n)) ∧`

3. `(G_{eq}(t) (G_f(f) (G_f inv) a) a) G_c(n)`

equation builtin commut_group(f, inv, n). This is like group, adding that the group is commutative. We generate the same lemmas as for group, and a commutativity lemma for f like above.

In case we know that f is commutative, we could simplify the lemmas for the neutral element and the inverse, including only one of the conditions, respectively. For simplicity of our code, we chose not to do that at the moment.
For equality test functions, CryptoVerif uses the built-in equation system to indicate that they are commutative. Thus, as a side effect of our translation of built-in equations, we generate commutativity lemmas for the equality test functions of extracted types. We could prove more properties about equality test functions, and we plan to do so in future work, see Section 6.17.

For the fixed types, `cv2fstar` is not generating lemmas about equality test functions. However, as equality check for fixed types is directly using HACL*'s equality test `lbytes_eq`, commutativity and other properties are already proven within HACL*: `lbytes_eq` is proven to be equivalent to F*'s (`==`) operator.

## 6.14 DIFFERENCES TO THE OCAML EXTRACTION

The major difference between `cv2fstar` and OCaml extraction developed previously [CB13; CB15] is that `cv2fstar` connects CryptoVerif to a proof-oriented programming language with a richer type system, $F^*$, that allows to not only execute the CryptoVerif models but also to prove more properties about them.

Additionally, `cv2fstar` translates more parts of a CryptoVerif model than `cv2ocaml` does: we translate events, which are ignored in `cv2ocaml`; we translate equations and other assumptions as lemmas, which are not translated by `cv2ocaml`.

Then, there are differences in how a CryptoVerif model is translated. In `cv2ocaml`, a series of oracles is expressed by closures: an oracle with following oracles returns a closure representing the next possible oracle calls. In `cv2fstar`, we translate each oracle as a separate function and enforce the calling order by passing around a state object holding session state, and by using session IDs. We use this style rather than closures because it is closer to the style of efficient implementations in Low*, the subset of $F^*$ that can be extracted to C code using the tool KaRaMeL [Pro+17]. This will make it easier to prove functional equivalence of the $F^*$ specifications generated by `cv2fstar` and a Low* implementation, in future work.

The state also holds table data in memory, that is always written to and read from files in `cv2ocaml`. For sharing variables between modules, `cv2ocaml` provides a mechanism by writing to and reading from files. We do not need this kind of sharing in `cv2fstar`, because we require all modules to be at the top of the main process.

`cv2fstar` makes the handling of entropy for random sampling explicit to produce pure functional code. `cv2ocaml` does not make this explicit and is producing code with side effects. However, as discussed in Section 6.6.1, the OCaml backend used by `cv2fstar` is not ideal concerning random sampling, neither. In `cv2ocaml`, CryptoVerif `letfun`s used to be inlined, and we translate them as separate functions in `cv2fstar`. This has been backported to `cv2ocaml` in the meantime.

While `cv2ocaml` allows top-level oracles to be restricted to a single call, `cv2fstar` requires that all top-level oracles are under replication. Furthermore, `cv2fstar` requires that all top-level oracles are extracted as modules, which is not the case for `cv2ocaml`. The motivation and some consequences of this

<footnote>[CB13] Cadé and Blanchet, “From Computationally-Proved Protocol Specifications to Implementations and Application to SSH”</footnote>

<footnote>[CB15] Cadé and Blanchet, “Proved Generation of Implementations from Computationally Secure Protocol Specifications”</footnote>

<footnote>[Pro+17] Protzenko et al., “Verified Low-Level Programming Embedded in $F^*$”</footnote>
are described in Section 6.4.2.

In the implementation annotations of a CryptoVerif model, `cv2ocaml` allows the indication of a predicate function for a type. It serves to determine if a value of an OCaml type corresponds to the type in CryptoVerif. Let us take the example of all bitstrings of length *l* bits that start with a zero bit. In OCaml, neither the length requirement nor the restriction on the starting bit can be expressed directly with the type definition. We would use `string` as base type, and a predicate that checks the additional requirements. We do not need this mechanism in `cv2fstar` because F*'s rich type system allows us to express such predicates directly in the definition of the type, as refinements.

Finally, as a small last difference, `cv2fstar` introduces the new `use_entropy` annotation for `letfun`s that shall be translated by a predefined function.

## 6.15 CASE STUDY: THE NEEDHAM-SCHROEDER-LOWE PROTOCOL

As stated in Section 2.5, the Needham-Schroeder and Needham-Schroeder-Lowe protocols have been the “Hello World” of security protocol verification methodologies since many years, and so we chose to do our first case study of `cv2fstar` on them, too. As `cv2fstar`'s goal is not to produce a security proof or to find flaws in a protocol specification, but to generate code for a protocol that has been proven secure, we are using the Needham-Schroeder-Lowe (NSL) protocol as example. As a reminder, this protocol uses a public-key encryption scheme and has the goal of mutually authenticating two participants. To keep our first usage of `cv2fstar` simple, we use the simplified version of NSL that we introduced in Section 2.5: we remove the trusted key server and instead implement it as tables in CryptoVerif. In the following subsections, we resurface some elements of the CryptoVerif model discussed in Section 2.5 that are relevant to the `cv2fstar` case study, and that we are slightly adapting. The reader shall feel free to go back to Section 2.5 for a more detailed description of the CryptoVerif model. For reference, we reproduce the protocol diagram in Figure 6.2.

### 6.15.1 CryptoVerif Model for NSL

The CryptoVerif model we presented in Section 2.5 already has the top-level oracle structure that is required by `cv2fstar`: the four top-level oracles `setup`, `key_register`, `initiator`, and `responder` are in parallel composition and under replication. For `cv2fstar`, we add a module annotation for the extraction, respectively (see Lines 2 and 6):

1. `let setup() =`
2. `Setup {`
3.   `foreach i & Qsetup do`
4.     `setup(addr: address) :=`
5.     ...
6. }`

Following the module names in the annotations, `cv2fstar` will generate the files `NSL.setup.fst(i)`, `NSL.Keyائلist.fst(i)`, `NSL.Initiator.fst(i)`, and `NSL.Responder.fst(i)`.

Also, we use a public-key encryption scheme where encryption can fail, because we want to use the HPKE standard to implement it.<fnref n="25" />

<footnote n="25">²⁵HPKE instantiated with the Diffie-Hellman-based DHKEM fails encryption if the Diffie-Hellman shared secret results in the all-zero bitstring.</footnote>
<figure><img src="image_33.png" /><figcaption>FIGURE 6.2: The simplified version of the Needham-Schroeder-Lowe protocol that we use. We assume that A and B possess a secret key and know the other participant's public key $pk_{B,A}$. We assume that they have an address $addr_{A,B}$ and know the one of the other participant. The events $beginA$, $beginB$, $endA$, and $endB$ are used to express the authentication properties of the protocol.</figcaption></figure>

### 6.15.2 Types

In the following, we list the main types used in the CryptoVerif model and explain how we implement them in $F^*$ after extraction with cv2fstar.

We define nonce as a fixed, large type. For key-pair generation, we use a keyseed that is also defined as fixed and large type. We annotate nonce with size 64 bits and keyseed with size 256 bits, and so they are translated to `lbytes 8` and `lbytes 32`. The 64 bits for nonce are an arbitrary choice, the 256 bits for keyseed correspond to the length of HPKE private keys: we want to use the HPKE standard to implement public-key encryption.

For the other types, `cv2fstar` generates a type declaration in `NSLсс. Types. fsti`. We manually write `NSLсс. Types. fst` to implement them, mostly by reusing the types that are defined in the `cv2fstar` framework in the `CVTypes` module. Concerning the implementation annotations in the CryptoVerif model, we use a convention for all types: the same name is used in $F^*$, equality test functions have the name `eq_` followed by the type's name, serialization and deserialization functions are ` serialize_` and ` deserialze_` followed by the type's name, and random sampling functions are `gen_` followed by the type's name. While `cv2fstar` enforces the translation of `[fixed]` types to fixed-length types, there is no such automatism for `[bounded]` types. Therefore, in the following, we lay out how `[bounded]` types also have a bound in the $F^*$ implementation.

For public-key encryption, we use the implementation of HPKE that we developed within the HACL\* library, see Section 5.2.5. Private keys `skey` and public keys `pkey` are declared `[bounded]` and implemented by HPKE's appropriate types; the HPKE ciphersuite we use is DHKEM with Curve25519 and SHA256, and the remainder of HPKE with the ChaCha20Poly1305 AEAD and SHA256. Curve25519 private and public keys have a fixed-size byte representation, so this is sound with respect to the `[bounded]` declaration in the CryptoVerif model, because `[fixed]` implies `[bounded]`. The type `keypair` groups together a secret and public key, we implement it by a tuple `pkey * skey`. The type `ciphertext` is `[bounded]` and implemented by a tuple of an HPKE public key (the KEM ciphertext), and a ChaCha20Poly1305 ciphertext, which is a byte sequence with an upper limit.

HPKE encryption can fail, so as described in Section 2.5.3, we instantiate a CryptoVerif public-key encryption macro such that the return type of the encryption function is an option type `ciphertext_opt`. In $F^*$, we imple-
ment this option type by option ciphertext. `cv2fstar` extracts a lemma for the equation that states that the failure symbol is different from all other possible values. For $F^*$, this lemma is trivial, and thus, it is proved without further steps. The type for plaintext is `[bounded]` and implemented by a ChaCha20Poly1305 plaintext, which is a byte sequence with an imposed maximum length. The type of the random coins needed for the probabilistic HPKE encryption is `encseed` and `[bounded]` in our model; in the implementation, this is an HPKE private key, and so we extract them as a fixed-length type with a size annotation of 256 bits.<fnref n="26" /> Finally, the `[bounded]` type address for the participant's identities is implemented by `bytes`. We impose a maximum length derived from the maximum length of POSIX usernames and DNS hostnames.

**EQUALITY TEST FUNCTIONS.** The equality test functions for all these types are implemented by using `eq_bytes` internally, decomposing a tuple before, if necessary.

**SERIALIZATION AND DESERIALIZATION.** Serialization of a ciphertext is implemented by serializing public key and AEAD ciphertext, and concatenating both byte sequences. Deserialization splits according to the fixed size of a public key. The correctness proof reuses existing $F^*$ lemmas about splitting the result of a concatenation, and vice versa. The private and public keys and the address are already byte sequences, so serialization is the identity function. Deserialization only needs to check that the length of the input byte sequence is appropriate. $F^*$ proves their correctness without further proof indications.

**RANDOM SAMPLING.** The only two types that are used with random sampling are `keyseed` and `encseed`. They are both annotated as fixed-length types, and so the random sampling function is the built-in `gen_lbytes` with 32 as length parameter.

### 6.15.3 Tables

As a reminder, we use two tables, `trusted_keys` and `all_keys`. Each table entry contains data about a participant. The table `trusted_keys` contains addresses and key pairs of honest participants. The table `all_keys` contains addresses and the public keys of all participants, and a trust bit indicating if this participant is honest.

`cv2fstar` generates the following types in `NSL Tables.fsti`. Again, we set the table implementation annotation to use the same name as in the CryptoVerif model.

```
type nsl_table_name : eqtype =
  | Table_trusted_keys
  | Table_all_keys

noeq type nsl_table_entry (tn: nsl_table_name) =
  | TableEntry_trusted_keys :
      address
      -> skey
      -> _: pkey{tn == Table_trusted_keys}
      -> nsl_table_entry tn
```

<footnote n="26">²⁶`cv2fstar` allows annotating bounded types as fixed-length types for the implementation.</footnote>
```sql
11 | TableEntry_all_keys :
12     address
13     -> pkey
14     -> _: bool{tn == Table_all_keys}
15     -> nsl_table_entry tn
```

In `nsl_table_entry`, we use a refinement to restrict the first constructor to the `trusted_keys` table and the second constructor to the `all_keys` table. Technically, this refinement belongs to the `pkey` and the `trust` field, respectively, so we have to give this field a name. However, as we do not use the field's name in the refinement, we can use `.`.

### 6.15.4 Message Encoding Functions

As a reminder, the message encoding functions `msg1`, `msg2`, and `msg3` are defined as follows:

1. `fun msg1(nonce, address): plaintext [data]`.

2. `fun msg2(nonce, nonce, address): plaintext [data]`.

3. `fun msg3(nonce): plaintext [data]`.

We assume that the outputs of these functions never collide, by using three equations (see Section 2.5.5), that `cv2fstar` translates to $F^*$ lemmas. We implement the three functions in $F^*$ by a concatenation of their parameters, using a one-byte prefix `0x01`, `0x02`, `0x03` for `msg1`, `msg2`, and `msg3`, respectively. This allows us to prove the disjointness of outputs.

### 6.15.5 Implementing Public-Key Encryption

As a reminder, the macro we use to instantiate probabilistic public-key encryption in the `CryptoVerif` model declares a function `enc_r` that takes randomness explicitly as parameter, and defines a `letfun enc` that samples the randomness needed for encryption and passes it to `enc_r`:

1. `fun enc_r(plaintext, pkey, encseed): ciphertext.`

2. `letfun enc(m: plaintext, pk: pkey) = r <-R encseed; enc_r(m, pk, r)`.

3.

The implementation of `HPKE`'s encryption function in `HACL*` expects to receive the ephemeral private key as parameter; this fits well together, because we implement the type `encseed` by a byte sequence of the right size. Thus, in $F^*$, we implement `enc_r` as a thin wrapper around `HPKE`'s encryption function in `Base mode`. The wrapper just adds the other two necessary parameters to the function call, the info bitstring and additional data, and we use an empty bitstring for both, for simplicity. We use the following implementation annotation in the `CryptoVerif` model:

1. `implementation fun enc_r="enc"`.

The decryption function `dec_opt` takes a value of type `ciphertext_opt` as parameter, to allow it to be called on the failure value `ciphertext_bottom`. We define a `letfun` function `dec` as a wrapper that can be called with a value of type `ciphertext` directly. It injects the value into `ciphertext_opt` using the function `ciphertext_some` before calling `dec_opt`. We add an implementation annotation to indicate that we want to implement `dec` directly in $F^*$, hiding the `letfun`'s body:
1 implementation fun dec="dec".

We do this because the HPKE decryption function does not allow a failure
symbol as parameter.

We briefly recall the CryptoVerif code for the kp function and the keygen
letfun:

1 fun kp(pkey, skey): keypair [data].

2 letfun keygen() = k <-R keyseed; kp(pkgen(k), skgen(k)).

The type keyseed is implemented as a byte sequence of exactly the length
of an HPKE private key. Thus, we implement skgen as the identity function,
pkgen as exponentiation, and cv2fstar translates keygen as letfun doing the
random sampling.

6.15.6 Events and Queries

The CryptoVerif model uses the four events beginA, beginB, endA, and endB,
that are all declared to take both participants' addresses and the two nonces
as parameters, as described in Section 2.5.7. cv2fstar generates the following
type as part of NSL Events fsti:

1 noeq type nsl_event =

2 | Event_endA : address → address → lbytes 8 → lbytes 8 → nsl_event

3 | Event_beginA : address → address → lbytes 8 → lbytes 8 → nsl_event

4 | Event_endB : address → address → lbytes 8 → lbytes 8 → nsl_event

5 | Event_beginB : address → address → lbytes 8 → lbytes 8 → nsl_event

6.15.7 Honest Participant Oracles

In the following, we discuss the code generated for the initiator oracles.
The code generated for the other oracles is included in Appendix D. As a
reminder, the initiator process exposes three oracles that can be called only in
sequence. The first oracle sends the first protocol message, the second oracle
receives the second protocol message and sends the third protocol message,
and the third oracle issues the event endA if the responder is honest.

To showcase the translation of letfun as separate F* functions, we outsource the body of the first oracle into a letfun, deviating from the model presented in Section 2.5.8:

1 initiator_sendMsg_1 (addrA: address, addrX: address) :=

2 let msg1succ(skA, pkX, trustX, Na, c1) =

3 initiator_sendMsg_1_inner(addrA, addrX) in

4 return (c1);

We declare a new option type for the result of this letfun. On the F* side, it is
implemented by option (skey * pkey * bool * nonce * ciphertext).

1 type msg1res_t.

2 fun msg1succ(skey, pkey, bool, nonce, ciphertext): msg1res_t [data].

3 const msg1fail: msg1res_t.

4 equationforall x1: skey, x2: pkey, x3: bool,

5 x4: nonce, x5: ciphertext;

6 msg1succ(x1, x2, x3, x4, x5) <> msg1fail.

The function msg1succ is used to construct the return value in case the
encryption of the first protocol message succeeds, and the constant value
msg1fail is used if the retrieval of key material or the encryption fails.
The body of the letfun is practically the same as the oracle body of
initiator_sendMsg_1 in Section 2.5.8. However, in letfun s it is required
to make the failing branch of get requests and let binding pattern matchings
explicit:

1 letfun initiator_sendMsg_1_inner(addrA: address, addrX: address) =
2 (* the gets fail if addrA or addrX have not been
3 setup by the adversary. *)
4 get[unique] trusted_keys(=addrA, skA, pkA) in (
5 get[unique] all_keys(=addrX, pkX, trustX) in (
6 (* Prepare Message 1 *)
7 Na <-R nonce;
8 let ccl = enc(msg1(Na, addrA), pkX) in
9 let ciphertext_some(c1: ciphertext) = ccl in (
10 msg1succ(skA, pkX, trustX, Na, c1)
11 ) else msg1fail
12 ) else msg1fail
13 ) else msg1fail.

cv2fstar generates the following function declarations in NSL.Initiator.
fsti. We see that each takes at least nsl_state as input and returns at
least nsl_state. Only the first oracle returns a new session ID, and only
the two last oracles take a session ID as input.

1 val oracle_initiator_sendMsg_1: nsl_state -> address -> address
2 -> nsl_state * option (nat * ciphertext)
3
4 val oracle_initiator_sendMsg_3: nsl_state -> nat -> ciphertext
5 -> nsl_state * option (ciphertext)
6
7 val oracle_initiator_finished: nsl_state -> nat
8 -> nsl_state * option (unit)

The following session entry type is generated in NSL.Sessions.fsti.
There is one entry for the responder side, used to share variables from the
first oracle with the second oracle, and two entries for the initiator side. The
integer suffixes of variable names starting with var_ come from CryptoVerif,
it adds them to guarantee unique variable names.

1 noeq type nsl_session_entry =
2 | R1_responder_receivedMsg_3 : 
3 var_Na_4: lbytes 8 -> 
4 var_Nb_2: lbytes 8 -> 
5 var_addrB_0: address -> 
6 var_addrY_0: address -> 
7 var_skB_0: skey -> 
8 var_trustY_0: bool 
9 -> nsl_session_entry
10 | R1_initiator_sendMsg_3 : 
11 var_Na_3: lbytes 8 -> 
12 var_addrA_1: address -> 
13 var_addrX_1: address -> 
14 var_pkX_4: pkey -> 
15 var_skA_2: skey -> 
16 var_trustX_2: bool 
17 -> nsl_session_entry
18 | R1_initiator_finished : 
19 var_Na_3: lbytes 8 -> 
20 var_Nb_1: lbytes 8 -> 
21 var_addrA_1: address -> 
22 var_addrX_1: address ->
23 var_trustX2: bool
24 → nsl_session_entry

The following code is generated for the first initiator oracle in NSL.
Initiator.fst:

1 let oracle_initiator_sendMsg1 state input_43 input_42 =
2 let state, sid = state_reserve_session_id state in
3 let var_addrA1 = input_43 in
4 let var_addrX1 = input_42 in
5 let state, v44 = NSL.Letfun.fun_initiator_send_msg1_inner
6         state var_addrA1 var_addrX1 in
7 let bvar_45 = v44 in
8 match inv_msg1succ bvar_45 with
9 | None → state, None
10 | Some (var_skA2, var_pkX4, var_trustX2, var_Na3, var_cl3) →
11  let sel =
12   [R1_initiator_send_msg3 var_Na3 var_addrA1 var_addrX1
13    var_pkX4 var_skA2 var_trustX2]
14 in
15 let state = state_add_to_session state sid sel in
16 (state, Some (sid, var_cl3))

We can see how a session ID is reserved (Line 2), how the letfun is called (Line 5), how the letfun's result is pattern matched (Lines 7 to 10), how the session entry is created and added (Lines 11 to 15), and that the session ID is returned alongside the ciphertext (last line). This oracle does not use complex pattern matching for its parameters, and so all that is necessary is a simple assignment (Lines 3 and 4). The integer suffixes of variable names not starting with `var_` come from `cv2fstar`, also for the reason of creating unique variable names.

We show the beginning of the generated implementation of the second initiator oracle, to see how session entry retrieval looks like:

1 let oracle_initiator_send_msg3 state sid input_46 =
2 match get_and_remove_session_entry
3 state Oracle_initiator_send_msg3 sid with
4 | state, None → state, None
5 | state, Some (se: nsl_session_entry) →
6 match se with
7 | R1_initiator_send_msg3 var_Na3 var_addrA1 var_addrX1
8         var_pkX4 var_skA2 var_trustX2 →

The oracle needs a session entry matching the oracle name `Oracle_initiator_send_msg3`; the entry is removed after retrieval because the oracle is not under replication (Line 2). The first initiator oracle has only one return, and so there is only one possible session entry (Line 7). The remaining code is included in Appendix D.

### 6.15.8 Executing the Protocol

As a way to evaluate the code generated by `cv2fstar`, we write a small test application. It runs one full protocol execution by calling the oracle functions one after another, feeding back the protocol messages without passing via a network, and printing parts of the state before and after each function call. This means we execute both the initiator and the responder within one process on one machine. While this does not constitute a real-world use case, it allows us to test if the protocol code generated by `cv2fstar` works.
We write an F\* file *Application.fst* and extract it to OCaml using F\*'s standard toolchain and a helper Makefile generated by `cv2fstar`.

We setup two honest participants with addresses `A@localhost` and `B@localhost` using the setup oracle. Afterwards, we use the printing helper generated by `cv2fstar` to print the table entries of both tables. Then, we call the first initiator oracle function with the two addresses as parameters, and go on with the other oracle functions, switching between responder and initiator. After each oracle function call, we use the generated printing helpers to print the session entries, and the protocol message. At the end, we print the list of events issued during protocol execution.

The experiment is successful: a full protocol run finishes such that both participants end up with the same two nonces, and we see that tables, sessions, and event list are populated as expected. The main code of *Application.fst* and its full printout is included in *Appendices D.6* and D.7.

The sequence of oracle function calls is contained in the function `testrun` in *Application.fst*. It has effect ML, which means it has side effects; this is because we print information about the protocol run to the terminal. The function does not have any other side effects – after removing the printing, the ML effect could be removed. The function `testrun` takes an initial entropy value as parameter, which it uses to initialize the `cv2fstar` framework. This means the function is generic and we could prove properties about it for all entropy values. The initialization to the special entropy0 value happens in the function `main` in *Application.fst*, which passes it as parameter to `testrun`.

We can provide an anecdotic evidence that executing code generated with `cv2fstar` helps finding bugs in the CryptoVerif model: While modifying the CryptoVerif model over and over again for testing different styles, we ended up using the wrong public key to encrypt one of the protocol messages. This rendered the protocol effectively incorrect; the recipient of the message would not be able to decrypt and would abort the session. CryptoVerif did still prove the correspondance queries because the properties hold also if there is no `endA` nor `endB` event. When executing the code generated by `cv2fstar`, it became clear that a decryption always fails, and we eventually found the mistake in `nsl.ocv`. So, the code served as test for correctness of the protocol.

## 6.16 CONCLUSION

Given the case study presented in the previous section, we can say that `cv2fstar` succeeds in extracting a protocol model with all oracles exposed to the adversary. Furthermore, we extract all relevant non-cryptographic assumptions to lemmas as proof obligations on the F\* side, and prove them manually for our implementation. For NSL, these are the assumptions that the message decoding functions are correct inverses of the message encoding functions, the assumptions that the message encoding functions produce disjoint outputs, and the assumptions that (de) serialization functions of protocol-specific types are correct.
To conclude, `cv2fstar` allows to execute CryptoVerif models, and makes it possible to use a verified cryptographic library, through its framework made ready to use HACL*. Furthermore, because $F^*$ is a proof-oriented programming language, we are not only able to fill in the implementation details that a CryptoVerif model is assuming, but can also prove that the implementation fulfills the model's assumptions. `cv2fstar` generates $F^*$ lemmas as proof obligations for this, translating non-cryptographic assumptions in a meaningful way. The correctness of (de) serialization functions included in the `cv2fstar` framework for CryptoVerif's built-in types is proven once and for all, and we can reuse these lemmas to prove correctness of protocol-specific functions.

The only missing piece to have a translation of all parts of a CryptoVerif model, is the translation of the theorems proved by CryptoVerif into a form usable by $F^*$, e. g., assumed lemmas.

## 6.17 FUTURE WORK

Avenues for future work on `cv2fstar` are manifold. From a scientific view point, the most interesting steps are those further reinforcing the formal link between CryptoVerif and $F^*$. Most importantly, that would be to express the theorems that CryptoVerif proves in a way that $F^*$ understands and that can be used to built upon for further proofs. For correspondence properties, the straightforward first step is to implement the definitions of non-injective and injective correspondences used by CryptoVerif [Bla07] as predicates in $F^*$, and generating appropriate assumed lemmas based on it from `cv2fstar`. Secrecy and equivalence properties from CryptoVerif are relational properties, which are less straightforward to express and work with in $F^*$. One idea is to extract both the real and ideal version of the game, and then use the real version for linking with an implementation, and the ideal version for further proofs. Another, more advanced idea would be to use a framework for relational verification like the one introduced by [Gri+19] and generate assumed lemmas that can then be used for further proofs.

A minor next step is to generate stronger lemmas as proof obligations for equality test functions: instead of just commutativity as side effect of our translation of built-in equational theories, we could explicitly generate lemmas that establish equality test functions as being equivalent to $F^*'$s (`==`) operator.

As a reinforcement of the trust in `cv2fstar` itself, we believe that the soundness proof of `cv2ocaml` [CB15] could be adapted to `cv2fstar`. The most important difference of `cv2fstar`'s code generation relevant to the proof is the usage of sessions instead of closures for sequences of oracles.

An exciting next step would be to apply `cv2fstar` to a practically relevant real-world protocol. The natural next example given the work presented in this thesis would be `WireGuard`. Moreover, we could try to link the specification generated by `cv2fstar` to the efficient low-level implementation of Noise* [Ho+22], presenting an end-to-end case study from cryptographic proofs down to verified C code.

There are several ideas we have to strengthen the `cv2fstar` framework,

<footnote>[Bla07] Blanchet, "Computationally Sound Mechanized Proofs of Correspondence As-sertions"</footnote>

<footnote>[Gri+19] Grimm et al., *A Monadic Frame-work for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations*</footnote>

<footnote>[CB15] Cadé and Blanchet, "Proved Genera-tion of Implementations from Computation-ally Secure Protocol Specifications"</footnote>

<footnote>[Ho+22] Ho et al., "Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations"</footnote>
using the F* type system to express more guarantees. We would like to write
predicates expressing that an oracle function only adds session entries that
are valid for the following oracles, and other invariants concerning the state.
cv2fstar could then generate lemmas or post-conditions for the extracted
oracle functions using these predicates. We could build stronger lemmas
based on this, to prove that given a valid session ID, if an oracle function
succeeds, all new session entries added by it are valid. This will permit
to prove, using the type system, that a sequential execution of all protocol
functions (oracle calls) is in principle possible.<fnref n="27" />

We want to mention two possible functionality improvements that we
envision for the cv2fstar framework. First, we want to add support for writing
tables to and reading them from a file. Second, as already mentioned in
*Section 6.6*, we could use a cryptographically secure pseudo-random number
generator like HMAC-DRBG to improve the efficiency of random sampling.

Finally, there are various improvements concerning usability that we
consider. First, we would like to generate speaking lemma names instead
of just numbering them. The NSL case study has shown that this is a pain
point for work-in-progress models: Changing the order of type or function
declarations in the CryptoVerif model influences the order in which lemmas
are generated, and thus, it changes their name. This is cumbersome to fix
in NSL.Equations.fst. Second, we might change the handling of imple-
mentation annotations. In the NSL case study, we followed a convention for
all of them, which brought up the idea whether the annotations could be
optional for most cases and use the convention as a default in absence of
an annotation. Third, as an improvement concerning the integration of the
HACL\* library, we could prepare an F\* module for each macro included in
CryptoVerif's default library.

<footnote n="27">²⁷This would still not catch a protocol cor-
rectness bug like the one mentioned in the
previous section.</footnote>
<figure><img src="image_34.png" /></figure>
Part IV

EPILOGUE
<figure><img src="image_35.png" /></figure>
# 7

## Conclusion

In this thesis, we have shown that writing cryptographic proofs using the CryptoVerif proof assistant is practical for the analysis of real-world protocols. We demonstrated this on the examples of the WireGuard VPN protocol and the HPKE standard. In our analyses, we used more detailed models of elliptic curves than any handwritten protocol analysis did before. We hope that our work on these models gets picked up and will be used by others, particularly for protocols that use X25519 or X448 for Diffie-Hellman key agreement. The advent of the ristretto255 and decaf448 groups, currently being standardized by the CFRG [Val+22], might render this less relevant for protocols developed in the future: they provide a prime-order-group abstraction layer around Curve25519 and Curve448, respectively, with only “minor overhead”, and “still allowing the use of high-performance curve implementations internally”. However, given the widespread support of X25519 in cryptographic libraries, we expect this algorithm to still be relevant in practice for a while.

In the WireGuard analysis, we carefully modeled the protocol very close to its actual implementation: we cared in detail about the instantiation of hash and key derivation functions, and considered that X25519 Diffie-Hellman agreement is not using a prime-order group.

In the analysis of HPKE's authenticated mode, we go further and provide concrete security bounds. While the WireGuard analysis took place *after* the protocol was already deployed, the analysis of HPKE was conducted *during* development of the standard. We could provide valuable feedback to the authors, suggested significant design changes that have been incorporated, and in the end became an official co-author of the standard. The two most important design changes were to make the Diffie-Hellman-based KEM IND-CCA-secure on its own, and to introduce thorough oracle separation through labels in hash function calls.

With cv2fstar, we introduced a compiler from CryptoVerif models to executable F* specifications. This allows to guarantee cryptographic properties on executable code. Additionally, because F* is a proof-oriented programming language, or, a proof assistant, we can prove properties about the specific implementation of functions that are only assumed in the CryptoVerif model. This compiler represents another step in connecting analysis tools.

[Val+22] Valence et al., The ristretto255 and decaf448 Groups
## 7.1 PLACEMENT OF MECHANIZED CRYPTOGRAPHIC PROOFS WITHIN THE CRYPTOGRAPHIC COMMUNITY

As mentioned in the introduction, proofs have not always been part of publications within the cryptography community. It has been an important advancement of the community's scientific standards that this is now the case. For the fact that cryptography actually *can* have mathematical proofs, it “is held up as a role model for Science in Security” [Hv17]. Nevertheless, multiple community members have called out a “crisis of rigor”, with proofs being “essentially unverifiable” [BR06]. Thus, maybe it is time to go the next step and bring computer-aided cryptographic proofs to a broader audience. Halevi’s motivational vision published in the year 2005 clearly has not been realized [Hal05]:

> Also, I believe that if a tool like that is built well, it will be adopted and used by many. Wouldn’t you like to be cited by half of the papers appearing in CRYPTO 2010? Here is your chance...

It is debatable whether this was even a reachable goal: the current landscape of cryptographic proof assistants suggests that it is not expectable to have *one* tool that can handle a variety of proof methodologies or security notions, be it game-based, simulation-based, using the UC framework, or the state-separating proofs technique. However, it is clear that even after 17 years we have not even come close to Halevi’s vision. As anecdotic evidence, our paper on the HPKE analysis at Eurocrypt 2021 was the only one using a proof assistant. It seems Rogaway’s statement from 2015 is still true: “formalistic approaches are gone [from cryptography’s tier-1 venues] (unless they claim to bridge to ‘real’ crypto)” [Rog15]. We believe this is because building a cryptographic proof assistant that is expressive enough to handle practically relevant proofs *and* is user-friendly is truly hard and requires an extensive engineering effort. Furthermore, as Halevi already said in 2005, developing a user-friendly proof assistant “does not have a very appealing ‘business case’” [Hal05]. With probably only cryptographers as a relatively small user base for any tool in this space, we have to navigate incentives and funding sources for an effort in making proof assistants more user-friendly. If we want more users, we clearly have to invest in such an effort, because currently, only people in the immediate surroundings of tool developers are able to use cryptographic proof assistants efficiently and effectively. Another option would be to rely on the tool developers and their surroundings as “proof engineers” that can be brought into or contracted for a project – however, it is doubtful whether this approach would scale sufficiently well within the academic cryptography community.<fnref n="1" /> There is a clear demand for computer-assisted proofs, as shown by cryptographers reaching out expressing their interest in using a tool, and standardization bodies being interested in seeing high-assurance proofs of cryptographic systems currently under standardization.

**DO TOOLS ACTUALLY HELP DETECT ERRORS?** In his two articles “Another Look at Automated Theorem-Proving” [Kob07; Kob12], Neal Koblitz asks if proof assistants actually help catch errors of the type that have been

<footnote>[Hv17] Herley and van Oorschot, “SoK: Science, Security and the Elusive Goal of Security as a Scientific Pursuit”</footnote>

<footnote>[BR06] Bellare and Rogaway, “The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs”</footnote>

<footnote>[Hal05] Halevi, *A plausible approach to computer-aided cryptographic proofs*</footnote>

<footnote>[Rog15] Rogaway, *The Moral Character of Cryptographic Work*</footnote>

<footnote n="1">¹The term “proof engineer(ing)” was coined by the sel4 verification project: http://trustworthy.systems/projects/sel4-verification/.</footnote>

<footnote>[Kob07] Koblitz, “Another look at automated theorem-proving”</footnote>

<footnote>[Kob12] Koblitz, “Another look at automated theorem-proving II”</footnote>
embarrassing for the cryptographic community in the past. We want to
mention two cases of proof mistakes in connection to the work presented in
this thesis.

First, for the case of WireGuard, we recall that a handwritten proof was
published by Dowling and Paterson [DP18] before our mechanized proof. In
a work on a post-quantum-secure version of WireGuard, the authors Hülsing,
Ning, Schwabe, Weber, and Zimmermann [Hül+21] build upon the proof by
Dowling and Paterson. Weber found a mistake in the original proof, which
consists in the accidental swapping of two parameters of a KDF, and led to
the realization that a dual PRF assumption is needed to regain a proof.<fnref n="2" />
Such a mistake would probably have been found using a proof assistant like
CryptoVerif or EasyCrypt: either by the type system in case the parameters
of the KDF have different types, or when trying to apply the cryptographic
hardness assumption used for the KDF; using a parameter as KDF key would
be impossible in CryptoVerif if it has not been shown to be indistinguishable
from a randomly sampled value, amongst other conditions. We could not
find this error because we did not formalize Dowling and Paterson's proof
which uses the PRF-ODH assumption in the standard model. We wrote our
proof in the random oracle model because at that time, CryptoVerif was not
yet equipped to handle PRF-ODH assumptions. (Also, it seems implausible
to instantiate PRF-ODH without using a random oracle [Bre+17].) We show
that HKDF-BLAKE2 is a random oracle (assuming that BLAKE2 is a random
oracle), which implies the dual PRF assumption.

Second, we recall that our analysis of HPKE's Auth mode that was pub-
lished at Eurocrypt 2021 contains several handwritten proofs in the appendix
that establish our theorems for 1-user and 2-user security notions. We can
report that an ongoing formalization effort of these proofs by Pierre Boutry
and Christian Doczkal using EasyCrypt surfaced a few subtle errors concern-
ing collisions of public keys and ciphertexts, and the counting of adversary
queries to oracles exposed by the game. These errors have been corrected
in the long version of the paper [Alw+20] and in this thesis.

While it is debatable if these examples constitute embarrassing mistakes,
we believe, in response to Koblitz, that formal methods and proof assistants
do deliver on their promises to detect errors and to produce proofs with a
high assurance.

In their survey about the Science of Security, Herley and van Oorschot
cite DeMillo, Lipton, and Perlis, who express the opinion that (1) “it is a
social process that determines whether mathematicians feel confident about
a theorem”, that (2) “no comparable social process can take place among
program verifiers”, and that (3) “the point is that mathematicians’ errors are
corrected, not by formal symbolic logic, but by other mathematicians”.

Responding to the first and second quote, we believe that the building
up of trust into a proof assistant can be a *separate* social process from the
one determining confidence about a theorem. And we believe that building
up trust into a proof assistant is actually a social process that *can* take place,
just like proof methodologies and styles in cryptography have shifted over
the years, e. g., the cultural shift to code-based proofs. This social process
has not yet converged for CryptoVerif, as we can report on the example of
the HPKE analysis: when we started working with our co-authors, it was

<footnote>[DP18] Dowling and Paterson, “A Crypto-graphic Analysis of the WireGuard Protocol”</footnote>

<footnote>[Hül+21] Hülsing et al., “Post-quantum WireGuard”</footnote>

<footnote n="2">²See Section IV-A in [Hül+21].</footnote>

<footnote>[Bre+17] Brendel et al., “PRF-ODH: Relations, Instantiations, and Impossibility Results”</footnote>

<footnote>[Alw+20] Alwen et al., *Analysing the HPKE Standard*</footnote>
hard for them to even understand the *statements* of the theorems proven in CryptoVerif, because its input language was unknown to them and not close enough to the style known from cryptography papers to be understandable without further explanation.

For a specific proof conducted using a proof assistant, there is still place for a social process to determine whether the community feels confident about the formulation of the theorem in the proof assistant – the benefit of using the proof assistant is that the social process only needs to be about the input to the proof assistant, and not about checking the correctness of the entire proof; of course given that the proof assistant has generally already gained trust. On the specific example of HPKE, we present our theorems and security notions in a way typical for cryptography venues – part of the social process, or review, should then be the confirmation that this representation is equivalent to the implementation in CryptoVerif.

Responding to the third quote, we just want to say that the proof assistants do not act on their own, they are tools *used* by mathematicians or cryptographers that help *them* find errors. At least currently, this seems clear to us, because cryptographic proofs assistants are still expert tools, in the sense that the user has to understand the proof methodology to use the tool in a meaningful way. This might be different from symbolic analysis tools that exhibit a high degree of automation, more or less hiding the underlying formalism.

**PROOF ASSISTANTS AS A FORCING FUNCTION?** In the conclusion of his first essay on automated theorem proving [Kob07], Koblitz asks what the benefit of a proof assistant is, compared to a handwritten proof, “written out clearly and carefully with proper attention to lucid expository style”. This looks like another social effect to us: there rarely seem to be handwritten proofs actually written out in great detail. A proof assistant can be a *forcing function* here, because by design, they require a great level of detail. The notion of a forcing function was used by [Hv17] as a suggestion to resolve the problem of “undocumented and implicit assumptions [that] are common in security research”: “one possibility is to find a *forcing function* to make assumptions explicit”. For cryptography, such a forcing function could be to require computer-verified proofs or at least establish a culture of using proof assistants more. <fnref n="3" /> Then, starting from assumptions underlying the proof assistant, the formal language used by the tool forces users to document everything.

**ARTIFACT EVALUATION.** With mechanized proofs, reproducibility becomes interesting: as proof assistants are evolving, it is not assured that a once-published proof can still be checked by more recent versions of the proof assistant, or, an even more basic requirement, if readers of a paper manage to install the tool and re-check the proof. For now, the community relies on the original authors to publish the original files in a suitable way. When mechanized proofs are getting more popular, we encourage publication venues and the community to adopt the artifact evaluation approach that has been used by the POPL community since 2015 <fnref n="4" /> and by the CHES community since 2021 <fnref n="5" />. The main idea behind artifact evaluation is to

<footnote>[Kob07] Koblitz, "Another look at automated theorem-proving"</footnote>

<footnote>[Hv17] Herley and van Oorschot, "SoK: Science, Security and the Elusive Goal of Security as a Scientific Pursuit"</footnote>

<footnote n="3">³Such a culture is for example present in the POPL community, where it is much more common to formalize the semantics of a newly proposed (research) programming language using a proof assistant.</footnote>

<footnote n="4">⁴https://popl22.sigplan.org/track/POPL-2022-artifact-evaluation</footnote>

<footnote n="5">⁵https://ches.iacr.org/2022/artifacts.php</footnote>
ensure reproducibility and reusability of the code that underlines the results
presented in a paper.

## 7.2 FUTURE WORK

We plan to continue working with cryptographic proof assistants in the area of practice-oriented cryptography both by collaborating with cryptographers on new constructions, and by supporting formal and informal standardization efforts, like within the IETF and IRTF, and for example the Noise protocol framework community. Specific protocols that could be targets of mechanized proofs are the Messaging Layer Security secure group messaging protocol<sup>6</sup> and some of the ongoing standardization efforts within the IRTF's CFRG.<sup>7</sup>

Furthermore, we plan to advance the development of proof assistants on different fronts. On the one hand, improving usability seems crucial to bring mechanized proofs to a wider audience, and we would like to support efforts in this direction. This could be trying to bring some kinds of automation to EasyCrypt, or developing a user-friendly frontend for CryptoVerif or EasyCrypt, inspired by, e. g., the Visual Studio Code extension for the Lean theorem prover, to mention just two ideas.<sup>8</sup> On the other hand, the adaption of proof assistants such that they are able to handle security proofs considering quantum adversaries is an important research direction. There have been first steps done for EasyCrypt [Bar+21] and Squirrel [CFJ22]. Case studies for mechanized proofs could be the candidates of the NIST post-quantum cryptography competition,<sup>9</sup> and post-quantum-secure versions of important protocols, in the spirit of KEMTLS [SSW20] and PQ-WireGuard [Hül+21]. Post-quantum security clearly fits into Rogaway's call for anti-surveillance research, as the first users of large-scale quantum computers might well be state agencies or other global players.

We are looking forward to the first results of the ongoing work on a translation between CryptoVerif and EasyCrypt, and are interested in exploring more potential links between proof assistants. Concretely, we want to finish up some of the ideas mentioned as future work in the cv2fstar chapter, and apply the compiler to our WireGuard models written in CryptoVerif.

Finally, to conclude this thesis, we believe that computer-aided cryptographic proofs are an exciting and in-demand research and development effort, with many promising open problems.

<footnote n="6"><sup>6</sup>https://messaginglayersecurity.rocks/</footnote>

<footnote n="7"><sup>7</sup>https://datatracker.ietf.org/rg/cfrg/documents/</footnote>

<footnote n="8"><sup>8</sup>https://github.com/leanprover/vscode-lean</footnote>

<footnote>[Bar+21] Barbosa et al., "EasyPQC: Verifying Post-Quantum Cryptography"</footnote>

<footnote>[CFJ22] Cremers et al., "A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols"</footnote>

<footnote n="9"><sup>9</sup>https://csrc.nist.gov/Projects/Post-Quantum-Cryptography</footnote>

<footnote>[SSW20] Schwabe et al., "Post-Quantum TLS Without Handshake Signatures"</footnote>

<footnote>[Hül+21] Hülsing et al., "Post-quantum WireGuard"</footnote>
<figure><img src="image_36.png" /></figure>
[AF01] Martín Abadi and Cédric Fournet. "Mobile Values, New Names, and Secure Communication". In: *Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. POPL '01. London, United Kingdom: Association for Computing Machinery, 2001, pp. 104115. ISBN: 1581133367. DOI: 10.1145/360204.360213. URL: https://doi.org/10.1145/360204.360213 (cit. on pp. 14, 15).

[Aba+21] Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Catalin Hritcu, Kenji Maillard, and Bas Spitters. "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq". In: *CSF 2021 Computer Security Foundations Symposium*. Ed. by Ralf Küsters and Dave Naumann. IEEE Computer Society Press, 2021, pp. 1–15. DOI: 10.1109/CSF51468.2021.00048 (cit. on p. 6).

[ABR01] Michel Abdalla, Mihir Bellare, and Phillip Rogaway. "The Oracle Diffie-Hellman Assumptions and an Analysis of DHIES". In: *CT-RSA 2001*. Ed. by David Naccache. Vol. 2020. LNCS. Springer, Heidelberg, Apr. 2001, pp. 143–158. DOI: 10.1007/3-540-45353-9_12 (cit. on p. 83).

[AGJ11] Mihhail Aizatulin, Andy Gordon, and Jan Jürjens. "Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution". In: *CCS '11 Proceedings of the 18th ACM Conference on Computer and Communications Security*. ACM Press, 2011, pp. 331–340. ISBN: 978-1-4503-0948-6. URL: https://www.mi crosoft.com/en-us/research/publication/extracting-verifying-cryptographic-models-c-pro tocol-code-symbolic-execution/ (cit. on p. 128).

[AGJ12] Mihhail Aizatulin, Andy Gordon, and Jan Jürjens. *Computational Verification of C Protocol Implementations by Symbolic Execution*. Tech. rep. MSR-TR-2012-80. CCS '12 Proceedings of the 2012 ACM conference on Computer and communications security. 2012, pp. 712–723. URL: https://www.microsoft.com/en-us /research/publication/computational-verification-of-c-protocol-implementations-by-symbo lic-execution/ (cit. on p. 128).

[Alm+17] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. "Jasmin: High-Assurance and High-Speed Cryptography". In: *Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security*. CCS '17. Dallas, Texas, USA: Association for Computing Machinery, 2017, pp. 18071823. ISBN: 9781450349468. DOI: 10.1145/3133956.3134078. URL: https://doi.org/10.1145/3133956.3134078 (cit. on p. 128).

[Alm+19] José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, and Pierre-Yves Strub. "Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3". In: *Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security*. CCS '19. London, United Kingdom: Association for Computing Machinery, 2019, pp. 16071622. ISBN: 9781450367479. DOI: 10.1145/3319535.3363211. URL: https://doi.org/10.1145/3319535.3363211 (cit. on pp. 5, 128).

[Alw+] Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. *Analysing the HPKE Standard Supplementary Material*. DOI: 10.5281/zenodo.4297811 (cit. on pp. 100, 102, 103, 106, 224, 227).

[Alw+20] Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. *Analysing the HPKE Standard*. Cryptology ePrint Archive, Report 2020/1499. https://eprint.iacr.org/2020/1499. 2020 (cit. on pp. 78, 183).

[Alw+21] Joël Alwen, Bruno Blanchet, Eduard Hauck, Eike Kiltz, Benjamin Lipp, and Doreen Riepel. "Analysing the HPKE Standard". In: *EUROCRYPT 2021, Part I*. Ed. by Anne Canteaut and François-Xavier Standaert. Vol. 12696. LNCS. Springer, Heidelberg, Oct. 2021, pp. 87–116. DOI: 10.1007/978-3-030-77870-5_4 (cit. on pp. 8, 78).

[Aum+13] Jean-Philippe Aumasson, Samuel Neves, Zooko Wilcox-O'Hearn, and Christian Winnerlein. "BLAKE2: Simpler, Smaller, Fast as MD5". In: *Applied Cryptography and Network Security*. Vol. 7954. LNCS. Springer, 2013, pp. 119–135 (cit. on p. 58).

[BHU09] Michael Backes, Dennis Hofheinz, and Dominique Unruh. "CoSP: A General Framework for Computational Soundness Proofs". In: *Proceedings of the 16th ACM Conference on Computer and Communications Security*. CCS '09. Chicago, Illinois, USA: Association for Computing Machinery, 2009, pp. 6678. ISBN: 9781605588940. DOI: 10.1145/1653662.1653672. URL: https://doi.org/10.1145/1653662.1653672 (cit. on p. 128).
[BHM14] Michael Backes, Catalin Hritcu, and Matteo Maffei. "Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations". In: *J. Comput. Secur.* 22.2 (2014), pp. 301–353. DOI: 10.3233/JCS-130493. URL: https://doi.org/10.3233/JCS-130493 (cit. on p. 129).

[Bae+21] David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, and Solène Moreau. "An Interactive Prover for Protocol Verification in the Computational Model". In: *2021 IEEE Symposium on Security and Privacy*. IEEE Computer Society Press, May 2021, pp. 537–554. DOI: 10.1109/SP40001.2021.00078 (cit. on p. 6).

[BC14] Gergei Bana and Hubert Comon-Lundh. "A Computationally Complete Symbolic Attacker for Equivalence Properties". In: *ACM CCS 2014*. Ed. by Gail-Joon Ahn, Moti Yung, and Ninghui Li. ACM Press, Nov. 2014, pp. 609–620. DOI: 10.1145/2660267.2660276 (cit. on p. 6).

[Bar+21] Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, and Li Zhou. "EasyPQC: Verifying Post-Quantum Cryptography". In: *ACM CCS 2021*. Ed. by Giovanni Vigna and Elaine Shi. ACM Press, Nov. 2021, pp. 2564–2586. DOI: 10.1145/3460120.3484567 (cit. on p. 185).

[BAC19] Richard L. Barnes, Joël Alwen, and Sandro Corretti. *Homomorphic Multiplication for X25519 and X448*. Internet Draft. https://tools.ietf.org/html/draft-barnes-cfrg-mult-for-7748-00. IETF, Nov. 2019 (cit. on p. 92).

[Bar+20a] Richard L. Barnes, Benjamin Beurdouche, Jon Millican, E. Omara, K. Cohn-Gordon, and Raphael Robert. *The Messaging Layer Security (MLS) Protocol*. Internet-Draft draft-ietf-mls-protocol-09. IETF Secretariat, Mar. 2020. URL: https://tools.ietf.org/html/draft-ietf-mls-protocol-09 (cit. on p. 79).

[Bar+20b] Richard L. Barnes, Karthik Bhargavan, Benjamin Lipp, and Christopher A. Wood. *Hybrid Public Key Encryption*. Internet-Draft draft-irtf-cfrg-hpke-08. IETF Secretariat, Oct. 2020. URL: https://tools.ietf.org/html/draft-irtf-cfrg-hpke-08 (cit. on p. 79).

[Bar+22] Richard L. Barnes, Karthik Bhargavan, Benjamin Lipp, and Christopher A. Wood. *Hybrid Public Key Encryption*. RFC 9180. RFC Editor, Feb. 2022, pp. 1–107. URL: https://www.rfc-editor.org/rfc/rfc9180.html (cit. on pp. 9, 78, 79, 102, 106, 119).

[Bar+14] Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. "Probabilistic Relational Verification for Cryptographic Implementations". In: *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*. POPL '14. San Diego, California, USA: Association for Computing Machinery, 2014, pp. 193205. ISBN: 9781450325448. DOI: 10.1145/2535838.2535847. URL: https://doi.org/10.1145/2535838.2535847 (cit. on p. 128).

[Bar+11] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. "Computer-Aided Security Proofs for the Working Cryptographer". In: *Advances in Cryptology – CRYPTO 2011*. Ed. by Phillip Rogaway. Berlin, Heidelberg: Springer Berlin Heidelberg, 2011, pp. 71–90. ISBN: 978-3-642-22792-9 (cit. on pp. 5, 14, 128).

[BGZB09] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. "Formal Certification of Code-Based Cryptographic Proofs". In: *SIGPLAN Not.* 44.1 (2009), pp. 90101. ISSN: 0362-1340. DOI: 10.1145/1594834.1480894. URL: https://doi.org/10.1145/1594834.1480894 (cit. on pp. 5, 127).

[Bel15] Mihir Bellare. "New Proofs for NMAC and HMAC: Security without Collision Resistance". In: *Journal of Cryptology* 28.4 (Oct. 2015), pp. 844–878. DOI: 10.1007/s00145-014-9185-x (cit. on p. 105).

[BCK96] Mihir Bellare, Ran Canetti, and Hugo Krawczyk. "Keying Hash Functions for Message Authentication". In: *CRYPTO'96*. Ed. by Neal Koblitz. Vol. 1109. LNCS. Springer, Heidelberg, Aug. 1996, pp. 1–15. DOI: 10.1007/3-540-68697-5_1 (cit. on p. 105).

[BDG20] Mihir Bellare, Hannah Davis, and Felix Günther. "Separate Your Domains: NIST PQC KEMs, Oracle Cloning and Read-Only Indifferentiability". In: *EUROCRYPT 2020, Part II*. Ed. by Anne Canteaut and Yuval Ishai. Vol. 12106. LNCS. Springer, Heidelberg, May 2020, pp. 3–32. DOI: 10.1007/978-3-030-45724-2_1 (cit. on p. 118).

[BN00] Mihir Bellare and Chanathip Namprempre. "Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm". In: *ASIACRYPT'00*. Vol. 1976. LNCS. Springer, Dec. 2000, pp. 531–545 (cit. on pp. 43, 116).

[BR93] Mihir Bellare and Philip Rogaway. "Random Oracles Are Practical: a Paradigm for Designing Efficient Protocols". In: *ACM CCS'93*. ACM Press, 1993, pp. 62–73 (cit. on p. 43).

[BR04] Mihir Bellare and Phillip Rogaway. *Code-Based Game-Playing Proofs and the Security of Triple Encryption*. Cryptology ePrint Archive, Report 2004/331. https://eprint.iacr.org/2004/331. 2004 (cit. on pp. 5, 11, 13, 85).
[BR06] Mihir Bellare and Phillip Rogaway. "The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs". In: *EUROCRYPT 2006*. Ed. by Serge Vaudenay. Vol. 4004. LNCS. Springer, Heidelberg, 2006, pp. 409-426. DOI: 10.1007/11761679_25 (cit. on pp. 4, 182).

[BS20] Mihir Bellare and Igors Stepanovs. "Security Under Message-Derived Keys: Signcryption in iMessage". In: *EUROCRYPT 2020, Part III*. Ed. by Anne Canteaut and Yuval Ishai. Vol. 12107. LNCS. Springer, Heidelberg, May 2020, pp. 507-537. DOI: 10.1007/978-3-030-45727-3_17 (cit. on p. 84).

[BT16] Mihir Bellare and Björn Tackmann. "The Multi-user Security of Authenticated Encryption: AES-GCM in TLS 1.3". In: *CRYPTO 2016, Part I*. Ed. by Matthew Robshaw and Jonathan Katz. Vol. 9814. LNCS. Springer, Heidelberg, Aug. 2016, pp. 247-276. DOI: 10.1007/978-3-662-53018-4_10 (cit. on p. 109).

[Ben+08] Jesper Bengtson, Karthik Bhargavan, Cédric Fournet, Andy Gordon, and Sergio Maffeis. *Refinement Types for Secure Implementations*. Tech. rep. MSR-TR-2008-118. 20th IEEE Computer Security Foundations Symposium (CSF) 2008. 2008, pp. 17-32. URL: https://www.microsoft.com/en-us/research/publication/refinement-types-for-secure-implementations/ (cit. on p. 129).

[Ber+15] Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. "Verified Correctness and Security of OpenSSL HMAC". In: *24th USENIX Security Symposium (USENIX Security 15)*. Washington, D.C.: USENIX Association, Aug. 2015, pp. 207-221. ISBN: 978-1-939133-11-3. URL: https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/beringer (cit. on pp. 6, 128).

[Ber05] Daniel J. Bernstein. "The Poly1305-AES Message-Authentication Code". In: *FSE 2005*. Vol. 3557. LNCS. Springer, 2005, pp. 32-49 (cit. on p. 43).

[Ber06] Daniel J. Bernstein. "Curve25519: New Diffie-Hellman Speed Records". In: *PKC 2006*. Ed. by Moti Yung, Yevgeniy Dodis, Aggelos Kiayias, and Tal Malkin. Vol. 3958. LNCS. Springer, Heidelberg, Apr. 2006, pp. 207-228. DOI: 10.1007/11745853_14 (cit. on pp. 44, 88).

[Ber11] Daniel J. Bernstein. *Extending the Salsa20 nonce*. https://cr.yp.to/snuffle/xsalsa-20110204.pdf. 2011 (cit. on p. 41).

[Beu+15] Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Jean Karim Zinzindohoué. "A Messy State of the Union: Taming the Composite State Machines of TLS". In: *IEEE S&P (Oakland)*. 2015, pp. 535-552 (cit. on p. 34).

[Bha+08a] Karthik Bhargavan, Ricardo Corin, Cédric Fournet, and Eugen Zalinescu. "Cryptographically verified implementations for TLS". In: *15th ACM Conference on Computer and Communications Security (CCS'08)*. Association for Computing Machinery, Inc., 2008. URL: https://www.microsoft.com/en-us/research/publication/cryptographically-verified-implementations-for-tls/ (cit. on p. 128).

[Bha+17] Karthikeyan Bhargavan, Benjamin Beurdouche, Jean-Karim Zinzindohoué, and Jonathan Protzenko. "HACL*: A Verified Modern Cryptographic Library". In: *ACM CCS (2017)*. URL: https://www.microsoft.com/en-us/research/publication/hacl-a-verified-modern-cryptographic-library/ (cit. on pp. 119, 126).

[Bha+21] Karthikeyan Bhargavan, Abhishek Bichhawat, Quoc Huy Do, Pedram Hosseyni, Ralf Küsters, Guido Schmitz, and Tim Würtele. "DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code". In: *EuroS&P 2021 - 6th IEEE European Symposium on Security and Privacy*. Virtual, Austria, Sept. 2021. URL: https://hal.inria.fr/hal-03178425 (cit. on p. 128).

[BBK17] Karthikeyan Bhargavan, Bruno Blanchet, and Nadim Kobeissi. "Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate". In: *2017 IEEE Symposium on Security and Privacy*. IEEE Computer Society Press, May 2017, pp. 483-502. DOI: 10.1109/SP.2017.26 (cit. on pp. 5, 15, 74, 82, 126).

[Bha+14a] Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, and Pierre-Yves Strub. "Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS". In: *IEEE S&P (Oakland)*. 2014, pp. 98-113 (cit. on pp. 34, 67).

[Bha+08b] Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, and Stephen Tse. "Verified Interoperable Implementations of Security Protocols". In: *ACM Trans. Program. Lang. Syst.* 31.1 (2008). ISSN: 0164-0925. DOI: 10.1145/1452044.1452049. URL: https://doi.org/10.1145/1452044.1452049 (cit. on p. 129).

[Bha+13] Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, and Pierre-Yves Strub. "Implementing TLS with Verified Cryptographic Security". In: *2013 IEEE Symposium on Security and Privacy*. 2013, pp. 445-459. DOI: 10.1109/SP.2013.37 (cit. on p. 128).

[Bha+14b] Karthikeyan Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin, and Cédric Fournet. "Proving the TLS Handshake Secure (As It Is)". In: *Advances in Cryptology - CRYPTO 2014*. Vol. 8617. Lecture Notes in Computer Science. Springer, 2014, pp. 235-255. URL: https://www.microsoft.com/en-us/research/publication/proving-the-tls-handshake-secure-as-it-is/ (cit. on p. 128).
[BL16] Karthikeyan Bhargavan and Gaëtan Leurent. "On the Practical (In-)Security of 64-bit Block Ciphers: Collision Attacks on HTTP over TLS and OpenVPN". In: *ACM CCS'16*. 2016, pp. 456–467 (cit. on p. 34).

[Bla07] Bruno Blanchet. "Computationally Sound Mechanized Proofs of Correspondence Assertions". In: *CSF 2007 Computer Security Foundations Symposium*. Ed. by Andrei Sabelfeld. *IEEE Computer Society Press*, 2007, pp. 97–111. DOI: 10.1109/CSF.2007.16 (cit. on pp. 17, 18, 35, 176).

[Bla08] Bruno Blanchet. "A Computationally Sound Mechanized Prover for Security Protocols". In: *IEEE Transactions on Dependable and Secure Computing* 5.4 (2008), pp. 193–207 (cit. on pp. 35, 82, 126).

[Bla12] Bruno Blanchet. "Security Protocol Verification: Symbolic and Computational Models". In: *Principles of Security and Trust, POST'12*. Vol. 7215. LNCS. Springer, 2012, pp. 3–29 (cit. on p. 74).

[Bla16] Bruno Blanchet. "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif". In: *Foundations and Trends in Privacy and Security* 1.1-2 (Oct. 2016), pp. 1–135. ISSN: 2474-1558 (cit. on pp. 5, 34).

[Bla17] Bruno Blanchet. *CryptoVerif: A Computationally-Sound Security Protocol Verifier*. Nov. 20, 2017. URL: https://bblanche.gitlabpages.inria.fr/CryptoVerif/cryptoverif.pdf (cit. on pp. 14–17).

[Bre+17] Jacqueline Brendel, Marc Fischlin, Felix Günther, and Christian Janson. "PRF-ODH: Relations, Instantiations, and Impossibility Results". In: *CRYPTO 2017, Part III*. Ed. by Jonathan Katz and Hovav Shacham. Vol. 10403. LNCS. Springer, Heidelberg, Aug. 2017, pp. 651–681. DOI: 10.1007/978-3-319-63697-9_22 (cit. on pp. 53, 107, 183).

[BCK21] Chris Brzuska, Eric Cornelissen, and Konrad Kohbrok. *Cryptographic Security of the MLS RFC, Draft 11*. Cryptology ePrint Archive, Report 2021/137. https://eprint.iacr.org/2021/137. 2021 (cit. on p. 6).

[Brz+18] Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Konrad Kohbrok, and Markulf Kohlweiss. "State Separation for Code-Based Game-Playing Proofs". In: *ASIACRYPT 2018, Part III*. Ed. by Thomas Peyrin and Steven Galbraith. Vol. 11274. LNCS. Springer, Heidelberg, Dec. 2018, pp. 222–249. DOI: 10.1007/978-3-030-03332-3_9 (cit. on p. 6).

[BAN90] Michael Burrows, Martin Abadi, and Roger Needham. "A Logic of Authentication". In: *ACM Trans. Comput. Syst.* 8.1 (1990), pp. 1836. ISSN: 0734-2071. DOI: 10.1145/77648.77649. URL: https://doi.org/10.1145/77648.77649 (cit. on p. 4).

[CB13] David Cadé and Bruno Blanchet. "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH". In: *Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)* 4.1 (Mar. 2013). Special issue ARES'12, pp. 4–31 (cit. on pp. 126, 127, 133, 167).

[CB15] David Cadé and Bruno Blanchet. "Proved Generation of Implementations from Computationally Secure Protocol Specifications". In: *Journal of Computer Security* 23.3 (2015), pp. 331–402 (cit. on pp. 127, 133, 167, 176).

[Can00] Ran Canetti. *Universally Composable Security: A New Paradigm for Cryptographic Protocols*. Cryptology ePrint Archive, Report 2000/067. https://eprint.iacr.org/2000/067. 2000 (cit. on p. 5).

[CSV19] Ran Canetti, Alley Stoughton, and Mayank Varia. "EasyUC: Using EasyCrypt to Mechanize Proofs of Universally Composable Security". In: *CSF 2019 Computer Security Foundations Symposium*. Ed. by Stephanie Delaune and Limin Jia. *IEEE Computer Society Press*, 2019, pp. 167–183. DOI: 10.1109/CSF.2019.00019 (cit. on p. 5).

[CD09] Sagar Chaki and Anupam Datta. "ASPIER: An Automated Framework for Verifying Security Protocol Implementations". In: *Proceedings of the 2009 22nd IEEE Computer Security Foundations Symposium*. CSF '09. USA: *IEEE Computer Society*, 2009, pp. 172185. ISBN: 9780769537122. DOI: 10.1109/CSF.2009.20. URL: https://doi.org/10.1109/CSF.2009.20 (cit. on p. 129).

[CT08] Liqun Chen and Qiang Tang. "Bilateral Unknown Key-Share Attacks in Key Agreement Protocols". In: *Journal of Universal Computer Science* 14.3 (Feb. 2008), pp. 416–440 (cit. on p. 67).

[CR10] Yannick Chevalier and Michaël Rusinowitch. "Compiling and securing cryptographic protocols". In: *Information Processing Letters* 110.3 (2010), pp. 116–122. ISSN: 0020-0190. DOI: https://doi.org/10.1016/j.pl.2009.11.004. URL: https://www.sciencedirect.com/science/article/pii/S0020019009003251 (cit. on p. 128).

[Cor+08] Ricardo Corin, Pierre-Malo Denielou, Cédric Fournet, Karthik Bhargavan, and James Leifer. "A Secure Compiler for Session Abstractions". In: *Journal of Computer Security (Special issue for CSF'07)* (2008). URL: https://www.microsoft.com/en-us/research/publication/secure-compiler-session-abstractions/ (cit. on p. 128).
[Cor+05] Jean-Sébastien Coron, Yevgeniy Dodis, Cécile Malinaud, and Prashant Puniya. "Merkle-Damgård Revisited: How to Construct a Hash Function". In: CRYPTO 2005. Vol. 3621. LNCS. Springer, 2005, pp. 430-448 (cit. on p. 54).

[CKW11] Véronique Cortier, Steve Kremer, and Bogdan Warinschi. "A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems". In: Journal of Automated Reasoning 46.3 (2011), pp. 225-259. DOI: 10.1007/s10817-010-9187-9. URL: https://doi.org/10.1007/s10817-010-9187-9 (cit. on p. 6).

[CS03] Ronald Cramer and Victor Shoup. "Design and Analysis of Practical Public-Key Encryption Schemes Secure against Adaptive Chosen Ciphertext Attack". In: SIAM Journal on Computing 33.1 (2003), pp. 167-226 (cit. on p. 79).

[CFJ22] Cas Cremers, Caroline Fontaine, and Charlie Jacomme. "A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols". In: S&P 2022 - 43rd IEEE Symposium on Security and Privacy. San Francisco / Virtual, United States, May 2022. URL: https://hal.inria.fr/hal-03620358 (cit. on p. 185).

[CJ19] Cas Cremers and Dennis Jackson. "Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman". In: IEEE CSF'19. To appear. Extended version at https://people.cisp.a.io/cas.cremers/downloads/papers/prime_order_please.pdf. June 2019 (cit. on p. 74).

[DL+17] Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan, Jianyang Pan, and Jean Karim Zinzindohoue. "Implementing and Proving the TLS 1.3 Record Layer". In: SP '17 38th IEEE Symposium on Security and Privacy. 2017. URL: https://www.microsoft.com/en-us/research/publication/implementing-prov-ing-tls-1-3-record-layer/ (cit. on p. 128).

[Den05a] Alexander W. Dent. "Hybrid Signcryption Schemes with Insider Security". In: ACISP 05. Ed. by Colin Boyd and Juan Manuel González Nieto. Vol. 3574. LNCS. Springer, Heidelberg, July 2005, pp. 253-266 (cit. on p. 84).

[Den05b] Alexander W. Dent. "Hybrid Signcryption Schemes with Outsider Security". In: ISC 2005. Ed. by Jianying Zhou, Javier Lopez, Robert H. Deng, and Feng Bao. Vol. 3650. LNCS. Springer, Heidelberg, Sept. 2005, pp. 203-217 (cit. on p. 84).

[DZ10] Alexander W. Dent and Yuliang Zheng, eds. *Practical Signcryption*. Information Security and Cryptography. Springer, 2010. ISBN: 978-3-540-89409-4. DOI: 10.1007/978-3-540-89411-7 (cit. on pp. 83, 84).

[Dod+12] Yevgeniy Dodis, Thomas Ristenpart, John Steinberger, and Stefano Tessaro. "To Hash or Not to Hash Again? (In)Differentiability Results for $H^2$ and HMAC". In: CRYPTO 2012. Vol. 7417. LNCS. Full version at https://eprint.iacr.org/2013/382. Springer, 2012, pp. 348-366 (cit. on pp. 58, 107, 204).

[DY83] Danny Dolev and Andrew C. Yao. "On the Security of Public Key Protocols". In: IEEE Transactions on Information Theory IT-29.12 (Mar. 1983), pp. 198-208. URL: https://doi.org/10.1109/TIT.1983.1056650 (cit. on p. 4).

[Don17] Jason A. Donenfeld. "WireGuard: Next Generation Kernel Network Tunnel". In: Network and Distributed System Security Symposium, NDSS. We use the up-to-date whitepaper version for our analysis, which differs in how the MACs are defined: https://www.wireguard.com/papers/wireguard.pdf, Nov. 2nd, 2017, draft revision ceb3a49. 2017 (cit. on pp. 4, 34-36, 41, 67, 74).

[DM18] Jason A. Donenfeld and Kevin Milner. *Formal Verification of the WireGuard Protocol*. https://www.wireguard.com/papers/wireguard-formal-verification.pdf. 2018 (cit. on pp. 34, 54, 74, 75).

[DP18] Benjamin Dowling and Kenneth G. Paterson. "A Cryptographic Analysis of the WireGuard Protocol". In: Applied Cryptography and Network Security, ACNS 2018. Vol. 10892. LNCS. Springer, 2018, pp. 3-21 (cit. on pp. 7, 35, 53, 54, 74, 75, 183).

[DKO21] François Dupressoir, Konrad Kohbrok, and Sabine Oechsner. *Bringing State-Separating Proofs to EasyCrypt-A Security Proof for Cryptobox*. Cryptology ePrint Archive, Report 2021/326. https://eprint.iacr.org/2021/326. 2021 (cit. on p. 6).

[Dup+11] François Dupressoir, Andy Gordon, Jan Jürjens, and David A. Naumann. *Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols*. Tech. rep. MSR-TR-2011-50. Computer Security Foundations Symposium (CSF), 2011 IEEE 24th. 2011. URL: https://www.microsoft.com/en-us/research/publication/guiding-a-general-purpose-c-verifier-to-prove-cryptographic-protocols-2011/ (cit. on p. 129).

[FM21] Marc Fischlin and Arno Mittelbach. *An Overview of the Hybrid Argument*. Cryptology ePrint Archive, Report 2021/088. https://eprint.iacr.org/2021/088. 2021 (cit. on pp. 11-13, 15).
[FGR09] Cédric Fournet, Gurvan Le Guernic, and Tamara Rezk. "A Security-Preserving Compiler for Distributed Programs". In: *ACM Conference on Computer and Communications Security (CCS'09)*. ACM, 2009, pp. 432–441. URL: https://www.microsoft.com/en-us/research/publication/security-preserving-compiler-distributed-programs/ (cit. on p. 128).

[FKS11] Cédric Fournet, Markulf Kohlweiss, and Pierre-Yves Strub. "Modular code-based cryptographic verification". In: *ACM Conference on Computer and Communications Security*. ACM, 2011, pp. 341–350. ISBN: 978-1-4503-0948-6. URL: https://www.microsoft.com/en-us/research/publication/modular-code-based-cryptographic-verification/ (cit. on p. 128).

[Fro+19] Aymeric Fromherz, Nick Giannarakis, Chris Hawblitzel, Bryan Parno, Aseem Rastogi, and Nikhil Swamy. "A Verified, Efficient Embedding of a Verifiable Assembly Language". In: *Principles of Programming Languages (POPL 2019)*. ACM, 2019. URL: https://www.microsoft.com/en-us/research/publication/a-verified-efficient-embedding-of-a-verifiable-assembly-language/ (cit. on p. 126).

[GM+10] Víctor Gayoso Martínez, F. Alvarez, Luis Hernandez Encinas, and Carmen Sánchez Ávila. "A comparison of the standardized versions of ECIES". In: *2010 6th International Conference on Information Assurance and Security, IAS 2010* (Aug. 2010). DOI: 10.1109/ISIAS.2010.5604194 (cit. on p. 83).

[GH04] Henri Gilbert and Helena Handschuh. "Security Analysis of SHA-256 and Sisters". In: *SAC 2003*. Ed. by Mitsuru Matsui and Robert J. Zuccherato. Vol. 3006. LNCS. Springer, Heidelberg, Aug. 2004, pp. 175–193. DOI: 10.1007/978-3-540-24654-1_13 (cit. on p. 105).

[Gir19] Guillaume Girol. "Formalizing and Verifying the Security Protocols from the Noise Framework". Available at https://doi.org/10.3929/ethz-b-000332859. MA thesis. ETH Zürich, Mar. 2019 (cit. on pp. 75, 76).

[GM84] Shafi Goldwasser and Silvio Micali. "Probabilistic Encryption". In: *Journal of Computer and System Sciences* 28 (1984), pp. 270–299 (cit. on p. 5).

[Gri+19] Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, and Santiago Zanella-Béguelin. *A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations*. 2019. arXiv: 1703.00055 [cs.PL] (cit. on pp. 128, 176).

[GJK21] Yanqi Gu, Stanislaw Jarecki, and Hugo Krawczyk. "KHAPE: Asymmetric PAKE from Key-Hiding Key Exchange". In: *CRYPTO 2021, Part IV*. Ed. by Tal Malkin and Chris Peikert. Vol. 12828. LNCS. Virtual Event: Springer, Heidelberg, Aug. 2021, pp. 701–730. DOI: 10.1007/978-3-030-84259-8_24 (cit. on p. 6).

[Gut+05] Joshua D. Guttman, Jonathan C. Herzog, John D. Ramsdell, and Brian T. Sniffen. "Programming Cryptographic Protocols". In: *Trustworthy Global Computing*. Ed. by Rocco De Nicola and Davide Sangiorgi. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 116–145. ISBN: 978-3-540-31483-7 (cit. on p. 128).

[Haa+18] Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, and Pierre-Yves Strub. "Computer-Aided Proofs for Multiparty Computation with Active Security". In: *CSF 2018 Computer Security Foundations Symposium*. Ed. by Steve Chong and Stephanie Delaune. IEEE Computer Society Press, 2018, pp. 119–131. DOI: 10.1109/CSF.2018.00016 (cit. on p. 5).

[Hal05] Shai Halevi. *A plausible approach to computer-aided cryptographic proofs*. Cryptology ePrint Archive, Report 2005/181. https://eprint.iacr.org/2005/181. 2005 (cit. on pp. 4, 182).

[Hv17] Cormac Herley and Paul C. van Oorschot. "SoK: Science, Security and the Elusive Goal of Security as a Scientific Pursuit". In: *2017 IEEE Symposium on Security and Privacy*. IEEE Computer Society Press, May 2017, pp. 99–120. DOI: 10.1109/SP.2017.38 (cit. on pp. 3, 182, 184).

[Ho+22] S. Ho, J. Protzenko, A. Bichhawat, and K. Bhargavan. "Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations". In: *2022 2022 IEEE Symposium on Security and Privacy (SP) (SP)*. Los Alamitos, CA, USA: IEEE Computer Society, 2022, pp. 650–667. DOI: 10.1109/SP46214.2022.00038. URL: https://doi.ieeecomputersociety.org/10.1109/SP46214.2022.00038 (cit. on pp. 128, 176).

[Hül+21] Andreas Hülsing, Kai-Chun Ning, Peter Schwabe, Florian Weber, and Philip R. Zimmermann. "Post-quantum WireGuard". In: *2021 IEEE Symposium on Security and Privacy*. IEEE Computer Society Press, May 2021, pp. 304–321. DOI: 10.1109/SP40001.2021.00030 (cit. on pp. 183, 185).

[Jag+12] Tibor Jager, Florian Kohlar, Sven Schäge, and Jörg Schwenk. "On the Security of TLS-DHE in the Standard Model". In: *CRYPTO 2012*. Vol. 7417. LNCS. Springer, 2012, pp. 273–293 (cit. on pp. 7, 61).

[KY05] S. Kent and K. Yao. *Security Architecture for the Internet Protocol*. IETF RFC 4301. 2005 (cit. on p. 34).

[KNB19] N. Kobeissi, G. Nicolas, and K. Bhargavan. "Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols". In: *2019 IEEE European Symposium on Security and Privacy (EuroS&P)*. Los Alamitos, CA, USA: IEEE Computer Society, 2019, pp. 356–370. DOI: 10.1109/EuroSP.2019.00034. URL: https://doi.ieeecomputersociety.org/10.1109/EuroSP.2019.00034 (cit. on pp. 74, 75, 128).