construction pads it to a multiple of the block size and breaks it into blocks (Line 1). The padding scheme must be injective and length-regular (both properties are necessary in a padding scheme used in secure cryptographic hashing) and must also guarantee that no padded input ends with an all-zero block (which is a necessary condition for the security of the SPONGE). The padded input is then absorbed block-by-block into the SPONGE's internal state (initialized to all 0 bits on Line 3) by interleaving the addition of blocks into the state with applications of the permutation (Lines 4-5). Once all input blocks have been absorbed, the permutation is used, again, to extract the output by blocks of size $r$ (Lines 7-13), truncating the final block to the requested $\ell$ bits (Line 14).<fnref n="2" />

In the description and formal treatment, I abstract the permutation's bitwidth (set to 1600 by the standard) to some positive integer $b$, refining it only in the final steps of the proof. Thus $r+c=b$. $s_c$ is the part of the internal state that is not exposed to or controlled by the adversary. For a fixed state width, the capacity serves as the main security parameter for the SPONGE construction, and the rate as its main performance parameter. Therefore, as illustrated in Figure 6.3, I often use $c$ and $r$ to specify a particular SPONGE construction, rather than $b$ and $r$.

The standard defines SHA3-224, SHA3-256, SHA3-384 and SHA3-512 — collectively referred to as SHA3-x in the following, as approved hash functions that accept any bitstring as input, and deterministically produce a fixed-length hash (of length $x$, for SHA3-x). For a fixed output length $x$, these functions instantiate the SPONGE construction with KECCAK-$p$, fix $r = 1600 - 2 \cdot x$ and use the multi-rate padding scheme pad10*1 defined as

$$ \mathrm{pad10*1}(r, \ell) := 1 \Vert 0^{(-\ell-2)} \mod r \Vert 1. $$

The pad10*1 scheme simply appends a string composed of two 1 bits around as many 0 bits as necessary (from 0 to $r-1$) to the message. It is easy to see that it satisfies the properties required by the SPONGE construction. Formally, the SHA3-x functions are defined as:

$$ \mathrm{SHA3-x}(m) = \mathrm{SPONGE}_{2 \cdot x}[\mathrm{KECCAK-p}, \mathrm{pad10*1}, 1600 - 2 \cdot x](m \Vert 01, x), $$

where 01 denote two domain separation bits.

The SHA3 standard also defines two XOFs, SHAKE128 and SHAKE256 — collectively referred to as SHAKEx, that accept arbitrary bitstrings as input, and produce a caller-chosen-length prefix of an infinite bitstream deterministically defined by the input. On input a bitstring $m$ and an output length $d$, the SHAKEx XOFs are defined as

$$ \mathrm{SHAKEx}(m, d) = \mathrm{SPONGE}_{2 \cdot x}[\mathrm{KECCAK-p}, \mathrm{pad10*1}, 1600 - 2 \cdot x](m \Vert ss \Vert 11, d), $$

where ss denote two suffix bits and 11 denote two domain separation bits. The standard introduces suffix bits for future compatibility with coding schemes for tree hashing variants of the SHAKEx functions. They have no effect on security; in fact, our security proof applies for arbitrary application suffixes (of any length fixed in advance).

## 6.2 Security Statement

The SPONGE construction satisfies the strong security notion known as indifferentiability from a (extendable output) random oracle, defined in Section 5.3.

<footnote n="2">2. Figure 6.3 is as close to the standard as it could be made with a structured programming language. This specification differs slightly in that there is no squeezing at all when 0 bits of output are requested. Both specifications are proven functionally equivalent.</footnote>
<figure><img src="image_84.png" /><figcaption>Figure 6.4 – Games defining the indifferentiability of the SPONGE construction from an (ex tendable output) RO.</figcaption></figure>

For concreteness, we give the real experiment and ideal experiments in Figure 6.4 when the notion of indifferentiability is applied to the SPONGE construction, as used in the SHA3 standard and formalized in our proof. In the real game, p is a permutation sampled uni- formly at random from the set of all permutations over bit strings of length 1600. The distinguisher is given access to oracles p_+ and p_- that allow it to query the permutation backwards as well as forwards. In the ideal game, the simulator P = (S+, S-) must fake the outputs of the p_+ and p_- oracles, while oblivious of the calls that the distinguisher places to the construction (which is replaced by a random object in the ideal world). We show the simulator as two different algorithms for clarity, but we allow them to share state. The ideal functionality is an extendable output random oracle. This is implemented as an infi- nite random oracle F that associates to each input an infinite (lazy) bitstring, each element of which is sampled uniformly at random. The distinguisher and simulator are restricted to queries to the ideal functionality of the form (m, l), matching the syntax of the SPONGE interface; these queries return prefixes of size l of the random oracle F outputs (denoted using F_l notation in the security games). In our formalization we consider a random func- tion f ∈ {0, 1}* × N → {0, 1} and construct the observable prefix of length l of the infinite random oracle F as follows:

$$
F(m, \ell) = f(m, 0) \| f(m, 1) \| \dots \| f(m, \ell - 1)
$$

We actually implement f lazily: representing it as a finite map from {0, 1}* × N to {0, 1} to
which we add new input/output pairs as needed.

Our machine-checked proof establishes the following security result for the EasyCrypt
specification of the SPONGE, which corresponds to the pseudo code described in Figure 6.3.

**Theorem 6.2.1 (Indifferentiability of SPONGE).** The SPONGE construction is $(\sigma, \sigma, \frac{\sigma^2-\sigma}{2^{b+1}} + \frac{\sigma^2}{2^{b-r-2}})$-indifferentiable from an extendable output random oracle for any $\sigma < 2^{b-r}$. Namely, the simulator SIMULATOR exhibited in Figure 6.13 makes at most $\sigma$ queries when the adversary makes queries of total cost at most $\sigma$.

$$
\left| \Pr[\mathrm{Real}_{b-r, \mathrm{pad}, r}^{\mathrm{D}} = 1] - \Pr[\mathrm{Ideal}_{\mathrm{P}}^{\mathrm{D}} = 1] \right| \le \frac{\sigma^2}{2^{b-r-2}} + \frac{\sigma^2 - \sigma}{2^{b+1}}
$$

**6.3 Layered Indifferentiability**

Our formalization of definitions and top-level statements is direct: we simply express
the SPONGE, its ideal functionality, and the simulator, as the indifferentiability result in
EasyCrypt is already stated in Theorem 6.2.1.

In order to carry out the proof, we layer it as shown in Figure 6.5 to account for indi-
vidual aspects of the construction. Our layers separately deal with truncation and padding
(SPONGE), and squeezing (BLOCKSPONGE) over a simplified CORESPONGE which outputs
<figure><img src="image_85.png" /><figcaption>Figure 6.5 – A layered proof for the SPONGE construction.</figcaption></figure>

only a single block. The simulator constructed by layers is not optimal in terms of query cost, and we then show its equivalence to the top-level simulator, allowing us to conclude with a tighter concrete security result.

Beyond the proof of indifferentiability for the bare SPONGE construction, we then show that the functions defined in the SHA3 standard [?] inherit specialized version of this indifferentiability, and formally establish concrete security bounds on an adversary's ability to produce collisions, preimages or second preimages on the SHA3 hash functions without first breaking the security assumption on the KECCAK-p permutation. At the highest level, our indifferentiability proof is instantiated to the hash functions SHA3-224, SHA3-256, SHA3-384 and SHA3-512, and extendable output functions SHAKE128 and SHAKE256 as they are defined in the SHA3 standard [?].

### 6.3.1 General Decomposition

The decomposition outlined in Figure 6.5 is made possible by the following general observation. Suppose we have a stateless “upper-level” construction C[RP] that we want to prove to be indifferentiable from an upper-level ideal functionality J. Furthermore, let us assume that we already know that a stateless “lower-level” construction E[RP] is indifferentiable from a lower-level ideal functionality I, where S is a lower-level simulator such that no adversary can effectively distinguish between (E[RP], RP) and (I, S[I]).

We construct a pair of stateless converters D and U that work as follows: D (“down”) transforms an upper-level functionality into a lower-level one; and U (“up”) transforms a lower-level functionality into an upper-level one. We define the upper-level simulator T such that $T[J] := S[D[J]]$. And, for any upper-level adversary $\mathcal{A}$ that is asked to differentiate C from J, let the lower-level adversary $\mathcal{B}[\mathcal{A}]$ be defined as $\mathcal{B}[\mathcal{A}]^{X,Y} := \mathcal{A}^{U[X],Y}$.

Then, to prove that C[RP] is indifferentiable from J, it will suffice to show the following
<figure><img src="image_86.png" /><figcaption>Figure 6.6 – General decomposition argument</figcaption></figure>

two equivalences, as represented in Figure 6.6.

$$ \mathcal{A}^{C[RP],RP} \sim \mathcal{B}[\mathcal{A}]^{E[RP],RP} \qquad (6.1) $$

$$ \mathcal{A}^{J,T[J]} \sim \mathcal{B}[\mathcal{A}]^{I,S[I]} \qquad (6.2) $$

Equivalence (6.1) relates the “real” games, and simply reflects that the modular construction is correct. Equivalence (6.2), on the other hand, pertains to the “ideal” games. Since E is indifferentiable from I for all adversaries, this holds in particular for $\mathcal{B}[\mathcal{A}]$.

Because C and E (and U) are stateless, it is clear what $C[RP] \sim U[E[RP]]$ should mean, and that it will be sufficient to imply that Equivalence (6.1) holds.

However the situation is more complex for the ideal equivalence (6.2), since our ideal functionalities have persistent local state (say, query maps) of different types. Consequently it is unclear what the statements $J \sim U[I]$ and $I \sim D[J]$ would even mean, and we must instead prove finer-grained equivalence statements where equivalence—over the whole game—also defines how the ideal functionalities' states are related.

### 6.3.2 First Layer : SPONGE (not part of my contributions)

The BLOCKSPONGE construction is similar to SPONGE, but works on blocks rather than bits, forgoing padding of inputs and truncation of outputs. The IDEALBLOCK ideal functionality is like the infinite random oracle IDEALSPONGE, except that it, too, works on blocks
rather than bits. Both the construction and ideal functionality should only be called with
lists of blocks that can be successfully unpadded; when called with invalid arguments, they
return the empty list.

We prove that, if BLOCKSPONGE is indifferentiable from IDEALBLOCK, then SPONGE is
indifferentiable from IDEALSPONGE by instantiating the generic argument discussed in Sec-
tion 6.3.1. In this instance, C is SPONGE, E is BLOCKSPONGE, J is IDEALSPONGE, I is IDE-
ALBLOCK, and S is the block sponge simulator. We construct the transformers D and U as
follows:

— D[J'] takes in a list of blocks and a requested length n. If given an input that is not correctly padded, it returns the empty list. Otherwise, it calls J' with the unpadded input and n*r, and then chunks the resulting bitstring into n blocks. It is represented in Figure 6.7.

<figure><img src="image_87.png" /><figcaption>Figure 6.7 – Representation of the construction D with message input of size 4 blocks and asked for an output of size 3 blocks.</figcaption></figure>

— U[I'] takes in a list of bits and a requested length n. It calls I' on the padding of its input and [n/r], and then truncates the result of turning the resulting blocks into a list of bits. It is represented in Figure 6.8.

<figure><img src="image_88.png" /><figcaption>Figure 6.8 – Representation of the construction U with message input of size *m* and asked for an output of size *l* such that *3r* ≤ *m* < *4r* and *2r* < *l* ≤ *3r*.</figcaption></figure>

For the real equivalence $\mathcal{A}^{\text{C[RP],RP}} \sim \mathcal{B}[\mathcal{A}]^{\text{E[RP],RP}}$, we simply prove that the construc-
tion and its modularly-constructed version are equivalent, as $\text{C[RP]} \sim \text{U[E[RP]]}$. This
involves inlining and code rewriting, noting that U simply truncates and pads exactly as the
SPONGE does.

In contrast, and as discussed in Section 6.3.1, the proof of the ideal equivalence $\mathcal{A}^{J,\tau[J]} \sim \mathcal{B}[\mathcal{A}]^{1,S[1]}$ is more complex. We carry it out in three steps, involving *hybrid infinite random*
oracles (hybrid IROs), which are midway between J and I. An input to a hybrid IRO is a well-padded list of blocks and a desired number of output bits. Internally, they work with finite maps from ({0, 1}^r)* × N to {0, 1}. A hybrid IRO can be raised, for comparison with J, or lowered, for comparison with I. Two hybrid IROs are defined: a lazy one, and an eager one. The lazy one consults/updates just enough inputs of its finite map to provide the requested bits, whereas the eager one continues up to a block boundary, consulting/updating subsequent inputs of the finite map, as if it had been asked for a multiple of r bits.

The first step of the proof transitions from $\mathcal{A}^{J,T[J]}$ to a game involving the lazy IRO. This is done by employing a relational invariant between the maps of J and the lazy IRO.

The second step of the proof uses the eager sampling facility of Section 2.3.2 to transition from a game involving the lazy IRO to one involving the eager IRO. A graphical representation is displayed in Figure 6.8. The bridge between these games uses the eager sampling theory's sample oracle to sample the extra bits needed to take one up to a block boundary. The lazy version of sample then gives us the lazy IRO, whereas its eager version gives us the eager IRO.

The third step of the proof takes us from the game involving the eager IRO to $\mathcal{B}[\mathcal{A}]^{1,S[I]}$. This is done by employing an invariant between the maps of the eager IRO and I. The proof is rather involved, and makes use of: (a) EasyCrypt's library's support for showing the equivalence of randomly choosing a block versus forming a block out of r randomly chosen bits; and (b) a mathematical induction over a pRHL judgement.

### 6.3.3 Second Layer : BLOCKSPONGE

The next step in our proof is to show that squeezing, the operation through which the SPONGE's output is extended to any desired length, also preserves indifferentiability. Consider a functionality CORESPONGE that computes only the absorption stage of BLOCKSPONGE (lines 3-5 of Figure 6.3, taking as input a list of blocks, and outputting the final value of $s_a$).

We prove that, if CORESPONGE is indifferentiable from IDEALCORE, then BLOCKSPONGE is indifferentiable from IDEALBLOCK by instantiating the generic argument discussed in Section 6.3.1. In this instance, C is BLOCKSPONGE, E is CORESPONGE, J is IDEALBLOCK, I is IDEALCORE, and S is CORESIM. We construct the transformers D and U as follows:

- D is renamed as SQUEEZE. SQUEEZE[J'] takes a list of blocks m (a padded bitstring) and a desired output length l (in blocks). It iteratively calls $J' \cdot l$ times, with inputs $(m \parallel 0^{r \cdot j})_{0 \le j < l}$, each call producing a single block. It outputs the list of all these blocks in order, as shown in Figure 6.9.

<figure><img src="image_89.png" /><figcaption>Figure 6.9 – BLOCKSPONGE [RP] and SQUEEZE ◦ CORESPONGE[RP] on inputs that are a list of 4 blocks and output size 3.</figcaption></figure>
— U is renamed as LAST. LAST[l'] takes in a list of blocks and outputs a single block. It parses the list of blocks into a pair of a valid list of blocks — that terminates with a non full-0 block — and an output size. It then calls l' on this pair, obtaining a list of blocks from which it outputs only the last block, as shown in Figure 6.10.

<figure><img src="image_90.png" /><figcaption>Figure 6.10 – IDEALCORE and LAST[IDEALBLOCK] on input that is a 6-blocks list whose last two blocks are full of 0.</figcaption></figure>

For the real equivalence SQUEEZE ◦ CORESPONGE[RP] ∼ BLOCKSPONGE[RP], since the primitive RP appears deterministic (and in particular returns the same output when queried twice on the same input) it is easy to prove in EasyCrypt that this equivalence holds.

As before, the ideal equivalence here must be expressed and proved over the whole game, and indeed requires relating the states of ideal functionalities and simulator based on queries done on both interfaces. We thus prove in EasyCrypt for all adversaries $\mathcal{A}$

$$ \mathcal{A}^{\text{SQUEEZE}[\text{IDEALCORE}], \text{CORESIM}[\text{IDEALCORE}]} \sim \mathcal{A}^{\text{IDEALBLOCK}, \text{CORESIM}[\text{LAST} \circ \text{IDEALBLOCK}]} $$

Once again, this proof leverages the generic lazy-eager sampling theory described in Section 2.3.2 to prove that the intermediate blocks sampled and thrown away by LAST[IDEALBLOCK] can instead not be sampled at all.

## On the query cost

In this particular application of the decomposition, the cost in number of permutation queries differs greatly between BLOCKSPONGE[RP] and SQUEEZE ◦ CORESPONGE[RP], resulting in a lost in the security bound. Considering the example shown in Figure 6.9, the cost of that query to BLOCKSPONGE is 6 permutation calls, but the same query to SQUEEZE ◦ CORESPONGE costs $4+5+6=15$ permutation calls. Simply applying the decomposition as described would yield a bound dominated by $O(\sigma^4/2^r)$.

We therefore also use this transfer result to refine the way in which the cost of a query in CORESPONGE is measured, to avoid double-counting common prefixes. This is done through a construction named PREFIXES applied to BLOCKSPONGE [RP] and CORESPONGE [RP] that stores all resulting states of the absorption phase from all queries's prefixes. For any fresh query, it takes the longest common prefix with all previous queries, and starts with the stored state for this prefix. That way, all calls to RP that follow the same prefix as a previous query's are avoided. Then, it continues squeezing with RP for the rest of the query's blocks.
### 6.3.4 Core Layer : CORESPONGE

All proof steps discussed thus far involve transferring indifferentiability from a simple construction to a more complex one. We now focus on the core of the SPONGE construction, a block-oriented construction that, on input a list of blocks, produces a single block of output.

As discussed above, our notion of query cost on this CORESPONGE construction differs from the top-level notion, and is defined instead as the length of the query without its longest common prefix with any of the previous queries. We call this cost the *prefix cost* of a query. Considering this notion of cost requires us to carefully design the CORESPONGE by integrating the construction PREFIXES to ensure that the prefix cost and query cost of the same query align when transferring indifferentiability to BLOCKSPONGE. We prove in EasyCrypt that CORESPONGE is indifferentiable from IDEALCORE.

As a first simplifying step, we replace the primitive, a random permutation, with a random function. This simplifies some of the formal reasoning—in particular by removing internal dependencies between samplings in the random permutation—but introduces an additional term $\frac{\sigma^2-\sigma}{2^{b+1}}$ in the bound. We note that all results discussed above transfer indifferentiability *without loss*. Therefore, improving the bound for this simpler functionality would be sufficient in improving the bound for the whole SPONGE construction at almost no formal cost beyond that of tightening the bound for CORESPONGE.

#### The idea behind the simulator

Indifferentiability requires us to simulate answers to the permutation, in a way that is consistent with what the adversary may have already observed of the ideal functionality, without knowing which queries the distinguisher has made—or will make—to the functionality. To do so, the simulator CORESIM, shown in Figure 6.11, keeps track of *paths*—which

<figure><img src="image_91.png" /><figcaption>Figure 6.11 – The core simulator CORESIM</figcaption></figure>

are sequences of blocks that, when fed through CORESPONGE, leave its state with a particular value of the capacity—and uses the functionality to simulate its answer to any query
that makes use of a capacity to which a path is known, that is, a query that extends a known path through CORESPONGE. Queries that are disjoint from path are answered as if by the ideal random function.

## When the simulation fails

The indifferentiability between the real game and the ideal game mainly relies on the unicity of capacities that appears in the different absorbtion phases. Therefore, when an event occurs that contradicts this unicity, the simulation fails. More specifically, it fails (and can be distinguished from the true permutation) if either one of the following events occurs:

* bcol: A capacity that was previously seen as output of the permutation with a block $s_a$ has been output again, associated with a different block $s'_a$.

<figure><img src="image_92.png" /><figcaption>Figure 6.12 – Representation of bcol.</figcaption></figure>

* bext: The adversary has queried the primitive or its inverse with a capacity that has already been, or is later sampled internally by CORESPONGE, but to which the simulator does not know a path. In other words, it guessed a value of a hidden capacity, i.e. that was or will be an intermediate capacity in an absorbtion phase.

We show in EasyCrypt that these are the only conditions under which the distinguisher can indeed distinguish the construction from the ideal functionality.

## Bounding the probability of a simulation failure

It remains to bound the probability that these bad events occur. The collision event bcol is straightforward since it occurs as values are sampled and its probability can be bounded immediately.

On the other hand, bounding the probability that bext occurs in any particular run is much more complex, as it requires identifying that the adversary has guessed a previously sampled value, or will be sampled later on in the run. We note, however, that the event is only triggered when the adversary guesses a value that is independent from its view of the system: indeed CORESPONGE keeps all capacities internal, and the event does not consider the case where the adversary has obtained the capacity's value through a legitimate sequence of calls to the permutation that mimics CORESPONGE's operations. The trick is therefore to delay the sampling of capacities that are used in CORESPONGE until the end of the game (at which point we can sample them all, and easily bound the probability that any one of them was used by the adversary), or until the simulator constructs a path to it, at which point bext is no longer triggered.

In order to deploy the lazy-eager sampling theory described in Section 2.3.2, we must first remove the dependencies between capacities and rates introduced by their joint use in the permutation.
### A proof trick: indirection

We deploy an indirection technique similar to that used in [Backes et al., 2012] that proves indifferentiability of Merkle-Damgård. Since only the unicity of capacities is needed in the indifferentiability rather than their value, we deploy an isomorphism (that stays an isomorphism if no failure event happens) that associates a counter (with type handle in Section 6.4) to each capacity.

Concretely, each fresh permutation query (made by the adversary or the functionality) is tagged with its indirection number. The main permutation map (G1.mh) is used to keep track, given an input state, of the rate that was returned, and of the indirection number. An auxiliary map is used to translate indirection numbers into capacities (FRO.m).

This auxiliary map can then be sampled lazily: on direct permutation queries, both rate and capacities are sampled and returned to the distinguisher; on permutation queries made by the construction, the rate is sampled and associated with an indirection number, but the capacity is not sampled. A loop after the distinguisher has finished running samples all remaining capacities — that is, exactly those that have been used in the construction, but not been observed as part of a path — triggering the bad event a *posteriori* if any one of them collides with an adversarial input that is not part of a path. This last transformation makes heavy use of the lazy-eager sampling theory described in Section 2.3.2, including in particular the use of programming queries in some cases.

## 6.3.5 The final SPONGE simulator

As described in Figure 6.5, the simulator resulting from the proof described above is constructed from the modular layers as:

SPONGESIM[BLOCKSIM[CORESIM[·]]]

The final step of our proof is to collapse the layered construction into a final simulator, shown in Figure 6.13. This allows us to reduce the cost of simulator queries, aligning them with the announced notion of query cost, and to present the simulator as a single algorithm. However, the layered nature of the simulator can still be seen in this final presentation: the core simulator still appears, keeping track of paths through the simulated permutation that could correspond to functionality calls and extending them as required, or simply simulating the random permutation with a random function. However, the way in which paths are extended in the layered simulator (lines 5-16 in Figure 6.13 replacing the single line 5 in Figure 6.11) reflects the different layers required to turn a path through the core sponge (a well-padded bitstring followed by a number of $0^r$ blocks) into a valid query to the SPONGE (a bitstring that the SPONGE itself pads and a number of desired output bits), also turning the output of the SPONGE (a list of bits of the requested length) into the expected output for the core simulator (a single block). For top-level simulator queries that would yield invalid queries to any intermediate functionalities (for example because they correspond to paths that do not reflect well-padded inputs), the layered simulator simply simulates an independent random function.

In other words, our final simulator is CORESIM where the ideal functionality IDEALCORE itself is further simulated from the top-level IDEALSPONGE ideal functionality.
<figure><img src="image_93.png" /><figcaption>Figure 6.13 – The optimized SIMULATOR for SPONGE</figcaption></figure>

## 6.4 A deeper look at the upto-bad game

In this section, instead of describing the full formal proof that has been verified in Easy-Crypt, I describe the formalization of the game named G1 and the invariant that are both involved in the upto-bad formal proof of the indifferentiability. Placing G1 in the context:

— G1 is indifferentiable from the real game with CORESPONGE and RP:

$$ \left| \Pr[\text{Real}_{b-r,pad,r}^{\text{D}} = 1] - \Pr[G1 = 1] \right| \le \Pr[G1 : G1.bcol \lor G1.bcol] \le \frac{\sigma^2}{2^{b-r-2}} + \frac{\sigma^2 - \sigma}{2^{b+1}} $$

— and G1 is equivalent to the ideal game with IDEALCORE and CORESIM:

$$ \Pr[G1 = 1] = \Pr[\text{Ideal}_p^{\text{D}} = 1] $$

In this part, I first describe the meaning of G1's global variables, then other global variables and modules, then each procedure, and finally the invariant that holds when proving the indifferentiability upto the bad event $G1.bext \lor G1.bcol$.
<figure><img src="image_94.png" /></figure>

EasyCrypt

type state = block * capacity.

type smap = (state, state) fmap.

type handle = int.

type hstate = block * handle.

type hmap = (hstate, hstate) fmap.

module G1 (D : DISTINGUISHER) = {

var m, mi : smap

var mh, mhi : hmap

var chandle : int

var paths : (capacity, block list * block) fmap

var bext, bcol : bool

module M = { proc f(p : block list): block = { (* functionality *) } }

module S = {

proc f(x : state): state = { (* primitive *) }

proc fi(x : state): state = { (* inverse *) }

}

proc main(): bool = {

var b;

(* initialization *)

b ← D(M,S).distinguish();

return b;

}}.

The intuition of G1's global variables is as follows:

- G1.chandle: is the next indirection number that is attributed to a new capacity.

- G1.m, G1.mi: represented in Figure 6.14, they are the finite maps that keep track of the simulator's answers to queries, with G1.m for the permutation, and G1.mi for its inverse.

<figure><img src="image_95.png" /><figcaption>Figure 6.14 – Representation of G1.m and G1.mi</figcaption></figure>

- G1.mh, G1.mhi: represented in Figure 6.15, they are the finite maps that help compute the absorbtion phase where capacities are replaced by their indirection number, with G1.mh for the permutation, and G1.mhi for its inverse.

- G1.paths: represented in Figure 6.16, this is the finite map that keeps track of how each computed capacity was obtained from the absorbtion phase of a block list. The block associated is the one output at the same time as the capacity at the end of the absorbtion.

- G1.bext, G1.bcol: are booleans that identify the triggering of bad events.

The other global variables and modules that appear in G1 or in the invariant are:
<figure><img src="image_96.png" /><figcaption>Figure 6.15 – Representation of G1.mh and G1.mhi</figcaption></figure>

<figure><img src="image_97.png" /><figcaption>Figure 6.16 – Representation of G1.path s</figcaption></figure>

— C.queries: represented in Figure 6.17, this is the finite map that keeps track of all the answers of the functionnality. It prevents the adversary to ask again its first oracle the non-fresh queries, and helps compute the maximum size of commom prefixes with previous queries.

<figure><img src="image_98.png" /><figcaption>Figure 6.17 – Representation of C.queries</figcaption></figure>

— FRO.m: is the finite map that keeps track of the value of the capacity that is associated to each indirection number. It is also associated to the flag that states if the capacity is in the adversary’s view: Known or Unknown.

— F.RO: is the module that represents the ideal random function IDEALCORE.

— P.m, P.mi: are the finite maps of the permutation in the real setting that keeps track of all the permutation's answers to queries made either by the adversary or during the absorbtion, with m for the permutation, and mi for its inverse.

— Redo.prefixes: represented in Figure 6.18, this is the map that keeps track of all the states that are a result of an absorption of one of the queries' prefixes.

Invariant

The invariant that holds when none of the bad events has been triggered is a conjonction
of the following ten properties:
<figure><img src="image_99.png" /><figcaption>Figure 6.18 – Representation of Redo prefixes</figcaption></figure>

1. In the map FRO.m, unique capacities are associated to each indirection number, the indirection number 0 is associated to the full-0 capacity (Known), and all indirection numbers are positive and less than chandle (the next indirection number to set).

2. The maps G1.mh and G1.mhi are inverse to each other.

3. The maps P.m and P.mi are inverse to each other.

4. Represented in Figure 6.19, if a state is in P.m, then the corresponding pair is in G1.mh, following the associations of indirection number and capacity provided by FRO.m.

<figure><img src="image_100.png" /><figcaption>Figure 6.19 – Representation of the first property of 4.</figcaption></figure>

Inversely, if a pair is in G1.mh, the corresponding state is in P.m, following FRO.m.
This is represented in Figure 6.20.

<figure><img src="image_101.png" /><figcaption>Figure 6.20 – Representation of the second property of 4.</figcaption></figure>

5. Same as 4 but for P.mi, G1.mhi and FRO.m.

6. The map G1.m is included in the map P.m.

7. The map G1.mi is included in the map P.mi.
8. This property is about building paths and is divided into a conjunction of three sub- properties:

(a) Represented in Figure 6.21, if some pair is in G1.mh, then either the flag corre- sponding to both input and output's indirection numbers is Known and G1.m has the corresponding entries, or the resulting flag is Unknown and the absorbtion path exists upto this point.

<figure><img src="image_102.png" /><figcaption>Figure 6.21 – Representation of the property 8a.</figcaption></figure>

(b) There is an equivalence between the belonging of a list to F.RO's map and build-
ing the full absorbtion path with G1.mh, as represented in Figure 6.22.

<figure><img src="image_103.png" /><figcaption>Figure 6.22 – Representation of the property 8b.</figcaption></figure>

(c) While building paths using G1.mh, the resulting indirection number identifies a unique list and a unique resulting block, as represented in Figure 6.23.

9. For every entry in the map G1.path, the absorbtion path built from G1.mh exists in full, and the resulting indirection number associated to this resulting capacity has the flag Known in FRO.m.

10. This property is about the prefix map and is divided into a conjunction of three sub-
properties:

(a) Each computation of absorbtion through P.m are stored in Redo.prefixes.

(b) The map C.queries is a sub-map of Redo.prefixes.

(c) If a list of blocks is in Redo.prefixes, then it is a prefix a previous query stored in C.queries.
<figure><img src="image_104.png" /></figure>

<figure><img src="image_105.png" /></figure>

$$ i = j \Rightarrow \text{[Grid]} = \text{[Grid]} \quad \text{and} \quad \overrightarrow{\text{[Grid]} \cdots \text{[Grid]}} = \text{[Grid]} \cdots \text{[Grid]} $$

<caption>Figure 6.23 – Representation of the property 8c.</caption>

Initialization

<figure><img src="image_106.png" /></figure>

EasyCrypt

module G1(D:DISTINGUISHER) = {
(* global variables, module M, module S *)

proc main(): bool = {
var b;
(* initializing all the global variables *)

F.RO.m ← empty;

m ← empty;

mi ← empty;

mh ← empty;

mhi ← empty;

bext ← false;

bcol ← false;

C.queries ← empty[[ ← b0];

(* the empty path is initially known by the adversary to lead to capacity 0^c *)

FRO.m ← empty[0 ← (c0, Known)];

paths ← empty[c0 ← ([<:block>],b0)];

chandle ← 1;

(* call the distinguisher and outputs its answer *)

b ← D(M,S).distinguish();

return b;

}

<caption>Listing 6.1 – Initialization of global variables</caption>
## Functionality

The submodule M implements the functionnality that is functionnally equivalent to the ideal random function previously named IDEALCORE and implemented by F.RO. It keeps an absorption structure with the indirection described in the previous section. The map that associates states to states P.m is replaced by the indirection map G1.mh that associates a pair composed of a block and a indirection number to a pair composed of a block and another indirection number.

<figure><img src="image_107.png" /></figure>

### EasyCrypt

```python
module G1(D:DISTINGUISHER) = {
    (* global variables *)
    module M = {
        proc f(p : block list): block = {
            var sa, sa', sc;
            var h, i, counter ← 0; (* all three variables are initialized to 0 *)
            (sa,sc) ← (b0,c0); (* initial state *)
            while (i < size p) {
                if ((sa + ^ nth witness p i, h) ∈ mh) (* if the path is already known *) {
                    (sa, h) ← oget mh[(sa + ^ nth witness p i, h)]; (* follow it *)
                } else {
                    (* check if the prefix cost is respected (helpful when proving the invariant) *)
                    if (counter < size p - prefix p (get_max_prefix p (elem s (fdom C.queries)))) {
                        sc ← cdistr; (* sample the next capacity *)
                        (* does it trigger a bad event ? *)
                        bcol ← bcol ∨ hinv FRO.m sc ≠ None;
                        (* ask to the random oracle for the next block *)
                        sa' ← F.RO.get(take (i+1) p);
                        (* xors the message's block with the last block of the absorption *)
                        sa ← sa + ^ nth witness p i;
                        (* updates the indirection map and its inverse *)
                        mh[(sa,h)] ← (sa', chandle);
                        mhi[(sa',chandle)] ← (sa, h);
                        (* adds the correspondance of the indirection number to its capacity *)
                        FRO.m[chandle] ← (sc,Unknown);
                        (* updates iterative variables *)
                        (sa,h) ← (sa',chandle);
                        chandle ← chandle + 1;
                        counter ← counter + 1;
                    }
                    } (* end if (···, h) ∈ mh *)
                    i ← i + 1;
                } (* end while *)
                (* ask for the block associated to the full message *)
                sa ← F.RO.get(p);
                return sa;
            }
        }
        (* module S *)
        (* proc main *)
    }.
```

<caption>Listing 6.2 – Algorithm of the functionnality in G1</caption>
In this procedure, the bad event bcol can be triggered using the operator hinv. It looks into the map given as its first argument to find a indirection number that may be associated to the capacity given as its second argument, that may be associated with the flag Known or Unknown. If the bad event is triggered, this means that either there is a collision of capacities with two different messages (two different absorbtion paths), or the adversary correctly guessed a capacity before it was sampled.

## Simulation of the permutation

The other sub-module of G1 is named S and is given to the adversary as the primitive. We show in EasyCrypt that the sub-module S is equivalent to the simulator in Figure 6.11. The next EasyCrypt's code outlines the inverse permutation that is simpler than the direct permutation, followed by the direct permutation.

<figure><img src="image_108.png" /></figure>

```pascal
module G1(D:DISTINGUISHER) = {
  (* global variables *)
  (* module M *)
module S = {
  proc f(x : state): state = { (* ... *) }
  proc fi(x : state): state = {
    var y, y1, y2, hx2, hy2;
    if (x \ notin mi) {
      (* has the adversary guessed one of the sampled non-revealed capacities *)
      bext ← bext ∨ rng FRO.m (x.`2, Unknown);
      (* updates the maps associating indirection numbers to capacities (and known/leable flags) *)
      if (¬(rng FRO.m (x.`2, Known))) {
        FRO.m[chandle] ← (x.`2, Known);
        chandle ← chandle + 1;
      }
      (* obtain the indirection number *)
      hx2 ← oget (hinvK FRO.m x.`2);
      (* sample the output *)
      y1 $← bdistr;
      y2 $← cdistr;
      y ← (y1,y2);
      (* if the input block is associated to the obtained indirection number, and the capacity associated to the next indirection number is unknown to the adversary, follow the path *)
      if ((x.`1,hx2) ∈ mhi ∧ in_with FRO.m (oget mhi[(x.`1,hx2)].`2 Unknown)) {
        (y1,hy2) ← oget mhi[(x.`1, hx2)];
        y ← (y.`1, (oget FRO.m[hy2]).`1);
        FRO.m[hy2] ← (y.`2, Known);
        (* update the maps of the simulator with the computed values *)
        mi[x] ← y;
        m[y] ← x;
      } else {
        (* the bad event is triggered if the capacity sampled already has appeared *)
        bcol ← bcol ∨ hinv FRO.m y.`2 ≠ None;
        (* update the maps to keep the absorbing structure *)
        hy2 ← chandle;
        chandle ← chandle + 1;
        FRO.m[hy2] ← (y.`2, Known);
        mi[x] ← y;
      }
```
```python
mhi[(x.`1, hx2)] ← (y.`1, hy2);
m[y] ← x;
mh[(y.`1, hy2)] ← (x.`1, hx2);
}
} else {
    y ← oget mi[x];
}
return y;
}
}
(* proc main *)
}.
```

Listing 6.3 – Inverse permutation that is equivalent to the simulator

The direct permutation is the only procedure that uses the global variable paths. That way, if the adversary asks a query that is part of an absorbtion computation, the variable paths will keep track of the message from which it is a absorbtion, and the simulator will asks F.RO for the next block. In any case, the capacity is sampled in the same way as for the inverse procedure.

<figure><img src="image_109.png" /></figure>

EasyCrypt

```python
module G1(D:DISTINGUISHER) = {
    (* global variables *)
    (* module M *)
    module S = {
        proc f(x : state): state = {
            var p, v, y, y1, y2, hy2, hx2;
            (* has this state not already been queried to S.f or was an output of S.fi ? *)
            if (x \notin m) {
                (* is this capacity output from an absorbing phase ? *)
                if (x.`2 ∈ paths) {
                    (* if so, get the message and output block associated to this capacity *)
                    (p,v) ← oget paths[x.`2];
                    (* call the ideal random function as if this query was part of an absorbtion phase *)
                    y1 ← F.RO.get (rcons p (v + ^ x.`1));
                    (* sample the capacity normally *)
                    y2 ← $ c distr;
                } else {
                    (* sample both block and capacity normally *)
                    y1 ← $ b distr;
                    y2 ← $ c distr;
                }
                y ← (y1, y2);
                (* bad event : was the queried capacity part of a previous absorbtion phase ? *)
                bext ← bext ∨ rng FRO.m (x.`2, Unknown);
                (* updates the map associating indirection numbers to capacities and knowledgable flags *)
                if (¬(rng FRO.m (x.`2, Known))) {
                    FRO.m/chandle ← (x.`2, Known);
                    chandle ← chandle + 1;
                }
                (* obtain the indirection number associated to the queried capacity *)
                hx2 ← oget (hinvK FRO.m x.`2);
                (* test if the indirection number that is next after (y.`1,hx2) is already associated to a capacity *)
            }
        }
    }
}
```
```c
if ((x. `1, hx2) ∈ mh ∧ in_with FRO.m (oget mh[(x. `1, hx2)]). `2 Unknown) {
    (* then erase the sampled capacity and output the associated capacity *)
    hy2 ← (oget mh[(x. `1, hx2)]. `2;
    y ← (y. `1, (oget FRO.m[hy2]). `1);
    FRO.m[hy2] ← (y. `2, Known);
    m[x] ← y;
    mi[y] ← x;
} else { (* otherwise, associate this capacity to the indirection number with the flag Known *)
    (* bad event triggered if the capacity is already associated to a previous indirection number *)
    bcol ← bcol ∨ hinv FRO.m y. `2 ≠ None;
    (* update the maps and global variables *)
    hy2 ← chandle;
    chandle ← chandle + 1;
    FRO.m[hy2] ← (y. `2, Known);
    m[x] ← y;
    mh[(x. `1, hx2)] ← (y. `1, hy2);
    mi[y] ← x;
    mhi[(y. `1, hy2)] ← (x. `1, hx2);
}
(* same test as the beginning *)
if (x. `2 ∈ paths) {
    (* update the known path of a given capacity *)
    (p, v) ← oget paths[x. `2];
    paths[y. `2] ← (rcons p (v + ^ x. `1), y. `1);
}
else {
    y ← oget m[x];
}
return y;
}
proc fi(x: state): state = { (* ... *) }
(* proc main *)
}
```

<caption>Listing 6.4 – Permutation that is equivalent to the simulator</caption>
Part IV

Confidentiality and Authentication
<figure><img src="image_110.png" /></figure>
# Chapter 7

## Security of Authenticated Encryption

In cryptography, *encryption* is the process of encoding information, often encoded as a message, in such a way that only authorized parties can access it while non-authorized others cannot. In an encryption scheme, the intended message, referred to as *plaintext*, is encrypted using an encryption algorithm — a *cipher* — generating a *ciphertext* that can be read — whose meaning can be retrieved — only if decrypted. Sender and recipient share keys that can encrypt and decrypt messages. When the encryption key is the same as the decryption key, the scheme is called *symmetric encryption* (or *private key encryption*), otherwise it is called *asymmetric encryption* (or *public key encryption*). In my manuscript, I focus on the security of symmetric encryption.

The objective of encryption is to deny the intelligible content to a would-be interceptor. This security property is called *data confidentiality*. This means that any entity that does not possess the secret key is unable to retrieve information on plaintext from ciphertext.

### 7.1 Authenticated Encryption

Data confidentiality has been one of main goals of cryptography for quite a long time, while the need to combine *data integrity* with confidentiality came from the banking field.

<figure><img src="image_111.png" /></figure>

**Example**

Integrity of banking transactions, e.g. the price agreed upon, is a main concern, especially when using substitution ciphers. In this setting, an attacker does not need to decrypt the ciphertext, but just flip a coin and change the amount in the transaction without knowing the secret key. This concern may be extended to any encryption scheme, even without the malleability of substitution ciphers; banks did not want to transmit encrypted data that would allow an attacker to change messages undetected.

*Authenticated encryption (AE) and *authenticated encryption with associated data (AEAD)* are forms of encryption which simultaneously aim to provide the confidentiality and authenticity of data, the associated data being a non-encrypted part of the message that is nonetheless authenticated (e.g. packet header for transportation across the network).

The easiest way to create a AE scheme is to combine an existing encryption scheme with an existing message authentication code (MAC) scheme with two different secret keys. In [Bellare and Namprempre, 2000], Bellare and Namprempre analyze the security of three general compositions of encryption schemes and MAC schemes: 1. Encrypt-then-MAC 2. Encrypt-and-MAC 3. MAC-then-Encrypt. In their work, they prove that, under the security
assumption that the encryption scheme and the MAC scheme are secure, only the general approach Encrypt-then-MAC provides a secure authenticated encryption scheme.

This means that the other two are in general insecure. Indeed, securely combining separate confidentiality and authentication block cipher operation modes can be difficult and error prone. « In fact, efficient integration of encryption, authentication, and message integrity using a single shared key is an important and intensely studied problem in network security [Kaufman et al., 1995, Perlman et al., 2016, Preneel, 1998] which is solved by the use of [an authenticated] encryption scheme.» ([Katz and Yung, 2000b]) This issue has been raised for decades, and a recent example of an attempt to answer it is the CAESAR competition [CAE, 2013] that aimed to determine the best AE scheme through a long process of public competitive peer review.

## 7.2 Security Definitions

Against a secure encryption scheme, any adversary should learn no information from seeing a ciphertext. Therefore, the adversary should be able to do no better than if it guessed randomly. The following definition encompasses this security notion.

An encryption scheme is considered secure if no adversary, given an encryption of a message randomly chosen from a two-element message space determined by the adversary, can identify the message choice with probability significantly better than that of random guessing ($\frac{1}{2}$). If any adversary can succeed in distinguishing the chosen ciphertext with a probability significantly greater than $\frac{1}{2}$, then this adversary is considered to have an advantage in distinguishing the ciphertext, and the scheme is not considered secure.

Security in terms of indistinguishability has several definitions, depending on assumptions made about the adversary's capabilities. The most common definitions used in provable security — first in the public-key setting [Bellare et al., 1997, Bellare et al., 1998a], then extended into the private-key setting [Katz and Yung, 2000a] — are indistinguishability under chosen plaintext attack (IND-CPA), indistinguishability under (non-adaptive) chosen ciphertext attack (IND-CCA1 [Naor and Yung, 1990]), and indistinguishability under adaptive chosen ciphertext attack (IND-CCA2 [Rackoff and Simon, 1991]).

Security under either of the latter definition implies security under the previous ones: a scheme which is IND-CCA1 secure is also IND-CPA secure, and a scheme which is IND-CCA2 secure is both IND-CCA1 and IND-CPA secure. Thus, IND-CCA2 is the strongest of the three definitions of security.

Intuitively, the IND-CPA security is the security definition relative to data confidentiality; information about plaintexts cannot be retrieved from ciphertexts without knowing the secret key. Whereas the IND-CCA2 security also includes data integrity and authentication; that is, in addition, no valid ciphertext can be produced without the secret key.

<figure><img src="image_112.png" /></figure>

**Example**

In [Garman et al., 2016], Garman et al. found an adaptive chosen ciphertext attack (showing the IND-CCA2 insecurity) against Apple's iMessage in which they achieve to break the security of a ciphertext if they have access to $2^{18}$ decryption oracle queries after the ciphertext they want to break is obtained. « The practical implication of these attacks is that any party who gains access to iMessage ciphertexts may potentially decrypt them remotely and after the fact.» ([Garman et al., 2016])
### 7.2.1 IND-CPA

A chosen-plaintext attack (CPA) is an attack model for cryptanalysis which presumes that the attacker can obtain the ciphertexts for arbitrary plaintexts. The goal of the attack is to gain information that reduces the security of the encryption scheme.

In a chosen-plaintext attack, the adversary can adaptively ask for the encryption of arbitrary plaintext messages. This is formalized by allowing the adversary to interact with an encryption oracle, viewed as a black box that encrypts plaintexts using the secret key. The attacker's goal is to retrieve any information or pattern about encrypted plaintexts.

The game IND-CPA is works as follows.

1. The game initializes the secret key of the encryption scheme.

2. The adversary interacts with the encryption oracle by querying adaptive plaintexts.

3. The adversary submits a challenge that consists of a pair of two plaintexts $m_0, m_1$.

4. The game randomly samples a bit $b \in \{0, 1\}$ and sends to the adversary the ciphertext associated to $m_b$.

5. The adversary may ask for new queries to the encryption oracle.

6. The adversary outputs a bit $b'$ that represents its guess of the bit $b$.

The adversary has won if it guessed correctly, i.e. $b = b'$.

<figure><img src="image_113.png" /></figure>

#### EasyCrypt

```python
module type Enc = {
    proc key_gen() : key
    proc enc(_: key * plaintext) : ciphertext
    proc dec(_: key * ciphertext) : plaintext
}.
```

```python
module type CPA_Oracles = {
    proc enc(_: plaintext) : ciphertext
}.
```

```python
module Mem (E : Enc) : CPA_Oracles = {
    var key : key
    proc enc (m : plaintext) = {
        var c;
        c ← E.enc(Mem.key, m);
        return c;
    }.
```

```python
module type Adv_CPA (E : CPA_Oracles) = {
    proc challenge() : plaintext * plaintext { E.enc }
    proc guess(_: ciphertext) : bool { E.enc }
    (* remove E.enc when the adversary is not
     allowed to ask for further encryptions *)
}.
```

```python
module IND_CPA (A : Adv_CPA, E : Enc) = {
    proc game() : bool = {
        var b, b', m0, m1, c;
        Mem.key ← E.key_gen();
        (m0, m1) ← A(Mem(E)).challenge();
        b ← {0,1};
        c ← Mem(E).enc(b ? m1 : m0);
        b' ← A(Mem(E)).guess(c);
        return b = b';
    }.
```

The IND-CPA advantage of an adversary $\mathcal{A}$ against an encryption scheme E is defined as

$$ \mathrm{Adv}_E^{\mathrm{ind-cpa}}(\mathcal{A}) := \left| \Pr[b \leftarrow \mathrm{IND\_CPA}(\mathcal{A}, E).\mathrm{game}() : b = 1] - \frac{1}{2} \right| $$

### 7.2.2 IND-CCA1 and IND-CCA2

Indistinguishability under non-adaptive and adaptive Chosen Ciphertext Attack (IND-CCA1, IND-CCA2) uses a definition similar to that of IND-CPA. However, in addition to
the encryption oracle, the adversary is given access to a decryption oracle which decrypts arbitrary ciphertexts at the adversary's request, returning either the plaintext or an error message stating that the ciphertext provided is not well-formed. In the non-adaptive definition, the adversary is allowed to query the decryption oracle only up to receiving the challenge ciphertext. In the adaptive definition, the adversary may continue to query the decryption oracle even after receiving the challenge ciphertext, with the caveat that it may not ask the challenge ciphertext for decryption (otherwise, the definition would be trivial).

The game IND-CCA works as follows, where the difference between IND-CCA1 and IND-CCA2 is respectively either the absence or presence of the decryption oracle in step 5.

1. The game initializes the secret key of the encryption scheme.

2. The adversary interacts with both the encryption and decryption oracles by querying adaptative plaintexts and ciphertexts.

3. The adversary submits a challenge that consists of a pair of two plaintexts $m_0, m_1$.

4. The game randomly samples a bit $b \in \{0, 1\}$ and sends to the adversary the ciphertext associated to $m_b$.

5. The adversary may ask for new queries to the encryption (and decryption) oracles (with the restriction of not asking for the decryption of the challenge's ciphertext).

6. The adversary outputs a bit $b'$ that represents its guess of the bit $b$.

The adversary has won if it guessed correctly, i.e. $b = b'$.

## IND-CCA1

The IND-CCA1 advantage of an adversary $\mathcal{A}$ against an encryption scheme E is defined as

$$ \mathrm{Adv}_{\mathrm{E}}^{\mathrm{ind-cca1}}(\mathcal{A}) := \left| \Pr[b \leftarrow \mathrm{IND\_CCA1}(\mathcal{A}, E).\mathrm{game}() : b = 1] - \frac{1}{2} \right| $$

### EasyCrypt

```pascal
module type CCA_Oracles = {
    proc enc(_: plaintext) : ciphertext
    proc dec(_: ciphertext) : plaintext option
}.```

```pascal
module Mem (E : Enc) : CPA_Oracles = {
    var key : key
    proc enc (m : plaintext) = {
        var c;
        c ← E.enc(Mem.key, m);
        return c;
    }
    proc dec (c : ciphertext) = {
        var p;
        p ← E.dec(Mem.key, c);
        return p;
    }.
```

```pascal
module type Adv_CCA1
    (E : CCA_Oracles) = {
    proc challenge()
        : plaintext * plaintext { E.enc E.dec }
    proc guess(_: ciphertext)
        : bool { E.enc } (* E.dec is absent *)
    }.
```

```pascal
module IND_CCA1 (A : Adv_CCA1, E : Enc) = {
    proc game() : bool = {
        var b, b', m0, m1, c;
        Mem.key ← E.key_gen();
        (m0, m1) ← A(Mem(E)).challenge();
        b ← {0,1};
        c ← Mem(E).enc(b ? m1 : m0);
        b' ← A(Mem(E)).guess(c);
        return b = b';
    }.
```
## IND-CCA2

The IND-CCA2 advantage of an adversary $\mathcal{A}$ against an encryption scheme E is defined as

$$ \mathrm{Adv}_{\mathrm{E}}^{\mathrm{ind-cca2}}(\mathcal{A}) := \left| \Pr[b \leftarrow \mathrm{IND\_CCA2}(\mathcal{A}, E).\mathrm{game}() : b = 1] - \frac{1}{2} \right| $$

### EasyCrypt

```pascal
module Mem (E : Enc)
    : CPA_Oracles = {
    var key : key
    var cipher : ciphertext option
    proc enc (m : plaintext) = {
        var c;
        c ← E.enc(Mem.key, m);
        return c;
    }
    proc dec (c : ciphertext) = {
        var p;
        if (Some c = Mem.cipher) { p ← None; }
        else { p ← E.dec(Mem.key, c); }
        return p;
    }}.
module type Adv_CCA2 (E : CCA_Oracles) = {
    proc challenge()
        : plaintext * plaintext { E.enc E.dec }
    proc guess(_: ciphertext): bool { E.enc E.dec }
```

```pascal
module IND_CCA2 (A : Adv_CCA2, E : Enc) = {
    proc game() : bool = {
        var b, b', m0, m1, c;
        Mem.key ← E.key_gen();
        Mem.cipher ← None;
        (m0, m1) ← A(Mem(E)).challenge();
        b ← {0,1};
        c ← Mem(E).enc(b ? m1 : m0);
        Mem.cipher ← Some c;
        b' ← A(Mem(E)).guess(c);
        return b = b';
    }}.
```

<figure><img src="image_114.png" /></figure>

### Remark

In the following, whenever we talk about IND-CCA, we refer to IND-CCA2 unless stated otherwise.

### 7.2.3 INT-CTXT : Integrity of the CipherTeX

First named *unforgeable encryption* in [Katz and Yung, 2000b], *integrity of ciphertexts* (INT-CTXT) is a security requirement necessary for any protocol that wants to detect any unauthentic ciphertext. That is, no one without the secret key should be able to produce a ciphertext that can be successfully decrypted, even if valid ciphertexts can be asked for chosen plaintexts and several attempts can be made to forge a valid ciphertext.

In the INT-CTXT game, the adversary can ask for encryption queries and it wins if it succeeds in querying the decryption query with a ciphertext that was not an output of the encryption oracle that can be successfully decrypted. The advantage of such an adversary is defined as the probability of winning this particular game:

$$ \mathrm{Adv}_{\mathrm{E}}^{\mathrm{int-ctxt}}(\mathcal{A}) := \Pr[\mathrm{INTCTXT}(\mathcal{A}, E).\mathrm{main}() : \exists c, c \in \mathrm{Mem}.lc \wedge \mathrm{dec}_E(\mathrm{Mem}.k, c) \neq \mathrm{None}] $$

Here, Mem.lc is the list that keeps track of all decryption queries and dec_E refers to the decryption algorithm of the scheme E.
<figure><img src="image_115.png" /></figure>

EasyCrypt

In EasyCrypt, an event in a probability formula cannot contain procedures, but it may contain operators and global variables. While procedures are more expressive than operators — they allow random sampling and updates of internal states — EasyCrypt can prove equivalences between operators and stateless deterministic procedures. Since symmetric encryption generally has stateless deterministic procedures, they can be expressed as operators.

type key, plaintext, ciphertext.

op enc : key → plaintext → ciphertext.

op dec : key → ciphertext → plaintext option.

module type StLOcls = {

proc * init () : unit

proc kg () : key

}

module Mem = {

var k : key

var log : (ciphertext, plaintext) fmap

var lc : ciphertext list

}

module type INTCTXT_Oracles = {

proc enc(_: plaintext): ciphertext

proc dec(_: ciphertext): plaintext option

}

module type Adv_INTCTXT

(O : INTCTXT_Oracles) = {

proc main(): bool

}

module INTCTXTOrcls (S : StLOcls)

: INTCTXT_Oracles = {

proc init () = {

S.init();

Mem.log ← empty;

Mem.lc ← [];

Mem.k ← S.kg();

}

proc enc (p : plaintext) = {

var c;

c ← enc Mem.k p;

Mem.log[c] ← p;

return c;

}

proc dec (c : ciphertext) = {

(* note that the operator dec is not used in
the "decryption oracle" *)

Mem.lc ← if c ∈ Mem.log then Mem.lc

else c :: Mem.lc;

return Mem.log[c];

]}.

module INTCTXT

(A : Adv_INTCTXT, StL : StLOcls) = {

module O = INTCTXTOrcls(StL)

proc main () = {

var b;

O.init();

b ← A(O).main();

return b;

]}.

7.3 Relations between IND-CCA, IND-CPA and INT-CTXT

In EasyCrypt, the difference between the games IND-CPA and IND-CCA is the set of
procedures accessible by the adversary. In particular, the decryption oracle is only accessible
in the IND-CCA game.

When in the game IND-CCA the encryption scheme is modified so that the decryption al-
gorithm always answers None unless the query was the output of a previous encryption, then
IND-CCA security is equivalent to IND-CPA security for this scheme. Using this observation,
we define a module that transforms an IND-CCA adversary into an IND-CPA adversary.
EasyCrypt

The formalization uses the global variables from the module Mem. It transforms a module of module type Enc into the module type accepted by an IND-CCA adversary and hides the secret key inside Mem.k.

module Mem (S : Enc) = {
  var k : key
  var log : (ciphertext, plaintext) fmap
  proc init () = { Mem.k ← S.keygen(); }
  proc enc(p: plaintext) = {
    var c;
    c ← S.enc(Mem.k,p);
    return c;
  }
  proc dec(c:ciphertext) = {
    var p;
    p ← S.dec(Mem.k,c);
    return p;
  }}.

Given an IND-CCA adversary A and
an IND-CPA encryption oracle, we built
the IND-CPA adversary by giving to A
a direct access to the encryption oracle,
and by simulating the decryption oracle
using the information contained in the
state of Mem.

module CPA_CCA_Orcls(O:CPA_Oracles)
: CCA_Oracles = {
  proc init () = {
    Mem.log ← empty;
  }
  proc enc(p: plaintext) = {
    var c;
    c ← O.enc(p);
    Mem.log[c] ← p;
    return c;
  }
  proc dec(c:ciphertext) = {
    return Mem.log[c];
  }}.

Finally, the construction of an IND-CCA adversary is named CPA_CCA_Adv.

module CPA_CCA_Adv
(A:CCA_Adv, O:CPA_Oracles) = {
  proc main () = {
    var b;
    CPA_CCA_Orcls(O).init();
    b ← A(CPA_CCA_Orcls(O)).main();
    return b;
  }}.

7.3.1 IND-CCA from IND-CPA and INT-CTXT

The game IND-CPA is equivalent to IND-CCA when the decryption procedure always
answers None. Therefore, when in IND-CCA the adversary asks for a decryption query that
is correctly decrypted (and was not an output from the encryption oracle), this event dis-
tinguishes IND-CPA from IND-CCA. This distinguishing event is exactly what INT-CTXT ac-
counts for. This means that the IND-CCA advantage is bounded by the IND-CPA advantage
plus the INT-CTXT advantage, as first stated in [Bellare and Namprempre, 2000].

**Theorem 7.3.1.** For all IND-CCA adversary *A*, its IND-CCA advantage is bounded by the
IND-CPA advantage of CPA\_CCA\_Adv(*A*) plus the INT-CTXT advantage of *C*(*A*):

$$
\mathrm{Adv}_{\mathrm{E}}^{\mathrm{ind-cca}}(\mathcal{A}) \leq \mathrm{Adv}_{\mathrm{E}}^{\mathrm{ind-cpa}}(\mathrm{CPA\_CCA\_Adv}(\mathcal{A})) + \mathrm{Adv}_{\mathrm{E}}^{\mathrm{int-ctx}}(\mathcal{C}(\mathcal{A}))
$$

when the adversary $\mathcal{C}(\mathcal{A})^0$ is defined as the simulation of the game IND-CCA with $\mathcal{A}$ and $O$, and outputs the result of the game.

*Proof.* The proof is a simple application of a failure event: the forgery of a valid decryption.

<figure><img src="image_116.png" /></figure>
## EasyCrypt

Furthermore, this remains true for more general games than IND-CPA and IND-CCA, that plays two rounds challenge and guess. We name them CCA and CPA, that use the module Mem from Section 7.3. The main difference between those games is the module type of the adversary that differs in the procedures allowed.

module type CCA_Adv (O: CCA_Oracles) = {
    proc main () : bool { O.enc O.dec }
}.
module CCA (A : CCA_Adv, E : Enc) = {
    proc game () : bool = {
        var b;
        Mem(E).init();
        b ← A(Mem(E)).main();
        return b;
    }.
}

module type CPA_Adv (O: CCA_Oracles) = {
    proc main () : bool { O.enc }
}.
module CPA (A : CPA_Adv, E : Enc) = {
    proc game () : bool = {
        var b;
        Mem(E).init();
        b ← A(Mem(E)).main();
        return b;
    }.
}

**Theorem 7.3.2.** For all CCA adversary $\mathcal{A}$, its CCA probability is bounded by the CPA probability of $\text{CPA\_CCA\_Adv}(\mathcal{A})$ plus the INT-CTXT advantage of $\mathcal{A}$.

$$ \Pr[b \leftarrow \text{CCA}(\mathcal{A}, E).\text{game()} : b = 1] \\ \le \Pr[b \leftarrow \text{CPA}(\text{CPA\_CCA\_Adv}(\mathcal{A}), E).\text{game()} : b = 1] + \text{Adv}_{\text{E}}^{\text{int-ctxt}}(\mathcal{A}) $$

*Proof.* The proof is a simple application of a failure event: the forgery of a valid decryption. $\square$

## 7.3.2 Ideal Encryption Scheme

The encryption scheme described in the next chapter in a *nonce-based* AEAD scheme [Rogaway, 2004b]. This means that the user supplies not only a symmetric key k, the message m, and associated data a, but also a *nonce* n. The concept of a nonce is something that takes on a new value with every message one encrypts. This idea was introduced (partly) in order to randomize the encryption of the same message over time.

The module we name *Ideal* is the unrealistic module that captures this idea that every fresh encryption query will output a truly random ciphertext, and every non-encrypted ciphertext will never be authenticated and decrypted. The IND-CPA, IND-CCA and INT-CTXT advantages of this “scheme” are proven to be equal to 0:

$$ \forall \mathcal{A}, \quad \Pr[b \leftarrow \text{IND\_CPA}(\mathcal{A}, \text{Ideal}).\text{game()} : b = 1] = \frac{1}{2} $$

$$ \forall \mathcal{A}, \quad \Pr[b \leftarrow \text{IND\_CCA}(\mathcal{A}, \text{Ideal}).\text{game()} : b = 1] = \frac{1}{2} $$

$$ \forall \mathcal{A}, \quad \text{Adv}_{\text{Ideal}}^{\text{int-ctxt}}(\mathcal{A}) = 0 $$

Therefore, any nonce-based AEAD scheme that is indistinguishable from *Ideal*, is IND-CPA, IND-CCA and INT-CTXT secure, under some nonce-respecting condition expressed in further details in Chapter 8.
<figure><img src="image_117.png" /></figure>

EasyCrypt

In the case of an encryption scheme
that operates on a message space that
can be interpreted as the set of lists of
bytes, the Ideal scheme ressembles to the
following.

The decryption always answers
None, and the encryption outputs a list
of random bytes that has the same over-
all size as the plaintext given as input,
and a random tag.

type key, nonce, associated_data, tag, block, byte.

type ad = associated_data.

type message = byte list.

type bytes = byte list.

type plaintext =
    nonce * associated_data * message.

type ciphertext =
    nonce * associated_data * message * tag.

op bytes_of_block : block → byte list.

op dtag : tag distr.

op dblock : block distr.

module Ideal : Enc = {
    proc key_gen () : key = { return witness; }
    proc cc(n:nonce, p:message) : bytes = {
        var z, c;
        p ← List.map (fun _ ⇒ witness<:byte>) p;
        c ← [];
        while (p ≠ []) {
            z ← dblock;
            c ←
                c ++ take (size p) (bytes_of_block z);
            p ← drop block_size p;
        }
        return c;
    }
    proc enc (k: key, nap : plaintext)
        : ciphertext = {
            var n, a, p, c, t;
            (n,a,p) ← nap;
            c ← cc(n,p);
            t ← $ dtag;
            return (n,a,c,t);
        }
    proc dec (_: key * ciphertext)
        : plaintext option = {
            return None;
        }.
};

<figure><img src="image_118.png" /><figcaption>Figure 7.1 – Representation of the encryption of Ideal.</figcaption></figure>
<figure><img src="image_119.png" /></figure>
# Chapter 8

## ChaCha20-Poly1305's Formal Proof

The Internet Engineering Task Force (IETF) is an open standard organization, which develops and promotes voluntary Internet standards, in particular the standards that comprise the Internet protocol suite (TCP/IP). Due to concern over the reliance of existing IETF protocols on AES and the risk that advances in the cryptanalysis of AES could leave users without a good choice for a symmetric cryptographic primitive, there has been a proposal to the CFRG (Crypto Forum Research Group of the Internet Research Task Force (IRTF)) to consider a combination of ChaCha20 and Poly1305 for inclusion in future IETF protocols [Nir and Langley, 2015].

<figure><img src="image_120.png" /></figure>

### Remark

A similar concern led to the SHA-3 competition; improvements to attacks against SHA-1 [Stevens et al., 2017, Leurent and Peyrin, 2019] lead NIST to transition to the SHA-2 family of hash functions and to announce the SHA-3 competition, with the aim of choosing an alternative hash function to SHA-2, so that it improves the robustness of NIST overall hash algorithm toolkit' [Kayser, 2007].

Furthermore, ChaCha20 [Bernstein, 2008a] and Poly1305 [Bernstein, 2005] have both been designed for high performance in software implementations. They typically admit a compact implementation that uses few resources and inexpensive operations, which makes them suitable on a wide range of architectures. They have also been designed to minimize leakage of information through side-channels. Some attacks [Al Fardan and Paterson, 2013] used the particularities of the CBC-mode cipher suites in TLS, as well as issues with the only supported stream cipher RC4 [Isobe et al., 2013]. While the existing AEAD cipher suites —based on AES-GCM [McGrew and Viega, 2004a], whose security proof was flawed and repaired in [Iwata et al., 2012]— address some of these issues, there are concerns about their performance and ease of software implementation.

Therefore, a new stream cipher to replace RC4 and address all the previous issues has been proposed. The construction named ChaCha20-Poly1305 [Langley et al., 2016] aims to provide a secure stream cipher for TLS [Nir and Langley, 2015] that is comparable to RC4 in speed on a wide range of platforms and can be implemented easily without being vulnerable to software side-channel attacks. Indeed, in [Almeida et al., 2019a], Almeida et al. proposed a fast implementation of ChaCha20-Poly1305 that is resistant to some side-channel attacks. My contribution is to provide an IND-CCA security proof of the AEAD scheme that is functionally equivalent to the one implemented in [Almeida et al., 2019a].
## 8.1 Description of ChaCha20-Poly1305

The confidentiality of the AEAD scheme is provided by ChaCha20 [Bernstein, 2008a], a stream cipher based on the Salsa family [Bernstein, 2008b]. The encryption ressembles the counter mode of operation for which the block cipher is replaced by a PRF with signature $CC : \{0, 1\}^{256} \times \{0, 1\}^{128} \rightarrow \{0, 1\}^{512}$, i.e. 32-byte key, 16-byte input, and 64-byte output.

As opposed to a MAC scheme, the data integrity is provided by a one-time authenticator named Poly1305, meaning that keys should only be used once. Poly1305 is a universal hash function based on polynomial evaluation [Carter and Wegman, 1977, Bernstein, 2005].

<figure><img src="image_121.png" /><figcaption>Figure 8.1 – Representation of the encryption algorithm of ChaCha20-Poly1305.</figcaption></figure>

As represented in Figure 8.1, the counter mode for ChaCha20 is used with the initial counter 1, instead of the usual counter 0 which is used for the single use authentication key for Poly1305. The polynomial to be evaluated for Poly1305 is an interpretation of the composition of the associated data and ciphertext as a sequence of polynomial coefficients: integers modulo $2^{130} - 5$. This polynomial is evaluated in $\mathbb{F}_{2^{130}-5}$ at the key $r \in \{0, 1\}^{128}$: the first 128-bits of the ChaCha20 block derivation with the counter 0. The final tag of the AEAD scheme is the addition modulo $2^{128}$ of the polynomial evaluation's output plus the next 128-bits of the same ChaCha20 block derivation with the counter 0. The decryption algorithm is analogous to the encryption, with a check on the validity of the tag.

<figure><img src="image_122.png" /></figure>

### EasyCrypt

In the following, CC refers to the function described in the standard ChaCha20 that given a ChaCha20 key ($\{0, 1\}^{256}$), a nonce ($\{0, 1\}^{96}$) and a counter ($\{0, 1\}^{32}$) outputs a block ($\{0, 1\}^{512}$). The computation of c from m, the nonce N and the ChaCha20 key is called ChaCha (parametrized by the underlying CC function), whereas the authenticated encryption scheme — also parametrized by the CC function — is called CCPoly.
The formalization of the formal security proof of ChaCha20-Poly1305 is based on a general finite type named byte that represents what is commonly called with the same name.

We give here a simplified version, since the objective is not to argue that this is a strong formalization, but to explain as clearly as possible our formal security proof.

type key, nonce, byte, tag, associated_data, block, polynomial, poly_key.

type message = byte list.

type plaintext =
    nonce * associated data * message.

type ciphertext =
    nonce * associated data * message * tag.

op dkey : key distr.

op dtag : tag distr.

op dpoly_key : poly_key distr.

op bytes_of_block : block → byte list.

op extend : message → block.

op (+^) : block → block → block.

op block_size : int.

op parse_block : block → poly_key * tag.

op topol : associated_data → message → polynomial.

op eval_pol : poly_key → polynomial → tag.

op (+) : tag → tag → tag.

theory C.

type counter.

op ofint : int → counter.

end C.

module type CC = {
    proc cc (k:key, n:nonce, c: C.corner) : block
}.

module type FCC = {

proc * init () : unit

include CC

}

module ChaCha(CC:CC) = {
    proc enc(k:key, n:nonce, p:message)
        : message = {
            var z, c, l;
            c ← [];
            while (p ≠ []) {
                z ← CC.cc(k, n, C.ofint i);
                l ← bytes_of_block (extend p +^ z);
                c ← c ++ take (size p) l;
                p ← drop block_size p;
            }
            return c;
        }
    }.
}

module CCPoly (CC : CC) : Encryption = {
    proc keygen () : key = {
        var k;
        k ← dkey;
        return k;
    }
    proc enc (k : key, nap : plaintext) = {
        var n, a, p, c, b, r, s, t;
        (n,a,p) ← nap;
        c ← ChaCha(CC).enc(k,n,p);
        b ← CC.cc(k,n,C.ofint 0);
        (r,s) ← parse_block b;
        t ← (eval_pol y r (topol a c)) + s;
        return (n,a,c,t);
    }
    proc dec (k : key, nact : ciphertext) = {
        var n, a, c, t, b, r, s, p, ret;
        (n,a,c,t) ← nact;
        b ← CC.cc(k,n,C.ofint 0);
        (r,s) ← parse_block b;
        if (t = (eval_pol y r (topol a c)) + s) {
            p ← ChaCha(CC).enc(k,n,c);
            ret ← Some p;
        } else { ret ← None; }
        return ret;
    }
}.

The formal proof may be found (as of December 15, 2020) in the branch deploy-chachapoly in the GitHub repository at https://github.com/EasyCrypt/easycrypt.git.

## 8.2 Security of ChaCha20-Poly1305

This work extends the work of [Almeida et al., 2019a] in which Almeida et al. present an optimized implementation of ChaCha20 and Poly1305. Their work uses EasyCrypt to prove in particular the functional correctness of their implementation according to the reference.

ChaCha20-Poly1305 is a slightly modified version of Encrypt-then-MAC with the schemes ChaCha20 and Poly1305. In [Bellare and Namprempre, 2000], the security proof of Encrypt-then-MAC assumes the keys of the cipher and MAC scheme to be sampled independently.
In Chacha20&Poly1305, since the key of Poly1305 is derived from ChaCha20, Bellare and Namprempre's proof cannot be applied in this setting.

In [Procter, 2014], Procter proposes a simple security reduction for ChaCha20-Poly1305 in the nonce-respecting adversarial model. In the effort to formalize their proof, we noticed that some reasoning flaws and corrected them in our proof. We first present the nonce-respecting adversarial model, then we state our verified security bound and present our formal security proof.

## 8.2.1 Adversarial Model

The security proof of ChaCha20-Poly1305 is placed in the *nonce-respecting* adversarial model. This means that the adversary respects the uniqueness of nonces in its encryption queries. Moreover, there is *no restriction* on nonces asked with decryption queries.

Along with the formalization in EasyCrypt of a nonce-respecting adversary, we include bounds in the number of oracle queries it can make: at most $q_e$ encryption queries and at most $q_d$ decryption queries.

<figure><img src="image_123.png" /></figure>

### EasyCrypt

We formalize this adversarial model by restricting oracle access using a module named BNR (Bounded Nonce-Respecting) which provide an interface that restricts oracle calls from the adversary. A bounded nonce-respecting adversary is formalized using the module BNR_Adv.

```python
op check plaintext (lenc:nonce list) (p: plaintext) =
    let (n, a, m) = p in n \ n \ lenc \ valid_topol a m \ size lenc < qenc.
```

```python
op check_cipher (ndec:int) (c:ciphertext) =
    let (n, a, m, t) = c in valid_topol a m \ ndec < qdec.
```

The variable BNR.lenc is the list of all nonces already queried by the adversary and it encodes both nonce respecting and the number of encryption queries. The variable BNR.ndec encodes the number of decryption queries.

```python
module BNR (O:CCA_Oracles) = {
    var lenc : nonce list
    var ndec : int
    proc init () = { lenc ← []; ndec ← 0; }
    proc enc (p: plaintext) = {
        var c ← witness;
        if (check plaintext lenc p) {
            c ← O.enc(p);
            lenc ← p.'1 :: lenc;
        }
        return c;
    }
}
```

```python
proc dec (c:ciphertext) = {
    var p ← None;
    if (check_cipher ndec c) {
        p ← O.dec(c);
        ndec ← ndec + 1;
    }
    return p;
}}
```

```python
module BNR_Adv(A:CCA_Adv,
               O:CCA_Oracles) = {
    proc main() = {
        var b;
        BNR(O).init();
        b ← A(BNR(O)).main();
        return b;
    }}.
```
## 8.2.2 Security Statement

The AEAD scheme named ChaCha20-Poly1305 is secure under the assumption that the ChaCha20 function is indistinguishable from a random function when the ChaCha20 key is randomly sampled and kept secret. A few papers have attacked reduced round versions for ChaCha20 (e.g. [Aumasson et al., 2008, Ishiguro, 2012, Shi et al., 2012]). This analysis has not contradicted the security assumption about the PRF security of the full round version for ChaCha20.

**Theorem 8.2.1.** For any nonce-respecting adversary $\mathcal{A}$ making at most $q_d$ decryption queries and at most $q_e$ encryption queries, its advantage in CCA to distinguish ChaCha20-Poly1305 from Ideal is bounded by a small probability plus the distinguishing advantage of $\mathcal{B}(\mathcal{A})$ between CC and a random function $\mathcal{S}$, where the algorithm $\mathcal{B}(\mathcal{A})^0$ runs once $\mathcal{A}^{\text{CCPoly}(\mathcal{O})}$ and outputs the same result.

$$ \text{Adv}_{\text{CCPoly(CC),Ideal}}^{\text{dist}}(\mathcal{A}) \le q_d \cdot \max(p_0, p_1) + q_d \cdot p_1 + \text{Adv}_{\text{CC},\mathcal{S}}^{\text{dist}}(\mathcal{B}(\mathcal{A})) $$

Let $L$ be the maximum byte length of messages, when we instantiate all the specifications of the standard ChaCha20-Poly1305: $p_0 = 2^{-128}$ and $p_1 = \frac{8[L/16]}{2^{106}}$.

## 8.3 Security Proof

### First Step - Security Assumption - ChaCha20 is a PRF

The first step of the security proof is to transform ChaCha20-Poly1305 into the same construction built upon a random function instead of CC. This transformation introduces a particular instance of an adversary playing the game to distinguish CC (when the key is sampled randomly) from a truly random function PRF. Therefore, the security of the scheme ChaCha20-Poly1305 relies on the indistinguishability of CC from a random function.

$$ \begin{aligned} \text{Adv}_{\text{CCPoly(CC),Ideal}}^{\text{dist}}(\mathcal{A}) &\le \text{Adv}_{\text{CCPoly(CC),CCPoly(PRF)}}^{\text{dist}}(\mathcal{A}) + \text{Adv}_{\text{CCPoly(PRF),Ideal}}^{\text{dist}}(\mathcal{A}) \\ &= \text{Adv}_{\text{CC,PRF}}^{\text{dist}}(\mathcal{B}(\mathcal{A})) + \text{Adv}_{\text{CCPoly(PRF),Ideal}}^{\text{dist}}(\mathcal{A}) \end{aligned} $$

Here $\mathcal{B}(\mathcal{A})^0$ is defined as the algorithm that, given $O$, returns the output of $\mathcal{A}^{\text{CCPoly}(\mathcal{O})}$.

### Second Step - IND-CCA from IND-CPA and INT-CTXT

The second step is the application of the general lemma 7.3.2 that states that any probability of a CCA game can be bound by the probability of a CPA game plus the INT-CTXT advantage with the same AE scheme.

$$ \begin{aligned} \text{Adv}_{\text{CCPoly(PRF),Ideal}}^{\text{dist}}(\mathcal{A}) &= |\text{Pr}[b \leftarrow \text{CCA}(\mathcal{A}, \text{CCPoly(PRF)}) : b] - \text{Pr}[b \leftarrow \text{CCA}(\mathcal{A}, \text{Ideal}) : b]| \\ &\le |\text{Pr}[b \leftarrow \text{CPA}(\text{CPA\_CCA\_Adv}(\mathcal{A}), \text{CCPoly(PRF)}) : b] \\ &\quad - \text{Pr}[b \leftarrow \text{CCA}(\mathcal{A}, \text{Ideal}) : b]| + \text{Adv}_{\text{CCPoly(PRF)}}^{\text{int-ctxt}}(\mathcal{A}) \end{aligned} $$

The third step modifies the calls to PRF in CCPoly(PRF), in both the games CPA and INT-CTXT. In CPA, the final goal is to prove that CCPoly(PRF) is equivalent to Ideal under the assumption that the adversary is bounded and nonce-respecting. For INT-CTXT, those manipulations are aimed at bounding the event.
### Third Step - Modifications of PRF

In CPA and INT-CTXT, all decryption queries output None, whether the tag is valid or not. Therefore, all calls to PRF in the decryption oracle can be delayed in both games without changing the behavior of the adversary. This first modification is done using the lazy-eager library described in Section 2.3.2, and has different implications for CPA and INT-CTXT:

- In CPA, calls can be erased, since they do not affect the event of the probability we are interested in.

- In INT-CTXT, the event of the probability we are interested in is affected by those calls. This modification also delays the update of the event to *after* the end of the interactions with the adversary. This operation is achieved by archiving all decryption queries in a list when interacting with the adversary, and then afterwards, iterating on each decryption query to test if the event is triggered for this particular query.

<figure><img src="image_124.png" /></figure>

## EasyCrypt

The loop after the interactions with the adversary iterates on each unique nonce that was asked in a decryption query. This is motivated by the fact that one random sampling is involved for all decryption queries that share the same nonce: the first is random, whereas the others are fixed values. When several decryption queries share the same nonce, we choose to group them into only one iteration.

op getlingen (x : α * β * γ * 'd) = x.'1.

op same nonce (a : α) (x : α * β * γ * 'd) : bool = x.'1 = a.

op compute_s (r : poly_key) (c:ciphertext) = c.'4 - poly_eval r (topol c.'2 c.'3).

local module G1 (A : CCA_Adv) = {
    var forged : bool
    proc distinguish () = {
        var b, ns, i, n, bl, r, s;
        forged ← false;
        b ← CPA(CPA_CCA_Adv(BNR_Adv(A)),CCPoly(PRF)).main();
        if (size Mem.lc ≤ qdec) {
            ns ← undup (List.map get nonce Mem.lc);
            i ← 0;
            while (i < size ns) {
                n ← nth witness ns i;
                bl ← PRF.get(n,C.ofint 0);
                (r,s) ← parse_block bl;
                forged ← forged || s ∈ List.map (compute_s r) (List.filter (same nonce n) Mem.lc)
                i ← i + 1;
            }
            return b;
        }}.
    };

We have:

$$ \mathrm{Adv}_{\mathrm{CCPoly}(\mathrm{PRF})}^{\mathrm{int-ctx}}(\mathcal{A}) = \Pr[b \leftarrow \mathrm{G1}(\mathcal{A}).\mathrm{distinguish}(): \mathrm{G1}.\mathrm{forged}] $$

and

$$ \Pr[b \leftarrow \mathrm{CPA}(\mathrm{CPA\_CCA\_Adv}(\mathcal{A}), \mathrm{CCPoly}(\mathrm{PRF})) : b] = \Pr[b \leftarrow \mathrm{G1}(\mathcal{A}).\mathrm{distinguish}() : b] $$
The second modification of PRF separates its domain into the encryption domain and the authentication domain using the library SplitDom described in Section 2.3.3. The random oracle PRF is split into two random oracles : $PRF_1$ and $PRF_2$, as shown in Figure 8.2.

<figure><img src="image_125.png" /><figcaption>Figure 8.2 – Split Dom of PRF</figcaption></figure>

The third modification of PRF transforms the co-domain of $PRF_1$ into three parts : the r part, the s part, and the non-used part. We use the library SplitCodom (twice) described in Section 2.3.3, as shown in Figure 8.3 :

1. split the co-domain into the useful part $PRF_u$ and the useless part $PRF_\emptyset$,

2. split the useful $PRF_u$ into $PRF_r$ and $PRF_s$.

<figure><img src="image_126.png" /><figcaption>Figure 8.3 – Split Codom of $PRF_1$</figcaption></figure>

The last PRF modification erases all calls to $PRF_\emptyset$, since its outputs are never used or shown to the adversary.
EasyCrypt

```python
local module G2 (A : CCA_Adv) = {
    module O = {
        proc keygen = CCPoly(PRF2).keygen
        proc enc (k : key, nap : plaintext) = {
            var n, a, p, c, t, r, s;
            c ← ChaCha(PRF2).enc(k,n,p);
            r ← PRFr.get(n,C.ofint 0);
            s ← PRFs.get(n,C.ofint 0);
            t ← (poly_eval r (topol a c)) + s;
            return (n,a,c,t);
        }
        proc dec (k : key, nact : ciphertext) = { return None; }
    }
    proc distinguish () = {
        var b, ns, i, n, r, s;
        G1.forged ← false;
        PRFs.init(); PRFr.init(); PRF2.init();
        b ← CCA(BNR_Adv(A),O).main();
        if (size Mem.lc ≤ qdec) {
            ns ← undup (List.map get_nonce Mem.lc);
            i ← 0;
            while (i < size ns) {
                n ← nth witness ns i;
                r ← PRFr.get(n,C.ofint 0);
                s ← PRFs.get(n,C.ofint 0);
                G1.forged ← G1.forged || s ∈ List.map (compute_s r) (List.filter (same_nonce n) Mem.lc)
                i ← i + 1;
            }
            return b;
        }}
    }.
```

We have:

$$ \mathrm{Adv}_{\mathrm{CCPoly}(\mathrm{PRF})}^{\mathrm{int-ctx}}(\mathcal{A}) = \mathrm{Pr}[b \leftarrow \mathrm{G2}(\mathcal{A}).\mathrm{distinguish}(): \mathrm{G1}.\mathrm{forged}] $$

and

$$ \mathrm{Pr}[b \leftarrow \mathrm{CPA}(\mathrm{CPA\_CCA\_Adv}(\mathcal{A}), \mathrm{CCPoly}(\mathrm{PRF})) : b] = \mathrm{Pr}[b \leftarrow \mathrm{G2}(\mathcal{A}).\mathrm{distinguish}() : b] $$

Fourth Step - Application of the BNR restriction in CPA

A nonce-respecting adversary may only ask fresh nonces for its encryption queries. Therefore, in G2 with a BNR adversary, inputs to PRFs, PRF2 are fresh in the encryption oracle, and calls to those random functions may be replaced by direct random samplings (when we are only interested in the return value of the adversary, not in the value of G1.forged).

When the encryption oracle is queried in G2, say with input (n, a, p) (the secret key being hidden to the adversary), each portion of c is computed by xoring the corresponding portion of p with a uniform random value. Using the bijectivity of the xor operation (⊕), the value of each portion of c may be directly sampled from the uniform distribution.

Furthermore, the output tag t is computed from the values of r and s which are now uniform random samplings. Since the function $a + \cdot$ is bijective (for all values of a) and
the intermediate value s is not revealed to the adversary, the output tag t can be directly sampled and output to the adversary, without using r.

Both modifications of the computation of the output of the encryption oracle prove that under the BNR restrictions, both the encryption oracle and decryption oracle of the game G2 have the same distribution as Ideal in CCA, as represented in Figure 8.4:

$$ \begin{aligned} \Pr[b \leftarrow \text{CPA}(\text{CPA\_CCA\_Adv}(\mathcal{A}), \text{CCPoly}(\text{PRF})) : b] &= \Pr[b \leftarrow \text{G2}(\mathcal{A}).\text{distinguish}() : b] \\ &= \Pr[b \leftarrow \text{CCA}(\mathcal{A}, \text{Ideal}) : b] \end{aligned} $$

<figure><img src="image_127.png" /><figcaption>Figure 8.4 – Forth step</figcaption></figure>

We can conclude from this transition that:

$$ \text{Adv}_{\text{CCPoly(CC),Ideal}}^{\text{dist}}(\mathcal{A}) \le \text{Adv}_{\text{CC,PRF}}^{\text{dist}}(\mathcal{B}(\mathcal{A})) + \Pr[b \leftarrow \text{G2}(\mathcal{A}).\text{distinguish}() : \text{G1.forged}] $$

This transition changes the polynomial used in the computation of the event G1.forged. Therefore, the application of the BNR restriction cannot replace calls to the random functions by direct random samplings to formally bound the event G1.forged.

### Fifth step - Modify G2 to bound G1.forged using the BNR restrictions

To bound the event G1.forged, we need to be more careful about how we use the bijections and the BNR restrictions. We do not care about calls to PRF<sub>2</sub>, since they do not appear in the computation of G1.forged, so they may be replaced by direct random samplings. However, the calls to PRF<sub>r</sub>, PRFs cannot be replaced by direct random samplings since their is no restriction on the nonces asked to the decryption, we cannot ensure that the occurrences that happen in the loop have fresh inputs or that they remain consistent with oracle outputs.
<figure><img src="image_128.png" /></figure>

**Remark**

The event of finding a polynomial root can be easily bounded when the point of evaluation is sampled uniformly at random. But, when a decryption query is asked with a nonce already used in a previous query, the key r of the polynomial is already set and is not random anymore. Therefore, the probability of the forgery event for this decryption query can only be bounded by 1 (very far from being negligible).

Generally, this absence of randomness that comes from the BNR adversarial model (nonce-repeating in decryption queries) is often forgotten, as in [Procter, 2014]. Our formal analysis has shown this reasoning flaw in their security proof, but this does not lead to any security issue. Indeed, the technique we use (that is presented in the following) allows us to bound the INT-CTXT advantage with a similar bound.

We still want to modify G2 into a game G3 in which all the calls to PRFs, PRFr in G2 are replaced by random samplings. We need to specify the event(s) in G3 that fully capture the event G1.forged in G2. We end up with a disjonction of three events that capture more than the event G1.forged in G2, but since we want an upper bound, this is still relevant.

The first event that we split is for the case when the nonce iterated on (after the inter-action with the adversary) has not been asked to the encryption oracle. We call G3.e2 the event that is the conjonction of this case with the event G1.forged.

Left with all the nonces that were asked at some point to the encryption oracle, the event needs further treatment to be bounded. We want to delay all the calls to PRFr in the encryption oracle, so that all the calls in the loop have fresh inputs, and then use the probability of *sampling* a root of a non-zero polynomial. In order to ensure that all polynomials we test in G1.forged are non-zero, we ensure that all outputs (n, a, c, t) of the encryption oracle have never been asked to the decryption oracle by introducing a failure event named G3.e1. The rest of the event G1.forged that is not covered by G3.e1 or G3.e2 is called G3.e3.

<figure><img src="image_129.png" /></figure>

**EasyCrypt**

The event G3.e1 is defined as the event in which the tag t computed in an encryption query in the game G3 is equal to one of the previous inputs for decryption contained in Mem.lc that share the same nonce.

local module G2 (A : CCA_Adv) = {

module O = { (* ... keygen ... *)

proc enc (k : key, nap : plaintext) = {
(* ... *)
r ← PRFr.get(n, C.ofint 0);
s ← PRFs.get(n, C.ofint 0);
t ← (poly_eval r (topol a c)) + s;

return (n,a,c,t);
}
proc dec (* ... *)
}

local module G3 (A : CCA_Adv) = {

var e1 : bool
var e2 : bool
var e3 : bool
var log : (nonce,
associated_data * message * tag) fmap

module O = { (* ... keygen ... *)

proc enc (k : key, nap : plaintext) = {
(* ... *)
t $← dtag;
e1 ← e1 || t ∈ map get_tag
(List.filter (same_nonce n) Mem.lc);
log[n] ← (a,c,t);
return (n,a,c,t);
}
proc dec (* same as G2 *)
}
```pascal
proc distinguish () = {
  var b, ns, i, n, r, s;
  G1.forged ← false;
  PRFs.init(); PRFr.init(); PRF2.init();
  b ← CCA(BNR_Adv(A),O).main();
  if (size Mem.lc ≤ qdec) {
    ns ← undup (List.map get在校非 Mem.lc);
    i ← 0;
    while (i < size ns) {
      n ← nth witness ns i;
      r ← PRFr.get(n,C.ofint 0);
      s ← PRFs.get(n,C.ofint 0);
      G1.forged ← G1.forged ||
        s ∈ List.map (compute_s r)
        (List.filter (same在校非 n) Mem.lc)
        i ← i + 1;
    }
  }
return b;
}}. (* end G2 *)
```

```pascal
proc distinguish () = {
  var b, ns, i, n, r, s;
  e1 ← false; e2 ← false; e3 ← false;
  log ← empty; PRF2.init();
  b ← CCA(BNR_Adv(A),O).main();
  if (size Mem.lc ≤ qdec) {
    ns ← undup (List.map get在校非 Mem.lc);
    i ← 0;
    while (i < size ns) {
      n ← nth witness ns i;
      if (n ∈ BNR.lenc) {
        r ← $d\text{poly\_key};
        e3 ← e3 ||
          test\_poly\_key n Mem.lc r (oget log[n])
      } else {
        r ← $d\text{poly\_key};
        s ← $d\text{tag};
        e2 ← e2 || s ∈ map (compute_s r)
        (List.filter (same在校非 n) Mem.lc);
      }
      i ← i + 1;
    }
  }
return b;
}}. (* end G3 *)
```

```pascal
op valid\_topol\_cipher (c : ciphertext) = valid\_topol c.`2 c.`3.
```

```pascal
op test\_poly\_key (n : nonce) (lc : ciphertext list) (r : poly\_key)
  (amt: associated\_data * message * tag) =
  let (a,m,t) = amt in
  let p = topol a m in
  let pts =
    List.map (fun (c : ciphertext) ⇒ (topol c.`2 c.`3, c.`4))
      (List.filter (same在校非 n) (List.filter valid\_topol\_cipher lc)) in
  valid\_topol a m ∧
  List.has (fun (pt : polynomial * tag) ⇒
    pt.`1 ≠ p ∧ pt.`2 = t + (poly\_eval r pt.`1 − poly\_eval r p)) pts.
```

We have:

$$
\begin{align*}
\text{Adv}_{\text{CCPoly(PRF)}}^{\text{int-ctxt}}(\mathcal{A}) &= \text{Pr}[b \leftarrow \text{G2}(\mathcal{A})\text{.distinguish() : G1.forged}] \\
&\le \text{Pr}[b \leftarrow \text{G3}(\mathcal{A})\text{.distinguish() : G3.e1}] + \\
&\quad \text{Pr}[b \leftarrow \text{G3}(\mathcal{A})\text{.distinguish() : G3.e2} \lor \text{G3.e3}]
\end{align*}
$$

<figure><img src="image_130.png" /></figure>

## Remark

Let us recall that all values that are added into the list of decryption queries Mem.lc are checked for not having been answered by the encryption oracle up to this point. Therefore, the only remaining possibility to trigger G3.e1 is that the encryption query is asked after the decryption queries. We use the randomness in the encryption oracle to bound G3.e1 in G3.
<figure><img src="image_131.png" /></figure>

**Remark**

The event G3.e1 is larger than only ensuring that the tested polynomial in G1.forged is non-zero. In our formal analysis, we obtain a smaller bound for G3.e1 than for the disjonction G3.e2 ∨ G3.e3. This is sufficient to conclude of the security of the scheme, but someone interested in making the bound more accurate may use the randomness of the parts of c. This would introduce the use of some restriction encryption calls, whether it is $q_e$ or a maximum communication complexity on encryption queries.

At first, we have bounded those events in a very loose way that have yielded in a quadratic bound in the number of oracle calls. The short argument is the following. Since the size of the list Mem.lc is bounded by $q_d$, and there are at most $q_e$ calls to trigger G3.e1, and $q_d$ calls to trigger either G3.e2 or G3.e3, we can bound the probability of these event by:

$$ \text{Pr[b} \leftarrow \text{G3}(\mathcal{A}).distinguish() : \text{G3.e1}] \le q_e q_d \cdot p_1, $$

$$ \text{Pr[b} \leftarrow \text{G3}(\mathcal{A}).distinguish() : \text{G3.e2}] \le q_d^2 \cdot p_1, \text{ and} $$

$$ \text{Pr[b} \leftarrow \text{G3}(\mathcal{A}).distinguish() : \text{G3.e3}] \le q_d^2 \cdot p_0. $$

<figure><img src="image_132.png" /></figure>

**Remark**

We noticed that each event does not use the full list Mem.lc, but only the part filtered by the nonce value. Furthermore, a nonce used to trigger each event may not be used to trigger the same event a second time. Therefore, for each event, each nonce may only trigger once each event, reducing the quadratic bound to a linear one. The following explains our argument a little further.

We choose to bound the events G3.e2 and G3.e3 together. They are located in the loop that iterates on each unique nonce that appears in Mem.lc, which have a fixed value after the interaction with the adversary that we name lc. The formula to obtain n from lc and the iteration counter i is $n := \text{nth witness ulc i}$, where ulc := $\text{List.undup}(\text{List.map get_nonce lc})$. The probability of each iteration to trigger either G3.e2 or G3.e3 is bounded by

$$ \text{size}(\text{List.filter(same_nonce n) lc}) \cdot \max(p_0, p_1) $$

where n is the unique nonce iterated on. We use the fel tactic<fnref n="1" /> to bound the event G3.e2 ∨ G3.e3 by:

$$ \text{Pr[b} \leftarrow \text{G3}(\mathcal{A}).distinguish() : \text{G3.e2} \lor \text{G3.e3}] $$

$$ \le \sum_{i=0}^{\text{size ulc}-1} \text{size}(\text{List.filter(same_nonce n) lc}) \cdot \max(p_0, p_1) $$

$$ \le \max(p_0, p_1) \cdot \sum_{i=0}^{\text{size ulc}-1} \text{size}(\text{List.filter(same_nonce n) lc}) $$

We prove that $\text{size lc} = \sum_{i=0}^{\text{size ulc}-1} \text{size}(\text{List.filter(same_nonce n) lc})$. Then, using the bound $\text{size lc} \le q_d$, we can bound the full event G3.e2 ∨ G3.e3 in G3 by:

$$ \text{Pr[b} \leftarrow \text{G3}(\mathcal{A}).distinguish() : \text{G3.e2} \lor \text{G3.e3}] \le q_d \cdot \max(p_0, p_1) $$

<footnote n="1">1. Refer to the manual of EasyCrypt for more details.</footnote>
## Sixth step - Bound G3.el in G3

We would use the same technique to bound G3.el, but the list that appears in the expression of the bound to trigger G3.el is not constant. Indeed, the list Mem.lc has no fixed value during the interaction with the adversary, preventing us to use the tactic fel in this context. Therefore, we use another technique that splits the event G3.el into $q_d$ parts. The definition of these parts comes with the game G4.

<figure><img src="image_133.png" /></figure>

### EasyCrypt

In the game G4, we build the list composed of all the couples of tags that are tested to trigger G3.el. This list is named G4.lt and the way it is constructed enforces the following invariants. For each element $(t, t')$ of G4.lt:

- it is associated to a nonce $n$,

- a decryption query has been recorded in Mem.lc that contains both $n$ and $t'$, and,

- at the end of the encryption, $t$ is the tag associated to $n$ in G3.log.

```python
local module G4 (A : CCA_Adv) = {
    var lt : (tag * tag) list
    module O = { (* ... keygen ... *)
        proc enc (k : key, nap : plaintext) = {
            (* ... *)
            t $←$ dtag;
            lt $←$ List.map (fun c ⇒ (t, get_tag c))
                (List.filter (same_nonce n) Mem.lc)
            return (n,a,c,t);
        }
        proc dec (* same as G3 *)
        {
            proc distinguish () = {
                var b, ns, i, n, r, s;
                lt $←$ [];
                PRF2.init();
                b $←$ CCA(BNR_Adv(A),O).main();
                (* the loop is not relevant for G3.el *)
                return b;
            }.
        }
    }
}
```

We prove in EasyCrypt that:

$$ \Pr[b \leftarrow G3(\mathcal{A}).distinguish() : G3.e1] \\ \le \Pr[b \leftarrow G4(\mathcal{A}).distinguish() : \exists (t, t') \in G4.lt, t = t'] $$

Using the invariants of G4, we prove that the size of G4.lt is bounded by $q_d$. Therefore, we can partition the event $\exists (t, t') \in G4.lt, t = t'$ into $q_d$ parts, where each part is indexed by $0 \le i < q_d$ and says that this event is triggered at the position $i$ of the list. The library EventPartitioning allows us to use apply this partitioning and obtain the following result:

$$ \Pr[b \leftarrow G4(\mathcal{A}).distinguish() : \exists (t, t') \in G4.lt, t = t'] \\ \le \sum_{i=0}^{q_d-1} \Pr[b \leftarrow G4(\mathcal{A}).distinguish() : (\text{nth witness G4.lt } i).'1 = (\text{nth witness G4.lt } i).'2] $$

We have defined another game that only triggers the bad event for the $i$-th position in the list. Then we have proven the equivalence of this game and G4 when in relation to this
event. Then we proved that for all indexes, the probability in this new game to set bad is bounded by $p_1$:

$$ \forall i, \Pr[b \leftarrow G4(\mathcal{A}).distinguish() : (\text{nth witness } G4.\text{lt } i).'1 = (\text{nth witness } G4.\text{lt } i).'2] \le p_1 $$

Finally, we have:

$$ \Pr[b \leftarrow G4(\mathcal{A}).distinguish() : \exists(t, t') \in G4.\text{lt}, t = t'] \le \sum_{i=0}^{q_d-1} p_1 \le q_d \cdot p_1 $$

which concludes the security proof of ChaCha20-Poly1305.
# Conclusion

In this thesis, we formalize and prove concrete security bounds for several cryptographic constructions: a standard MAC scheme named CMAC [Baritel-Ruet et al., 2018], a standard hash function named SHA-3 [Almeida et al., 2019b], and a standard nonce-based AEAD scheme named ChaCha20-Poly1305.

For the last two standards, the formal security proof is accompanied by an implementation [Almeida et al., 2019a, Almeida et al., 2019b] in Jasmin [Almeida et al., 2017] that includes formal functional correctness, an optimized implementation, and protection against some side-channel attacks. Even though I did not participate in the Jasmin developments, this collaboration proposes an approach that not only delivers an optimized version of the standard that is functionally secure and side-channel resistant but also links the functional correctness with the formal security proof.

In a related work [Protzenko et al., 2019], Protzenko et al. expose EverCrypt and fast implementation of a library of cryptographic primitives in C and/or assembly code that includes functional correctness and side-channel resistance. It is based on F* [Swamy et al., 2016] and HACL* [Zinzindohoué et al., 2017] and represents an extensive work. It is an important step in the direction of high-assurance high-speed cryptography, but the link with formal security proofs is still missing. The combination of EasyCrypt and Jasmin is (for now) the only one that provides end-to-end security to implement cryptographic schemes.

# Standardization

The final product of the work in this thesis has many advantages for cryptography and the process of standardization, but its development has some downsides to consider when such a formalization effort is considered. Computer security is generally about evaluating the risks versus the cost to deploy a security solution. I do not argue that every user should use only formally proven cryptographic constructions. My argument is that, in a standardization process, which aims at providing the best cryptosystems in terms of security and/or efficiency, organizers should consider including a phase in which formal security proofs are required so that no more cases like OCB2 [Inoue et al., 2019] happen in the future.

To emphasize this argument a little further, in each security proof that we formalized from an existing pen-and-paper proof, we spotted a few fallacies in the reasoning. They do not question the overall security of the constructions, since for each, we found another formal argument to make the security bound hold. However, no construction is free from such a fallacy to effectively harm its security, unless they are formally verified.

Indeed, once a formal security proof is provided, all reasoning steps have been carefully
described and related to simple axioms and local security assumptions. There is no leap of
faith to convince of the correctness of a formal security proof, except for the correctness of
the proof assistant itself. In my point of view, the level of detail and the verification provided
by the tool both increase the trustworthiness of security proof that are formalized.

Furthermore, the verification provided by the proof assistant allows the costs of verifying each reasoning to be offloaded. This cognitive discharge allows scientific reviewers to redirect their attention from checking the accuracy of evidence to the definitions of security, from adversarial models and security assumptions. Since cognitive effort is limited, this improves the quality of criticism, which in turn improves the quality of the peer-review process. In the long term, security proofs will hopefully be more critical, more accurate and more practical for real-world applications.

The high value of formal proofs of security must be mitigated because the cost of the formalization effort is also high. The time and work needed to formalize and prove the security of a cryptographic construction are much more expensive than for its pen-and-paper equivalent, even for an expert. The EasyCrypt user needs to know how to communicate to the proof assistant the properties he needs to prove and how he is going to do it. Such work requires the understanding and mastery of both cryptography and formal proofs, two different high-level fields in each of which a research career is commonplace. The lack of such experts in both fields is one of the challenges of producing libraries composed exclusively of formally secure cryptographic implementations.

## Perspectives

EasyCrypt is very expressive in terms of the results it can prove. It should be possible to extend the domain of applications of EasyCrypt, e.g. post-quantum cryptography, and to model stronger security properties, e.g. other side-channel resistances. Its application domain is not restricted to cryptography or computer security and may include the study of more general randomized algorithms, provided that the cost of formalization is worth the effort. Indeed, formalization effort remains an issue and future work may also include the reduction of its cost, e.g. by including more automation in EasyCrypt.

For the implementation of cryptographic standards, the link between formal security proofs and secure fast implementation that includes formal functional security and resistance against side-channel attacks should be encouraged and reinforced. A first approach has been implemented using EasyCrypt and Jasmin, and future work may extend each framework, their link, or may introduce alternatives.
List of Figures

<table>
  <tbody>
    <tr>
      <td>1</td>
      <td>Cryptography: a field composed of various security goals and techniques</td>
      <td>2</td>
    </tr>
    <tr>
      <td>2.1</td>
      <td>Eager-lazy random sampling example.</td>
      <td>32</td>
    </tr>
    <tr>
      <td>2.2</td>
      <td>The eager and lazy programmable random oracle</td>
      <td>33</td>
    </tr>
    <tr>
      <td>2.3</td>
      <td>Split domain</td>
      <td>34</td>
    </tr>
    <tr>
      <td>2.4</td>
      <td>Split co-domain</td>
      <td>36</td>
    </tr>
    <tr>
      <td>3.1</td>
      <td>ECB reveals patterns, even when using a secure block cipher.</td>
      <td>46</td>
    </tr>
    <tr>
      <td>4.1</td>
      <td>Representation of CBC-MAC<sub>E<sub>k</sub></sub> (m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</td>
      <td>49</td>
    </tr>
    <tr>
      <td>4.2</td>
      <td>Representation of ECBC<sub>E<sub>k<sub>1</sub></sub>,E<sub>k<sub>2</sub></sub>,E<sub>k<sub>3</sub></sub></sub> (m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</td>
      <td>51</td>
    </tr>
    <tr>
      <td>4.3</td>
      <td>Representation of FCBC<sub>E<sub>k<sub>1</sub></sub>,E<sub>k<sub>2</sub></sub>,E<sub>k<sub>3</sub></sub></sub> (m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</td>
      <td>53</td>
    </tr>
    <tr>
      <td>4.4</td>
      <td>Representation of XCBC<sub>E<sub>k<sub>1</sub></sub>,k<sub>2</sub>,k<sub>3</sub></sub> (m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</td>
      <td>54</td>
    </tr>
    <tr>
      <td>4.5</td>
      <td>Representation of CMAC<sub>E<sub>k</sub></sub> (m<sub>1</sub>||m<sub>2</sub>||m<sub>3</sub>||m<sub>4</sub>)</td>
      <td>55</td>
    </tr>
    <tr>
      <td>4.6</td>
      <td>Layers of the CMAC's security proof.</td>
      <td>56</td>
    </tr>
    <tr>
      <td>4.7</td>
      <td>Illustration of MOMAC, by increasing size order: |m| &lt; n, |m| = n, 2n &lt; |m| &lt; 3n, |m| = 3n,</td>
      <td>62</td>
    </tr>
    <tr>
      <td>4.8</td>
      <td>Sequence of games.</td>
      <td>64</td>
    </tr>
    <tr>
      <td>4.9</td>
      <td>Games X<sub>1</sub>(A) (including dotted boxes) and X<sub>2</sub>(A) (excluding dotted boxes).</td>
      <td>65</td>
    </tr>
    <tr>
      <td>4.10</td>
      <td>Games S(A) (including dotted boxes) and T(A) (excluding dotted boxes).</td>
      <td>67</td>
    </tr>
    <tr>
      <td>5.1</td>
      <td>Indifferentiability</td>
      <td>75</td>
    </tr>
    <tr>
      <td>6.1</td>
      <td>Our results. Full lines represent extraction to EasyCrypt and compilation to assembly by the Jasmin compiler. Dashed lines represent equivalence and security proofs, formalized in EasyCrypt.</td>
      <td>79</td>
    </tr>
    <tr>
      <td>6.2</td>
      <td>Representation of SPONGE<sub>c</sub>[f, pad, r](m, l)</td>
      <td>80</td>
    </tr>
    <tr>
      <td>6.3</td>
      <td>Pseudocode for the SPONGE construction [?]</td>
      <td>80</td>
    </tr>
    <tr>
      <td>6.4</td>
      <td>Games defining the indifferentiability of the SPONGE construction from an (extendable output) RO.</td>
      <td>82</td>
    </tr>
    <tr>
      <td>6.5</td>
      <td>A layered proof for the SPONGE construction.</td>
      <td>83</td>
    </tr>
    <tr>
      <td>6.6</td>
      <td>General decomposition argument</td>
      <td>84</td>
    </tr>
    <tr>
      <td>6.7</td>
      <td>Representation of the construction D with message input of size 4 blocks and asked for an output of size 3 blocks.</td>
      <td>85</td>
    </tr>
    <tr>
      <td>6.8</td>
      <td>Representation of the construction U with message input of size m and asked for an output of size l such that 3r ≤ m &lt; 4r and 2r &lt; l ≤ 3r.</td>
      <td>85</td>
    </tr>
    <tr>
      <td>6.9</td>
      <td>BLOCKSPONGE [RP] and SQUEEZE ◦ CORESPONGE [RP] on inputs that are a list of 4 blocks and output size 3.</td>
      <td>86</td>
    </tr>
    <tr>
      <td>6.10</td>
      <td>IDEALCORE and LAST[IDEALBLOCK] on input that is a 6-blocks list whose last two blocks are full of 0.</td>
      <td>87</td>
    </tr>
    <tr>
      <td>6.11</td>
      <td>The core simulator CORESIM</td>
      <td>88</td>
    </tr>
  </tbody>
</table>
<table><tr><td>6.12 Representation of bcol.</td><td>89</td></tr><tr><td>6.13 The optimized SIMULATOR for SPONGE</td><td>91</td></tr><tr><td>6.14 Representation of G1.m and G1.mi</td><td>92</td></tr><tr><td>6.15 Representation of G1.mh and G1.mhi</td><td>93</td></tr><tr><td>6.16 Representation of G1.paths</td><td>93</td></tr><tr><td>6.17 Representation of C.queries</td><td>93</td></tr><tr><td>6.18 Representation of Redo prefixes</td><td>94</td></tr><tr><td>6.19 Representation of the first property of 4.</td><td>94</td></tr><tr><td>6.20 Representation of the second property of 4.</td><td>94</td></tr><tr><td>6.21 Representation of the property 8a.</td><td>95</td></tr><tr><td>6.22 Representation of the property 8b.</td><td>95</td></tr><tr><td>6.23 Representation of the property 8c.</td><td>96</td></tr><tr><td>7.1 Representation of the encryption of Ideal.</td><td>111</td></tr><tr><td>8.1 Representation of the encryption algorithm of ChaCha20-Poly1305.</td><td>114</td></tr><tr><td>8.2 Split Dom of PRF</td><td>119</td></tr><tr><td>8.3 Split Codom of PRF<sub>1</sub></td><td>119</td></tr><tr><td>8.4 Forth step</td><td>121</td></tr></table>
Bibliography

[Coq, 1984] (1984). The coq proof assistant. https://coq.inria.fr/. Accessed: December 15, 2020.

[Lea, 2012] (2012). Lean, theorem prover. https://leanprover.github.io/. Accessed: December 15, 2020.

[CAE, 2013] (2013). CAESAR competition. https://competitions.cr.yp.to/caesar.html. Accessed: December 15, 2020.

[Affeldt et al., 2007] Affeldt, R., Tanaka, M., and Marti, N. (2007). Formal proof of provable security by game-playing in a proof assistant. In *International Conference on Provable Security*, pages 151–168. Springer.

[Al Fardan and Paterson, 2013] Al Fardan, N. J. and Paterson, K. G. (2013). Lucky thirteen: Breaking the tls and dtls record protocols. In *2013 IEEE Symposium on Security and Privacy*, pages 526–540. IEEE.

[Almeida et al., 2017] Almeida, J. B., Barbosa, M., Barthe, G., Blot, A., Grégoire, B., Laporte, V., Oliveira, T., Pacheco, H., Schmidt, B., and Strub, P.-Y. (2017). Jasmin: High-assurance and high-speed cryptography. In *Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security*, pages 1807–1823. ACM.

[Almeida et al., 2019a] Almeida, J. B., Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Laporte, V., Oliveira, T., and Strub, P.-Y. (2019a). The last mile: High-assurance and high-speed cryptographic implementations. *arXiv preprint arXiv:1904.04606*.

[Almeida et al., 2019b] Almeida, J. B., Baritel-Ruet, C., Barbosa, M., Barthe, G., Dupressoir, F., Grégoire, B., Laporte, V., Oliveira, T., Stoughton, A., and Strub, P.-Y. (2019b). 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*, pages 1607–1622.

[Aumasson et al., 2008] Aumasson, J.-P., Fischer, S., Khazaei, S., Meier, W., and Rechberger, C. (2008). New features of latin dances: analysis of salsa, chacha, and rumba. In *International Workshop on Fast Software Encryption*, pages 470–488. Springer.

[Backes et al., 2012] Backes, M., Barthe, G., Berg, M., Grégoire, B., Kunz, C., Skoruppa, M., and Zanella-Béguelin, S. (2012). Verified security of merkle-Damgård. pages 354–368.

[Baritel-Ruet et al., 2018] Baritel-Ruet, C., Dupressoir, F., Fouque, P.-A., and Grégoire, B. (2018). Formal security proof of cmac and its variants. In *2018 IEEE 31st Computer Security Foundations Symposium (CSF)*, pages 91–104. IEEE.
[Barthe et al., 2010] Barthe, G., Grégoire, B., and Béguelin, S. Z. (2010). Programming language techniques for cryptographic proofs. In *International Conference on Interactive Theorem Proving*, pages 115–130. Springer.

[Barthe et al., 2011a] Barthe, G., Grégoire, B., Heraud, S., and Béguelin, S. Z. (2011a). Computer-aided security proofs for the working cryptographer. In *Annual Cryptology Conference*, pages 71–90. Springer.

[Barthe et al., 2011b] Barthe, G., Grégoire, B., Lakhnech, Y., and Béguelin, S. Z. (2011b). Beyond provable security verifiable ind-cca security of oaep. In *Cryptographers' Track at the RSA Conference*, pages 180–196. Springer.

[Barthe et al., 2009] Barthe, G., Grégoire, B., and Zanella Béguelin, S. (2009). Formal certification of code-based cryptographic proofs. In *Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages*, pages 90–101.

[Bellare, 1997] Bellare, M. (1997). Practice-oriented provable-security. In *International Workshop on Information Security*, pages 221–231. Springer.

[Bellare et al., 1997] Bellare, M., Desai, A., Jokipii, E., and Rogaway, P. (1997). A concrete security treatment of symmetric encryption. In *Proceedings 38th Annual Symposium on Foundations of Computer Science*, pages 394–403. IEEE.

[Bellare et al., 1998a] Bellare, M., Desai, A., Pointcheval, D., and Rogaway, P. (1998a). Relations among notions of security for public-key encryption schemes. In *Annual International Cryptology Conference*, pages 26–45. Springer.

[Bellare et al., 1998b] Bellare, M., Garay, J. A., and Rabin, T. (1998b). Fast batch verification for modular exponentiation and digital signatures. In *International Conference on the Theory and Applications of Cryptographic Techniques*, pages 236–250. Springer.

[Bellare et al., 1994] Bellare, M., Kilian, J., and Rogaway, P. (1994). The security of cipher block chaining. In *Advances in Cryptology—CRYPTO’94*, pages 341–358. Springer.

[Bellare and Namprempre, 2000] Bellare, M. and Namprempre, C. (2000). Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In *International Conference on the Theory and Application of Cryptology and Information Security*, pages 531–545. Springer.

[Bellare et al., 2005] Bellare, M., Pietrzak, K., and Rogaway, P. (2005). Improved security analyses for CBC MACs. In *Crypto*, volume 3621, pages 527–545. Springer.

[Bellare and Rogaway, 1994] Bellare, M. and Rogaway, P. (1994). Optimal asymmetric encryption. In *Workshop on the Theory and Application of Cryptographic Techniques*, pages 92–111. Springer.

[Bellare and Rogaway, 1995] Bellare, M. and Rogaway, P. (1995). Random oracles are practical: a paradigm for designing efficient protocols. *Proc. of the 1st CCS*, pages 62–73.

[Bellare and Rogaway, 2006] Bellare, M. and Rogaway, P. (2006). The security of triple encryption and a framework for code-based game-playing proofs. In *Annual International Conference on the Theory and Applications of Cryptographic Techniques*, pages 409–426. Springer.

[Bernstein, 2005] Bernstein, D. J. (2005). The poly1305-aes message-authentication code. In *International Workshop on Fast Software Encryption*, pages 32–49. Springer.

[Bernstein, 2008a] Bernstein, D. J. (2008a). Chacha, a variant of salsa20. In *Workshop Record of SASC*, volume 8, pages 3–5.
[Bernstein, 2008b] Bernstein, D. J. (2008b). The salsa20 family of stream ciphers. In *New stream cipher designs*, pages 84–97. Springer.

[Bertoni et al., 2008] Bertoni, G., Daemen, J., Peeters, M., and Van Assche, G. (2008). On the indifferentiability of the sponge construction. pages 181–197.

[Bertot, 2006] Bertot, Y. (2006). Coq in a hurry. *arXiv preprint cs/0603118*.

[Black and Rogaway, 2005] Black, J. and Rogaway, P. (2005). CBC MACs for arbitrary-length messages: The three-key constructions. *Journal of Cryptology*, 18(2):111–131.

[Blanchet, 2013] Blanchet, B. (2013). Automatic verification of security protocols in the symbolic model: The verifier proverif. In *Foundations of Security Analysis and Design VII*, pages 54–87. Springer.

[Boneh and Franklin, 2003] Boneh, D. and Franklin, M. (2003). Identity-based encryption from the weil pairing. *SIAM journal on computing*, 32(3):586–615.

[Bosselaers and Preneel, 1995] Bosselaers, A. and Preneel, B. (1995). *Integrity Primitives for Secure Information Systems: Final Ripe Report of Race Integrity Primitives Evaluation*. Number 1007. Springer Science & Business Media.

[Carter and Wegman, 1977] Carter, J. L. and Wegman, M. N. (1977). Universal classes of hash functions (extended abstract). In *in STOC'77: Proceedings of the ninth annual ACM symposium on Theory of computing*. Citeseer.

[Chakraborty et al., 2015] Chakraborty, D., Hernandez-Jimenez, V., and Sarkar, P. (2015). Another look at xcb. *Cryptography and Communications*, 7(4):439–468.

[Cogliati et al., 2018] Cogliati, B., Dodis, Y., Katz, J., Lee, J., Steinberger, J. P., Thiruvengadam, A., and Zhang, Z. (2018). Provable security of (tweakable) block ciphers based on substitution-permutation networks. pages 722–753.

[Coron, 2002] Coron, J.-S. (2002). Optimal security proofs for pss and other signature schemes. In *International Conference on the Theory and Applications of Cryptographic Techniques*, pages 272–287. Springer.

[Coron et al., 2005] Coron, J.-S., Dodis, Y., Malinaud, C., and Puniya, P. (2005). Merkle-Damgård revisited: How to construct a hash function. pages 430–448.

[Coron and Naccache, 1999] Coron, J.-S. and Naccache, D. (1999). On the security of rsa screening. In *International Workshop on Public Key Cryptography*, pages 197–203. Springer.

[Dachman-Soled et al., 2016] Dachman-Soled, D., Katz, J., and Thiruvengadam, A. (2016). 10-round feistel is indifferentiable from an ideal cipher. In *Annual International Conference on the Theory and Applications of Cryptographic Techniques*, pages 649–678. Springer.

[Dachman-Soled et al., 2016] Dachman-Soled, D., Katz, J., and Thiruvengadam, A. (2016). 10-round Feistel is indifferentiable from an ideal cipher. pages 649–678.

[Daemen and Rijmen, 1999] Daemen, J. and Rijmen, V. (1999). Aes proposal: Rijndael.

[Daemen and Rijmen, 2013] Daemen, J. and Rijmen, V. (2013). *The design of Rijndael: AES-the advanced encryption standard*. Springer Science & Business Media.

[Dai and Steinberger, 2016a] Dai, Y. and Steinberger, J. (2016a). Indifferentiability of 8-round feistel networks. In *Annual International Cryptology Conference*, pages 95–120. Springer.

[Dai and Steinberger, 2016b] Dai, Y. and Steinberger, J. P. (2016b). Indifferentiability of 8-round Feistel networks. pages 95–120.
[Dalal et al., 2010] Dalal, N., Shah, J., Hisaria, K., and Jinwala, D. (2010). A comparative analysis of tools for verification of security protocols. *International Journal of Communications, Network and System Sciences*, 3(10):779.

[Dolev and Yao, 1983] Dolev, D. and Yao, A. (1983). On the security of public key protocols. *IEEE Transactions on information theory*, 29(2):198–208.

[Dworkin, 2015] Dworkin, M. J. (2015). Sha-3 standard: Permutation-based hash and extendable-output functions. Technical report.

[Dworkin, 2016] Dworkin, M. J. (2016). Recommendation for block cipher modes of operation: The CMAC mode for authentication. *Special Publication (NIST SP)-800-38B*.

[Ehrsam et al., 1978] Ehrsam, W. F., Meyer, C. H., Smith, J. L., and Tuchman, W. L. (1978). Message verification and transmission error detection by block chaining. US Patent 4,074,066.

[Galindo, 2005] Galindo, D. (2005). Boneh-franklin identity based encryption revisited. In *International Colloquium on Automata, Languages, and Programming*, pages 791–802. Springer.

[Garman et al., 2016] Garman, C., Green, M., Kaptchuk, G., Miers, I., and Rushanan, M. (2016). Dancing on the lip of the volcano: Chosen ciphertext attacks on apple imessage. In *25th {USENIX} Security Symposium ({USENIX} Security 16)*, pages 655–672.

[Gaži and Maurer, 2009] Gaži, P. and Maurer, U. (2009). Cascade encryption revisited. In *International Conference on the Theory and Application of Cryptology and Information Security*, pages 37–51. Springer.

[Goldwasser and Micali, 1984] Goldwasser, S. and Micali, S. (1984). Probabilistic encryption. *Journal of computer and system sciences*, 28(2):270–299.

[Goldwasser et al., 1988] Goldwasser, S., Micali, S., and Rivest, R. L. (1988). A digital signature scheme secure against adaptive chosen-message attacks. *SIAM Journal on Computing*, 17(2):281–308.

[Gordon, 1988] Gordon, M. J. (1988). Hol: A proof generating system for higher-order logic. In *VLSI specification, verification and synthesis*, pages 73–128. Springer.

[Hales, 2008] Hales, T. C. (2008). Formal proof. *Notices of the AMS*, 55(11):1370–1380.

[Herzog, 2005] Herzog, J. (2005). A computational interpretation of dolev-yao adversaries. *Theoretical Computer Science*, 340(1):57–81.

[Impagliazzo and Rudich, 1989] Impagliazzo, R. and Rudich, S. (1989). Limits on the provable consequences of one-way permutations. In *Proceedings of the twenty-first annual ACM symposium on Theory of computing*, pages 44–61. ACM.

[Inoue et al., 2019] Inoue, A., Iwata, T., Minematsu, K., and Poettering, B. (2019). Cryptanalysis of ocb2: Attacks on authenticity and confidentiality. *IACR Cryptology ePrint Archive*, 2019:311.

[Ishiguro, 2012] Ishiguro, T. (2012). Modified version of 'latin dances revisited: New analytic results of salsa20 and chacha". *IACR Cryptology ePrint Archive*, 2012:65.

[Isobe et al., 2013] Isobe, T., Ohigashi, T., Watanabe, Y., and Morii, M. (2013). Full plaintext recovery attack on broadcast rc4. In *International Workshop on Fast Software Encryption*, pages 179–202. Springer.

[Iwata and Kurosawa, 2003] Iwata, T. and Kurosawa, K. (2003). OMAC: One-key CBC MAC. In *FSE*, volume 2887, pages 129–153. Springer.
[Iwata et al., 2012] Iwata, T., Ohashi, K., and Minematsu, K. (2012). Breaking and repairing GCM security proofs. In *Crypto*, volume 7417, pages 31–49. Springer.

[Jha and Nandi, 2016] Jha, A. and Nandi, M. (2016). Revisiting structure graphs: Applications to cbc-mac and emac. *Journal of Mathematical Cryptology*, 10(3-4):157–180.

[Jonsson et al., 2001] Jonsson, B., Yi, W., and Larsen, K. G. (2001). Probabilistic extensions of process algebras. In *Handbook of process algebra*, pages 685–710. Elsevier.

[Kakvi and Kiltz, 2012] Kakvi, S. A. and Kiltz, E. (2012). Optimal security proofs for full domain hash, revisited. In *Annual International Conference on the Theory and Applications of Cryptographic Techniques*, pages 537–553. Springer.

[Katz and Lindell, 2014] Katz, J. and Lindell, Y. (2014). *Introduction to modern cryptography*. CRC press.

[Katz and Yung, 2000a] Katz, J. and Yung, M. (2000a). Complete characterization of security notions for probabilistic private-key encryption. In *Proceedings of the thirty-second annual ACM symposium on Theory of computing*, pages 245–254.

[Katz and Yung, 2000b] Katz, J. and Yung, M. (2000b). Unforgeable encryption and chosen ciphertext secure modes of operation. In *International Workshop on Fast Software Encryption*, pages 284–299. Springer.

[Kaufman et al., 1995] Kaufman, C., Perlman, R., and Speciner, M. (1995). Network security: private communication in a public world.

[Kayser, 2007] Kayser, R. F. (2007). Announcing request for candidate algorithm nominations for a new cryptographic hash algorithm (sha-3) family. *Federal Register*, 72(212):62.

[Kerckhoffs, 1883] Kerckhoffs, A. (1883). La cryptographic militaire. *Journal des sciences militaires*, pages 5–38.

[Krawczyk, 2005] Krawczyk, H. (2005). Hmqv: A high-performance secure diffie-hellman protocol. In *Annual International Cryptology Conference*, pages 546–566. Springer.

[Langley et al., 2016] Langley, A., Chang, W., Mavrogiannopoulos, N., Strombergson, J., and Josefsson, S. (2016). Chacha20-poly1305 cipher suites for transport layer security (tls). *RFC 7905*, (10).

[Leurent and Peyrin, 2019] Leurent, G. and Peyrin, T. (2019). From collisions to chosen-prefix collisions application to full sha-1. In *Annual International Conference on the Theory and Applications of Cryptographic Techniques*, pages 527–555. Springer.

[Maurer et al., 2004] Maurer, U. M., Renner, R., and Holenstein, C. (2004). Indifferentiability, impossibility results on reductions, and applications to the random oracle methodology. pages 21–39.

[McGrew and Viega, 2004a] McGrew, D. and Viega, J. (2004a). The galois/counter mode of operation (gcm). *Submission to NIST Modes of Operation Process*, 20.

[McGrew and Fluhrer, 2007] McGrew, D. A. and Fluhrer, S. R. (2007). The security of the extended codebook (xcb) mode of operation. In *International Workshop on Selected Areas in Cryptography*, pages 311–327. Springer.

[McGrew and Viega, 2004b] McGrew, D. A. and Viega, J. (2004b). The security and performance of the galois/counter mode (GCM) of operation. In *Indocrypt*, volume 3348, pages 343–355. Springer.

[Menezes, 2007] Menezes, A. (2007). Another look at hmqv. *Mathematical Cryptology JMC*, 1(1):47–64.
[Morris et al., 1977] Morris, R., Sloane, N., and Wyner, A. D. (1977). Assessment of the national bureau of standards proposed federal data encryption standard. *Cryptologia*, 1(3):281-291.

[Nandi, 2014] Nandi, M. (2014). Xls is not a strong pseudorandom permutation. In *International Conference on the Theory and Application of Cryptology and Information Security*, pages 478-490. Springer.

[Naor and Yung, 1990] Naor, M. and Yung, M. (1990). Public-key cryptosystems provably secure against chosen ciphertext attacks. In *Proceedings of the twenty-second annual ACM symposium on Theory of computing*, pages 427-437.

[Nir and Langley, 2015] Nir, Y. and Langley, A. (2015). ChaCha20 and Poly1305 for IETF Protocols. RFC 7539.

[Oechslin, 2003] Oechslin, P. (2003). Making a faster cryptanalytic time-memory trade-off. In *Annual International Cryptology Conference*, pages 617-630. Springer.

[Owre et al., 1992] Owre, S., Rushby, J. M., and Shankar, N. (1992). Pvs: A prototype verification system. In *International Conference on Automated Deduction*, pages 748-752. Springer.

[Paulson, 1994] Paulson, L. C. (1994). *Isabelle: A generic theorem prover*, volume 828. Springer Science & Business Media.

[Perlman et al., 2016] Perlman, R., Kaufman, C., and Speciner, M. (2016). *Network security: private communication in a public world*. Pearson Education India.

[Preneel, 1998] Preneel, B. (1998). Cryptographic primitives for information authentication—state of the art. In *State of the Art in Applied Cryptography*, pages 49-104. Springer.

[Procter, 2014] Procter, G. (2014). A security analysis of the composition of chacha20 and poly1305. *IACR Cryptology ePrint Archive*, 2014:613.

[Protzenko et al., 2019] Protzenko, J., Parno, B., Fromherz, A., Hawblitzel, C., Polubelova, M., Bhargavan, K., Beurdouche, B., Choi, J., Delignat-Lavaud, A., Fournet, C., et al. (2019). Evercrypt: A fast, verified, cross-platform cryptographic provider. In *2020 IEEE Symposium on Security and Privacy (SP)*, pages 634-653.

[Rackoff and Simon, 1991] Rackoff, C. and Simon, D. R. (1991). Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In *Annual International Cryptology Conference*, pages 433-444. Springer.

[Regenscheid, 2016] Regenscheid, A. R. (2016). Nist cryptographic standards and guidelines development process. Technical report.

[Ristenpart and Rogaway, 2007] Ristenpart, T. and Rogaway, P. (2007). How to enrich the message space of a cipher. In *International Workshop on Fast Software Encryption*, pages 101-118. Springer.

[Rivest et al., 1983] Rivest, R. L., Shamir, A., and Adleman, L. (1983). A method for obtaining digital signatures and public-key cryptosystems. *Communications of the ACM*, 26(1):96-99.

[Rogaway, 2004a] Rogaway, P. (2004a). Efficient instantiations of tweakable blockciphers and refinements to modes ocb and pmac. In *International Conference on the Theory and Application of Cryptology and Information Security*, pages 16-31. Springer.

[Rogaway, 2004b] Rogaway, P. (2004b). Nonce-based symmetric encryption. In *International Workshop on Fast Software Encryption*, pages 348-358. Springer.
[Rogaway, 2009] Rogaway, P. (2009). Practice-oriented provable security and the social construction of cryptography. *Unpublished essay*.

[Shannon, 1949] Shannon, C. E. (1949). Communication theory of secrecy systems. *Bell system technical journal*, 28(4):656–715.

[Shi et al., 2012] Shi, Z., Zhang, B., Feng, D., and Wu, W. (2012). Improved key recovery attacks on reduced-round salsa20 and chacha. In *International Conference on Information Security and Cryptology*, pages 337–351. Springer.

[Shoup, 1998] Shoup, V. (1998). *Why chosen ciphertext security matters*, volume 57. IBM TJ Watson Research Center.

[Shoup, 2002] Shoup, V. (2002). Oaep reconsidered. *Journal of Cryptology*, 15(4):223–249.

[Shoup, 2004] Shoup, V. (2004). Sequences of games: a tool for taming complexity in security proofs. *IACR Cryptology ePrint Archive*, 2004:332.

[Song et al., 2006] Song, J., Poovendran, R., Lee, J., and Iwata, T. (2006). The AES-CMAC algorithm. Technical report, RFC 4493, June.

[Stern et al., 2002] Stern, J., Pointcheval, D., Malone-Lee, J., and Smart, N. P. (2002). Flaws in applying proof methodologies to signature schemes. In *Annual International Cryptology Conference*, pages 93–110. Springer.

[Stevens et al., 2017] Stevens, M., Bursztein, E., Karpman, P., Albertini, A., and Markov, Y. (2017). The first collision for full sha-1. In *Annual International Cryptology Conference*, pages 570–596. Springer.

[Swamy et al., 2016] Swamy, N., Hrițcu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P-Y., Kohlweiss, M., et al. (2016). Dependent types and multi-monadic effects in f. In *Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, pages 256–270.

[Vaudenay, 2000] Vaudenay, S. (2000). Decorrelation over infinite domains: the encrypted CBC-MAC case. In *Selected Areas in Cryptography*, volume 2012, pages 189–201. Springer.

[Yao, 1982] Yao, A. C. (1982). Theory and application of trapdoor functions. In *23rd Annual Symposium on Foundations of Computer Science (sfcs 1982)*, pages 80–91. IEEE.

[Zinzindohoué et al., 2017] Zinzindohoué, J.-K., Bhargavan, K., Protzenko, J., and Beurdouche, B. (2017). Hacl*: A verified modern cryptographic library. In *ACM Conference on Computer and Communications Security (CCS)*.