<table><caption>Figure 13: Subset of the calculus for the initial game</caption><tr><td>M, N ::=</td><td>terms</td></tr><tr><td>i</td><td>replication index</td></tr><tr><td>x[M<sub>1</sub>,...,M<sub>m</sub>]</td><td>variable access</td></tr><tr><td>f(M<sub>1</sub>,...,M<sub>m</sub>)</td><td>function application</td></tr><tr><td>x R T; N</td><td>random number</td></tr><tr><td>let p = M in N else N'</td><td>assignment (pattern-matching)</td></tr><tr><td>let x : T = M in N</td><td>assignment</td></tr><tr><td>if M then N else N'</td><td>conditional</td></tr><tr><td>find[unique?] (&#8700;<sub>j=1</sub><sup>m</sup> u<sub>j1</sub>[i&#x0303;] = i<sub>j1</sub> &le; n<sub>j1</sub>,...,u<sub>jm<sub>j</sub></sub>[i&#x0303;] = i<sub>jm<sub>j</sub></sub> &le; n<sub>jm<sub>j</sub></sub> suchthat<br/>defined(M<sub>j1</sub>,...,M<sub>jl<sub>j</sub></sub>) &and; M'<sub>j</sub> then N<sub>j</sub>) else N'</td><td>array lookup</td></tr><tr><td>insert Tbl(M<sub>1</sub>,...,M<sub>l</sub>); N</td><td>insert in table</td></tr><tr><td>get[unique?] Tbl(p<sub>1</sub>,...,p<sub>l</sub>) suchthat M in N else N'</td><td>get from table</td></tr><tr><td>event e(M<sub>1</sub>,...,M<sub>l</sub>); N</td><td>event</td></tr><tr><td>event_abort e</td><td>event e and abort</td></tr><tr><td>p ::=</td><td>pattern</td></tr><tr><td>x : T</td><td>variable</td></tr><tr><td>f(p<sub>1</sub>,...,p<sub>m</sub>)</td><td>function application</td></tr><tr><td>=M</td><td>comparison with a term</td></tr><tr><td>Q ::=</td><td>oracle definition</td></tr><tr><td>0</td><td>nil</td></tr><tr><td>Q | Q'</td><td>parallel composition</td></tr><tr><td>foreach i &le; n do Q</td><td>replication n times</td></tr><tr><td>O(p) := P</td><td>oracle definition</td></tr><tr><td>P ::=</td><td>oracle body</td></tr><tr><td>return (N); Q</td><td>return</td></tr><tr><td>x R T; P</td><td>random number</td></tr><tr><td>let p = M in P else P'</td><td>assignment</td></tr><tr><td>if M then P else P'</td><td>conditional</td></tr><tr><td>find[unique?] (&#8700;<sub>j=1</sub><sup>m</sup> u<sub>j1</sub>[i&#x0303;] = i<sub>j1</sub> &le; n<sub>j1</sub>,...,u<sub>jm<sub>j</sub></sub>[i&#x0303;] = i<sub>jm<sub>j</sub></sub> &le; n<sub>jm<sub>j</sub></sub> suchthat<br/>defined(M<sub>j1</sub>,...,M<sub>jl<sub>j</sub></sub>) &and; M<sub>j</sub> then P<sub>j</sub>) else P</td><td>array lookup</td></tr><tr><td>insert Tbl(M<sub>1</sub>,...,M<sub>l</sub>); P</td><td>insert in table</td></tr><tr><td>get[unique?] Tbl(p<sub>1</sub>,...,p<sub>l</sub>) suchthat M in P else P'</td><td>get from table</td></tr><tr><td>event e(M<sub>1</sub>,...,M<sub>l</sub>); P</td><td>event</td></tr><tr><td>event_abort e</td><td>event e and abort</td></tr><tr><td>yield</td><td>end</td></tr></table>
indices at the definition of $x$. Such accesses are simply abbreviated as $x$. Variables can then be considered as ordinary variables instead of arrays, since we only access the array cell at the current replication indices. This choice has several other advantages:

* Tables with get/insert are closer to lists usually used by cryptographers than find, they should be easier to understand for the user.

* Our compiler that translates CryptoVerif specifications into OCaml implementations [32] does not support find, because tables with get/insert are also much easier to implement than find.

We can define processes by macros: let pid($x_1$: $T_1$, ..., $x_m$: $T_m$) = P or let qid($x_1$: $T_1$, ..., $x_m$: $T_m$) = Q. If a process pid($M_1$, ..., $M_m$) occurs in the initial game, CryptoVerif verifies that $M_1$, ..., $M_m$ are of types $T_1$, ..., $T_m$ respectively, and replaces pid($M_1$, ..., $M_m$) with the expansion $P\{M_1/x_1, ..., M_m/x_m\}$.

We can also define functions by macros: letfun $f(x_1$: $T_1$, ..., $x_m$: $T_m$) = M. If a term $f(M_1, ..., M_m)$ occurs in the initial game, CryptoVerif verifies that $M_1$, ..., $M_m$ are of types $T_1$, ..., $T_m$ respectively, and replaces $f(M_1, ..., M_m)$ with the expansion $M\{M_1/x_1, ..., M_m/x_m\}$.

In the initial game, all bound variables with several incompatible definitions (different indices, different types, or variables defined in the same branch of a test) as well as variables declared without an explicit type are not allowed to occur in $V$ nor in defined conditions of find or if and are renamed to distinct names, so that Invariant 1 is satisfied for these variables. CryptoVerif checks the rest of the invariants.

## 2.6 Input Language with Channels instead of Oracles

CryptoVerif also allows defining games in a channel-based process calculus inspired by the applied pi calculus [1, 2] and by the calculi of [59] and of [55]. This input language is mostly compatible with the symbolic protocol verifier ProVerif [28] (http://proverif.inria.fr), up to the following differences:

* ProVerif does not support find. Since ProVerif supports tables, one can encode most usages of find using tables instead for compatibility with ProVerif.

* ProVerif does not support channels with indices. As mentioned below, in CryptoVerif, the channels are indexed with the current replication indices. Since CryptoVerif automatically adds the current replication indices to channels without indices, one can easily use channels without indices.

So avoiding find and channels with indices allows us to have a language compatible with ProVerif for the definition of processes. (The assumptions on cryptographic primitives still need to be defined in a different way. In practice, these assumptions can be included in a library, using different libraries for ProVerif and for CryptoVerif.)

### 2.6.1 Input Language Description

Instead of defining oracles that the adversary can interact with, processes are now considered as communicating over a network with explicit input and output commands. The adversary has full control over the network: it receives any value output by a process and it is in charge of sending the input values to the processes. Inputs and outputs are made over channels, a set of constants often denoted by $c$.

Concretely, the following changes are made to the syntax previously defined in Figure 1:
* oracle definitions are called input processes and oracle bodies are called output processes;

* oracle declarations $O[\tilde{i}](p) := P$ do not exist anymore and are replaced with inputs $c[\tilde{i}](p)$; $P$, where $\tilde{i}$ are the current replication indices;

* return commands `return` ($N$); $Q$ are now output commands $\overline{c[\tilde{i}]}\langle N \rangle$; $Q$, where $\tilde{i}$ are the current replication indices;

* the `yield` command is now considered as syntactic sugar for `yield`($\langle N \rangle$), where `yield` is a specific channel not used elsewhere;

* oracle calls and oracle restrictions do not exist anymore. (Oracle calls can be encoded via channel inputs and outputs. We could introduce a channel restriction to match the oracle restriction, but it would be useful only in proofs, not in the input calculus of CryptoVerif.)

### 2.6.2 Translating from the Channel Calculus to the Oracle Calculus

Processes specified in the channel calculus are directly translated to the oracle calculus; this feature is only a form of syntactic sugar available for convenience. Notably, we do not define a formal semantics for the channel calculus, and all up to date theoretical developments of CryptoVerif are over the oracle calculus. For reference, the old semantics of the channel calculus variant can be found here [29]. We describe informally the translation here, which proceeds as follows:

* Any input of the form $c[\tilde{i}](p)$; $P$ is translated as an oracle definition $O_c[\tilde{i}](p) := P$ where the oracle name $O_c$ is built from the input channel $c$.

* Any output of the form $\overline{c[\tilde{i}]}\langle N \rangle$; $Q$ is translated as `return`($N$); $Q$.

All input processes cannot be translated. We provide a list of invariants needed so that the translation preserves the semantics and produces valid instances of the oracle calculus. A first invariant is needed so that the translated process satisfies Invariant 7. We define the following multiset by induction over input and output processes, in a similar fashion to the previously defined *Defined*<sup>O</sup>:

$$ 
\begin{align*}
\text{Defined}^c(0) &= \emptyset \\
\text{Defined}^c(Q_1 | Q_2) &= \text{Defined}^c(Q_1) \uplus \text{Defined}^c(Q_2) \\
\text{Defined}^c(\text{foreach } i \le n \text{ do } Q) &= \text{Defined}^c(Q) \\
\text{Defined}^c(c[\tilde{i}](p); P) &= \{c\} \uplus \text{Defined}^c(P) \\
\text{Defined}^c(C[Q_1, \dots, Q_k]) &= \max_{j=1}^k \text{Defined}^c(Q_j)
\end{align*}
$$

where $C$ is any oracle body context.

**Channel Calculus Invariant 1** The input process $Q_0$ satisfies the Channel Invariant 1 if and only if

1. in every input and output over channel $c$ in $Q_0$, the indices $\tilde{i}$ of $c$ are the current replication indices at that declaration, and

2. $\text{Defined}^c(Q_0)$ does not contain duplicate elements.
In other words, Item 2 of Channel Invariant 1 means that inputs on the same channel occur in different branches of a find, if (or let), oracle call, or get.

A more complex issue is that in the channel calculus semantics, whenever an output can be received on the same channel by an input of the process, the output is probabilistically either caught by the attacker or directly transmitted to the input process. There is no equivalent to this probabilistic choice in the oracle setting. We thus add a channel invariant that makes it so that no output of the defined process can be received by the process itself. To this end, we define the following functions:

* $Ch_o(Q)$ is the set of pairs $(c, k)$ of channels $c$ that occur with $k$ indices as output inside $Q$, that is, in a subprocess of the form $c[i] \langle N \rangle; Q'$ inside $Q$, where the length of $i$ is $k$;

* $Ch_i(Q)$ is the set of pairs $(c, k)$ of channels $c$ that occur with $k$ indices as input inside $Q$, that is, in a subprocess of the form $c[i](p); P$ inside $Q$, where the length of $i$ is $k$;

* $NoIntIO(Q)$ is true when no direct communication on a channel can occur inside $Q$, without going through the attacker:

$$ 
\begin{align*}
\text{NoIntIO}(0) &= \text{true} \\
\text{NoIntIO}(Q_1 | Q_2) &= \text{NoIntIO}(Q_1) \wedge \text{NoIntIO}(Q_2) \wedge \\
& \quad (\text{Ch}_i(Q_1) \cap \text{Ch}_o(Q_2) = \emptyset) \wedge (\text{Ch}_i(Q_2) \cap \text{Ch}_o(Q_1) = \emptyset) \\
\text{NoIntIO}(\text{foreach } i \le n \text{ do } Q) &= \text{NoIntIO}(Q) \\
\text{NoIntIO}(c[i](p); C[Q_1, \dots, Q_k]) &= \bigwedge_{j=1}^{k} \text{NoIntIO}(Q_j)
\end{align*}
$$

where $C$ is any oracle body context.

**Channel Calculus Invariant 2** The input process $Q_0$ satisfies the Channel Invariant 2 if and only if $\text{NoIntIO}(Q_0) = \text{true}$.

This invariant guarantees that dynamically, there will be no input available in the process on a channel when the process performs an output on that channel. This is obtained by statically requiring that, when there is an output on channel $c$, the inputs on channel $c$ with the same number of indices are syntactically above or under that output, or in a different branch, but not in a process in parallel.

When translating an output to a return, notice that the channel is dropped. The attacker might lose some distinguishing power if several outputs in distinct branches were made on distinct channels. We thus forbid this in the channel calculus.

**Channel Calculus Invariant 3** The input process $Q_0$ satisfies the Channel Invariant 3 if and only if for all inputs on a given channel, all outputs directly below these inputs are over the same channel.

Most other previously defined invariants must also hold and can be seen as independent from oracles or channels.

**Channel Calculus Invariant 4** The input process $Q_0$ satisfies the Channel Invariant 4 if only if it satisfies the Invariants 1 (with the minor modification that there are no oracle calls), 2, 3, 4, 5 and 6.
We do not explicitly state the typing Channel Invariant, which would correspond to Invariant 8. The old typing invariant for the channel calculus can be found in [29]. However, the translation to oracles strengthens this invariant: informally, inputs on the same channel must receive messages of same type (since they translate to oracle definitions of the same oracle) and outputs that follow inputs on the same channel must send messages of the same type (since they translate into returns of the same oracle).

## 2.7 Subsets used inside the Sequence of Games

During the computation of the sequence of games, several properties are used by CryptoVerif, either required by some game transformations or guaranteed by others. We summarize them in this section.

**Property 1** No function returns values of interval types. The types of values chosen by $x[i] \stackrel{R}{\leftarrow} T$ are not interval types. The type *T* of the returned message in the (TRet) rule and of the receiving pattern in the (TDecl) rule are not interval types.

This property is satisfied by all games manipulated by CryptoVerif, but not by contexts that model parts of the adversary. Combined with Invariants 8, 2, and 5, it implies that the terms of variable accesses $x[M_1, \dots, M_m]$ contain only replication indices and variables. (Tuples, events, and tables can take interval types as arguments. The constraint on oracle declarations and returns could probably be relaxed.)

For oracles that model security assumptions on primitives, the receiving variable can be of an interval type. (This is used for instance to specify the computational Diffie-Hellman assumption; see Section 5.2.)

**Property 2** The construct newOracle *O* and the oracle calls do not appear in games.

These properties are also satisfied by all games manipulated by CryptoVerif, but not by processes that model the adversary.

**Property 3** The constructs *insert* and *get* do not occur in the game.

This property is not valid in the initial game, but it is in all other games of the sequence produced by CryptoVerif. The very first game transformation applied by CryptoVerif, **expand_tables**, encodes *insert* and *get* using *find* (see Section 5.1.2). The constructs *insert* and *get* are never introduced by subsequent game transformations, so this property remains valid in the rest of the sequence.

**Property 4** The variables defined in conditions of *find* have pairwise distinct names.

This property is enforced by the transformation **auto_SArename** (see Section 5.1.2) by renaming variables defined in conditions of *find* to distinct names. (This is easy since these variables do not have array accesses by Invariant 3.) Property 4 is required as a precondition by many game transformations, and may be broken by game transformations that duplicate code. Therefore, we apply **auto_SArename** after these game transformations.

**Property 5** The terms *M* are simple except for conditions of *find*.
<figure><img src="image_6.png" /><figcaption>Figure 14: Subset after game expansion</figcaption></figure>
The grammar of the language taking into account this property as well as Properties 2 and 3 is shown in Figure 14. By Invariant 4, **event** does not occur in conditions of **find**, so **event** never occurs as term. Property 5 is enforced by the transformation **expand** (see Section 5.1.3) by converting other terms into processes. This transformation is applied on the initial game after **expand_tables**. Property 5 is broken by the cryptographic transformation of Section 5.2, so by default **expand** is called again after this transformation. Many game transformations require Property 5 as a precondition.

## 2.8 Security Properties, Indistinguishability

A context is a process containing a hole []. An evaluation context $C$ is a context built from [], `newOracle O; C, Q | C`, and $C | Q$.

We use an evaluation context to represent an adversary in addition to the attacker $\mathcal{A}$. Adversarial contexts are useful, e.g., to push code inside the adversary in reduction proofs, but are also needed so that the attacker $\mathcal{A}$ can raise events, access the public variables in $V$, and return its final result to a distinguisher by raising an event with that result as argument, by calling oracles of the context that execute these actions. We denote by $C[Q]$ the oracle definition obtained by replacing the hole [] in the context $C$ with the oracle definition $Q$.

We write $event(D)$ for the set of events that occur in the distinguisher $D$ (i.e. are used by the distinguisher $D$). We write $event(Q)$ for the set of events that occur in the process $Q$. We use similar notations for oracle bodies, contexts, ... We write $event(Q, Q')$ for $event(Q) \cup event(Q')$.

From now on, we consider in this section a fixed attacker space $\mathcal{BB}$, and all security definitions are given for this $\mathcal{BB}$. There must exist a function allowing to extract a run-time from the execution of an attacker. Classically, $\mathcal{BB}$ would be the set of interactive probabilistic Turing machines, but the theory of CryptoVerif is sound for any kind of black-box interactive attacker, where the computational power is restricted by the cryptographic axioms. As cryptographic reductions sound for a black-box interactive attacker are also sound for quantum Turing Machines, this notably implies the post-quantum soundness of CryptoVerif, by considering as $\mathcal{BB}$ the set of interactive quantum Turing machines.

**Definition 5 (Indistinguishability)** Let $Q$ and $Q'$ be two processes, $V$ a set of variables, and $\mathcal{E}$ a set of events. Assume that $Q$ and $Q'$ satisfy Invariants 1 to 8 with public variables $V$, and the variables of $V$ are defined in $Q$ and $Q'$, with the same types.

An evaluation context $C$ is said to be *acceptable* for $Q$ with public variables $V$ if and only if $\text{var}(C) \cap \text{var}(Q) \subseteq V$, $\text{vardef}(C) \cap V = \emptyset$, $C$ and $Q$ do not use any common table, and $C[Q]$ satisfies Invariants 1 to 8 with public variables $V$.

We write $Q \approx_p^{V, \mathcal{E}} Q'$ when, for all attackers $A \in \mathcal{BB}$, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ and all distinguishers $D$ that run in time at most $t_D$ and such that $event(D) \cap event(Q, Q') \subseteq \mathcal{E}$, $|\text{Pr}^A[C[Q] : D] - \text{Pr}^A[C[Q'] : D]| \le p(A, C, t_D)$.

This definition formalizes that the probability that algorithms $A$, $C$, and $D$ distinguish the games $Q$ and $Q'$ is at most $p(A, C, t_D)$. The probability $p$ typically depends on the runtime of $A$, $C$, and $D$, but may also depend on other parameters, such as the number of queries to each oracle made by $C$ or $A$. That is why $p$ takes as arguments the whole algorithms $A$, $C$ and the runtime of $D$. More specifically:

**Property 6** All probabilities computed by CryptoVerif are built from the following components by mathematical operations:

* the runtime of the context plus the attacker;
* the maximum number of oracle calls made by the context or the attacker;

* the value of replication bounds, which is also determined from the number of calls performed by the context or attacker;

* the maximum length of the bitstring represented by a term, in particular a variable; this length may depend on messages computed by the context or the attacker; it is used only for unbounded types; for bounded types, we use the maximum length of the type instead;

* the maximum length of bitstring of a type $T$;

* the length of the result of a function, expressed as a function of the length of its arguments;

* the time of some action, expressed as a function of other elements of the formula;

* probability functions, used in particular to express the probability of breaking each primitive from other elements of the formula;

* the cardinal $|T|$ of a type $T$;

* the probability of collision between two random values of a type $T$, or between a random value and a value independent from that random value; these probabilities depend on the default distribution on the type $D_T$;

* $\epsilon_T$, the distance between the default distribution $D_T$ of type $T$ and the uniform distribution;

* $\epsilon_{find}$, where the distance between $D_{find}(S)$ and the uniform distribution is $\epsilon_{find}/2$.

Among the elements above, the first four depend on the context and the attacker. In particular, probability formulas output by CryptoVerif do not depend on the variable, table, event names in the context. They also do not depend on the values of variables, but may depend on their length. For variables of bounded types, the probabilities do not depend at all on the values. We do not in practice distinguish between the calls of the context or the attacker.

The set of events $\mathcal{E}$ corresponds to events that the adversary is allowed to observe. When $\mathcal{E} = \text{event}(Q, Q')$, we omit it and write $Q \approx_p^{\mathcal{V}, \mathcal{E}} Q'$.

The unusual requirement on variables of $C$ comes from the presence of arrays and of the associated find construct which gives $C$ direct access to variables of $Q$ and $Q'$: the context $C$ is allowed to access variables of $Q$ and $Q'$ only when they are in the finite set of public variables $V$. (In more standard settings, the calculus does not have constructs that allow the context to access variables of $Q$ and $Q'$..) When $V$ is empty, we omit it and write $Q \approx_p^{\mathcal{E}} Q'$.

When $C$ is acceptable for $Q$ with public variables $V$, and we transform $Q$ into $Q'$, we can rename the fresh variables of $Q'$ (introduced by the game transformation) so that they do not occur in $C$. Then $C$ is also acceptable for $Q'$ with public variables $V$. (To establish this property, we use that the variables of $V$ are defined in $Q$ and $Q'$, with the same types, so that, if $C[Q]$ is well-typed, then so is $C[Q']$.)

When $C$ is acceptable for $Q$ with public variables $V$, we have that $\text{vardef}(C) \cap \text{var}(Q) = \emptyset$, because $\text{vardef}(C) \cap \text{var}(Q) = \text{vardef}(C) \cap \text{var}(C) \cap \text{var}(Q) \subseteq \text{vardef}(C) \cap V = \emptyset$.

The following lemma is a straightforward consequence of Definition 5:

**Lemma 19** 1. Reflexivity: $Q \approx_0^{\mathcal{V}, \mathcal{E}} Q$.

2. Symmetry: If $Q \approx_p^{\mathcal{V}, \mathcal{E}} Q'$, then $Q' \approx_p^{\mathcal{V}, \mathcal{E}} Q$.

3. Transitivity: If $Q \approx_p^{\mathcal{V}, \mathcal{E}} Q'$ and $Q' \approx_{p'}^{\mathcal{V}, \mathcal{E}} Q''$, then $Q \approx_{p+p'}^{\mathcal{V}, \mathcal{E}} Q''$.
4. Application of a context: If $Q \approx_p^{V,\mathcal{E}} Q'$ and $C$ is an evaluation context acceptable for $Q$ and $Q'$ with public variables $V$, then $C[Q] \approx_{p'}^{V',\mathcal{E}'} C[Q']$, where $p'(A, C', t_D) = p(A, C'[C[]])$, $V' \subseteq V \cup \text{var}(C)$, and $\mathcal{E}' = \mathcal{E} \cup (\text{event}(C) \setminus \text{event}(Q, Q'))$.

Next, we introduce a notion related to indistinguishability that treats Shoup and non-unique events specially.

**Definition 6 (Property preservation with introduction of events)** Let $Q$ and $Q'$ be two processes and $V$ a set of variables. Assume that $Q$ and $Q'$ satisfy Invariants 1 to 8 with public variables $V$, and the variables of $V$ are defined in $Q$ and $Q'$, with the same types.

Let $D_{\text{false}}(\mathcal{E}v) = \text{false}$ for all $\mathcal{E}v$. Let $\text{NonUnique}_Q = \bigvee\{e \mid [\text{unique}_e] \text{ occurs in } Q\}$ and $\text{NonUnique}_{Q,D} = \bigvee\{e \mid [\text{unique}_e] \text{ occurs in } Q, e \notin D\}$, where $D$ is a distinguisher consisting of a disjunction of Shoup and non-unique events, and we write $e \notin D$ to say that $e$ does not occur in this disjunction. We have $\text{NonUnique}_{Q,D} = \text{NonUnique}_Q \wedge \neg D$.

We write $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, EvUsed \xrightarrow{V} p Q', D', EvUsed'$ when $\mathcal{D}$ is a set of distinguishers, $\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $EvUsed$, $D$ and $D'$ are distinguishers consisting of a disjunction of Shoup and non-unique events, the events that occur in $Q$ or in $D$ are in $EvUsed$, $EvUsed \subseteq EvUsed'$, the events that occur in $Q'$ but not in $Q$ are in $EvUsed'$ but not in $EvUsed$, the events that occur in $D'$ but not in $D$ are in $EvUsed'$ but not in $EvUsed$, and, for all $A \in \mathcal{B}\mathcal{B}$, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $EvUsed'$, all distinguishers $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ that run in time at most $t_{D_0}$, all distinguishers $D_1$ that are disjunctions of events in $\mathcal{D}_{\text{SNU}}$,

$$ \begin{aligned} & \mathrm{Pr}^A[C[Q] : (D_0 \lor D_1 \lor D) \land \neg \mathrm{NonUnique}_{Q,D_1 \lor D}] \\ & \le \mathrm{Pr}^A[C[Q'] : (D_0 \lor D_1 \lor D') \land \neg \mathrm{NonUnique}_{Q',D_1 \lor D'}] + p(A, C, t_{D_0}) \end{aligned} \quad (1) $$

Intuitively, the events $EvUsed$ are those used by CryptoVerif in the sequence of games until the game $Q$ included, while the events $EvUsed'$ are those used until $Q'$. Hence, $EvUsed$ contains the events that occur in $Q$; $EvUsed'$ contains $EvUsed$ and the events that occur in $Q'$. The formula $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ corresponds to the initial query to prove: it is

* a correspondence distinguisher $\neg \varphi$ for a correspondence property (see Section 2.8.3);

* $S$ or $\neg \bar{S}$ for (one-session) secrecy (see Section 2.8.1) and bit secrecy (see Section 2.8.2);

* any distinguisher for indistinguishability;

* $D_{\text{false}}$ when the initial query has already been proved, and only Shoup and non-unique events remain to be proved.

We need to specify precisely the distinguishers needed for the queries we want to prove, because some game transformations of CryptoVerif rely on that. For instance, **simplify** (Section 5.1.21) removes events that are not used by the queries.

The formula $D_1$ is a disjunction of Shoup and non-unique events that remain to be proved, both in $Q$ and in $Q'$. These events are in $\mathcal{D}_{\text{SNU}}$ and in $EvUsed$. The formula $D$ is a disjunction of Shoup and non-unique events that remain to be proved in $Q$, while the formula $D'$ is a disjunction of Shoup and non-unique events that remain to be proved in $Q'$. Hence, the events that occur in $D$ and not in $D'$ are events proved while transforming $Q$ into $Q'$. ("Proving" an event means proving that this event has a negligible probability of occurring, and adding that probability to $p$.) In contrast, the events that occur in $D'$ and not in $D$ are fresh Shoup and non-unique events introduced during the transformation of $Q$ into $Q'$, and that will need to be proved later; hence
these events are in $EvUsed'$ but not in $EvUsed$. More generally, all events that occur in $Q'$ but not in $Q$ are fresh events introduced in the transformation of $Q$ into $Q'$, so they are in $EvUsed'$ but not in $EvUsed$.

When there are no Shoup nor non-unique events, we have $D_1 = D = D' = D_{\text{false}}$ and $\text{NonUnique}_{Q,D_1 \lor D} = \text{NonUnique}_{Q',D_1 \lor D'} = D_{\text{false}}$, so the inequality (1) reduces to

$$ \mathrm{Pr}^{\mathrm{A}}[C[Q] : D_0] \le \mathrm{Pr}^{\mathrm{A}}[C[Q'] : D_0] + p(\mathcal{A}, C, t_{D_0}) $$

Using $\neg D_0$ instead of $D_0$, we obtain

$$ 1 - \mathrm{Pr}^{\mathrm{A}}[C[Q] : D_0] \le 1 - \mathrm{Pr}^{\mathrm{A}}[C[Q'] : D_0] + p(\mathcal{A}, C, t_{D_0}) $$

so by combining the two, $|\mathrm{Pr}^{\mathrm{A}}[C[Q] : D_0] - \mathrm{Pr}^{\mathrm{A}}[C[Q'] : D_0]| \le p(\mathcal{A}, C, t_{D_0})$ as in the definition of indistinguishability. In the general case, the inequality (1) differs from this formula because (1) always counts the traces that execute Shoup and non-unique events that remain to be proved (these traces are always included in the probability by $D_1 \lor D$, resp. $D_1 \lor D'$; the probability of these events needs to be bounded), and never counts the traces that execute proved non-unique events (these traces are excluded by $\neg \text{NonUnique}_{Q,D_1 \lor D}$, resp. $\neg \text{NonUnique}_{Q',D_1 \lor D'}$; the probability of these events has already been bounded). We could also exclude traces that execute proved Shoup events, though it is less essential: Shoup events often simply disappear when they are proved, while non-unique events remain in the game. Excluding traces that execute proved non-unique events allows us to exploit that the corresponding find or get is unique in the transformation from $Q$ to $Q'$: intuitively, the traces in which the find or get is not unique are not counted, so they can be ignored. (Obviously, this point needs to be proved more precisely for each game transformation.)

We need to introduce a distinct event for each $[\text{unique}_e]$ because not all find[unique$_e$] and get[unique$_e$] may be proved unique in the current process and because we need to distinguish the non-unique events that occur in $Q$ from those that occur in the context $C$. (We note that the attacker $\mathcal{A}$ cannot raise events itself.) However, once a $[\text{unique}_e]$ is proved, its name does not matter: all such events are counted in $\text{NonUnique}_{Q,D_1 \lor D}$, and that remains true in future game transformations, since events are never re-added to $D_1$ or $D$. Therefore, we can rename all such events to the same name. So we simply abbreviate $[\text{unique}_e]$ by $[\text{unique}]$ when event $e$ is proved. The context $C$ must not contain the events used in $Q$ or $Q'$ and more generally events in $EvUsed'$.

The formula (1) could also be written

$$ \mathrm{Pr}^{\mathrm{A}}[C[Q] : (D_0 \land \neg \text{NonUnique}_Q) \lor D_1 \lor D] \\ \le \mathrm{Pr}^{\mathrm{A}}[C[Q'] : (D_0 \land \neg \text{NonUnique}_{Q'}) \lor D_1 \lor D'] + p(\mathcal{A}, C, t_{D_0}) $$

since $\text{NonUnique}_{Q,D_1 \lor D} = \text{NonUnique}_Q \land \neg (D_1 \lor D)$. The advantage of the latter formulation is that the dependency in $D_1$, $D$, $D'$ is simpler, which we sometimes exploit in the proofs. However, its drawback is that it is less clear for which events the traces are always counted and for which ones they are never counted, because some events appear both in $\text{NonUnique}_Q$ and in $D_1 \lor D$. That is why we chose formula (1), to make it clear that the traces that execute events in $D_1 \lor D$ are always counted and the traces that execute events in $\text{NonUnique}_{Q,D_1 \lor D}$ are never counted.

When $f$ is a function from sequences of events to sequences of events and $D$ is a distinguisher, we define the distinguisher $D \circ f$ by $(D \circ f)(\mathcal{E}v) = D(f(\mathcal{E}v))$. In particular, when $\sigma$ is a renaming of events, the distinguisher $D \circ \sigma^{-1}$ is defined by $(D \circ \sigma^{-1})(\mathcal{E}v) = D(\sigma^{-1}\mathcal{E}v)$. When $D$ is defined as a logical formula, that corresponds to renaming the events in $D$. For instance, if $D = e_1 \lor \dots \lor e_m$, then $D \circ \sigma^{-1} = \sigma e_1 \lor \dots \lor \sigma e_m$. When $\mathcal{D}$ is a set of distinguishers, $\sigma \mathcal{D} = \{D \circ \sigma^{-1} | D \in \mathcal{D}\}$.

We write $\mathcal{D}_{\neg \mathcal{E}}$ for the set of distinguishers that do not use events in $\mathcal{E}$.
**Lemma 20** 1. Link with indistinguishability:

(a) Suppose that $\mathcal{D}_{\text{SNU}}$ is a set of Shoup events, $D$ is a distinguisher consisting of a disjunction of Shoup events, $Q, Q'$ do not contain non-unique events, the events that occur in $Q, D, D$, or $\mathcal{D}_{\text{SNU}}$ are in $\text{EvUsed}$, and the events that occur in $Q'$ also occur in $Q$. If $Q \approx_p^{V,\mathcal{E}} Q'$, then $D, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} p Q', D, \text{EvUsed}$, for all $D, \mathcal{D}_{\text{SNU}}, D$ such that $\text{event}(D) \cap \text{EvUsed} \subseteq \mathcal{E}, \mathcal{D}_{\text{SNU}} \subseteq \mathcal{E}$, $\text{event}(D) \subseteq \mathcal{E}$.

(b) Suppose that $Q$ and $Q'$ do not contain non-unique events, the events that occur in $Q$ are in $\text{EvUsed}$, and the events that occur in $Q'$ also occur in $Q$. Then $\mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}, \emptyset : Q, D_{\text{false}}, \text{EvUsed} \xrightarrow{V} p Q', D_{\text{false}}, \text{EvUsed}$ if and only if $Q \approx_p^{V,\mathcal{E}} Q'$.

2. Reflexivity: If $\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $\text{EvUsed}$, $D$ is a distinguisher consisting of a disjunction of Shoup and non-unique events, and the events that occur in $Q$ or in $D$ are in $\text{EvUsed}$, then $D, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _0 Q, D, \text{EvUsed}$.

3. Transitivity: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$ and $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q', D', \text{EvUsed}' \xrightarrow{V} _{p'} Q'', D'', \text{EvUsed}'$, then we have $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _{p''} Q'', D'', \text{EvUsed}'$, where $p''(A, C, t_{D_0}) = p(A, C, t_{D_0}) + p'(A, C, t_{D_0})$.

4. Application of a context: If $\mathcal{D}_{-\text{EvUsed}'}$, $\mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$, $\sigma$ is a renaming of the events in $\text{EvUsed}'$ to events not in $\text{EvUsed}^+$, $C$ is a context acceptable for $\sigma Q$ and $\sigma Q'$ with public variables $V$ such that $\text{event}(C) \subseteq \text{EvUsed}^+$, and $\mathcal{D}'_{\text{SNU}}$ is a set of Shoup and non-unique events in $\text{EvUsed}^+$, then we have $\mathcal{D}_{-\sigma\text{EvUsed}'}$, $\sigma\mathcal{D}_{\text{SNU}} \cup \mathcal{D}'_{\text{SNU}} : C[\sigma Q], D \circ \sigma^{-1}, \sigma\text{EvUsed} \cup \text{EvUsed}^+ \xrightarrow{V} _{p'} C[\sigma Q'], D' \circ \sigma^{-1}, \sigma\text{EvUsed}' \cup \text{EvUsed}^+$, where $p'(A, C', t_{D_0}) = p(A, \sigma^{-1}(C'[C[]]), t_{D_0})$, and $V' \subseteq V \cup \text{var}(C)$.

5. Adding distinguishers: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$ and $e \in \mathcal{D}_{\text{SNU}}$, then $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D \lor e, \text{EvUsed} \xrightarrow{V} _p Q', D' \lor e, \text{EvUsed}'$.

6. Removing distinguishers: If $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$, $\mathcal{D}' \subseteq \mathcal{D}$, and $\mathcal{D}'_{\text{SNU}} \subseteq \mathcal{D}_{\text{SNU}}$, then $\mathcal{D}', \mathcal{D}'_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D', \text{EvUsed}'$

**Proof** Property 1a: Given the hypothesis, $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} _p Q', D, \text{EvUsed}$ reduces to: for all attackers $A \in \mathcal{B}\mathcal{B}$, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $\text{EvUsed}$, all distinguishers $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ that run in time at most $t_{D_0}$, and all distinguishers $D_1$ that are disjunctions of events in $\mathcal{D}_{\text{SNU}}$,

$$ \mathrm{Pr}^A[C[Q] : D_0 \lor D_1 \lor D] \le \mathrm{Pr}^A[C[Q'] : D_0 \lor D_1 \lor D] + p(A, C, t_{D_0}) $$

We have $\text{event}(D_0 \lor D_1 \lor D) \cap \text{event}(Q, Q') \subseteq \text{event}(D_0 \lor D_1 \lor D) \cap \text{EvUsed} \subseteq \mathcal{E}$. Moreover, $D_0 \lor D_1 \lor D$ can be implemented in the same time as $D_0$ since evaluating $D_0 \lor D_1 \lor D$ can be done by setting the final result to true as soon as an event in $D_1 \lor D$ is executed, and evaluating $D_0$ otherwise. This does not take more time than evaluating $D_0$. So this inequality is a consequence of $Q \approx_p^{V,\mathcal{E}} Q'$.

Property 1b: Given the hypothesis, $\mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}, \emptyset : Q, D_{\text{false}}, \text{EvUsed} \xrightarrow{V} _p Q', D_{\text{false}}, \text{EvUsed}$ reduces to: for all attackers $A \in \mathcal{B}\mathcal{B}$, for all evaluation contexts $C$ acceptable for $Q$ and $Q'$ with public variables $V$ that do not contain events in $\text{EvUsed}$, and all distinguishers $D_0 \in \mathcal{D}_{-(\text{EvUsed}\setminus\mathcal{E})}$ that run in time at most $t_{D_0}$,

$$ \mathrm{Pr}^A[C[Q] : D_0] \le \mathrm{Pr}^A[C[Q'] : D_0] + p(A, C, t_{D_0}), $$
that is,

$$ \mathrm{Pr}^{\mathcal{A}}[C[Q] : D_0] - \mathrm{Pr}^{\mathcal{A}}[C[Q'] : D_0] \le p(\mathcal{A}, C, t_{D_0}). \quad (2) $$

We have $\mathrm{event}(D_0) \cap \mathrm{event}(Q, Q') \subseteq \mathrm{event}(D_0) \cap \mathrm{EvUsed} \subseteq \mathcal{E}$. Therefore, $Q \approx_p^{V, \mathcal{E}} Q'$ implies $D_{\neg(EvUsed \setminus \mathcal{E})}, \emptyset : Q, D_{\mathrm{false}}, \mathrm{EvUsed} \xrightarrow{V} p Q', D_{\mathrm{false}}, \mathrm{EvUsed}$.

Conversely, assume $D_{\neg(EvUsed \setminus \mathcal{E})}, \emptyset : Q, D_{\mathrm{false}}, \mathrm{EvUsed} \xrightarrow{V} p Q', D_{\mathrm{false}}, \mathrm{EvUsed}$. Let $\mathcal{A} \in \mathcal{BB}$ be an attacker, Let $C$ be an evaluation context $C$ acceptable for $Q$ and $Q'$ with public variables $V$ and $D$ be a distinguisher such that $\mathrm{event}(D) \cap \mathrm{event}(Q, Q') \subseteq \mathcal{E}$. Let $\sigma$ be a renaming of events in $\mathrm{EvUsed}$ to fresh events. Then $\sigma C$ does not contain events in $\mathrm{EvUsed}$. Given a sequence of events $\mathcal{E}$, let $f(\mathcal{E})$ be obtained by removing all events in $\mathrm{EvUsed} \setminus \mathcal{E}$ from $\mathcal{E}$ and, in the remaining sequence, renaming the events $e$ in $\sigma \mathrm{EvUsed}$ to $\sigma^{-1}(e)$. Let $D_0 = D \circ f$. By construction, $D_0 \in D_{\neg(EvUsed \setminus \mathcal{E})}$. So by (2), we get

$$ \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q] : D_0] - \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q'] : D_0] \le p(\mathcal{A}, C, t_{D_0}). $$

Since $\neg D_0 \in D_{\neg(EvUsed \setminus \mathcal{E})}$ and runs in the same time as $D_0$,

$$ 1 - \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q] : D_0] - 1 + \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q'] : D_0] \le p(\mathcal{A}, C, t_{D_0}) $$

so

$$ | \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q] : D_0] - \mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q'] : D_0] | \le p(\mathcal{A}, C, t_{D_0}). $$

Furthermore, each trace of $(\sigma C)[Q]$ with sequence of events $\mathcal{E}$ corresponds to a trace of $C[Q]$ with the same probability and a sequence of events $\mathcal{E}'$ equal to $f(\mathcal{E})$ plus some events not used by $D$, so $D_0(\mathcal{E}) = D(f(\mathcal{E})) = D(\mathcal{E}'')$. Indeed, in a trace of $(\sigma C)[Q]$, if an event $e(\dots)$ is executed in $Q$, then it is executed by $C[Q]$ as well. If it is in $\mathcal{E}$, then it is left unchanged by $f$. If it is not in $\mathcal{E}$, then it is in event($Q$) $\setminus \mathcal{E} \subseteq \mathrm{EvUsed} \setminus \mathcal{E}$, so it is removed by $f$; furthermore, this event is not used by $D$ since event($D$) $\cap$ event($Q$) $\subseteq \mathcal{E}$. If an event $e(\dots)$ is executed in $\sigma C$, then either $e \in \sigma \mathrm{EvUsed}$, $e'(\dots)$ is executed by $C[Q]$ with $e' = \sigma^{-1}(e)$, and $f$ maps $e$ to $e'$; or $e \notin \sigma \mathrm{EvUsed}$, $e \notin \mathrm{EvUsed}$, $e(\dots)$ is executed by $C[Q]$, and $f$ leaves $e$ unchanged. Therefore, $\mathrm{Pr}^{\mathcal{A}}[(\sigma C)[Q] : D_0] = \mathrm{Pr}^{\mathcal{A}}[C[Q] : D]$. We have a similar situation for $Q'$ instead of $Q$, and $D$ can be implemented in the same time as $D_0$, so

$$ | \mathrm{Pr}^{\mathcal{A}}[C[Q] : D] - \mathrm{Pr}^{\mathcal{A}}[C[Q'] : D] | \le p(\mathcal{A}, C, t_D) $$

so $Q \approx_p^{V, \mathcal{E}} Q'$.

Property 2: Obvious.

Property 3: The events in $Q$ or $D$ are in $\mathrm{EvUsed}$. We have $\mathrm{EvUsed} \subseteq \mathrm{EvUsed}' \subseteq \mathrm{EvUsed}''$. The events that occur in $Q''$ but not in $Q$ occur either in $Q''$ but not in $Q'$ or in $Q'$ but not in $Q$; in the former case, they are in $\mathrm{EvUsed}'' \setminus \mathrm{EvUsed}'$; in the latter case, they are in $\mathrm{EvUsed}' \setminus \mathrm{EvUsed}$; so in both cases they are in $\mathrm{EvUsed}'' \setminus \mathrm{EvUsed}$. The same reasoning applies for the events that occur in $D''$ but not in $D$.

Let $\mathcal{A} \in \mathcal{BB}$ be an attacker, $C$ be any evaluation context acceptable for $Q$ and $Q''$ with public variables $V$ that does not contain events in $\mathrm{EvUsed}''$. After renaming the variables of $C$ that do not occur in $Q$ and $Q''$ and the tables of $C$ that do not occur in $Q$ and $Q''$ so that they do not occur in $Q'$, $C$ is also acceptable for $Q'$ with public variables $V$. Furthermore, by Property 6, this renaming does not change the probabilities. Since $\mathrm{EvUsed}' \subseteq \mathrm{EvUsed}''$, $C$ does not contain events in $\mathrm{EvUsed}'$.
Let $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$ that runs in time at most $t_{D_0}$. Let $D_1$ be a disjunction of events of $\mathcal{D}_{\text{SNU}}$. Then we have:

$$
\begin{align*}
& \Pr^{\mathcal{A}}[C[Q] : (D_0 \lor D_1 \lor D)] \land \neg \text{NonUnique}_{Q, D_1 \lor D} \\
\le {} & \Pr^{\mathcal{A}}[C[Q'] : (D_0 \lor D_1 \lor D') \land \neg \text{NonUnique}_{Q', D_1 \lor D'}] + p(\mathcal{A}, C, t_{D_0}) \\
\le {} & \Pr^{\mathcal{A}}[C[Q''] : (D_0 \lor D_1 \lor D'') \land \neg \text{NonUnique}_{Q'', D_1 \lor D''}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C, t_{D_0}) \\
\le {} & \Pr^{\mathcal{A}}[C[Q''] : (D_0 \lor D_1 \lor D'') \land \neg \text{NonUnique}_{Q'', D_1 \lor D''}] + p''(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

by definition of $p''$. Therefore, we have $\mathcal{D}, \mathcal{D}_{\text{SNU}} : Q, D, EvUsed \xrightarrow{V} p'' Q'', D'', EvUsed''$.

Property 4: $\sigma\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $\sigma EvUsed \subseteq \sigma EvUsed \cup EvUsed^+$, so $\sigma\mathcal{D}_{\text{SNU}} \cup \mathcal{D}'_{\text{SNU}}$ is a set of Shoup and non-unique events in $\sigma EvUsed \cup EvUsed^+$. The events that occur in $C[\sigma Q]$ are either in $C$ or in $\sigma Q$; the former case, they are in $EvUsed^+$ by hypothesis; in the latter case, they are also in $\sigma EvUsed$, since the events of $Q$ are in $EvUsed$. So the events that occur in $C[\sigma Q]$ are in $\sigma EvUsed \cup EvUsed^+$. The events in $D \circ \sigma^{-1}$ are in $\sigma EvUsed \subseteq \sigma EvUsed \cup EvUsed^+$. We have $EvUsed \subseteq EvUsed'$, so $\sigma EvUsed \cup EvUsed^+ \subseteq \sigma EvUsed' \cup EvUsed^+$. The events that occur in $C[\sigma Q']$ but not in $C[\sigma Q]$ are in $\sigma Q'$ but not in $\sigma Q$, so they are in $\sigma EvUsed' \setminus \sigma EvUsed$, so in $(\sigma EvUsed' \cup EvUsed^+) \setminus (\sigma EvUsed \cup EvUsed^+)$. Similarly, the events that occur in $D' \circ \sigma^{-1}$ but not in $D \circ \sigma^{-1}$ are in $\sigma EvUsed' \setminus \sigma EvUsed$, so they are in $(\sigma EvUsed' \cup EvUsed^+) \setminus (\sigma EvUsed \cup EvUsed^+)$.

Let $C'$ be any evaluation context acceptable for $C[\sigma Q]$ and $C[\sigma Q']$ with public variables $V'$ that does not contain events in $\sigma EvUsed' \cup EvUsed^+$. We rename the variables of $C'$ not in $V'$ so that they are not in $V$; by Property 6, this renaming does not change the probabilities. Then $\sigma^{-1}(C'[C[]])$ is an evaluation context acceptable for $Q$ and $Q'$ with public variables $V$. Indeed,

$$
\begin{align*}
\mathrm{var}(\sigma^{-1}(C'[C[]])) \cap \mathrm{var}(Q) &= (\mathrm{var}(C') \cup \mathrm{var}(C)) \cap \mathrm{var}(Q) \\
&\subseteq (V' \cup \mathrm{var}(C)) \cap \mathrm{var}(Q) \\
&\qquad \text{since } \mathrm{var}(C') \cap \mathrm{var}(Q) \subseteq \mathrm{var}(C') \cap \mathrm{var}(C[Q]) \subseteq V' \\
&\subseteq (V \cup \mathrm{var}(C)) \cap \mathrm{var}(Q) \\
&\qquad \text{since } V' \subseteq V \cup \mathrm{var}(C) \\
&\subseteq V \\
&\qquad \text{since } \mathrm{var}(C) \cap \mathrm{var}(Q) \subseteq V
\end{align*}
$$

We have similarly $\mathrm{var}(\sigma^{-1}(C'[C[]])) \cap \mathrm{var}(Q') \subseteq V$. We also have $\mathrm{vardef}(\sigma^{-1}(C'[C[]])) \cap V = (\mathrm{vardef}(C') \cap V) \cup (\mathrm{vardef}(C) \cap V) = \emptyset$ since $\mathrm{vardef}(C) \cap V = \emptyset$ because $C$ is an acceptable evaluation context for $\sigma Q$ with public variables $V$ and $\mathrm{vardef}(C') \cap V \subseteq \mathrm{vardef}(C') \cap V' = \emptyset$ because we have renamed the variables of $C'$ not in $V'$ so that they are not in $V$ and $C'$ is an acceptable evaluation context for $C[\sigma Q]$ and with public variables $V'$. Moreover, $C$ and $\sigma Q$ do not use any common table, and $C'$ and $C[\sigma Q]$ do not use any common table so a fortiori $C'$ and $\sigma Q$ do not use any common table. Therefore, $C'[C[]]$ and $\sigma Q$ do not use any common table, so $\sigma^{-1}(C'[C[]])$ and $Q$ do not use any common table. Similarly, $\sigma^{-1}(C'[C[]])$ and $Q'$ do not use any common table. The context $\sigma^{-1}(C'[C[]])$ does not contain events in $EvUsed'$, since $C'$ and $C$ do not contain events in $\sigma EvUsed'$, because $C'$ does not contain events in $\sigma EvUsed' \cup EvUsed^+$ and the events of $C$ are in $EvUsed^+$ which is disjoint from $\sigma EvUsed'$. (The renamings $\sigma$ and $\sigma^{-1}$ are bijections, so for instance $\sigma$ maps the fresh events introduced by $\sigma$ to $EvUsed'$ and $\sigma^{-1}$ maps $EvUsed'$ to the fresh events introduced by $\sigma$.)

By using the property $\mathcal{D}_{\neg EvUsed'}, \mathcal{D}_{\text{SNU}} : Q, D, EvUsed \xrightarrow{V} p' Q', D', EvUsed'$ with the context $\sigma^{-1}(C'[C[]])$, we get for all attackers $A \in \mathcal{BB}$ and for any distinguishers $D_0 \in \mathcal{D}_{\neg EvUsed'} \cup \{D_{\text{false}}\}$
that runs in time $t_{D_0}$ and $D_1$ disjunction of events in $\mathcal{D}_{SNU}$:

$$
\begin{align}
& \Pr^{\mathcal{A}}[\sigma^{-1}C'[\sigma^{-1}C[Q]] : (D_0 \lor D_1 \lor D)] \land \neg \text{NonUnique}_{Q, D_1 \lor D}] \nonumber \\
& \le \Pr^{\mathcal{A}}[\sigma^{-1}C'[\sigma^{-1}C[Q')] : (D_0 \lor D_1 \lor D')] \land \neg \text{NonUnique}_{Q', D_1 \lor D'}] + p(\mathcal{A}, \sigma^{-1}(C'[C[]]), t_{D_0}) \tag{3}
\end{align}
$$

Let $D'_0 \in \mathcal{D}_{\neg\sigma\mathcal{E}v\mathcal{U}s\mathcal{e}d'} \cup \{D_{\mathcal{F}alse}\}$ that runs in time at most $t_{D_0}$, Let $D'_1$ be a disjunction of events in $\sigma\mathcal{D}_{SNU} \cup \mathcal{D}'_{SNU}$. We can write $D'_1$ under the form $D'_1 = D'_2 \lor D'_3$ where $D'_2$ is a disjunction of events in $\sigma\mathcal{D}_{SNU}$ and $D'_3$ is a disjunction of events in $\mathcal{D}'_{SNU}$.

By applying (3) to $D_0 = (D'_0 \circ \sigma \lor D'_3 \circ \sigma) \land \neg \text{NonUnique}_{\sigma^{-1}C, D'_3 \circ \sigma}$, which uses events not in $\mathcal{E}v\mathcal{U}s\mathcal{e}d'$, and to $D_1 = D'_2 \circ \sigma$, we get for all $\mathcal{A} \in \mathcal{B}\mathcal{B}$

$$
\begin{align*}
& \Pr^{\mathcal{A}}[\sigma^{-1}C'[\sigma^{-1}C[Q]] : (((D'_0 \circ \sigma \lor D'_3 \circ \sigma) \land \neg \text{NonUnique}_{\sigma^{-1}C, D'_3 \circ \sigma}) \lor D'_2 \circ \sigma \lor D)] \\
& \quad \land \neg \text{NonUnique}_{Q, D'_2 \circ \sigma \lor D}] \\
& \le \Pr^{\mathcal{A}}[\sigma^{-1}C'[\sigma^{-1}C[Q')] : (((D'_0 \circ \sigma \lor D'_3 \circ \sigma) \land \neg \text{NonUnique}_{\sigma^{-1}C, D'_3 \circ \sigma}) \lor D'_2 \circ \sigma \lor D')] \\
& \quad \land \neg \text{NonUnique}_{Q', D'_2 \circ \sigma \lor D'}] + p(\mathcal{A}, \sigma^{-1}(C'[C[]]), t_{D'_0})
\end{align*}
$$

since $D_0$ can be implemented to run in the same time as $D'_0$. By applying $\sigma$, we have for all $\mathcal{A} \in \mathcal{B}\mathcal{B}$

$$
\begin{align*}
\Pr^{\mathcal{A}}[C'[C[\sigma Q]] : (((D'_0 \lor D'_3) \land \neg \text{NonUnique}_{C,D'_3}) \lor D'_2 \lor D \circ \sigma^{-1})] \land \neg \text{NonUnique}_{\sigma Q, D'_2 \lor D \circ \sigma^{-1}}] \\
\le \Pr^{\mathcal{A}}[C'[C[\sigma Q'}} : (((D'_0 \lor D'_3) \land \neg \text{NonUnique}_{C,D'_3}) \lor D'_2 \lor D' \circ \sigma^{-1})] \\
\quad \land \neg \text{NonUnique}_{\sigma Q', D'_2 \lor D' \circ \sigma^{-1}}] + p(\mathcal{A}, \sigma^{-1}(C'[C[]]), t_{D'_0})
\end{align*}
$$

Since the events of $C$ are in $\mathcal{E}v\mathcal{U}s\mathcal{e}d^+$, the events of $\text{NonUnique}_{C,D'_3}$ are disjoint from those in $(D'_2 \lor D \circ \sigma^{-1})$, so $(\neg \text{NonUnique}_{C,D'_3}) \lor (D'_2 \lor D \circ \sigma^{-1}) = \neg \text{NonUnique}_{C,D'_3}$ and similarly $(\neg \text{NonUnique}_{C,D'_3}) \lor (D'_2 \lor D' \circ \sigma^{-1}) = \neg \text{NonUnique}_{C,D'_3}$. So we have for all $\mathcal{A} \in \mathcal{B}\mathcal{B}$

$$
\begin{align*}
\Pr^{\mathcal{A}}[C'[C[\sigma Q]] : (D'_0 \lor D'_3 \lor D'_2 \lor D \circ \sigma^{-1})] \land \neg \text{NonUnique}_{C,D'_3} \land \neg \text{NonUnique}_{\sigma Q, D'_2 \lor D \circ \sigma^{-1}}] \\
\le \Pr^{\mathcal{A}}[C'[C[\sigma Q'}} : (D'_0 \lor D'_3 \lor D'_2 \lor D' \circ \sigma^{-1})] \land \neg \text{NonUnique}_{C,D'_3} \\
\quad \land \neg \text{NonUnique}_{\sigma Q', D'_2 \lor D' \circ \sigma^{-1}}] + p(\mathcal{A}, \sigma^{-1}(C'[C[]]), t_{D'_0})
\end{align*}
$$

that is

$$
\begin{align*}
\Pr^{\mathcal{A}}[C'[C[\sigma Q]] : (D'_0 \lor D'_1 \lor D \circ \sigma^{-1})] \land \neg \text{NonUnique}_{C[\sigma Q], D'_1 \lor D \circ \sigma^{-1}}] \\
\le \Pr^{\mathcal{A}}[C'[C[\sigma Q'}} : (D'_0 \lor D'_1 \lor D' \circ \sigma^{-1})] \land \neg \text{NonUnique}_{C[\sigma Q'], D'_1 \lor D' \circ \sigma^{-1}}] \\
+ p(\mathcal{A}, \sigma^{-1}(C'[C[]]), t_{D'_0})
\end{align*}
$$

Properties 5 and 6: Obvious.

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

When CryptoVerif transforms a game $G$ into a game $G'$, in most cases, we have $G \approx_p^{V, \mathcal{E}} G'$, where $p$ is the probability difference coming from the transformation, and computed by CryptoVerif, which implies $D, \mathcal{D}_{SNU} : G, D, \mathcal{E}v\mathcal{U}s\mathcal{e}d \xrightarrow{V} p G', D, \mathcal{E}v\mathcal{U}s\mathcal{e}d$, for all $D, \mathcal{D}_{SNU}, D$ such that $\text{event}(D) \cap \mathcal{E}v\mathcal{U}s\mathcal{e}d \subseteq \mathcal{E}$, $\mathcal{D}_{SNU} \subseteq \mathcal{E}$, $\text{event}(D) \subseteq \mathcal{E}$ by Lemma 20, Property 1a. However, there are exceptions to this situation:
* transformations that exploit the uniqueness of find[unique<sub>e</sub>] or get[unique<sub>e</sub>], which are valid only when event e is not executed. These events are taken into account by NonUnique<sub>Q,D</sub>.

* transformations that insert events using Shoup's lemma. This is the case of the transformations insert_event (see Section 5.1.12) and insert (see Section 5.1.13). In this case, we have D, D<sub>SNU</sub>: G, D<sub>false</sub>, EvUsed &rarr; p G', e, EvUsed &cup; {e} where e is the introduced event. The addition of Shoup events may also be combined with the cryptographic transformation of Section 5.2, for example for specifying the decisional Diffie-Hellman assumption. In general, the cryptographic axioms are of the form

$$D_{\neg EvUsed_R}, \emptyset : L, D_{false}, \emptyset \to_p R, D_R, EvUsed_R$$

where L does not contain events, D<sub>R</sub> = V{e | event_abort e occurs in R} and EvUsed<sub>R</sub> = {e that occur in R} (both event_abort e and [unique<sub>e</sub>]). By Lemma 20, Property 4, we infer

$$D_{\neg \sigma EvUsed_R}, D_{SNU}: C[L], D_{false}, EvUsed \xrightarrow{V} p' C[\sigma R], D_R \circ \sigma^{-1}, EvUsed \cup \sigma EvUsed_R$$

where σ is a renaming of the events in EvUsed<sub>R</sub> to events not in EvUsed, C is a context acceptable for L and R such that the events that occur in C are in EvUsed, D<sub>SNU</sub> is a set of Shoup and non-unique events in EvUsed, p'(A, C', t<sub>D<sub>0</sub></sub>) = p(A, σ<sup>-1</sup>(C'[C[]]), t<sub>D<sub>0</sub></sub>), and V ⊆ var(C).

Distinguishers in D<sub>\neg σ EvUsed_R</sub> include distinguishers that use events in EvUsed, in particular distinguishers for correspondences in G, as well as distinguishers in D<sub>\neg (EvUsed &cup; σ EvUsed_R)</sub> used for secrecy and indistinguishability.

* transformations that prove the absence of some events (up to some probability). For such transformations, we have D, D<sub>SNU</sub>: G, e, EvUsed &rarr; p G, D<sub>false</sub>, EvUsed where p is an upper bound of the probability of event e in G. For Shoup events, this generally happens when G does not contain e and p(A, C, t<sub>D<sub>0</sub></sub>) = 0. For non-unique events, p is the probability that the find[unique<sub>e</sub>] or get[unique<sub>e</sub>] yields several possible choices; after this step, the event e is in NonUnique<sub>G,D</sub>, so we can exploit uniqueness of find[unique<sub>e</sub>] or get[unique<sub>e</sub>].

That is why, in general, when CryptoVerif transforms a game G into a game G', we have D, D<sub>SNU</sub>: G, D, EvUsed &rarr; p G', D', EvUsed'.

There are still transformations that do not fit in this framework (guess and guessahan, because they multiply probabilities, as shown in Sections 5.1.17, 5.1.18, and 5.1.19; success simplify because it needs to compensate probabilities of traces that execute S with those that execute S to show soundness for secrecy, as shown in Section 5.1.23).

### 2.8.1 Secrecy

Let us now define the secrecy properties that are proved by CryptoVerif.

**Definition 7 ((One-session) secrecy)** Let Q be an oracle definition, x a variable, and V a set of variables. Let

$$Q_{1-ses.secr.}(x) = O_{s0}() := b \stackrel{R}{\leftarrow} \mathit{bool}; \mathit{return} (); \\ (O_s(u_1 : [1, n_1], \dots, u_m : [1, n_m]) := \mathit{if} \ \mathit{defined}(x[u_1, \dots, u_m]) \ \mathit{then} \\ \qquad \mathit{if} \ b \ \mathit{then} \ \mathit{return} (x[u_1, \dots, u_m]) \ \mathit{else} \ y \stackrel{R}{\leftarrow} T; \mathit{return} (y)$$

Inria
$|O'_s(b' : bool) := \text{if } b = b' \text{ then event_abort S else event_abort } \bar{S})$

$Q_{\text{Secrecy}(x)} = O_{s0}() := b \stackrel{R}{\leftarrow} \text{bool; return } ();$
(foreach $i_s \le n_s$ do $O_s[i_s](u_1 : [1, n_1], \dots, u_m : [1, n_m]) :=$
if defined($x[u_1, \dots, u_m]$) then
if $b$ then return ($x[u_1, \dots, u_m]$) else
find $u'_s = i'_s \le n_s$ such that $\text{defined}(y[i'_s], u_1[i'_s], \dots, u_m[i'_s]) \land$
$u_1[i'_s] = u_1 \land \dots \land u_m[i'_s] = u_m$
then return ($y[u'_s]$)
else $y \stackrel{R}{\leftarrow} T$; return ($y$)
$|O'_s(b' : bool) := \text{if } b = b' \text{ then event_abort S else event_abort } \bar{S})$

where $O_{s0}, O_s, O'_s \notin \text{fo}(Q), u_1, \dots, u_m, u'_s, y, b, b' \notin \text{var}(Q) \cup V$, $S, \bar{S}$ do not occur in $Q$, and $\mathcal{E}(x) = [1, n_1] \times \dots \times [1, n_m] \to T$.

Let sp be 1-ses.secr.(x) (one-session secrecy of x) or Secrecy(x) (secrecy of x). The events used by sp are S and $\bar{S}$. Let $C_{sp} = [] | Q_{sp}$.

Let $C$ be an evaluation context acceptable for $C_{sp}[Q]$ with public variables $V$ ($x \notin V$) that does not contain the events used by sp, and $A \in \mathcal{B}\mathcal{B}$ be an attacker. The advantage of the adversary $A, C$ against sp in process $Q$ is

$$ \text{Adv}_Q^{sp}(A, C) = \text{Pr}^A[C[C_{sp}[Q]] : \mathcal{S}] - \text{Pr}^A[C[C_{sp}[Q]] : \bar{\mathcal{S}}] $$

The process $Q$ satisfies sp with public variables $V$ ($x \notin V$) up to probability $p$ when, for all attackers $A \in \mathcal{B}\mathcal{B}$, for all evaluation contexts $C$ acceptable for $C_{sp}[Q]$ with public variables $V$ that do not contain the events used by sp, $\text{Adv}_Q^{sp}(A, C) \le p(A, C)$.

Intuitively, when $Q$ satisfies sp, the adversary cannot guess the random bit $b$, that is, it cannot distinguish whether the test oracle $Q_{sp}$ returns the value of the secret ($b$ = true) or a random number ($b$ = false).

For one-session secrecy, the adversary performs a single test query, modeled by $Q_{1-ses.secr.}(x)$. In more detail, in $Q_{1-ses.secr.}(x)$, we choose a random bit $b$; the adversary queries oracle $O_s$ with the indices $(u_1, \dots, u_m)$ to perform a test query on $x[u_1, \dots, u_m]:$ if $b$ = true, the test query returns $x[u_1, \dots, u_m]$; if $b$ = false, it returns a random value $y$. Finally, the adversary should guess the bit $b$: it calls oracle $O'_s$ with its guess $b'$ and, if the guess is correct, then event $S$ is executed, and otherwise, event $\bar{S}$ is executed. The probability of getting some information on the secret is the difference between the probability of $S$ and the probability of $\bar{S}$. (When the adversary always calls oracle $O'_s$, we have $\text{Pr}^A[C[C_{sp}[Q]] : \bar{S}] = 1 - \text{Pr}^A[C[C_{sp}[Q]] : S]$, so the advantage of the adversary is $\text{Adv}_Q^{sp}(A, C) = \text{Pr}^A[C[C_{sp}[Q]] : S] - \text{Pr}^A[C[C_{sp}[Q]] : \bar{S}] = 2\text{Pr}^A[C[C_{sp}[Q]] : S] - 1$, which is a more standard formula. By flipping a coin, the adversary can execute events $S$ and $\bar{S}$ with the same probability, that is why the probability that the adversary really guesses $b$ is the difference between the probability of these two events. We need not take the absolute value of $\text{Pr}^A[C[C_{sp}[Q]] : S] - \text{Pr}^A[C[C_{sp}[Q]] : \bar{S}]$ because, when it is negative, we can obtain the opposite, positive value by considering an adversary that calls $O'_s$ with the guess $\neg b'$ instead of $b'$.)

For secrecy, the adversary can perform several test queries, modeled by $Q_{\text{Secrecy}(x)}$. This corresponds to the “real-or-random” definition of security [4]. (As shown in [4], this notion is stronger than the more standard approach in which the adversary can perform a single test query and some reveal queries, which always reveal $x[u_1, \dots, u_m]$.) The replication bound $n_s$ in $Q_{\text{Secrecy}(x)}$ is chosen large enough so that it does not prevent oracle calls that would otherwise
occur, so $n_s$ does not actually limit the number of test queries. When we return a random value ($b$ = false) and several tests queries are performed on the same indices $u_1, \dots, u_m$, we must return the same random value. That is why, in this case, we look for previous test queries (find $u'_s$...) and return the previous value of $y$ in case a previous test query was performed with the same indices. For different indices $u_1, \dots, u_m$, the returned random values are independent of each other, so the secrecy of $x$ requires that the cells of array $x$ are indistinguishable from independent random values. In contrast, the one-session secrecy of $x$ only requires that all array cells of $x$ are indistinguishable from random values, not that they are independent of each other.

By Invariant 3, the variables defined in conditions of find and in patterns and in conditions of get have no array accesses. Therefore, the definition above applies only to variables $x$ that are not defined in conditions of find nor in patterns nor in conditions of get.

**Lemma 21** Let sp be 1-ses.secr($x$) or Secrecy($x$).

If $Q$ satisfies sp with public variables $V$ up to probability $p$ and $C$ is an acceptable evaluation context for $Q$ with public variables $V$, then for all $V' \subseteq V \cup \text{var}(C)$, $C[Q]$ satisfies sp with public variables $V'$ up to probability $p'$ such that $p'(A, C') = p(A, C'[C])$.

If $Q \stackrel{V \cup \{x\}, \varepsilon}{\approx}_p Q'$ and $Q$ satisfies sp with public variables $V$ up to probability $p'$, then $Q'$ satisfies sp with public variables $V$ up to probability $p''$ such that $p''(A, C) = p'(A, C) + 2 \times p(A, C[C_{sp}[]], t_S)$.

**Proof** Suppose that $Q$ satisfies sp with public variables $V$ ($x \notin V$), $A \in BB$ is an attacker and $C$ is an acceptable evaluation context for $Q$ with public variables $V$. Let $V' \subseteq V \cup \text{var}(C)$. Choose oracles $O_{s0}, O_s, O'_s$, variables $u_1, \dots, u_m, u'_s, y, b, b'$, and events $S, \bar{S}$ such that they do not occur in $C[Q]$. Let $C'$ be an acceptable evaluation context for $C_{sp}[C[Q]]$ with public variables $V'$ that does not contain $S$ nor $\bar{S}$. Then we have

$$ 
\begin{aligned}
\text{Adv}_{C[Q]}^{sp}(A, C') &= \text{Pr}^A[C'[C_{sp}[C[Q]]] : S] - \text{Pr}^A[C'[C_{sp}[C[Q]]] : \bar{S}] \\
&= \text{Pr}^A[C'[C_{sp}[Q]] : S] - \text{Pr}^A[C'[C_{sp}[Q]] : \bar{S}] \\
&\le p(A, C'[C])
\end{aligned}
$$

We can commute the contexts $C$ and $C_{sp}$ because the context $C$ does not bind the oracles of $Q_{sp}$. The context $C'[C]$ is an acceptable evaluation context for $C_{sp}[Q]$ with public variables $V$ that does not contain $S$ nor $\bar{S}$: there is no common table between $C$ and $Q$, and between $C'$ and $C_{sp}[C[Q]]$, so a fortiori between $C'$ and $Q$ and $Q_{sp}$ does not use tables, so there is no common table between $C'[C]$ and $C_{sp}[Q]$; moreover

$$ 
\begin{aligned}
\text{var}(C'[C]) \cap \text{var}(C_{sp}[Q]) \\
&= ((\text{var}(C') \cap \text{var}(C_{sp}[Q])) \cup \text{var}(C)) \cap \text{var}(C_{sp}[Q]) \\
&\subseteq (V' \cup \text{var}(C)) \cap \text{var}(C_{sp}[Q]) && \text{since } \text{var}(C') \cap \text{var}(C_{sp}[C[Q]]) \subseteq V' \\
&\subseteq (V \cup \text{var}(C)) \cap \text{var}(C_{sp}[Q]) && \text{since } V' \subseteq V \cup \text{var}(C) \\
&\subseteq V && \text{since } \text{var}(C) \cap \text{var}(Q) \subseteq V \text{ and } \text{var}(C) \cap \text{var}(Q_{sp}) = \emptyset
\end{aligned}
$$

Suppose that $Q \stackrel{V \cup \{x\}, \varepsilon}{\approx}_p Q'$ and $Q$ satisfies sp with public variables $V$ up to probability $p'$. Let $A \in BB$ be an attacker. Let $C$ be an acceptable evaluation context for $C_{sp}[Q']$ with public
variables $V$ that does not contain $S$ nor $\bar{S}$.

$$
\begin{align*}
\mathrm{Adv}_{Q'}^{sp}(\mathcal{A}, C) &= \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q')] : S] - \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q')] : \bar{S}] \\
&\leq \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q]] : S] - \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q]] : \bar{S}] + \\
&\phantom{\leq} |\mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q')] : S] - \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q]] : S]| + \\
&\phantom{\leq} |\mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q]] : \bar{S}] - \mathrm{Pr}^{\mathcal{A}}[C[C_{sp}[Q')] : \bar{S}]| \\
&\leq p'(\mathcal{A}, C) + 2 \times p(\mathcal{A}, C[C_{sp}[]], t_S)
\end{align*}
$$

since $t_S = t_{\bar{S}}$. Indeed, by renaming the variables and tables of $C$ that do not appear in $Q'$ to variables and tables that also do not occur in $Q$, $C$ is also an acceptable evaluation context for $C_{sp}[Q]$ with public variables $V$. Furthermore, by Property 6, this renaming does not change the probabilities. $\square$

## 2.8.2 Secrecy for a Bit

**Definition 8 (Bit secrecy)** Let $Q$ be a process, $x$ a boolean variable defined under no replication, and $V$ a set of variables. Let

$$Q_{\text{bit secr.}(x)} = O_s''(b' : \text{bool}) := \text{if defined}(x) \text{ then } x = b' \text{ then } \text{event_abort} S \text{ else } \text{event_abort } \bar{S}$$

where $O_s'' \notin \text{fo}(Q)$, $b' \notin \text{var}(Q) \cup V$, $S, \bar{S}$ do not occur in $Q$, and $\mathcal{E}(x) = \text{bool}$.

Let $sp$ be bit secr.($x$) ($\text{bit secrecy of } x$). The events used by $sp$ are $S$ and $\bar{S}$. Let $C_{sp} = [] | Q_{sp}$. The definitions of $\mathrm{Adv}_Q^{sp}(\mathcal{A}, C)$ and "$Q$ satisfies sp" are as in Definition 7.

Intuitively, when $Q$ satisfies sp, the adversary cannot guess the boolean $x$, that is, it cannot distinguish whether $x = \text{true}$ or $x = \text{false}$. The adversary performs a single test query, modeled by $Q_{\text{bit secr.}}(x)$. This definition is simpler than the definition of (one-session) secrecy for $x$, because we do not introduce an additional random bit $b$.

By Invariant 3, the variables defined in conditions of find and in patterns and in conditions of get have no array accesses. Therefore, the definition above applies only to variables $x$ that are not defined in conditions of find nor in patterns nor in conditions of get.

Lemma 21 is also valid when $sp = \text{bit secr.}(x)$, with the same statement and proof.

**Lemma 22** If $b_0$ is a boolean variable defined under no replication and $Q$ preserves the one-session secrecy of $b_0$ with public variables $V$ up to probability $p$, then $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $2p$.

**Proof** Let $\mathcal{A} \in \mathcal{BB}$ be an attacker. Let $C$ be any acceptable evaluation context for $Q$ | $Q_{\text{bit secr.}(b_0)}$ with public variables $V$. Let

$$C' = C[-|O_s''(b'_0 : \text{bool}) := \text{let } () = O_{s0}() \text{ in let } b'_0 : \text{bool} = O_s() \text{ in let } () = O'_s(b'_0 = b''_0) \text{ in yield}].$$

We execute $C'[Q | Q_{\text{1-ses.secr.}(b_0)}]$ with attacker $\mathcal{A}$.

When $b'_0 = b_0$ ($C[Q | Q_{\text{bit secr.}(b_0)}]$ executes $S$),

* if $b = \text{true}$ (probability $1/2$), then $b''_0 = b_0$, so $b' = (b'_0 = b''_0) = \text{true}$ and $S$ is executed with probability $1/2$

* if $b = \text{false}$ (probability $1/2$), then $b''_0$ is random, so

$$-b''_0 = b'_0 \text{ with probability } 1/4, \text{ so } b' = (b'_0 = b''_0) = \text{true} \text{ and } \bar{S} \text{ is executed;}$$
– $b_0'' = \neg b_0'$ with probability 1/4, so $b' = (b_0' = b_0'') = \text{false and } \bar{S}$ is executed.

When $b_0' = \neg b_0$ ($C[Q | Q_{\text{bit secr.}(b_0)}]$ executes $\bar{S}$),

• if $b = \text{true}$ (probability 1/2), then $b_0'' = b_0$, so $b'$ is false and $\bar{S}$ is executed with probability 1/2;

• if $b = \text{false}$ (probability 1/2), then $b_0''$ is random, so

– $b_0'' = b_0'$ with probability 1/4, so $b' = \text{true and } \bar{S}$ is executed;

– $b_0'' = \neg b_0'$ with probability 1/4, so $b' = \text{false and } \bar{S}$ is executed.

So

$$ \Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}] = \frac{3}{4} \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] + \frac{1}{4} \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] $$

$$ \Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}] = \frac{1}{4} \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] + \frac{3}{4} \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] $$

Finally, we obtain

$$ \begin{aligned} \Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}] - \Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}] \\ = \frac{1}{2}(\Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] - \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}]) \end{aligned} $$

so $\Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] - \Pr^A[C[Q | Q_{\text{bit secr.}(b_0)}] : \bar{S}] = 2(\Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}] - \Pr^A[C'[Q | Q_{1-\text{ses.secr.}(b_0)}] : \bar{S}]) \le 2p(\mathcal{A}, C') = 2p(\mathcal{A}, \mathcal{C})$, neglecting the additional runtime of $C'$. $\square$

Intuitively, the factor 2 is necessary, because in the definition of one-session secrecy, even if the adversary knows the secret bit $b_0$ perfectly, it will not be able to distinguish $b_0$ from the random bit $y$ in half of the cases, because $b_0$ and $y$ have the same value.

In the rest of Section 2.8.2, we consider a process

$$ Q = O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return } Q' $$

and let $Q_L = Q'\{\text{true}/b_0\}$ and $Q_R = Q'\{\text{false}/b_0\}$, so that $Q$ chooses a random bit $b_0$ and runs as $Q_L$ when $b_0$ is true and as $Q_R$ when $b_0$ is false. We assume that $Q_L$ and $Q_R$ never abort, that is, they contain neither `event_abort` nor `find[unique_e]`. Moreover, they do not use the variable $b_0$. We have the following lemmas.

**Lemma 23** We assume that attackers in $\mathcal{B}\mathcal{B}$ can at least represent probabilistic Turing machines. If $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then $Q_L \approx_{p'}^{V, \emptyset} Q_R$ where $p'(\mathcal{A}, \mathcal{C}, t_D) = p(\mathcal{A} + C + t_D, C_V)$ for some attacker $\mathcal{A} + C + t_D$ and context $C_V$ such that the attacker $\mathcal{A} + C + t_D$ with context $C_V$ runs in time $t_A + t_C + t_D$ and its other parameters (replication bounds, lengths of bitstrings) are the same as for $\mathcal{A}$ plus $\mathcal{C}$.

The processes $Q_L$ and $Q_R$ can execute different events without breaking the bit secrecy of $b_0$, because the adversary for the bit secrecy of $b_0$ does not have access to the events executed by $Q$. Hence, $Q_L \approx_{p'}^V Q_R$ would not hold in general.
**Proof** Let $\mathcal{A} \in \mathcal{BB}$ be an attacker. Let $C$ be any acceptable evaluation context for $Q_L$ and $Q_R$ with public variables $V$, and $D$ a distinguisher such that $\text{event}(D) \cap \text{event}(Q_L, Q_R) = \emptyset$. Let $O$ and $O_s''$ be oracles that $C$ does not use.

Let $\mathcal{A}'$ be an attacker that calls oracle $O$, runs $\mathcal{A}$ and $C$ but stores events executed by $C$ in its internal state instead of actually executing events, computes $D$ on the stored sequence of events executed by $C$, stores the result in $b'_0$, and calls $O_s''(b'_0)$. Such an attacker $\mathcal{A}'$ exists because attackers in $\mathcal{BB}$ can at least represent probabilistic Turing machines. However, this attacker needs to be able to access the public variables in $V$. To this end, given a variable $x \in V$ with type $x: [1, n_1] \times \dots \times [1, n_m] \to T$, we define the oracle definition $Q_x = \text{foreach } i \le n \text{ do } O_x(u_1: [1, n_1], \dots, u_m: [1, n_m]) := \text{if defined}(x[u_1, \dots, u_m]) \text{ then return } (x[u_1, \dots, u_m]),$ with $n$ large enough so that it does not limit the number of queries that the attacker makes. Given a set of public variables $V = \{v_1, \dots, v_m\}$, we then define the context $C_V = Q_{v_1} | \dots | Q_{v_m} | []$. Whenever $\mathcal{A}'$ executes a part of $C$ that depends on some public variable, it uses the corresponding oracle to obtain the values inside the array. With such a construction, and without going into any formal details, the runtime of $t_A + t_C + t_D$ is roughly equal to the runtime of $t_{A'} + t_{C'}$. To formalize this statement, some care would need to be taken on how $\mathcal{A}'$ can simulate the find constructs of $C$ by going through the full array by making many queries to oracles in $C_V$.

When $b_0$ is true, $Q | Q_{\text{bit secr.}(x)}$ run with attacker $\mathcal{A}'$ and context $C_V$ stores in $b'_0$ the result of $C[Q_L]:D$ run with attacker $\mathcal{A}$. When $b'_0 = \text{true}$, $S$ is executed. When $b'_0 = \text{false}$, $\bar{S}$ is executed. So

$$ \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: S/b_0 = \text{true}] = \Pr^{\mathcal{A}}[C[Q_L]: D] $$

$$ \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: \bar{S}/b_0 = \text{true}] = 1 - \Pr^{\mathcal{A}}[C[Q_L]: D] $$

When $b_0$ is false, $Q | Q_{\text{bit secr.}(x)}$ run with attacker $\mathcal{A}'$ and context $C_V$ stores in $b'_0$ the result of $C[Q_R]:D$ run with attacker $\mathcal{A}$. When $b'_0 = \text{true}$, $\bar{S}$ is executed. When $b'_0 = \text{false}$, $S$ is executed. So

$$ \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: S/b_0 = \text{false}] = 1 - \Pr^{\mathcal{A}}[C[Q_R]: D] $$

$$ \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: \bar{S}/b_0 = \text{false}] = \Pr^{\mathcal{A}}[C[Q_R]: D] $$

Finally, we obtain

$$ \begin{aligned} & \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: S] - \Pr^{\mathcal{A}'}[C_V[Q | Q_{\text{bit secr.}(x)}]: \bar{S}] \\ &= \frac{1}{2}(\Pr[C[Q_L]: D] + 1 - \Pr^{\mathcal{A}}[C[Q_R]: D] - (1 - \Pr^{\mathcal{A}}[C[Q_L]: D]) - \Pr^{\mathcal{A}}[C[Q_R]: D]) \\ &= \Pr^{\mathcal{A}}[C[Q_L]: D] - \Pr^{\mathcal{A}}[C[Q_R]: D] \end{aligned} $$

so $\Pr^{\mathcal{A}}[C[Q_L]: D] - \Pr^{\mathcal{A}}[C[Q_R]: D] \le p'(\mathcal{A}, C, t_D)$. By negating the bit $b'_0$, we swap the events $S$ and $\bar{S}$ without changing the probability, so $\Pr^{\mathcal{A}}[C[Q_R]: D] - \Pr^{\mathcal{A}}[C[Q_L]: D] \le p'(\mathcal{A}, C, t_D)$. Therefore, $|\Pr^{\mathcal{A}}[C[Q_L]: D] - \Pr^{\mathcal{A}}[C[Q_R]: D]| \le p'(\mathcal{A}, C, t_D)$. So $Q_L \approx_{p'}^{V, \emptyset} Q_R$. $\square$

Lemma 23 is the main motivation for the notion of secrecy for a bit: it allows proving indistinguishability between two processes by showing secrecy of bit $b_0$. Using this notion instead of one-session secrecy of $b_0$ avoids losing a factor 2, as shown by Lemma 22.

We use this idea to encode the diff construct originally introduced in ProVerif [30]: given a process $Q_1$ that contains terms $\text{diff}[M, M']$ and processes $\text{diff}[P, P']$, we define $\text{fst}(Q_1)$ as $Q_1$ with $\text{diff}[M, M']$ replaced with $M$ and $\text{snd}(Q_1)$ as $Q_1$ with $\text{diff}[M, M']$ replaced with $M'$, and similarly for $\text{diff}[P, P']$; the goal is to show that $\text{fst}(Q_1) \approx_{p'}^{V, \emptyset} \text{snd}(Q_1)$ for some $p$ and determine
p. In order to do that, we define $Q'$ as $Q_1$ with $\text{diff}[M, M']$ replaced with $\text{if\_fun}(b_0, M, M')$ when $M$ and $M'$ are simple and with if $b_0$ then $M$ else $M'$ otherwise<fnref n="1" />, $\text{diff}[P, P']$ replaced with if $b_0$ then $P$ else $P'$, and $Q = O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q'$. We have $Q_L = Q'\{\text{true}/b_0\} \approx_0^{V,\emptyset} \text{fst}(Q_1)$ and $Q_R = Q'\{\text{false}/b_0\} \approx_0^{V,\emptyset} \text{snd}(Q_1)$, so by Lemma 23, if $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then $\text{fst}(Q_1) \approx_{p'}^{V,\emptyset} \text{snd}(Q_1)$ where $p'(A, C, t_D) = p(A + C + t_D, C_V)$.

**Lemma 24** If $Q_L \approx_p^{V,\emptyset} Q_R$ then $Q \stackrel{V \cup \{b_0\},\emptyset}{\approx_{p/2}} O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R$.

**Proof** Let $A \in \mathcal{B}\mathcal{B}$ be an attacker. Let $C$ be an evaluation context acceptable for $Q$ and $O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R$ with public variables $V \cup \{b_0\}$ and $D$ be a distinguisher. We have

$$ 
\begin{aligned}
& | \Pr^A[C[Q] : D] - \Pr^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R] : D| \\
& \le \frac{1}{2} | \Pr^A[C[Q] : D/b_0 = \text{true}] - \Pr^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R] : D/b_0 = \text{true}]| \\
& \quad + \frac{1}{2} | \Pr^A[C[Q] : D/b_0 = \text{false}] - \Pr^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R] : D/b_0 = \text{false}]| \\
& \le \frac{1}{2} | \Pr^A[C[O() := \text{let } b_0 = \text{true in return} (); Q_L] : D| \\
& \quad - \Pr^A[C[O() := \text{let } b_0 = \text{true in return} (); Q_R] : D]| \\
& \le \frac{1}{2} p(A, C, t_D)
\end{aligned}
$$

Indeed, $\Pr^A[C[O() := \text{let } b_0 = \text{true in return} (); Q_L] : D] = \Pr^A[C''[Q_L] : D]$ (and similarly for $Q_R$), where $C'' = C[\text{newOracle } \tilde{O}'; (F_{\tilde{O},\tilde{O}'} | \text{newOracle } \tilde{O}; (O() := \text{let } b_0 = \text{true in return} (); F_{\tilde{O}',\tilde{O}}) | []])$, $\tilde{O}$ are the oracles at the root of $Q_L$ and $Q_R$ (they are not used elsewhere by Invariant 7), $\tilde{O}'$ are fresh oracles corresponding to oracles in $\tilde{O}$, and $F_{\tilde{O}',\tilde{O}}$ forwards all oracle calls on an oracle in $\tilde{O}'$ to the corresponding oracle in $\tilde{O}$, with the same replication bounds as in $Q_L$ and $Q_R$. (All calls to oracles in $\tilde{O}$ are forwarded to oracles in $\tilde{O}'$ and then back to oracles in $\tilde{O}$ provided the code $O() := \text{let } b_0 = \text{true in return} ()$ has already been executed. That prevents executing $Q_L$ or $Q_R$ before $O() := \text{let } b_0 = \text{true in return} ()$. By Property 6, replacing $C''$ with $C$ as argument of $p(C, t_D)$ does not affect the probability. (We neglect the additional runtime of $C''$.) $\square$

Lemma 25 is the converse of Lemma 23.

**Lemma 25** If $Q_L \approx_p^{V,\emptyset} Q_R$, then $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p'$ where $p'(A, C) = p(A, C[C_{\text{bit secr.}(b_0)}], t_S)$.

**Proof** If $Q_L \approx_p^{V,\emptyset} Q_R$, then by Lemma 24, $Q \approx_{p/2}^{V \cup \{b_0\},\emptyset} O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R$. Moreover, $O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability 0. (Since $Q_R$ does not use $b_0$, the variable $b'$ in $Q_{\text{bit secr.}(b_0)}$ is independent of $b_0$, so a trace that executes $S$ corresponds to a trace of the same probability and that executes $\tilde{S}$ by changing the value of $b_0$, so $\Pr^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return} (); Q_R | Q_{\text{bit secr.}(b_0)}] : S] =$

<footnote n="1">¹if\_fun($b_0, M, M'$) differs from if $b_0$ then $M$ else $M'$ in that it evaluates both $M$ and $M'$. Since $\text{diff}[M, M']$ evaluates either $M$ or $M'$ but not both, we translate it into if $b_0$ then $M$ else $M'$ when the evaluation of $M$ or $M'$ may modify the semantic state, e.g. by executing an event or by defining a variable. The evaluation of simple terms does not modify the semantic state.</footnote>
Pr<sup>A</sup>[C[O() := b<sub>0</sub> <sub><i>R</i></sub> bool; return (); Q<sub>R</sub> | Q<sub>bit secr.(b<sub>0</sub>)</sub>] : S&#773;].) So by Lemma 21 (version for bit secrecy), Q preserves the bit secrecy of b<sub>0</sub> with public variables V up to probability p'. □

Lemma 26 provides a converse of Lemma 22 when Q has the particular form given above.
There is no probability loss in this case.

**Lemma 26** *We assume that attackers in BB can at least represent probabilistic Turing machines. If Q preserves the bit secrecy of b<sub>0</sub> with public variables V up to probability p, then Q preserves the one-session secrecy of b<sub>0</sub> with public variables V up to probability p.*

**Proof** If $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then by Lemma 23, $Q_L \stackrel{V,\emptyset}{\approx}_{p'} Q_R$ where $p'(A, C, t_D) = p(A + C + t_D, C_V)$. By Lemma 24, $Q \stackrel{V \cup \{b_0\}, \emptyset}{\approx}_{p'/2} O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return()}; Q_R$.

Moreover, $O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return()}; Q_R$ preserves the one-session secrecy of $b_0$ with public variables $V$ up to probability 0. Indeed, since $Q_R$ does not use $b_0$, $b_0$ can in fact be chosen in the test query in $Q_{1-ses.secr.}(b_0)$, so that test query always returns a random boolean, independently of the value of the variable $b$ of $Q_{1-ses.secr.}(b_0)$. Therefore, the variable $b'$ is independent of $b$, so a trace that executes $S$ corresponds to a trace of the same probability and that executes $\bar{S}$ by changing the value of $b$, so $\text{Pr}^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return()}; Q_R | Q_{1-ses.secr.}(b_0)] : \bar{S}] = \text{Pr}^A[C[O() := b_0 \stackrel{R}{\leftarrow} \text{bool; return()}; Q_R | Q_{1-ses.secr.}(b_0)] : \bar{S}]$.

So by Lemma 21 (version for one-session secrecy), $Q$ preserves the one-session secrecy of $b_0$ with public variables $V$ up to probability $p''$ such that $p''(A, C) = p'(A, C[C_{1-ses.secr.}(b_0)], t_S) = p(A + C[C_{1-ses.secr.}(b_0)] + t_S, C_V)$ which is about $p(A, C)$ by Property 6, neglecting the additional runtime of the context. □

### 2.8.3 Correspondences

In this section, we define non-injective and injective correspondences.

**Non-injective Correspondences** A non-injective correspondence is a property of the form "if some events have been executed, then some other events have been executed at least once". Here, we generalize these correspondences to implications between logical formulas $\psi \Rightarrow \phi$, which may contain events. We use the following logical formulas:

$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l}
\phi ::= & \multicolumn{2}{l}{\text{formula}} \\
M & \multicolumn{2}{l}{\text{term}} \\
event(e(M_1, \dots, M_m)) & \multicolumn{2}{l}{\text{event}} \\
\phi_1 \wedge \phi_2 & \multicolumn{2}{l}{\text{conjunction}} \\
\phi_1 \vee \phi_2 & \multicolumn{2}{l}{\text{disjunction}}
\end{array}
$$

Terms $M, M_1, \dots, M_m$ in formulas must contain only variables $x$ without array indices and function applications, and their variables are assumed to be distinct from variables of processes. Formulas denoted by $\psi$ are conjunctions of events. In a correspondence $\psi \Rightarrow \phi$, the variables of $\psi$ are universally quantified; those of $\phi$ that do not occur in $\psi$ are existentially quantified. Formally:

**Definition 9** The semantics of the correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, also written $\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'; \psi \Rightarrow \phi$ in a less explicit syntax, is $[\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi] = [\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'; \psi \Rightarrow \phi] = \forall \tilde{x} \in \tilde{T}, (\psi \Rightarrow \exists \tilde{y} \in \tilde{T}', \phi)$, where $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$.
The formula $M$ holds when $M$ evaluates to true. The formula $\mathbf{event}(e(M_1, \dots, M_n))$ holds when the event $e(M_1, \dots, M_n)$ has been executed. Conjunction, disjunction, implication, existential and universal quantifications are defined as usual. More formally, we write $\rho, \mathcal{E}v \vdash \varphi$ when the sequence of events $\mathcal{E}v$ satisfies the formula $\varphi$, in the environment $\rho$ that maps variables to their values. We define $\rho, \mathcal{E}v \vdash \varphi$ as follows:

$\rho, \mathcal{E}v \vdash M$ if and only if $\rho, M \Downarrow$ true
$\rho, \mathcal{E}v \vdash \mathbf{event}(e(M_1, \dots, M_m))$ if and only if
  for all $j \le m$, $\rho, M_j \Downarrow a_j$ and $e(a_1, \dots, a_m) \in \mathcal{E}v$
$\rho, \mathcal{E}v \vdash \varphi_1 \wedge \varphi_2$ if and only if $\rho, \mathcal{E}v \vdash \varphi_1$ and $\rho, \mathcal{E}v \vdash \varphi_2$
$\rho, \mathcal{E}v \vdash \varphi_1 \vee \varphi_2$ if and only if $\rho, \mathcal{E}v \vdash \varphi_1$ or $\rho, \mathcal{E}v \vdash \varphi_2$
$\rho, \mathcal{E}v \vdash \varphi_1 \Rightarrow \varphi_2$ if and only if $\rho, \mathcal{E}v \vdash \varphi_1$ implies $\rho, \mathcal{E}v \vdash \varphi_2$
$\rho, \mathcal{E}v \vdash \exists x \in T, \varphi$ if and only if there exists $a \in T$ such that $\rho[x \mapsto a], \mathcal{E}v \vdash \varphi$
$\rho, \mathcal{E}v \vdash \forall x \in T, \varphi$ if and only if for every $a \in T$, we have $\rho[x \mapsto a], \mathcal{E}v \vdash \varphi$

When $\varphi$ is a closed formula, we write $\mathcal{E}v \vdash \varphi$ for $\rho, \mathcal{E}v \vdash \varphi$ where $\rho$ is the empty function.

**Definition 10** The sequence of events $\mathcal{E}v$ satisfies the correspondence $\varphi$ if and only if $\mathcal{E}v \vdash \varphi$.

**Definition 11** We define a distinguisher $D(\mathcal{E}v) = \text{true if and only if } \mathcal{E}v \vdash \varphi$, and we denote this distinguisher $D$ simply by $\varphi$.

The advantage of the adversary $A, C$ against the correspondence $\varphi$ in process $Q$ is $\mathbf{Adv}_Q^\varphi(A, C) = \text{Pr}^A[C[Q] : \neg\varphi]$, where $C$ is an evaluation context acceptable for $Q$ with any public variables that does not contain events used by $\varphi$.

The process $Q$ satisfies the correspondence $\varphi$ with public variables $V$ up to probability $p$ if and only if for all evaluation contexts $C$ acceptable for $Q$ with public variables $V$ that do not contain events used by $\varphi$ and all $A \in \mathcal{BB}$, $\mathbf{Adv}_Q^\varphi(A, C) \le p(A, C)$.

When $sp$ is a correspondence $\varphi$, we define $C_{sp} = []$ and the events used by $sp$ are the events that occur in the formula $\varphi$. Therefore, the definition of "$Q$ satisfies the correspondence $\varphi$" matches the definition of "$Q$ satisfies $sp$" given in Definition 7.

A process satisfies $\varphi$ up to probability $p$ when the probability that it generates a sequence of events $\mathcal{E}v$ that does not satisfy $\varphi$ is at most $p(A, C)$, in the presence of an adversary represented by the attacker $A$ and the context $C$.

**Example 2** The semantics of the correspondence

$$ \forall x : pkey, y : host, z : nonce; \mathbf{event}(e_B(x, y, z)) \Rightarrow \mathbf{event}(e_A(x, y, z)) \quad (4) $$

is

$$ \forall x \in pkey, \forall y \in host, \forall z \in nonce, \mathbf{event}(e_B(x, y, z)) \Rightarrow \mathbf{event}(e_A(x, y, z)) \quad (5) $$

It means that, with overwhelming probability, for all $x, y, z$, if $e_B(x, y, z)$ has been executed, then $e_A(x, y, z)$ has been executed.

The semantics of the correspondence

$$ \begin{aligned} \forall x : T; & \mathbf{event}(e_1(x)) \wedge \mathbf{event}(e_2(x)) \Rightarrow \\ & \exists y : T'; \mathbf{event}(e_3(x)) \vee (\mathbf{event}(e_4(x, y)) \wedge \mathbf{event}(e_5(x, y))) \end{aligned} $$

is

$$ \begin{aligned} \forall x \in T, & \mathbf{event}(e_1(x)) \wedge \mathbf{event}(e_2(x)) \Rightarrow \\ & \exists y \in T', \mathbf{event}(e_3(x)) \vee (\mathbf{event}(e_4(x, y)) \wedge \mathbf{event}(e_5(x, y))) \end{aligned} $$
It means that, with overwhelming probability, for all $x$, if $e_1(x)$ and $e_2(x)$ have been executed, then $e_3(x)$ has been executed or there exists $y$ such that both $e_4(x, y)$ and $e_5(x, y)$ have been executed.

**Injective Correspondences**

Injective correspondences are properties of the form “if some event has been executed $n$ times, then some other events have been executed at least $n$ times”. In order to model them in our logical formulas, we extend the grammar of formulas $\phi$ with injective events `inj-event(e(M_1, ..., M_m))`. The formula $\psi$ is a conjunction of (injective or non-injective) events. The conditions on the number of executions of events apply only to injective events.

The definition of formula satisfaction is also extended, to be able to indicate at which step an event has been executed (that is, at which index it appears in $\mathcal{E}v$): `event(e(\tilde{M}))@\tau` means that event $e(\tilde{M})$ has been executed at step $\tau$. Formally:

$\rho, \mathcal{E}v \vdash \text{event}(e(M_1, \dots, M_m))@M_0$ if and only if
for all $j \le m$, $\rho, M_j \downarrow a_j, a_0 \ne \perp$, and $e(a_1, \dots, a_m) = \mathcal{E}v(a_0)$

With this definition, we have:

**Definition 12** The semantics of the correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, also written $\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'; \psi \Rightarrow \phi$ in a less explicit syntax, is

$$[\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi] = [\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'; \psi \Rightarrow \phi] = \exists f_1, \dots, f_k \in \mathbb{N}^m \times \prod \tilde{T} \to \mathbb{N} \cup \{\perp\}, \\ \text{Inj}(I, f_1) \wedge \dots \wedge \text{Inj}(I, f_k) \wedge \forall \tau_1, \dots, \tau_m \in \mathbb{N}, \forall \tilde{x} \in \tilde{T}, (\psi^\tau \Rightarrow \exists \tilde{y} \in \tilde{T}', \phi^\tau),$$

where $\tilde{x} = \text{var}(\psi)$, $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$, $\psi = F_1 \wedge \dots \wedge F_m$, $\psi^\tau = F_1^\tau \wedge \dots \wedge F_m^\tau$, $F_j^\tau = \text{event}(e(\tilde{M}))@\tau_j$ if $F_j = \text{event}(e(\tilde{M}))$ or $F_j = \text{inj-event}(e(\tilde{M}))$, $I = \{j | F_j = \text{inj-event}(\dots)\}$, $\phi^\tau$ is obtained from $\phi$ by replacing each injective event `inj-event(e(\tilde{M}))` with `event(e(\tilde{M}))@f_j(\tau_1, \dots, \tau_m, \tilde{x})$ using a distinct function $f_j$ for each injective event in $\phi^\tau$, and $\text{Inj}(I, f)$ if and only if $f(\tau_1, \dots, \tau_m, \tilde{x}) = f(\tau'_1, \dots, \tau'_m, \tilde{x}') \ne \perp \Rightarrow \forall j \in I, \tau_j = \tau'_j$.

In $\psi^\tau$ and $\phi^\tau$, events are labeled with their associated execution step, $\tau_j$ for the events in $\psi^\tau$ and $f_j(\tau_1, \dots, \tau_m, \tilde{x})$ for the injective events in $\phi^\tau$. Therefore, the functions $f_j$ map the execution steps of events in $\psi, \tau_1, \dots, \tau_m$, and the values of the variables in $\psi, \tilde{x}$, to the associated execution steps of injective events in $\phi$. (The result $\perp$ corresponds to the case in which the event in $\phi$ is not executed: in case of disjunctions, not all events in $\phi$ are required to be executed.) The correspondence is injective when these functions $f_j$ are injective in their arguments that correspond to injective events in $\psi$. The indices of injective events in $\psi$ are collected in the set $I$, and injectivity is guaranteed by $\text{Inj}(I, f_j)$, which means that, ignoring the result $\perp$, $f_j$ is injective in its arguments of indices in $I$.

Definition 11 is unchanged for injective correspondences.

**Example 3** The semantics of the correspondence

$$\forall x : pkey, y : host, z : nonce; \text{inj-event}(e_B(x, y, z)) \Rightarrow \text{inj-event}(e_A(x, y, z)) \quad (6)$$

is

$$\exists f \in \mathbb{N} \times pkey \times host \times nonce \rightarrow \mathbb{N} \cup \{\perp\}, \text{Inj}(\{1\}, f) \wedge \\ \forall \tau \in \mathbb{N}, \forall x \in pkey, \forall y \in host, \forall z \in nonce, \\ \text{event}(e_B(x, y, z))@\tau \Rightarrow \text{event}(e_A(x, y, z))@f(\tau, x, y, z) \quad (7)$$
It means that, with overwhelming probability, each execution of $e_B(x, y, z)$ corresponds to a distinct execution of $e_A(x, y, z)$. In this case, $f$ is a function that maps the execution step $\tau$ of $e_B(x, y, z)$ and the variables $x, y, z$ to the execution step of $e_A(x, y, z)$. (This step is never $\perp$.) This function is injective in its first argument, the step $\tau$, so if there are $n$ executions of $e_B(x, y, z)$, at steps $\tau_1, \dots, \tau_n$, then there are at least $n$ executions of $e_A(x, y, z)$, at steps $f(\tau_1, x, y, z), \dots, f(\tau_n, x, y, z)$ and these steps are distinct by injectivity of $f$ in its first argument.

The semantics of the correspondence

$$ \forall x : T; \mathit{event}(e_1(x)) \wedge \mathit{inj-event}(e_2(x)) \Rightarrow \exists y : T'; \mathit{inj-event}(e_3(x)) \vee \\ (\mathit{inj-event}(e_4(x, y)) \wedge \mathit{inj-event}(e_5(x, y))) $$

is

$$ \exists f_1, f_2, f_3 \in \mathbb{N}^2 \times T \rightarrow \mathbb{N} \cup \{\perp\}, \mathit{Inj}(\{2\}, f_1) \wedge \mathit{Inj}(\{2\}, f_2) \wedge \mathit{Inj}(\{2\}, f_3) \wedge \\ \forall \tau_1, \tau_2 \in \mathbb{N}, \forall x \in T, \mathit{event}(e_1(x))@\tau_1 \wedge \mathit{event}(e_2(x))@\tau_2 \Rightarrow \exists y \in T', \mathit{event}(e_3(x))@f_1(\tau_1, \tau_2, x) \vee \\ (\mathit{event}(e_4(x, y))@f_2(\tau_1, \tau_2, x) \wedge \mathit{event}(e_5(x, y))@f_3(\tau_1, \tau_2, x)) $$

It means that, with overwhelming probability, for all $x$, if $e_1(x)$ has been executed, then each execution of $e_2(x)$ corresponds to distinct executions of $e_3(x)$ or to distinct executions of $e_4(x, y)$ and $e_5(x, y)$. The functions $f_1, f_2$, and $f_3$ map the execution steps $\tau_1$ and $\tau_2$ of $e_1$ and $e_2$ and the variable $x$ to the execution steps of $e_3, e_4$, and $e_5$ respectively. Ignoring the result $\perp$, they are injective in their second argument, which corresponds to the execution step of the injective event $e_2$.

When no injective event occurs in $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, Definition 12 reduces to the definition of non-injective correspondences: there are no functions $f_j, \phi^\tau = \phi$, and $\mathit{event}(e(\tilde{M}))@\tau$ holds for some $\tau$ if and only if $\mathit{event}(e(\tilde{M}))$ holds, so $\psi^\tau$ holds for some $\tau_1, \dots, \tau_m$ if and only if $\psi$ holds.

**Well-formedness condition** When we consider a correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, with $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$, we should have

$$ \forall \tilde{x} \in \tilde{T}, \forall \tilde{x}' \in \tilde{T}, \forall \tilde{y} \in \tilde{T}', \psi = \psi\{\tilde{x}'/\tilde{x}\} \Rightarrow \phi = \phi\{\tilde{x}'/\tilde{x}\} \quad (8) $$

where $\tilde{x}'$ are fresh variables, and the equality of terms is the equality of their values, but dis-junctions, conjunctions, and events are considered syntactically. This condition guarantees that, given an execution of events in $\psi$, the formula to verify $\exists \tilde{y} \in \tilde{T}', \phi^\tau$ is uniquely determined. It avoids pathological correspondences such as

$$ \forall x : T; \mathit{event}(e(f(x)) \Rightarrow \mathit{event}(e'(x))) \quad (9) $$

with $f(a) = f(b) = c$, for which $\mathit{event}(e(c))$ corresponds to both $\mathit{event}(e(f(a)))$ and $\mathit{event}(e(f(b)))$, so when event $e(c)$ is executed, $x$ can take both values $a$ and $b$, so (9) requires the execution of events $e'(a)$ and $e'(b)$. An even more pathological case is when $f(x) = c$ for all $x$: in this case, when event $e(c)$ is executed, (9) requires the execution of event $e'(x)$ for all $x \in T$, which is impossible when $T$ is infinite. However, the condition allows the correspondence (9) when $f$ is injective, so $x$ is uniquely determined, and it also allows the correspondences

$$ \forall x : T; \mathit{event}(e(f(x)) \Rightarrow \mathit{false}) \quad (10) $$

and

$$ \forall x : T; \mathit{event}(e(f(x)) \Rightarrow \mathit{event}(e'(f(x)))) \quad (11) $$
for any function $f$: (10) requires that event $e(y)$ is never executed with $y$ in the image of $f$, and
(11) requires that $e'(y)$ is executed when $e(y)$ is executed with $y$ in the image of $f$.

CryptoVerif displays a warning when it does not manage to prove the well-formedness condition (8).

## Property

**Lemma 27** If $Q$ satisfies a correspondence $\varphi$ with public variables $V$ up to probability $p$ and $C$ is an acceptable evaluation context for $Q$ with public variables $V$ that does not contain events used in $\varphi$, then for all $V' \subseteq V \cup \text{var}(C)$, $C[Q]$ satisfies a correspondence $\varphi$ with public variables $V'$ up to probability $p'$ such that $p'(A, C') = p(A, C'[C])$.

If $Q \approx_p^{V,\mathcal{E}} Q'$, $Q$ satisfies a correspondence $\varphi$ with public variables $V$ up to probability $p'$, and $\mathcal{E}$ contains all events in $\varphi$, then $Q'$ satisfies $\varphi$ with public variables $V$ up to probability $p''$ such that $p''(A, C) = p'(A, C) + p(A, C, t_\varphi)$.

**Proof** Suppose that $Q$ satisfies a correspondence $\varphi$ with public variables $V$, $A \in \mathcal{B}\mathcal{B}$ is an attacker, and $C$ is an acceptable evaluation context for $Q$ with public variables $V$ that does not contain events used in $\varphi$. Let $V' \subseteq V \cup \text{var}(C)$. Let $C'$ be an evaluation context acceptable for $C[Q]$ with public variables $V'$ that does not contain events used by $\varphi$. We rename the variables of $C'$ not in $V'$ so that they are not in $V$; by Property 6, this renaming does not change the probabilities. We have

$$ \text{Adv}_{C[Q]}^{\varphi}(A, C') = \text{Pr}^{\mathcal{A}}[C'[C[Q]] : \neg\varphi] \le p(A, C'[C]) $$

because $C'[C]$ is an evaluation context acceptable for $Q$ with public variables $V$: there is no common table between $C$ and $Q$, and between $C'$ and $C[Q]$, so a fortiori between $C'$ and $Q$, so there is no common table between $C'[C]$ and $Q$; moreover

$$
\begin{align*}
\text{var}(C'[C]) \cap \text{var}(Q) &= ((\text{var}(C') \cap \text{var}(Q)) \cup \text{var}(C)) \cap \text{var}(Q) \\
&\subseteq (V' \cup \text{var}(C)) \cap \text{var}(Q) \quad \text{since } \text{var}(C') \cap \text{var}(C[Q]) \subseteq V' \\
&\subseteq (V \cup \text{var}(C)) \cap \text{var}(Q) \quad \text{since } V' \subseteq V \cup \text{var}(C) \\
&\subseteq V \quad \text{since } \text{var}(C) \cap \text{var}(Q) \subseteq V
\end{align*}
$$

We also have $\text{vardef}(C'[C]) \cap V = (\text{vardef}(C') \cap V) \cup (\text{vardef}(C) \cap V) = \emptyset$ since $\text{vardef}(C) \cap V = \emptyset$ because $C$ is an acceptable evaluation context for $Q$ with public variables $V$ and $\text{vardef}(C') \cap V \subseteq \text{vardef}(C') \cap V' = \emptyset$ because we have renamed the variables of $C'$ not in $V'$ so that they are not in $V$ and $C'$ is an acceptable evaluation context for $C[Q]$ and with public variables $V'$.

Suppose that $Q \approx_p^{V,\mathcal{E}} Q'$, $Q$ satisfies a correspondence $\varphi$ with public variables $V$ up to probability $p'$, and $\mathcal{E}$ contains all events in $\varphi$. Let $A \in \mathcal{B}\mathcal{B}$ be an attacker. Let $C$ be an evaluation context acceptable for $Q'$ with public variables $V$ that does not contain events used by $\varphi$. We have

$$
\begin{align*}
\text{Adv}_{Q'}^{\varphi}(A, C) &= \text{Pr}^{\mathcal{A}}[C[Q'] : \neg\varphi] \\
&\le \text{Pr}^{\mathcal{A}}[C[Q] : \neg\varphi] + |\text{Pr}^{\mathcal{A}}[C[Q'] : \neg\varphi] - \text{Pr}^{\mathcal{A}}[C[Q] : \neg\varphi]| \\
&\le p'(A, C) + p(A, C, t_{\varphi})
\end{align*}
$$

Indeed, by renaming the variables and tables of $C$ that do not appear in $Q'$ to variables and tables that also do not occur in $Q$, $C$ is also an acceptable evaluation context for $Q$ with public variables $V$. Furthermore, by Property 6, this renaming does not change the probabilities. $\square$
**Reachability secrecy** Reachability secrecy aims to show that the adversary cannot compute the secret value. This notion is standard in the symbolic model, but less common than the notion of secrecy as “the adversary cannot distinguish the secret from a random value” (Section 2.8.1) in the computational model. It is still used, e.g. in the property of one-wayness or in the computational Diffie-Hellman assumption.

This notion makes sense only when the secret value is of a large type. Otherwise, the adversary would have a non-negligible probability of finding the secret value just by random guessing.

This notion is in fact encoded as a correspondence property. We distinguish two variants. One-session reachability secrecy of $x$ means that the adversary cannot compute any cell of array $x$, even if it has access to the public variables in $V$. Reachability secrecy of $x$ means that the adversary cannot compute any cell of array $x$, even if it has access to the other cells of $x$ and to the public variables in $V$.

**Definition 13 (One-session) reachability secrecy)** Let $Q$ be a process, $x$ a variable, and $V$ a set of variables. Let

$$
\begin{align*}
Q_{1\text{-ses.reach.secr.}(x)} &= \text{foreach } i_t \le n_t \text{ do } O_s[i_t](x' : T, u_1 : [1, n_1], \dots, u_m : [1, n_m]) := \\
&\quad \text{if defined}(x[u_1, \dots, u_m]) \land x' = x[u_1, \dots, u_m] \text{ then event } \text{adv\_has\_x} \\
Q_{\text{Reach.secr.}(x)} &= \text{foreach } i_r \le n_r \text{ do } O_r[i_r](u'_1 : [1, n_1], \dots, u'_m : [1, n_m]) := \\
&\quad \text{if defined}(x[u'_1, \dots, u'_m]) \text{ then} \\
&\quad \text{let } \text{reveal} : \mathbf{bool} = \text{true in return } (x[u'_1, \dots, u'_m]) \\
&\quad \text{| } \text{foreach } i_t \le n_t \text{ do } O_s[i_t](x' : T, u_1 : [1, n_1], \dots, u_m : [1, n_m]) := \\
&\quad \text{find } i \le i_r \text{ suchthat } \text{defined}(\text{reveal}[i], u'_1[i], \dots, u'_m[i]) \land \\
&\quad \qquad u'_1[i] = u_1 \land \dots \land u'_m[i] = u_m \text{ then yield else} \\
&\quad \text{if defined}(x[u_1, \dots, u_m]) \land x' = x[u_1, \dots, u_m] \text{ then event } \text{adv\_has\_x}
\end{align*}
$$

where $O_s, O_r \notin \text{fo}(Q)$, $x', u_1, \dots, u_m, u'_1, \dots, u'_m$, $\text{reveal} \notin \text{var}(Q) \cup V$, $\text{adv\_has\_x}$ does not occur in $Q$, and $\mathcal{E}(x) = [1, n_1] \times \dots \times [1, n_m] \to T$.

The process $Q$ satisfies one-session reachability secrecy of $x$ with public variables $V$ ($x \notin V$) up to probability $p$ if and only if the process $Q \mid Q_{1\text{-ses.reach.secr.}(x)}$ satisfies the correspondence event($\text{adv\_has\_x}$) $\Rightarrow$ false with public variables $V$ up to probability $p$.

The process $Q$ satisfies reachability secrecy of $x$ with public variables $V$ ($x \notin V$) up to probability $p$ if and only if $Q \mid Q_{\text{Reach.secr.}(x)}$ satisfies the correspondence event($\text{adv\_has\_x}$) $\Rightarrow$ false with public variables $V$ up to probability $p$.

The process $Q_{1\text{-ses.reach.secr.}(x)}$ waits for a call to oracle $O_s[i_t]$ with a candidate value $x'$ and indices $u_1, \dots, u_m$. If $x[u_1, \dots, u_m]$ is defined and equal to $x'$, the adversary managed to compute $x[u_1, \dots, u_m]$, hence to break one-session reachability secrecy. In this case, we execute event $\text{adv\_has\_x}$, and our goal will be to bound the probability of this event, by showing the correspondence event($\text{adv\_has\_x}$) $\Rightarrow$ false.

The process $Q_{\text{Reach.secr.}(x)}$ additionally provides a reveal query: by calling oracle $O_r[i_r]$ with indices $u'_1, \dots, u'_m$, the adversary can obtain the value of $x[u'_1, \dots, u'_m]$ if it is defined. Obviously, the adversary breaks reachability secrecy if it computes $x[u_1, \dots, u_m]$ without having first made a successful reveal query on the indices $u_1, \dots, u_m$. The absence of such a reveal query is verified by find $i \le i_r \dots$ before executing event $\text{adv\_has\_x}$.

The bounds on the number of queries ($n_t, n_r$) are chosen large enough that they do not limit the adversary.
### 2.8.4 Computation of Advantages

**Definition 14** Let sp be a security property: sp is 1-ses.secr.(x), Secrecy(x), bit secr.(x), or a trace property, represented by any distinguisher that does not use S, $\bar{S}$, nor non-unique events. (Trace properties include correspondences $\phi$, as well as true, the property that is always true.) Let D be a disjunction of Shoup and non-unique events that does not contain S nor $\bar{S}$. Let C be an evaluation context acceptable for Q with any public variables and A an attacker in BB.

When sp is a trace property, we define $V_{sp} = \emptyset$ and

$$ \mathrm{Adv}_Q(\mathcal{A}, C, sp, D) = \mathrm{Pr}^A[C[Q] : (\neg sp \lor D) \land \neg \mathrm{NonUnique}_{Q,D}] \quad (12) $$

When sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x), we define $V_{sp} = \{x\}$ and

$$ \mathrm{Adv}_Q(\mathcal{A}, C, sp, D) = \mathrm{Pr}^A[C[Q] : S \lor D] - \mathrm{Pr}^A[C[Q] : \bar{S} \lor \mathrm{NonUnique}_{Q,D}] \quad (13) $$

We write $\mathrm{Bound}_Q(V, sp, D, p)$ when $V_{sp} \subseteq V$ and for all $\mathcal{A} \in BB$, for all evaluation contexts $C'$ acceptable for $C_{sp}[Q]$ with public variables $V \setminus V_{sp}$ that does not contain events used by sp or D nor non-unique events in Q, we have $\mathrm{Adv}_Q(\mathcal{A}, C, sp, D) \le p(\mathcal{A}, C)$ for $C = C'[C_{sp}[]]$.

The events S and $\bar{S}$ are only executed by event_abort. In (13), we could write $(S \lor D) \land \neg \mathrm{NonUnique}_{Q,D}$ instead of $S \lor D$, to be more similar to (12). That would be equivalent because the game immediately aborts after executing S as well as events in D and in $\mathrm{NonUnique}_{Q,D}$, so only one of these events is executed. In (13), we expect that $C = C'[C_{sp}[]]$ for some context $C'$. This is what happens in the definition of $\mathrm{Bound}_Q(V, sp, D, p)$. In that definition, C is a context acceptable for Q with public variables V.

**Lemma 28** 1. In the initial game Q, let $D_U = \bigcup\{e \mid [\mathrm{unique}_e] \mathrm{occurs in Q}\} = \mathrm{NonUnique}_Q$.
If $\mathrm{Bound}_Q(V, sp, D_U, p)$, then Q satisfies property sp with public variables $V \setminus V_{sp}$ up to probability $p'$ where $p'(\mathcal{A}, C') = p(\mathcal{A}, C'[C_{sp}[]])$.

2. If $D, D_{SNU} : Q, D, EvUsed \xrightarrow{V} p$ $Q', D', EvUsed'$, the events S and $\bar{S}$ are not in $EvUsed'$, $\mathrm{Bound}'_Q(V, sp, D', p')$, and

* either sp is a trace property, $\neg sp \in D$, and $p''(\mathcal{A}, C) = p(\mathcal{A}, C, t_{\neg sp}) + p'(\mathcal{A}, C)$;

* or sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x), $\{S, \neg \bar{S}\} \subseteq D$, and $p''(\mathcal{A}, C) = 2p(\mathcal{A}, C, t_S) + p'(\mathcal{A}, C)$

then $\mathrm{Bound}_Q(V, sp, D, p'')$.

3. Let D and $D'$ be disjunctions of Shoup and non-unique events that do not contain S nor $\bar{S}$.

* If sp is a trace property, $\mathrm{Bound}_Q(V, sp, D, p)$, and $\mathrm{Bound}_Q(V, \mathrm{true}, D', p')$, then we have $\mathrm{Bound}_Q(V, sp, D \lor D', p + p')$.

* If sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x), $D'_{NU} = \bigcup\{e \mid e \mathrm{occurs in D'} \text{ and } e \text{ is a non-unique event}\}$, $\mathrm{Bound}_Q(V, sp, D, p)$, $\mathrm{Bound}_Q(V, \mathrm{true}, D', p')$, and $\mathrm{Bound}_Q(V, \mathrm{true}, D'_{NU}, p'')$, then $\mathrm{Bound}_Q(V, sp, D \lor D', p + p' + p'')$.

4. If $D, D_{SNU} : Q, D, EvUsed \xrightarrow{V} p$ $Q', D', EvUsed'$, the distinguisher $D''$ is a disjunction of Shoup and non-unique events in $EvUsed$ that does not contain S nor $\bar{S}$, and $\mathrm{Bound}_Q(V, \mathrm{true}, D'', p')$, then $D, D_{SNU} : Q, D \lor D'', EvUsed \xrightarrow{V} p_{p+p'} Q', D', EvUsed'$.
**Proof** Property 1: We have $\mathbf{NonUnique}_{Q,D_U} = D_{\text{false}}$. Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C'$ be an evaluation context acceptable for $C_{sp}[Q]$ with public variables $V \setminus V_{sp}$ that does not contain events used by $sp$, and $C = C'[C_{sp}]$. Since $\text{Bound}_Q(V, sp, D_U, p)$, we have $\text{Adv}_Q(\mathcal{A}, C, sp, D_U) \le p(\mathcal{A}, C)$.

* In case $sp$ is a trace property, $\text{Adv}_Q^{sp}(\mathcal{A}, C') = \text{Pr}^A[C'[Q] : \neg sp] \le \text{Pr}^A[C'[Q] : \neg sp \lor D_U] = \text{Pr}^A[C'[C_{sp}[Q]] : \neg sp \lor D_U] = \text{Adv}_Q(\mathcal{A}, C'[C_{sp}[]], sp, D_U)$.

* In case $sp$ is 1-ses.secr.(x), Secrecy(x), or bit secr.(x), $\text{Adv}_Q^{sp}(\mathcal{A}, C') = \text{Pr}^A[C'[C_{sp}[Q]] : \mathcal{S}] - \text{Pr}^A[C'[C_{sp}[Q]] : \bar{\mathcal{S}}] \le \text{Pr}^A[C'[C_{sp}[Q]] : \mathcal{S} \lor D_U] - \text{Pr}^A[C'[C_{sp}[Q]] : \bar{\mathcal{S}}] = \text{Adv}_Q(\mathcal{A}, C'[C_{sp}[]], sp, D_U)$.

In both cases, $\text{Adv}_Q^{sp}(\mathcal{A}, C') \le \text{Adv}_Q(\mathcal{A}, C'[C_{sp}[]], sp, D_U) = \text{Adv}_Q(\mathcal{A}, C, sp, D_U) \le p(\mathcal{A}, C) = p'(\mathcal{A}, C')$, so $Q$ satisfies property $sp$ with public variables $V \setminus V_{sp}$ up to probability $p'$.

Property 2, case $sp$ is a trace property: Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C$ be an evaluation context acceptable for $Q$ with public variables $V$ that does not contain events used by $sp$ nor $D$ nor non-unique events of $Q$. Let $C'$ be obtained by renaming the variables and tables of $C$ that do not occur in $Q$ to variables and tables that also do not occur in $Q'$, and by renaming the events of $C$ so that they are not in $\text{EvUsed}'$. The context $C'$ is then acceptable for $Q$ and $Q'$ with public variables $V$ and does not contain events in $\text{EvUsed}'$. Since $D, D_{\text{SNU}} : Q, D, \text{EvUsed} \xrightarrow{V} p'Q', D', \text{EvUsed}'$ and $\neg sp \in D$, we have by taking $D_1 = D_{\text{false}}$,

$$ \begin{aligned} \text{Adv}_Q(\mathcal{A}, C, sp, D) &= \text{Pr}^A[C[Q] : (\neg sp \lor D) \land \neg \text{NonUnique}_{Q,D}] \\ &= \text{Pr}^A[C'[Q] : (\neg sp \lor D) \land \neg \text{NonUnique}_{Q,D}] \end{aligned} $$

since the renaming of events does not affect the events of the distinguisher

$$ \begin{aligned} &\le p(\mathcal{A}, C', t_{\neg sp}) + \text{Pr}^A[C'[Q'] : (\neg sp \lor D') \land \neg \text{NonUnique}_{Q',D'}] \\ &\le p(\mathcal{A}, C', t_{\neg sp}) + \text{Adv}_{Q'}(\mathcal{A}, C', sp, D') \\ &\le p(\mathcal{A}, C', t_{\neg sp}) + p'(\mathcal{A}, C') \quad \text{since } \text{Bound}_{Q'}(V, sp, D', p') \\ &\le p(\mathcal{A}, C, t_{\neg sp}) + p'(\mathcal{A}, C) \end{aligned} $$

since the renaming does not modify the probability formulas by Property 6

$$ \le p''(\mathcal{A}, C) $$

so $\text{Bound}_Q(V, sp, D, p'')$.

Property 2, case $sp$ is 1-ses.secr.(x), Secrecy(x), or bit secr.(x): Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C'$ be an evaluation context acceptable for $C_{sp}[Q]$ with public variables $V \setminus V_{sp}$ that does not contain $\mathcal{S}, \bar{\mathcal{S}}$, events used by $D$, nor non-unique events of $Q$. Let $C = C'[C_{sp}[]]$. Let $C''$ be obtained by renaming the variables and tables of $C$ that do not occur in $Q$ to variables and tables that also do not occur in $Q'$, and by renaming the events of $C$ so that they are not in $\text{EvUsed}'$. (The events $\mathcal{S}$ and $\bar{\mathcal{S}}$ are left unchanged by this renaming; they are not in $\text{EvUsed}'$.) The context $C''$ is then acceptable for $Q$ and $Q'$ with public variables $V$ and does not contain events in $\text{EvUsed}'$. Then we have

$$ \begin{aligned} \text{Adv}_Q(\mathcal{A}, C, sp, D) &= \text{Pr}^A[C[Q] : \mathcal{S} \lor D] - \text{Pr}^A[C[Q] : \bar{\mathcal{S}} \lor \text{NonUnique}_{Q,D}] \\ &= \text{Pr}^A[C''[Q] : \mathcal{S} \lor D] - \text{Pr}^A[C''[Q] : \bar{\mathcal{S}} \lor \text{NonUnique}_{Q,D}] \end{aligned} $$

since the renaming of events does not affect the events of the distinguisher

$$ \begin{aligned} &= \text{Pr}^A[C''[Q] : (\mathcal{S} \lor D) \land \neg \text{NonUnique}_{Q,D}] \\ &\quad - \text{Pr}^A[C''[Q] : (\bar{\mathcal{S}} \land \neg D) \lor \text{NonUnique}_{Q,D}] \end{aligned} $$
since $S \lor D$ is equivalent to $(S \lor D) \land \neg \text{NonUnique}_{Q,D}$ and $\bar{S}$ is equivalent to $\bar{S} \land \neg D$: the game aborts immediately after executing $S, \bar{S}$, and the events in $D$ and $\text{NonUnique}_{Q,D}$ so only one of them can be executed

$$
\begin{align*}
&= \Pr^A[C''[Q] : (S \lor D) \land \neg \text{NonUnique}_{Q,D}] \\
&\quad + \Pr^A[C''[Q] : (\neg \bar{S} \lor D) \land \neg \text{NonUnique}_{Q,D}] - 1 \\
&\le \Pr^A[C''[Q'] : (S \lor D') \land \neg \text{NonUnique}_{Q',D'}] + p(\mathcal{A}, C'', t_S) \\
&\quad + \Pr^A[C''[Q'] : (\neg \bar{S} \lor D') \land \neg \text{NonUnique}_{Q',D'}] + p(\mathcal{A}, C'', t_S) - 1 \\
&\qquad \text{since } \neg \bar{S} \text{ can be implemented in the same time as } S \\
&\le \Pr^A[C''[Q'] : (S \lor D') \land \neg \text{NonUnique}_{Q',D'}] + p(\mathcal{A}, C'', t_S) \\
&\quad - \Pr^A[C''[Q'] : (\bar{S} \land \neg D') \lor \text{NonUnique}_{Q',D'}] + p(\mathcal{A}, C'', t_S) \\
&\le \Pr^A[C''[Q'] : S \lor D'] - \Pr^A[C''[Q'] : \bar{S} \lor \text{NonUnique}_{Q',D'}] + 2p(\mathcal{A}, C'', t_S)
\end{align*}
$$

since $S \lor D'$ is also equivalent to $(S \lor D') \land \neg \text{NonUnique}_{Q,D'}$ and $\bar{S}$ is also equivalent to $\bar{S} \land \neg D'$

$$
\begin{align*}
&\le \text{Adv}_{Q'}(\mathcal{A}, C'', sp, D') + 2p(\mathcal{A}, C'', t_S) \\
&\le p'(\mathcal{A}, C'') + 2p(\mathcal{A}, C'', t_S) \quad \text{since } \text{Bound}_{Q'}(V, sp, D', p') \\
&\le p'(\mathcal{A}, C) + 2p(\mathcal{A}, C, t_S) \\
&\qquad \text{since the renaming does not modify the probability formulas by Property 6} \\
&\le p''(\mathcal{A}, C)
\end{align*}
$$

so $\text{Bound}_Q(V, sp, D, p'')$.

Property 3, case sp is a trace property: Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C$ be an evaluation context acceptable for $Q$ with public variables $V$ that does not contain events used by sp, $D$, $D'$, nor non-unique events of $Q$. We have $\text{NonUnique}_{Q,D} = \text{NonUnique}_Q \land \neg D$. Therefore

$$
\begin{align*}
\text{Adv}_Q(\mathcal{A}, C, sp, D) &= \Pr^A[C[Q] : (\neg sp \lor D) \land \neg \text{NonUnique}_{Q,D}] \\
&= \Pr^A[C[Q] : (\neg sp \lor D) \land \neg (\text{NonUnique}_Q \land \neg D)] \\
&= \Pr^A[C[Q] : (\neg sp \lor D) \land (\neg \text{NonUnique}_Q \lor D)] \\
&= \Pr^A[C[Q] : (\neg sp \land \neg \text{NonUnique}_Q) \lor D]
\end{align*}
$$

In particular, $\text{Adv}_Q(\mathcal{A}, C, \text{true}, D) = \Pr^A[C[Q] : D]$. Hence

$$
\begin{align*}
\text{Adv}_Q(\mathcal{A}, C, sp, D \lor D') &= \Pr^A[C[Q] : (\neg sp \land \neg \text{NonUnique}_Q) \lor D \lor D'] \\
&\le \Pr^A[C[Q] : (\neg sp \land \neg \text{NonUnique}_Q) \lor D] + \Pr^A[C[Q] : D'] \\
&\le \text{Adv}_Q(\mathcal{A}, C, sp, D) + \text{Adv}_Q(\mathcal{A}, C, \text{true}, D') \\
&\le p(\mathcal{A}, C) + p'(\mathcal{A}, C)
\end{align*}
$$

since $\text{Bound}_Q(V, sp, D, p)$ and $\text{Bound}_Q(V, \text{true}, D', p')$. So $\text{Bound}_Q(V, sp, D \lor D', p + p')$.

Property 3, case sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x): Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C'$ be an evaluation context acceptable for $C_{sp}[Q]$ with public variables $V \setminus V_{sp}$ that does not contain $S, \bar{S}$, events used by $D, D'$, nor non-unique events of $Q$. Let $C = C'[C_{sp}]$. Since $\text{NonUnique}_{Q,D} = \text{NonUnique}_Q \land \neg D$, we have

$$
\text{Adv}_Q(\mathcal{A}, C, sp, D) = \Pr^A[C[Q] : S \lor D] - \Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D)]
$$
Hence

$$
\begin{align*}
\mathrm{Adv}_Q(\mathcal{A}, C, sp, D \lor D') &= \Pr^A[C[Q] : S \lor D \lor D'] \\
&\quad - \Pr^A[C[Q] : \bar{S} \lor (\mathrm{NonUnique}_Q \land \neg D \land \neg D')] \\
&\le \Pr^A[C[Q] : S \lor D] + \Pr^A[C[Q] : D'] \\
&\quad - \Pr^A[C[Q] : \bar{S} \lor (\mathrm{NonUnique}_Q \land \neg D)] + \Pr^A[C[Q] : D'_{\mathrm{NU}}] \\
&\le \mathrm{Adv}_Q(\mathcal{A}, C, sp, D) + \mathrm{Adv}_Q(\mathcal{A}, C, \text{true}, D') + \mathrm{Adv}_Q(\mathcal{A}, C, \text{true}, D'_{\mathrm{NU}}) \\
&\le p(\mathcal{A}, C) + p'(\mathcal{A}, C) + p''(\mathcal{A}, C)
\end{align*}
$$

since $\text{Bound}_Q(V, sp, D, p)$, $\text{Bound}_Q(V, \text{true}, D', p')$, $\text{Bound}_Q(V, \text{true}, D'_{\text{NU}}, p'')$, and $C$ is also an evaluation context acceptable for $Q$ with public variables $V$. So $\text{Bound}_Q(V, sp, D \lor D', p+p'+p'')$.

The inequality $-\Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D \land \neg D')] \le -\Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D)] + \Pr^A[C[Q] : D'_{\text{NU}}]$ used above is justified as follows:

$$
\begin{align*}
\Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D)]
  &\le \Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D \land \neg D') \lor (\text{NonUnique}_Q \land D')] \\
  &\le \Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D \land \neg D')] + \Pr^A[C[Q] : \text{NonUnique}_Q \land D'] \\
  &\le \Pr^A[C[Q] : \bar{S} \lor (\text{NonUnique}_Q \land \neg D \land \neg D')] + \Pr^A[C[Q] : D'_{\text{NU}}]
\end{align*}
$$

Property 4: The distinguisher $D \lor D''$ is a disjunction of Shoup and non-unique events in $EvUsed$. Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $C$ be any evaluation context acceptable for $Q$ with public variables $V$ that does not contain events in $EvUsed'$. Let $D_0 \in \mathcal{D} \cup \{D_{\text{false}}\}$. Let $D_1$ be a disjunction of events in $D_{\text{NU}}$. We have

$$
\begin{align*}
\Pr^A[C[Q] : (D_0 \lor D_1 \lor D \lor D'') \land \neg \text{NonUnique}_{Q, D_1 \lor D \lor D''}] \\
&= \Pr^A[C[Q] : (D_0 \land \neg \text{NonUnique}_Q) \lor D_1 \lor D \lor D''] \\
&\qquad \text{as in Property 3, case sp is a trace property} \\
&\le \Pr^A[C[Q] : (D_0 \land \neg \text{NonUnique}_Q) \lor D_1 \lor D] + \Pr^A[C[Q] : D''] \\
&\le \Pr^A[C[Q] : (D_0 \lor D_1 \lor D) \land \neg \text{NonUnique}_{Q, D_1 \lor D}] + \text{Adv}_Q(\mathcal{A}, C, \text{true}, D'') \\
\text{since } \text{Adv}_Q(\mathcal{A}, C, \text{true}, D'') &= \Pr^A[C[Q] : D''] \text{ (see Property 3, case sp is a trace property)} \\
&\le \Pr^A[C[Q'] : (D_0 \lor D_1 \lor D') \land \neg \text{NonUnique}_{Q, D_1 \lor D'}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C)
\end{align*}
$$

since $\text{Bound}_Q(V, \text{true}, D'', p')$. (Note that the context $C$ does not contain events used by $D''$ nor non-unique events of $Q$.) $\square$

This lemma allows one to bound the advantage of the adversary against secrecy and correspondences. Property 1 is used in the initial game, to express the desired probability from $\text{Bound}_Q(V, sp, D_U, p)$. (Using the distinguisher $D_U$ can also be understood by saying that we consider that the adversary wins if some non-unique event is executed, that is, if a find or get declared unique by the user actually has several possible choices. That allows the implementation to make any choice when a find[unique$_e$] or get[unique$_e$] has several possible choices: the security proof remains valid. In particular, a find[unique$_e$] or get[unique$_e$] can be implemented by always choosing the first found element.) Property 2 is used when a game $Q$ is transformed into a game $Q'$ during the proof. It allows one to bound the probability in $Q$ from a bound in $Q'$. Property 3 is useful when distinct sequences of games are used for bounding the probabilities of breaking sp and of $D$ on one side and of $D'$ on the other side. We bound these two
<figure><img src="image_8.png" /><figcaption>Figure 15: Structure of a proof tree</figcaption></figure>

probabilities by $\text{Bound}_Q(V, sp, D, p)$ and $\text{Bound}_Q(V, \text{true}, D', p')$ separately, then obtain a bound $\text{Bound}_Q(V, sp, D \lor D', p'')$ by computing a sum. (When we deal with secrecy and $D'_{\text{NU}} \neq D_{\text{false}}$, the probability of $D'_{\text{NU}}$ can be bounded by looking at the proof for $D'$.)

More formally, consider the following cases, using Lemma 28, Property 1:

* If we want to prove that $Q_0$ satisfies the correspondence $\varphi$ with public variables $V$, then we let $sp = \varphi$.

* If we want to prove that $Q_0$ satisfies the (one-session or bit) secrecy of $x$ with public variables $V'(x \notin V')$, then we let $sp$ be $\text{1-ses.secr}(x)$, $\text{Secrecy}(x)$, or bit $\text{secr}(x)$ and $V = V' \cup \{x\}$.

In both cases, we show $\text{Bound}_{Q_0}(V, sp, D_U, p)$. The proof produced by CryptoVerif can be represented as a tree whose nodes are labeled with quintuples $(Q, V, sp', D, \text{EvUsed})$ and whose edges are labeled with triples $(sp'', D'', p'')$, where $Q$ is the current game, $V$ is the set of public variables, $sp'$ and $sp''$ are either the initial property to prove $sp$ or true, $D$ and $D''$ are disjunctions of Shoup and non-unique events, $\text{EvUsed}$ is the set of events used so far, and $p''$ is a probability formula. The edges have a single source node, but may have 0, 1, or several target nodes. We associate to each node labeled with $(Q, V, sp', D, \text{EvUsed})$ a property $\text{Bound}_Q(V, sp', D, p)$, and to each edge labeled with $(sp'', D'', p'')$ with source node labeled with $(Q, V, sp', D, \text{EvUsed})$ a property $\text{Bound}_Q(V, sp'', D'', p')$. CryptoVerif computes the probabilities $p, p'$ such that these properties hold from the leaves of the tree to its root, as explained next.

The root of the tree is labeled with $(Q_0, V, sp, D_U, \text{EvUsed}_0)$ such that $\text{EvUsed}_0$ is the set containing the events used by correspondences to prove or that occur in $Q_0$.

When an edge labeled with $(sp'', D'', p'')$ has a source node labeled with $(Q, V, -, -, \text{EvUsed})$ and target nodes labeled with $(Q_j, V_j, sp'_j, D_j, \text{EvUsed}_j)$ for $j \in \{1, \dots, l\}$ (Figure 15(a)), the bound associated to the edge can be computed from the bound associated to the target nodes by the probability formula $p''$ that labels the edge: if $\text{Bound}_{Q_j}(V_j, sp'_j, D_j, p_j)$ for $j \in \{1, \dots, l\}$, then $\text{Bound}_Q(V, sp'', D'', p)$ where $p(\mathcal{A}, \mathcal{C}) = p''(\mathcal{A}, \mathcal{C}, p_1(\mathcal{C}), \dots, p_l(\mathcal{C}))$. This situation corresponds to a game transformation that transforms game $Q$ into games $Q_j$ ($j \in \{1, \dots, l\}$). We can distinguish several cases depending on where the edge comes from:
many target nodes as there are branches in the guessed instruction. For the transformation **guess** $i$, Lemma 59 requires $D'' = D_{\text{false}}$, which can be achieved as for **success** above.

When a node labeled with $(Q, V, sp', D, EvUsed)$ has outgoing edges labeled respectively $(sp'_1, D'_1, -)$, ..., $(sp'_l, D'_l, -)$ (Figure 15(b)), then $D = D'_1 \lor \dots \lor D'_l$ ($D$ is a disjunction of the form $e_1 \lor \dots \lor e_m$, $D'_1, \dots, D'_l$ are disjunctions that form a partition of the disjuncts of $D$), there exists $j_0 \le l$ such that $sp'_{j_0} = sp'$ and for all $j \ne j_0$, $sp'_{j'} = \text{true}$. The bound associated to the node is computed from the bound associated to the edges by Lemma 28, Property 3:

* If $sp'$ is a trace property, then we have $\text{Bound}_Q(V, sp', D, p'_1 + \dots + p'_l)$, where $\text{Bound}_Q(V, sp'_j, D'_j, p'_j)$ for all $j \in \{1, \dots, l\}$.

* If $sp'$ is 1-ses.secr.(x), Secrecy(x), or bit secr.(x), then we have $\text{Bound}_Q(V, sp', D, \sum_{j=1}^l p'_j + \sum_{j=1, \dots, l; j \ne j_0} p''_j)$, where $\text{Bound}_Q(V, sp'_j, D'_j, p'_j)$ for all $j \in \{1, \dots, l\}$, $\text{Bound}_Q(V, sp'_j, D'_NU_j, p''_j)$ for all $j \in \{1, \dots, l\}$ with $j \ne j_0$, and $D'_NU_j$ is obtained from $D'_j$ by keeping only the non-unique events.

To prove $\text{Bound}_Q(V, sp'_j, D'_NU_j, p''_j)$, we build a proof tree with root $Q, V, sp'_j, D'_NU_j, EvUsed$ from the subtree $Q, V, sp', D, EvUsed \xrightarrow{sp'_j, D'_j, p_j} \dots$ by

- replacing the root $Q, V, sp', D, EvUsed$ with $Q, V, sp'_j, D'_j, EvUsed$.

- removing all Shoup events of $D'_j$ from distinguishers that label nodes and edges. In particular, the root $Q, V, sp'_j, D'_j, EvUsed$ then becomes $Q, V, sp'_j, D'_NU_j, EvUsed$.

- removing subtrees that start with an edge labeled $sp'_j, D_{\text{false}}, p$ for some $p$.

The proof steps remain valid: all proof steps are a fortiori valid when we ignore some Shoup events. That can be verified for each transformation using its soundness lemma. For instance, for proof steps that come from usual transformations that satisfy property preservation with introduction of events and have a Shoup event $e$ of $D'_j$ both before and after, we can avoid adding that event $e$ when we derive $D_1, \emptyset : Q, D'_j, EvUsed \xrightarrow{V} p'$ $Q_1, D_1, EvUsed_1$ from $D, D_{\text{SNU}} : Q, D, EvUsed \xrightarrow{V} p'$ $Q_1, D', EvUsed_1$. For proof steps that prove a Shoup event $e$ of $D'_j$ (via **success**), that proof step starts with just event $e$, so it is simply removed. We can then apply the previous reasoning to that proof tree.

When the proof is a basic sequence of games, each node has one son, which is the next game in the sequence, except the last game of the sequence which has no son. Only the final proof step is distinct for each query. However, it may happen that distinct sequences of games are used to bound several events occurring in the game; in this case, there is a branching in the proof and a node has several sons. Examples of proof trees can be found in Figure 16; they are explained below.

The bound associated to the leaves of the tree is computed by **success**; the bound associated to an edge is computed from the bounds associated to its target nodes, and the bound associated to a node is computed from the bounds associated to its outgoing edges. We can then compute the bounds associated to all nodes of the tree, by induction from the leaves to the root. At the root, we obtain a bound $\text{Bound}_{Q_0}(V, sp, D_U, p)$ that yields the desired result.

Lemma 28 allows us to obtain more precise probability bounds than the standard computation of probabilities generally done by cryptographers, when we use Shoup's lemma [68]. By Shoup's lemma, if $G'$ is obtained from $G$ by inserting an event $e$ and modifying the code executed after $e$, the probability of distinguishing $G'$ from $G$ is bounded by the probability of executing $e$: for
<figure><img src="image_9.png" /><figcaption>Figure 16: Examples of proof trees</figcaption></figure>

all attackers $\mathcal{A} \in \mathcal{BB}$ and all contexts $C$ acceptable for $G$ and $G'$ (with any public variables) and all distinguishers $D$, $|\Pr^A[C[G] : D] - \Pr^A[C[G'] : D]| \le \Pr^A[C[G'] : e]$. Hence,

$$ \Pr^A[C[G] : D] \le \Pr^A[C[G'] : e] + \Pr^A[C[G'] : D]. $$

We improve over this computation of probabilities by considering $e$ and $D$ simultaneously instead of making the sum of the two probabilities:

$$ \Pr^A[C[G] : D] \le \Pr^A[C[G'] : D \lor e]. $$

For example, suppose that we want to bound the probability of event $e_0$ in $G_0$: we define $sp = [\text{event}(e_0) \Rightarrow \text{false}] = \neg e_0$. We transform $G_0$ into $G_1$ using Shoup's lemma, so that $G_1$ differs from $G_0$ only when $G_1$ executes event $e$, and we have $\{e_0\}, \emptyset : G_0, D_{\text{false}}, \text{EvUsed}_0 \to_0 G_1, e, \text{EvUsed}_1$; then we transform $G_1$ into $G_2$, so that $G_1 \approx_p^{\{e_0,e\}} G_2$, so we have $\{e_0\}, \emptyset : G_1, e, \text{EvUsed}_1 \to_p G_2, e, \text{EvUsed}_1$ by Lemma 20, Property 1a; and $G_2$ executes neither $e_0$ nor $e$. We suppose for simplicity that no $[\text{unique}_e]$ occurs, so that $\text{NonUnique}_{G_i,D}$ is always false. The corresponding proof tree is given in Figure 16(a).

* Since $e_0$ does not occur in $G_2$, we have $\text{Adv}_{G_2}(\mathcal{A}, C, sp, D_{\text{false}}) = 0$ for all $\mathcal{A} \in \mathcal{BB}$ and all evaluation contexts $C$ acceptable for $G_2$ with public variables $V$ that do not contain event $e_0$. So $\text{Bound}_{G_2}(V, sp, D_{\text{false}}, 0)$. Similarly, $\text{Bound}_{G_2}(V, true, e, 0)$. These two properties are represented in the proof tree by the two edges outgoing from node $G_2, V, sp, e, \{e_0, e\}$.

* By Lemma 28, Property 3, $\text{Bound}_{G_2}(V, sp, e, p'_3)$ where $p'_3(C) = 0$.

* Since $\{e_0\}, \emptyset : G_1, e, \text{EvUsed}_1 \to_p G_2, e, \text{EvUsed}_1$, by Lemma 28, Property 2, we obtain $\text{Bound}_{G_1}(V, sp, e, p'_2)$ where $p'_2(\mathcal{A}, C) = p(\mathcal{A}, C, t_{\text{sp}}) + p'_3(\mathcal{A}, C)$. This is represented in the proof tree by the edge from node $G_1, V, sp, e, \{e_0, e\}$ to node $G_2, V, sp, e, \{e_0, e\}$ labeled with $sp, e, pstd_p^{sp}$.
<figure><img src="image_10.png" /><figcaption>Figure 17: Removing subtrees</figcaption></figure>

* Since {$e_0$}, $\emptyset: G_0, D_{\text{false}}, \text{EvUsed}_0 \to_0 G_1, e, \text{EvUsed}_1$, by Lemma 28, Property 2, we obtain $\text{Bound}_{G_0}(V, sp, D_{\text{false}}, p'_1)$ where $p'_1(\mathcal{A}, C) = 0 + p'_2(\mathcal{A}, C)$. This is represented in the proof tree by the edge from node $G_0, V, sp, D_{\text{false}}, \{e_0\}$ to node $G_1, V, sp, e, \{e_0, e\}$ labeled with sp, $D_{\text{false}}$, $\text{pstd}_0^{sp}$.

* Finally, by Lemma 28, Property 1, we conclude that $G_0$ satisfies sp with public variables V up to probability $p'_1$, where $p'_1(\mathcal{A}, C) = p'_2(\mathcal{A}, C) = p(\mathcal{A}, C, t_{\neg sp}) + p'_3(\mathcal{A}, C) = p(\mathcal{A}, C, t_{e_0})$, which means that $\text{Pr}^A[C[G_0]: e_0] \le p(\mathcal{A}, C, t_{e_0})$ for all evaluation contexts C acceptable for $G_0$ with public variables V that do not contain event $e_0$.

Let C be an evaluation context acceptable for $G_0$ with public variables V that does not contain event $e_0$ and A an attacker in BB. Since we suppose for simplicity that no $[\text{unique}_e']$ occurs, so that $\text{NonUnique}_{G_i,D}$ is always false, we have $\text{Adv}_{G_i}(\mathcal{A}, C, sp, D) = \text{Pr}^A[C[G_i]: \neg sp \lor D]$, so we can write the previous computation simply using probabilities:

$$ \begin{align*} \text{Pr}^A[C[G_0]: e_0] &\le \text{Pr}^A[C[G_1]: e_0 \lor e] \quad \text{since } \{e_0\}, \emptyset: G_0, D_{\text{false}}, \text{EvUsed}_0 \to_0 G_1, e, \text{EvUsed}_1 \\ &\le p(\mathcal{A}, C, t_{e_0}) + \text{Pr}^A[C[G_2]: e_0 \lor e] \\ &\qquad \text{since } \{e_0\}, \emptyset: G_1, e, \text{EvUsed}_1 \to_0 G_2, e, \text{EvUsed}_1 \\ &\le p(\mathcal{A}, C, t_{e_0}) \quad \text{since } G_2 \text{ executes neither } e_0 \text{ nor } e. \end{align*} $$

In contrast, the standard computation of probabilities yields

$$ \text{Pr}^A[C[G_0]: e_0] \le \text{Pr}^A[C[G_1]: e_0] + \text{Pr}^A[C[G_1]: e] \le p(\mathcal{A}, C, t_{e_0}) + p(\mathcal{A}, C, t_e). $$

The runtime $t_D$ of D is essentially the same for $e_0, e$, and $e_0 \lor e$, so $\text{Pr}^A[C[G_0]: e_0] \le p(\mathcal{A}, C, t_D)$ by Lemma 28, while $\text{Pr}^A[C[G_0]: e_0] \le 2p(\mathcal{A}, C, t_D)$ by the standard computation, so we have gained a factor 2. The probability that comes from the transformation of $G_1$ into $G_2$ is counted once (for distinguisher $e_0 \lor e$) instead of counting it twice (once for $e_0$ and once for $e$).

The standard computation of probabilities corresponds to applying point 3 of Lemma 28 to bound each probability separately and compute the sum, as soon as the considered distinguisher D has several disjuncts. Instead, we use point 3 of Lemma 28 only when the proof uses different sequences of games to bound the probabilities of the events, as in Figure 16(b).

Consider a proof tree that consists of a main branch that is a sequence of applications of transformations that satisfy property preservation with introduction of events (properties of the
for $G_2$ with public variables $V$. Furthermore, by Property 6, this renaming does not change the probabilities. Let $D_0 \in \mathcal{D}$ be a distinguisher that runs in time at most $t_{D_0}$. We rename the events of $C$ in $EvUsed'$ or $EvUsed'_1$ to some fresh events, and modify $D_0$ so that it considers the renamed events as if they were the original events. That does not change the probability $|\Pr^A[C[G_0]: D_0] - \Pr^A[C[G_1]: D_0]|$, and guarantees that $C$ does not contain events in $EvUsed'$ nor in $EvUsed'_1$. So

$$
\begin{align*}
\Pr^A[C[G_0]: D_0] &\le \Pr^A[C[G_0]: D_0 \lor D_{U0}] \\
&\le \Pr^A[C[G_2]: (D_0 \lor D_2) \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) \\
&\le \Pr^A[C[G_2]: ((D_0 \land \neg D_2) \lor D_2) \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) \\
&\le \Pr^A[C[G_2]: (D_0 \land \neg D_2) \land \neg \text{NonUnique}_{G_2,D_2}] \\
&\qquad + \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) \\
&\le \Pr^A[C[G_2]: D_0 \land \neg D_2] + \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

By applying (15) to $\neg D_0$, which is also in $\mathcal{D}$ and runs in the same time as $D_0$, we have

$$
\begin{align*}
1 - \Pr^A[C[G_1]: D_0] &= \Pr^A[C[G_1]: \neg D_0] \\
&\le \Pr^A[C[G_1]: \neg D_0 \lor D_{U1}] \\
&\le \Pr^A[C[G_2]: (\neg D_0 \lor D_2) \land \neg \text{NonUnique}_{G_2,D_2}] + p'(\mathcal{A}, C, t_{D_0}) \\
&\le \Pr^A[C[G_2]: \neg D_0 \lor D_2] + p'(\mathcal{A}, C, t_{D_0}) \\
&\le 1 - \Pr^A[C[G_2]: D_0 \land \neg D_2] + p'(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

$$
\text{so} \qquad - \Pr^A[C[G_1]: D_0] \le - \Pr^A[C[G_2]: D_0 \land \neg D_2] + p'(\mathcal{A}, C, t_{D_0})
$$

$$
\begin{align*}
\Pr^A[C[G_0]: D_0] - \Pr^A[C[G_1]: D_0] \\
\le \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

By applying the formula above to $\neg D_0$, which runs in the same time as $D_0$, we have

$$
\begin{align*}
\Pr^A[C[G_1]: D_0] - \Pr^A[C[G_0]: D_0] \\
\le \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

$$
\begin{align*}
\text{so} \\
& | \Pr^A[C[G_0]: D_0] - \Pr^A[C[G_1]: D_0]| \\
& \le \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C, t_{D_0})
\end{align*}
$$

$$
\text{so } G_0 \approx_{p''}^V G_1 \text{ where } p''(\mathcal{A}, C, t_{D_0}) = \Pr^A[C[G_2]: D_2 \land \neg \text{NonUnique}_{G_2,D_2}] + p(\mathcal{A}, C, t_{D_0}) + p'(\mathcal{A}, C, t_{D_0}).
$$

2.8.6 Proof of query\_equiv

**Decisional case (query-equiv without [computational] annotation)** The situation is similar to the proof of indistinguishability, but the property we want to prove is $\mathcal{D}_{\neg EvUsed_1, \emptyset}: G_0, D_{\text{false}}, \emptyset \xrightarrow{V} p G_1, D_1, EvUsed_1$ where $G_0$ contains no events, $D_1 = e_1 \lor \dots \lor e_m, e_1, \dots, e_m$
are the Shoup events occurring in $G_1$, $e'_1, \dots, e'_l$ are the non-unique events occurring in $G_1$, $EvUsed_1 = \{e_1, \dots, e_m, e'_1, \dots, e'_l\}, V = \emptyset$.

We need to show that, for all attackers $\mathcal{A} \in \mathcal{BB}$, all evaluation contexts $C$ acceptable for $G_0$ and $G_1$ without public variables that do not contain events in $EvUsed_1$ and all distinguishers $D_0 \in \mathcal{D}_{\neg EvUsed_1}$,

$$ \mathrm{Pr}^{\mathcal{A}}[C[G_0] : D_0] \leq \mathrm{Pr}^{\mathcal{A}}[C[G_1] : (D_0 \lor D_1) \land \neg \mathrm{NonUnique}_{G_1, D_1}] + p(\mathcal{A}, C, t_{D_0}) $$

CryptoVerif finds a game $G_2$ such that $\mathcal{D}_{\neg EvUsed_0'}, \emptyset : G_0, D_{\text{false}}, \emptyset \xrightarrow{V} p_0 G_2, D_2, EvUsed_0'$ and $\mathcal{D}_{\neg EvUsed_0'}, \emptyset : G_1, D_{U1}, EvUsed_1 \xrightarrow{V} p_1 G_2, D_2', EvUsed_1'$ where $EvUsed_1'' = EvUsed_1' \setminus \{e_1, \dots, e_m\}, D_{U1} = e'_1 \lor \dots \lor e'_l = \mathrm{NonUnique}_{G_1, D_1}$, and $D_2 = D_1 \lor D_2'$. (The events $e_1, \dots, e_m$ must be preserved by the second proof, hence we allow distinguishers in $\mathcal{D}_{\neg EvUsed_0'}$ to use these events. The events $e_1, \dots, e_m$ will be introduced in the first proof, and the active queries in $G_2$ are also required to match so $D_2 = D_1 \lor D_2'$.) So for all attackers $\mathcal{A} \in \mathcal{BB}$, all evaluation contexts $C$ acceptable for $G_0$ and $G_2$ without public variables that do not contain events in $EvUsed_0'$, and all distinguishers $D_0 \in \mathcal{D}_{\neg EvUsed_0'}$ that run in time at most $t_{D_0}$,

$$ \mathrm{Pr}^{\mathcal{A}}[C[G_0] : D_0] \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : (D_0 \lor D_2) \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) $$

and for all attackers $\mathcal{A} \in \mathcal{BB}$, for all evaluation contexts $C$ acceptable for $G_1$ and $G_2$ without public variables that do not contain events in $EvUsed_1'$, and all distinguishers $D_0 \in \mathcal{D}_{\neg EvUsed_1'}$ that run in time at most $t_{D_0}$,

$$ \mathrm{Pr}^{\mathcal{A}}[C[G_1] : D_0 \lor D_{U1}] \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : (D_0 \lor D_2') \land \neg \mathrm{NonUnique}_{G_2, D_2'}] + p_1(\mathcal{A}, C, t_{D_0}) $$

In the last equation, we replace $D_0$ with $\neg D_0 \land \neg D_1$ for $D_0 \in \mathcal{D}_{\neg EvUsed_1'}$, yielding

$$ \mathrm{Pr}^{\mathcal{A}}[C[G_1] : (\neg D_0 \land \neg D_1) \lor D_{U1}] \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : ((\neg D_0 \land \neg D_1) \lor D_2') \land \neg \mathrm{NonUnique}_{G_2, D_2'}] + p_1(\mathcal{A}, C, t_{D_0}) $$

so

$$ \mathrm{Pr}^{\mathcal{A}}[C[G_2] : ((D_0 \lor D_1) \land \neg D_2') \lor \mathrm{NonUnique}_{G_2, D_2'}] \leq \mathrm{Pr}^{\mathcal{A}}[C[G_1] : (D_0 \lor D_1) \land \neg D_{U1}] + p_1(\mathcal{A}, C, t_{D_0}) $$

Then we get

$$ \begin{aligned} \mathrm{Pr}^{\mathcal{A}}[C[G_0] : D_0] & \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : (D_0 \lor D_2) \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) \\ & \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : (D_0 \lor D_1 \lor D_2') \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) \\ & \leq \mathrm{Pr}^{\mathcal{A}}[C[G_2] : ((D_0 \lor D_1) \land \neg D_2') \lor \mathrm{NonUnique}_{G_2, D_2}] \\ & \qquad + \mathrm{Pr}^{\mathcal{A}}[C[G_2] : D_2' \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) \\ & \leq \mathrm{Pr}^{\mathcal{A}}[C[G_1] : (D_0 \lor D_1) \land \neg D_{U1}] \\ & \qquad + p_1(\mathcal{A}, C, t_{D_0}) + \mathrm{Pr}^{\mathcal{A}}[C[G_2] : D_2' \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) \\ & \leq \mathrm{Pr}^{\mathcal{A}}[C[G_1] : (D_0 \lor D_1) \land \neg \mathrm{NonUnique}_{G_1, D_1}] \\ & \qquad + p_1(\mathcal{A}, C, t_{D_0}) + \mathrm{Pr}^{\mathcal{A}}[C[G_2] : D_2' \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}) \end{aligned} $$

so we get the desired result with

$$ p(\mathcal{A}, C, t_{D_0}) = p_1(\mathcal{A}, C, t_{D_0}) + \mathrm{Pr}^{\mathcal{A}}[C[G_2] : D_2' \land \neg \mathrm{NonUnique}_{G_2, D_2}] + p_0(\mathcal{A}, C, t_{D_0}). $$

Inria
**Computational case (query-equiv with [computational] annotation)** As in the decisional case, we want to prove $D_{\neg EvUsed_1}, \emptyset : G_0, D_{false}, \emptyset \xrightarrow{V} p G_1, D_1, EvUsed_1$ where $G_0$ contains no events, $D_1 = e_1 \lor \dots \lor e_m, e_1, \dots, e_m$ are the Shoup events occurring in $G_1, e'_1, \dots, e'_l$ are the non-unique events occurring in $G_1, EvUsed_1 = \{e_1, \dots, e_m, e'_1, \dots, e'_l\}, V = \emptyset$. Additionally, we want to show that the random values of $G_0$ and $G_1$ marked [unchanged] can be used in events (different from $e_1, \dots, e_m$ since $e_1, \dots, e_m$ have no arguments) in the game transformed using this assumption. That corresponds to adding oracles that execute the same arbitrary events using [unchanged] random values to both $G_0$ and $G_1$. We write $G'_0$ and $G'_1$ for the games $G_0$ and $G_1$ respectively with additional events and show $D_{\neg EvUsed_1}, \emptyset : G'_0, D_{false}, EvUsed_0 \xrightarrow{V} p G'_1, D_1, EvUsed_1 \cup EvUsed_0$ where $EvUsed_0$ contains these additional events. These additional events can be observed by the adversary, so they are allowed in distinguishers in $D_{\neg EvUsed_1}$.

Let $D_{U1} = e'_1 \lor \dots \lor e'_l = \text{NonUnique}_{G_1, D_1}$.

Let us write $O_0(\tilde{r}, \tilde{args})$ (resp. $O_1(\tilde{r}, \tilde{args})$) for the result of oracle $O$ in game $G_0$ (resp. $G_1$) with randomness $\tilde{r}$ and arguments $\tilde{args}$.

In order to establish this property, we show that there exists a mapping $\phi$ of the randomness, such that if random value variable $r$ has value $v$ in $G_0$, then it has value $\phi_r(v)$ in $G_1$, $\phi_r$ is the identity when the variable $r$ is marked [unchanged], $\phi_r$ preserves the probability distribution of variable $r$, and we define a game $G_2$ in which oracle $O$ with randomness $\tilde{r}$ and arguments $\tilde{args}$ returns

let $x_0 = O_0(\tilde{r}, \tilde{args})$ in
let $x_1 = O_1(\phi(\tilde{r}), \tilde{args})$ in
if $x_0 = x_1$ then $x_0$ else event_abort distinguish

We bound

$$ 
\begin{align*}
p(\mathcal{A}, C) &= \Pr^{\mathcal{A}}[C[G_2] : \text{distinguish} \lor \text{NonUnique}_{G_2, D_{\text{false}}}] \\
&= \Pr^{\mathcal{A}}[C[G_2] : \text{distinguish} \lor D_{U1}] \\
&= \text{Adv}_{G_2}(\mathcal{A}, C, \text{distinguish} \Rightarrow \text{false}, D_{U1})
\end{align*}
$$

From this bound, we infer the desired property.

We consider a game $G_3$ in which oracle $O$ returns

let $x_0 = O_0(\tilde{r}, \tilde{args})$ in
let $x_1 = O_1(\phi(\tilde{r}), \tilde{args})$ in
$x_0$

We define $G'_2$ as $G_2$ with the same additional events as in $G'_0$ and $G'_1$, and $G'_3$ as $G_3$ with the same additional events as in $G'_0$ and $G'_1$. The game $G'_3$ behaves as $G'_0$ except that it executes a Shoup event $e_i$ or a non-unique event when $G_1$ does, so we have, for any $\mathcal{A} \in \mathcal{BB}$ and any evaluation context $C$ acceptable for $G'_0$ and $G'_3$ without public variables, and any distinguisher $D_0$,

$$ \Pr^{\mathcal{A}}[C[G'_0] : D_0] \leq \Pr^{\mathcal{A}}[C[G'_3] : D_0 \lor D_1 \lor D_{U1}] $$

Moreover, $G'_3$ behaves as $G'_1$ except when $G'_2$ executes event distinguish, that is, when $G_2$ executes event distinguish (the additional events introduced in $G'_2$ are not needed to evaluate the probability of distinguish since we do not consider their probability), so for all $D$,

$$ | \Pr^{\mathcal{A}}[C[G'_3] : D] - \Pr^{\mathcal{A}}[C[G'_1] : D] | \leq \Pr^{\mathcal{A}}[C[G_2] : \text{distinguish}] \quad (16) $$
Let $C$ be any evaluation context acceptable for $G'_0$ and $G'_2$ without public variables and $\mathcal{A}$ be an attacker in $\mathcal{BB}$. By renaming $x_0$ and $x_1$ to variables not in $C$, $C$ is also acceptable for $G'_0$ and $G'_3$ without public variables. Let $D_0$ be any distinguisher. With $D = D_0 \lor D_1 \lor D_{U1}$ in (16), we obtain

$$
\begin{align*}
\Pr^{\mathcal{A}}[C[G'_0] : D_0] &\le \Pr^{\mathcal{A}}[C[G'_3] : D_0 \lor D_1 \lor D_{U1}] \\
&\le \Pr^{\mathcal{A}}[C[G'_1] : D_0 \lor D_1 \lor D_{U1}] + \Pr^{\mathcal{A}}[C[G_2] : \text{distinguish}] \\
&\le \Pr^{\mathcal{A}}[C[G'_1] : (D_0 \lor D_1) \land \neg \text{NonUnique}_{G_1, D_1}] + \Pr^{\mathcal{A}}[C[G'_1] : D_{U1}] \\
&\phantom{\le \Pr^{\mathcal{A}}[C[G'_1] : (D_0 \lor D_1) \land \neg \text{NonUnique}_{G_1, D_1}]} + \Pr^{\mathcal{A}}[C[G_2] : \text{distinguish}] \\
&\le \Pr^{\mathcal{A}}[C[G'_1] : (D_0 \lor D_1) \land \neg \text{NonUnique}_{G_1, D_1}] + p(\mathcal{A}, C)
\end{align*}
$$

since $G'_1$ and $G_2$ execute events $D_{U1}$ in the same cases, and $D_{U1}$ and distinguish are mutually exclusive. Therefore, we have $D_{\neg EvUsed_1}, \emptyset : G'_0, D_{false}, EvUsed_0 \xrightarrow{V} p G'_1, D_1, EvUsed_1 \cup EvUsed_0$.

Currently, CryptoVerif can prove query_equiv only when the mapping $\phi$ is the identity for all variables. Other cases can be proved manually and used as assumptions in equiv statements.

## 3 Collecting True Facts

In this section, we consider only processes that satisfy Properties 3 and 4. We can assume without loss of generality that the adversary context also satisfies these properties: tables (insert and get) can be removed by encoding them using find by transformation expand_tables (Section 5.1.2) and variables defined in conditions of find can be renamed to have distinct names by transformation auto_SArename (Section 5.1.1).

Given a configuration Conf = $E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v$ or Conf = $E, St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$, we denote by $E_{Conf}$ the environment $E$ in configuration Conf. We denote by $E_{Tr \leq Conf}$ the union of $E_{Conf'}$ for all configurations Conf' $\leq_{Tr} Conf$ in Tr. It is a set of mappings $x[\tilde{a}] \mapsto b$. At this stage, it may include conflicting mappings $x[\tilde{a}] \mapsto b$ and $x[\tilde{a}] \mapsto b'$ with $b \neq b'$. We prove below (Lemma 29) that this situation never happens. The notation $E_{Tr \leq Conf}$ is useful because the environment computed in the semantics does not keep the values of variables defined in conditions of find after these conditions are evaluated. Considering the union of all environments of previous configurations allows us to recover the values of these variables, and to use them in the facts that we collect. Given a configuration Conf = $E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v$ or Conf = $E, (\sigma, P) :: St, Q, Or, \mathcal{T}, \mu\mathcal{E}v$, we denote by $\sigma_{Conf}$ the mapping sequence for replication indices $\sigma$ in the configuration Conf and by $\mu\mathcal{E}v_{Conf}$ the sequence of events $\mu\mathcal{E}v$ in configuration Conf.

Let us define Defined as in Section 2.4.3, except that

$$
Defined(\sigma, \mu^{\text{find}[\text{unique?}]})(\bigoplus_{j=1}^{m} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } \text{defined}(\tilde{M}_j) \land M_j \text{ then } N_j) \text{ else } N) = \\
\left(\biguplus_{j=1}^{m} \biguplus_{\tilde{a} \le \tilde{n}_j} Defined(\sigma[\tilde{i}_j \mapsto \tilde{a}], M_j)\right) \uplus \max\left(\max_{j=1}^{m} (\{\tilde{u}_j[\sigma(\tilde{i})]\} \uplus Defined(\sigma, N_j)), Defined(\sigma, N)\right)
$$

$$
Defined(\sigma, \mu^{\text{find}[\text{unique?}]})(\bigoplus_{j=1}^{m} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } \text{defined}(\tilde{M}_j) \land M_j \text{ then } P_j) \text{ else } P) = \\
\left(\biguplus_{j=1}^{m} \biguplus_{\tilde{a} \le \tilde{n}_j} Defined(\sigma[\tilde{i}_j \mapsto \tilde{a}], M_j)\right) \uplus \max\left(\max_{j=1}^{m} (\{\tilde{u}_j[\sigma(\tilde{i})]\} \uplus Defined(\sigma, P_j)), Defined(\sigma, P)\right)
$$

so that the variables defined in conditions of find are now considered as defined forever, and not
temporarily during the evaluation of the considered condition. We also define

$$Defined(Tr \preceq Conf) = \text{Dom}(E_{Tr \preceq Conf}) \uplus Defined^{\text{Fut}}(Conf).$$

**Lemma 29** Let $Q_0$ be a process that satisfies Properties 3 and 4. Let $Tr$ be a trace of $Q_0$ for any $A \in \mathcal{B}\mathcal{B}$ and $Conf$ be a configuration in the derivation of $Tr$. Then the following properties hold:

1. Defined($Tr \preceq Conf$) does not contain duplicate elements.

2. Each variable is defined at most once for each value of its array indices in $Tr$.

3. $E_{Tr \preceq Conf}$ contains at most one binding for each $x[\tilde{a}]$.

**Proof sketch** The proof is similar to the proof of Lemma 9. We first show as in Lemma 9 that, for all program points $\mu$ in $Q_0$, if $\text{Dom}(\sigma) = I_\mu$ are the current replication indices at $\mu$ and the process or term $Q$ at $\mu$ satisfies Invariant 1, then all elements of $Defined(\sigma, Q)$ are of the form $x[\tilde{a}]$ where $x \in \text{vardef}(Q)$ and $\text{Im}(\sigma)$ is a prefix of $\tilde{a}$.

Next, we show that, for all program points $\mu$, if $\text{Dom}(\sigma) = I_\mu$ are the current replication indices at $\mu$ and the process or term $Q$ at $\mu$ satisfies Invariant 1, then $Defined(\sigma, Q)$ does not contain duplicate elements. The proof proceeds by induction on $Q$. All multiset unions in the computation of $Defined(\sigma, Q)$ are disjoint unions by the property above, because either they use different extensions of $\sigma$ (cases of replication and of conditions of find) or they use disjoint variable definitions or subprocesses or subterms in the same branch of find or if, which must define different variables by Invariant 1 and by Property 4.

We show by induction on the derivations that, if $Conf \xrightarrow{p_1} Conf'$, then $Defined(Tr \preceq Conf) \supset Defined(Tr \preceq Conf')$ and for all semantic configurations $Conf''$ in the derivation of $Conf \xrightarrow{p_2} Conf'$, $Defined(Tr \preceq Conf) \supset Defined(Tr \preceq Conf'')$, and similarly with $\rightsquigarrow$ instead of $\xrightarrow{p_1}$. The first result follows: since $Q_0$ satisfies Invariant 1, $Defined(\sigma_0, Q_0)$ does not contain duplicate elements, where $\sigma_0$ is the empty mapping sequence. Let $Conf_0 = \{(\sigma_0, Q_0)\}$, $(\text{fo}(Q_0), \emptyset)$, $Conf_1 = \text{reduce}(\{(\sigma_0, Q_0)\}, (\text{fo}(Q_0), \emptyset))$, $Conf_2 = \text{initConfig}(Q_0, A)$, and $Conf_3$ be any other configuration of $Tr$. Then $Defined(Tr \preceq Conf_0)$, $Defined(Tr \preceq Conf_1)$, $Defined(Tr \preceq Conf_2)$, and therefore $Defined(Tr \preceq Conf_3)$ do not contain duplicate elements.

Let us prove the second result. In order to derive a contradiction, assume that two transitions $Conf_1 \xrightarrow{p_1} Conf'_1$ and $Conf_2 \xrightarrow{p_2} Conf'_2$ inside $Tr$ define the same variable $x[\tilde{a}]$.

* First case: one transition happens before the other, for instance $Conf'_1 \preceq Tr Conf_2$. (The case $Conf'_2 \preceq Tr Conf_1$ is symmetric.) Since $Conf_1 \xrightarrow{p_1} Conf'_1$ defines $x[\tilde{a}]$, we have $x[\tilde{a}] \in \text{Dom}(E_{Conf'_1})$, so $x[\tilde{a}] \in \text{Dom}(E_{Tr \preceq Conf_2})$. Moreover, since $Conf_2 \xrightarrow{p_2} Conf'_2$ defines $x[\tilde{a}]$, we have $x[\tilde{a}] \in Defined^{\text{Fut}}(Conf_2)$, by inspecting all rules that add elements to the environment. Therefore $Defined(Tr \preceq Conf_2) = \text{Dom}(E_{Tr \preceq Conf_2}) \uplus Defined^{\text{Fut}}(Conf_2)$ contains twice $x[\tilde{a}]$. Contradiction.

* Second case: the transitions cannot be ordered. By definition of $\preceq_{Tr}$, this can happen only when a semantic rule uses several derivations for its assumptions, which happens only in rules for find. (Recall that get is excluded by Property 3.) Therefore, there exists $k_1$ and $k_2$ such that $Conf_1 \xrightarrow{p_1} Conf'_1$ is in the derivation of $Conf_{0,k} = E, \sigma[i_{jk} \mapsto \tilde{a}_k], D_{jk} \wedge M_{jk}, T, \mu\mathcal{E}v \xrightarrow{p_k} Conf'_{0,k} = E_k, \sigma_k, r_k, T, \mu\mathcal{E}v$ with $v_k = (j_k, \tilde{a}_k)$ for $k = k_1$ and $Conf_2 \xrightarrow{p_2} Conf'_2$ is in that derivation for $k = k_2$, with $k_1 \neq k_2$. We have $x[\tilde{a}] \in Defined(Tr \preceq Conf'_{0,k_1}) \subseteq Defined(Tr \preceq Conf_{0,k_1}) = \text{Dom}(E_{Tr \preceq Conf_{0,k_1}}) \cup$
Defined($\sigma[i_{jk_1} \mapsto \tilde{a}_{k_1}]$, $M_{jk_1}$). Moreover, $Conf_{0,k} \preceq Conf_1$, so $\text{Dom}(E_{\text{Tr}\preceq\text{Conf}_{0,k_1}}) \subseteq \text{Dom}(E_{\text{Tr}\preceq\text{Conf}_1})$. Since $Conf_1 \xrightarrow{p_1} Conf'_1$ defines $x[\tilde{a}]$, we have $x[\tilde{a}] \in \text{Defined}^{\text{Fut}}(Conf_1)$, by inspecting all rules that add elements to the environment. Since $\text{Defined}(\text{Tr} \preceq Conf_1) = \text{Dom}(E_{\text{Tr}\preceq\text{Conf}_1}) \uplus \text{Defined}^{\text{Fut}}(Conf_1)$ does not contain duplicate elements, we have $x[\tilde{a}] \notin \text{Dom}(E_{\text{Tr}\preceq\text{Conf}_1})$, so $x[\tilde{a}] \notin \text{Dom}(E_{\text{Tr}\preceq\text{Conf}_{0,k_1}})$. Hence $x[\tilde{a}] \in \text{Defined}(\sigma[i_{jk_1} \mapsto \tilde{a}_{k_1}], M_{jk_1})$. Similarly, $x[\tilde{a}] \in \text{Defined}(\sigma[i_{jk_2} \mapsto \tilde{a}_{k_2}], M_{jk_2})$. Let us show that the sets $\text{Defined}(\sigma[i_{jk_1} \mapsto \tilde{a}_{k_1}], M_{jk_1})$ and $\text{Defined}(\sigma[i_{jk_2} \mapsto \tilde{a}_{k_2}], M_{jk_2})$ are disjoint. We have $v_{k_1} \neq v_{k_2}$, so either $j_{k_1} \neq j_{k_2}$ and in this case these sets are disjoint because $M_{jk_1}$ and $M_{jk_2}$ define different variables by Property 4, or $j_{k_1} = j_{k_2}$ and $\tilde{a}_{k_1} \neq \tilde{a}_{k_2}$ and in this case these sets are disjoint because they use different extensions of $\sigma$. Since these sets are disjoint, they cannot both contain $x[\tilde{a}]$. Contradiction.

The last result is an immediate consequence of the second one. $\square$

**Lemma 30** Let $Q_0$ be a process that satisfies Properties 3 and 4. Let $\text{Tr}$ be a trace of $Q_0$ for any $A \in \mathcal{A}$ and $Conf$ be a configuration in the derivation of $\text{Tr}$. We have $E_{\text{Tr}\preceq\text{Conf}} = E_{\text{Conf}}[x[\tilde{a}] \mapsto b$ for some variables $x$ defined in a condition of find and some indices $\tilde{a}$ and values $b]$.

**Proof sketch** By induction on the derivation. $\square$

The previous lemma shows that the only difference between $E_{\text{Conf}}$ and $E_{\text{Tr}\preceq\text{Conf}}$ is that variables defined in conditions of find are added to $E_{\text{Tr}\preceq\text{Conf}}$. These variables have no array accesses, so they do not appear in defined conditions of find. Therefore, these defined conditions yield the same result whether they are evaluated in $E_{\text{Conf}}$ or in $E_{\text{Tr}\preceq\text{Conf}}$.
We consider the following facts:

* The boolean term $M$ means that $M$ evaluates to true.

* $\text{defined}(M)$ means that $M$ is defined (all array accesses in $M$ are defined).

* $\text{event}(e(\tilde{M}))$ means that event $e(\tilde{M})$ has been executed.

* $\text{event}(e(\tilde{M}))@\tau$ means that event $e(\tilde{M})$ has been executed at step $\tau$ (index in the sequence of events $\mu\in\nu$).

* $M_1 : \text{event}(e(\tilde{M}))$ means that event $e(\tilde{M})$ has been executed with pair (program point, replication indices) equal to $M_1$.

* $M_1 : \text{event}(e(\tilde{M}))@\tau$ means that event $e(\tilde{M})$ has been executed at step $\tau$ with pair (program point, replication indices) equal to $M_1$.

* $\text{programpoint}(\mu, \tilde{M})$ means that program point $\mu$ has been executed with replication indices equal to $\tilde{M}$.

* $\text{programpoint}(S_1, \tilde{M}_1) \preceq \dots \preceq \text{programpoint}(S_m, \tilde{M}_m)$ means that, for $j \le m$, some program point $\mu_j \in S_j$ has been executed with replication indices equal to $\tilde{M}_j$, and furthermore these program points have been executed in the order of increasing $j$.

* $\text{lastdefprogrampoint}(\mu, \tilde{M})$ means that program point $\mu$ has been executed with replication indices equal to $\tilde{M}$ and the values of variables and replication indices are unchanged since that program point (that is, no variable definition nor oracle call, return, or yield that changes the replication indices was executed since that program point).
Given an environment $E$ mapping process variables to their values, an environment $\rho$ mapping replication indices and non-process variables of the formula $\varphi$ to their values, and a sequence of events $\mu\mathcal{E}v$, we define $E, \rho, \mu\mathcal{E}v \vdash \varphi$, meaning that $E, \rho, \mu\mathcal{E}v$ satisfy $\varphi$, as follows:

* $E, \rho, \mu\mathcal{E}v \vdash M$ if and only if $E, \rho, M \Downarrow true$.

* $E, \rho, \mu\mathcal{E}v \vdash \text{defined}(M)$ if and only if $E, \rho, M \Downarrow a$ for some $a$.

* $E, \rho, \mu\mathcal{E}v \vdash \text{event}(e(\tilde{M}))$ if and only if $E, \rho, \tilde{M} \Downarrow \tilde{a}$ and $(\mu, \tilde{a}') : e(\tilde{a}) \in \mu\mathcal{E}v$ for some $\mu$ and $\tilde{a}'$.

* $E, \rho, \mu\mathcal{E}v \vdash \text{event}(e(\tilde{M}))@M_0$ if and only if $E, \rho, \tilde{M} \Downarrow \tilde{a}, E, \rho, M_0 \Downarrow a_0$, and $\mu\mathcal{E}v(a_0) = (\mu, \tilde{a}') : e(\tilde{a})$ for some $\mu$ and $\tilde{a}'$.

* $E, \rho, \mu\mathcal{E}v \vdash M_1 : \text{event}(e(\tilde{M}))$ if and only if $E, \rho, \tilde{M} \Downarrow \tilde{a}, E, \rho, M_1 \Downarrow (\mu, \tilde{a}')$ and $(\mu, \tilde{a}') : e(\tilde{a}) \in \mu\mathcal{E}v$.

* $E, \rho, \mu\mathcal{E}v \vdash M_1 : \text{event}(e(\tilde{M}))@M_0$ if and only if $E, \rho, \tilde{M} \Downarrow \tilde{a}, E, \rho, M_0 \Downarrow a_0, E, \rho, M_1 \Downarrow (\mu, \tilde{a}')$, and $\mu\mathcal{E}v(a_0) = (\mu, \tilde{a}') : e(\tilde{a})$.

Logical connectives are defined as usual. When $\varphi$ does not contain events, $\mu\mathcal{E}v$ can be omitted, writing $E, \rho \vdash \varphi$.

Let $\mathcal{A}$ be an attacker in $\mathcal{BB}$ and $\text{Tr}$ be a trace of $Q_0$ for attacker $\mathcal{A}$. Let $\text{Conf} = E, \sigma, N, \mathcal{T}, \mu\mathcal{E}v$ or $\text{Conf} = E, \text{St}, \mathcal{Q}, \text{Or}, \mathcal{T}, \mu\mathcal{E}v$ be a configuration that occurs in the derivation of $\text{Tr}$. We define $\text{Tr} \preceq \text{Conf}, \rho \vdash \varphi$, meaning that the prefix of $\text{Tr}$ until $\text{Conf}$ satisfies the formula $\varphi$ with environment $\rho$ (giving values of non-process variables of $\varphi$) as follows:

* $\text{Tr} \preceq \text{Conf}, \rho \vdash F$ if and only if $E_{\text{Tr} \preceq \text{Conf}}, \sigma_{\text{Conf}} \cup \rho, \mu\mathcal{E}v_{\text{Conf}} \vdash F$, when $F$ is a term $M$, a defined fact $\text{defined}(M)$, or an event $\text{event}(e(\tilde{M}))$, $\text{event}(e(\tilde{M}))@M_0$, $M_1 : \text{event}(e(\tilde{M}))$, or $M_1 : \text{event}(e(\tilde{M}))@M_0$.

* $\text{Tr} \preceq \text{Conf}, \rho \vdash \text{programpoint}(S_1, \tilde{M}_1) \preceq \dots \preceq \text{programpoint}(S_m, \tilde{M}_m)$ if and only if, for all $j \in \{1, \dots, m\}$, there exists $\text{Conf}_j$ at program point $\mu_j \in S_j$ in $\text{Tr}$ such that $E_{\text{Tr} \preceq \text{Conf}}, \sigma_{\text{Conf}_j} \cup \rho, \tilde{M}_j \Downarrow \text{Im}(\sigma_{\text{Conf}_j})$ and $\text{Conf}_1 \preceq_{\text{Tr}} \dots \preceq_{\text{Tr}} \text{Conf}_m \preceq_{\text{Tr}} \text{Conf}$.

The fact $\text{programpoint}(\mu, \tilde{M})$ is actually a particular case of $\text{programpoint}(S_1, \tilde{M}_1) \preceq \dots \preceq \text{programpoint}(S_m, \tilde{M}_m)$ with $m = 1$ and $S_1 = \{\mu\}$. Hence, we have $\text{Tr} \preceq \text{Conf}, \rho \vdash \text{programpoint}(\mu, \tilde{M})$ if and only if there is a configuration $\text{Conf}'$ at program point $\mu$ in $\text{Tr}$ such that $\text{Conf}' \preceq_{\text{Tr}} \text{Conf}$ and $E_{\text{Tr} \preceq \text{Conf}}, \sigma_{\text{Conf}'}, \cup \rho, \tilde{M} \Downarrow \text{Im}(\sigma_{\text{Conf}'})$.

* $\text{Tr} \preceq \text{Conf}, \rho \vdash \text{lastdefprogrampoint}(\mu, \tilde{M})$ if and only if there is a configuration $\text{Conf}'$ at program point $\mu$ in $\text{Tr}$ such that $\text{Conf}' \preceq_{\text{Tr}} \text{Conf}, E_{\text{Tr} \preceq \text{Conf}'} = E_{\text{Tr} \preceq \text{Conf}}, \sigma_{\text{Conf}'} = \sigma_{\text{Conf}}$, and $E_{\text{Tr} \preceq \text{Conf}}, \sigma_{\text{Conf}} \cup \rho, \tilde{M} \Downarrow \text{Im}(\sigma_{\text{Conf}'})$.

Logical connectives are defined as usual. Most facts are evaluated in the environment $E_{\text{Tr} \preceq \text{Conf}}$ and the mapping sequence $\sigma_{\text{Conf}}$. Events are evaluated using the sequence of events $\mu\mathcal{E}v_{\text{Conf}}$ in $\text{Conf}$, but correspond to an execution of the event at some point before $\text{Conf}$ in the trace.

We define that a trace $\text{Tr}$ satisfies a logical formula $\varphi$ with environment $\rho$ (giving values of non-process variables of $\varphi$), denoted $\text{Tr}, \rho \vdash \varphi$ as $\text{Tr} \preceq \text{Conf}, \rho \vdash \varphi$, where $\text{Tr}$ ends with $\text{Conf}$. Along the same line, we define $E_{\text{Tr}} = E_{\text{Tr} \preceq \text{Conf}}$ and $\mu\mathcal{E}v_{\text{Tr}} = \mu\mathcal{E}v_{\text{Conf}}$ where $\text{Tr}$ ends with $\text{Conf}$.

When the formula $\varphi$ does not contain free non-process variables, we may write $\text{Tr} \vdash \varphi$ instead of $\text{Tr}, \rho \vdash \varphi$ since the environment $\rho$ is useless. When $\mathcal{F}$ is a set of formulas (in particular, of
facts), we write $\bigwedge \mathcal{F}$ for $\bigwedge_{F \in \mathcal{F}} F$ and $\bigvee \mathcal{F}$ for $\bigvee_{F \in \mathcal{F}} F$. We also write $Tr, \rho \vdash \mathcal{F}$ when for all $\varphi \in \mathcal{F}$, $Tr, \rho \vdash \varphi$. This is equivalent to $Tr, \rho \vdash \bigwedge \mathcal{F}$. We use similar notations for prefixes $Tr \preceq Conf$ instead of traces $Tr$.

Additionally, we define the following facts:

* $[\exists \mathit{find}((i_1 \le n_1, \dots, i_m \le n_m), (M_1, \dots, M_l), M)] = \forall i_1 \in [1, n_1], \dots, \forall i_m \in [1, n_m], \neg(\mathit{defined}(M_1) \wedge \dots \wedge \mathit{defined}(M_l) \wedge M)$.

* $[\exists \mathit{let}(\tilde{x} : \tilde{T}, N, M)] = \forall \tilde{x} \in \tilde{T}, N \neq M$.

**Extension:** The following description is based on the first version of the collection of known facts. Many improvements and extensions have been implemented. In particular, the following description often uses $P$ instead of $\mu$ for program points; the syntax does not allow $\stackrel{R}{\leftarrow}$, if, let, find in terms; events are not handled.

## 3.1 User-defined Rewrite Rules

The user can give two kinds of information:

* claims of the form $\forall x_1 : T_1, \dots, \forall x_m : T_m, M$ which mean that for all environments $E$, if for all $j \le m$, $E(x_j) \in T_j$, then $E, M \downarrow$ true.

Such claims must be well-typed, that is, $\{x_1 \mapsto T_1, \dots, x_m \mapsto T_m\} \vdash M : \mathit{bool}$.

They are translated into rewrite rules as follows:

- If $M$ is of the form $M_1 = M_2$ and $\mathit{vardef}(M_2) \subseteq \mathit{vardef}(M_1)$, we generate the rewrite rule $\forall x_1 : T_1, \dots, \forall x_m : T_m, M_1 \to M_2$.

- If $M$ is of the form $M_1 \neq M_2$, we generate the rewrite rules $\forall x_1 : T_1, \dots, \forall x_m : T_m, (M_1 = M_2) \to \text{false}, \forall x_1 : T_1, \dots, \forall x_m : T_m, (M_1 \neq M_2) \to \text{true}$. (Such rules are used for instance to express that different constants are different.)

- Otherwise, we generate the rewrite rule $\forall x_1 : T_1, \dots, \forall x_m : T_m, M \to \text{true}$.

The term $M$ reduces into $M'$ by the rewrite rule $\forall x_1 : T_1, \dots, \forall x_m : T_m, M_1 \to M_2$ if and only if $M = C[\sigma M_1]$, $M' = C[\sigma M_2]$, where $C$ is a term context and $\sigma$ is a substitution that maps $x_j$ to any term of type $T_j$ for all $j \le m$.

* claims of the form $y_1 \stackrel{R}{\leftarrow} T'_1, \dots, y_l \stackrel{R}{\leftarrow} T'_l, \forall x_1 : T_1, \dots, \forall x_m : T_m, M_1 \approx_p M_2$ with $\mathit{vardef}(M_2) \subseteq \mathit{vardef}(M_1)$. Informally, these claims mean that $M_1$ and $M_2$ evaluate to the same bitstring except in cases of probability at most $p$, provided that $y_1, \dots, y_l$ are chosen randomly with uniform probability and independently among $T'_1, \dots, T'_l$ respectively, and that $x_1, \dots, x_m$ are of type $T_1, \dots, T_m$. ($x_1, \dots, x_m$ may depend on $y_1, \dots, y_l$.) Formally, these claims are defined as:

$$ \begin{array}{l} \Pr[E(y_1) \stackrel{R}{\leftarrow} T'_1; \dots E(y_l) \stackrel{R}{\leftarrow} T'_l; \\ \qquad (E(x_1), \dots, E(x_m)) \leftarrow \mathcal{A}(E(y_1), \dots, E(y_l)); \\ \qquad E, M_1 \downarrow a; E, M_2 \downarrow a' : a \neq a'] \le p(\mathcal{A}) \end{array} $$

where $\mathcal{A}$ is an attacker in BB.

The above claim must be well-typed, that is, $\{x_1 \mapsto T_1, \dots, x_m \mapsto T_m, y_1 \mapsto T'_1, \dots, y_l \mapsto T'_l\} \vdash M_1 = M_2$.

This claim is translated into the rewrite rule $y_1 \stackrel{R}{\leftarrow} T'_1, \dots, y_l \stackrel{R}{\leftarrow} T'_l, \forall x_1 : T_1, \dots, \forall x_m : T_m, M_1 \to M_2$.
The prover has built-in rewrite rules for defining boolean functions:

$$ \neg true \rightarrow false \qquad \neg false \rightarrow true \qquad \forall x : bool, \neg(\neg x) \rightarrow x $$

$$ \forall x : T, \forall y : T, \neg(x = y) \rightarrow x \neq y $$

$$ \forall x : T, \forall y : T, \neg(x \neq y) \rightarrow x = y $$

$$ \forall x : T, x = x \rightarrow true \qquad \forall x : T, x \neq x \rightarrow false $$

$$ \forall x : bool, \forall y : bool, \neg(x \land y) \rightarrow (\neg x) \lor (\neg y) $$

$$ \forall x : bool, \forall y : bool, \neg(x \lor y) \rightarrow (\neg x) \land (\neg y) $$

$$ \forall x : bool, x \land true \rightarrow x \qquad \forall x : bool, x \land false \rightarrow false $$

$$ \forall x : bool, x \lor true \rightarrow true \qquad \forall x : bool, x \lor false \rightarrow x $$

$$ \forall x : T, \forall y : T, \text{if\_fun}(true, x, y) \rightarrow x \qquad \forall x : T, \forall y : T, \text{if\_fun}(false, x, y) \rightarrow y $$

$$ \forall x : bool, \forall y : T, \text{if\_fun}(x, y, y) \rightarrow y $$

$$ \forall x_1 : T_1, \dots, \forall x_m : T_m, \forall x : bool, \forall y : T_k, \forall z : T_k, \\ f(x_1, \dots, x_{k-1}, \text{if\_fun}(x, y, z), x_{k+1}, \dots, x_m) \rightarrow \\ \text{if\_fun}(x, f(x_1, \dots, x_{k-1}, y, x_{k+1}, \dots, x_m), f(x_1, \dots, x_{k-1}, z, x_{k+1}, \dots, x_m)) \\ \text{when } f : T_1 \times \dots \times T_m \rightarrow T \text{ has option } \mathbf{autoSwapIf} $$

The prover also has support for commutative function symbols, that is, binary function symbols $f : T \times T \rightarrow T'$ such that for all $x, y \in T$, $f(x, y) = f(y, x)$. For such symbols, all equality and matching tests are performed modulo commutativity. The functions $\land$, $\lor$, $=$, and $\neq$ are commutative. So, for instance, the rewrite rules above may also be used to rewrite $true \land M$ into $M$, $false \land M$ into false, $true \lor M$ into true, and $false \lor M$ into $M$. Used-defined functions may also be declared commutative; xor is an example of such a commutative function.

**Example 4** For example, considering MAC and encryption schemes as in Definitions 2 and 3 respectively, we have:

$$ \forall k : T_{mk}, \forall m : \text{bitstring}, \qquad \text{mac} \\ \text{verify}(m, k, \text{mac}(m, k)) = \text{true} $$

$$ \forall m : \text{bitstring}; \forall k : T_k, \forall r : T_r, \qquad \text{enc} \\ \text{dec}(\text{enc}(m, k, r), k) = i_{\perp}(m) $$

We express the poly-injectivity of the function k2b of Example 1 by

$$ \forall x : T_k, \forall y : T_k, (\text{k2b}(x) = \text{k2b}(y)) = (x = y) \qquad \text{(k2b)} \\ \forall x : T_k, \text{k2b}^{-1}(\text{k2b}(x)) = x $$

where $\text{k2b}^{-1}$ is a function symbol that denotes the inverse of k2b. We have similar formulas for $i_{\perp}$.

## 3.2 Collecting True Facts from a Game

We use facts to represent properties that hold at certain program points in processes. We consider two kinds of facts: defined($M$) means that $M$ is defined, and a term $M$ means that $M$ is true (the boolean term $M$ evaluates to true). In this section, we show how to compute a set of facts $\mathcal{F}_{\mu}$ that are guaranteed to hold at the program point $\mu$ of the game.
The function collectFacts collects facts that hold at each program point of the game. More precisely, for each program point $\mu$ in the game, it computes a set $\mathcal{F}_{\mu}$ of facts that hold at that program point. The function collectFacts also computes a set $\mathcal{D}$ containing pairs $(x[\tilde{i}], \mu)$ where $x[\tilde{i}]$ has been defined immediately above program point $\mu$. (If there are several definitions of $x$, there is one such pair for each definition of $x$.) Finally, for oracle bodies $P$, collectFacts($P$) returns a set of facts that will hold when the return is executed and stores this set in $\mathcal{F}_{\mu}^{\text{Fut}}$. (The superscript Fut stands for *future*, since these facts do not hold yet at $P$, but will hold in the future.)

The function collectFacts is defined in Figure 18. It is initially called by collectFacts($Q_0$). It takes into account that $x[\tilde{i}]$ may be defined by an oracle definition, a random choice, a let, or a find and updates $\mathcal{D}$ accordingly. Furthermore, when we execute let $x[\tilde{i}] : T = M$ in $P'$, $x[\tilde{i}] = M$ holds in $P'$ and $x[\tilde{i}]$ is defined in $P'$. When we execute find $(\bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \text{ suchthat } \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j)$ else $P'$, $u_{j1}[\tilde{i}], \dots, u_{jm_j}[\tilde{i}], \sigma M_{j1}, \dots, \sigma M_{jl_j}$ are defined in $P_j$, $\sigma M_j$ holds in $P_j$ where $\sigma = \{u_{j1}[\tilde{i}]/i_{j1}, \dots, u_{jm_j}[\tilde{i}]/i_{jm_j}\}$, and $\neg M_j$ holds in $P'$ when $m_j = l_j = 0$.

After calling collectFacts($Q_0$), we complete the computed sets $\mathcal{F}_P$ (where $P$ may be an oracle definition or body) by adding facts that come from processes above $P$:

$$ \mathcal{F}_P \leftarrow \mathcal{F}_P \cup \mathcal{F}_{P'} \text{ if } P \text{ is immediately under } P' $$

We also add facts that we can deduce from facts defined($M$). Precisely, if defined($M$) $\in \mathcal{F}_P$ and $x[M_1, \dots, M_m]$ is a subterm of $M$, then we take into account facts that are known to be true at the definitions of $x$ by adding them to $\mathcal{F}_P$ as follows:

$$ \mathcal{F}_P \leftarrow \mathcal{F}_P \cup \left( \bigcap_{(x[i_1, \dots, i_m], P') \in \mathcal{D}} \left\{ \begin{array}{ll} \sigma(\mathcal{F}_{P'} \cup (\mathcal{F}_{P'}^{\text{Fut}} \cap \mathcal{F}_P)) & \text{if } P \text{ is under } P' \\ \sigma(\mathcal{F}_{P'} \cup \mathcal{F}_{P'}^{\text{Fut}}) & \text{otherwise} \end{array} \right. \right) $$

where $\sigma = \{M_1/i_1, \dots, M_m/i_m\}$. Indeed, if defined($M$) $\in \mathcal{F}_P$ and $x[M_1, \dots, M_m]$ is a subterm of $M$, then $x[M_1, \dots, M_m]$ is defined at $P$, so some definition of $x[M_1, \dots, M_m]$, immediately above the process $P'$, must have been executed before reaching $P$, so the facts that hold at $P'$ also hold at $P$, with a suitable substitution of indices: we have $\sigma\mathcal{F}_{P'}$, that is, $\mathcal{F}_{P'}\{M_1/i_1, \dots, M_m/i_m\}$. Moreover, if the occurrence $P$ is not syntactically under the occurrence $P'$, then the code of $P'$ must have been executed until the next return before yielding control to some other code and reaching $P$, so in fact $\sigma(\mathcal{F}_{P'} \cup \mathcal{F}_{P'}^{\text{Fut}})$ hold. If $P$ is syntactically under $P'$, it is possible that the code of $P'$ has been executed until reaching $P$ instead of until reaching the next return or yield, so we have only $\sigma(\mathcal{F}_{P'} \cup (\mathcal{F}_{P'}^{\text{Fut}} \cap \mathcal{F}_P))$. If there are several definitions of $x$, we do not know which one has been executed, so we only add to $\mathcal{F}_P$ the facts that hold in all cases, by taking the intersection on all definitions of $x$.

This operation may add new defined facts to $\mathcal{F}_P$, so it is executed until a fixpoint is reached, except that, in order to avoid infinite loops, we do not execute this step for definitions defined($M$) in which $M$ contains nested occurrences of the same symbol (such as $x[\dots x[\dots] \dots]$).

We also consider an additional fact that serves in expressing that the condition part of a find failed. Precisely, the fact elsefind((i1 ≤ n1, ..., im ≤ nm), (M1, ..., Ml), M) means that for all i1 ∈ [1, n1], ..., im ∈ [1, nm], the terms M1, ..., Ml are not all defined or M is false. The function collectElseFind described in Figure 19 collects elsefind facts that hold at each occurrence. The function collectElseFind($P, \mathcal{F}$) is called when $\mathcal{F}$ is the set of true elsefind facts at occurrence $P$. It sets the value of $\mathcal{F}_{\mathcal{P}}^{\text{ElseFind}}$ to $\mathcal{F}$.
collectFacts($Q$) =
  if $Q = Q_1 | Q_2$ then collectFacts($Q_1$); collectFacts($Q_2$)

if $Q = \text{foreach } i \le n \text{ do } Q'$ then collectFacts($Q'$)

if $Q = \text{newOracle } O; Q'$ then collectFacts($Q'$)

if $Q = O[\tilde{i}](x[\tilde{i}] : T) := P$ then

$$ \mathcal{F}_P = \{\text{defined}(x[\tilde{i}])\}; \mathcal{F}_P^{\text{Fut}} = \text{collectFacts}(P) $$

$$ \mathcal{D} = \mathcal{D} \cup \{(x[\tilde{i}], P)\} $$

collectFacts($P$) =
  if $P = \text{return } (N)$; $Q$ then collectFacts($Q$); return $\emptyset$

if $P = x[\tilde{i}] \stackrel{R}{\leftarrow} T; P'$ then

$$ \mathcal{F}_{P'} = \{\text{defined}(x[\tilde{i}])\}; \mathcal{F}_{P'}^{\text{Fut}} = \text{collectFacts}(P') $$

$$ \mathcal{D} = \mathcal{D} \cup \{(x[\tilde{i}], P')\}; \text{ return } \mathcal{F}_{P'} \cup \mathcal{F}_{P'}^{\text{Fut}} $$

if $P = \text{let } x[\tilde{i}] : T = M$ in $P'$ then

$$ \mathcal{F}_{P'} = \{\text{defined}(x[\tilde{i}]), x[\tilde{i}] = M\} $$

$$ \mathcal{F}_{P'}^{\text{Fut}} = \text{collectFacts}(P') $$

$$ \mathcal{D} = \mathcal{D} \cup \{(x[\tilde{i}], P')\}; \text{ return } \mathcal{F}_{P'} \cup \mathcal{F}_{P'}^{\text{Fut}} $$

if $P = \text{find} \left( \bigoplus_{j=1}^{m} u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \right.$
\qquad suchthat $\text{defined}(M_{j1}, \dots, M_{j_{l_j}}) \land M_j$ then $P_j$ else $P'$

then
for each $j \le m$,

$$ \begin{gathered} \mathcal{F}_{P_j} = \{\text{defined}(u_{j1}[\tilde{i}]), \dots, \text{defined}(u_{jm_j}[\tilde{i}]), \text{defined}(\sigma M_{j1}), \dots, \text{defined}(\sigma M_{j_{l_j}}), \sigma M_j\} \\ \text{where } \sigma = \{u_{j1}[\tilde{i}]/i_{j1}, \dots, u_{jm_j}[\tilde{i}]/i_{jm_j}\} \end{gathered} $$

$$ \mathcal{F}_{P_j}^{\text{Fut}} = \text{collectFacts}(P_j); $$

$$ \mathcal{D} = \mathcal{D} \cup \{(u_{j1}[\tilde{i}], P_j), \dots, (u_{jm_j}[\tilde{i}], P_j)\} $$

$$ \mathcal{F}_{P'} = \{\neg M_j \mid m_j = l_j = 0\}; \mathcal{F}_{P'}^{\text{Fut}} = \text{collectFacts}(P') $$

$$ \text{return } (\mathcal{F}_{P'} \cup \mathcal{F}_{P'}^{\text{Fut}}) \cap \bigcap_{j=1}^{m} (\mathcal{F}_{P_j} \cup \mathcal{F}_{P_j}^{\text{Fut}}) $$

<caption>Figure 18: The function collectFacts</caption>
collectElseFind($Q$) =
  if $Q = Q_1 | Q_2$ then collectElseFind($Q_1$); collectElseFind($Q_2$)
  if $Q = \text{foreach } i \le n \text{ do } Q'$ then collectElseFind($Q'$)
  if $Q = \text{newOracle } O; Q'$ then collectElseFind($Q'$)
  if $Q = O[\tilde{i}](x[\tilde{i}] : T) := P$ then collectElseFind($P, \emptyset$)

collectElseFind($P, \mathcal{F}$) =
  $\mathcal{F}_P^{\text{ElseFind}} = \mathcal{F}$
  if $P = \text{return } (N); Q$ then collectElseFind($Q$)
  if $P = x[\tilde{i}] \stackrel{R}{\leftarrow} T; P'$ or $P = \text{let } x[\tilde{i}] : T = M \text{ in } P'$ then
    $\mathcal{F}' = \{ \text{elsefind}((\tilde{i}' \le \tilde{n}), (M'_1, \dots, M'_l), M') \in \mathcal{F} \mid x \text{ does not occur in } M'_1, \dots, M'_l \}$
    collectElseFind($P', \mathcal{F}'$)
  if $P = \text{find} \left( \bigoplus_{j=1}^m u_{j1}[\tilde{i}] = i_{j1} \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] = i_{jm_j} \le n_{jm_j} \middle| \text{suchthat } \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j \right) \text{ else } P'$
  then
    for each $j \le m$,
      $\mathcal{F}_j' = \{ \text{elsefind}((\tilde{i}' \le \tilde{n}), (M'_1, \dots, M'_l), M') \in \mathcal{F} \mid u_{j1}, \dots, u_{jm_j} \text{ do not occur in } M'_1, \dots, M'_l \}$
      collectElseFind($P_j, \mathcal{F}_j'$)
      $\sigma_j = \{i_1/i_{j1}, \dots, i_{m_j}/i_{jm_j}\}$
      collectElseFind($P', \mathcal{F} \cup \{ \text{elsefind}((i_1 \le n_{j1}, \dots, i_{m_j} \le n_{jm_j}), \sigma_j(M_{j1}, \dots, M_{jl_j}), \sigma_j M_j) \mid j \in \{1, \dots, m\} \})$

<caption>Figure 19: The function collectElseFind</caption>
* In the case of random choices, assignments, and then branches of find, it takes into account that a variable $x$ or $u_{j1}, \dots, u_{jm_j}$ is newly defined. Hence `elsefind` facts that claim that one of these variables is not defined are removed.

* In the case of the else branch of a find, it adds the new `elsefind` facts that hold when the conditions of the find fail. These conditions express that each then branch of the find fails by a `elsefind` fact. To construct this fact, we replace (by applying $\sigma_j$) the indices $i_{j1}, \dots, i_{jm_j}$ with fresh indices $i_1, \dots, i_m$, respectively.

* In the case of a return, any code may be executed before the oracle definition under it, so any variable may be defined by that code, and all `elsefind` facts are removed. That is why the function `collectElseFind` for oracle definitions has no $\mathcal{F}$ argument (this argument would always be empty) and calls `collectElseFind(P, \emptyset)` for processes $P$ that follow an oracle definition. The situation is similar for an oracle call inside an oracle body.

The `elsefind` facts can be used to add new facts to the facts $\mathcal{F}_P$. Indeed, if $\mathcal{F}_P$ implies that $M_1, \dots, M_l$ are defined for some values of $i_1, \dots, i_m$, then the fact `elsefind((i_1 \le n_1, \dots, i_m \le n_m), (M_1, \dots, M_l), M)$ implies that $M$ is false for these values of $i_1, \dots, i_m$. Precisely, we define

$$ \begin{array}{l} \text{convert\_elsefind}(\mathcal{F}^{\text{ElseFind}}, \mathcal{F}) = \{\neg \sigma M \mid \\ \quad \text{elsefind}((i_1 \le n_1, \dots, i_m \le n_m), (M_1, \dots, M_l), M) \in \mathcal{F}^{\text{ElseFind}}, \text{Dom}(\sigma) = \{i_1, \dots, i_m\}, \\ \quad \text{for each } j \in \{1, \dots, l\}, \sigma M_j \text{ is a subterm of } M'_j \text{ and } \text{defined}(M'_j) \in \mathcal{F}\} \end{array} $$

The possible images of $\sigma$ are found by exploring the set of defined facts in $\mathcal{F}_P$. We execute:

$$ \mathcal{F}_P \leftarrow \mathcal{F}_P \cup \text{convert\_elsefind}(\mathcal{F}_P^{\text{ElseFind}}, \mathcal{F}_P) $$

In the implementation, an additional fact expresses that a pattern-matching failed: in the else branch of let $N = M$ in $P$ else $Q$, we know that $\forall x_1, \dots, x_l, N \neq M$, where $x_1, \dots, x_l$ are the variables bound in the pattern $N$. In this report, we consider that the pattern-matching is encoded using assignments and tests, so we do not consider this fact further.

Furthermore, when the previous update of $\mathcal{F}_P$ adds facts, we again complete the computed sets $\mathcal{F}_P$ by adding facts that come from processes above $P$:

$$ \mathcal{F}_P \leftarrow \mathcal{F}_P \cup \mathcal{F}_{P'} \text{ if } P \text{ is immediately under } P' $$

We could also iterate the addition of consequences of defined facts. (However, for simplicity, the current implementation does not perform such an iteration.)

$$ \text{We have } \text{programpoint}(\mu, I_{\mu}) \in \mathcal{F}_{\mu}. $$

**Lemma 31** Let $C$ be an evaluation context acceptable for $Q_0$, $A$ an attacker in $\mathcal{BB}$, $Tr$ be a trace of $C[Q_0]$ for $A$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_{\mu}$ be computed in $Q_0$. If a configuration $\text{Conf}$ is at program point $\mu$ in $Tr$, then $Tr \preceq \text{Conf} \vdash \mathcal{F}_{\mu}$.

When a single variable can be defined at multiple distinct program points, the basic version presented previously of the collected facts only contains the intersection of what holds at all the possible definitions points. A more refined version of $\mathcal{F}_{\mu}$ has also been implemented, that allows distinguishing cases depending on the multiple possible program points at which a variable is defined, generating several $\mathcal{F}_{\mu,c}$ for the various cases $c$. This more refined version is easily leveraged within proofs, simply by checking that a fact holds in all the possible cases over $c$. Note that more refined versions could be made by increasing the possible set of cases, but this would increase the overall complexity of the proof search. For this version, we have:
**Lemma 32** Let $C$ be an evaluation context acceptable for $Q_0$, $\mathcal{A}$ an attacker in $\mathcal{BB}$, $\text{Tr}$ be a trace of $C[Q_0]$ for $\mathcal{A}$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_{\mu,c}$ be computed in $Q_0$. If a configuration $\text{Conf}$ is at program point $\mu$ in $\text{Tr}$, then there exists a $c$ such that $\text{Tr} \preceq \text{Conf} \vdash \mathcal{F}_{\mu,c}$.

$\mathcal{F}_{\mu}$ can be seen as a particular case of $\mathcal{F}_{\mu,c}$ by considering a single case $c$.

**Corollary 3** Let $C$ be an evaluation context acceptable for $Q_0$, $\mathcal{A}$ an attacker in $\mathcal{BB}$, $\text{Tr}$ be a trace of $C[Q_0]$ for $\mathcal{A}$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_{\mu}$ (resp. $\mathcal{F}_{\mu,c}$) be computed in $Q_0$. Let $\text{Conf}$ be a configuration at program point $\mu$ in $\text{Tr}$. Let $\theta$ be a renaming of $I_{\mu}$ to fresh replication indices and $\rho = \{\theta I_{\mu} \mapsto \sigma_{\text{Conf}} I_{\mu}\}$. Let $\text{Conf}'$ be a term or oracle body configuration in $\text{Tr}$ such that $\text{Conf} \preceq_{\text{Tr}} \text{Conf}'$.

We have $\text{Tr} \preceq \text{Conf}'$, $\rho \vdash \theta \mathcal{F}_{\mu}$ and there exists a $c$ such that $\text{Tr} \preceq \text{Conf}'$, $\rho \vdash \theta \mathcal{F}_{\mu,c}$.

In particular, $\text{Tr}$, $\rho \vdash \theta \mathcal{F}_{\mu}$ and there exists a $c$ such that $\text{Tr}$, $\rho \vdash \theta \mathcal{F}_{\mu,c}$.

**Proof** By Lemma 31, $\text{Tr} \preceq \text{Conf} \vdash \mathcal{F}_{\mu}$. By Lemma 32, there exists a $c$ such that $\text{Tr} \preceq \text{Conf} \vdash \mathcal{F}_{\mu,c}$. Let $\mathcal{F} = \mathcal{F}_{\mu}$ (resp. $\mathcal{F} = \mathcal{F}_{\mu,c}$) such that $\text{Tr} \preceq \text{Conf} \vdash \mathcal{F}$. By definition of $\rho$, we have $\text{Tr} \preceq \text{Conf}$, $\rho \vdash \theta \mathcal{F}$. Since $\text{Conf} \preceq_{\text{Tr}} \text{Conf}'$, the environment $E_{\text{Tr} \preceq_{\text{Conf}'}}$ is an extension of $E_{\text{Tr} \preceq_{\text{Conf}'}}$, so the terms and defined facts in $\theta \mathcal{F}$ are preserved when considering $\text{Tr} \preceq \text{Conf}'$ instead of $\text{Tr} \preceq \text{Conf}$. (They do not use $\sigma_{\text{Conf}}$, resp. $\sigma_{\text{Conf}'}$, by the renaming $\theta$.) Moreover, by Lemma 3, $\mu \in \text{Conf}'$ is an extension of $\mu \in \text{Conf}$, so the events are also preserved. By definition of $\text{Tr} \preceq \text{Conf}$, $\rho \vdash \text{programpoint}(S_1, \tilde{M}_1) \preceq \dots \preceq \text{programpoint}(S_m, \tilde{M}_m)$, the sequences of program points $\text{programpoint}(S_1, \tilde{M}_1) \preceq \dots \preceq \text{programpoint}(S_m, \tilde{M}_m)$ are also preserved. Since $\mathcal{F}$ is a set of facts containing only terms, defined facts, events, and sequences of program points, we conclude that $\text{Tr} \preceq \text{Conf}'$, $\rho \vdash \theta \mathcal{F}$.

The last point is obtained by choosing $\text{Conf}'$ to be the last configuration of $\text{Tr}$. $\square$

**Lemma 33** Let $C$ be an evaluation context acceptable for $Q_0$, $\mathcal{A}$ an attacker in $\mathcal{BB}$, $\text{Tr} = \text{initConfig}(C[Q_0], \mathcal{A}) \xrightarrow{p} \dots \xrightarrow{p'} E$, $(\sigma, P) :: St, Q, Or, T, \mu \in \text{Conf}$ be a trace for $\mathcal{A}$ that does not execute any non-unique event of $Q_0$ with $P = \text{return} (a)$; $Q$ for some $a$ and $Q$ or $P = \text{yield}$ or $P = \text{abort}$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_{\mu}^{\text{Fut}}$ be computed in $Q_0$. If the configuration $\text{Conf}$ is at program point $\mu$ in $\text{Tr}$ and no executed process in the configurations between the configuration at the end of reduction step that contains $\text{Conf}$ (included) and $E$, $(\sigma, P) :: St, Q, Or, T, \mu \in \text{Conf}$ (excluded) is of the form $\text{return} (a)$; $Q$ for some $a$ and $Q$ or $\text{yield}$ (when $\text{Conf}$ is a process configuration with process $\text{return} (a)$; $Q$ for some $a$ and $Q$ or $\text{yield}$, we have $\text{Conf} = E$, $(\sigma, P) :: St, Q, Or, T, \mu \in \text{Conf}$), then $\text{Tr} \vdash \mathcal{F}_{\mu}^{\text{Fut}}$.

## 3.3 Local Dependency Analysis

For each program point $P$ and each variable $x$, the local dependency analysis tries to find which variables and terms depend on $x[i]$ at program point $P$, where $i$ denotes the current replication indices at the definition of $x$. It simplifies the game on-the-fly when possible.

For each occurrence of a process $P$ and each variable $x$ such that a random choice $x \stackrel{R}{\leftarrow} T$ occurs above $P$ and $T$ is a large type, we compute a set of terms $\text{indep}_P(x)$ that are independent of $x[i]$ where $i$ denotes the current replication indices at the definition of $x$.

For each occurrence of a process $P$ and each variable $x$ such that a random choice $x \stackrel{R}{\leftarrow} T$ occurs above $P$ and $T$ is a large type, we also compute $\text{depend}_P(x)$ which can be either $\top$ (I don't know) or a set of pairs $(y, M)$ where $y[i]$ depends on $x[i]$ by assignments, and $M$ is a term defining $y[i]$ as a function of $x[i]$. (The tuple $i$ denotes the current replication indices at the definition of $x$ and of $y$.)
$$
\begin{align*}
\text{depAnal}(Q, \text{indep}) &= \\
& \quad \forall y, \text{depend}_Q(y) = \top; \text{indep}_Q = \text{indep} \\
& \quad \text{if } Q = Q_1 | Q_2 \text{ then } \text{depAnal}(Q_1, \text{indep}); \text{depAnal}(Q_2, \text{indep}) \\
& \quad \text{if } Q = \text{foreach } i \le n \text{ do } Q' \text{ then } \text{depAnal}(Q', \text{indep}) \\
& \quad \text{if } Q = \text{newOracle } O; Q' \text{ then } \text{depAnal}(Q', \text{indep}) \\
& \quad \text{if } Q = O[\tilde{i}](x[\tilde{i}] : T) := P \text{ then } \text{depAnal}(P, \{\forall y, y \mapsto \top\}, \text{indep})
\end{align*}
$$

<caption>Figure 20: Local dependency analysis (1)</caption>

We define “M characterizes a part of $x[\tilde{i}]$ at P” as follows. Let $\alpha$ be defined by $\alpha(f(M_1, \dots, M_m)) = f(\alpha M_1, \dots, \alpha M_m)$; $\alpha(i) = i$ where $i$ is a replication index; $\alpha(M') = M'$ when $M' \in \text{indep}_P(x)$; $\alpha(y[M_1, \dots, M_{m'}]) = y[\alpha M_1, \dots, \alpha M_{m'}]$ when $y \neq x$ and $y$ either is defined only by random choices or $\text{depend}_P(x) \neq \top$ and $(y, M') \notin \text{depend}_P(x)$ for any $M'$; $\alpha(y[M_1, \dots, M_{m'}]) = y'[\alpha M_1, \dots, \alpha M_{m'}]$ where $y'$ is a fresh variable, otherwise. We write $y' = \alpha y$ in this case. We say that M characterizes a part of $x[\tilde{i}]$ at P when $\alpha M = M$ implies $f_1(\dots f_k((\alpha x)[\tilde{i}])) = f_1(\dots f_k(x[\tilde{i}]))$ for some uniform functions $f_1, \dots, f_k$, where $x[\tilde{i}]$ is a subterm of M, $(\alpha x)[\tilde{i}]$ is a subterm of $\alpha M$, $T'$ is the type of the result of $f_1$ (or of $x$ when $k=0$), and $T'$ is a large type. In that case, the value of M uniquely determines the value of $f_1(\dots f_k(x[\tilde{i}]))$. This property is shown by a simple rewriting prover, as in the global dependency analysis.

We denote by subterms(*M*) the set of subterms of the term *M*.

We say that *M* does not depend on *x* at *P* when *M* is built by function applications from terms in indep<sub>*P*</sub>(*x*), replications indices, and terms *y*[*M*<sub>1</sub>, ..., *M*<sub>*m*</sub>] such that *M*<sub>1</sub>, ..., *M*<sub>*m*</sub> do not depend on *x* at *P*, *y* ≠ *x*, and either *y* is defined only by random choices or depend<sub>*P*</sub>(*x*) ≠ ⊤ and *y* ≠ *y'* for all (*y*', *M*') ∈ depend<sub>*P*</sub>(*x*). Since terms in indep<sub>*P*</sub>(*x*) do not depend on *x*[*tilde;i*] and when depend<sub>*P*</sub>(*x*) ≠ ⊤, variables not in the first component of depend<sub>*P*</sub>(*x*) do not depend on *x*[*tilde;i*], the conditions above guarantee that *M* does not depend on *x*[*tilde;i*], where *tilde;i* are the current replication indices at the definition of *x*.

When depend ≠ ⊤, we denote by M depend the term obtained from M by replacing y[tilde{i}] with
M' for each (y, M') ∈ depend, where tilde{i} denotes the replication indices at the definition of y.

We define simplifyTerm such that simplifyTerm(M, P) is a simplified version of M, equal to
M except in cases of negligible probability. The term simplifyTerm(M, P) is defined as follows:

* Case 1: *M* is *M*<sub>1</sub> = *M*<sub>2</sub>. For each *x*, we proceed as follows. If depend<sub>*P*</sub>(*x*) = ⊤, let *M*<sub>0</sub> = *M*<sub>1</sub>; otherwise, let *M*<sub>0</sub> = *M*<sub>1</sub>depend<sub>*P*</sub>(*x*). Let *M*'<sub>0</sub> and *M*'<sub>2</sub> be obtained respectively from *M*<sub>0</sub> and *M*<sub>2</sub> by replacing all array indices that depend on *x* at *P* with fresh replication indices. If *M*'<sub>0</sub> characterizes a part of *x*[*tilde;i*] at *P*, and *M*'<sub>2</sub> does not depend on *x* at *P*, then simplifyTerm(*M*, *P*) = false. Indeed, *M* is equal to false up to negligible probability in this case. We have similar cases swapping *M*<sub>1</sub> and *M*<sub>2</sub> or when *M* is *M*<sub>1</sub> ≠ *M*<sub>2</sub>. (In the latter case, simplifyTerm(*M*, *P*) = true.)

* Case 2: *M* is *M*<sub>1</sub> ∧ *M*<sub>2</sub>. Let *M*'<sub>1</sub> = simplifyTerm(*M*<sub>1</sub>, *P*) and *M*'<sub>2</sub> = simplifyTerm(*M*<sub>2</sub>, *P*). If *M*'<sub>1</sub> or *M*'<sub>2</sub> are false, we return false. If *M*'<sub>1</sub> is true, we return *M*'<sub>2</sub>. If *M*'<sub>2</sub> is true, we return *M*'<sub>1</sub>. Otherwise, we return *M*'<sub>1</sub> ∧ *M*'<sub>2</sub>. We have similar cases when *M* is *M*<sub>1</sub> ∨ *M*<sub>2</sub> or ¬*M*<sub>1</sub>.

* In all other cases, simplifyTerm(*M*, *P*) = *M*.

The local dependency analysis is defined in Figures 20 and 21. The function depAnal is
initially called with depAnal(*Q*<sub>0</sub>, ∅) where ∅ designates the function defined nowhere.
<figure><img src="image_11.png" /><figcaption>Figure 21: Local dependency analysis (2)</figcaption></figure>

Inria
* For oracle definitions, depAnal sets depend<sub>Q</sub>(y) to $\top$, so that depend<sub>Q</sub> gives no information, and propagates indep. Indeed, when $y[\tilde{i}']$ is set in some oracle body $P_0$, the value of $y[\tilde{i}']$ may be passed to another oracle by $P_0$ or read by find in other oracle bodies executed after $P_0$, so as soon as $P_0$ passes control to another oracle by the first return after the definition of y, we lose track of exactly which variables depend on $y[\tilde{i}']$. However, variables already defined before $P_0$ passes control to another oracle and proved to be independent of $y[\tilde{i}']$ remain independent of $y[\tilde{i}']$, so we can propagate indep in all subprocesses of $P_0$.

* In the case of a return, depAnal forgets the information in depend<sub>P</sub> as mentioned above.

* In the case of a random choice $x[\tilde{i}] \stackrel{R}{\leftarrow} T$, if $T$ is a large type, we create the dependency information for the newly defined variable $x$: no variable depends on $x[\tilde{i}]$, and all terms already defined before the random choice are independent of $x[\tilde{i}]$. We also note that $x[\tilde{i}]$ is independent of $y[\tilde{i}']$ for other variables $y$ by adding $x[\tilde{i}]$ to indep(y).

* In the case of an assignment let $x[\tilde{i}] : T = M$, if $M$ depends on $y[\tilde{i}']$ for some variable $y$, then $x[\tilde{i}]$ depends on $y[\tilde{i}']$, so $x$ is added to depend(y) (if it is not $\top$); otherwise, $x[\tilde{i}]$ does not depend on $y[\tilde{i}']$ so it is added to indep(y).

* In the case of a find, we first simplify each condition of the find, remove branches when we can prove that they are taken with negligible probability, and remove the find itself when we know which branch is taken and this branch of the find does not define variables. Furthermore, if some condition of find depends on $y[\tilde{i}]$ for some variable $y$, depend'(y) is set to $\top$: the control flow depends on $y[\tilde{i}]$ so future assignments in fact depend on $y[\tilde{i}]$ even if the assigned expression itself does not, so we can no longer keep track precisely of which variables depend on $y[\tilde{i}]$. Otherwise, we add all terms that are guaranteed to be defined and independent of $y[\tilde{i}]$ to indep(y).

## 3.4 Equational Prover

We use an algorithm inspired by the Knuth-Bendix completion algorithm [51], with differences detailed below.

The prover manipulates pairs $\mathcal{F}, \mathcal{R}$ where $\mathcal{F}$ is a set of facts ($M$ or defined($M$)) and $\mathcal{R}$ is a set of rewrite rules $M_1 \rightarrow M_2$. We say that $M$ reduces into $M'$ by $M_1 \rightarrow M_2$ when $M = C[M_1]$ and $M' = C[M_2]$ for some term context $C$. (That is, all variables in rewrite rules of $\mathcal{R}$ are considered as constants.) The prover starts with a certain set of facts $\mathcal{F}$ and $\mathcal{R} = \emptyset$. Then the prover transforms the pairs $(\mathcal{F}, \mathcal{R})$ by the following rules (the rule $\frac{\mathcal{F}, \mathcal{R}}{\mathcal{F}', \mathcal{R}'}$ means that $\mathcal{F}, \mathcal{R}$ is transformed into $\mathcal{F}', \mathcal{R}')$:

$$ \frac{\mathcal{F} \cup \{F\}, \mathcal{R}}{\mathcal{F} \cup \{F'\}, \mathcal{R}} \quad \begin{array}{l} \text{if } F \text{ reduces into } F' \text{ by a rule of } \mathcal{R} \text{ or} \\ \text{a user-defined rewrite rule knowing } \mathcal{F}, \mathcal{R} \end{array} \qquad (17) $$

$$ \frac{\mathcal{F} \cup \{M_1 \wedge M_2\}, \mathcal{R}}{\mathcal{F} \cup \{M_1, M_2\}, \mathcal{R}} \qquad (18) $$

$$ \frac{\mathcal{F} \cup \{x[M_1, \dots, M_m] = x[M'_1, \dots, M'_m]\}, \mathcal{R}}{\mathcal{F} \cup \{M_1 = M'_1, \dots, M_m = M'_m\}, \mathcal{R}} \quad \begin{array}{l} \text{when } x \text{ is defined only by random choices} \\ x \stackrel{R}{\leftarrow} T \text{ and } T \text{ is a large type} \end{array} \qquad (19) $$
$\mathcal{F} \cup \{M_1 = M_2\}, \mathcal{R}$ when one of the following conditions holds:
$\{\text{false}\}, \mathcal{R}$

* denoting by $M'_1$ the term obtained from $M_1$ by replacing all array indices that are not replication indices with fresh replication indices, we have the following properties: $x$ occurs in $M'_1$, $x$ is defined only by random choices $x \stackrel{R}{\leftarrow} T$, $T$ is a large type, $M'_1$ characterizes a part of $x$, and $M_2$ is obtained by optionally applying function symbols to terms of the form $y[\tilde{M}]$ where $y$ is defined only by random choices and $y \neq x$;

* simplifyTerm($M_1 = M_2, P$) = false, where $P$ is the current program point. (20)

$$ \frac{\mathcal{F} \cup \{M = M'\}, \mathcal{R}}{\mathcal{F}, \mathcal{R} \cup \{M \to M'\}} \text{ if } M > M' \qquad (21) $$

$$ \frac{\mathcal{F}, \mathcal{R} \cup \{M_1 \to M_2\}}{\mathcal{F} \cup \{M_1 = M'_2\}, \mathcal{R}} \text{ if } M_2 \text{ reduces into } M'_2 \text{ by a rule of } \mathcal{R} \qquad (22) $$

$$ \frac{\mathcal{F}, \mathcal{R} \cup \{M_1 \to M_2\}}{\mathcal{F} \cup \{M'_1 = M_2\}, \mathcal{R}} \text{ if } M_1 \text{ reduces into } M'_1 \text{ by a rule of } \mathcal{R} \qquad (23) $$

We also use the symmetries of Rules (20) and (21) obtained by swapping the two sides of the equality.

Rule (17) simplifies facts using rewrite rules. Let us define when $M$ reduces into $M'$ by a user-defined rewrite rule knowing $\mathcal{F}, \mathcal{R}$. For the first kind of rewrite rules of Section 3.1, this is simply when $M$ reduces into $M'$ by the considered rewrite rule. For the second kind of rewrite rules of Section 3.1, consider a rewrite rule $y_1 \stackrel{R}{\leftarrow} T'_1, \dots, y_l \stackrel{R}{\leftarrow} T'_l, \forall x_1 : T_1, \dots, \forall x_m : T_m, M_1 \to M_2$. Suppose that $M = C[\sigma M_1]$, where $C$ is a term context and $\sigma$ is a substitution that maps $x_j$ to any term of type $T_j$ for all $j \le m$ and $y_j$ to terms to the form $z_j[\tilde{M}_j]$ where $z_j$ is defined only by random choices $z_j \stackrel{R}{\leftarrow} T'_j$ for all $j \le l$. Let $\text{Cond} = \{\tilde{M}_j = \tilde{M}_{j'} \mid j \neq j' \wedge z_j = z_{j'}\}$.

* If $\text{Cond} = \emptyset$, the random choices $z_j[\tilde{M}_j]$ are independent, so $M = C[\sigma M_1]$ reduces into $M' = C[\sigma M_2]$.

* If $\text{Cond} \neq \emptyset$, let $\text{Cond} = \{\text{cond}_1, \dots, \text{cond}_k\}$. When $\text{cond}_1 \lor \dots \lor \text{cond}_k$ is true, the random choices $z_j[\tilde{M}_j]$ are not independent, so we must leave $M$ as it is. When $\text{cond}_1 \lor \dots \lor \text{cond}_k$ is false, $M$ reduces into $M' = C[\sigma M_2]$. Suppose that $M' = \text{false}$. Hence, we could rewrite $M$ into if $\text{cond}_1 \lor \dots \lor \text{cond}_k$ then $M$ else false, that is, $(\text{cond}_1 \lor \dots \lor \text{cond}_k) \land M$, that is, $(\text{cond}_1 \land M) \lor \dots \lor (\text{cond}_k \land M)$. However, since this term itself contains $M$, this transformation could lead to a loop. We avoid it as follows. If for all $k' = 1, \dots, k$, $M$ is transformed into $M'_{k'}$ by rewrite rules generated by our equational prover from $\mathcal{F} \cup \{\text{cond}_{k'}\}, \mathcal{R}$ and user-defined rewrite rules, using only the first kind of user-defined rewrite rules of Section 3.1, and $M'_{k'} \neq M_k$, then we rewrite $M$ into $(\text{cond}_1 \land M'_1) \lor \dots \lor (\text{cond}_k \land M'_k)$. Otherwise, $M$ does not rewrite by the considered user-defined rewrite rule knowing $\mathcal{F}, \mathcal{R}$.

Rule (18) decomposes conjunctions of facts. Rules (19) and (20) exploit the elimination of collisions between random values. Rule (19) takes into account that, when $x$ is defined by a random choice of a large type, two different cells of $x$ have a negligible probability of containing the same value. So when two cells of $x$ contain the same value, we can conclude up to negligible probability that they are the same cell. Rule (20) expresses that $M_1$ and $M_2$ have a negligible probability of being equal when $x$ is defined by a random choice of a large type, $M_1$ characterizes a part of $x$, and $M_2$ does not depend of $x$. The first item of (20) establishes these properties without further dependency analysis and the second item exploits the local dependency analysis.