event is not used in the proof of $\phi$, we have

$$ \mu\mathcal{E}v \vdash \exists f_1, \dots, f_k \in \mathbb{N}^m \times \prod \tilde{T} \to \mathbb{N} \cup \{\perp\}, \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) \quad (32) $$

It remains to show $\text{Inj}(I, f)$ for all $f \in \{f_1, \dots, f_k\}$.

Let $f \in \{f_1, \dots, f_k\}$ and $\text{event}(e(\tilde{M}))@f(\tau_1, \dots, \tau_m, \tilde{x})$ be the event labeled with $f$ in $\phi^\tau$. Suppose that $f(\tau'_1, \dots, \tau'_m, \tilde{a}') = f(\tau''_1, \dots, \tau''_m, \tilde{a}'') \neq \perp$ and there exists $j \in I$ such that $\tau'_j \neq \tau''_j$, and let us prove a contradiction.

Since $f(\tau'_1, \dots, \tau'_m, \tilde{a}') \neq \perp$, $\text{event}(e(\tilde{M}))@f(\tau'_1, \dots, \tau'_m, \tilde{a}')$ is used in the proof of (32), so letting $\rho_1 = \{\tau_1 \mapsto \tau'_1, \dots, \tau_m \mapsto \tau'_m, \tilde{x} \mapsto \tilde{a}'\}$, $\rho_1, \mu\mathcal{E}v \vdash \psi^\tau$ and there exists an extension $\rho'_1$ of $\rho_1$ to $\tilde{y}$ such that $\rho'_1, \mu\mathcal{E}v \vdash \phi^\tau$ and $\rho'_1, \mu\mathcal{E}v \vdash \text{event}(e(\tilde{M}))@f(\tau_1, \dots, \tau_m, \tilde{x})$.

Since $\rho_1, \mu\mathcal{E}v \vdash \psi^\tau$, for all events $F_\ell = \text{event}(e_\ell(\tilde{M}_\ell))@\tau_\ell$ in $\psi^\tau$, $\text{Tr}, \rho_1 \vdash F_\ell$ and $\mu\mathcal{E}v(\tau'_\ell) = (\dots) : e_\ell(\tilde{a}_{\ell,1})$ for $\tilde{a}_{\ell,1}$ such that $\rho_1, \tilde{M}_\ell \Downarrow \tilde{a}_{\ell,1}$. By Lemma 38, there exists a program point $\mu_{\ell,1}$ that executes $F_\ell$ (in $Q_0$) and a case $c_{\ell,1}$ such that, for any $\theta_{\ell,1}$ renaming of $I_{\mu_{\ell,1}}$ to fresh replication indices, there exists a mapping $\sigma_{\ell,1}$ with domain $\theta_{\ell,1}I_{\mu_{\ell,1}}$ such that $\mu\mathcal{E}v(\rho_1(\tau_\ell)) = (\mu_{\ell,1}, \sigma_{\ell,1}(\theta_{\ell,1}I_{\mu_{\ell,1}})) : \dots$ and $\text{Tr}, \sigma_{\ell,1} \cup \rho_1 \vdash \theta_{\ell,1}F_{\ell,\mu_{\ell,1},c_{\ell,1}}$. So $\mu\mathcal{E}v(\tau'_\ell) = (\mu_{\ell,1}, \sigma_{\ell,1}(\theta_{\ell,1}I_{\mu_{\ell,1}})) : e_\ell(\tilde{a}_{\ell,1})$.

Let $S$ be the label of $C$ at the occurrence corresponding to $f$, and $\text{inj-event}(e(\tilde{M}))$ be the injective event at that occurrence in $\phi$. Let $\mathcal{F}_1 = \bigcup_\ell \theta_{\ell,1}\mathcal{F}_{F_\ell,\mu_{\ell,1},c_{\ell,1}}$, $\mathcal{I}_1 = \{\ell \to (\mu_{\ell,1}, \theta_{\ell,1}I_{\mu_{\ell,1}}) | F_\ell$ is an injective event$\}$, and $\mathcal{V}_1 = \text{var}(\theta_{1,1}I_{\mu_{1,1}}) \cup \dots \cup \text{var}(\theta_{m,1}I_{\mu_{m,1}}) \cup \{\tilde{x}, \tilde{y}\}$. By construction of $C$, we have $(\mathcal{F}_1, (\tilde{M}), \mathcal{I}_1, \mathcal{V}_1) \in S$.

So we have $\text{Tr}, \bigcup_\ell \sigma_{\ell,1} \cup \rho_1 \vdash \bigcup_\ell \theta_{\ell,1}\mathcal{F}_{F_\ell,\mu_{\ell,1},c_{\ell,1}}$. Letting $\sigma_1 = \bigcup_\ell \sigma_{\ell,1}$, we have $\text{Tr}, \sigma_1 \cup \rho'_1 \vdash \mathcal{F}_1$; for $\ell$ such that $F_\ell$ is an injective event, $\mu\mathcal{E}v(\tau'_\ell) = \sigma_1\mathcal{I}_1(\ell) : e_\ell(\dots)$; $\mathcal{V}_1 = \text{Dom}(\sigma_1) \cup \{\tilde{x}, \tilde{y}\}$. Since $\rho'_1, \mu\mathcal{E}v \vdash \text{event}(e(\tilde{M}))@f(\tau_1, \dots, \tau_m, \tilde{x})$, we have $\rho'_1, \tilde{M} \Downarrow \tilde{a}_1$ and $\mu\mathcal{E}v(f(\tau'_1, \dots, \tau'_m, \tilde{a}')) = (\dots) : e(\tilde{a}_1)$ for some $\tilde{a}_1$.

Since $f(\tau''_1, \dots, \tau''_m, \tilde{a}'') \neq \perp$, we have similarly $(\mathcal{F}_2, (\tilde{M}), \mathcal{I}_2, \mathcal{V}_2) \in S$, $\rho'_2$, and $\sigma_2$ such that $\text{Tr}, \sigma_2 \cup \rho'_2 \vdash \mathcal{F}_2$; for $\ell$ such that $F_\ell$ is an injective event, $\mu\mathcal{E}v(\tau''_\ell) = \sigma_2\mathcal{I}_2(\ell) : e_\ell(\dots)$; $\mathcal{V}_2 = \text{Dom}(\sigma_2) \cup \{\tilde{x}, \tilde{y}\}$; $\rho'_2, \tilde{M} \Downarrow \tilde{a}_2$ and $\mu\mathcal{E}v(f(\tau''_1, \dots, \tau''_m, \tilde{a}'')) = (\dots) : e(\tilde{a}_1)$ for some $\tilde{a}_2$.

Let $\theta''$ be a renaming of variables in $\mathcal{V}_2$. Then $\text{Tr}, \sigma_2\theta''^{-1} \cup \rho'_2\theta''^{-1} \vdash \theta''\mathcal{F}_2$; for $\ell$ such that $F_\ell$ is an injective event, $\mu\mathcal{E}v(\tau''_\ell) = \sigma_2\theta''^{-1}\theta''\mathcal{I}_2(\ell) : e_\ell(\dots)$; $\rho'_2\theta''^{-1}, \theta''\tilde{M} \Downarrow \tilde{a}_2$ and $\mu\mathcal{E}v(f(\tau''_1, \dots, \tau''_m, \tilde{a}'')) = (\dots) : e(\tilde{a}_2)$ for some $\tilde{a}_2$.

Then $\text{Tr}, \sigma_1 \cup \sigma_2\theta''^{-1} \cup \rho'_1 \cup \rho'_2\theta''^{-1} \vdash \mathcal{F}_1 \cup \theta''\mathcal{F}_2$.

There exists $j \in I$ such that $\tau'_j \neq \tau''_j$, so $\sigma_1\mathcal{I}_1(j) \neq \sigma_2\theta''^{-1}\theta''\mathcal{I}_2(j)$ (distinct events have distinct pairs (program point, replication indices) by Lemma 41), so there exists $j \in \text{Dom}(\mathcal{I}_1) = I$ such that $\text{Tr}, \sigma_1 \cup \sigma_2\theta''^{-1} \cup \rho'_1 \cup \rho'_2\theta''^{-1} \vdash \mathcal{I}_1(j) \neq \theta''\mathcal{I}_2(j)$.

Since $f(\tau'_1, \dots, \tau'_m, \tilde{a}') = f(\tau''_1, \dots, \tau''_m, \tilde{a}'')$, $\mu\mathcal{E}v(f(\tau'_1, \dots, \tau'_m, \tilde{a}')) = \mu\mathcal{E}v(f(\tau''_1, \dots, \tau''_m, \tilde{a}'))$, so $\tilde{a}_1 = \tilde{a}_2$, so $\text{Tr}, \sigma_1 \cup \sigma_2\theta''^{-1} \cup \rho'_1 \cup \rho'_2\theta''^{-1} \vdash \tilde{M} = \theta''\tilde{M}$.

So $\text{Tr}, \sigma_1 \cup \sigma_2\theta''^{-1} \cup \rho'_1 \cup \rho'_2\theta''^{-1} \vdash \mathcal{F}_1 \cup \theta''\mathcal{F}_2 \cup \{\bigvee_{j \in \text{Dom}(\mathcal{I}_1)} \mathcal{I}_1(j) \neq \theta''\mathcal{I}_2(j), \tilde{M} = \theta''\tilde{M}\}$.

Since the trace satisfies $\{\vdash C\}$, this is a contradiction. Therefore, we conclude that the considered trace satisfies $\varphi$. Hence, every full trace of $C[Q_0]$ that satisfies $\varphi_{\text{ni}}$, $\{\vdash C\}$, and does not execute a non-unique event of $Q_0$ also satisfies $\varphi$. Therefore, every full trace of $C[Q_0]$ that satisfies $\neg\varphi$ satisfies $\neg(\varphi_{\text{ni}} \wedge \{\vdash C\} \wedge \neg\text{NonUnique}_{Q_0})$, so every full trace of $C[Q_0]$ that satisfies $\neg\varphi \wedge \neg\text{NonUnique}_{Q_0}$ satisfies $\neg(\varphi_{\text{ni}} \wedge \{\vdash C\} \wedge \neg\text{NonUnique}_{Q_0}) \wedge \neg\text{NonUnique}_{Q_0} = (\neg\varphi_{\text{ni}} \vee \neg\{\vdash C\}) \wedge \neg\text{NonUnique}_{Q_0, D_{\text{false}}}$, so it satisfies
($\neg \varphi_{\text{ni}} \wedge \neg \text{NonUnique}_{Q_0}$) $\lor$ $\neg \{[\vdash C]\}$. So

$$
\begin{align*}
\mathrm{Adv}_{Q_0}(\mathcal{A}, C, \varphi, D_{\mathrm{false}}) &= \mathrm{Pr}^A[C_{Q_0} : \neg\varphi \wedge \neg\mathrm{NonUnique}_{Q_0}] \\
&\leq \mathrm{Pr}^A[C_{Q_0} : (\neg\varphi_{\mathrm{ni}} \wedge \neg\mathrm{NonUnique}_{Q_0}) \lor \neg\{[\vdash C]\}] \\
&\leq \mathrm{Pr}^A[C_{Q_0} : \neg\{[\vdash C]\}] + \mathrm{Pr}^A[C_{Q_0} : \neg\varphi_{\mathrm{ni}} \wedge \neg\mathrm{NonUnique}_{Q_0}] \\
&\leq \mathrm{Pr}^A[C_{Q_0} : \neg\{[\vdash C]\}] + \mathrm{Adv}_{Q_0}(\mathcal{A}, C, \varphi_{\mathrm{ni}}, D_{\mathrm{false}}) \\
&\leq \mathrm{Pr}^A[C_{Q_0} : \neg\{[\vdash C]\}] + p(\mathcal{A}, C) \quad \text{since } \mathrm{Bound}_{Q_0}(V, \varphi_{\mathrm{ni}}, D_{\mathrm{false}}, p) \\
&\leq p'(\mathcal{A}, C).
\end{align*}
$$

Therefore $\mathrm{Bound}_{Q_0}(V, \varphi, D_{\mathrm{false}}, p')$. $\square$

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

If the proof that noninj($\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$) implies $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ works, we just have to prove noninj($\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$) and we can apply the **guess** transformation for non-injective correspondences. Otherwise, we simply leave the query $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ unchanged.

A transformation **guess** *i* &**&** above, similar to **guess** *i*, can be used to guess the whole sequence $\tilde{i}$ of replication indices above and including the modified replication, by testing the equality $\tilde{i} = \tilde{i}_{\text{tested}}$ instead of $i = i_{\text{tested}}$.

### 5.1.18 guess $x[c_1, \dots, c_m]$

Like the transformation **guess** *i*, when **guess**$\mathbf{RemoveUnique} = \mathbf{true}$ and some (one-session or bit) secrecy queries are present, the transformation **guess** $x[c_1, \dots, c_m]$ first transforms the game *G* into $G_{\text{RU}}$, by replacing all proved find[unique] with find. Lemma 58 shows the soundness of this preliminary transformation.

Next, the transformation **guess** $x[c_1, \dots, c_m]$ transforms a game *G* into a game *G'* by guessing the value of a variable $x[c_1, \dots, c_m]$: it replaces the processes *P* under the definition of $x[c_1, \dots, c_m]$ with

if $x[c_1, \dots, c_m] = v_{\text{tested}}$ then $P$ else event_abort bad.guess

and $v_{\text{tested}}$ is a constant, which is the guessed value of $x[c_1, \dots, c_m]$. (At each definition of *x*, CryptoVerif must be able to determine whether it is a definition of $x[c_1, \dots, c_m]$ or not. The variable *x* must not be defined inside a term. In case **diff\_constants** = **true**, the constant $v_{\text{tested}}$ must not be considered different from other constants of the same type.)

In case there is a (one-session or bit) secrecy query, it uses instead

let guess\_x\_defined = true in if $x[c_1, \dots, c_m] = v_{\text{tested}}$ then $P$ else event_abort bad.guess

where **guess**\_x\_defined is a fresh variable, and we add **guess**\_x\_defined to the public variables of (one-session or bit) secrecy queries. That gives the adversary knowledge of whether the guessed variable is defined or not. This is useful because the adversary may need to swap its answer differently depending on whether the guessed variable is defined or not, so that the cases in which this variable is not defined always increase the probability of breaking (one-session or bit) secrecy.

When there are only correspondence queries, we can actually execute any code when $x[c_1, \dots, c_m]$ is different from the guessed value $v_{\text{tested}}$. In particular, we can execute *P* with $x[c_1, \dots, c_m]$ set to $v_{\text{tested}}$, which has the effect of replacing the definition of $x[c_1, \dots, c_m]$ with let $x = v_{\text{tested}}$ and removing the test $x[c_1, \dots, c_m] = v_{\text{tested}}$.
To sum up, we also define a transformation **guess** $x[c_1, ..., c_m]$ **no_test** that can be applied when there are only correspondence queries and when $x[c_1, ..., c_m]$ is defined only by definitions of the form let $x = M$. (This is the most useful case, since the definition of $x$ can then be simplified.) This transformation replaces these definitions let $x = M$ with let $x = v_{tested}$ when $M$ is a simple term and with let ignore = $M$ in let $x = v_{tested}$ otherwise, where ignore is a fresh variable whose value is not used.

The transformation **guess** $x[c_1, ..., c_m]$ **no_test** would not be valid in the presence of secrecy queries (at least not with the same probability), because before transformation the value of $x[c_1, ..., c_m]$ may contain part of the secret variable and this value may leak, while after transformation, that leaks disappears and the variable may be perfectly secret for all values $x[c_1, ..., c_m] = v_{tested}$.

**Lemma 60** The transformations **guess** $x[c_1, ..., c_m]$ and **guess** $x[c_1, ..., c_m]$ **no_test** require and preserve Properties 1, 2, 3, and 4. They preserve Property 5.

Suppose the game $G$ is transformed into $G'$ by the transformation **guess** $x[c_1, ..., c_m]$ or **guess** $x[c_1, ..., c_m]$ **no_test**, where $x$ is of type $T$ and $T \neq \emptyset$.

Let $\varphi$ be the semantics of a correspondence. Let $D$ be a disjunction of Shoup and non-unique events that does not contain $S$ nor $\bar{S}$. If $\text{Bound}_{G'}(V, \varphi, D, p)$ and $p$ is independent of the value of $v_{tested}$, then $\text{Bound}_G(V, \varphi, D, |T|p)$.

Let sp be 1-ses.secr.(y), Secrecy(y), or bit secr.(x). Then $G$ is transformed into $G'$ by the transformation **guess** $x[c_1, ..., c_m]$. If $G'$ satisfies sp with public variables $V \cup \{\text{guess } x\text{-defined}\}$ ($y \notin V$) up to probability $p$ and $p$ satisfies Property 6, then $G$ satisfies sp with public variables $V$ up to probability $|T| \times p$ (neglecting a small additional runtime of the context). If $\text{Bound}_{G'}(V' \cup \{\text{guess } x\text{-defined}\}, sp, \text{NonUnique}_{G'}, p)$ and $p$ satisfies Property 6, then $\text{Bound}_G(V', sp, D_{false}, |T|p)$ (neglecting a small additional runtime of the context).

## Proof

**Correspondences** Let $C$ be an evaluation context acceptable for $G$ with any public variables that does not contain events used by $\varphi$ or $D$ and $A$ be an attacker in $\mathcal{B}\mathcal{B}$.

$$
\begin{align*}
\text{Adv}_G(\mathcal{A}, C, \varphi, D) \\
&= \text{Pr}^A[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D}] \\
&= \text{Pr}^A[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D} \land x[c_1, \dots, c_m] \text{ not defined}] + \\
&\qquad \sum_{v \in T} \text{Pr}^A[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D} \land x[c_1, \dots, c_m] = v] \\
&\le \sum_{v \in T} \text{Pr}^A[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D} \land (x[c_1, \dots, c_m] = v \lor x[c_1, \dots, c_m] \text{ not defined})]
\end{align*}
$$

Moreover,

$$
\begin{align*}
\text{Pr}^A[C[G'] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G',D}] &\ge \\
\text{Pr}^A[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D} \land (x[c_1, \dots, c_m] = v_{tested} \lor x[c_1, \dots, c_m] \text{ not defined})]
\end{align*}
$$
This property holds because $G'$ behaves like $G$ when $x[c_1, \dots, c_m]$ is not defined or $x[c_1, \dots, c_m] = v_{\text{tested}}$, in both transformations **guess** $x[c_1, \dots, c_m]$ and **guess** $x[c_1, \dots, c_m]$ **no_test**. So

$$ \begin{aligned} \mathrm{Adv}_G(\mathcal{A}, C, \varphi, D) &\le \sum_{v \in T} \mathrm{Pr}^A[C[G'] : (\neg \varphi \lor D) \land \neg \mathrm{NonUnique}_{G', D}] \text{ for } v_{\text{tested}} = v \\ &\le \sum_{v \in T} \mathrm{Adv}_{G'}(\mathcal{A}, C, \varphi, D) \text{ for } v_{\text{tested}} = v \end{aligned} $$

Since $\mathrm{Bound}_{G'}(V, \varphi, D, p)$, we have $\mathrm{Adv}_{G'}(\mathcal{A}, C, \varphi, D) \le p(\mathcal{A}, C)$ and $p$ is independent of the value of $v_{\text{tested}}$, so we obtain $\mathrm{Adv}_G(\mathcal{A}, C, \varphi, D) \le |T| \times p(\mathcal{A}, C)$. Therefore $\mathrm{Bound}_G(V, \varphi, D, |T|p)$.

(One-session or bit) secrecy Let $C$ be an evaluation context acceptable for $C_{sp}[G]$ with public variables $V$ that does not contain $S$ nor $\bar{S}$ and $\mathcal{A}$ be an attacker in $\mathcal{BB}$. We have

$$ \begin{aligned} \mathrm{Adv}_G^{sp}(\mathcal{A}, C) &= \mathrm{Pr}^A[C[C_{sp}[G]] : S] - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S}] \\ &= \mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] \text{ not defined}] - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] \text{ not defined}] \\ &\quad + \sum_{v=1}^{|T|} \mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] = v] - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] = v] \end{aligned} $$

From the adversary $C$, we define four adversaries $C'$ that call oracle $O'_s$ ($O''_s$ for bit secrecy) with $b''$ instead of $b'$, where $b'' = \text{if defined}(\text{guess } x\text{-defined})$ then $f_1(b')$ else $f_2(b')$ where $f_1(b')$ is either $b'$ or $\neg b'$, and similarly for $f_2$, and consider the adversary $C'_{\max,v_{\text{tested}}}$ among those four that yields the maximum $\mathrm{Adv}_{G'}^{sp}(\mathcal{A}, C')$. Changing $b'$ into $\neg b'$ swaps the events $S$ and $\bar{S}$, and therefore swaps their probabilities. Hence, for this adversary $C'_{\max,v_{\text{tested}}}$,

$$ \mathrm{Adv}_{G'}^{sp}(\mathcal{A}, C'_{\max, v_{\text{tested}}}) = |\mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] = v_{\text{tested}}] - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] = v_{\text{tested}}]| + |\mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] \text{ not defined}] - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] \text{ not defined}]| $$

Since $G'$ satisfies sp with public variables $V \cup \{\text{guess } x\text{-defined}\}$ ($y \notin V$) up to probability $p$ and $C'_{\max,v_{\text{tested}}}$ is an evaluation context acceptable for $C_{sp}[G']$ with public variables $V \cup \{\text{guess } x\text{-defined}\}$ that does not contain $S$ nor $\bar{S}$, we have $\mathrm{Adv}_{G'}^{sp}(\mathcal{A}, C'_{\max,v_{\text{tested}}}) \le p(\mathcal{A}, C'_{\max,v_{\text{tested}}})$. So we have

$$ \begin{aligned} \sum_{v_{\text{tested}}=1}^{|T|} p(\mathcal{A}, C'_{\max, v_{\text{tested}}}) &\ge \sum_{v_{\text{tested}}=1}^{|T|} \mathrm{Adv}_{G'}^{sp}(\mathcal{A}, C'_{\max, v_{\text{tested}}}) \\ &\ge \sum_{v_{\text{tested}}=1}^{|T|} \left| \begin{array}{l} \mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] = v_{\text{tested}}] \\ - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] = v_{\text{tested}}] \end{array} \right| \\ &\quad + |T| \times \left| \begin{array}{l} \mathrm{Pr}^A[C[C_{sp}[G]] : S \land x[c_1, \dots, c_m] \text{ not defined}] \\ - \mathrm{Pr}^A[C[C_{sp}[G]] : \bar{S} \land x[c_1, \dots, c_m] \text{ not defined}] \end{array} \right| \\ &\ge \mathrm{Adv}_G^{sp}(\mathcal{A}, C) \end{aligned} $$

Moreover, by Property 6, $p$ is independent of the value of $v_{\text{tested}}$ (since the type $T$ is bounded) and $p(\mathcal{A}, C)$ depends only on the runtime of $C$, the number of calls $C$ makes to the various oracles
From the adversary C, we define four adversaries C' that call oracle $O'_s$ ($O''_s$ for bit secrecy) with $b''$ instead of $b'$, where $b'' = \text{if defined}(\text{guess\_br\_defined})$ then $f_1(b')$ else $f_2(b')$ where $f_1(b')$ is either $b'$ or $\neg b'$, and similarly for $f_2$, and consider the adversary $C'_{\max,j}$ among those four that yields the maximum $\text{Adv}^{sp}_{G'_j}(\mathcal{A}, \mathcal{C}')$. Changing $b'$ into $\neg b'$ swaps the events $S$ and $\bar{S}$, and therefore swaps their probabilities. Hence, for this adversary $C'_{\max,j}$,

$$ \text{Adv}^{sp}_{G'_j}(\mathcal{A}, C'_{\max,j}) = |\text{Pr}^A[C[C_{sp}[G]] : S \land \text{branch } j \text{ is taken at } \mu] - \text{Pr}^A[C[C_{sp}[G]] : \bar{S} \land \text{branch } j \text{ is taken at } \mu]| \\ + |\text{Pr}^A[C[C_{sp}[G]] : S \land \mu \text{ not executed}] - \text{Pr}^A[C[C_{sp}[G]] : \bar{S} \land \mu \text{ not executed}]| $$

So

$$ \sum_{j=0}^{k-1} \text{Adv}^{sp}_{G'_j}(\mathcal{A}, C'_{\max,j}) \\ \geq \sum_{j=0}^{k-1} \left| \begin{array}{l} \text{Pr}^A[C[C_{sp}[G]] : S \land \text{branch } j \text{ is taken at } \mu] \\ - \text{Pr}^A[C[C_{sp}[G]] : \bar{S} \land \text{branch } j \text{ is taken at } \mu] \end{array} \right| \\ + \sum_{j=0}^{k-1} |\text{Pr}^A[C[C_{sp}[G]] : S \land \mu \text{ not executed}] - \text{Pr}^A[C[C_{sp}[G]] : \bar{S} \land \mu \text{ not executed}]| \\ \geq \text{Adv}^{sp}_{\bar{G}}(\mathcal{A}, \mathcal{C}) $$

Since $G'_j$ satisfies sp with public variables $V \cup \{\text{guess\_br\_defined}\}$ up to probability $p_j$ and $C'_{\max,j}$ is an evaluation context acceptable for $C_{sp}[G'_j]$ with public variables $V \cup \{\text{guess\_br\_defined}\}$ that does not contain $S$ nor $\bar{S}$, we have $\text{Adv}^{sp}_{G'_j}(\mathcal{A}, C'_{\max,j}) \leq p_j(\mathcal{A}, C'_{\max,j})$. Moreover, by Property 6, $p_j(\mathcal{C})$ depends only on the runtime of $\mathcal{C}$, the number of calls $\mathcal{C}$ makes to the various oracles (which determine replication bounds), and the length of bitstrings, so we have $p_j(C'_{\max,j}) = p_j(\mathcal{C})$. (The additional runtime of the context can be neglected.) So $\text{Adv}^{sp}_{\bar{G}}(\mathcal{A}, \mathcal{C}) \leq \sum_{j=0}^{k-1} p_j(\mathcal{C})$. Therefore, $\mathcal{G}$ satisfies sp with public variables $V$ up to probability $\sum_{j=0}^{k-1} p_j$. The proof of the second property for (one-session or bit) secrecy proceeds as for **guess** i in Lemma 59. $\square$

### 5.1.20 global\_dep\_anal [26]

**Extension:** A few minor extensions have been implemented with respect to the following description.

The global dependency analysis **global\_dep\_anal** $x$ tries to find a set of variables $S$ such that only variables in $S$ depend on $x$. In particular, when the global dependency analysis succeeds, the control flow and the view of the adversary do not depend on $x$, except in cases of negligible probability.

Let $x$ be a variable defined only by random choices $x \stackrel{R}{\leftarrow} T$ where $T$ is a large type. Let $S_{\text{def}}$ be a set of variables defined only by assignments. Let $S_{\text{dep}}$ be a set of variables containing $x$. (Intuitively, $S_{\text{dep}}$ will be a superset of variables that depend on $x$.)

We say that a function $f: T \to T'$ is uniform when each element of $T'$ has at most $|T'|/|T'|$ antecedents by $f$. In particular, this is true in the following two cases:

* $f$ is such that $f(x)$ is uniformly distributed in $T'$ if $x$ is uniformly distributed in $T$.
* $f$ is the restriction to the image of $f'$ of an inverse of $f'$, where $f'$ is a poly-injective function. (We consider that $f(x)$ is undefined when $x$ is not in the image of $f'$. Here, in contrast to the rest of the paper, we allow $f: T \to T'$ to be defined only on a subset of $T$..) Precisely, when $x_k \in S_{\text{def}}$ is defined by a pattern-matching let $f'(x_1, \dots, x_n) = M$ in P else $P'$, we have $x_k = f'_k^{-1}(M)$, but furthermore when $x_k$ is defined we know that the value of $M$ is in the image of $f'$, so we have $x_k = f(M)$ where $f = f'_k|_{\text{im } f'}$.

We say that $M$ characterizes a part of $x$ with $S_{\text{def}}, S_{\text{dep}}$ when for all $M_0$ obtained from $M$ by substituting variables of $S_{\text{def}}$ with their definition (when there is a dependency cycle among variables of $S_{\text{def}}$, we do not substitute a variable inside its definition), $\alpha M_0 = M_0$ implies $f_1(...f_k((\alpha x)[\tilde{M}])) = f_1(...f_k(x[\tilde{M}]))$ for some uniform functions $f_1, \dots, f_k$ and for some $\tilde{M}$ and $\tilde{M}'$, where $\alpha$ is a renaming of variables of $S_{\text{dep}}$ to fresh variables, $x[\tilde{M}]$ is a subterm of $M_0$, $(\alpha x)[\tilde{M}']$ is a subterm of $\alpha M_0$, the variables in $S_{\text{dep}}$ do not occur in $\tilde{M}$ or $\tilde{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(...f_k(x[\tilde{M}]))$.

We use a simple rewriting prover to determine that. We consider the set of terms $M_0 = \{\alpha M_0 = M_0\}$, and we rewrite elements of $M_0$ using the first kind of user-defined rewrite rules mentioned in Section 3.1 and the rule $\{M_1 \wedge M_2\} \cup M' \to \{M_1, M_2\} \cup M'$.

When $M_0$ can be rewritten to a set that contains an equality of the form $f_1(...f_k(x[\tilde{M}])) = f_1(...f_k((\alpha x)[\tilde{M}]))$ or $f_1(...f_k((\alpha x)[\tilde{M}])) = f_1(...f_k(x[\tilde{M}]))$ for some $\tilde{M}$ and $\tilde{M}'$ such that the variables in $S_{\text{dep}}$ do not occur in $\tilde{M}$ or $\tilde{M}'$, we have that $M$ characterizes a part of $x$ with $S_{\text{def}}, S_{\text{dep}}$.

We say that $M$ characterizes a part of $x$ when $M$ characterizes a part of $x$ with $\emptyset, S'$ where $S'$ is $\{x\}$ union the set of all variables except those defined by random choices. (We know that variables different from $x$ and defined by random choices do not depend on $x$, so in the absence of more precise information, we can set $S_{\text{dep}} = S'$.)

We say that only\_dep($\mathcal{A}, x$) = $S$ when intuitively, only variables in $S$ depend on $x$, and the adversary cannot see the value of $x$. Formally, only\_dep($\mathcal{A}, x$) = $S$ when

* $S \cap V = \emptyset$.

* Variables of $S$ do not occur in a term $N$ of a return value return ($N$).

* Variables of $S$ except $x$ are defined only by assignments.

* If a variable $y \in S$ occurs in $M$ in let $z: T = M$ in $P$, then $z \in S$.

* Variables in $S$ may occur in defined conditions of find but only at the root of them.

* All terms $M_j$ in processes find ($\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] \le \tilde{n}_j$ such that defined($M_{j1}, \dots, M_{jl_j}$) $\wedge$ $M_j$ then $P_j$) else $P'$ are combinations by $\wedge, \vee$, or $\neg$ of terms that either do not contain variables in $S$ or are of the form $M_1 = M_2$ or $M_1 \neq M_2$ where $M_1$ characterizes a part of $x$ with $S \setminus \{x\}, S$ and no variable of $S$ occurs in $M_2$, or $M_2$ characterizes a part of $x$ with $S \setminus \{x\}, S$ and no variable of $S$ occurs in $M_1$.

The last item implies that the result of tests does not depend on the values of variables in $S$, except in cases of negligible probability. Indeed, the tests $M_1 = M_2$ with $M_1$ characterizes a part of $x$ with $S \setminus \{x\}, S$ and $M_2$ does not depend on variables in $S$ are false except in cases of negligible probability, since the value of $M_1$ uniquely determines the value of $f_1(...f_k(x[\tilde{M}]))$ and $M_2$ does not depend on $f_1(...f_k(x[\tilde{M}]))$, so the equality $M_1 = M_2$ happens for a single value of $f_1(...f_k(x[\tilde{M}]))$, which yields a negligible probability because $f_1, \dots, f_k$ are uniform, $x$
is chosen with uniform probability, and the type of the result of $f_1$ is large. Similarly, the tests $M_1 \neq M_2$ are true except in cases of negligible probability.

In checking the conditions of only\_dep($\mathcal{A}$, $x$) = $S$, we do not consider the parts of the code that are unreachable due to tests whose result is known by the conditions above.

The set $S$ is computed by a fixpoint iteration, starting from $\{x\}$ and adding variables defined by assignments that depend on variables already in $S$.

If we manage to show that only\_dep($\mathcal{A}$, $x$) = $S$, we transform the game as follows:

* We replace with false terms $M_1 = M_2$ in conditions of find where $M_1$ characterizes a part of $x$ with $S \setminus \{x\}$, $S$ and no variable of $S$ occurs in $M_2$, or symmetrically.

* We replace with true terms $M_1 \neq M_2$ in conditions of find where $M_1$ characterizes a part of $x$ with $S \setminus \{x\}$, $S$ and no variable of $S$ occurs in $M_2$, or symmetrically.

**Lemma 62** *The transformation global\_dep\_anal requires and preserves Properties 1, 2, 3, 4, and 5. If transformation global\_dep\_anal transforms $G$ into $G'$, then $\mathcal{D}, \mathcal{D}_{SNU} : G, D, \text{EvUsed} \xrightarrow{V} p G', D, \text{EvUsed}$, where $p$ is an upper bound on the probability that required equalities do not hold.*

### 5.1.21 simplify [26,27]

*Extension: Some extensions have been implemented with respect to the following description.*

We use the following transformations in order to simplify games. These transformations exploit the information collected as explained in Section 3.

1. Each term $M$ in the game is replaced with a simplified term $M'$ obtained by reducing $M$ by user-defined rewrite rules knowing $\mathcal{F}_{P_M}$ (see Sections 3.1 and 3.4) and the rewrite rules obtained from $\mathcal{F}_{P_M}$ by the above equational prover where $P_M$ is the smallest process containing $M$. The replacement is performed only when at least one user-defined rewrite rule has been used, to avoid complicating the game by substituting all variables with their value.

2. When setting **inferUnique** is true, CryptoVerif tries to prove uniqueness of find[unique<sub>e</sub>], as in transformation **prove_unique** (Section 5.1.4).

3. If $P = \text{find}[\text{unique?}] (\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) \text{ else } P'$, $M_j$ does not contain event\_abort nor unproved find[unique<sub>e</sub>], $u_{jk}[\tilde{i}]$ reduces into $M'$ by user-defined rewrite rules knowing $\mathcal{F}_{P_j}$ (see Sections 3.1 and 3.4) and the rewrite rules obtained from $\mathcal{F}_{P_j}$, and $u_{jk}$ does not occur in $M'$, then $u_{jk}$ is removed from the j-th branch of this find, $i_{jk}$ is replaced with $M'\{i_{j'k'}/u_{j'k'}, j' \le m, k' \le m_j\}$ in $M_{j1}, \dots, M_{jl_j}, M_j$ and $P_j$ is replaced with let $u_{jk}[\tilde{i}] : [1, n_{jk}] = M'$ in $P_j$. (Intuitively, $u_{jk}[\tilde{i}] = M'$, so the value of $u_{jk}[\tilde{i}]$ can be computed by evaluating $M'$ instead of performing an array lookup. We remove $u_{jk}[\tilde{i}]$ from the variables looked up by find and replace $u_{jk}[\tilde{i}]$ with its value $M'$.)

4. Suppose that $P = \text{find}[\text{unique?}] (\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) \text{ else } P'$, there exists a term $M$ such that $\text{defined}(M) \in \mathcal{F}_{P_j}$, $x[N_1, \dots, N_l]$ is a subterm of $M$, $x \neq u_{jk}$ for all $k \le m_j$, and none of the following conditions holds: a) $P$ is under a definition of $x$ in $Q_0$; b) $Q_0$ contains $Q_1 \mid Q_2$ such that a definition of $x$ occurs in $Q_1$ and $P$ is under $Q_2$ or a definition of $x$ occurs in $Q_2$ and $P$ is under $Q_1$; c) $Q_0$ contains $lp + 1$ replications above a process $Q$
that contains a definition of $x$ and $P$, where $lp$ is the length of the longest common prefix between $N_1, \dots, N_l$ and the current replication indices at the definitions of $x$. Then the $j$-th branch of the find is removed. (In this case, $x[N_1, \dots, N_l]$ cannot be defined at $P$, so the $j$-th branch of the find cannot be taken.)

5. Suppose that $P = \text{find}[\text{unique?}] (\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 defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j) \text{ else } P'$, there exist terms $M, M'$ such that $\text{defined}(M) \in \mathcal{F}_{P_j}, x[N_1, \dots, N_l]$ is a subterm of $M$, $\text{defined}(M') \in \mathcal{F}_{P_j}, x'[N'_1, \dots, N'_l]$ is a subterm of $M'$, $N_k = N'_k$ for all $k \le \min(l, l')$, $x \ne x'$, and $x$ and $x'$ are incompatible, then the $j$-th branch of the find is removed. Two variables $x$ and $x'$ are said to be compatible when either there exists $Q_1 | Q_2$ in the game such that $x$ is defined in $Q_1$ and $x'$ is defined in $Q_2$, or there is a definition of $x'$ under a definition of $x$, or symmetrically.

6. If $P = \text{find}[\text{unique?}] (\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j) \text{ else } P'$ and $\mathcal{F}_{P_j}$ yields a contradiction, then the $j$-th branch of the find is removed if $M_j$ does not contain event_abort nor unproved find[unique$_e$], and $P_j$ is replaced with yield if $M_j$ contains event_abort or some unproved find[unique$_e$].

7. If $P = \text{find}[\text{unique?}] \text{ else } P'$, then $P$ is replaced with $P'$.

8. If find[unique?] $(\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j) \text{ else } P'$ and $\mathcal{F}_{P'}$ yields a contradiction, then $P'$ is replaced with yield.

9. If $P = \text{find}[\text{unique?}] \tilde{u}[\tilde{i}] = \tilde{i}' \le \tilde{n} \text{ suchthat defined}(M_1, \dots, M_l) \wedge M \text{ then } P_1 \text{ else } P'$, [unique?] is not [unique$_e$] for some non-unique event $e$ that is not proved yet to have negligible probability, $\mathcal{F}_{P'}$ yields a contradiction, $M$ is simple (so $M$ never aborts), and the variables in $\tilde{u}$ are not used outside $P$ and are not in $V$, then $P$ is replaced with $P_1$. (When the find defines variables $\tilde{u}$ used elsewhere, we cannot remove it.)

10. If $P = \text{find}[\text{unique?}] (\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] \le \tilde{n}_j \text{ suchthat defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then yield}) \text{ else } P'$, [unique?] is not [unique$_e$] for some non-unique event $e$ that is not proved yet to have negligible probability, the terms $M_j$ do not contain event_abort nor unproved find[unique$_e$], and the variables in $\tilde{u}_j$ are not used outside $P$ and are not in $V$, then $P$ is replaced with yield.

11. The defined conditions of find are updated so that Invariant 2 is satisfied. (When such a defined condition guarantees that $M$ is defined, defined($M$) implies defined($M'$), and after simplification $M'$ appears in the scope of this condition, then $M'$ has to be added to this condition if it is not already present.)

12. If $P = x \stackrel{R}{\leftarrow} T; P'$ or let $x : T = M$ in $P'$ and $x$ is not used in the game and is not in $V$, then $P$ is replaced with $P'$.

13. If one of the then branches of a find[unique] always succeeds and the conditions of this find[unique] do not contain event_abort nor unproved find[unique$_e$], then we keep only that branch.

Indeed, the other branches are never taken: the conditions of this find[unique] never abort in traces counted in the probability, and the find itself aborts when there are several successful choices.
14. We reorganize a find[unique] that occurs in a then branch of a find[unique]: we transform

$$ \text{find}[\text{unique}] (\bigoplus_{j=1}^{k} \tilde{u}_j = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } c_j \text{ then } P_j) \text{ else } P $$

$$ \text{where } P_{j_0} = \text{find}[\text{unique}] (\bigoplus_{j'=1}^{k'} FB_{j'}) \text{ else } P_{j_0}^{\prime\prime} \text{ into} $$

$$ \text{find}[\text{unique}] (\bigoplus_{j=1,...,k; j \neq j_0} \tilde{u}_j = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } c_j \text{ then } P_j) $$

$$ \oplus (\bigoplus_{j'=1}^{k'} \bigoplus_{(\tilde{u}'=\tilde{i}' \le \tilde{n}' \text{ suchthat } c' \text{ then } P') \in \mathbf{b}(FB_{j'}, L_{j'})} \tilde{u}_{j_0} = \tilde{i}_{j_0} \le \tilde{n}_{j_0}, \tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c_{j_0} \land c' \text{ then } P') $$

$$ \text{else find}[\text{unique}] \tilde{u}_{j_0} = \tilde{i}_{j_0} \le \tilde{n}_{j_0} \text{ suchthat } c_{j_0} \text{ then } P_{j_0}^{\prime\prime} \text{ else } P $$

where

- either for all $j \le k$, $c_j$ does not contain event_abort nor unproved find[unique_e] or $c_{j_0}$ never aborts (this is true in particular when $c_{j_0}$ does not contain event_abort nor proved or unproved find[unique_e])

- $\tilde{i}$ are the current replication indices at the transformation point

- for all $j'$, $FB_{j'} = (\tilde{u}'_{j'} = \tilde{i}'_{j'} \le \tilde{n}'_{j'} \text{ suchthat } c'_{j'} \text{ then } P'_{j'})$, $c'_{j'} = \text{defined}(\tilde{M}_{j'}) \land \dots, c'_{j'}$ never aborts, and $L_{j'}$ is the list of $x[\tilde{N}]$ subterm of $\tilde{M}_{j'}$ with $x \in \tilde{u}_{j_0}$ and $\tilde{N} \ne \tilde{i}$, ordered by increasing size

- $\text{b}(\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c' \text{ then } P',[]) = \{\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c'\{\tilde{i}_{j_0}/\tilde{u}_{j_0}\} \text{ then } P'\}$

- $\text{b}(FB,x[\tilde{N}] :: L) = \text{b}(FB,L) \cup \{\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c'\{i/x[\tilde{N}]\} \land \tilde{N} = \tilde{i} \text{ then } P' \mid (\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c' \text{ then } P') \in \text{b}(FB,L)\}$ where $i = x\{\tilde{i}_{j_0}/\tilde{u}_{j_0}\}$.

The function b takes into account that, before the transformation, $\tilde{u}_{j_0}[\tilde{i}]$ is defined when we test defined($\tilde{M}_{j'}$) in $FB_{j'}$, while after the transformation, $\tilde{u}_{j_0}[\tilde{i}]$ is not defined yet when we perform this test. Furthermore, the value of $\tilde{u}_{j_0}[\tilde{i}]$ will be $\tilde{i}_{j_0}$. Therefore, 1) when we access $x[\tilde{i}]$ in $c'_{j'} = \text{defined}(\tilde{M}_{j'}) \land \dots$, we replace this access with $i$, where $i = x\{\tilde{i}_{j_0}/\tilde{u}_{j_0}\}$; this is done in $\text{b}(FB,[])$ by the substitution $\{\tilde{i}_{j_0}/\tilde{u}_{j_0}\}$; and 2) when we access $x[\tilde{N}]$ in $c'_{j'} = \text{defined}(\tilde{M}_{j'}) \land \dots$ for $\tilde{N}$ not syntactically equal to $\tilde{i}$, we need to distinguish two cases: either at runtime $\tilde{N} = \tilde{i}$ and we replace this access with $i$ (second part of the union in $\text{b}(FB,x[\tilde{N}] :: L)$), or at runtime $\tilde{N} \ne \tilde{i}$ and we continue using $x[\tilde{N}]$ (first part of the union in $\text{b}(FB,x[\tilde{N}] :: L)$). The array accesses $x[\tilde{N}]$ in $L_{j'}$ are ordered by increasing size because, in case of nested array accesses, we need to handle the bigger array access first (so it must occur last in the list), because after substitution of the smaller one with $i$, we would not recognize the bigger one.

This transformation cannot be performed when the outer find is not unique because it might change the probability of taking each branch. Moreover, we tried performing such a transformation when the inner find is not unique (in this case, after transformation, the outer find is not unique), but it had a negative impact in some examples. Furthermore, in the latter case, the transformation can be performed manually by inserting the desired outer find and simplifying the game: CryptoVerif will remove the useless branches of find.

The conditions $c_{j_0}$ and $c'_{j'}$ are conjunctions of defined conditions and a term. In the current implementation, the transformation is not performed when the term in $c_{j_0}$ is false (the branch of find will be removed by another transformation), and the branches such that the terms in $c'_{j'}$ are false are first removed. Furthermore, the transformation is performed only when one of the following conditions holds: the terms in $c_{j_0}$ and all $c'_{j'}$ are simple, or
the term in $c_{j_0}$ is true and all $c'_{j'}$ never abort, or the terms in $c'_{j'}$ are all true and $c_{j_0}$ never aborts. With the usual simplification of $\wedge$ true, this guarantees that the transformed game satisfies Property 5. Moreover, this implies the abortion conditions ($c_{j_0}$ and all $c'_{j'}$ never abort).

After this transformation, we advise renaming the variables $\tilde{u}_{j_0}$ to distinct names, since they now have multiple definitions.

15. We reorganize a find[unique] that occurs in a condition of a find: we transform

$$ \text{find}[\text{unique?}] (\bigoplus_{j=1}^{k} \tilde{u}_j = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } c_j \text{ then } P_j) \text{ else } P $$

where

$$ c_{j_0} = \text{defined}(\tilde{M}') \wedge \text{find}[\text{unique}](\bigoplus_{j'=1}^{k'} \tilde{u}_{j'} = \tilde{i}_{j'} \le \tilde{n}_{j'} \text{ suchthat } c'_{j'} \text{ then } M'_{j'}) \text{ else false} $$

for all $j' \le k'$, $M'_{j'}$ never aborts and either for all $j \le k$, $c_j$ does not contain event_abort nor unproved find[unique] or for all $j' \le k'$, $c'_{j'}$ never aborts, into

$$ \begin{array}{l} \text{find}[\text{unique?}] (\bigoplus_{j=1,...,k; j \ne j_0} \tilde{u}_j = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } c_j \text{ then } P_j) \\ \oplus (\bigoplus_{j'=1}^{k'} \tilde{u}_{j_0} = \tilde{i}_{j_0} \le \tilde{n}_{j_0}, \tilde{u}'_{j'} = \tilde{i}'_{j'} \le \tilde{n}'_{j'} \text{ suchthat} \\ \quad \text{defined}(\tilde{M}') \wedge c'_{j'} \wedge M'_{j'}\{\tilde{i}'_{j'}/\tilde{u}'_{j'}\} \text{ then } P_{j_0}) \\ \text{else } P \end{array} $$

The indication [unique?] corresponds to either [unique] or empty. The find is marked [unique] after transformation if the outer find was [unique] before transformation.

The variables $\tilde{u}'_{j'}$ are defined inside the condition of a find so by Invariant 3, they have no array accesses. The transformation performed by function b above is therefore not needed here.

The conditions $c'_{j'}$ are conjunctions of defined conditions and a term. The current implementation first removes the branches such that one of the following two conditions holds: the terms in $c'_{j'}$ are false or $M'_{j'}$ is false and $c'_{j'}$ never aborts. Furthermore, the transformation is performed only when for all $j'$, one of the following conditions holds: the term in $c'_{j'}$ and $M'_{j'}$ are simple, or the term in $c'_{j'}$ is true and $M'_{j'}$ never aborts, or $M'_{j'}$ is true or false and the term in $c'_{j'}$ never aborts. With the usual simplification of $\wedge$ true and $\wedge$ false, this guarantees that the transformed game satisfies Property 5. Moreover, this implies the abortion conditions ($c'_{j'}$ and $M'_{j'}$ never abort).

The simplification is iterated at most maxIterSimplif times. The iteration stops earlier in case a fixpoint is reached.

**Lemma 63** The transformation simplify requires and preserves Properties 1, 2, 3, and 4. It preserves 5. If transformation simplify transforms G into G', then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V \to_p} G', D, EvUsed$, where p is an upper bound on the probability that required equalities do not hold.

**Extension:** When the game is not expanded, simplify is actually a weaker simplification transformation. We plan to improve that.
### 5.1.22 all_simplify

all_simplify perform several simplifications on the game, as if

* simplify,

* move all if `autoMove = true`,

* remove_assign useless if `autoRemoveAssignFindCond = false`, remove_assign findcond if `autoRemoveAssignFindCond = true`,

* SArename random if `autoSARename = true`,

* and `merge Fet branches if `autoMergeBranches = true`

had been called.

### 5.1.23 success simplify

The transformation **success simplify** is a combination of **success** (Section 4) and **simplify** (Section 5.1.21), with the following addition. First, in the **success** step, the command **success simplify** collects information that is known to be true when the adversary manages to break at least one of the desired properties. Then, the first iteration of the **simplify** step removes parts of the game that contradict this information and replaces them with **event_abort** adv_loses.

In more detail, **success simplify** collects a set $\mathcal{L}^-$ of $(\mathcal{V}, \mathcal{F})$ and a set of formulas $\mathcal{L}^+$. If the adversary breaks a desired security property, then either there exists a set of facts $\mathcal{F}$ in $\mathcal{L}^-$ that holds or there exists a formula in $\mathcal{L}^+$ that holds. The sets of facts $\mathcal{L}^-$ correspond to cases in which the proof of the security property failed; their probability may be high. The associated variables $\mathcal{V}$ are replication indices and non-process variables that occur in $\mathcal{F}$. The formulas in $\mathcal{L}^+$ correspond to cases in which the security property was proved (up to a certain probability); these formulas are negations of the formulas that prove the security property in the considered case; the probability that they hold is bounded by the equational prover of CryptoVerif. The contents of $\mathcal{L}^+$ does not influence the game obtained after the transformation. It is useful to compute the probability difference coming from the transformation. The sets $\mathcal{L}^-$ and $\mathcal{L}^+$ are computed as follows:

* In case there is an indistinguishability query, or a (one-session or bit) secrecy query on a variable $x$ not defined only by $\stackrel{R}{\leftarrow}$ or by assignments of variables defined by $\stackrel{L}{\leftarrow}$, or a correspondence query $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ with some event $e$ in $\psi$ such that the game contains **event e(M)** and some term in $\tilde{M}$ is not simple, no information is collected at all and **simplify** is not performed.

* For each correspondence query **event(e)** $\Rightarrow$ **false** where e is a non-unique event, for every $\mu$ that executes **event(e)**, for every c, $(\theta' I_\mu, \theta' \mathcal{F}_{\text{event(e),\mu,c}}^0)$ is added to $\mathcal{L}^-$, for some $\theta'$ renaming of $I_\mu$ to fresh replication indices. (Indeed, in order to break **event(e)** $\Rightarrow$ **false**, event e must be executed, so the facts $\mathcal{F}_{\text{event(e),\mu,c}}^0$ at some execution of event e hold.)

* For each other correspondence query $\forall \tilde{x} : \tilde{T}; F_1 \wedge \dots \wedge F_m \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, let $\varphi = [\forall \tilde{x} : \tilde{T}; F_1 \wedge \dots \wedge F_m \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ and $S_0 = \{(\mu_1, c_1, \dots, \mu_m, c_m) \mid \forall j \le m, \mu_j \text{ executes } F_j \text{ and } c_j \text{ is a case for } \mathcal{F}_{\mu_j, c_j}\}$; by trying to prove the correspondence, we build a subset $S_1$ of $S_0$, a family of substitutions $\theta$, and a pseudo-formula $C$ such that $\text{prove}(C, \theta, S_1)$. ($\theta$ and $C$ are computed incrementally on the successful cases in the proof of the correspondence.)
For all $(\mu_1, c_1, \dots, \mu_m, c_m) \in S_0 \setminus S_1$ (success fails to prove the correspondence for those cases):

- If the query is $\forall \tilde{x} : \tilde{T}; \text{event}(e(\tilde{N})) \Rightarrow \text{false}$ and the process or term at $\mu_1$ is event $e(\tilde{M})$; 
  ..., then $(\tilde{x} \cup \theta'I_{\mu_1}, \theta'\mathcal{F}_{\mu_1, c_1} \cup \{\text{lastdefprogrampoint}(\mu_1, \theta'I_{\mu_1}), \tilde{N} = \theta'\tilde{M}\})$ is added to $\mathcal{L}^-$, where $\theta'$ is a renaming of $I_{\mu_1}$ to fresh replication indices. (We can stop the trace just after event $e$ without changing the truth of the query, and that is more precise because we can use the *elsefind* facts at $e$.)

- Otherwise, $(\tilde{x} \cup \bigcup_{j=1}^m \theta_j I_{\mu_j}, \bigcup_{j=1}^m \theta_j \mathcal{F}_{F_j, \mu_j, c_j})$ is added to $\mathcal{L}^-$, where for $j \le m$, $\theta_j$ is a renaming of $I_{\mu_j}$ to fresh replication indices. (Indeed, in order to break the correspondence $\forall \tilde{x} : \tilde{T}; F_1 \wedge \dots \wedge F_m \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, the events $F_1, \dots, F_m$ must be executed, so the facts $\mathcal{F}_{F_j, \mu_j, c_j}$ for $j \le m$ that hold when $F_1, \dots, F_m$ are executed certainly hold when the correspondence is broken. In principle, we could add $\neg \exists \tilde{y} : \tilde{T}'; \phi$ to the facts $\bigcup_{j=1}^m \theta_j \mathcal{F}_{F_j, \mu_j, c_j}$ added to $\mathcal{L}^-$.) However, we have no way to express universal quantification in general in known facts, so when $\tilde{y}$ is not empty, we could not add $\forall \tilde{y} : \tilde{T}'; \neg \phi$ but would end up adding $\neg \phi$ which in fact means $\exists \tilde{y} : \tilde{T}'; \neg \phi$. That would remain sound assuming the types in $\tilde{T}'$ are not empty, but would be weaker. Moreover, in practice, we end up having to distinguish precisely the case in which $\exists \tilde{y} : \tilde{T}'; \phi$ can be proved from the case in which it cannot, which can typically be done by inserting an appropriate *find*. We generally insert a Shoup event $e$ in the *else* branch of that *find*, triggered when the correspondence cannot be proved, a case for which we want to bound the probability. After that, it remains to prove *event(e) ⇒ false*: we apply **success simplify** to that correspondence. Adding $\neg \phi = \text{true}$ would not change anything for that correspondence, and we exploit that the condition of the inserted *find* is false at *event e*, which gives us more precise information than having added $\neg \phi$ for the initial correspondence.)

Moreover, $\neg\{[\text{prove}^\varphi(C, \theta, S_1)]\}$ is added to $\mathcal{L}^+$. (success proves the correspondence for the cases in $S_1$.)

* For each secrecy, one-session secrecy, or bit secrecy query on a variable $x$ defined only by $\leftarrow^R$ or by assignments of variables defined by $\leftarrow^R$, let $S_0 = \{\mu \mid \mu$ follows a definition of $x\}$ and $S_1 = \{\mu \in S_0 \mid \text{prove}^{\text{1-ses.secr.}(x)}(\mu)\}$.

For each $\mu \in S_0 \setminus S_1$ (success fails to prove one-session secrecy for those cases), $(\theta I_\mu, \theta \mathcal{F}_\mu)$ is added to $\mathcal{L}^-$, where $\theta$ is a renaming of $I_\mu$ to fresh replication indices. (Indeed, if secrecy, one-session secrecy, or bit secrecy of $x$ is broken, a definition of $x$ must have been executed, so the facts $\mathcal{F}_\mu$ at that definition hold.)

Moreover, $\neg\{[\text{prove}^{\text{1-ses.secr.}(x)}(S_1)]\}$ is added to $\mathcal{L}^+$. (success proves one-session secrecy for the cases in $S_1$.)

Additionally, if the considered query is a secrecy query, then for each $\mu_1, \mu_2 \in S_0$, let $z_1[\tilde{M}_1] = \text{defRand}_{\mu_1}(x)$ and $z_2[\tilde{M}_2] = \text{defRand}_{\mu_2}(x)$. If $z_1 \ne z_2$, then the definitions at $\mu_1$ and $\mu_2$ are proved to be independent, and nothing is added to $\mathcal{L}^-$ nor $\mathcal{L}^+$. If $z_1 = z_2$, let $\tilde{i}$ be the current replication indices at the definition of $x$, let $\theta_1$ and $\theta_2$ be two distinct renamings of $\tilde{i}$ to fresh replication indices, let $\tilde{i}_1 = \theta_1\tilde{i}$ and $\tilde{i}_2 = \theta_2\tilde{i}$, let $\mathcal{F} = \theta_1\mathcal{F}_{\mu_1} \cup \theta_2\mathcal{F}_{\mu_2} \cup \{\theta_1\tilde{M}_1 = \theta_2\tilde{M}_2, \tilde{i}_1 \ne \tilde{i}_2\}$. If $\mathcal{F}$ yields a contradiction, then the definitions at $\mu_1$ and $\mu_2$ are proved to be independent up to a small probability, $\exists \tilde{i}_1, \exists \tilde{i}_2, \wedge \mathcal{F}$ is added to $\mathcal{L}^+$. Otherwise, $(\tilde{i}_1 \cup \tilde{i}_2, \mathcal{F})$ is added to $\mathcal{L}^-$.
In the **simplify** step, the set $\mathcal{L}^-$ is used as follows: for each program point $\mu$ not in a condition of find, if for all $(\mathcal{V}, \mathcal{F}) \in \mathcal{L}^-$, $\mathcal{F}_\mu \cup \mathcal{F}$ yields a contradiction, then the code at $\mu$ is replaced with **event_abort** adv_loses. (The reason why $\mathcal{V}$ is needed in the implementation is for the optimization of probabilities of collisions: we determine using which indices in $\mathcal{V}$ we get the smaller bound for the number of collisions.)

The probability that a security property is broken before the transformation and not after is then bounded by the probability that a modified program point $\mu$ is reached and the adversary breaks the property. If that breach corresponds to a case in $\mathcal{L}^+$, the probability of the breach itself is bounded by construction of $\mathcal{L}^+$. If that breach corresponds to a case in $\mathcal{L}^-$, the probability of the breach and reaching $\mu$ is bounded because for all $(\mathcal{V}, \mathcal{F}) \in \mathcal{L}^-$, $\mathcal{F}_\mu \cup \mathcal{F}$ yields a contradiction, which bounds the probability that the facts $\mathcal{F}_\mu \cup \mathcal{F}$ hold for some $(\mathcal{V}, \mathcal{F}) \in \mathcal{L}$, and $\mathcal{F}_\mu$ holds when $\mu$ is reached while some $\mathcal{F}$ in $\mathcal{L}$ holds when the adversary breaks the property. This is formalized by the following lemma.

**Lemma 64** *The transformation success simplify requires and preserves Properties 1, 2, 3, 4, and 5.*

If transformation **success simplify** transforms $G$ into $G'$, the distinguisher $D$ is a disjunction of Shoup and non-unique events, the property sp and the disjuncts in $D$ correspond to active queries, $\mathcal{L}^- = \{(\mathcal{V}_j, \mathcal{F}_j) \mid j \in J\}$, the modified program points are $\mu_k$ for $k \in K$, $\mathcal{F}_k^{\text{mod}} = \mathcal{F}_{\mu_k}$, for all $A \in \mathcal{BB}$ and all evaluation contexts $C$ acceptable for $G$, $\text{Pr}^A[C[G] \preceq (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+)] \le p(A, C)$, and $\text{Bound}_{G'}(V, sp, D, p')$, then we have $\text{Bound}_G(V, sp, D, p + p')$.

Unfortunately, we cannot prove $D, D_{\text{SNU}} : G, D, \text{EvUsed} \xrightarrow{V} p G', D, \text{EvUsed} \cup \{\text{adv\_loses}\}$ for the transformation **success simplify**, because, in case of (one-session or bit) secrecy of a variable $x$, the inequality needed for this property may not hold: we need to take into account that, when $x$ is not defined, traces that execute $S$ and those that execute $\bar{S}$ compensate in the computation of $\text{Adv}_G(A, C, sp, D)$ in order to prove the soundness of this transformation. We cannot prove this soundness independently for $\text{Pr}^A[C[G] : S]$ and for $\text{Pr}^A[C[G] : \neg \bar{S}]$.

Moreover, in the implementation, for (one-session or bit) secrecy properties, a probability $2p(A, C)$ is added instead of just $p(A, C)$ as shown by the lemma above. The factor 2 is difficult to avoid because other simplifications are performed at the same time as described in the transformation **simplify** (Section 5.1.21), and the factor 2 is needed for these transformations.

## Proof

**Fact 1.** Let $\varphi$ be a correspondence not of the form $\forall \tilde{x} \in \tilde{T}, \text{event}(e(\tilde{N})) \Rightarrow$ false, or the correspondence $\text{event}(e) \Rightarrow$ false for some Shoup event $e$. Let $C$ be any evaluation context acceptable for $G$ with public variables $V$ that does not contain events used by $\varphi$ and $A$ be an attacker in $\mathcal{BB}$. Let $\text{Tr}$ be any full trace of $C[G]$ for $A$ that does not execute any non-unique event of $G$ and such that $\text{Tr} \vdash \neg \varphi$. Then $\text{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

**Proof of Fact 1.** By Lemma 42, for any substitutions $\theta(\mu_1, c_1, \dots, \mu_m, c_m)$ equal to the identity on $\tilde{x}$, for any pseudo-formula $C$,

$$ \mathrm{Tr} \vdash \neg \{[\mathrm{prove}^{\varphi}(C, \theta, S_0)]\} $$

So

$$ \mathrm{Tr} \vdash (\neg \{[\mathrm{prove}^{\varphi}(C, \theta, S_1)]\}) \lor (\bigvee_{(\mu_1, c_1, \dots, \mu_m, c_m) \in S_0 \setminus S_1} \neg \{[\mathrm{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)]\}) . $$
Moreover, $\neg\{[\mathcal{F} \models_{\tilde{\theta}}^{\mathcal{I},\mathcal{V},\mathcal{C}} \phi]\} \Rightarrow \exists \tilde{z} \in \tilde{T}''$, $\wedge \mathcal{F}$ where $\tilde{z} = \mathcal{V}$ and $\tilde{T}''$ are the types of these variables, by an easy induction on $\phi$, so $\neg\{[\text{prove}^{\varphi}(\mathcal{C}, \theta, \mu_1, c_1, \dots, \mu_m, c_m)]\} \Rightarrow \exists \theta_1 I_{\mu_1}, \dots, \exists \theta_m I_{\mu_m}, \exists \tilde{x} \in \tilde{T}$, $\wedge \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$ where, for $j \le m$, $\theta_j$ is a renaming of $I_{\mu_j}$ to fresh replication indices. So

$$ \mathrm{Tr} \vdash (\neg\{[\mathrm{prove}^{\varphi}(\mathcal{C}, \theta, \mathcal{S}_1)]\} \lor (\bigvee_{(\mu_1, c_1, \dots, \mu_m, c_m) \in \mathcal{S}_0 \setminus \mathcal{S}_1} \exists \theta_1 I_{\mu_1}, \dots, \exists \theta_m I_{\mu_m}, \exists \tilde{x} \in \tilde{T}, \wedge \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m})). $$

The formula $\neg\{[\text{prove}^{\varphi}(\mathcal{C}, \theta, \mathcal{S}_1)]\}$ is added to $\mathcal{L}^+$ and $(\tilde{x} \cup \bigcup_{j=1}^m \theta_j I_{\mu_j}, \bigcup_{j=1}^m \theta_j \mathcal{F}_{F_j, \mu_j, c_j})$ is added to $\mathcal{L}^-$ when $(\mu_1, c_1, \dots, \mu_m, c_m) \in \mathcal{S}_0 \setminus \mathcal{S}_1$ (recall that, when $e$ is Shoup event, $e$ is always executed by event_abort $e$) so $\mathrm{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

**Fact 2.** Let $e$ be a non-unique event. Let $C$ be any evaluation context acceptable for $G$ with public variables $V$ that does not contain $e$ and $\mathcal{A}$ be an attacker in $\mathcal{BB}$. Let $\mathrm{Tr}$ be any full trace of $C[G]$ for $\mathcal{A}$ such that $\mathrm{Tr} \vdash e$. Then $\mathrm{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

**Proof of Fact 2.** By Lemma 38, there exist a program point $\mu$ (in $G$) and a case $c$ such that, for any $\theta'$ renaming of $I_\mu$ to fresh replication indices, there exists a mapping $\sigma$ with domain $\theta' I_\mu$ such that $\mathrm{Tr}, \sigma \vdash \theta' \mathcal{F}_{\mathrm{event}(e), \mu, c}^0$. Let $(\mathcal{V}, \mathcal{F}) = (\theta' I_\mu, \theta' \mathcal{F}_{\mathrm{event}(e), \mu, c}^0)$ be the element of $\mathcal{L}^-$ for $\mu$ and $c$, in the treatment of correspondence $\mathrm{event}(e) \Rightarrow$ false. We have $\mathrm{Tr} \vdash \exists \mathcal{V}, \wedge \mathcal{F}$. Therefore, $\mathrm{Tr} \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j$.

**Fact 3.** Let $C$ be any evaluation context acceptable for $G$ with public variables $V$ and $\mathcal{A}$ be an attacker in $\mathcal{BB}$. Let $\mathrm{Tr}$ be any trace of $C[G]$ for $\mathcal{A}$. If $\mathrm{Tr} \vdash \neg \bigvee_{k \in K} \exists I_{\mu_k}, \wedge \mathcal{F}_k^{\mathrm{mod}}$, then there is no configuration in $\mathrm{Tr}$ at a modified program point $\mu_k$.

**Proof of Fact 3.** By contraposition, if there is a configuration $\mathrm{Conf} = E, \sigma, \mu_k M, \mathcal{T}, \mu \mathcal{E} v$ or $\mathrm{Conf} = E, (\sigma, \mu_k P), Q, \mathrm{Or}, \mathcal{T}, \mu \mathcal{E} v$ at a modified program point $\mu_k$ in trace $\mathrm{Tr}$, then let $\theta$ be a renaming of $I_{\mu_k}$ to fresh indices and $\rho = \{\theta I_{\mu_k} \mapsto \sigma I_{\mu_k}\}$; by Corollary 31, $\mathrm{Tr}, \rho \vdash \theta \mathcal{F}_{\mu_k}$. So $\mathrm{Tr}, \rho \vdash \theta \mathcal{F}_k^{\mathrm{mod}}$, so $\mathrm{Tr} \vdash \exists I_{\mu_k}, \wedge \mathcal{F}_k^{\mathrm{mod}}$.

We perform the proof for each query separately.

**Case 1:** sp is some correspondence $\varphi$ different from $\forall \tilde{x} \in \tilde{T}, \mathrm{event}(e(\tilde{N})) \Rightarrow$ false (including sp is true). Let $C$ be any evaluation context acceptable for $G$ with public variables $V$ that does not contain events used by $\varphi$, $D$, nor non-unique events of $G$, and $\mathcal{A}$ be an attacker in $\mathcal{BB}$.

Consider any full trace $\mathrm{Tr}$ of $C[G]$ for $\mathcal{A}$ such that $\mathrm{Tr} \vdash (\neg \varphi \lor D) \wedge \neg \mathrm{NonUnique}_{G,D}$. Let us show that $\mathrm{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \wedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

Case 1.1: $\mathrm{Tr}$ does not execute any non-unique event of $G$. Then $\mathrm{Tr} \vdash \neg \varphi \lor D_s$ where $D_s$ is the disjunction of Shoup events in $D$.

Case 1.1.1: $\mathrm{Tr} \vdash \neg \varphi$ We conclude by Fact 1.

Case 1.1.2: $\mathrm{Tr} \vdash e$ for some Shoup event $e$ in $D_s$. We conclude by Fact 1 for the correspondence $\mathrm{event}(e) \Rightarrow$ false.

Case 1.2: $\mathrm{Tr}$ executes a non-unique event of $G$. Then $\mathrm{Tr} \vdash e$ for some non-unique event $e$ in $G$ and in $D$. We conclude by Fact 2.
If $Tr \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $Tr \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+)$.

Otherwise, by Fact 3, there is no configuration in $Tr$ at a modified program point $\mu_k$, so $Tr$ has a matching trace in $C[G']$ that also satisfies $(\neg \varphi \lor D) \wedge \neg \text{NonUnique}_{G',D}$.

We conclude that

$$ \mathbf{Adv}_G(\mathcal{A}, C, \varphi, D) \leq \mathrm{Pr}^A[C[G] : (\neg \varphi \lor D) \wedge \neg \mathrm{NonUnique}_{G,D}] $$

$$ \leq \mathrm{Pr}^A[C[G] : \left( \bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\mathrm{mod}} \right) \lor (\bigvee \mathcal{L}^+) \right) \\ + \mathrm{Pr}^A[C[G'] : (\neg \varphi \lor D) \wedge \neg \mathrm{NonUnique}_{G',D}] $$

$$ \leq \mathrm{Pr}^A[C[G] \leq \left( \bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\mathrm{mod}} \right) \lor (\bigvee \mathcal{L}^+) ] \\ + \mathrm{Pr}^A[C[G'] : (\neg \varphi \lor D) \wedge \neg \mathrm{NonUnique}_{G',D}] $$

by Lemma 1

$$ \leq p(\mathcal{A}, C) + \mathbf{Adv}_{G'}(\mathcal{A}, C, \varphi, D) $$

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

since $\mathrm{Bound}_{G'}(V, sp, D, p')$

Hence, we have $\mathrm{Bound}_G(V, sp, D, p + p')$.

**Case 2:** sp is some correspondence $\varphi = \forall \tilde{x} \in \tilde{T}, \mathrm{event}(e(\tilde{N})) \Rightarrow$ false. Let C be any evaluation context acceptable for G with public variables V that does not contain events used by $\varphi$, D, nor non-unique events of G, and A be an attacker in BB.

Consider a full trace $Tr$ of $C[G]$ for A such that $Tr \vdash (\neg \varphi \lor D) \wedge \neg \text{NonUnique}_{G,D}$. Let us show that either some prefix of $Tr$ satisfies $(\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+) \text{ or there is a matching trace in } C[G'] \text{ that satisfies } (\neg \varphi \lor D) \wedge \neg \text{NonUnique}_{G',D}$.

We have $Tr \vdash \exists \tilde{x} \in \tilde{T}, \mathrm{event}(e(\tilde{N})) \lor D$.

**Case 2.1:** $Tr$ executes a Shoup event $e'$ of D. Then $Tr \vdash e'$ and $Tr$ is actually a full trace that does not execute any non-unique event of G. By Fact 1, $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge_{F \in \mathcal{F}_j} F) \lor (\bigvee \mathcal{L}^+)$.

**Case 2.2:** $Tr$ executes a non-unique event of G. Then $Tr \vdash e'$ for some non-unique event $e'$ in G and in D. Then $Tr$ is actually a full trace. By Fact 2, $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge_{F \in \mathcal{F}_j} F) \lor (\bigvee \mathcal{L}^+)$.

In cases 2.1 and 2.2,

* If $Tr \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $Tr \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \wedge \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+)$.

* Otherwise, by Fact 3, there is no configuration in $Tr$ at a modified program point $\mu_k$, so $Tr$ has a matching trace in $C[G']$ that also satisfies $(\neg \varphi \lor D) \wedge \neg \text{NonUnique}_{G',D}$.

**Case 2.3:** $Tr$ does not execute any non-unique event of G nor any Shoup event of D. Then $Tr \vdash \exists \tilde{x} \in \tilde{T}, \mathrm{event}(e(\tilde{N}))$.

Let $\mu \in \mathcal{E}v$ be the sequence of events and E be the environment in the last configuration of $Tr$. There is a mapping $\rho$ of the variables $\tilde{x}$ to their values such that $Tr, \rho \vdash e(\tilde{N})$. As in the proof of Lemma 38, there exist $\tilde{a}$ and $\tau \in \mathbb{N}$ such that $\rho, \tilde{N} \downarrow \tilde{a}$ and $\mu \in \mathcal{E}v(\tau) = (\mu, \tilde{a}_0) : e(\tilde{a})$ for some $\mu$ and $\tilde{a}_0$. The rule of the semantics that may have added this element to $\mu \in \mathcal{E}v$ is (Event), (EventAbort), (CtxEvent), (FindE) or (EventT). (It cannot be (Find3) nor (Get3) because e is not a non-unique event. It cannot be (GetE) because G does not contain get by Property 3.)
* Case 2.3.1: In case (Event), we have reductions

$$ 
\begin{align*}
\mathit{Conf} = E_0, (\sigma_0, \mu^{\mathit{event}} e(\widetilde{M}); P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
&\xrightarrow{p_0} t_0 \dots \xrightarrow{p_1} t_1 E_1, (\sigma_1, \mu^{\mathit{event}} e(\tilde{a}); P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_1, \mu\mathcal{E}v_1 \\
&\xrightarrow{1} \mathit{Conf}' = E_1, (\sigma_1, P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_1, (\mu\mathcal{E}v_1, (\mu, \mathit{Im}(\sigma_1)) : e(\tilde{a}))
\end{align*}
$$

where $^{\mu}$event $e(\widetilde{M}); P$ is a subprocess of $C[G]$ up to renaming of oracles, by any number of applications of (Ctx) and a final application of (Event). The terms $\widetilde{M}$ are simple terms (when some term in $\widetilde{M}$ is not simple, no information is collected at all and **simplify** is not performed), so in fact

$$ 
\begin{align*}
\mathit{Conf} = E_0, (\sigma_0, \mu^{\mathit{event}} e(\widetilde{M}); P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
&\xrightarrow{1}^* E_0, (\sigma_0, \mu^{\mathit{event}} e(\tilde{a}); P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
&\xrightarrow{1} \mathit{Conf}' = E_0, (\sigma_0, P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathit{Im}(\sigma_0)) : e(\tilde{a}))
\end{align*}
$$

* Case 2.3.2: In case (EventAbort), we have a reduction

$$ 
\begin{align*}
\mathit{Conf} = E, (\sigma_0, \mu^P) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{p} t \mathit{Conf}' = E, (\sigma_0, \mathit{abort}) &:: \mathit{St}, \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathit{Im}(\sigma_0)) : e)
\end{align*}
$$

where $^{\mu}$P is a subprocess of $C[G]$ up to renaming of oracles, by (EventAbort).

* Case 2.3.3: In case (EventT), we have reductions

$$ 
\begin{align*}
\mathit{Conf} = E_0, \sigma_0, \mu^{\mathit{event}} e(\widetilde{M}); N, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{p_0} t_0 \dots \xrightarrow{p_1} t_1 E_1, \sigma_1, \mu^{\mathit{event}} e(\tilde{a}); N, \mathcal{T}_1, \mu\mathcal{E}v_1 \\
\xrightarrow{1} E_1, \sigma_1, N, \mathcal{T}_1, (\mu\mathcal{E}v_1, (\mu, \mathit{Im}(\sigma_1)) : e(\tilde{a}))
\end{align*}
$$

where $^{\mu}$event $e(\widetilde{M}); N$ is a subterm of $C[G]$, by any number of applications of (CtxT) and a final application of (EventT). The terms $\widetilde{M}$ are simple terms, so in fact

$$ 
\begin{align*}
\mathit{Conf} = E_0, \sigma_0, \mu^{\mathit{event}} e(\widetilde{M}); N, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{1}^* E_0, \sigma_0, \mu^{\mathit{event}} e(\tilde{a}); N, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{1} E_0, \sigma_0, N, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathit{Im}(\sigma_0)) : e(\tilde{a}))
\end{align*}
$$

By Invariant 4, $\mu$ is not inside a condition of find or get, so by Lemma 5, Conf is not in the derivation of an hypothesis of a rule for find or get. The only rule for processes other than those for find or get that evaluates a non-simple term is (Ctx) and similarly, the only rule for terms other than those for find or get that evaluates a term is (CtxT), so we have

$$ 
\begin{align*}
E_0, (\sigma_0, C_0[C_1[\dots C_k[\mu^{\mathit{event}} e(\widetilde{M}); N]\dots]]], \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{1}^* \mathit{Conf}' = E_0, (\sigma_0, C_0[C_1[\dots C_k[N]\dots]]), \mathcal{Q}_0, \mathcal{Or}_0, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathit{Im}(\sigma_0)) : e(\tilde{a}))
\end{align*}
$$

for some $C_0$ context defined in Figure 12, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 7, by $k$ applications of (CtxT) and one application of (Ctx).
* Case 2.3.4: In case (CtxEvent), we have

$$ Conf = E_0, \sigma_0, \mu^{\text{event\_abort}} e, \mathcal{T}_0, \mu e v_0 \xrightarrow{p} e E_0, \sigma_0, \text{event\_abort}(\mu, \text{Im}(\sigma_0)) : e, \mathcal{T}_0, \mu e v_0 $$

by (EventAbortT) where $\mu^{\text{event\_abort}} e$ is a subterm of $C[G]$, followed by applications (FindTE), (CxtT), (CxtEventT), (FindE), (Cxt), and (CxtEvent). We let $Conf'$ be the last configuration of $Tr$.

Let $\theta'$ be a renaming of $I_\mu$ to fresh replication indices. We have

$$ \begin{gathered} \text{prove}^{\varphi}(C, \theta_0, \mu, c) = (\theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c}) \text{ yields a contradiction}, \\ \{[\text{prove}^{\varphi}(C, \theta_0, \mu, c)]\} = \forall \theta' I_\mu, \forall \tilde{x} \in \tilde{T}, \neg \bigwedge \theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c}, \\ C \text{ is a pseudo-formula with all leaves } \perp, \text{ so } \{[\vdash C]\} = \text{true.} \end{gathered} $$

If $(\mu, c) \in S_0 \setminus S_1$, then in cases 2.3.1 and 2.3.3, $(\tilde{x} \cup \theta' I_\mu, \theta' \mathcal{F}_{\mu, c} \cup \{\text{lastdefprogrampoint}(\mu, \theta' I_\mu), \tilde{N} = \theta' \tilde{M}\})$ is added to $\mathcal{L}^-$ and in cases 2.3.2 and 2.3.4, $(\theta' I_\mu, \theta' \mathcal{F}_{\text{event}(e), \mu, c})$ is added to $\mathcal{L}^-$. Moreover, $\neg \{[\text{prove}^{\varphi}(C, \theta_0, S_1)]\} = \bigvee_{(\mu, c) \in S_1} \exists \theta' I_\mu, \exists \tilde{x} \in \tilde{T}, \bigwedge \theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c}$ is added to $\mathcal{L}^+$.

As in the proof of Lemma 38, we have $\sigma_0 = [I_\mu \mapsto \tilde{a}_0]$. Let $\sigma = \{\theta' I_\mu \mapsto \tilde{a}_0\}$. As in the proof of Lemma 38, we have $Tr, \sigma \cup \rho \vdash \theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c}$, since $Tr$ does not execute any non-unique event of $G$.

* In cases 2.3.1 and 2.3.3 when $(\mu, c) \in S_1$ and in cases 2.3.2 and 2.3.4, we have $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

- If $Tr \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $Tr \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \land \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+)$.

- Otherwise, by Fact 3, there is no configuration in $Tr$ at a modified program point $\mu_k$, so $Tr$ has a matching trace in $C[G']$ that also satisfies $(\neg \varphi \lor D) \land \neg \text{NonUnique}_{G', D}$.

* In cases 2.3.1 and 2.3.3 when $(\mu, c) \in S_0 \setminus S_1$, let $Tr'$ be the prefix of $Tr$ that stops at $Conf'$. We have $Conf \preceq_{Tr} Conf'$, so by Corollary 3, $Tr \preceq Conf'$, $\sigma \vdash \theta' \mathcal{F}_{\mu, c}$, that is, $Tr'$, $\sigma \vdash \theta' \mathcal{F}_{\mu, c}$. We have $E_0, \sigma_0, \tilde{M} \llcorner \tilde{a}$, so $E_0, \sigma, \theta' \tilde{M} \llcorner \tilde{a}$. The environment $E_{Tr'}$ extends $E_0$, so $E_{Tr'}$, $\sigma, \theta' \tilde{M} \llcorner \tilde{a}$, so $Tr'$, $\sigma \cup \rho \vdash \theta' \tilde{M} = \tilde{N}$. Since $E_{Tr' \preceq Conf'} = E_{Tr' \preceq Conf}$ and $\sigma_{Conf'} = \sigma_{Conf}$, $Tr'$, $\sigma \vdash \text{lastdefprogrampoint}(\mu, \theta' \tilde{i})$. Hence $Tr' \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j$.

- If $Tr' \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $Tr' \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \land \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+) \text{ and } Tr'$ is a prefix of $Tr$.

- Otherwise, by Fact 3, there is no configuration in $Tr'$ at a modified program point $\mu_k$, so $Tr'$ has a matching trace in $C[G']$ that also satisfies $(\neg \varphi \lor D) \land \neg \text{NonUnique}_{G', D}$. (Note that $Tr'$ may still be modified by **success simplify**: the matching trace in $C[G']$ may execute a modified program point $\mu_k$ after $Conf'$, but still the matching trace executes $e(\tilde{M})$, so satisfies $\neg \varphi$, and it does not execute any non-unique event of $G'$.)
We conclude that

$$
\begin{align*}
\mathrm{Adv}_G(\mathcal{A}, C, \varphi, D) &= \Pr^A[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G,D}] \\
&\leq \Pr^A[C[G] \leq \left( \bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j \land \bigwedge \mathcal{F}_k^{\mathrm{mod}} \right) \lor \left( \bigvee \mathcal{L}^+ \right)] \\
&\quad + \Pr^A[C[G'] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G',D}] \\
&\leq p(\mathcal{A}, C) + \mathrm{Adv}_{G'}(\mathcal{A}, C, \varphi, D) \\
&\leq p(\mathcal{A}, C) + p'(\mathcal{A}, C) \tag*{since $\mathrm{Bound}_{G'}(V, sp, D, p')$}
\end{align*}
$$

Hence, we have $\mathrm{Bound}_G(V, sp, D, p + p')$.

**Case 3:** sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x) with $C = C'[C_{sp}[]]$ and x is defined only by $\leftarrow^R$ or by assignments of variables defined by $\leftarrow^R$. Let $C'$ be any evaluation context acceptable for $C_{sp}[G]$ with public variables $V \setminus V_{sp}$ that does not contain $\overline{S}$, $\overline{S}$, any event in $D$, nor any non-unique event of $G$, and $\mathcal{A}$ be an attacker in $\mathcal{BB}$.

$$
\begin{align*}
\mathrm{Adv}_G(\mathcal{A}, C, sp, D) \\
&= \Pr^A[C[G] : \mathcal{S} \lor D] - \Pr^A[C[G] : \overline{\mathcal{S}} \lor \mathrm{NonUnique}_{G,D}] \\
&= \Pr^A[C[G] : \mathcal{S}] + \Pr^A[C[G] : D] - \Pr^A[C[G] : \overline{\mathcal{S}}] - \Pr^A[C[G] : \mathrm{NonUnique}_{G,D}] \\
&\qquad \text{since these events are mutually exclusive} \\
&= \Pr^A[C[G] : \mathcal{S} \land \neg sp] + \Pr^A[C[G] : D] \\
&\quad - \Pr^A[C[G] : \overline{\mathcal{S}} \land \neg sp] - \Pr^A[C[G] : \mathrm{NonUnique}_{G,D}] \tag*{by Lemma 36} \\
&= \Pr^A[C[G] : (\mathcal{S} \land \neg sp) \lor D] - \Pr^A[C[G] : \overline{\mathcal{S}} \land \neg sp] - \Pr^A[C[G] : \mathrm{NonUnique}_{G,D}]
\end{align*}
$$

We have

* $\Pr^A[C[G'] : \mathrm{NonUnique}_{G',D}] \leq \Pr^A[C[G] : \mathrm{NonUnique}_{G,D}]$

* $\Pr^A[C[G'] : \overline{\mathcal{S}} \land \neg sp] \leq \Pr^A[C[G] : \overline{\mathcal{S}} \land \neg sp]$

since a trace that executes a non-unique event or $\overline{\mathcal{S}}$ in $G'$ cannot execute event adv loses, so it executed without change in $G$. Let us show that $\Pr^A[C[G] : (\mathcal{S} \land \neg sp) \lor D] \leq p(\mathcal{A}, C) + \Pr^A[C[G'] : (\mathcal{S} \land \neg sp) \lor D]$. Let $\mathrm{Tr}$ be a full trace of $C[G]$ for $\mathcal{A}$ such that $\mathrm{Tr} \vdash (\mathcal{S} \land \neg sp) \lor D$. Let us show that $\mathrm{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

Case 3.1: $\mathrm{Tr}$ executes a non-unique event of $G$. Then $\mathrm{Tr} \vdash e$ for some non-unique event $e$ in $G$ and in $D$. We conclude by Fact 2.

Case 3.2: $\mathrm{Tr} \vdash e$ for some Shoup event $e$ in $D$. Then $\mathrm{Tr}$ does not execute any non-unique event of $G$. We conclude by Fact 1 for the correspondence $\mathrm{event}(e) \Rightarrow$ false.

Case 3.3: $\mathrm{Tr} \vdash \mathcal{S} \land \neg sp$. Since $\mathrm{Tr} \vdash \neg sp$, we have $\mathrm{Tr} \vdash \neg\{[\mathrm{prove}^{sp}(\mathrm{Tpp}(\mathrm{Tr}))]\}$, so we are in one of the following two cases:

* There exists $\mu \in \mathrm{Tpp}(\mathrm{Tr})$ such that $\mathrm{Tr} \vdash \neg\{[\mathrm{prove}^{1\text{-ses.secr.}(x)}(\mu)]\}$.

- If $\mu \in S_1$, then $\mathrm{Tr} \vdash \bigvee \mathcal{L}^+$ since $\neg\{[\mathrm{prove}^{1\text{-ses.secr.}(x)}(S_1)]\}$ is added to $\mathcal{L}^+$.

- If $\mu \in S_0 \setminus S_1$, then $(\theta I_\mu, \theta \mathcal{F}_\mu)$ is added to $\mathcal{L}^-$, where $\theta$ is a renaming of $I_\mu$ to fresh replication indices. Moreover, we have $\neg\{[\mathrm{noleak}(z[\widetilde{M'}, \mathcal{I}, \mathcal{F}])]\} \Rightarrow \exists \mathcal{I}, \bigwedge \mathcal{F}$, so $\neg\{[\mathrm{prove}^{1\text{-ses.secr.}(x)}(\mu)]\} \Rightarrow \exists \theta I_\mu, \bigwedge \theta \mathcal{F}_\mu$ since $\mathrm{defRand}_\mu(x)$ is defined. Therefore, $\mathrm{Tr} \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j$.
* In case $sp = \text{Secrecy}(x)$, there exist $\mu_1, \mu_2 \in \text{Tpp}(\text{Tr})$ such that $\text{Tr} \vdash \neg[\text{prove}^{\text{distinct}}(x)(\mu_1, \mu_2)]$. Let $z_1[\tilde{M}_1] = \text{defRand}_{\mu_1}(x)$, $z_2[\tilde{M}_2] = \text{defRand}_{\mu_2}(x)$, $\tilde{i}$ be the current replication indices at the definition of $x$, $\theta_1$ and $\theta_2$ be two distinct renamings of $\tilde{i}$ to fresh replication indices, $\tilde{i}_1 = \theta_1\tilde{i}$, $\tilde{i}_2 = \theta_2\tilde{i}$, and $\mathcal{F} = \theta_1\mathcal{F}_{\mu_1} \cup \theta_2\mathcal{F}_{\mu_2} \cup \{\theta_1\tilde{M}_1 = \theta_2\tilde{M}_2, \tilde{i}_1 \neq \tilde{i}_2\}$ Then $z_1 = z_2$ and $\text{Tr} \vdash \exists\tilde{i}_1, \exists\tilde{i}_2, \wedge\mathcal{F}$.

- If $\mathcal{F}$ yields a contradiction, then $\exists\tilde{i}_1, \exists\tilde{i}_2, \wedge\mathcal{F}$ is added to $\mathcal{L}^+$, so $\text{Tr} \vdash \bigvee\mathcal{L}^+$.

- Otherwise, $(\tilde{i}_1 \cup \tilde{i}_2, \mathcal{F})$ is added to $\mathcal{L}^-$, so $\text{Tr} \vdash \bigvee_{j \in J} \exists\mathcal{V}_j, \wedge\mathcal{F}_j$.

If $\text{Tr} \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \wedge\mathcal{F}_k^{\text{mod}}$, then $\text{Tr} \vdash (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists\mathcal{V}_j, \wedge\mathcal{F}_j \wedge \wedge\mathcal{F}_k^{\text{mod}}) \vee (\bigvee\mathcal{L}^+)$.

Otherwise, by Fact 3, there is no configuration in $\text{Tr}$ at a modified program point $\mu_k$, so $\text{Tr}$ has a matching trace in $C[G']$ that also satisfies $(S \wedge \neg sp) \vee D$.

Therefore, $\text{Pr}^A[C[G] : (S \wedge \neg sp) \vee D] \le p(A, C) + \text{Pr}^A[C[G'] : (S \wedge \neg sp) \vee D]$, so

$\text{Adv}_G(A, C, sp, D)$

$$ \le p(A, C) + \text{Pr}^A[C[G'] : (S \wedge \neg sp) \vee D] - \text{Pr}^A[C[G'] : \bar{S} \wedge \neg sp] - \text{Pr}^A[C[G'] : \text{NonUnique}_{G',D}] $$

Moreover, by applying on $G'$ the same steps as on $G$ at the beginning of this proof, we have

$\text{Adv}_{G'}(A, C, sp, D)$

$$ = \text{Pr}^A[C[G'] : (S \wedge \neg sp) \vee D] - \text{Pr}^A[C[G'] : \bar{S} \wedge \neg sp] - \text{Pr}^A[C[G'] : \text{NonUnique}_{G',D}] $$

so

$$ \text{Adv}_G(A, C, sp, D) \le p(A, C) + \text{Adv}_{G'}(A, C, sp, D) \le p(A, C) + p'(A, C) $$

since $\text{Bound}_{G'}(V, sp, D, p')$. Therefore, we have $\text{Bound}_G(V, sp, D, p+p')$. $\square$

## 5.2 crypto: Applying the Security Assumptions on Primitives

**Extension:** This description is based on the first version of the crypto transformation. Some extensions and improvements have been implemented since then.

### 5.2.1 Basic Transformation

The security of cryptographic primitives is defined using observational equivalences given as axioms. Importantly, this formalism allows us to specify many different primitives in a generic way. Such equivalences are then used by the prover in order to transform a game into another, observationally equivalent game, as explained below in this section.

The primitives are specified using equivalences of the form $G_1 | \dots | G_m \approx G'_1 | \dots | G'_m$ where $G$ is defined by the following grammar, with $l \ge 0$ and $m \ge 1$:

$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l}
G ::= & \multicolumn{2}{l}{\text{group of oracles}} \\
& \multicolumn{2}{l}{\text{foreach } i \le n \text{ do } y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l; (G_1 | \dots | G_m)} \\
& & \text{replication, random choices} \\
& O(x_1 : T_1, \dots, x_l : T_l) ::= FP & \text{oracle}
\end{array}
$$

$$
\begin{array}{l@{\hspace{2em}}l}
\text{FP ::=} & \text{oracle body} \\
\text{return (M)} & \text{return} \\
x[\tilde{i}] \stackrel{R}{\leftarrow} T; \text{FP} & \text{random number}
\end{array}
$$
let $x[\tilde{i}] : T = M$ in FP assignment
find $(\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] \le \tilde{n}_j$ such that $\text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j$ then FP$_j)$ else FP array lookup

Intuitively, $O(x_1 : T_1, \dots, x_l : T_l) := FP$ represents an oracle that takes as argument values $x_1, \dots, x_l$ of types $T_1, \dots, T_l$ respectively and returns a result computed by FP. The observational equivalence $G_1 | \dots | G_m \approx G'_1 | \dots | G'_m$ expresses that the adversary has a negligible probability of distinguishing oracles in the left-hand side from corresponding oracles in the right-hand side. Formally, groups of oracles can be encoded as oracle definitions that take as input their arguments and return their result, as shown in Figure 23: $\llbracket G \rrbracket_i^j$ denotes the translation of the group of oracles $G$ into an oracle definition. The translation of $\text{foreach } i \le n \text{ do } y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l; (G_1 | \dots | G_m)$ defines oracle $O_j$ so that the context can trigger the generation of random numbers $y_1, \dots, y_l$. (In the left-hand side of equivalences, the result FP of oracles must simply be a return return ($M$) where $M$ is a simple term.) The observational equivalence $G_1 | \dots | G_m \approx G'_1 | \dots | G'_m$ is then an abbreviation for $\llbracket G_1 | \dots | G_m \rrbracket \approx \llbracket G'_1 | \dots | G'_m \rrbracket$.

For example, the security of a MAC (Definition 2) is represented by the equivalence $L \approx R$ where:

$$
\begin{align*}
L &= \text{foreach } i'' \le n'' \text{ do } k \stackrel{R}{\leftarrow} T_{mk}; ( \\
  &\quad \text{foreach } i \le n \text{ do } O_m(x : \text{bitstring}) := \text{return } (\text{mac}(x, k)) \\
  &\quad | \text{foreach } i' \le n' \text{ do } O_v(m : \text{bitstring}, ma : T_{ms}) := \text{return } (\text{verify}(m, k, ma))) \\
R &= \text{foreach } i'' \le n'' \text{ do } k \stackrel{R}{\leftarrow} T_{mk}; ( \\
  &\quad \text{foreach } i \le n \text{ do } O_m(x : \text{bitstring}) := \text{return } (\text{mac}'(x, k)), \\
  &\quad | \text{foreach } i' \le n' \text{ do } O_v(m : \text{bitstring}, ma : T_{ms}) := \\
  &\quad \quad \text{find } u \le n \text{ such that } \text{defined}(x[u]) \wedge (m = x[u]) \\
  &\quad \quad \wedge \text{verify}'(m, k, ma) \text{ then return } (\text{true}) \text{ else return } (\text{false}))
\end{align*}
$$

where mac' and verify' are function symbols with the same types as mac and verify respectively. (We use different function symbols on the left- and right-hand sides, just to prevent a repeated application of the transformation induced by this equivalence. Since we add these function symbols, we also add the equation

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

which restates (mac) for mac' and verify'.) Intuitively, the equivalence $L \approx R$ leaves MAC computations unchanged (except for the use of primed function symbols in $R$), and allows one to replace a MAC checking $\text{verify}(m, k, ma)$ with a lookup in the array $x$ of messages whose mac has been computed with key $k$: if $m$ is found in the array $x$ and $\text{verify}(m, k, ma)$, we return true; otherwise, the check fails (up to negligible probability), so we return false. (If the check succeeded with $m$ not in the array $x$, the adversary would have forged a MAC.) Obviously, the form of $L$ requires that $r$ is used only to compute or check MACs, for the equivalence to be correct. Formally, the following result shows the correctness of our modeling. It is a fairly easy consequence of Definition 2, and is proved in [26, Appendix E.3].

**Proposition 5** If (mac, verify) is a UF-CMA message authentication code, mac' = mac, and verify' = verify, then $\llbracket L \rrbracket \approx \llbracket R \rrbracket$.
$$ 
\begin{align*}
& [[G_1 | \dots | G_m]] = [[G_1]]^1 | \dots | [[G_m]]^m \\
& [[\text{foreach } i \le n \text{ do } y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l; (G_1 | \dots | G_m)]_{\tilde{i}}^{\tilde{j}} = \\
& \quad \text{foreach } i \le n \text{ do } O_{\tilde{j}}[\tilde{i}, i]() := y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l; \text{return } (); ([[G_1]]_{\tilde{i},i}^{\tilde{j},1} | \dots | [[G_m]]_{\tilde{i},i}^{\tilde{j},m}) \\
& [[O(x_1 : T_1, \dots, x_l : T_l) := FP]]_{\tilde{i}}^{\tilde{j}} = O[\tilde{i}](x_1 : T_1, \dots, x_l : T_l) := FP
\end{align*}
$$

where $O_{\tilde{j}}$ are pairwise distinct oracles, $\tilde{i} = i_1, \dots, i_{l'}$, and $\tilde{j} = j_0, \dots, j_{l'}$.

<caption>Figure 23: Translation from groups of oracles to oracle definitions</caption>

Similarly, if (enc, dec) is an IND-CPA symmetric encryption scheme (Definition 3), then we have the following equivalence:

$$ 
\begin{align*}
& \text{foreach } i' \le n' \text{ do } k \stackrel{R}{\leftarrow} T_k; \text{foreach } i \le n \text{ do} \\
& \qquad O_e(x : \text{bitstring}) := r \stackrel{R}{\leftarrow} T_r; \text{return } (\text{enc}(x, k, r)) \tag{enc\text{eq}} \\
& \approx \text{foreach } i' \le n' \text{ do } k \stackrel{R}{\leftarrow} T_k; \text{foreach } i \le n \text{ do} \\
& \qquad O_e(x : \text{bitstring}) := r \stackrel{R}{\leftarrow} T_r; \text{return } (\text{enc}'(Z(x), k, r))
\end{align*}
$$

where $enc'$ is a function symbol with the same type as $enc$, and $Z : \text{bitstring} \to \text{bitstring}$ is the function that returns a bitstring of the same length as its argument, consisting only of zeroes. Using equations such as $\forall x : T, Z(T2b(x)) = Z_T$, we can prove that $Z(T2b(x))$ does not depend on $x$ when $x$ is of a fixed-length type and $T2b : T \to \text{bitstring}$ is the natural injection. The equivalences that formalize the security assumptions on primitives are designed and proved correct by hand from security assumptions in a more standard form, as in the MAC example. Importantly, these manual proofs are done only once for each primitive, and the obtained equivalence can be reused for proving many different protocols automatically.

We use such equivalences $L \approx R$ in order to transform a process $Q_0$ observationally equivalent to $C[[L]]$ into a process $Q'_0$ observationally equivalent to $C[[R]]$, for some evaluation context $C$. In order to check that $Q_0 \approx^V C[[L]]$, the prover uses sufficient conditions, which essentially guarantee that all uses of certain secret variables of $Q_0$, in a set $S$, can be implemented by calling oracles of $L$. Let $\mathcal{M}$ be a set of occurrences of terms, corresponding to uses of variables of $S$. Informally, the prover shows the following properties.

* For each $M \in \mathcal{M}$, there exist a term $N_M$, which is the return value of an oracle of $L$, and a substitution $\sigma_M$ such that $M = \sigma_M N_M$. (Precisely, $\sigma_M$ applies to the abbreviated form of $N_M$ in which we write $x$ instead of $x[\tilde{i}]$.) Intuitively, the evaluation of $M$ in $Q_0$ will correspond to a call to the oracle returning $N_M$ in $C[[L]]$.

* The variables of $S$ do not occur in $V$, are bound by random choices in $Q_0$, and occur only in terms $M = \sigma_M N_M \in \mathcal{M}$ in $Q_0$, at occurrences that are images by $\sigma_M$ of variables bound by random choices in $L$. (To be precise, the variables of $S$ are also allowed to occur at the root of defined conditions; in that case, their value does not matter, just the fact that they are defined.)

* Let $\tilde{i}$ and $\tilde{i}'$ be the sequences of current replication indices at $N_M$ in $L$ and at $M$ in $Q_0$, respectively. The prover shows that there exists a function $map\text{Idx}_M$ that maps the array indices at $M$ in $Q_0$ to the array indices at $N_M$ in $L$: the evaluation of $M$ when
$\tilde{i}' = \tilde{a}$ will correspond in $C[[L]]$ to the evaluation of $N_M$ when $\tilde{i} = \text{mapIdx}_M(\tilde{a})$. Thus, $\sigma_M$ and $\text{mapIdx}_M$ induce a correspondence between terms and variables of $Q_0$ and variables of $L$: for all $M \in \mathcal{M}$, for all $x[i'']$ that occur in $N_M$, $(\sigma_M x)\{\tilde{a}/i''\}$ corresponds to $x[i'']\{\text{mapIdx}_M(\tilde{a})/i'\}$, that is, $(\sigma_M x)\{\tilde{a}/i''\}$ in a trace of $Q_0$ has the same value as $x[i'']\{\text{mapIdx}_M(\tilde{a})/i'\}$ in the corresponding trace of $C[[L]]$ ($i''$ is a prefix of $i'$). We detail below conditions that this correspondence has to satisfy.

For example, consider a process $Q_0$ that contains $M_1 = \text{enc}(M'_1, x_k, x'_r[i_1])$ under a replication *foreach* $i_1 \le n_1$ *do* and $M_2 = \text{enc}(M'_2, x_k, x''_r[i_2])$ under a replication *foreach* $i_2 \le n_2$ *do*, where $x_k, x'_r, x''_r$ are bound by random choices. Let $S = \{x_k, x'_r, x''_r\}$, $\mathcal{M} = \{M_1, M_2\}$, and $N_{M_1} = N_{M_2} = \text{enc}(x[i', i], k[i'], r[i', i])$. The functions $\text{mapIdx}_{M_1}$ and $\text{mapIdx}_{M_2}$ are defined by

$$ \text{mapIdx}_{M_1}(a_1) = (1, a_1) \text{ for } a_1 \in [1, n_1] $$

$$ \text{mapIdx}_{M_2}(a_2) = (1, a_2 + n_1) \text{ for } a_2 \in [1, n_2] $$

Then $M'_1\{a_1/i_1\}$ corresponds to $x[1, a_1]$, $x_k$ to $k[1]$, $x'_r[a_1]$ to $r[1, a_1]$, $M'_2\{a_2/i_2\}$ to $x[1, a_2 + n_1]$, and $x''_r[a_2]$ to $r[1, a_2 + n_1]$. The functions $\text{mapIdx}_{M_1}$ and $\text{mapIdx}_{M_2}$ are such that $x'_r[a_1]$ and $x''_r[a_2]$ never correspond to the same cell of $r$; indeed, $x'_r[a_1]$ and $x''_r[a_2]$ are independent random numbers in $Q_0$, so their images in $C[[L]]$ must also be independent random numbers.

The above correspondence must satisfy the following soundness conditions:

* when $x$ is an oracle argument in $L$, the term that corresponds to $x[\tilde{a}']$ must have the same type as $x[\tilde{a}']$, and when two terms correspond to the same $x[\tilde{a}']$, they must evaluate to the same value;

* when $x$ is bound by $x \stackrel{R}{\leftarrow} T$ in $L$, the term that corresponds to $x[\tilde{a}']$ must evaluate to $z[\tilde{a}']$ where $z \in S$ and $z$ is bound by $z \stackrel{R}{\leftarrow} T$ in $Q_0$, and the relation that associates $z[\tilde{a}']$ to $x[\tilde{a}']$ is an injective function (so that independent random numbers in $L$ correspond to independent random numbers in $Q_0$).

It is easy to check that, in the previous example, these conditions are satisfied.

The transformation of $Q_0$ into $Q'_0$ consists in two steps. First, we replace the random choices that define variables of $S$ with random choices that define fresh variables corresponding to variables bound by $\stackrel{R}{\leftarrow}$ in $R$. The correspondence between variables of $Q_0$ and variables of $C[[L]]$ is extended to include these fresh variables. Second, we reorganize $Q_0$ so that each evaluation of a term $M \in \mathcal{M}$ first stores the values of the arguments $x_1, \dots, x_m$ of the oracle $O(x_1 : T_1, \dots, x_m : T_m) := C[\text{return } (N_M)]$ in fresh variables, then computes $N_M$ and stores its result in a fresh variable, and uses this variable instead of $M$; then we simply replace the computation of $N_M$ with the corresponding oracle call of $R$, taking into account the correspondence of variables.

Next, we formalize this transformation. We require the following conditions for the equiva-
lences $L \approx R$ that model cryptographic primitives:

H0. $[[L]]$ and $[[R]]$ satisfy Invariants 1, 2, and 8. The oracle names in $L$ (resp. $R$) are pairwise distinct. Furthermore, the return value of each oracle in $R$ has the same type as the return value of the corresponding oracle of $L$.

H1. In $L$, the oracles bodies $FP$ are simply returns of terms $M$; all their array accesses use the current replication indices. (Allowing let or find in $L$ is difficult, because we need to recognize the terms $M$ in a context and in a possibly syntactically modified form.)
H2. L and R have the same structure: same replications, same number of oracles, same oracle names, same number of arguments with the same types for each oracle.

H3. The variables $y_j$ defined by $\stackrel{R}{\leftarrow}$ and $x_j$ defined by oracle arguments in L and R are distinct from other variables defined in R.

H4. Under **foreach** $i \le n$ **do** with no random choice in L, one can have only a single oracle $O(x_1: T_1, \dots, x_l: T_l) := FP$. (One can transform **foreach** $i \le n$ **do** $(O_1(\tilde{x}_1: \tilde{T}_1) := FP_1$ | ... | $O_m(\tilde{x}_m: \tilde{T}_m) := FP_m$ | **foreach** $i_1 \le n_1$ **do** ... | ... | **foreach** $i_{m'} \le n_{m'}$ **do** ...) into $(\mathbf{foreach} \ i \le n \ \mathbf{do} \ O_1(\tilde{x}_1: \tilde{T}_1) := FP_1 \ | \ \dots \ | \ \mathbf{foreach} \ i \le n \ \mathbf{do} \ O_m(\tilde{x}_m: \tilde{T}_m) := FP_m \ | \ \dots \ | \ \mathbf{foreach} \ i_1 \le n'_1 \ \mathbf{do} \ \dots \ | \ \dots \ | \ \mathbf{foreach} \ i_{m'} \le n'_{m'} \ \mathbf{do} \ \dots)$ in order to eliminate situations that do not satisfy this requirement.)

H5. Replications in L (resp. R) must have pairwise distinct bounds $n$. (This strengthens the typing: the typing then guarantees that, if several variables are accessed with the same array indices, then these variables are defined under the same replication.)

H6. For all random choices $y \stackrel{R}{\leftarrow} T$ that occur above a term $M$ in L, $y$ occurs in M. (This guarantees that, in Hypothesis H'3.1 below, $z_{jk}[M_{j1}, \dots, M_{jq_j}]$ is defined for all $j \le l$ and $k \le m_j$. With Hypothesis H4, this guarantees that $\text{index}_j$ is well-defined in Hypothesis H'3.1.3 below.)

H7. Finds in R are of the form

$$ \text{find} (\bigoplus_{j=1}^{m} \tilde{u}_j \le \tilde{n}_j \text{ such that defined}(z_{j1}[\tilde{u}_{j1}], \dots, z_{jl_j}[\tilde{u}_{jl_j}]) \land M_j \text{ then } FP_j) \text{ else } FP' $$

where the following conditions are satisfied:

* For all $1 \le k \le l_j$, $\tilde{u}_{jk}$ is the concatenation of a prefix of the current replication indices (the same prefix for all $k$) and a non-empty prefix of $\tilde{u}_j$.

* When $\tilde{u}_j$ is non-empty, at least one $\tilde{u}_{jk}$ for $1 \le k \le l_j$ is the concatenation of a prefix of the current replication indices with the whole sequence $\tilde{u}_j$.

* When $l_j \ne 0$, there exists $k \in \{1, \dots, l_j\}$ such that for all $k' \ne k$, $z_{jk'}$ is defined syntactically above all definitions of $z_{jk}$ and $\tilde{u}_{jk'}$ is a prefix of $\tilde{u}_{jk}$. (This implies that the same find cannot access variables defined in different oracles under the same replication in R.)

* Finally, variables $z_{jk}$ are not defined by a find in R. (Otherwise, the transformation would be considerably more complicated.)

Such equivalences $L \approx R$ are used by the prover by replacing a process $Q_0$ observationally equivalent to $C[[L]]$ with a process $Q'_0$ observationally equivalent to $C[[R]]$, for some evaluation context $C$. We now give sufficient conditions for a process to be equivalent to $C[[L]]$. These conditions essentially guarantee that all uses of certain secret variables of $Q_0$, in a set $S$, can be implemented by calling oracles of L. These conditions are explained in more detail below.

We first define the function extract used in order to extract information from the left- or right-hand sides of the equivalence.

$$ \begin{aligned} \text{extract}(O(x_1: T_1, \dots, x_l: T_l) := FP, \emptyset) &= \\ O(x_1: T_1, \dots, x_l: T_l) := FP \end{aligned} $$
$$
\begin{align*}
\text{extract}(\text{foreach } i \le n \text{ do } y_1 \underset{R}{\stackrel{R}{\leftarrow}} T_1; \dots; y_l \underset{R}{\stackrel{R}{\leftarrow}} T_l; (G_1 | \dots | G_m), (j_1, \dots, j_k)) &= \\
&\quad (y_1 : T_1, \dots, y_l : T_l), \text{extract}(G_{j_1}, (j_2, \dots, j_k)) \\
\text{extract}((G_1 | \dots | G_m), (j_0, \dots, j_k)) &= \\
&\quad \text{extract}(G_{j_0}, (j_1, \dots, j_k))
\end{align*}
$$

We rename the variables of $Q_0$ such that variables of $L$ and $R$ do not occur in $Q_0$. Assume that there exist a set of variables $S$ and a set $\mathcal{M}$ of occurrences of terms in $Q_0$ such that:

H'1. $S \cap V = \emptyset$.

H'2. No term in $\mathcal{M}$ occurs in the condition part of a find (defined($M_1, \dots, M_l$) ∧ $\mathcal{M}$).

H'3. For each $M \in \mathcal{M}$, there exist a sequence $BL(M) = (j_0, \dots, j_l)$ such that $\text{extract}(L, BL(M)) = (y_{11} : T_{11}, \dots, y_{1m_1} : T_{1m_1}), \dots, (y_{l1} : T_{l1}, \dots, y_{lm_l} : T_{lm_l}), O(x_1 : T_1, \dots, x_m : T_m) := \text{return } (N)$ and a substitution $\sigma$ such that $M = \sigma N$ ($\sigma$ applies to the abbreviated form of $N$ in which we write $x$ instead of $x[\tilde{i}]$) and the following conditions hold:

H'3.1. For all $j \le l$ and $k \le m_j$, $\sigma y_{jk}$ is a variable access $z_{jk}[M_{j1}, \dots, M_{jq_j}]$, with $z_{jk} \in S$. We define $z_{jk} = \text{varImL}(y_{jk}, M)$.

H'3.1.1. All definitions of $z_{jk}$ in $Q_0$ are of the form $z_{jk}[\dots] \stackrel{R}{\leftarrow} T_{jk}$, and for all $k \le m_j$, they occur under the same replications (but they may occur under different replications for different values of $j$).

H'3.1.2. When $j \neq j'$ or $k \neq k'$, $z_{jk} \neq z_{j'k'}$.

H'3.1.3. The sequence of array indices $M_{j1}, \dots, M_{jq_j}$ is the same for all $k \le m_j$ (but may depend on $j$). We denote by $\text{index}_j(M)$ a substitution that maps the current replication indices at the definition of $z_{jk}$ to $M_{j1}, \dots, M_{jq_j}$ respectively. If $m_l = 0$, $\text{index}_l(M)$ is not set by the previous definition, so we set $\text{index}_l(M)$ to map the current replication indices at $M$ to themselves. For each $j < l$, there exists a substitution $\rho_j(M)$ such that $\text{index}_j(M) = \text{index}_{j+1}(M) \circ \rho_j(M)$ and the image of $\rho_j(M)$ does not contain the current replication indices at $M$. We denote by $\text{im index}_j(M)$ the sequence image by $\text{index}_j(M)$ of the sequence of current replication indices at the definition of $z_{jk}$ (so, $\text{im index}_j(M) = (M_{j1}, \dots, M_{jq_j})$). We define $\text{im } \rho_j(M)$ similarly.

H'3.2. For all $j \le m$, $\sigma x_j$ is a term of type $T_j$.

H'3.3. All occurrences in $Q_0$ of a variable in $S$ are either as $z_{jk}$ above or at the root of an argument of a defined test in a find process.

To make it precise which term $M$ each element refers to, we add $M$ as a subscript, writing $y_{jk,M}$ for $y_{jk}, z_{jk,M}$ for $z_{jk}, T_{jk,M}$ for $T_{jk}, x_{j,M}$ for $x_j, T_{j,M}$ for $T_j, N_M$ for $N$, and $\sigma_M$ for $\sigma$. We also define $\text{nNew}_{j,M} = m_j$, $\text{nNewSeq}_M = l$, and $\text{nInput}_M = m$.

H'4. We say that two terms $M, M' \in \mathcal{M}$ share the first $l'$ sequences of random variables when $y_{jk,M} = y_{jk,M'}$ and $z_{jk,M} = z_{jk,M'}$ for all $j \le l'$ and $k \le \text{nNew}_{j,M} = \text{nNew}_{j,M'} \ne 0$. Let $l'$ be the greatest integer such that $M$ and $M'$ share the first $l'$ sequences of random variables. Then we require:

H'4.1. The sets of variables $\{z_{jk,M} \mid j > l'\}$ and $k \le \text{nNew}_{j,M}$} and $\{z_{jk,M'} \mid j > l'\}$ and $k \le \text{nNew}_{j,M'}$} must be disjoint.

H'4.2. $\rho_j(M) = \rho_j(M')$ for all $j < l'$.
H'4.3. If $l' = nNewSeq_M$ and $N_M = N_{M'}$, then there exists $M_0$ such that we have $M = (\text{index}_{l'}(M))M_0$, $M' = (\text{index}_{l'}(M'))M_0$, and $M_0$ does not contain the current replication indices at $M$ or $M'$.

When these conditions are satisfied, there exists a context $C$ such that $Q_0 \approx_0^V C[[L]]$.

Terms in $\mathcal{M}$ must not occur in conditions of find (Hypothesis H'2) because such terms may refer to variables defined by find, and by the transformation, these variables might be moved outside their scope, thus violating Invariant 2.

In Hypothesis H'3, the sequence $BL(M)$ indicates which branch of $L$ corresponds to the term $M$.

Hypothesis H'3.2 checks that the values received as arguments in $L$ are of the proper type. Hypothesis H'3.1.1 checks that variables $z_{jk,M}$ that correspond to variables defined by $\stackrel{R}{\leftarrow}$ in $L$ are of the proper type. The variables $y_{jk}$ defined by $\stackrel{R}{\leftarrow}$ in $L$ are used only in terms $N$ in $L$. Correspondingly, Hypothesis H'3.3 checks that the corresponding variables $z_{jk,M} \in S$ are not used elsewhere in $Q_0$ and Hypothesis H'1 checks that they cannot be used directly by the context.

In $L$, for distinct $j, k$, the variables $y_{jk}$ correspond to independent random numbers. Correspondingly, Hypothesis H'3.1.2 requires that the variables $z_{jk,M}$ are created by different random choices for distinct $j, k$. In $L$, the variables $y_{jk}$ are accessed with the same indices for any $k$ (but a fixed $j$). Correspondingly, Hypothesis H'3.1.3 requires that the variables $z_{jk,M}$ are accessed with the same indices in $\text{index}_j(M)$ for any $k$. When instances of $N$ and $N'$ both refer to $y_{jk}$ with the same indices, then they also refer to $y_{j'k'}$ with the same indices when $j' \le j$. Correspondingly, if $M$ and $M'$ refer to the same $z_{jk}$, by Hypothesis H'4.1, they also refer to the same $z_{j'k'}$ for $j' \le j$. Moreover, if $\text{index}_j(M)$ and $\text{index}_j(M')$ evaluate to the same bitstrings, then $\text{index}_{j'}(M)$ and $\text{index}_{j'}(M')$ also evaluate to the same bitstrings, since $\text{index}_{j'}(M) = \text{index}_j(M) \circ \rho_{j-1}(M) \circ \dots \circ \rho_{j'}(M)$ by Hypothesis H'3.1.3 and $\rho_k(M) = \rho_k(M')$ for $k < j$ by Hypothesis H'4.2. These conditions guarantee that we can establish a correspondence from the array cells of variables of $S$ in $Q_0$ to the array cells of variables defined by $\stackrel{R}{\leftarrow}$ in $L$, and that this correspondence is an injective function, as required in Section 5.2.

Finally, a term $N$ in $L$ is evaluated at most once for each value of the indices of $y_{l_1}, \dots, y_{l_m}$, so $N$ is computed for a single value of the arguments $x_1, \dots, x_m$. Correspondingly, by Hypothesis H'4.3, when $M$ and $M'$ share the $l = nNewSeq_M$ sequences of random variables and $\text{index}_l(M)$ and $\text{index}_l(M')$ evaluate to the same bitstring, then $M$ and $M'$ evaluate to the same bitstring.

We compute the possible values of the sets $S$ and $\mathcal{M}$ by fixpoint iteration. We start with $\mathcal{M} = \emptyset$ and $S$ containing a single variable of $Q_0$ bound by a random choice. (We try all possible variables.) When a term $M$ of $Q_0$ contains a variable in $S$, we try to find an oracle in $L$ that corresponds to $M$, and if we succeed, we add $M$ to $\mathcal{M}$, and add to $S$ variables in $M$ that correspond to variables bound by random choices in $L$. (If we fail, the transformation is not possible.) We continue until a fixpoint is reached, in which case all occurrences of variables of $S$ are in terms of $\mathcal{M}$.

We now describe how we construct a process $Q'_0$ such that $Q'_0 \approx_0^V C[[R]]$.

1. We first move random choices in the right-hand side of the equivalence, so that they occur above oracle definitions instead of inside oracle bodies. As explained below, this is necessary for the correctness of the subsequent transformation of $Q_0$, when random choices appear in the corresponding part of the left-hand side. More precisely, we transform the right-hand side of the equivalence, $R$, as follows: for each $j_1, \dots, j_l$, if $\text{extract}(L, (j_1, \dots, j_l)) = (y_{11} : T_{11}, \dots, y_{1m_1} : T_{1m_1}), \dots, (y_{l1} : T_{l1}, \dots, y_{lm_l} : T_{lm_l}), O(x_1 : T_1, \dots, x_m : T_m) := \text{return}(N)$ with $m_l \ne 0$ and $\text{extract}(R, (j_1, \dots, j_l)) = (y'_{11} : T'_{11}, \dots, y'_{1m'_1} : T'_{1m'_1}), \dots, (y'_{l1} : T'_{l1}, \dots,$
$y'_{lm'_l} : T'_{lm'_l})$, $O(x_1 : T_1, \dots, x_m : T_m) := FP$, for each $z \stackrel{R}{\leftarrow} T$ in FP,

• we add $z : T$ in the sequence of random variables $y'_{l1} : T'_{l1}, \dots, y'_{lm'_l} : T'_{lm'_l}$;

• if $z$ does not occur in defined conditions of find in $R$, we remove $z \stackrel{R}{\leftarrow} T$ from FP;

• otherwise, we replace $z \stackrel{R}{\leftarrow} T$ with let $z' : T = \text{cst}$ for some constant $\text{cst}$ and add $z'[\tilde{M}]$ to each defined condition of $R$ that contains $z[\tilde{M}]$.

This transformation is needed, because in the right-hand side, a new random number must be chosen exactly for each different call to the oracle $O(x_1 : T_1, \dots, x_m : T_m) := FP$. This would not be guaranteed without that transformation, because when the left-hand side $N$ is evaluated at several occurrences with the same random numbers $y_{l1} : T_{l1}, \dots, y_{lm_l} : T_{lm_l}$ ($m_l \neq 0$), these occurrences all correspond to a single call to $O(x_1 : T_1, \dots, x_m : T_m) := \text{return } (N)$, so a single call to $O(x_1 : T_1, \dots, x_m : T_m) := FP$, but we create a copy of FP for each occurrence. After the transformation, FP contains no choice of random numbers, so we can evaluate it several times without changing the result. When $m_l = 0$, evaluations of $N$ at several occurrences can correspond to different calls to $O(x_1 : T_1, \dots, x_m : T_m) := \text{return } (N)$, so the transformation is not necessary.

2. Next, we create fresh variables corresponding to variables of the right-hand side of the equivalence. For each $M \in \mathcal{M}$, let extract$(R, BL(M)) = (y'_{11,M} : T'_{11,M}, \dots, y'_{lm'_1,M} : T'_{lm'_1,M})$, ..., $(y'_{l1,M} : T'_{l1,M}, \dots, y'_{lm'_l,M} : T'_{lm'_l,M})$, $O(x_{1,M} : T_{1,M}, \dots, x_{m,M} : T_{m,M}) := FP_M$ with $l = \text{nNewSeq}_M$, $m = \text{nInput}_M$ and we define $\text{nNew}'_{j,M} = m'_j$. We create fresh variables $z'_{jk,M} = \text{varImR}(y'_{jk,M}, M)$ for each $j \le \text{nNewSeq}_M$, $k \le \text{nNew}'_{j,M}$, and $M \in \mathcal{M}$, such that if $M$ and $M'$ share the first $l'$ sequences of random variables, then $z'_{jk,M} = z'_{jk,M'}$ for $j \le l'$ and $k \le \text{nNew}'_{j,M}$. All variables $z'_{jk,M}$ are otherwise pairwise distinct.

We also create a fresh variable $\text{varImR}(x_{j,M}, M)$ for each $j \le \text{nInput}_M$ and each $M \in \mathcal{M}$, and a fresh variable $\text{varImR}(z, M)$ for each variable $z$ defined by let or $\stackrel{R}{\leftarrow}$ in $FP_M$ and each $M \in \mathcal{M}$.

3. We update the defined conditions of finds, in order to preserve Invariant 2. More precisely, if a defined condition of a find contains $z_{j1,M}[M_1, \dots, M_{l'}]$ for some $M$, we add defined($z'_{jk',M}[M_1, \dots, M_{l'}]$) for all $k' \le \text{nNew}'_{j,M}$ to this condition. (So that accesses to $z'_{jk',M}[M_1, \dots, M_{l'}]$ created when transforming term $M$ satisfy Invariant 2, since accesses to $z_{j1,M}[M_1, \dots, M_{l'}]$ occur in $M$ and satisfy Invariant 2.)

4. We update random choices corresponding to random choices of the left-hand side of the equivalence: we either remove them or replace them with random choices corresponding to the right-hand side of the equivalence. More precisely, when $x \in S$ occurs at the root of a term $M_k$ in a condition defined($M_1, \dots, M_l$), we replace its definition $x \stackrel{R}{\leftarrow} T$; $Q$ with let $x : T = \text{cst}$ in $Q$ for some constant $\text{cst}$; when it does not occur in defined tests, we remove its definition. If $x = z_{j1,M}$ for some $M$, we add $z'_{jk,M} \stackrel{R}{\leftarrow} T'_{jk,M}$ for each $k \le \text{nNew}'_{j,M}$ where $x \stackrel{R}{\leftarrow} T$ was.

5. Finally, we transform the terms $M \in \mathcal{M}$ corresponding to oracles of the left-hand side of the equivalence into their corresponding oracle in the right-hand side. For each term $M \in \mathcal{M}$, let $l = \text{nNewSeq}_M$. We replace $M$ with $(z'_{lk,M} \stackrel{R}{\leftarrow} T'_{lk,M})$; $k \le \text{nNew}'_{l,M}$, $M'$ if $\text{nNew}_{l,M} = 0$ and $\text{nNew}'_{l,M} > 0$, and with $P'_M$ otherwise, where
- $M' = (\text{let varImR}(x_{k,M}, M) : T_{k,M} = \sigma_M x_{k,M} \text{ in})_{k \le n \text{Input}_M} \text{transf}_{\phi_0}(FP_M)$.

- $\phi_0$ is defined as follows:

$$\phi_0(x_{j,M}[i_1, \dots, i_l]) = \text{varImR}(x_{j,M}, M)[i'_1, \dots, i'_{l'}]$$

$$\phi_0(z[i_1, \dots, i_l]) = \text{varImR}(z, M)[i'_1, \dots, i'_{l'}]$$

$$\phi_0(y'_{jk,M}[i_1, \dots, i_j]) = \text{varImR}(y'_{jk,M}, M)[\text{im index}_j(M)]$$

where $i_1, \dots, i_l$ are the current replication indices at the definition of $x_{j,M}$ in $R$, $i'_1, \dots, i'_{l'}$ are the current replication indices at $M$ in $Q_0$, and $z$ is a variable defined by let or $\stackrel{R}{\leftarrow}$ in $FP_M$.

- A function $\phi$ from array accesses to array accesses is extended to terms as a substitution, by $\phi(f(M_1, \dots, M_m)) = f(\phi(M_1), \dots, \phi(M_m))$.

- $\text{transf}_{\phi}(FP)$ is defined recursively as follows:

$$\text{transf}_{\phi}(\text{return } (M')) = \phi(M')$$

$$\text{transf}_{\phi}(z \stackrel{R}{\leftarrow} T; FP') = \text{varImR}(z, M) \stackrel{R}{\leftarrow} T; \text{transf}_{\phi}(FP')$$

$$\text{transf}_{\phi}(\text{let } z : T = M' \text{ in } FP') = \text{let } \text{varImR}(z, M) : T = \phi(M') \text{ in } \text{transf}_{\phi}(FP')$$

$$\text{transf}_{\phi}(\text{find}(\bigoplus_{j=1}^{m} FB_j) \text{ else } FP') = \text{find}(\bigoplus_{j=1}^{m} \text{transf}_{\phi}(FB_j)) \text{ else } \text{transf}_{\phi}(FP')$$

and for find branches $FB$, $\text{transf}_{\phi}(FB)$ is defined as follows:

$$\text{transf}_{\phi}(\text{suchthat } M' \text{ then } FP') = \text{suchthat } \phi(M') \text{ then } \text{transf}_{\phi}(FP')$$

$$\text{transf}_{\phi}(\tilde{u} \le \tilde{n} \text{ suchthat defined}(z_k[M_{k1}, \dots, M_{kl'_k}]_{1 \le k \le l}) \land M_1 \text{ then } FP') =$$

$$\bigoplus_{M' \in \mathcal{M}'} \tilde{u}' \le \tilde{n}' \text{ suchthat defined}(\phi'(z_k[M_{k1}, \dots, M_{kl'_k}])_{1 \le k \le l}) \land \\ \text{im index}_{j_1}(M')\{\tilde{u}'/\tilde{n}'\} = \text{im index}_{j_1}(M) \land \phi'(M_1) \text{ then } \text{transf}_{\phi'}(FP')$$

where $l \ne 0$; $j_1$ is the length of the prefix of the current replication indices that occurs in $M_{k1}, \dots, M_{kl'_k}$ (by Hypothesis H7); $\mathcal{M}'$ is the set of $M' \in \mathcal{M}$ such that $\text{varImR}(z_k, M')$ is defined for $k \le l$ and $M'$ and $M$ share the first $j_1$ sequences of random variables; $\tilde{u}'$ is the sequence of current replication indices at $M'$; $\tilde{u}'$ is a sequence formed with a fresh variable for each variable in $\tilde{u}'$; $\tilde{n}'$ is the sequence of bounds of replications above $M'$; $\phi'$ is an extension of $\phi$ with $\phi'(z_k[M_{k1}, \dots, M_{kl'_k}]) = \text{varImR}(z_k, M')[\text{im index}_j(M')\{\tilde{u}'/\tilde{n}'\}]$ if $z_k = y'_{jk',M'}$ for some $k'$, and $\phi'(z_k[M_{k1}, \dots, M_{kl'_k}]) = \text{varImR}(z_k, M')[\tilde{u}']$ if $z_k$ is defined by let or by an oracle input. Optimizations for the definition of $\text{transf}_{\phi}(FB)$ are presented in Section 5.2.2.

The two essential parts of the transformation are the last two ones, numbered 4 and 5. In step 4, we add the random choices to create random variables that correspond to random variables of $R$. We create the variables $z'_{jk,M}$ at the place where $z_{j1,M}$ was created in the initial game (We could have chosen $z_{jk',M}$ for any $k'$), or when there is no $z_{j1,M}$, we have $j = n \text{NewSeq}_M$ and we create $z'_{jk,M}$ just before evaluating $M$. In step 5, we transform the term $M$ itself into the corresponding oracle process of $R$, $FP_M$. The only delicate part for evaluating $FP_M$ is the case of find: instead of looking up arrays of $R$, we look up the corresponding arrays of $Q'_0$ given by the mapping $\phi$.

This transformation may replace a simple term $M$ with a term that is not simple, since the oracle bodies in $R$ may contain random number generations, assignments and find. Therefore, it may break Property 5. Hence, by default, CryptoVerif calls **expand** (Section 5.1.3) after the **crypto** transformation, in order to recover Property 5.
### 5.2.2 Optimizations for transf<sub>φ</sub>(FB)

We can apply two optimizations to the definition of transf<sub>φ</sub>(FB):

* When im index<sub>j₁</sub>(M') is a prefix of ̃i', im index<sub>j₁</sub>(M'){̃u'/i'} is a prefix of ̃u', so the equality im index<sub>j₁</sub>(M'){̃u'/i'} = im index<sub>j₁</sub>(M) defines the value of a prefix of ̃u'. We simply substitute the fixed elements of ̃u' with their value, and remove them from the sequence of variables to be looked up by find.

* When all variables z<sub>k</sub> are y<sub>jk',M'</sub> for some j, k', and M', with max j = j<sub>0</sub>, we use the following definition instead:

$$ \text{transf}_{\phi}(\tilde{i} \le \tilde{n} \text{ suchthat defined}(z_k[M_{k1}, \dots, M_{kl'_k}]_{1 \le k \le l}) \wedge M_1 \text{ then FP}') = \\ \bigoplus_{M' \in \mathcal{M}'} \tilde{u}' \le \tilde{n}' \text{ suchthat defined}(\phi'(z_k[M_{k1}, \dots, M_{kl'_k}])_{1 \le k \le l}) \wedge \\ \text{im } (\rho_{j_0-1}(M') \circ \dots \circ \rho_{j_1}(M'))\{\tilde{u}'/\tilde{i}'\} = \text{im index}_{j_1}(M) \wedge \phi'(M_1) \text{ then transf}_{\phi'}(\text{FP}') $$

where j₁ is the length of the prefix of the current replication indices that occurs in M<sub>k1</sub>, ..., M<sub>kl'_k</sub> (by Hypothesis H7); M' is the set of M' ∈ M such that varImR(z<sub>k</sub>, M') is defined for k ≤ l and M' and M share the j₁ first sequences of random variables; ̃i' is the sequence of current replication indices at the definition of z<sub>j<sub>0</sub>k,M'</sub>; ̃u' is a sequence formed with a fresh variable for each variable in ̃i'; n' is the sequence of bounds of replications above the definition of z<sub>j<sub>0</sub>k,M'</sub>; φ' is an extension of φ with φ'(z<sub>k</sub>[M<sub>k1</sub>, ..., M<sub>kl'_k</sub>]) = varImR(z<sub>k</sub>, M')[im (ρ<sub>j<sub>0</sub>-1</sub>(M') ◦ ... ◦ ρ<sub>j<sub>1</sub></sub>(M')){̃u'/̃i'}] if z<sub>k</sub> = y<sub>jk,M'</sub>.

The composition ρ<sub>j<sub>0</sub>-1</sub>(M') ◦ ... ◦ ρ<sub>j<sub>1</sub></sub>(M') computes the indices of z'<sub>jk',M'</sub> for any k' from the indices of z'<sub>j<sub>0</sub>k'',M'</sub> for any k''.

When several terms M' ∈ M share the first j<sub>0</sub> sequences of random variables, they generate the same φ', so only one find branch needs to be added for all of them, which can reduce considerably the number of find branches to add.

An optimization similar to the first one above also applies to this case, when im (ρ<sub>j<sub>0</sub>-1</sub>(M') ◦ ... ◦ ρ<sub>j<sub>1</sub></sub>(M')) is a prefix of ̃i'.

### 5.2.3 Guiding the Application of Equivalences

We introduce a small extension to the equivalences G<sub>1</sub> | ... | G<sub>m</sub> ≈ G'<sub>1</sub> | ... | G'<sub>m</sub> described in Section 5.2. These equivalences become G<sub>1</sub> mode<sub>1</sub> | ... | G<sub>m</sub> mode<sub>m</sub> ≈ G'<sub>1</sub> | ... | G'<sub>m</sub>, where mode<sub>j</sub> is either empty or [all]. The mode [all] is an indication for the prover, to guide the application of the equivalence without changing its semantics. When mode<sub>j</sub> = [all], M must contain all occurrences in the initial game Q of the root function symbols of terms M inside G<sub>j</sub>. When mode<sub>j</sub> is empty, at least one variable defined by R<sub>←</sub> in G<sub>j</sub> must correspond to a variable in S.

The following hypotheses guarantee the good usage of modes:

H8. At most one mode<sub>j</sub> can be empty. (Otherwise, when several sets of random variables can be chosen for each G<sub>j</sub>, there are many possible combinations for applying the transformation.)

H9. If G<sub>j</sub> is of the form **foreach** i ≤ n **do** O(x<sub>1</sub> : T<sub>1</sub>, ..., x<sub>l</sub> : T<sub>l</sub>) := FP without any random choice, then mode<sub>j</sub> = [all]. (A random choice is needed in the definition of empty mode.)
An equivalence can be declared [manual]. In this case, this equivalence is not applied by the automatic proof strategy. It can be used only by manual proof indications. This is useful, for instance, if applying the equivalence would yield an infinite loop.

Each oracle in the left-hand side can also be labeled with an integer $[n]$, which represents a priority: CryptoVerif preferably uses oracles labeled with a lower integer. (The absence of label corresponds to the label [0].) Each oracle in the left-hand side can finally be labeled with [useful_change]. This indication is also used for the proof strategy: if at least one [useful_change] indication is present, CryptoVerif applies the transformation defined by the equivalence only when at least one [useful_change] oracle is called in the game.

### 5.2.4 Relaxing Hypothesis H6

Hypothesis H6 requires that for all random choices $y \stackrel{R}{\leftarrow} T$ that occur above a term $N$ in the left-hand side of an equivalence, $y$ occurs in $N$. We can relax this hypothesis, by allowing that some random variables $y$ do not occur in $N$, provided that the missing variables can be determined using Hypothesis H'4.1: when some term $M$ shares some variable $y$ in the $l'$-th sequence of random variables with some other term $M'$, we know that it must also share with $M'$ all random variables in sequences above and including the $l'$-th sequence; so, knowing the random variables associated to $M'$, we can determine some of those associated to $M$. The transformation simply fails when the algorithm described above cannot fully determine the random variables associated to some term $M$.

With this extension, we additionally need to make sure that, when an expression of the right-hand side uses a variable $y$ defined by a random choice, this variable will be defined in the transformed game before the expression is evaluated. To do that, we establish a correspondence between the random choices before the transformation and the random choices after, such that, as far as possible, if a variable is used in a transformed expression, the corresponding variable before transformation is also used in the initial expression. For variables that appear in a transformed expression but are not used in the initial expression, we check when performing the game transformation that they will correctly be defined. If they are not correctly defined, the transformation fails.

### 5.2.5 Relaxing Hypothesis H'2

Hypothesis H'2 requires that no term $N$ transformed by the equivalence occurs in the condition part of a find ($\text{defined}(M_1, \dots, M_l) \wedge M$). We can relax this hypothesis by allowing $N$ to occur in $M$ (but not in the defined test), provided

* the variables $\tilde{u}$ bound by this find do not occur in the following terms in the transformed expression of $N$:

- $N'$ in processes of the form $\text{let } x : T = N'$ in ...;

- $N'_{jk}$ and $N'_{j}$ in processes of the form find ($\bigoplus_{j=1}^m u_{j1}[\tilde{i}] \le n_{j1}, \dots, u_{jm_j}[\tilde{i}] \le n_{jm_j}$ such that $\text{defined}(N'_{j1}, \dots, N'_{j_l}) \wedge N'_{j}$ then ...) else ...

(If the variables $\tilde{u}$ bound by find occurred in such terms, the transformation would move them outside the scope of their definition.)

* if $N$ depends on the variables $\tilde{u}$ bound by this find, then the corresponding left-hand side of the equivalence $N'$ is under a replication `foreach i \le n do` with no random choice in $L$. (Otherwise, $L$ contains $y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l; (\dots | O(x_1 : T'_1, \dots, x_{l'} : T'_{l'}) := \text{return } (N')|$
...) and $L$ allows a single evaluation of $N'$ for each execution of the random choices $y_1 \stackrel{R}{\leftarrow} T_1; \dots; y_l \stackrel{R}{\leftarrow} T_l$, while the term $N$ is evaluated several times, once for each value of $\tilde{u}$, so the transformation is impossible. In other words, the variables $\tilde{u}$ must be considered as replication indices in this transformation.)

### 5.2.6 Soundness and Example

The following proposition shows the soundness of the transformation.

**Proposition 6** Let $Q_0$ be a process that satisfies Invariants 1, 2, and 8 and $Q'_0$ the process obtained from $Q_0$ by the above transformation. Then $Q'_0$ satisfies Invariants 1, 2, and 8 and, if $[[L]] \approx [[R]]$ for all polynomials $\max_{\eta}(c_{j_0, \dots, j_l})$ and $n$ where $n$ is any replication bound of $L$ or $R$, then $Q_0 \approx^{V} Q'_0$.

**Example 10** In order to treat Example 1, the prover is given as input the indication that $T_{mk}$, $T_k$, and $T_r$ are fixed-length types; the type declarations for the functions mac, $mac' : bitstring \times T_{mk} \to T_{ms}$, verify, $verify' : bitstring \times T_{mk} \times T_{ms} \to bool$, enc, $enc' : bitstring \times T_k \times T_r \to T_e$, dec : $T_e \times T_k \to bitstring_\perp$, k2b : $T_k \to bitstring$, $i_\perp : bitstring \to bitstring_\perp$, $Z : bitstring \to bitstring$, and the constant $Z_k : bitstring$; the equations (mac), ($mac'$), (enc), and $\forall x : T_k, Z(k2b(x)) = Z_k$ (which expresses that all keys have the same length); the indication that k2b and $i_\perp$ are poly-injective (which generates the equations (k2b) and similar equations for $i_\perp$); equivalences $L \approx R$ for MAC ($mac_{eq}$) and encryption ($enc_{eq}$); and the process $Q_0$ of Example 1.

The process $Q_0$ of Example 1 can be transformed using the security of the MAC. Let $S = \{x_{mk}\}$, $M_1 = \text{mac}(x_m[i], x_{mk})$, $M_2 = \text{verify}(x'_m[i'], x_{mk}, x_{ma}[i'])$, and $\mathcal{M} = \{M_1, M_2\}$. We have $N_{M_1} = \text{mac}(x[i'', i], k[i''])$, $N_{M_2} = \text{verify}(m[i'', i'], k[i''], ma[i'', i'])$, $\text{mapId}_{M_1}(a_1) = (1, a_1)$, and $\text{mapId}_{M_2}(a_2) = (1, a_2)$, so $x_m[a_1]$ corresponds to $x[1, a_1]$, $x_{mk}$ to $k[1]$, $x'_m[a_2]$ to $m[1, a_2]$, and $x_{ma}[a_2]$ to $ma[1, a_2]$.

After transformation, we get the following process $Q'_0$:

```
Q'_0 = Start() := x_k \stackrel{R}{\leftarrow} T_k; x_{mk} \stackrel{R}{\leftarrow} T_{mk}; \text{return } (); (Q'_A | Q'_B)

Q'_A = \text{foreach } i \le n \text{ do } O_A[i]() := x'_k \stackrel{R}{\leftarrow} T_k; x_r \stackrel{R}{\leftarrow} T_r;

\quad \text{let } x_m : \text{bitstring} = \text{enc}(\text{k2b}(x'_k), x_k, x_r) \text{ in}
\quad \text{return } (x_m, \text{mac}'(x_m, x_{mk}))

Q'_B = \text{foreach } i' \le n \text{ do } O_B[i'](x'_m, x_{ma}) :=

\quad \text{find } u \le n \text{ suchthat } \text{defined}(x_m[u]) \land x'_m = x_m[u] \land \text{verify}'(x'_m, x_{mk}, x_{ma}) \text{ then}
\quad \text{ if true then let } i_\perp(\text{k2b}(x''_k)) = \text{dec}(x'_m, x_k) \text{ in return } ()
\quad \text{ else }
\quad \text{ if false then let } i_\perp(\text{k2b}(x''_k)) = \text{dec}(x'_m, x_k) \text{ in return } ()

```

The initial definition of $x_{mr}$ is removed and replaced with a new definition, which we still call $x_{mr}$. The term $\text{mac}(x_m, x_{mk})$ is replaced with $\text{mac}'(x_m, x_{mk})$. The term $\text{verify}(x'_m, x_{mk}, x_{ma})$ becomes $\text{find } u \le n \text{ suchthat } \text{defined}(x_m[u]) \land x'_m = x_m[u] \land \text{verify}'(x'_m, x_{mk}, x_{ma}) \text{ then true else}$
false, which yields $Q'_B$ after the call to **expand**, which transforms the find term into a process. The process looks up the message $x'_m$ in the array $x_m$, which contains the messages whose MAC has been computed with key $x_{mk}$. If the MAC of $x'_m$ has never been computed, the check always fails (it returns false) by the definition of security of the MAC. Otherwise, it returns true when verify'(x'_m, x_{mk}, x_{ma}).

After applying **simplify**, $Q'_A$ is unchanged and $Q'_B$ becomes

$$ 
\begin{aligned}
Q''_B &= \text{foreach } i' \le n \text{ do } O_B[i'](x'_m, x_{ma}) := \\
&\quad \text{find } u \le n \text{ suchthat } \text{defined}(x_m[u], x'_k[u]) \land x'_m = x_m[u] \land \text{verify}'(x'_m, x_{mk}, x_{ma}) \text{ then} \\
&\quad \text{let } x''_k : T_k = x'_k[u] \text{ in return ()}
\end{aligned}
$$

First, the tests if true **then** ... and if false **then** ... are simplified. The term $\text{dec}(x'_m, x_k)$ is simplified knowing $x'_m = x_m[u]$ by the find condition, $x_m[u] = \text{enc}(\text{k2b}(x'_k[u]), x_k, x_r[u])$ by the assignment that defines $x_m$, and $\text{dec}(\text{enc}(m, k, r), k) = i_\perp(m)$ by (enc). So we have $\text{dec}(x'_m, x_k) = i_\perp(\text{k2b}(x'_k[u]))$. By injectivity of $i_\perp$ and k2b, the assignment to $x''_k$ simply becomes $x''_k = x'_k[u]$, using the equations $\forall x : \text{bitstring}, i_\perp^{-1}(i_\perp(x)) = x$ and $\forall x : T_k, \text{k2b}^{-1}(\text{k2b}(x)) = x$.

Then we apply the security of encryption: $\text{enc}(\text{k2b}(x'_k), x_k, x_r)$ becomes $\text{enc}'(\text{Z}(\text{k2b}(x'_k)), x_k, x_r)$. After **simplify**, it becomes $\text{enc}'(\text{Z}_k, x_k, x_r)$, using $\forall x : T_k, \text{Z}(\text{k2b}(x)) = Z_k$ (which expresses that all keys have the same length).

So we obtain the following game:

$$ 
\begin{aligned}
Q_0'' = \text{Start}() &:= x_k \stackrel{R}{\leftarrow} T_k; x_{mk} \stackrel{R}{\leftarrow} T_{mk}; \text{return } (); (Q_A'' | Q_B'') \\
Q_A'' = \text{foreach } i \le n \text{ do } O_A[i]() &:= x'_k \stackrel{R}{\leftarrow} T_k; x_r \stackrel{R}{\leftarrow} T_r; \\
\text{let } x_m : \text{bitstring} &:= \text{enc}'(\text{Z}_k, x_k, x_r) \text{ in} \\
\text{return } (x_m, \text{mac}'(x_m, x_{mk}))
\end{aligned}
$$

where $Q''_B$ remains as above.

# 6 Proof Strategy

**Extension:** This description is based on the initial proof strategy. Additional advice has been added since then.

Up to now, we have described the available game transformations. Next, we explain how we organize these transformations in order to prove protocols.

At the beginning of the proof and after each successful cryptographic transformation (that is, a transformation of Section 5.2), the prover executes **simplify** and tests whether the desired security properties are proved, as described in Section 4. If so, it stops.

In order to perform the cryptographic transformations and the other syntactic transformations, our proof strategy relies of the idea of advice. Precisely, the prover tries to execute each available cryptographic transformation in turn. When such a cryptographic transformation fails, it returns some syntactic transformations that could make the desired transformation work. (These are the advised transformations.) Then the prover tries to perform these syntactic transformations. If they fail, they may also suggest other advised transformations, which are then executed. When the syntactic transformations finally succeed, we retry the desired cryptographic transformation, which may succeed or fail, perhaps with new advised transformations, and so on.

The prover determines the advised transformations as follows:
* Assume that we try to execute a cryptographic transformation, and need to recognize a certain term $M$ of $L$, but we find in $Q_0$ only part of $M$, the other parts being variable accesses $x[...]$ while we expect function applications. In this case, we advise **remove_assign binder $x$**. For example, if $Q_0$ contains $\text{sign}(M', x_{sk}, x_r)$ and we look for $\text{sign}(x_m, \text{skgen}(x_{rk}), x_r)$, we advise **remove_assign binder $x_{sk}$**. (The transformation of Example 8 is advised for this reason.)

* When we try to execute **remove_assign binder $x$**, $x$ has several definitions, and there are accesses to variable $x$ guarded by find in $Q_0$, we advise **SArename $x$**.

* When we check whether $x$ is secret or one-session secret, we have an assignment $\text{let } x[\tilde{i}] : T = y[\tilde{M}] \text{ in } P$, and there is at least one assignment defining $y$, we advise **remove_assign binder $y$**.

When we check whether $x$ is secret or one-session secret, we have an assignment $\text{let } x[\tilde{i}] : T = y[\tilde{M}] \text{ in } P$, $y$ is defined by random choices, $y$ has several definitions, and some variable accesses to $y$ are not of the form $\text{let } y'[\tilde{i}'] : T = y[\tilde{M}'] \text{ in } P'$, we advise **SArename $y$**.

# 7 Conclusion

The tool CryptoVerif produces proofs by sequences of games like those manually written by cryptographers. It generates the games, using an automatic proof strategy or guidance from the user, who specifies the transformations to perform. It supports a wide variety of cryptographic primitives specified by indistinguishability axioms. Many of these primitives are included in a library so that the user does not have to redefine them. It can prove secrecy, correspondence, and indistinguishability properties. It has been applied to substantial case studies, including Signal [52], TLS 1.3 [23], and WireGuard [58].

CryptoVerif still has limitations. In particular, the size of games tends to grow too fast, which limits its ability to deal with large examples, especially because some game transformations require the game to be expanded first by the **expand** transformation, which duplicates the code from each test until the end of protocol. Planed improvements include allowing more game transformations to work without previous application of **expand**; allowing internal oracle calls in games, in order to share code between different parts of the game; using composition results in order to make proofs more modular. Moreover, some game transformations could be generalized. For instance, the transformation **merge Fet branches** merges branches of a test when they execute the same code; the detection that several branches execute equivalent code could be made more flexible, by allowing reorderings of instructions for instance. CryptoVerif only considers blackbox adversaries: it does not support proofs that manipulate the code of the adversary, such as the forking lemma [65].

**Acknowledgments** We warmly thank David Pointcheval for his advice and explanations of the computational proofs of protocols. This project would not have been possible without him. We also thank Jacques Stern for initiating this work. The design and implementation of CryptoVerif was partly done while Bruno Blanchet was at CNRS and at Ecole Normale Supérieure. This work was partly supported by the French National Research Agency (ANR) under the projects FormaCrypt (ARA SSIA 2005), ProSe (VERSO 2010, decision number 2010-VERS-004), TECAP (decision number ANR-17-CE39-0004-03) and received funding from the France 2030 program managed by the ANR under the references ANR-22-PECY-0006 (PEPR Cybersecurity SVP) and ANR-22-PETQ-0008 (PEPR Quantic PQ-TLS).
References

[1] M. Abadi, B. Blanchet, and C. Fournet. The applied pi calculus: Mobile values, new names, and secure communication. *Journal of the ACM*, 65(1):1–1–1:41, Oct. 2017.

[2] M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In *28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'01)*, pages 104–115, New York, NY, Jan. 2001. ACM Press.

[3] M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). *Journal of Cryptology*, 15(2):103–127, 2002.

[4] M. Abdalla, P.-A. Fouque, and D. Pointcheval. Password-based authenticated key exchange in the three-party setting. *IEE Proceedings Information Security*, 153(1):27–39, Mar. 2006.

[5] R. Affeldt, D. Nowak, and K. Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In *9th International Workshop on Automated Verification of Critical Systems (AVoCS'09)*, volume 23 of *Electronic Communications of the EASST*. EASST, Sept. 2009.

[6] J. B. Almeida, M. Barbosa, G. Barthe, M. Campagna, E. Cohen, B. Grégoire, V. Pereira, B. Portela, P.-Y. Strub, and S. Tasiran. A machine-checked proof of security for AWS key management service. In *ACM SIGSAC Conference on Computer and Communications Security (CCS'19)*, pages 63–78, New York, NY, Nov. 2019. ACM Press.

[7] M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In *ACM Conference on Computer and Communications Security (CCS'09)*, pages 66–78, New York, NY, Nov. 2009. ACM Press.

[8] M. Backes and P. Laud. Computationally sound secrecy proofs by mechanized flow analysis. In *13th ACM Conference on Computer and Communications Security (CCS'06)*, pages 370–379, New York, NY, Nov. 2006. ACM Press.

[9] M. Backes and B. Pfitzmann. Symmetric encryption in a simulatable Dolev-Yao style cryptographic library. In *17th IEEE Computer Security Foundations Workshop*, pages 204–218, Los Alamitos, CA, June 2004. IEEE Computer Society Press.

[10] M. Backes, B. Pfitzmann, and M. Waidner. A composable cryptographic library with nested operations. In *10th ACM conference on Computer and communication security (CCS'03)*, pages 220–230, New York, NY, Oct. 2003. ACM Press.

[11] D. Baelde, S. Delaune, A. Koutsos, C. Jacomme, and S. Moreau. An interactive prover for protocol verification in the computational model. In *42nd IEEE Symposium on Security and Privacy (S&P'21)*, pages 537–554, Los Alamitos, CA, May 2021. IEEE Computer Society Press.

[12] G. Barthe, J. M. Crespo, Y. Lakhnech, and B. Schmidt. Mind the gap: Modular machine-checked proofs of one-round key exchange protocols. In E. Oswald and M. Fischlin, editors, *Advances in Cryptology – EUROCRYPT 2015*, volume 9057 of *Lecture Notes in Computer Science*, pages 689–718, Berlin, Heidelberg, Apr. 2015. Springer.

[13] G. Barthe, M. Daubignard, B. Kapron, and Y. Lakhnech. Computational indistinguishability logic. In *17th ACM Conference on Computer and Communications Security (CCS'10)*, pages 375–386, New York, NY, Oct. 2010. ACM Press.
[14] G. Barthe, B. Grégoire, S. Z. Béguelin, and Y. Lakhnech. Beyond provable security. Verifiable IND-CCA security of OAEP. In A. Kiayias, editor, *Topics in Cryptology - CT-RSA 2011*, volume 6558 of *Lecture Notes in Computer Science*, pages 180–196, Berlin, Heidelberg, Feb. 2011. Springer.

[15] G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt. In P. Degano, J. Guttman, and F. Martinelli, editors, *5th International Workshop on Formal Aspects in Security and Trust, FAST 2008*, volume 5491 of *Lecture Notes in Computer Science*, pages 1–19, Berlin, Heidelberg, 2009. Springer.

[16] G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin. Computer-aided security proofs for the working cryptographer. In P. Rogaway, editor, *Advances in Cryptology - CRYPTO 2011*, volume 6841 of *Lecture Notes in Computer Science*, pages 71–90, Berlin, Heidelberg, Aug. 2011. Springer.

[17] G. Barthe, B. Grégoire, and S. Zanella. Formal certification of code-based cryptographic proofs. In *36th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'09)*, pages 90–101, New York, NY, Jan. 2009. ACM Press.

[18] D. Basin, A. Lochbihler, and S. R. Sefidgar. CryptHOL: Game-based proofs in higher-order logic. *Journal of Cryptology*, 33:494–566, 2020.

[19] S. Z. Béguelin, G. Barthe, S. Heraud, B. Grégoire, and D. Hedin. A machine-checked formalization of sigma-protocols. In *23rd Computer Security Foundations Symposium (CSF'10)*, pages 246–260, Los Alamitos, CA, July 2010. IEEE Computer Society Press.

[20] S. Z. Béguelin, B. Grégoire, G. Barthe, and F. Olmedo. Formally certifying the security of digital signature schemes. In *30th IEEE Symposium on Security and Privacy, S&P 2009*, pages 237–250, Los Alamitos, CA, May 2009. IEEE Computer Society Press.

[21] M. Bellare and C. Namprempre. Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In T. Okamoto, editor, *Advances in Cryptology – ASIACRYPT'00*, volume 1976 of *Lecture Notes in Computer Science*, pages 531–545, Berlin, Heidelberg, Dec. 2000. Springer.

[22] M. Bellare and P. Rogaway. The security of triple encryption and a framework for code-based game-playing proofs. In S. Vaudenay, editor, *Advances in Cryptology – Eurocrypt 2006 Proceedings*, volume 4004 of *Lecture Notes in Computer Science*, pages 409–426, Berlin, Heidelberg, May 2006. Springer. Extended version available at http://eprint.iacr.org/2004/331.

[23] K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In *IEEE Symposium on Security and Privacy (S&P'17)*, pages 483–503, Los Alamitos, CA, May 2017. IEEE Computer Society Press.

[24] B. Blanchet. Automatic proof of strong secrecy for security protocols. In *IEEE Symposium on Security and Privacy*, pages 86–100, May 2004.

[25] B. Blanchet. Computationally sound mechanized proofs of correspondence assertions. In *20th IEEE Computer Security Foundations Symposium (CSF'07)*, pages 97–111, Los Alamitos, CA, July 2007. IEEE Computer Society Press. Extended version available as ePrint Report 2007/128, http://eprint.iacr.org/2007/128.
[26] B. Blanchet. A computationally sound mechanized prover for security protocols. *IEEE Transactions on Dependable and Secure Computing*, 5(4):193-207, Oct.-Dec. 2008.

[27] B. Blanchet. Automatically verified mechanized proof of one-encryption key exchange. Cryptology ePrint Archive, Report 2012/173, Apr. 2012. Available at http://eprint.iacr.org/2012/173.

[28] B. Blanchet. Modeling and verifying security protocols with the applied pi calculus and ProVerif. *Foundations and Trends in Privacy and Security*, 1(1-2):1-135, Oct. 2016.

[29] B. Blanchet. Cryptoverif: a computationally-sound security protocol verifier (initial version with communication on channels). Research report RR-9525, Inria, Oct. 2023. Available at https://inria.hal.science/hal-04246199.

[30] B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. *Journal of Logic and Algebraic Programming*, 75(1):3-51, Feb.-Mar. 2008.

[31] I. Boureanu, C. C. Drăgan, F. Dupressoir, D. Gérault, and P. Lafourcade. Mechanised models and proofs for distance-bounding. In *34th IEEE Computer Security Foundations Symposium (CSF'21)*, Los Alamitos, CA, 2021. IEEE Computer Society Press.

[32] D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In *7th International Conference on Availability, Reliability and Security (ARES 2012)*, pages 65-74, Los Alamitos, CA, Aug. 2012. IEEE Computer Society Press.

[33] D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations and application to SSH. *Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)*, 4(1):4-31, Mar. 2013.

[34] R. Canetti. Universally composable security: A new paradigm for cryptographic protocols. In *42nd Symposium on Foundations of Computer Science (FOCS)*, pages 136-145, Los Alamitos, CA, Oct. 2001. IEEE Computer Society Press. An updated version is available at Cryptology ePrint Archive, http://eprint.iacr.org/2000/067.

[35] R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Linch, O. Pereira, and R. Segala. Time-bounded task-PIOAs: A framework for analyzing security protocols. In S. Dolev, editor, *20th Symposium on Distributed Computing (DISC)*, volume 4167 of *Lecture Notes in Computer Science*, pages 238-253, Berlin, Heidelberg, Sept. 2006. Springer.

[36] R. Canetti and J. Herzog. Universally composable symbolic analysis of cryptographic protocols (the case of encryption-based mutual authentication and key exchange). Cryptology ePrint Archive, Report 2004/334, 2004. Available at http://eprint.iacr.org/2004/334.

[37] H. Comon-Lundh and V. Cortier. Computational soundness of observational equivalence. In *15th ACM conference on Computer and communications security (CCS'08)*, pages 109-118, New York, NY, Oct. 2008. ACM Press.

[38] V. Cortier, C. C. Drăgan, F. Dupressoir, B. Schmidt, P.-Y. Strub, and B. Warinschi. Machine-checked proofs of privacy for electronic voting protocols. In *IEEE Symposium on Security and Privacy (SP'17)*, pages 993-1008, Los Alamitos, CA, 2017. IEEE Computer Society Press.
[39] V. Cortier, H. Hördegen, and B. Warinschi. Explicit randomness is not necessary when modeling probabilistic encryption. In C. Dima, M. Minea, and F. Tiplea, editors, *Workshop on Information and Computer Security (ICS 2006)*, volume 186 of *Electronic Notes in Theoretical Computer Science*, pages 49–65. Elsevier, Sept. 2006.

[40] V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. *Journal of Automated Reasoning*, 46(3-4):225–259, Apr. 2011.

[41] V. Cortier and B. Warinschi. Computationally sound, automated proofs for security protocols. In M. Sagiv, editor, *Proc. 14th European Symposium on Programming (ESOP'05)*, volume 3444 of *Lecture Notes in Computer Science*, pages 157–171, Berlin, Heidelberg, Apr. 2005. Springer.

[42] V. Cortier and B. Warinschi. A composable computational soundness notion. In *18th ACM Conference on Computer and Communications Security (CCS'11)*, pages 63–74, New York, NY, Oct. 2011. ACM Press.

[43] J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Towards automated proofs for asymmetric encryption schemes in the random oracle model. In *15th ACM conference on Computer and communications security (CCS'08)*, pages 371–380, New York, NY, Oct. 2008. ACM Press.

[44] J. Courant, M. Daubignard, C. Ene, P. Lafourcade, and Y. Lakhnech. Automated proofs for asymmetric encryption. In D. Dams, U. Hannemann, and M. Steffen, editors, *Concurrency, Compositionality, and Correctness*, volume 5930 of *Lecture Notes in Computer Science*, pages 300–321, Berlin, Heidelberg, 2010. Springer.

[45] J. Courant, C. Ene, and Y. Lakhnech. Computationally sound typing for non-interference: The case of deterministic encryption. In V. Arvind and S. Prasad, editors, *27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07)*, volume 4855 of *Lecture Notes in Computer Science*, pages 364–375, Berlin, Heidelberg, Dec. 2007. Springer.

[46] A. Datta, A. Derek, J. C. Mitchell, V. Shmatikov, and M. Turuani. Probabilistic polynomial-time semantics for a protocol security logic. In L. Caires and L. Monteiro, editors, *ICALP 2005: the 32nd International Colloquium on Automata, Languages and Programming*, volume 3580 of *Lecture Notes in Computer Science*, pages 16–29, Berlin, Heidelberg, July 2005. Springer.

[47] A. Datta, A. Derek, J. C. Mitchell, and B. Warinschi. Computationally sound compositional logic for key exchange protocols. In *19th IEEE Computer Security Foundations Workshop (CSFW'06)*, pages 321–334, Los Alamitos, CA, July 2006. IEEE Computer Society Press.

[48] J. Gancher, S. Gibson, P. Singh, S. Dharanikota, and B. Parno. OWL: Compositional verification of security protocols via an information-flow type system. In *2023 IEEE Symposium on Security and Privacy (S&P)*, pages 1114–1131, Los Alamitos, CA, May 2023. IEEE Computer Society Press.

[49] S. Goldwasser, S. Micali, and R. Rivest. A digital signature scheme secure against adaptive chosen-message attacks. *SIAM Journal of Computing*, 17(2):281–308, Apr. 1988.
[50] R. Janvier, Y. Lakhnech, and L. Mazaré. Completing the picture: Soundness of formal encryption in the presence of active adversaries. In M. Sagiv, editor, *Proc. 14th European Symposium on Programming (ESOP'05)*, volume 3444 of *Lecture Notes in Computer Science*, pages 172–185, Berlin, Heidelberg, Apr. 2005. Springer.

[51] D. E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, *Computational Problems in Abstract Algebra*, pages 263–297. Pergamon Press, Oxford, UK, 1970.

[52] N. Kobeissi, K. Bhargavan, and B. Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In *2nd IEEE European Symposium on Security and Privacy (EuroS&P'17)*, pages 435–450, Los Alamitos, CA, Apr. 2017. IEEE Computer Society Press.

[53] P. Laud. Handling encryption in an analysis for secure information flow. In P. Degano, editor, *Programming Languages and Systems, 12th European Symposium on Programming, ESOP'03*, volume 2618 of *Lecture Notes in Computer Science*, pages 159–173, Berlin, Heidelberg, Apr. 2003. Springer.

[54] P. Laud. Symmetric encryption in automatic analyses for confidentiality against active adversaries. In *IEEE Symposium on Security and Privacy*, pages 71–85, May 2004.

[55] P. Laud. Secrecy types for a simulatable cryptographic library. In *12th ACM Conference on Computer and Communications Security (CCS'05)*, pages 26–35, New York, NY, Nov. 2005. ACM Press.

[56] P. Laud and I. Tšahhirov. A user interface for a game-based protocol verification tool. In P. Degano and J. Guttman, editors, *6th International Workshop on Formal Aspects in Security and Trust (FAST2009)*, volume 5983 of *Lecture Notes in Computer Science*, pages 263–278, Berlin, Heidelberg, Nov. 2009. Springer.

[57] P. Laud and V. Vene. A type system for computationally secure information flow. In M. Liškiewicz and R. Reischuk, editors, *15th International Symposium on Fundamentals of Computation Theory (FCT'05)*, volume 3623 of *Lecture Notes in Computer Science*, pages 365–377, Berlin, Heidelberg, Aug. 2005. Springer.

[58] B. Lipp, B. Blanchet, and K. Bhargavan. A mechanised cryptographic proof of the Wire-Guard virtual private network protocol. In *IEEE European Symposium on Security and Privacy (EuroS&P'19)*, pages 231–246, Stockholm, Sweden, June 2019. IEEE Computer Society.

[59] J. C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time calculus for the analysis of cryptographic protocols. *Theoretical Computer Science*, 353(1–3):118–164, Mar. 2006.

[60] D. Nowak. A framework for game-based security proofs. In S. Qing, H. Imai, and G. Wang, editors, *Information and Communications Security, 9th International Conference, ICICS 2007*, volume 4861 of *Lecture Notes in Computer Science*, pages 319–333, Berlin, Heidelberg, Dec. 2007. Springer.

[61] D. Nowak. On formal verification of arithmetic-based cryptographic primitives. In P. J. Lee and J. H. Cheon, editors, *Information Security and Cryptology - ICISC 2008, 11th International Conference*, volume 5461 of *Lecture Notes in Computer Science*, pages 368–382, Berlin, Heidelberg, Dec. 2008. Springer.
[62] D. Nowak and Y. Zhang. A calculus for game-based security proofs. In *Provable Security, Fourth International Conference, ProvSec 2010*, volume 6402 of *Lecture Notes in Computer Science*, pages 35–52, Berlin, Heidelberg, Oct. 2010. Springer.

[63] T. Okamoto and D. Pointcheval. The gap-problems: a new class of problems for the security of cryptographic schemes. In K. Kim, editor, *International Workshop on Practice and Theory in Public Key Cryptography (PKC'2001)*, volume 1992 of *Lecture Notes in Computer Science*, pages 104–118, Berlin, Heidelberg, Feb. 2001. Springer.

[64] A. Petcher and G. Morrisett. The foundational cryptography framework. In R. Focardi and A. C. Myers, editors, *4th International Conference on Principles of Security and Trust (POST'15)*, volume 9036 of *Lecture Notes in Computer Science*, pages 53–72, Berlin, Heidelberg, Apr. 2015. Springer.

[65] D. Pointcheval and J. Stern. Security proofs for signature schemes. In U. Maurer, editor, *Advances in Cryptology — EUROCRYPT '96*, volume 1070 of *Lecture Notes in Computer Science*, pages 387–398, Berlin, Heidelberg, May 1996. Springer.

[66] V. Shoup. A proposal for an ISO standard for public-key encryption, Dec. 2001. ISO/IEC JTC 1/SC27.

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

[68] V. Shoup. Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332, Nov. 2004. Available at http://eprint.iacr.org/2004/332.

[69] G. Smith and R. Alpízar. Secure information flow with random assignment and encryption. In *4th ACM Workshop on Formal Methods in Security Engineering (FMSE'06)*, pages 33–43, Nov. 2006.

[70] C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, and M. Waidner. Cryptographically sound theorem proving. In *19th IEEE Computer Security Foundations Workshop (CSFW-19)*, pages 153–166, Los Alamitos, CA, July 2006. IEEE Computer Society Press.

[71] C. Sprenger and D. Basin. Cryptographically-sound protocol-model abstractions. In *23rd Annual IEEE Symposium on Logic in Computer Science*, pages 3–17, Los Alamitos, CA, June 2008. IEEE Computer Society Press.

[72] I. Tšahhirov and P. Laud. Application of dependency graphs to security protocol analysis. In G. Barthe and C. Fournet, editors, *3rd Symposium on Trustworthy Global Computing (TGC'07)*, volume 4912 of *Lecture Notes in Computer Science*, pages 294–311, Berlin, Heidelberg, Nov. 2007. Springer.

[73] T. Y. C. Woo and S. S. Lam. Authentication for distributed systems. In D. Denning and P. Denning, editors, *Internet Besieged: Countering Cyberspace Scofflaws*, pages 319–355. ACM Press and Addison-Wesley, Oct. 1997.
Inria

RESEARCH CENTRE
PARIS

2 rue Simone Iff - CS 42112
75589 Paris Cedex 12

Publisher
Inria
Domaine de Voluceau - Rocquencourt
BP 105 - 78153 Le Chesnay Cedex
inria.fr

ISSN 0249-6399