Bruno Blanchet
email: bruno.blanchet@inria.fr

Pierre Boutry
email: pierre.boutry@inria

Christian Doczkal
email: christian.doczkal@mpi-sp.org

Benjamin Grégoire
email: benjamin.gregoire@inria.fr

Pierre-Yves Strub
email: pierre-yves@strub.nu

CV2EC: Getting the Best of Both Worlds

Keywords: security protocols, computational model, mechanized proofs, combining tools

We define and implement CV2EC, a translation from CryptoVerif assumptions on primitives to EasyCrypt games. CryptoVerif and EasyCrypt are two proof tools for mechanizing game-based proofs. While CryptoVerif is primarily suited for verifying security protocols, EasyCrypt has the expressive power for verifying cryptographic primitives and schemes. CV2EC allows us to prove security protocols in CryptoVerif and then use EasyCrypt to prove the assumptions made in CryptoVerif, either directly or by reducing them to lower-level or more standard cryptographic assumptions. We apply this approach to several case studies: we prove the multikey computational and gap Diffie-Hellman assumptions used in CryptoVerif from the standard version of these assumptions; we also prove an n-user security property of authenticated key encapsulation mechanisms (KEMs), used in the CryptoVerif study of hybrid public-key encryption (HPKE), from the 2-user version. By doing that, we discovered errors in the paper proof of this property, which we reported to the authors who then fixed their proof.

I. INTRODUCTION

After three decades of active research on the verification of security protocols, there now exists a plethora of tools in this area. The first tools relied on the symbolic model of cryptography, also called Dolev-Yao model [START_REF] Dolev | On the security of public key protocols[END_REF], in which cryptographic primitives are considered as ideal blackboxes, the messages are terms on these primitives, and the adversary is restricted to apply only these primitives. ProVerif [START_REF]Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF] and Tamarin [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF] are two widely-used tools based on this approach. Later, tools were developed that rely on the computational model of cryptography, the model used by cryptographers in their (manual) proofs. This model is more realistic than the symbolic model: messages are bit strings, cryptographic primitives are functions from bit strings to bit strings, and the adversary is any probabilistic Turing machine. Several tools rely on this model: CryptoVerif [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF], EasyCrypt [START_REF] Barthe | Computeraided security proofs for the working cryptographer[END_REF], FCF [START_REF] Petcher | The foundational cryptography framework[END_REF], CryptHOL [START_REF] Basin | CryptHOL: Game-based proofs in higher-order logic[END_REF], Squirrel [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF], OWL [START_REF] Gancher | OWL: Compositional verification of security protocols via an information-flow type system[END_REF].

Each of these tools has its own strengths and limitations. For instance, symbolic tools are usually highly automated and may even find attacks against insecure protocols. However, these tools are usually not sound in the computational model. Tools based on the computational model provide stronger guarantees than those obtained by symbolic tools, because they consider a stronger adversary. Among computational tools, CryptoVerif provides a high degree of automation; in particular, it generates the cryptographic games. On the other hand, EasyCrypt, FCF, and CryptHOL provide the expressive power to support general mathematical reasoning. This comes at the cost of providing less automation and making things explicit that are implicit in CryptoVerif: the user has to give the games and guide proofs of indistinguishability between games. Squirrel relies on a logic that allows it to use symbolic techniques and be computationally sound. Still, it currently proves a security notion weaker than the standard one: the number of sessions of the protocol must be bounded independently of the security parameter (instead of being polynomial in the security parameter). OWL relies on typing and offers a high automation level but it is more limited in terms primitives that it can support. Therefore, no single tool solves all problems of security protocol verification, and we believe that one should combine tools in order to get the best result.

In this paper, we combine EasyCrypt and CryptoVerif. Thanks to its support for general purpose mathematical reasoning, EasyCrypt is particularly suited for proving cryptographic schemes, but using it for proving large security protocols becomes more tedious because the user has to write many large cryptographic games. In contrast, CryptoVerif is primarily suited for proving protocols, because of its higher level of automation but more limited cryptographic reasoning. Cryp-toVerif requires assumptions on primitives to be given in the form of indistinguishability axioms between two cryptographic games. Moreover, these axioms sometimes differ from the standard way in which cryptographers present the considered assumptions. For instance, CryptoVerif sometimes requires the assumptions to be expressed for n keys, while the standard way of writing it is for a single key. Therefore, our goal is to use CryptoVerif to prove properties of security protocols from assumptions on primitives, and use EasyCrypt to prove these assumptions directly or from lower-level or more standard cryptographic assumptions.

In order to achieve this goal, we define and implement an automatic translation from CryptoVerif assumptions on primitives into EasyCrypt games. This translation encodes the semantics of CryptoVerif assumptions in EasyCrypt. We can then reason in EasyCrypt on the output of the translation and prove the assumptions expected by CryptoVerif. Even though both tools were developed to mechanize game-based proofs, they are still very different. The CryptoVerif language defines a collection of oracles that can be called by the adversary. In this language, all variables are implicitly arrays, which is rather non-standard but helpful to remember the state of the whole game. In EasyCrypt, games are expressed using a while language with procedures. Our translation takes into account these differences and other subtleties in semantics of cryptographic assumptions in CryptoVerif as detailed in Section III. Our translation is included in CryptoVerif 2.08 available at https:// cryptoverif.inria.fr. The file cv2EasyCrypt/README.txt in that distribution gives details on how to run our examples.

We apply this approach to several case studies, detailed in Section IV. As a first example, we reduce the n query "real/ideal" formulation of the IND-CCA2 assumption in CryptoVerif to the standard formulation. We also reduce the n-user games for authenticated key encapsulation mechanisms (KEMs) to the 2-user version, for the Outsider-CCA property (basically IND-CCA security of the KEM when the adversary does not choose the secret keys used to produce challenge ciphertexts). This proof was done on paper in [START_REF] Alwen | Analysing the hpke standard[END_REF]Appendix A.1]. In the course of our work, we discovered errors in this paper proof. We reported them to the authors, who then fixed their proof in the last version of [START_REF] Alwen | Analysing the hpke standard[END_REF]. Finally, we show computational Diffie-Hellman (CDH) and gap Diffie-Hellman (GDH) [START_REF] Okamoto | The gap-problems: a new class of problems for the security of cryptographic schemes[END_REF] assumptions used by CryptoVerif, which allow generating Diffie-Hellman values g aibj for n randomly chosen a i and m randomly chosen b j , from standard CDH and GDH assumptions for a single Diffie-Hellman pair. The proof relies on the random self-reducibility of CDH and GDH in order to optimize the obtained probability bound. It is valid for primeorder groups, as well as for modern Diffie-Hellman structures like Curve25519 and Curve448 [START_REF] Langley | Elliptic curves for security[END_REF], which are not exactly groups. Simplified versions of these results were proved on paper in [START_REF]Automatically verified mechanized proof of one-encryption key exchange[END_REF] for CDH and [START_REF] Alwen | Analysing the hpke standard[END_REF] for GDH; we extend and mechanize them. These case studies were chosen to cover a variety of assumptions and show the applicability of the approach.

Related Work: Other ways of combining protocol verification tools also exist. At the symbolic level, SAPIC [START_REF] Kremer | Automated analysis of security protocols with global state[END_REF] and its extension SAPIC+ [START_REF] Cheval | Sapic+: protocol verifiers of the world, unite![END_REF] allow translating the same input model into inputs for three different symbolic tools: ProVerif [START_REF]Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF], Tamarin [START_REF] Schmidt | Automated analysis of Diffie-Hellman protocols and advanced security properties[END_REF], and DEEPSEC [START_REF] Cheval | DEEPSEC: deciding equivalence properties in security protocols theory and practice[END_REF], a tool that proves equivalence properties between two protocols, for a bounded number of executions of the protocols. That allows proving some properties using one tool and others using another tool, from a single file. The support for lemmas and axioms in Tamarin and ProVerif [START_REF] Blanchet | ProVerif with lemmas, induction, fast subsumption, and much more[END_REF] also opens the possibility of proving a lemma in one tool and using it as axiom in another tool, which is also what we do, although in a different context.

At the computational level, CV2F ⋆ (included in Cryp-toVerif 2.08 available at https://cryptoverif.inria.fr) translates CryptoVerif models into protocol implementations in F ⋆ (https: //fstar-lang.org/), a proof-oriented functional language with dependent types. It extends a previous translation to OCaml [START_REF] Cadé | Proved generation of implementations from computationally secure protocol specifications[END_REF] by generating F ⋆ lemmas for equations that are used as assumptions on cryptographic primitives in CryptoVerif. These lemmas can then be proved in F ⋆ on the implementation of the primitive. However, F ⋆ is not very suitable for proving indistinguishability axioms, also used as assumptions on cryptographic primitives in CryptoVerif; EasyCrypt, which we use in this work, is much more suitable for that task.

Combinations between symbolic and computational tools can also be considered. In particular, the tools ProVerif and CryptoVerif share a large common subset of their input language for describing protocols. That allows users to first verify a protocol at the symbolic level in ProVerif, trying to find attacks. If no attack is found, one can then verify the protocol at the computational level in CryptoVerif, which gives a stronger security result but is also more difficult.

II. BACKGROUND ON EASYCRYPT

EasyCrypt is a proof assistant geared towards proving properties of probabilistic programs. As a proof assistant, it provides a functional language to define types, operators, and logical formulas. On top of this, EasyCrypt provides a small imperative WHILE language to describe probabilistic programs. The language provides the usual control flow instructions (conditional, while loop, function call), assignment, and a special instruction allowing to sample a value from a (sub-)distribution (i.e., a distribution whose total probability mass may be less than 1), making the language probabilistic.

The semantics of a statement takes a memory (a mapping from variables to values) and returns a distribution over memories. The semantics of procedures takes a memory and a value (possibly a tuple) and returns a distribution over values × memories (i.e the return value and the final memory). 1 Since procedures are semantically indexed distributions, we can talk about the probability of events after executing procedures:

Pr[G(v) @ m : E]
The meaning of this judgment is the probability of the event E (a predicate depending on the return value and the final memory) in the distribution corresponding to the semantics of G starting from the initial memory m and the argument v.

EasyCrypt follows the game-based proofs paradigm. In this setting, security notions are expressed using games between the security scheme and the adversary. All components are represented using (high-order) probabilistic programs. For instance, a game can be parametrized by a scheme and an adversary, where the adversary has potentially access to oracles.

The high-order aspect is captured using a module system. A module is a collection of procedures and global variables. A functor is a function from modules to modules. For instance, adversaries are usually functors that expect modules as arguments (the oracles) and return a collection of procedures. A module type, or signature, is a collection of procedure type declarations. It specifies the input and output types of procedures a module of this type should provide.

The logic of EasyCrypt allows quantification over modules of a given module type (e.g. the type of adversaries for some security game G and some scheme S), allowing us to express bounds on the advantage of an adversary against a game:

∀(A : Adv) m. |Pr[G(A, S).main(v) @ m : E] - 1 2 | ≤ ϵ(A)
This kind of quantification is usually too strong to obtain a provable statement. It is generally necessary to restrict to adversaries that cannot access certain parts of the memory. For example, if the game stores a secret key in memory, security can generally only be proved for adversaries that do not have access to the secret key. Thus quantification over modules generally comes with some memory restrictions:

∀(A : Adv{-G, -S}). . . .
This means that the quantification is restricted to modules of type Adv that to not have (direct) access to the global variables of the modules G and S.

On top of the logic described above, EasyCrypt offers the notion of theories. A theory is a collection of types, operators, axioms, modules, and lemmas. Types, operators, and axioms can be declared without providing a concrete definition (or proof in the case of axioms). It is then possible to refine a theory by instantiating declared types and operators with concrete definitions and proving the axioms stated about them. This systematically refines all the types, operators, and lemmas in the theory. While this operation is called cloning in EasyCrypt we use the word instantiation in the remainder of the paper.

III. TRANSLATION FROM CRYPTOVERIF TO EASYCRYPT

CryptoVerif specifies assumptions on primitives as indistinguishability axioms L ≈ p R, meaning that an adversary has probability at most p of distinguishing the left-hand side L from the right-hand side R. (p is typically a function of the runtime of the adversary, the number of calls to oracles, and possibly other parameters.) CryptoVerif then uses these axioms by replacing L with R inside a bigger game [START_REF] Blanchet | A computationally sound mechanized prover for security protocols[END_REF].

We now describe the translation from CryptoVerif indistinguishability axioms to EasyCrypt games. We do this by giving two extended examples which together cover most of the relevant features of the language of CryptoVerif. For each example, we explain its semantics in CryptoVerif and how we translate it to EasyCrypt. We then briefly mention some of the features not covered by the examples.

A. IND-CPA Security

Our first example is the IND-CPA security game for a symmetric encryption primitive. In this game, the adversary is trying to distinguish an honest encryption oracle from an oracle that encrypts the zero string of the appropriate length. While simple, this example allows us to explain most of the core ideas behind the translation.

The CryptoVerif code of these games can be found in Fig. 1. The first four lines declare the types used in the game. In the order given: plaintexts, ciphertexts, encryption keys, and encryption seeds. Semantically, types are sets of bit strings, but CryptoVerif treats all types abstractly. Lines 6 and 7 declare the function symbols enc and Z. CryptoVerif assumes that all declared functions are effectively computable. The intended interpretation is that enc is an encryption function, and Z returns the zero string of the same length as its input. 2 The rest of the figure describes the actual indistinguishability axiom. The general form is equiv(name) L ⇐(p)⇒R, where L and R are oracle structures. These consist of a tree of random choices (e.g. k ← $ key) and replications (e.g. foreach i ≤ N do) with oracle definitions at the leaves (e.g. Oenc(x:cleartext) :=...). A random choice x ← $ T samples a value according the default distribution of the type T and stores it in x. The default distribution depends on the annotation of the type: for fixed (i.e. fixed-length bit strings) and bounded (i.e. finite types) the distribution is uniform; the annotation nonuniform leaves the distribution unspecified (it must however be lossless, i.e. not a subdistribution). A replication foreach i ≤ N, where N is a declared parameter, provides N copies of the code following it. In particular, the adversary may call each (copy of a replicated) oracle at most once. Oracles (e.g. Oenc) may take input from the adversary and perform some computation (e.g. returning the value of an expression).

CryptoVerif ensures that the two sides of the equivalence are compatible (i.e., they provide access to the same collection of oracles), and the description of the adversary trying to distinguish the two sides is given implicitly by this shared signature. Moreover, every sequence of random choices (e.g. lines 13, 15, 18, and 20) gives rise to an implicit oracle, allowing the adversary to decide when these choices are made. This is subject to the constraint that before an (implicit) oracle can be called, all oracles above it in the oracle structure must have been called.

Finally, all variables in CryptoVerif are arrays, indexed by the current replication indices at their definition (i.e. the indices of replications above that definition in the oracle structure). When a variable is accessed with the same indices as at its definition, the indices can be suppressed. In particular, a variable defined outside of any replication has no indices. A fully explicit rendering of lines 13 to 16 would be:

13 k[] ← $ key; 14 foreach i ≤ N do 15 r[i] ← $ enc seed; 16 Oenc(x[i]:cleartext) := return(enc(x[i], k[], r[i]))
We now describe the translation of the example in Fig. 1 to EasyCrypt. We start by translating the declared types and function symbols. This mostly amounts to declaring as the corresponding types and functions in EasyCrypt: For the types tagged as bounded, we add an axiom asserting that the type is finite (i.e. can be enumerated by a finite list). Here, <: > is EasyCrypt syntax for passing type arguments to polymorphic definitions. In particular, the finiteness axioms ensure that the uniform distribution on the respective type is well defined. For the parameter N, we declare an (abstract) integer constant b N.

1 type ciphertext.
As it comes to the indistinguishability axiom (i.e. from line 12 onward), we represent each side of the equivalence as a module. Since EasyCrypt, unlike CryptoVerif, does not have built-in notions of games and adversaries, we have to make these notions explicit first (cf. Fig. 2). We first define the module types Oracles end Oracles i. The former specifies all the procedures that the adversary is given access to, while the latter also includes an initialization procedure called by the game but inaccessible to the adversary. An Adversary is then a functor taking a module implementing the Oracles module type (e.g., the translation of the LHS or the RHS of the equiv described below) and providing a procedure distinguish. The Game then takes a collection of oracles with initialization procedure and an adversary, initializes the oracle, passes it to the adversary, and calls the procedure distinguish. Note that only the module type Oracles depends on the equivalence being extracted. Thus, while having to describe the game adds a certain amount of boilerplate, this is essentially the same for all extracted equivalences.

We now describe the translation of oracle structures, the most crucial part of the translation. We first describe the module for the LHS. The complete module is given in Fig. 3. Every module representing an oracle structure provides three types of procedures: a procedure init that initializes the state of the module and is not exposed to the adversary, procedures whose names start with r that correspond to the implicit oracles for sequences of random choices, and procedures whose names starts with p that correspond to the oracle procedures present in the CryptoVerif code.

We handle replicated random sequences and oracles (i.e. those under a foreach i ≤ N do replication) by adding the indices i of the replications above them as integer arguments of the corresponding procedure. We also introduce for every oracle procedure (both implicit and explicit) a finite map from index arguments to non-index arguments, or unit if there are none (c.f. lines [START_REF] Baelde | An interactive prover for protocol verification in the computational model[END_REF][START_REF] Barbosa | Mechanized proofs of adversarial complexity and application to universal composability[END_REF][START_REF] Barthe | Computeraided security proofs for the working cryptographer[END_REF]). These maps store all oracle procedure calls that have been performed. They are used for two main purposes: ensuring that replicated oracles are called at most once on any combination of (valid) indices, and enforcing the order restrictions on oracle calls (e.g. that for all k, r i(k) must be called before p Oenc(k, x) may be called for any x). This is realized by wrapping the body of every oracle in an if statement. 3 For explicit oracles we also store the

} proc r() = { if (() / ∈ m r) { m r.[()] ← (); O k.sample(); } } proc r i(i : int) = { if (1 ≤ i ≤ b N ∧ () ∈ m r ∧ i / ∈ m r i) { m r i.[i] ← (); O r.sample(i); } } proc p Oenc(i : int, x : cleartext) = { var aout : ciphertext ← witness;
var tmp k : key; var tmp r i : enc seed; Perhaps most surprising is our translation of the random variables k and r. A naive translation would employ finite maps from indices to values, similar to the maps storing oracle arguments. We use an equivalent translation that, as will become clear later, is more convenient to use in EasyCrypt proofs. For every random variable x, we introduce a module parameter O x. The default implementation for these modules, return witness, an arbitrary but fixed/known value, making such calls useless/irrelevant. which we call random oracles, is just a wrapper around a finite map from indices to sampled values: init() empties the map, sample(i) samples the value for index i according to the default distribution of the type (e.g., the uniform distribution for types tagged as fixed or bounded) and stores it in the map, and get(i) retrieves the value for i from the map (sampling one and storing it if necessary). Thus, the full translation of the LHS consists of the parameterized module LHS applied to default implementations for all random oracles (cf. line 44). The translation of the RHS is analogous.

if (1 ≤ i ≤ b N ∧ i ∈ m r i ∧ i / ∈ m Oenc) { m Oenc.[i] ← x; tmp k ← O k.get (
All parts of the translation (i.e. types, axioms, operators, and modules) are put into a theory. The user should then prove in EasyCrypt the indistinguishability of the two generated games for some instantiation of the generated theory. In particular, the user should instantiate the operators according to their intended meaning (e.g., enc should be instantiated with an encryption function). The details of the instantiation depend on the context: it may be proven for any IND-CPA encryption scheme, if the user only assumes IND-CPA for the scheme in EasyCrypt; it may also be proven for a particular encryption mode, for example, in case the EasyCrypt theory is instantiated with a definition of that mode. For the EasyCrypt proof to apply to the implementation of a protocol, the instance proven in EasyCrypt must contain the primitive that is actually used in the implementation.

Ideally, the translation of the indistinguishability axiom defined in CryptoVerif for the IND-CPA security should be something of the form:

op Penc : int → int → int → real. axiom LHS RHS &m (A <: Adversary{-LHS, -RHS}):
| Pr[Game(LHS, A).main() @ &m : res] -Pr[Game(RHS, A).main() @ &m : res] | ≤ Penc(time, N, maxlength(x)).

where Penc would be an abstract operator to be instantiated by the user, and the axiom would need to be proved. While this may be possible in principle, there are several reasons why we did not proceed this way.

Due to the dependence of Penc on time, we would need to restrict the quantification for A to time-bounded adversaries. While this is possible in EasyCrypt, this would require the user of our tool to use the cost logic of EasyCrypt [START_REF] Barbosa | Mechanized proofs of adversarial complexity and application to universal composability[END_REF]. This logic was only added to EasyCrypt recently and is currently not easy to use. Consequently, security bounds in EasyCrypt are predominantly stated with respect to a concrete reduction. That is, one proves that the advantage of some universally quantified adversary A against some security game can be bounded in terms of some adversary B(A) against a more basic security notion. Here, B is a concrete reduction that becomes part of the theorem statement. One therefore has to check that, in addition to invoking A, B(A) does not perform excessive computations. Given that most reductions do not go beyond keeping logs or counters and performing a constant number of (low cost) operations before/after calling A, this is usually neither difficult nor error-prone.

We still want to aid the user in proving the right statement about the extracted games (cf. Section III-C3). Therefore, we emit the lemma that needs to be proved as a comment, leaving a hole for the bound. This allows the user to decide whether he wants to express the bound in EasyCrypt using a fixed reduction or whether he wants to use the cost logic to obtain a more self-contained statement. For our example, we emit: lemma LHS RHS (A <: Adversary{-LHS, -RHS}) &m:

(forall (O <: Oracles{-A}), islossless O.r ⇒islossless O.r i ⇒islossless O.p Oenc ⇒islossless A(O).distinguish) ⇒ | Pr[Game(LHS, A).main() @ &m : res] -Pr[Game(RHS, A).main() @ &m : res] | ≤ <bound>.

Here, the predicate islossless O.r asserts that the procedure O.r terminates with probability 1. Thus, the assumption of the lemma asserts that running the adversary terminates provided all the oracles that it is given access to do. This hypothesis is justified, because CryptoVerif only considers terminating adversaries.

B. IND-CCA2

Our next example is IND-CCA2 security for a public key encryption scheme. The indistinguishability axiom is given in Fig. 4. For reasons of space, we suppress the declaration of those types and operators that are similar to the previous example. That is, we now sample a keyseed rather than a key and use pkgen/skgen to derive public/private keys as needed.

The main difference to the IND-CPA game is that the adversary is now given access to a decryption oracle. Decryption differs from encryption in that it can fail on certain inputs. For this purpose, CryptoVerif uses the special type bitstringbot. This type is interpreted as the type of all bit strings plus a special element bottom indicating failure. The translation treats this type specially: it is translated to the type bitstring option, where the type bitstring is assumed to be countably infinite.

if (1 ≤ i2 ≤ b N2 ∧ () ∈ m r ∧ i2 / ∈ m Odec) { 8 m Odec.[i2] ← c;
The second difference is that the decryption oracle on the RHS needs access to preceding encryption queries in order to stay consistent with the encryption oracle (which encrypts zero strings). For this, the game employs a table called cipher. Semantically, a table is a set of rows of the declared signature. The command insert cipher(m, c1) inserts the pair (m, c1) into the table. The command get cipher(m1, =c) in ... else ... checks whether the table contains rows whose second component equals c. If it does, it chooses a matching row uniformly at random, stores the first component of that row in the variable m1, and executes the in branch. Otherwise, the else branch is executed. Note that m1 is an array variable (i.e. it may be accessed from other oracles).

In EasyCrypt, we represent the table as a list. The part of the translation that deals with table access is given in Fig. 5 (insert just adds the pair to the list and is not shown). The first part (lines 9 to 13) computes the list of possible values for m1 (if the get binds multiple values, this will be a list of tuples). Here, the function List.pmap takes a function f : α → β option and a list s : α list and returns the list of y such that f (x) = Some(y) for some x in s. If the list of possible values is empty, we execute (the translation of) the else branch. Otherwise, we use the distribution operator drat to sample a value uniformly from the list of possible values. We then store this value in a map v m1 before executing the translation of the then branch. Generally, whenever a variable is defined (e.g. also in Fig. 4 line 24), the translation creates a map storing the value of this variable for different replication indices.

1 k ← $ keyseed; ( 2 Opk() := return(pkgen(k)) | 3 foreach i2 ≤ N2 do Odec(c:ciphertext) := 4 find j ≤ N 5 suchthat defined(c1[j],m[j]) & c = c1[j]
In addition to the indistinguishability axiom, the code in Fig. 4 also contains an equation stating the correctness of the encryption scheme (c.f. line 4). CryptoVerif applies such equations eagerly during proof search. All equations sharing function symbols with the equivalence being extracted are translated to axioms in EasyCrypt. Thus, in addition to proving that the indistinguishability property holds for the instance provided by the user, the user should prove that the instance satisfies all the equations assumed by CryptoVerif. In addition to explicit equational axioms, functions tagged with [data] are assumed to be injective, and the translation generates the corresponding injectivity axiom.

Instead of using a table, the RHS of Fig. 4 can also be written using a find construct. This is shown in Fig. 6. The find construct (lines 4 to 7) checks whether there exist indices j satisfying the condition following the suchthat. Here, defined(...) checks that the variables passed as arguments have been defined. If there exist indices satisfying the suchthat clause, j is chosen uniformly at random among these indices and the then branch is executed. Otherwise, the else branch is executed. The translation to EasyCrypt (cf. Fig. 7) first filters the list of all possible indices (e.g. in our example this is the list [1,..,b N] written iota 1 b N in EasyCrypt) and then, similar to the translation of get, executes either the else branch or the then branch with a matching index chosen uniformly at random. If the condition involves random variables, which is not the case in our example, checking the condition requires access to the map stored in the corresponding random oracle. In those cases, we change the type and implementation of the random oracle to one that exposes the internal map (see also Section IV-A). CryptoVerif supports find statements of the form find i 1 ≤ N 1 , ..., i k ≤ N k suchthat... searching for combinations of indices. In this case, we construct the list of all combinations of indices satisfying the condition and then select one of these combinations uniformly at random.

Internally, CryptoVerif expands tables to variable definitions and find statements. Thus, we could have chosen to only translate find statements. However, reasoning about the rows of a table is often more natural (i.e. closer to textbook arguments employing logs) than reasoning about array variables. In particular, reasoning about find statements usually requires complicated invariants relating the values of multiple array variables at certain indices. For tables, it is often sufficient to quantify over the rows in the table.

1 proc p Odec(i2 : int, c : ciphertext) = { 2 ... 3 if (...) { 4 m Odec.[i2] ← c; 5 j list ← List.filter (fun j ⇒ 6 (j ∈ v c1 ∧ j ∈ m Oenc) ∧ c = (oget v c1.[j])) 7 (iota 1 b N); 8 if (j list = []) { 9 tmp k ← O k.get();
C. Other Features 1) Arguments of Oracles used as Indices: In the left-hand side L, CryptoVerif allows array accesses x[j 1 , . . . , j m ] where x is any variable and j 1 , . . . , j m are arguments of the oracle O. In this case, oracle O can be called only when x is defined at indices j 1 , . . . , j m . Although this condition on oracle O is specified by looking only at the left-hand side L, it also applies to calls to O in the right-hand side R.

While this point may be counter-intuitive, it is motivated as follows: the indistinguishability axiom L ≈ p R is used to replace oracles of L with oracles of R in some game. If an array access x[j 1 , . . . , j m ] occurs in a term M , equal to the term returned by O, in the initial game, then that array access is guaranteed to be defined in the (initial) game. After the replacement of oracles of L with oracles of R, the same access x[j 1 , . . . , j m ] is still guaranteed to be defined in the (transformed) game.

Accordingly, the EasyCrypt translation verifies that these variables x[j 1 , . . . , j m ] are defined at the beginning of the translation of O, and returns immediately with the uninformative result witness when they are not.

2) unchanged: Some random choices in the right-hand side R may be marked [unchanged], when there is a randomly chosen variable of the same name and type in the matching sequence of random choices in the left-hand side L. Intuitively, this annotation means that the value of this random choice remains unchanged when we replace L with R. This annotation allows CryptoVerif to replace L with R inside a game in which variables marked [unchanged] occur as arguments of events: the adversary observes the events at the end of the game and will not be able to use these variables to distinguish the transformed game from the initial game, since the value of these variables is unchanged.

Formally, it means that the probability bound for distinguishing L from R applies even when the adversary is given access to the values of these random choices after executing all calls to oracles of L, resp. R. The translation captures this by adapting the security game accordingly (cf. Fig. 8). Here, S.unchanged is a procedure, inaccessible to the adversary because the module type of the adversary does not mention it, returning the finite maps storing all the values of the array variables tagged as unchanged. Further, the annotation {} (Fig. 8 line 3) ensures that the procedure A(S).guess cannot make (further) calls to the oracles provided by S.

3) events: CryptoVerif allows events to happen in the righthand side of the equivalence. These events are taken into account in the translation by setting a variable and adapting the formula of the probability to be bounded to include the probability of these events. CryptoVerif considers two categories of events.

First, CryptoVerif supports annotating find and get with [unique]. In the presence of this annotation, rather than sampling a matching replication index or table row uniformly at random, the game only selects an index/row if the choice is unique. If the choice is not unique, the game aborts with an event that is visible to the adversary. Due to a syntactic restriction in CryptoVerif, this can only happen on the righthand side, effectively telling the adversary that it is interacting with that side.

In the translation, when the RHS contains a [unique] annotation, we introduce a variable RHS .not unique that is set to true whenever there is more than one choice. For these games, the formula that the user should prove becomes:

| Pr[Game(LHS, A).main() @ &m : res] -Pr[Game(RHS, A).main() @ &m : res ∨ RHS .not unique]| ≤ <bound> By negating the result of the adversary, we can show that this formula is equivalent to Pr[Game(LHS, A).main() @ &m : res] ≤ Pr[Game(RHS, A).main() @ &m : res ∧ !RHS .not unique] + <bound>.

Second, CryptoVerif also supports explicitly aborting the game using a statement of the form event abort <name>. This is translated in a similar fashion, setting the variable RHS .abort to true when never such a statement is encountered. However, unlike the case for [unique], triggering an abort event is counted as a failure to distinguish the two sides. In these cases, the formula to prove therefore becomes:

Pr[Game(LHS, A).main() @ &m : res] ≤ Pr[Game(RHS, A).main() @ &m : res ∨ RHS .abort] + <bound>.

In the presence of event abort <name> in the right-hand side, the transformation of the left-hand side LHS into the right-hand side RHS intuitively groups together two steps: the transformation of LHS into an intermediate game G that differs from LHS only when the event <name> is executed, which implies that Pr[Game(LHS, A).main() @ &m : res] ≤ Pr[Game(G, A).main() @ &m : res ∨ RHS .abort] and a transformation of G into RHS for which we bound the probability of distinguishing G from RHS. Combining the two properties yields the inequality above. 4 For games that contain both the annotation unique and an abort event, the formula to prove becomes Pr[Game(LHS, A).main() @ &m : res] ≤ Pr[Game(RHS, A).main() @ &m : res ∧ !RHS .not unique ∨ RHS .abort] + <bound>.

In contrast to the probability of RHS .abort, the probability of RHS .not unique is counted in the probability bound that we compute. That is why we negate RHS .not unique in the formula above and do not negate RHS .abort.

IV. CASE STUDIES

A. IND-CCA2

We now prove that every IND-CCA2 secure encryption scheme validates the indistinguishability axiom in Fig. 4. In EasyCrypt, we define IND-CCA2 security via the usual security game where the adversary passes two messages (of equal length) to an encryption oracle and then tries to determine which of the two messages was encrypted. While the proof is completely standard from the mathematical perspective, it allows us to explain some of the common proof patterns for reasoning about the games extracted from CryptoVerif.

The first proof pattern is that we always introduce an intermediate game capturing the essence of the game extracted from CryptoVerif. The intermediate game for the right-hand side is given in Fig. 9. The main differences to the extracted game are: the key seed is sampled during init; the encryption seed is sampled within the procedure enc; and the implicit oracles for the random variables have been removed. In addition, we replace the table with a random map where map updates (e.g. cs.[c ← m]) are cumulative (i.e., a single key can be mapped to multiple values) and map access (e.g. cs.[c]) is a distribution selecting a binding uniformly at random. The lefthand side game is analogous, encrypting m rather than Z(m) and removing all lines dealing with cs.

The changes to random sampling, which we make to most of the games we extract, motivate the extraction of random variables as random oracles: while moving random sampling between procedures is hard in general, EasyCrypt provides lemmas to replace the default implementation of a random oracle with an eager or lazy implementation. Here, we replace the random oracle for the key seed, whose domain is the singleton type unit, with an eager implementation that samples the single contained value during initialization. Similarly, we replace the random oracle for the encryption seed with a lazy implementation where sample does nothing, causing sampling to occur when get is called. This turns the implicit oracles into no-ops, making it straightforward to turn every adversary distinguishing the extracted games into an adversary distinguishing the -much simpler -intermediate games.

IND-CCA2 01 (sk , pk ) $ ← Gen 02 b $ ← {0, 1} 03 C ← ∅ 04 b ′ ← A Enc,Dec (pk ) 05 return b ′ = b Adv IND-CCA2 (A) = |2 Pr[b ′ = b] -1| Oracle Enc(m 0 , m 1 ) 06 c ← Enc(pk , m b ) 07 C ← C ∪ {c} 08 return c Oracle Dec(c) 09 if c ∈ C return ⊥ 10 m ← Dec(sk , c) 11 return m
Changing the implementation of the random oracle for some random variable is only possible if the CryptoVerif game does not contain a find statement with a condition involving that random variable. Such find statements require an oracle implementation exposing the internal map, making the lemmas for changing oracle implementations inapplicable.

The reduction from the standard IND-CCA2 security game (cf. Fig. 10) to our intermediate game is straightforward.

Theorem 1: For every adversary A against the (extracted) IND-CCA2 game from CryptoVerif, making at most q enc queries to the encryption oracle and at most q dec queries to the decryption oracle, there exists an adversary B against the standard IND-CCA2 game, making at most q dec queries to the decryption oracle and a single query to the encryption oracle such that5

Adv CV-IND-CCA2 (A) ≤ q enc • Adv IND-CCA2 (B)
For all our case studies, the precise statement of the mechanized proof in EasyCrypt can be found in Appendix B. The full proof can be found in subdirectory cv2EasyCrypt of the CryptoVerif 2.08 distribution available at https://cryptoverif. inria.fr.

B. OutsiderCCA Security for Authenticated KEMs

An authenticated key encapsulation mechanism (AKEM) [START_REF] Alwen | Analysing the hpke standard[END_REF], [START_REF]Analysing the HPKE standard[END_REF] consists of three (probabilistic) algorithms:

• Gen outputs a key pair (sk , pk ), where pk defines a key space K. • AuthEncap takes as input a (sender) secret key sk and a (receiver) public key pk , and outputs a pair (c, K) where c is an encapsulation and K ∈ K is the (shared) secret key contained in c. • AuthDecap takes as input a (receiver) secret key sk , a (sender) public key pk , and an encapsulation c, and deterministically outputs a shared key K ∈ K. We require that for all (sk 1 , pk 1 ) ∈ Gen, (sk 2 , pk 2 ) ∈ Gen,

Pr (c,K)←AuthEncap(sk 1,pk 2 ) [AuthDecap(sk 2 , pk 1 , c) = K] = 1 . 2-OutsiderCCA ℓ / 2-OutsiderCCA r 01 (sk 1 , pk 1 ) $ ← Gen 02 (sk 2 , pk 2 ) $ ← Gen 03 E ← ∅ 04 b $ ← A AEncap,ADecap,Chall (pk 1 , pk 2 ) 05 return b Oracle Chall(i ∈ [2], j ∈ [2]) 06 (c, K) $ ← AuthEncap(sk i , pk j ) 07 K $ ← K 08 E ← E ∪ {(pk i , pk j , c, K)} 09 return (c, K) Oracle AEncap(i ∈ [2], pk ) 10 (c, K) $ ← AuthEncap(sk i , pk ) 11 return (c, K) Oracle ADecap(j ∈ [2], pk , c) 12 if ∃K : (pk , pk j , c, K) ∈ E 13 return K 14 K ← AuthDecap(sk j , pk , c) 15 return K Fig. 11. 2-OutsiderCCA Security
The indistinguishability axiom in CryptoVerif for OutsiderCCA secure authenticated KEMs models a scenario where we have n honest parties. For every honest party 1 ≤ i ≤ n we sample a keypair (pk i , sk i ). In the "real" game, the adversary is given access to the following oracles for every honest party i: an oracle returning the public key pk i for that party; an encapsulation oracle taking a (receiver) public key pk and returning (c, K) := AuthEncap(sk i , pk ); and a decapsulation oracle taking a (sender) public key pk and an encapsulation c and returning K := AuthDecap(sk i , pk , c). In the "ideal" game, the encapsulation oracle computes (c, K) in the same way as in the "real" game. However, if the provided public key belongs to an honest party (i.e. the adversary does not know the secret key) it returns (c, K ′ ) where K ′ is sampled uniformly at random. The game uses a table to keep the answers of the decapsulation oracle consistent with this randomization. We ignore the implicit oracles for sampling random values; these can be removed in the same fashion as in the previous section.

We prove that indistinguishability of the n-user games described above is implied by indistinguishability of the 2user games 2-OutsiderCCA ℓ and 2-OutsiderCCA r given in Fig. 11 (2-OutsiderCCA r includes the parts in dashed boxes; 2-OutsiderCCA ℓ does not) where the adversary is restricted to a single challenge query. The proof is based on the initial revision of [1, Appendix A.1] and is carried out in two parts. We first show, using a standard hybrid argument, that security for one challenge query implies security for q c challenge queries.

We then give a sequence of games G u,v (with 0 ≤ u, v ≤ n) and show that for every adversary A against the OutsiderCCA game (extracted from CryptoVerif) there exists an adversary B against the 2-OutsiderCCA game such that:

1) G n,n perfectly simulates A interacting with the "real" OutsiderCCA game 2) G 1,0 perfectly simulates A interacting with the "ideal"

OutsiderCCA game 3) G u,n perfectly simulates G u+1,0 whenever 1 ≤ u < n 4) B interacting with the "real" 2-OutsiderCCA ℓ game is perfectly simulated by sampling 1 ≤ u, v ≤ n uniformly at random and then running G u,v . 5) B interacting with the "ideal" 2-OutsiderCCA r game is perfectly simulated by sampling 1 ≤ u, v ≤ n uniformly at random and then running G u,v-1 . Thus, the probability of B winning the "real" game can be written as 1

n 2 n u=1 n v=1 Pr[G u,v ⇒ 1]
, and the probability of B winning the "ideal" game can be written as 1

n 2 n u=1 n v=1 Pr[G u,v-1 ⇒ 1].
Canceling the common terms and combining this with the first part, we obtain the theorem we have mechanized in EasyCrypt:

Theorem 2: For every adversary A against the (extracted) OutsiderCCA game making at most q e queries to the encapsulation oracle and at most q d queries to the decapsulation oracle there exists a 2-OutsiderCCA adversary B making at most 2q e queries to AEncap, at most q d queries to ADecap, and at most one query to Chall such that:

Adv OutsiderCCA (A) ≤ n 2 q e • Adv 2-OutsiderCCA (B) + n 2 P AKEM
P AKEM is the probability that two calls to Gen generate the same public key. The mechanized proof corrects two errors from [START_REF] Alwen | Analysing the hpke standard[END_REF]. We fix a counting error, leading to a factor of 2 in the queries to AEncap made by B. Further, the proof only works in the absence of public key collisions and the original proof failed to account for that. Specifically, the n users must have distinct public keys to keep the log of ciphertexts coherent between the n-user game and the combination of the 2-user game and a simulator that simulates the remaining n -2 users. Bounding the probability of public key collisions leads to an additional probability term of n 2 P AKEM . After being contacted by us, the authors acknowledged the errors and updated their proofs. 6 Finally, in the original formulation of the indistinguishability axiom in CryptoVerif the randomness used in the algorithms was tagged as unchanged, leaking the randomness to the adversary and making the axiom unsatisfiable by any reasonable AKEM. However, the extra flexibility that comes with this annotation was not used in the proof, making the error trivial to fix.

C. Computational Diffie-Hellman assumption

The computational Diffie-Hellman assumption (CDH) is usually defined as follows [START_REF] Okamoto | The gap-problems: a new class of problems for the security of cryptographic schemes[END_REF]: given a group G of prime order q, with a generator g, an adversary succeeds against CDH when it computes g ab knowing g a and g b for two random exponents a, b ∈ [1, q-1]. The modeling of the CDH assumption in CryptoVerif extends this definition in two directions.

First, it considers not only a single pair of exponents a, b, but two families of exponents a i (i ∈ {1, . . . , n a }) and b j (j ∈ {1, . . . , n b }), and considers all Diffie-Hellman values g aibj . This makes the assumption apply when protocol participants perform several sessions of a Diffie-Hellman exchange.

Further, the CryptoVerif CDH assumption also allows some of the exponents a i , b j to be queried by the adversary (i.e., compromised). As other assumptions on primitives in Cryp-toVerif, CDH is formalized as indistinguishability between two games L ≈ R: L returns results m = g aibj with m, i, and j coming from the adversary, while R returns false instead when the adversary cannot compute g aibj by CDH (i.e., when neither a i nor b j was compromised). The variables a i and b j are marked [unchanged] (see Section III-C): they have the same value in L and R. The CDH game transformation can thus be applied even when these variables occur as arguments of events in the game.

Second, the CryptoVerif assumption for CDH supports not only prime-order groups, but also modern Diffie-Hellman structures such as Curve25519 and Curve488, used in protocols like TLS 1.3 [START_REF] Rescorla | The Transport Layer Security (TLS) protocol version 1.3[END_REF] and the VPN WireGuard [START_REF] Donenfeld | WireGuard: Next generation kernel network tunnel[END_REF], which, strictly speaking, are not groups. In order to achieve this goal, it uses the notion of nominal groups first introduced in [1], [START_REF]Analysing the HPKE standard[END_REF], which axiomatizes properties needed of Diffie-Hellman structures and satisfied both by prime-order groups and by Curve25519/Curve448. Definition 1: A nominal group N = (G, Z, g, D H , exp, ˆ, mult, E U , f, inv) consists of an efficiently recognizable finite set of elements G (also called "group elements"), a set of exponents Z, a base element g ∈ G, a distribution of honest exponents D H over Z, two efficiently computable exponentiation functions exp : G × Z → G and ˆ: G × Z → G, where we write X y for ˆ(X, y), an efficiently computable associative and commutative function mult : Z × Z → Z, where we write xy for mult(x, y), a finite set of exponents E U ⊆ Z, a factor f ∈ Z, and an efficiently computable function inv : E U ∪ {f } → Z. We require the following properties:

1)

(X y ) z = X yz for all X ∈ G, y, z ∈ Z; 2) g xinv(x) = g for all x ∈ E U ∪ {f }; 3) exp(X, y) = X yinv(f ) for all X ∈ G, y ∈ Z; 4) the functions ϕ : E U → G defined by ϕ(y) = exp(g, y)
and for x ∈ E U , ϕ x : E U → G defined by ϕ x (y) = exp(g, xy) are injective and all have the same image. Groups of prime order q are instances of nominal groups, where G is the group, Z = E U = Z * q , mult and inv are the usual product and inverse on Z * q , exp = ˆis the usual exponentiation, f = 1, D H is the uniform distribution on Z * q . Properties 1 and 2 are standard properties of exponentiation. Property 3 is clear from exp = ˆand f = 1. In Property 4, the common image of ϕ and ϕ x is G minus its neutral element.

Curve25519 and Curve448 are also instances of nominal of groups, actually in two ways, which we sketch briefly. In the simplest way, f = inv(f ) = 1, inv is the inverse modulo a prime p, and both exponentiation functions are the same.

However, for Curve25519 and Curve448, choosing f to be the cofactor of the curve (8 for Curve25519, 4 for Curve448) yields a more precise model: these curves are unions of groups of cardinals f p and f ′ p ′ where f ′ divides f , p and p ′ are large primes, and the exponents are always multiple of f . We take advantage of this property to work in the subgroups of cardinals p and p ′ : X y = (X f ) y/f = exp(X f , y) and we have the guarantee that X f is in one of these subgroups. This is why we introduce a second exponentiation function exp that divides the exponents by f , as defined by Property 3.

The set E U provides exactly one exponent y to generate each element exp(g, y), which correspond to elements of the subgroup of cardinal p in Curve25519 and Curve448 (cf. Property 4). Such a model was used with pen-and-paper proofs in [START_REF] Lipp | A mechanised cryptographic proof of the WireGuard virtual private network protocol[END_REF]. Our definition of nominal groups generalizes the one of [START_REF] Alwen | Analysing the hpke standard[END_REF], [START_REF]Analysing the HPKE standard[END_REF] by allowing f ̸ = 1, thus supporting such more precise models of Curve25519 and Curve448.

The CDH assumption on nominal groups becomes: given a nominal group N = (G, Z, g, D H , exp, ˆ, mult, E U , f, inv), an adversary A succeeds against CDH when it computes exp(g, ab) knowing exp(g, a) and exp(g, b) for two random exponents a, b chosen uniformly in E U . Its probability of success is denoted Succ CDH N (A). Adapting to the notion of nominal groups, the CDH assumption in CryptoVerif uses exp instead of ˆand chooses the exponents a i and b j according to the distribution of honest exponents in the nominal group D H , which is the uniform distribution on E U for prime-order groups, but differs for Curve25519 and Curve448. We translate the two games L and R of this assumption into EasyCrypt and reduce in EasyCrypt the indistinguishability L ≈ R to the CDH assumption in the nominal group. The EasyCrypt proof mostly follows the same strategy as the mathematical paper proof detailed in Appendix A. In short, we first show that the two extracted games are equivalent up to an event bad, where bad is triggered when the adversary provides m, i, j such that m = exp(g, a i b j ) having queried neither a i nor b j (hence the adversary managed to compute exp(g, a i b j ) knowing only exp(g, a i ) and exp(g, b j )). Second, we change the distribution of exponents from D H to the uniform distribution on E U , with a probability loss (n a + n b )∆ N , where ∆ N is the statistical distance between these two distributions, which depends on the particular nominal group. Third, we construct a simulator that is given a CDH instance (X, Y ) and probabilistically injects that instance into the game by relying on the random self-reducibility of the CDH problem [START_REF] Bresson | The group Diffie-Hellman problems[END_REF]: given an instance of the CDH problem, any other instance can be obtained by re-randomization. More precisely, each exponential A i = exp(g, a i ) is replaced with X αi for α i ← $ E U with probability p a (in this case, the simulator does not know a i because it does not know the discrete logarithm of X) and with exp(g, α i ) for α i ← $ E U with probability 1 -p a (in this case, a i = α i ). We proceed similarly for B j = exp(g, b i ) using probability p b . The simulator loses if it is queried for an exponent a i or b i that it does not know. Otherwise, the two games are perfectly indistinguishable by Property 4. The simulator wins (i.e. successfully solves the CDH instance (X, Y )) when the bad event is triggered for indices where the simulator injected the given instance, that is, A i = X αi and B j = Y βj . Since the simulator cannot check whether the adversary solved its instance, one guesses randomly the decisional Diffie-Hellman query m = exp(g, a i b j ) for which the bad event is triggered. Finally, we optimize the probabilities p a and p b to maximize the probability of success of the simulator. This leads to the following theorem, which we have mechanized in EasyCrypt:

Theorem 3: Let N be a nominal group, and let A be an adversary against the (extracted) CDH assumption from Cryp-toVerif for N . That is, A is given access to A i = exp(g, a i ) (i ∈ {1, . . . , n a }) and B j = exp(g, b j ) (j ∈ {1, . . . , n b }) with the a i and b j sampled from D H ; A can compromise q a of the a i and q b of the b j ; and A can make at most q ddh attempts to provide (m, i, j) such that m = exp(g, a i b j ) (not involving compromised exponents). Then there exists in adversary B making a single attempt to solve a single (random) instance of the CDH problem for N such that:

Succ CV-CDH (A) ≤ q ddh (1 + 3q a )(1 + 3q b ) • Succ CDH N (B)+ (n a + n b )∆ N
The mechanized proof largely follows the structure of the paper proof sketched above, so we only comment briefly on two aspects regarding the mechanization.

First, the variables for a i and b j are marked as [unchanged] in CryptoVerif and thus given to the adversary after he has made all his queries. Given that the first step of the proof is an up-to-bad argument where the bad event can only occur when the adversary makes an oracle call with m = exp(g, a i b j ), declassifying the exponents after all queries have been made does not affect the proof in any significant way. We remark that marking random variables as [unchanged] and eliminating the associated oracles using up-to-bad arguments is a standard pattern for computational assumptions.

Second, the re-randomization argument requires some care in EasyCrypt. Proving indistinguishability of two games in the probabilistic relational Hoare logic (pRHL) of EasyCrypt amounts to (interactively) constructing a probabilistic coupling linking the two programs. For the sampling of α i ← $ E U (i ∈ {1, . . . , n a }), this amounts to providing a bijection h on E U that makes the rest of the game indistinguishable (i.e. ensures that exp(g, h(α i )) = if γ i then X αi else exp(g, α i ) where γ i is true when the simulator injects X from the CDH instance (X, Y ) at index i). By Property 4, such a bijection exists for every value X = exp(g, x) passed to the simulator.

D. Gap Diffie-Hellman assumption

The gap Diffie-Hellman (GDH) assumption [START_REF] Okamoto | The gap-problems: a new class of problems for the security of cryptographic schemes[END_REF] strengthens the CDH assumption by giving the adversary an additional decisional Diffie-Hellman oracle DDH(G, X, Y, Z) that tells the adversary whether X, Y , Z is a good Diffie-Hellman triple with generator G, that is, whether there exists x and y such that X = G x , Y = G y , and Z = G xy . Given a group G of prime order q, with a generator g, an adversary succeeds against GDH when it computes g ab knowing g a and g b for two random exponents a, b ∈ [1, q -1], with access to the DDH oracle.

The modeling in CryptoVerif extends this definition as in Section IV-C, considering in particular nominal groups. This modeling includes oracles that allow CryptoVerif to detect that certain equalities between exponentiations involving a i and/or b j can be decided using the DDH oracle, without compromising a i or b j . Further, in order to help CryptoVerif match the game against a protocol, the CryptoVerif modeling includes a number of additional oracles that are redundant from the mathematical point of view. In total, the game has 28 oracles.

Our proof mechanizes and extends a previous pen-and-paper proof [START_REF] Alwen | Analysing the hpke standard[END_REF], which considers a more restricted DDH oracle in which the generator G is always g, considers only nominal groups with f = 1, and does not consider the compromise of exponents a i and b j . As above, we translate the CryptoVerif games to EasyCrypt and prove their indistinguishability. The most fundamental difference in the proof is that, thanks to the DDH oracle, the simulator can determine which query raised the bad event instead of guessing it, which removes a factor q ddh in the probability bound. Thus, under conditions similar to those of Theorem 3 we obtain the following bound:

Succ CV-GDH (A) ≤ (1 + 3 (q a + min(1, q ddhma ))) • (1 + 3 (q b + min(1, q ddhmb ))) • Succ GDH N (B) + (n a + n b )∆ N
where q ddhma is the number of queries to the oracle ddhma(m, i ′ , i, j) = (exp(m, a i ′ ) = exp(g, a i b j )), and q ddhmb is similar with b j ′ instead of a i ′ . In order to solve the CDH instance (X, Y ) when the bad event is raised by such a query, one needs the replacement exponential for A i ′ = exp(g, a i ′ ) (resp. B j ′ = exp(g, b j ′ )) not to involve that CDH instance. This is the same requirement as for compromised exponents, hence this situation has the same effect as having one more compromised exponent.

V. CONCLUSION

We present a tool that translates CryptoVerif assumptions to EasyCrypt games. This allows using each tool where it is the most convenient: one can benefit from the automation of CryptoVerif to prove security protocols, and from the expressive power of EasyCrypt in order to prove assumptions on cryptographic primitives made in CryptoVerif proofs. We demonstrate the usefulness of our approach by applying it to several case studies: IND-CCA2 encryption, authenticated KEM, CDH and GDH assumptions. Our work also allowed us to discover and fix errors in the pen-and-paper proof of the authenticated KEM property. In total, the EasyCrypt proofs accompanying this paper amount to approximately 9300 (nonblank) lines. For every case study, the proof consists of a theory containing the core mathematical argument and a "bridging" theory that links these proofs with the games extracted from CryptoVerif. For the individual case studies we have: Our translation covers most of the language that CryptoVerif uses for specifying assumptions on cryptographic primitives. We still do not support pattern-matching with tuples in the get construct, which was never used in the examples we encountered, and could be added if needed. Another easy extension would be to translate together several CryptoVerif assumptions into one theory with a shared prelude, so that the instantiation in EasyCrypt can be done all at once.

For future work, it would also be interesting to improve EasyCrypt. The translation of the indistinguishability axiom for GDH yields modules with 29 procedures. This exposes a performance problem in EasyCrypt when dealing with modules that have many procedures, and needs to be fixed. Also the cost logic of EasyCrypt [START_REF] Barbosa | Mechanized proofs of adversarial complexity and application to universal composability[END_REF] needs to become more expressive and useable. This would make it more reasonable to also translate the probability formulas from CryptoVerif to EasyCrypt.

Finally, another extension would be translate not only the language of cryptographic assumptions of CryptoVerif, but the full language of games. This includes, for instance, sequences of oracles to model protocols with several messages. Such an extended translation would allow us to perform the most automatic and straightforward parts of the proof of a protocol in CryptoVerif, and to use EasyCrypt for more subtle game transformations.

APPENDIX A CDH WITH RANDOM SELF-REDUCIBILITY

This proof extends the proof of [8, Appendix B] to nominal groups. The proof of Lemma 1 is also modified to reflect the EasyCrypt proof of that result.

We assume a nominal group N = (G, Z, g, D H , exp, ˆ, mult, E U , f, inv) (see Section IV-C). First, let us rephrase the two games: LHS : One chooses random a i ← $ D H (i ∈ {1, . . . , n a }) and b j ← $ D H (j ∈ {1, . . . , n b }). The adversary is allowed to query

• for group elements, via oracles OA and OB: OA(i) returns exp(g, a i ) and OB(j) returns exp(g, b j ); • for discrete logarithms, via oracles Oa and Ob: Oa(i) returns a i (at most q a ≤ n a queries), Ob(j) returns b j (at most q b ≤ n b queries); • for Diffie-Hellman decisions, via oracle DDH(m, i, j) (at most q ddh queries) which check whether m = exp(g, a i b j ). RHS : One chooses random a i and b j as in the LHS. The adversary is allowed to query oracles

• OA, OB, Oa, and Ob, that answer as above;

• DDH(m, i, j), which returns the correct answer m = exp(g, a i b j ) if either a i or b j has been asked before for an Oa or Ob query. Otherwise, it returns is 'false'. Furthermore, the variables a i and b j are marked [unchanged], so in both games, these variables are given to the adversary after the interaction with these oracles.

We thus insist on the fact that the 2 games differ on DDH(m, i, j) Diffie-Hellman decisions queries, if neither a i nor b j has been asked before for an Oa or Ob query. In the first game, the answer is the correct one; in the second game, the answer is always 'false'.

To bound the probability of distinguishing these two games, we bound the probability that an event bad is executed, which happens as soon as a query gives a different result in the two games. Hence we define the following game G: the adversary is allowed to query oracles • OA, OB, Oa, and Ob, that answer as above; • DDH(m, i, j), which returns m = exp(g, a i b j ) if a i or b j has been asked before for an Oa or Ob query. Otherwise, if m = exp(g, a i b j ), then it executes event bad; it returns 'false'. The probability of distinguishing LHS from RHS is then at most the probability ε of event bad in G. Since the variables a i and b j are given to the adversary after the execution of event bad, giving those variables does not change the probability of bad.

Let us define a game G ′ that runs as G except that it chooses a i and b j according to the uniform distribution

D U on E U instead of D H . The probability of distinguishing D U from D H is ∆ N . Hence, the probability of distinguishing G ′ from G is at most (n a + n b )∆ N . So G ′ executes event bad with probability ε ′ ≥ ε -(n a + n b )∆ N .
Let us be given a CDH tuple (X = exp(g, x), Y = exp(g, y)) with x ← $ E U , y ← $ E U for which we want to compute Z = exp(g, xy). We provide a simulator B for this game:

For i ∈ {1, . . . , n a }, one chooses a random bit γ i with bias p a : with probability p a , γ i = 1, and with probability 1 -p a , γ i = 0. If γ i = 1, choose α i ← $ E U and set A i = X αi (and thus we have a i = α i x but the simulator cannot compute a i because it does not know x). If γ i = 0, choose α i ← $ E U and set a i = α i and A i = exp(g, α i ).

For j ∈ {1, . . . , n b }, one chooses a random bit δ j with bias p b : with probability p b , δ j = 1, and with probability 1 -p b , δ j = 0. If δ j = 1, choose β j ← $ E U , and set B j = Y βj (and thus b j = β j y). If δ j = 0, choose β j ← $ E U , and set b j = β j and B j = exp(g, β j ).

• OA(i) returns A i ;

• OB(j) returns B j ;

• For the query Oa(i), if γ i = 0, then return α i . Otherwise, the simulation stops; • For the query Ob(j), if δ j = 0, then return β j . Otherwise, the simulation stops. • For the query DDH(m, i, j), if one of the a i or b j has been asked an Oa or Obquery (and did not stop the simulation), which means that either γ i = 0 or δ j = 0, then one can either test whether m = B αi j or not, or whether m = A βj i or not, and provide the correct answer; otherwise, we answer 'false'. Since there are at most q a Oa queries and q b Ob queries, with probability at least (1 -p a ) qa (1 -p b ) q b , the simulation does not stop and is perfectly indistinguishable from G ′ , for the following reason. Let G U be the distribution of exp(g, y) where y is chosen uniformly in E U . Let G R (x) be the distribution of elements rerandomized from x, that is, the distribution of exp(g, xy) where y is chosen uniformly in E U . Using Property 4 of nominal groups, we have that G U = G R (x) for all x ∈ E U , because, by injectivity of ϕ, G U is the uniform distribution on the image of ϕ, and by injectivity of ϕ x , G R (x) is the uniform distribution on the image of ϕ x ; moreover ϕ and ϕ x have the same image. Since G U = G R (x), the distribution of A i in the simulation when γ i = 1 is the same as the distribution of A i in G ′ . The situation is similar for B j and from that it is easy to see that the games are perfectly indistinguishable.

The event bad is executed if for one DDH query, m = exp(g, a i b j ) but neither a i or b j has been asked for an Oa or Ob query. Since event bad is executed with probability ε ′ in game G ′ , then in the simulation, such a critial DDH query happens with probability at least ε ′ (1 -p a ) qa (1 -p b ) q b . Let us randomly choose k between 1 and q ddh , and bet that the k-th DDH query is the first critical one, which is true with probability 1/q ddh . For this query, with probability p a p b , both γ i = 1 and δ j = 1: m = exp(g, a i b j ) = exp(g, α i xβ j y) = Z αiβj and this query leads to the expected Z value, by computing Z = m inv(αi)inv(βj ) . This means that our simulator B achieves Succ CDH N (B) ≥ (1 -p a ) qa (1 -p b ) q b ε ′ p a p b /q ddh so ε ′ ≤ q ddh × Succ CDH N (B) (1 -p a ) qa (1 -p b ) q b p a p b Lemma 1: For all n ∈ N, there exists x ∈ [0, 1] such that

1 x(1 -x) n ≤ f (n)
where f (n) = 1 + γn with γ = 3.

Proof: Consider the function x → x(1 -x) n . It reaches its maximum for x = 1 n+1 . Let us prove that, for all n ∈ N,

1 1 n+1 (1-1 n+1 ) n ≤ f (n).
• if n = 0, x = 1 and we have 1 x(1 -x) n = 1 ≤ f (0).

• if n ≥ 1, 1 x(1 -x) n = 1 1 n+1 n n+1 n = (n + 1) n+1 n n . Let h(n) = (n + 1) n+1 n n .
For information, we have The second inequality holds because h(n) n+1 = 1 + 1 n n is monotonically increasing and tends to e when n tends to +∞. We could use one of the bounds given by these two inequalities. However, the bound given by the first inequality is always larger than f (n), so less precise than the bound given by the lemma. The bound given by the second inequality is best for large n, however it is not precise for small n. We believe that the bound given by the lemma yields a better compromise for all n.

To show the lemma, we just have to show that, for all n ≥ 1,

h(n) ≤ f (n). Let g(n) = f (n) h(n)
The value of γ is chosen such that g(1) = 1. Hence it is sufficient to show that g is monotonically increasing, that is, for all n ≥ 1, g(n + 1) ≥ g(n). We have g(n + 1) = g(n)

f + n + 1 2n(n + 2) 2 = 6n 5 + 38n 4 + 85n 3 + 75n 2 + 20n 6n 5 + 38n 4 + 84n 3 + 72n 2 + 16n which is greater than 1 for all n ≥ 1 thus completing the proof of the desired result.

(
Additionally, let us evaluate how precise the bound is. For that, we evaluate the limit of g(x) when x tends to +∞. We have For γ = 3, γ e = 3 e < 1.104. Hence, the loss coming from the replacement of h(n) with f (n) is less than 10.4%. That is remarkably precise given that the formula f (n) is much simpler than h(n).

By Lemma 1, we can choose p a and p b above so that 1 (1-pa) qa pa ≤ f (q a ) and 1 (1-p b ) q b p b ≤ f (q b ), so ε ′ ≤ q ddh (3q a + 1)(3q b + 1) × Succ CDH N (B).

Hence ε ≤ q ddh (3q a + 1)(3q b + 1) × Succ CDH N (B) + (n a + n b )∆ N .

We can further notice that the simulator B takes approximately the same time as the adversary against the initial game. More precisely, it computes at most n a + n b + q ddh + 1 additional exponentiations.

CVC.cddh = 0 =⇒ CVC.ca ≤ q oa ∧ CVC.cb ≤ q ob ∧ CVC.cddh ≤ q ddh]. module B (A : Adversary) = I.B(C(A)).

lemma main &m :

| Pr[Game(LHS, A).main() @ &m : res] -Pr[Game(RHS, A).main() @ &m : res] | ≤ q ddh%r × (1 + 3 × q oa)%r × (1 + 3 × q ob)%r × Pr[NCDH.Game(B(A)).main() @ &m : res] + (na + nb)%r × SDist.sdist dZ (duniform (FSet.elems EU)).

end section.

D. Gap Diffie-Hellman assumption

As for CDH, the result below is with respect to some fixed nominal group. In particular, NGDH.Game is the (singleinstance) GDH game that provides a ddh oracle to the simulator. CVC.ca = 0 ∧ CVC.cb = 0 ∧ CVC.cddhma = 0 ∧ CVC.cddhmb = 0 =⇒ CVC.ca ≤ q oa ∧ CVC.cb ≤ q ob ∧ CVC.cddhma ≤ q ddhma ∧ CVC.cddhmb ≤ q ddhmb].

module B (A : CV.Adversary) = I.B(C(A)).

lemma main &m :

| Pr[Game(LHS, A).main() @ &m : res] -Pr[Game(RHS, A).main() @ &m : res] | ≤ (1 + 3 × (q oa + min 1 q ddhma))%r × (1 + 3 × (q ob + min 1 q ddhmb))%r × Pr[NGDH.Game(B(A)).main() @ &m : res] + (na + nb)%r × SDist.sdist dZ (duniform (FSet.elems EU)). end section.

1

  type cleartext. 2 type ciphertext. 3 type key [bounded]. 4 type enc seed [bounded].

5 6

 5 fun enc(cleartext, key, enc seed): ciphertext. 7 fun Z(cleartext):cleartext.

8 9

 8 param N. 10 proba Penc.

11 12 13 k ← $ key; 14 foreach i ≤ N do 15 r 18 k ← $ key; 19 foreach i ≤ N do 20 r

 11131415181920 Fig. 1. IND-CPA Security in CryptoVerif

  2 type enc seed. 3 type key. 4 type cleartext.

5 6

 5 axiom enc seed fin : finite type<:enc seed>. 7 axiom key fin : finite type<:key>.

8 9

 8 op b N : int. 10 op Z : cleartext → cleartext. 11 op enc : cleartext × key × enc seed → ciphertext.

1

  module type Oracles = { 2 proc r() : unit 3 proc r i( : int) : unit 4 proc p Oenc(i : int, x : cleartext) : ciphertext 5 }.

11 12

 11 module type Adversary (S : Oracles) = { 13 proc distinguish() : bool 14 }.

15 16 module 17 proc 20 r

 161720 Game (S : Oracles i, A : Adversary) = { ← A(S).distinguish(); 21 return r; } 22 }.

Fig. 2 .

 2 Fig. 2. The Distinguishability Game

  : OL k.RO) (O r : OL r.RO) : Oracles i = { var m r i : (int, unit) fmap var m r : (unit, unit) fmap var m Oenc : (int, cleartext) fmap proc init() = { m r i ← empty; m r ← empty; m Oenc ← empty; O k.init(); O r.init();

  ); tmp r i ← O r.get(i); aout ← enc (x, tmp k, tmp r i); } return aout; } }. module LHS = LHS (OL k.RO, OL r.RO).

Fig. 3 .

 3 Fig. 3. LHS Game for IND-CPA

8 9

 8 equiv(ind cca2(enc)) 10 k ← $ keyseed; ( 11 Opk() := return(pkgen(k)) | 12 foreach i2 ≤ N2 do Odec(c:ciphertext) := 13 return(dec(c, skgen(k))) | 14 foreach i ≤ N do r ← $ enc seed; 15 Oenc(m:cleartext) := return(enc(m, pkgen(k),r))) 16 ⇐(...)⇒ 17 k ← $ keyseed; ( 18 Opk() := return(pkgen(k)) | 19 foreach i2 ≤ N2 do Odec(c:ciphertext) := 20 get cipher(m1, =c) in return(injbot(m1)) 21 else return(dec(c, skgen(k))) | 22 foreach i ≤ N do r ← $ enc seed; 23 Oenc(m:cleartext) := 24 c1 ← enc(Z(m), pkgen(k), r); 25 insert cipher(m, c1); return(c1)).

Fig. 4 .

 4 Fig. 4. IND-CCA2

1

  var t cipher : (cleartext × ciphertext) list 2 var v m1 : (int, cleartext) fmap 3 ... 4 proc p Odec(i2 : int, c : ciphertext) = { 5 var aout : bitstring option ← witness; 6 ...

7

 7

9 r 0 cipher ← List.pmap 10 (Fig. 5 .

 9105 Fig. 5. Translation of Table Access

6

  then return(injbot(m[j])) 7 else return(dec(c, skgen(k))) | 8 foreach i ≤ N do r1 ← $ enc seed; 9 Oenc(m:cleartext) := 10 c1:ciphertext ← enc(Z(m), pkgen(k), r1); 11 return(c1)).

Fig. 6 .

 6 Fig. 6. RHS of IND-CCA2 (using find)

10 aout 11 } else { 12 jFig. 7 .

 1011127 Fig. 7. Translation of find

1

  module type Adversary (S : Oracles) = { 2 proc distinguish() : unit 3 proc guess( : ... fmap × ... × ... fmap) : bool {} 4 }.

5 6 module 8 S

 68 Game (S : Oracles i, A : Adversary) = { 7 proc main() = {

Fig. 8 .

 8 Fig. 8. Game in the Presence of Unchanged Variables

7 ks ← $ dkeyseed; 8 pk ← pkgen ks; 9 sk 14 e ← $ dencseed; 15 c

 7891415 ← skgen ks; } 10 11 proc pk () = { return pk; } 12 13 proc enc (m : plaintext) : ciphertext = { ← enc(Z(m), pk, e); 16 cs ← cs.[c ← m]; 17 return c; } 18 19 proc dec (c : ciphertext) : plaintext option = { 20 if (c ∈ cs) { 21 m ← $ cs.[c]; 22 } else { 23 m ← dec(c, sk);

Fig. 9 .

 9 Fig. 9. "Ideal" Intermediate Game For IND-CCA2

Fig. 10 .

 10 Fig. 10. IND-CCA2 Security (Textbook Version)

  n tends to +∞ and we have en ≤ h(n) ≤ max (1, 4n) and h(n) ≤ e(n + 1).The first inequality holds because h(ndecreasing, tends to e when n tends to +∞, and evaluates to 4 for n = 1.

  ln (g(x)) = ln f (x) γx + ln(γx)+ ln(1) + x ln(x) -(x + 1) ln(x + 1) = ln f (x) γx + ln(γ) -(x + 1) ln x + 1 x ∼ ln(γ) -x 1 x → ln(γ) -1when x tends to +∞. Therefore, for all n ≥ 1, 0 ≤ ln(g(n)) < ln(γ) -1 hence for all n ≥ 0,

  section.declare module A <: Adversary {-LHS, -RHS, ...}.

	islossless O.p Oa ⇒
	islossless O.p ODDHa2 ⇒
	islossless O.p ODDHa3 ⇒
	islossless O.p ODDHa4 ⇒
	islossless O.p ODDHa5 ⇒
	islossless O.p ODDHa6 ⇒
	islossless O.p ODDHa7 ⇒
	islossless O.p OAeq ⇒
	islossless O.p ODDHa1 ⇒
	islossless O.p ODDHa ⇒
	islossless O.p ODDHa8 ⇒
	islossless O.p ODHa9 ⇒
	islossless O.p OB ⇒
	islossless O.p Ob ⇒
	islossless O.p ODDHb2 ⇒
	islossless O.p ODDHb3 ⇒
	islossless O.p ODDHb4 ⇒
	islossless O.p ODDHb5 ⇒
	islossless O.p ODDHb6 ⇒
	islossless O.p ODDHb7 ⇒
	islossless O.p OBeq ⇒
	islossless O.p ODDHb1 ⇒
	islossless O.p ODDHb ⇒
	islossless O.p ODDHb8 ⇒
	islossless O.p ODHb9 ⇒
	islossless A(O).distinguish.

declare axiom guess ll : forall (O <: Oracles{-A}), islossless A(O).guess. declare axiom distinguish ll : forall (O <: Oracles{-A}), islossless O.r ia ⇒ islossless O.r ib ⇒ islossless O.p OA ⇒ declare axiom A bound (O <: Oracles{-CVC, -A}) : hoare [A(CVC(O)).distinguish :

Since EasyCrypt allows sampling from sub-distributions as well as diverging programs, the semantics of statements and procedures can be subdistributions as well.

The intended interpretation is (clearly) not part of the CryptoVerif code. The code in Fig.1simply tells CryptoVerif to assume some functions satisfying the stated indistinguishability property, which should be the case for the intended interpretation.

EasyCrypt does not allow us to enforce order restrictions on procedure calls. We therefore adopt the convention that whenever the adversary against the EasyCrypt game makes an oracle call that would not be allowed by the CryptoVerif semantics, we preserve the state of the game and immediately

The probability of event <name> can typically not be bounded in the assumption on the primitive itself, but will be bounded by CryptoVerif in subsequent steps of the proof of the whole protocol. For instance, event abort <name> is executed when the adversary reuses a nonce in an encryption scheme with nonces, which breaks the security of the scheme. At the level of the cryptographic assumption on the encryption scheme, the adversary provides the nonces, and may therefore reuse several times the same nonce. That triggers the event event abort <name> and CryptoVerif will bound the probability of that event by showing that nonces are never or very rarely reused in the whole protocol.

While we do not verify this in EasyCrypt, we also have that Time(A) ≈ Time(B).

The corrections made by the authors differ from the corrections we proposed in that they restructure the proof and thereby manage to avoid the factor 2 in encapsulation queries.

Acknowledgments: This work was partly done while Christian Doczkal was at Université Côte d'Azur, Inria and Pierre-Yves Strub was at École Polytechnique. This work benefited from funding managed by the French National Research Agency under the France 2030 programme with the reference ANR-22-PECY-0006 (PEPR Cybersecurity SVP).

APPENDIX B STATEMENTS OF THE MECHANIZED PROOFS

We give the theorem statements that were proved using the EasyCrypt proof assistant. In each statement Game is an instance of the game extracted from CryptoVerif, A : Adversary is an adversary against that game, and B(A) is the adversary against the security game modeled in EasyCrypt.

To increase readability, we prove each lemma in a section. Sections allow the declaration of local assumptions (e.g., modules and axioms) which respectively become universally quantified variables and hypotheses of every lemma proved inside the section. For technical reasons, we also need to require that the memory of the adversary is disjoint from the memory of any module used in the proof.

A. IND-CCA2

In the following, CCA is the standard IND-CCA2 game and Nenc refers to the number of allowed encryption queries. section. declare module A <: Adversary{-LHS, -RHS, ...}.

B. OutsiderCCA Security for Authenticated KEMs

In the following, O2.Game is the 2-OutsiderCCA security game, and PK is the probability that for two random key seeds the resulting public keys are the same. Note that in the lemmas below qe and qd refer to the number of allowed encapsulation/decapsulation queries per user rather than the total number of queries. Thus, B is allowed to make 2×(qe×n) encapsulation queries and the probability loss is (n ˆ2 ×(qe ×n)). | Pr[Game(LHS, A).main() @ &m : res ]-Pr[Game(RHS, A).main() @ &m : res] | ≤ (n ˆ2 × (qe × n))%r × | Pr[O2.Game(O2.Oreal, B(A)).main() @ &m : res] -Pr[O2.Game(O2.Oideal, B(A)).main() @ &m : res] | + (n ˆ2)%r × PK. end section.

C. Computational Diffie-Hellman assumption

Everything below is with respect to some fixed (abstract) nominal group. In particular, NCDH.Game is the (single instance) CDH game for that nominal group. Further, SDist.sdist is the operator for the statistical distance in EasyCrypt.