event $e_A$ being executed; that is why event $e_B$ is executed only when $B$ runs a session with $A$.

By the unforgeability of signatures, the signature verification with $pk_A$ succeeds only for signatures generated with $sk_A$. So, when we verify that the signature is correct, we can furthermore check that it has been generated using $sk_A$. So, after game transformations explained below, we obtain the following final game:

$G_1 = c_0()$; new $rk_A : keyseed$;
let $pk_A = pkgen'(rk_A)$ in $\overline{c_1}[pk_A] : (Q_{1A} | Q_{1B})$
$Q_{1A} = !^{i_A \le n} c_2[i_A](x_N : nonce, x_B : host)$;
event $e_A(pk_A, x_B, x_N)$;
let $m = concat(pk_A, x_B, x_N)$ in
new $r : seed$; $\overline{c_3[i_A]}[\text{sign}'(m, skgen'(rk_A), r)]$
$Q_{1B} = !^{i_B \le n} c_4[i_B](x_{pk_A} : pkey)$; new $N : nonce$;
$\overline{c_5[i_B]}[N, B]$; $c_6[i_B](s : \text{signature})$;
find $u \le n$ such that $\text{defined}(m[u], x_B[u], x_N[u])$
$\wedge (x_{pk_A} = pk_A) \wedge (B = x_B[u]) \wedge (N = x_N[u])$
$\wedge \text{verify}'(concat(x_{pk_A}, B, N), x_{pk_A}, s)$ then
event $e_B(x_{pk_A}, B, N)$)

The assignment $sk_A = skgen(rk_A)$ has been removed and $skgen(rk_A)$ has been substituted for $sk_A$, in order to make the term $\text{sign}(m, skgen(rk_A), r)$ appear. This term is needed for the security of the signature scheme to apply.

In $Q_{1A}$, the signed message is stored in variable $m$, and this variable is used when computing the signature.

Finally, using the unforgeability of signatures, the signature verification has been replaced with an array lookup: the signature verification can succeed only when $\text{concat}(x_{pk_A}, B, N)$ has been signed with $sk_A$, so we look for the message $\text{concat}(x_{pk_A}, B, N)$ in the array $m$ and the event $e_B$ is executed only when this message is found. In other words, we look for an index $u \le n$ such that $m[u]$ is defined and $m[u] = \text{concat}(x_{pk_A}, B, N)$. By definition of $m$, $m[u] = \text{concat}(pk_A, x_B[u], x_N[u])$, so the equality $m[u] = \text{concat}(x_{pk_A}, B, N)$ can be replaced with $(x_{pk_A} = pk_A) \wedge (B = x_B[u]) \wedge (N = x_N[u])$. (Recall that the result of the concat function contains enough information to recover its arguments.) This transformation replaces the function symbols $pkgen$, $skgen$, $sign$, and verify with primed function symbols $pkgen'$, $skgen'$, $sign'$, and verify' respectively, to avoid repeated applications of the unforgeability of signatures with the same key. (The unforgeability of signatures is applied only to unprimed symbols.)

The soundness of the game transformations shows that $G_0 \approx G_1$. We will prove that $G_1$ satisfies the correspondences (4) and (6) with any public variables $V$, in particular with $V = \emptyset$. By Lemma 26, $G_0$ also satisfies these correspondences with public variables $V = \emptyset$. Let us sketch how the proof of correspondence (4) for the game $G_1$ will proceed. Let $Q'_{1A}$ and $Q'_{1B}$ such that $Q_{1A} = !^{i_A \le n} Q'_{1A}$ and $Q_{1B} = !^{i_B \le n} Q'_{1B}$. Assume that event $e_B$ is executed in the copy of $Q'_{1B}$ of index $i_B$, that is, $e_B(x_{pk_A}[i_B], B, N[i_B])$ is executed. (Recall that the variables $x_{pk_A}$, $N$, $u$, ... are implicitly arrays.) Then the condition of the find above $e_B$ holds, that is, $m[u[i_B]]$, $x_B[u[i_B]]$, and $x_N[u[i_B]]$ are defined, $x_{pk_A}[i_B] = pk_A$, $B = x_B[u[i_B]]$, and $N[i_B] = x_N[u[i_B]]$. Moreover, since $m[u[i_B]]$ is defined, the assignment that defines $m$ has been executed in the copy of $Q'_{1A}$ of index $i_A = u[i_B]$. Then the event $e_A(pk_A, x_B, x_N)$, located above the definition of $m$, must have been executed in that copy of $Q'_{1A}$, that is, $e_A(pk_A, x_B[u[i_B]], x_N[u[i_B]])$ has been executed.
The equalities in the condition of the find imply that this event is also $e_A(x_{pk_A}[i_B], B, N[i_B])$. To sum up, if $e_B(x_{pk_A}[i_B], B, N[i_B])$ has been executed, then $e_A(x_{pk_A}[i_B], B, N[i_B])$ has been executed, so we have the correspondence (4). This reasoning is typical of the way the prover shows correspondences. In particular, the conditions of array lookups are key in these proofs, because they allow us to relate values in processes that run in parallel (here, the processes that represent A and B), and interesting correspondences relate events that occur in such processes. Next, we detail and formalize this reasoning, both for non-injective and injective correspondences.

### 4.2.2 Non-unique Events

The only correspondence that involves a non-unique event $e$ is event($e$) $\Rightarrow$ false, and it is simply proved by noticing that the event $e$ no longer occurs in the game after the transformation prove_unique (Section 5.1.4). Therefore, non-unique events are not concerned by the proofs of Sections 4.2.3 and 4.2.4.

### 4.2.3 Non-injective Correspondences

Intuitively, in order to prove that $Q_0$ satisfies a non-injective correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, with $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$, we collect all facts that hold at events in $\psi$ and show that these facts imply $\phi$ using the equational prover.

When casesInCorresp = false, CryptoVerif uses $\mathcal{F}_\mu$ to collect these facts. When casesInCorresp = true (the default), it uses $\mathcal{F}_{\mu,c}$ for more precision. In this section, we detail the proof with $\mathcal{F}_{\mu,c}$. The usage of $\mathcal{F}_\mu$ can be considered as using a single case $c$, relying on Lemma 30 instead of Lemma 31. Formally, we collect facts that hold when the event $F$ in $\psi$ has been executed, as follows.

**Definition 16 (μ executes F, $\mathcal{F}_{F,\mu,c}$)** When $F = \text{event}(e(M_1, \dots, M_m))$ and $\mu$ event $e(M'_1, \dots, M'_m)$; $\dots$ occurs in $Q_0$ or, for $m = 0, \mu$ event abort $e$ or $\mu$ find[unique$_e]$; $\dots$ occurs in $Q_0$, we say that $\mu$ executes $F$.

If $\mu$ executes $F$ and for all $\mu$ event $e(M'_1, \dots, M'_m)$; $\dots$ in $Q_0$, $M'_1, \dots, M'_m$ are simple terms, then we define $\mathcal{F}_{F,\mu,c}^0 = \mathcal{F}_{\mu,c} \cup \{M'_j = M_j \mid j \le m\} \cup \{\text{lastdefprogrampoint}(\mu, I_\mu) \text{ if } \mu \text{ event abort } e \text{ or } \mu \text{ find}[\text{unique}_e] \dots \text{ occurs in } Q_0\}$. If additionally $F$ is not a non-unique event, then we define $\mathcal{F}_{F,\mu,c} = \mathcal{F}_{F,\mu,c}^0 \cup \mathcal{F}_\mu^{\text{Fut}}$.

Intuitively, when the event $F$ in $\psi$ has been executed, it has been executed by some subterm or subprocess of $Q_0$, so there exists a subterm or subprocess $\mu$ event $e(M'_1, \dots, M'_m)$; $\dots$ or, for $m = 0, \mu$ event abort $e$ or $\mu$ find[unique$_e]$; $\dots$ in $Q_0$ such that, the event $e(M'_1, \dots, M'_m)$ has been executed and it is equal to the event $F$, hence $M'_j = M_j$ holds for $j \le m$. Moreover, since the program point $\mu$, which executes $F$, has been reached, $\mathcal{F}_{\mu,c}$ holds for some case $c$ (Lemma 31). Furthermore, when the event aborts, it is the last step of the trace, so lastdefprogrampoint($\mu, I_\mu$) also holds. Hence $\mathcal{F}_{F,\mu,c}^0$ holds for some case $c$. Additionally, assuming we consider traces that do not execute non-unique events, since the adversary cannot stop execution of the process until the next output or event_abort $e$, $\mathcal{F}_\mu^{\text{Fut}}$ also holds (Lemma 32), so $\mathcal{F}_{F,\mu,c}$ holds for some case $c$. This is proved more formally in Lemma 37 below. (The case of get[unique$_e$] is not mentioned in Definition 16 because it is excluded by Property 4.)

We restrict ourselves to the case in which $M'_1, \dots, M'_m$ are simple terms because only simple terms allowed in sets of facts.

Let $\theta$ be a substitution equal to the identity on the variables $\tilde{x}$ of $\psi$. This substitution gives values to existentially quantified variables $\tilde{y}$ of $\phi$. We say that $\mathcal{F} \models_{\theta} \phi$ when we can show that $\mathcal{F}$ implies $\theta\phi$. Formally, we define:
$\mathcal{F} \Vdash_{\theta} M$ if and only if $\mathcal{F} \cup \{\neg \theta M\}$ yields a contradiction

$\mathcal{F} \Vdash_{\theta} \text{event}(e(M_1, \dots, M_m))$ if and only if there exist $M'_0, \dots, M'_m$ such that $M'_0 : \text{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F}$ and $\mathcal{F} \cup \{\bigvee_{j=1}^m \theta M_j \neq M'_j\}$ yields a contradiction

$\mathcal{F} \Vdash_{\theta} \phi_1 \wedge \phi_2$ if and only if $\mathcal{F} \Vdash_{\theta} \phi_1$ and $\mathcal{F} \Vdash_{\theta} \phi_2$

$\mathcal{F} \Vdash_{\theta} \phi_1 \vee \phi_2$ if and only if $\mathcal{F} \Vdash_{\theta} \phi_1$ or $\mathcal{F} \Vdash_{\theta} \phi_2$

Terms $\theta M$ are proved by contradiction, using the equational prover. Events $\theta F$ are proved by looking for some event $F'$ in $\mathcal{F}$ and showing by contradiction that $\theta F = F'$, using the equational prover.

Let $\varphi = [\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a non-injective correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms. Suppose that, for all $j \le m$, $\mu_j$ that executes $F_j$ and $c_j$ is a case for $\mathcal{F}_{\mu_j, c_j}$. For $j \le m$, let $\theta_j$ be a renaming of $I_{\mu_j}$ to fresh replication indices. (The renamings $\theta_j$ have pairwise disjoint images.) Let $\theta$ be a family parameterized by $\mu_1, c_1, \dots, \mu_m, c_m$ of substitutions equal to the identity on $\tilde{x}$. We define $\text{prove}^{\varphi}(\theta, \mu_1, c_1, \dots, \mu_m, c_m) = (\theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m} \Vdash_{\theta(\mu_1, c_1, \dots, \mu_m, c_m)} \phi)$. This function defines the algorithm that we use to prove the correspondence $\varphi$ assuming for all $j \le m$, $F_j$ is executed in $\mu_j$ and we are in case $c_j$. We also define $\text{prove}^{\varphi}(\theta, S) = \bigwedge_{(\mu_1, c_1, \dots, \mu_m, c_m) \in S} \text{prove}^{\varphi}(\theta, \mu_1, c_1, \dots, \mu_m, c_m)$.

Non-injective correspondences are proved as follows.

**Proposition 2** Let $\varphi = [\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a non-injective correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Let $Q_0$ be a process that satisfies Properties 4 and 5. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms. Let $S = \{(\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}\}$. If there exists a family of substitutions $\theta$ equal to the identity on $\tilde{x}$ such that $\text{prove}^{\varphi}(\theta, S)$ and for all evaluation contexts $C$ acceptable for $Q_0$, $\text{Pr}[C[Q_0] \preceq \neg[\text{prove}^{\varphi}(\theta, S)]] \le p(C)$, then $\text{Bound}_{Q_0}(V, \varphi, D_{\text{false}}, p)$ for any $V$.

Intuitively, when $\psi = F_1 \wedge \dots \wedge F_m$ holds, $\theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$ hold for some $\mu_1, c_1, \dots, \mu_m, c_m$. For some $\theta$ equal to the identity on $\psi$, $\theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$ implies $\theta \phi$, so $\theta \phi$ holds. Hence the correspondence is satisfied. The proof of Proposition 2 relies on the following properties and lemmas. We have

$$ \begin{align*} [\mathcal{F} \Vdash_{\theta} M] &= \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \neg \theta M) \\ [\mathcal{F} \Vdash_{\theta} \text{event}(e(M_1, \dots, M_m))] &= \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \bigvee_{j=1}^m \theta M_j \neq M'_j) \\ \text{for some } M'_0 : \text{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F} \\ [\mathcal{F} \Vdash_{\theta} \phi_1 \wedge \phi_2] &= [\mathcal{F} \Vdash_{\theta} \phi_1] \wedge [\mathcal{F} \Vdash_{\theta} \phi_2] \\ [\mathcal{F} \Vdash_{\theta} \phi_1 \vee \phi_2] &= \begin{cases} [\mathcal{F} \Vdash_{\theta} \phi_1] & \text{if } \mathcal{F} \Vdash_{\theta} \phi_1 \\ [\mathcal{F} \Vdash_{\theta} \phi_2] & \text{otherwise} \end{cases} \end{align*} $$

where $\tilde{z}$ are the non-process variables in $\mathcal{F}$, in the image of $\theta$, and in $\tilde{x}$, and $\tilde{T}''$ are their types.

**Lemma 36** $[\mathcal{F} \Vdash_{\theta} \phi] \Rightarrow \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \neg \theta \phi)$, where $\tilde{z}$ are the non-process variables in $\mathcal{F}$, in the image of $\theta$, and in $\tilde{x}$, and $\tilde{T}''$ are their types.
**Proof** By induction on $\phi$. $\square$

**Lemma 37** Let $Q_0$ be a process that satisfies Properties 4 and 5. Let $Tr$ be a full trace of $C[Q_0]$. Let $\mu\mathcal{E}v$ be the sequence of events in the last configuration of $Tr$. Let $F = \mathbf{event}(e(\tilde{M}))$ where $\tilde{M}$ is a tuple of terms and $e$ is an event that does not occur in $C$. Suppose that the arguments of $e$ in $Q_0$ are always simple terms. Let $\rho$ be a mapping of the variables of $\tilde{M}$ and $\tau$ to their values. Suppose that $Tr, \rho \vdash F@\tau$.

Then there exist a program point $\mu$ (in $Q_0$) that executes $F$ 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 $\mu\mathcal{E}v(\rho(\tau)) = (\mu, \sigma(\theta' I_\mu)) : e(\dots)$ and $Tr, \sigma \cup \rho \vdash \theta' \mathcal{F}_{F,\mu,c}^0$. If additionally, $Tr$ does not execute a non-unique event of $Q_0$, then $Tr, \sigma \cup \rho \vdash \theta' \mathcal{F}_{F,\mu,c}$.

**Proof** Let $E = E_{Tr}$. Since $Tr, \rho \vdash F@\tau$ and the variables of $\tilde{M}$ and $\tau$ are defined in $\rho$, there exists $\tilde{a}$ such that $\rho, \tilde{M} \Downarrow \tilde{a}$ and $\mu\mathcal{E}v(\rho(\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\mathcal{E}v$ is (Event), (EventAbort), (CtxEvent), (FindE), (Find3), (GetE), (Get3), or (EventT).

* In case (Event), the initial configuration of rule (Event) is of the form $E_1, (\sigma_1, \mu\mathbf{event} e(\tilde{a}); P), Q_0, Ch_0, T_1, \mu\mathcal{E}v_1$. By Lemma 8, Property 1 applied to this configuration, we have reductions

$$ 
\begin{align*}
\mathit{Conf} = E_0, (\sigma_0, \mu\mathbf{event} \ e(\tilde{M}'); P), &\ Q_0, Ch_0, T_0, \mu\mathcal{E}v_0 \\
& \xrightarrow{p_0} t_0 \dots \xrightarrow{p_1} t_1 \ E_1, (\sigma_1, \mu\mathbf{event} \ e(\tilde{a}); P), \ Q_0, Ch_0, T_1, \mu\mathcal{E}v_1 \\
& \xrightarrow{1} \ E_1, (\sigma_1, P), \ Q_0, Ch_0, T_1, (\mu\mathcal{E}v_1, (\mu, \mathrm{Im}(\sigma_1)) : e(\tilde{a}))
\end{align*}
$$

where $\mu\mathbf{event} e(\tilde{M}'); P$ is a subprocess of $C[Q_0]$ up to renaming of channels, by any number of applications of (Ctx) and a final application of (Event).

* In case (EventAbort), (Find3), or (Get3), the rules that can conclude with a process $\mu P$ with $P = \mathbf{event\_abort} e, P = \mathbf{find}[\mathit{unique}_e]\dots$, or $P = \mathbf{get}[\mathit{unique}_e]\dots$ are (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Output), (Event) and by Corollary 1, their target process is a subprocess of $C[Q_0]$ up to renaming of channels. So we have a reduction

$$ 
\begin{align*}
\mathit{Conf} = E_0, (\sigma_0, \mu P), &\ Q_0, Ch_0, T_0, \mu\mathcal{E}v_0 \\
& \xrightarrow{p} t \ E_0, (\sigma_0, \mathbf{abort}), \ Q_0, Ch_0, T_0, (\mu\mathcal{E}v_0, (\mu, \mathrm{Im}(\sigma_0)) : e)
\end{align*}
$$

where $\mu P$ is a subprocess of $C[Q_0]$ up to renaming of channels, by (EventAbort), (Find3), or (Get3).

* In case (EventT), the initial configuration of the rule (EventT) is of the form $E_1, \sigma_1, \mu\mathbf{event} e(\tilde{a}); N, T_1, \mu\mathcal{E}v_1$. By Lemma 8, Property 5 applied to this configuration with $l = 0$, we have reductions

$$ 
\begin{align*}
\mathit{Conf} = E_0, \sigma_0, &\ \mu\mathbf{event} \ e(\tilde{M}'); N, T_0, \mu\mathcal{E}v_0 \\
& \xrightarrow{p_0} t_0 \dots \xrightarrow{p_1} t_1 \ E_1, \sigma_1, \mu\mathbf{event} \ e(\tilde{a}); N, T_1, \mu\mathcal{E}v_1 \\
& \xrightarrow{1} \ E_1, \sigma_1, N, T_1, (\mu\mathcal{E}v_1, (\mu, \mathrm{Im}(\sigma_1)) : e(\tilde{a}))
\end{align*}
$$

where $\mu\mathbf{event} e(\tilde{M}'); N$ is a subterm of $C[Q_0]$, by any number of applications of (CtxT) and a final application of (EventT).
* In case (CtxEvent), the only rule that can conclude with a process $C[\text{event_abort}(\mu, \tilde{a}_0) : e]$ is (Ctx). (The rules (New), (Let), (If1), (If2), (Find1), (Find2), (Insert), (Get1), (Get2), (Output), (Event) cannot conclude with $C[\text{event_abort}(\mu, \tilde{a}_0) : e]$ because, by Corollary 1, their target process is a subprocess of $C[Q_0]$ up to renaming of channels, and the initial process $C[Q_0]$ does not contain the abort event value $\text{event_abort}(\mu, \tilde{a}_0) : e$.) Hence, there is a rule that concludes with a term $\text{event_abort}(\mu, \tilde{a}_0) : e$.

In cases (FindE) and (GetE), there is also a rule that concludes with a term $\text{event_abort}(\mu, \tilde{a}_0) : e$.

The only rules that conclude with a term $\text{event_abort}(\mu, \tilde{a}_0) : e$ are (FindTE), (FindT3), (GetTE), (GetT3), (EventAbortT), and (CtxEventT). (It cannot be (NewT), (LetT), (IfT1), (IfT2), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), (EventT), (DefinedYes) because, by Corollary 1, their target term is a subterm of $C[Q_0]$, and the initial process $C[Q_0]$ does not contain the abort event value $\text{event_abort}(\mu, \tilde{a}_0) : e$.) In cases (FindTE) and (GetTE), there is recursively another rule that concludes with $\text{event_abort}(\mu, \tilde{a}_0) : e$. In case (CtxEventT), the only rule that can conclude with $C[\text{event_abort}(\mu, \tilde{a}_0) : e]$ is (CtxT), so there is recursively another rule that concludes with $\text{event_abort}(\mu, \tilde{a}_0) : e$. Therefore, $\text{event_abort}(\mu, \tilde{a}_0) : e$ ultimately comes from an application of (EventAbortT), (FindT3), or (GetT3):

$$ Conf = E_0, \sigma_0, \mu N, \mathcal{T}_0, \mu \mathcal{E}v_0 \xrightarrow{p} t E_0, \sigma_0, \text{event_abort}(\mu, \text{Im}(\sigma_0)) : e, \mathcal{T}_0, \mu \mathcal{E}v_0 $$

where $N = \text{event_abort } e$, $N = \text{find}[\text{unique}_e]...$, or $N = \text{get}[\text{unique}_e]...$. Furthermore, the only rules that can conclude with such a term $\mu N$ are (NewT), (IfT1), (IfT2), (LetT), (FindT1), (FindT2), (InsertT), (GetT1), (GetT2), (EventT), (DefinedYes) and, by Corollary 1, their target term is a subterm of $C[Q_0]$.

In all cases, since $e$ does not occur in $C$, $\mu$ is in fact a program point of $Q_0$. Therefore, the process or term at program point $\mu$ in $Q_0$ is of the form $\mu \text{event } e(\tilde{M}');...$, $\mu \text{event_abort } e$, $\mu \text{find}[\text{unique}_e]...$, or $\mu \text{get}[\text{unique}_e]...$. In cases (Event) and (EventT), we have $\sigma_0 = \sigma_1$ by Lemma 3. In all cases, $\text{Dom}(\sigma_0) = I_\mu$ are the current replication indices at program point $\mu$ by Lemma 2, and $\text{Im}(\sigma_0) = \tilde{a}_0$, so $\sigma_0 = [I_\mu \mapsto \tilde{a}_0]$. Moreover, $\tilde{M}'$ are simple terms, so their evaluation can be written $E_0, \{I_\mu \mapsto \tilde{a}_0\}, \tilde{M}' \downarrow \tilde{a}$. Let $\sigma = \{\theta' I_\mu \mapsto \tilde{a}_0\}$. We have $\mu \mathcal{E}v(\rho(\tau)) = (\mu, \sigma(\theta' I_\mu)) : e(\tilde{a})$.

We have $E_0, \sigma_0, \tilde{M}' \downarrow \tilde{a}$ so $E_0, \sigma, \theta' \tilde{M}' \downarrow \tilde{a}$. The environment $E_{Tr}$ extends $E_0$, so $E_{Tr}, \sigma, \theta' \tilde{M}' \downarrow \tilde{a}$, so $Tr, \sigma \cup \rho \vdash \theta' \tilde{M}' = \tilde{M}$.

The configuration Conf is at program point $\mu$ in $Tr$, so by Corollary 3, we have $Tr, \sigma \vdash \theta' \mathcal{F}_{\mu,c}$.

When the process or term at $\mu$ is $\mu \text{event_abort } e$, $\mu \text{find}[\text{unique}_e]...$, or $\mu \text{get}[\text{unique}_e]...$, the environment and replication indices in Conf are the same as at the end of the trace, since the execution after Conf applies (EventAbort), (Find3), or (Get3), which terminate the trace keeping the same environment and replication indices as in Conf or (EventAbortT), (FindT3), or (GetT3) which build an abort event value keeping the same environment and replication indices as in Conf, followed by some rules among (FindTE), (GetTE), (CtxT), (CtxEventT), (FindE), (GetE), (Ctx), and (CtxEvent), which preserve the environment and replication indices that come with the abort event value. So $Tr, \sigma \vdash \text{lastdefprogrampoint}(\mu, \theta' I_\mu)$.

Therefore, $\mu$ executes $F$ and $Tr, \sigma \cup \rho \vdash \theta' \mathcal{F}_{F,\mu,c}^0$ for some $c$.

Suppose additionally that $Tr$ does not execute any non-unique event of $Q_0$. Let $Tr''$ be the prefix of $Tr$ that stops at the first evaluated output $c[a']\langle b \rangle; Q$ that follows Conf, or $Tr'' = Tr$ if $Tr$ contains no output after Conf. By Lemma 32, we have $Tr'' \vdash \mathcal{F}_{\mu}^{\text{Fut}}$, so $Tr'', \sigma \vdash \theta' \mathcal{F}_{\mu}^{\text{Fut}}$.
Moreover, E extends $E_{Tr''}$ and by Lemma 3, $\mu E v_{Tr}$ extends $\mu E v_{Tr''}$, so $Tr, \sigma \vdash \theta' \mathcal{F}_{\mu}^{\text{Fut}}$. Therefore, $Tr, \sigma \cup \rho \vdash \theta' \mathcal{F}_{F,\mu,c}$ for some c. $\square$

**Lemma 38** Let $\varphi = [\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a non-injective correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Let $Q_0$ be a process that satisfies Properties 4 and 5. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms.

Let $S = \{(\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}\}$. Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. Let $Tr$ be a full trace of $C[Q_0]$ that does not execute any non-unique event of $Q_0$. If $Tr \vdash \neg \varphi$, then for any $\theta$ family of substitutions equal to the identity on $\tilde{x}$, $Tr \vdash \neg[\text{prove}^{\varphi}(\theta, S)]$.

**Proof** Since $Tr \vdash \neg \varphi$, we have $Tr \vdash \exists \tilde{x} \in \tilde{T}, F_1 \wedge \dots \wedge F_m \wedge \forall \tilde{y} \in \tilde{T}', \neg \phi$. So there exists $\rho$ that maps $\tilde{x}$ to elements of $\tilde{T}$ such that $Tr, \rho \vdash F_1 \wedge \dots \wedge F_m \wedge \forall \tilde{y} \in \tilde{T}', \neg \phi$. By Lemma 37, for all $j \le m$, there exists a program point $\mu_j$ (in $Q_0$) that executes $F_j$ and a case $c_j$ such that, for any $\theta_j$ renaming of $I_{\mu_j}$ to fresh replication indices, there exists a mapping $\sigma_j$ with domain $\theta_j I_{\mu_j}$ such that $Tr, \sigma_j \cup \rho \vdash \theta_j \mathcal{F}_{F_j, \mu_j, c_j}$. Since $Tr, \rho \vdash \forall \tilde{y} \in \tilde{T}', \neg \phi$, we have $Tr, \rho \vdash \neg \theta(\mu_1, c_1, \dots, \mu_m, c_m)\phi$. Therefore, $Tr, \sigma_1 \cup \dots \cup \sigma_m \cup \rho \vdash \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m} \cup \{\neg \theta(\mu_1, c_1, \dots, \mu_m, c_m)\phi\}$, so $Tr \vdash \exists \theta_1 I_{\mu_1}, \dots, \exists \theta_m I_{\mu_m}, \exists \tilde{x} \in \tilde{T}, \wedge \mathcal{F}_0(\mu_1, c_1, \dots, \mu_m, c_m) \wedge \neg \theta(\mu_1, c_1, \dots, \mu_m, c_m)\phi$ where $\mathcal{F}_0(\mu_1, c_1, \dots, \mu_m, c_m) = \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$. We have

$$ \{[\text{prove}^{\varphi}(\theta, \mu_1, c_1, \dots, \mu_m, c_m)] \} \\ \Rightarrow \forall \theta_1 I_{\mu_1}, \dots, \forall \theta_m I_{\mu_m}, \forall \tilde{x} \in \tilde{T}, \neg (\wedge \mathcal{F}_0(\mu_1, c_1, \dots, \mu_m, c_m) \wedge \neg \theta(\mu_1, c_1, \dots, \mu_m, c_m)\phi) $$

by Lemma 36. (The non-process variables in $\mathcal{F}_0(\mu_1, c_1, \dots, \mu_m, c_m)$, in the image of $\theta(\mu_1, c_1, \dots, \mu_m, c_m)$, and in $\tilde{x}$ are in $\theta_1 I_{\mu_1}, \dots, \theta_m I_{\mu_m}, \tilde{x}$.) So $Tr \vdash \neg[\text{prove}^{\varphi}(\theta, \mu_1, c_1, \dots, \mu_m, c_m)]$, so $Tr \vdash \neg[\text{prove}^{\varphi}(\theta, S)]$. $\square$

**Proof of Proposition 2** Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. We have

$$ \begin{align*} \text{Adv}_{Q_0}(C, \varphi, D_{\text{false}}) &= \text{Pr}[C[Q_0] : \neg \varphi \wedge \neg \text{NonUnique}_{Q_0}] \\ &\le \text{Pr}[C[Q_0] : \neg[\text{prove}^{\varphi}(\theta, S)]] & \text{by Lemma 38} \\ &\le \text{Pr}[C[Q_0] \le \neg[\text{prove}^{\varphi}(\theta, S)]] & \text{by Lemma 1} \\ &\le p(C) \end{align*} $$

So $\text{Bound}_{Q_0}(V, \varphi, D_{\text{false}}, p)$. $\square$

**Example 6** Let us prove that the example $G_1$ satisfies (4). We first study the facts $\mathcal{F}_{\mu_B}$ that hold at the program point $\mu_B$ that executes event $e_B$. $\mathcal{F}_{\mu_B}$ contains defined($m[u[i_B]]$), defined($x_B[u[i_B]]$), defined($x_N[u[i_B]]$), $x_{pk_A}[i_B] = pk_A$, $B = x_B[u[i_B]]$, and $N[i_B] = x_N[u[i_B]]$, because the condition of find holds at $\mu_B$. Moreover, we have defined($m[u[i_B]]$) $\in \mathcal{F}_{\mu_B}$, and, when $m[i_A]$ is defined, $(\mu_A, i_A) : \text{event}(e_A(pk_A, x_B[i_A], x_N[i_A]))$ holds, so $(\mu_A, i_A) : \text{event}(e_A(pk_A, x_B[i_A], x_N[i_A]))\{u[i_B]/i_A\} \in \mathcal{F}_{\mu_B}$, that is, $(\mu_A, u[i_B]) : \text{event}(e_A(pk_A, x_B[u[i_B]], x_N[u[i_B]])) \in \mathcal{F}_{\mu_B}$. In other words, since $m$ is defined at index $u[i_B]$, event $e_A$ has been executed in the copy of $Q'_{1A}$ of index $u[i_B]$. ($\mathcal{F}_{\mu_B}$ also contains other facts, which are useless for proving the desired correspondences, so we do not list them.)

For $\psi = F = \text{event}(e_B(x, y, z))$, $\mu_B$ is the only program point that executes $F$, so this event has been executed in some copy of $Q'_{1B}$ of index $i'_B$, with $x_{pk_A}[i'_B] = x, B = y, N[i'_B] = z$. Then,
when $\psi$ holds, the facts $\theta' \mathcal{F}_{F,\mu_B} \supseteq \theta' \mathcal{F}_{\mu_B} \cup \{x_{pk_A}[i'_B] = x, B = y, N[i'_B] = z\}$ hold for some value of $i'_B$, with $\theta' = \{i'_B/i_B\}$. (We consider a single case $c$ here, so we can simply omit the case $c$.)

Furthermore, the substitution $\theta(\mu_B)$ is the identity since all variables of $\phi$ also occur in $\psi$. Then we just have to show that $\theta' \mathcal{F}_{F,\mu_B}$ implies $\phi = \text{event}(e_A(x, y, z))$, that is, $\theta' \mathcal{F}_{F,\mu_B} \models_{\theta(\mu_B)} \text{event}(e_A(x, y, z))$. Since $(\mu_A, u[i_B]) : \text{event}(e_A(pk_A, x_B[u[i_B]]), x_N[u[i_B]]) \in \mathcal{F}_{\mu_B}$, we have $(\mu_A, u[i'_B]) : \text{event}(e_A(pk_A, x_B[u[i'_B]]), x_N[u[i'_B]]) \in \theta' \mathcal{F}_{F,\mu_B}$, so the equational prover just has to prove by contradiction that $e_A(pk_A, x_B[u[i'_B]], x_N[u[i'_B]]) = e_A(x, y, z)$, that is, $pk_A = x, x_B[u[i'_B]] = y$, and $x_N[u[i'_B]] = z$. The proof succeeds using the following equalities of $\theta' \mathcal{F}_{F,\mu_B}$: $x_{pk_A}[i'_B] = x$, $B = y$, $N[i'_B] = z$, $x_{pk_A}[i'_B] = pk_A$, $B = x_B[u[i'_B]]$, and $N[i'_B] = x_N[u[i'_B]]$.

Hence, $G_1$ satisfies (4) with any public variables $V$: if $\psi = \text{event}(e_B(x, y, z))$ has been executed, then $\phi = \text{event}(e_A(x, y, z))$ has been executed.

In the implementation, the substitution $\theta$ is initially defined as the identity on $\tilde{x} = \text{var}(\psi)$. It is defined on other variables when checking $\mathcal{F} \models_{\theta} M$ by trying to find $\theta$ such that $\theta M \in \mathcal{F}$, and when checking $\mathcal{F} \models_{\theta} \text{event}(e(M_1, \dots, M_m))$ by trying to find $\theta$ such that $\theta \text{event}(e(M_1, \dots, M_m)) \in \mathcal{F}$. When we do not manage to find the image by $\theta$ of all variables of $M$, resp. $M_1, \dots, M_m$, the check fails. When there are several suitable facts $\theta M \in \mathcal{F}$ or $\theta \text{event}(e(M_1, \dots, M_m)) \in \mathcal{F}$, the system tries all possibilities.

### 4.2.4 Injective Correspondences

Injective correspondences are more difficult to check than non-injective ones, because they require distinguishing between several executions of the same event. We achieve that by relying on the pair (program points, replication indices) that is recorded in the sequence $\mu\mathcal{E}v$ together with each event: distinct executions of events either occur at different program points or have different values of replication indices.

We extend Definition 16 to injective events, with exactly the same definition as for non-injective events.

The proof of injective correspondences extends that for non-injective correspondences: for a correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, we additionally prove that distinct executions of the injective events of $\psi$ correspond to distinct executions of each injective event of $\phi$, that is, if the injective events of $\psi$ have different pairs (program point, replication indices), then each injective event of $\phi$ has a different pair (program point, replication indices). In order to achieve this proof, we collect the following information for each injective event of $\phi$:

* the set of facts $\mathcal{F}$ that are known to hold, which will be used to reason on replication indices of events;

* the program point and replication indices of the considered injective event of $\phi$, stored in a pair $M_0$; these program point and indices are computed when we prove that this event is executed;

* the program point and replication indices of the injective events of $\psi$, stored as a mapping $\mathcal{I} = \{j \mapsto (\mu_j, \theta_j I_{\mu_j}) \mid F_j$ is an injective event$\}$, where $\psi = F_1 \wedge \dots \wedge F_m$, $\mu_j$ is the program point that executes $F_j$, and $\theta_j$ is a renaming of $I_{\mu_j}$ to fresh replication indices, for $j \le m$;

* the set $\mathcal{V}$ containing the replication indices in $\mathcal{F}$ and the variables $\tilde{x}$ of $\psi$; these variables will be renamed to fresh variables in order to avoid conflicts of variable names between different events.

This information is stored in a set $\mathcal{S}$, which contains quadruples $(\mathcal{F}, M_0, \mathcal{I}, \mathcal{V})$. We will show that, if the pair (program point, replication indices) of two executions of the injective events of
$\psi$ are different, then the pair (program, replication indices) of the corresponding executions of the considered injective event of $\phi$ are also different. The equality between pairs (program point, replication indices) is obviously defined as the equality between program points and between replication indices. Formally, we consider $(\mathcal{F}, M_0, \mathcal{I}, \mathcal{V})$ and $(\mathcal{F}', M'_0, \mathcal{I}', \mathcal{V}')$ in $\mathcal{S}$. We rename the variables $\mathcal{V}'$ of the second element to fresh variables by a substitution $\theta''$ and show that, if $\mathcal{I} \neq \theta''\mathcal{I}'$, then $M_0 \neq \theta''M'_0$ (knowing $\mathcal{F}$ and $\theta''\mathcal{F}'$). This property implies injectivity.

Since this reasoning is done for each injective event in $\phi$, we collect the associated sets $\mathcal{S}$ in a pseudo-formula $\mathcal{C}$, obtained by replacing each injective event of $\phi$ with a set $\mathcal{S}$ and all other leaves of $\phi$ with $\perp$.

We say that $\vdash \mathcal{C}$ when for all non-bottom leaves $\mathcal{S}$ of $\mathcal{C}$, for all $(\mathcal{F}, M_0, \mathcal{I}, \mathcal{V})$, $(\mathcal{F}', M'_0, \mathcal{I}', \mathcal{V}')$ in $\mathcal{S}$, $\mathcal{F} \cup \theta''\mathcal{F}' \cup \{\bigvee_{j \in \text{Dom}(\mathcal{I})} \mathcal{I}(j) \neq \theta''\mathcal{I}'(j), M_0 = \theta''M'_0\}$ yields a contradiction, where the substitution $\theta''$ is a renaming of variables in $\mathcal{V}'$ to distinct fresh variables. As explained above, the condition $\vdash \mathcal{C}$ guarantees injectivity.

We extend the definition of $\mathcal{F} \models_{\theta} \phi$ used for non-injective correspondences to $\mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}} \phi$, which means that $\mathcal{F}$ implies $\theta\phi$ and $\mathcal{C}$ correctly collects the tuples $(\mathcal{F}, M_0, \mathcal{I}, \mathcal{V})$ associated to this proof. Formally, we define:

$$ \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\perp} M \text{ if and only if } \mathcal{F} \cup \{\neg \theta M\} \text{ yields a contradiction} $$

$$ \begin{array}{l} \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\perp} \text{event}(e(M_1, \dots, M_m)) \text{ if and only if} \\ \quad \text{there exist } M'_0, \dots, M'_m \text{ such that } M'_0 : \text{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F} \text{ and} \\ \quad \mathcal{F} \cup \{\bigvee_{j=1}^m \theta M_j \neq M'_j\} \text{ yields a contradiction} \end{array} $$

$$ \begin{array}{l} \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{S}} \text{inj-event}(e(M_1, \dots, M_m)) \text{ if and only if} \\ \quad \text{there exist } M'_0, \dots, M'_m \text{ such that } M'_0 : \text{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F}, \\ \quad \mathcal{F} \cup \{\bigvee_{j=1}^m \theta M_j \neq M'_j\} \text{ yields a contradiction, and } (\mathcal{F}, M'_0, \mathcal{I}, \mathcal{V}) \in \mathcal{S}. \end{array} $$

$$ \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_1 \wedge \mathcal{C}_2} \phi_1 \wedge \phi_2 \text{ if and only if } \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_1} \phi_1 \text{ and } \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_2} \phi_2 $$

$$ \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_1 \vee \mathcal{C}_2} \phi_1 \vee \phi_2 \text{ if and only if } \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_1} \phi_1 \text{ or } \mathcal{F} \models_{\theta}^{\mathcal{I},\mathcal{V},\mathcal{C}_2} \phi_2 $$

These formulas differ from the non-injective case in that we propagate $\mathcal{I}$, $\mathcal{V}$, $\mathcal{C}$ and, in the case of injective events, we make sure that quadruples $(\mathcal{F}, M'_0, \mathcal{I}, \mathcal{V})$ are collected correctly by requiring that $(\mathcal{F}, M'_0, \mathcal{I}, \mathcal{V}) \in \mathcal{S}$.

Let $\varphi = [\sqrt{\tilde{x}} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms. Suppose that, for all $j \le m$, $\mu_j$ executes $F_j$ and $c_j$ is a case for $\mathcal{F}_{\mu_j, c_j}$. For $j \le m$, let $\theta_j$ be a renaming of $I_{\mu_j}$ to fresh replication indices. (The renamings $\theta_j$ have pairwise disjoint images.) Let $\mathcal{C}$ be a pseudo formula and $\theta$ be a family parameterized by $\mu_1, c_1, \dots, c_m, \mu_m$ of substitutions equal to the identity on $\tilde{x}$. We define prove$^{\varphi}(\mathcal{C}, \theta, \mu_1, c_1, \dots, \mu_m, c_m) = (\mathcal{F} \models_{\theta(\mu_1, c_1, \dots, \mu_m, c_m)}^{\mathcal{I},\mathcal{V},\mathcal{C}} \phi)$ where $\mathcal{F} = \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$, $\mathcal{I} = \{j \mapsto (\mu_j, \theta_j I_{\mu_j}) \mid F_j \text{ is an injective event}\}$, and $\mathcal{V} = \text{var}(\theta_1 I_{\mu_1}) \cup \dots \cup \text{var}(\theta_m I_{\mu_m}) \cup \{\tilde{x}\}$. The algorithm prove$^{\varphi}(\mathcal{C}, \theta, \mu_1, \dots, \mu_m)$ shows that the non-injective version of the correspondence $\varphi$ holds assuming the events in $\psi = F_1 \wedge \dots \wedge F_m$ are executed at program points $\mu_1, \dots, \mu_m$ respectively. Indeed, in this case, the facts $\mathcal{F} = \theta_1 \mathcal{F}_{F_1, \mu_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m}$ hold and the formula $\mathcal{F} \models_{\theta(\mu_1, \dots, \mu_m)}^{\mathcal{I},\mathcal{V},\mathcal{C}} \phi$ shows that this implies $\theta(\mu_1, \dots, \mu_m)\phi$. (The substitution $\theta(\mu_1, \dots, \mu_m)\phi$ determines the values of $\tilde{y}$.) Additionally, prove$^{\varphi}(\mathcal{C}, \theta, \mu_1, \dots, \mu_m)$ makes sure that $\mathcal{C}$ correctly collects the information needed to prove injectivity. We also define prove$^{\varphi}(\mathcal{C}, \theta, \mathcal{S}) = (\vdash \mathcal{C}) \wedge \bigwedge_{(\mu_1, c_1, \dots, \mu_m, c_m) \in \mathcal{S}} \text{prove}^{\varphi}(\mathcal{C}, \theta, \mu_1, c_1, \dots, \mu_m, c_m)$. This algorithm proves the correspondence $\varphi$ assuming the events in $\psi$ are executed at program points in $\mathcal{S}$. It verifies injectivity via $\vdash \mathcal{C}$.
The following proposition shows the soundness of the proof of injective correspondences based on this algorithm.

**Proposition 3** Let $\varphi = [\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \ \text{var}(\psi)$. Let $Q_0$ be a process that satisfies Properties 4 and 5. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms.

Let $S = \{(\mu_1, c_1, \dots, \mu_m, c_m) \mid \forall j \le m, \mu_j$ executes $F_j$ and $c_j$ is a case for $F_{\mu_j, c_j}\}$. Assume that there exist a pseudo-formula $C$ and a family of substitutions $\theta$ equal to the identity on $\tilde{x}$ such that $\text{prove}^{\varphi}(C, \theta, S)$. Assume that for all evaluation contexts $C$ acceptable for $Q_0$, $\text{Pr}[C[Q_0] \subseteq \neg[\text{prove}^{\varphi}(C, \theta, S)]] \le p(C)$.

Then $\text{Bound}_{Q_0}(V, \varphi, D_{\text{false}}, p)$ for any $V$.

In the implementation, the value of $C$ is computed by adding $(\mathcal{F}, M'_0, \mathcal{I}, \mathcal{V})$ to $S$ when handling injective events during the checking of $\text{prove}^{\varphi}(C, \theta, S)$. We check $\vdash C$ incrementally, after each addition of an element to $C$. The proof of Proposition 3 relies on the following definitions and lemmas. We have

$$ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \perp} M]\} = \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \neg \theta M) $$

$$ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \perp} \mathbf{event}(e(M_1, \dots, M_m))\} = \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \bigvee_{j=1}^{m} \theta M_j \neq M'_j) \\ \text{for some } M'_0 : \mathbf{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F} $$

$$ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, S} \mathbf{inj-event}(e(M_1, \dots, M_m))\} = \forall \tilde{z} \in \tilde{T}'' , \neg (\bigwedge \mathcal{F} \wedge \bigvee_{j=1}^{m} \theta M_j \neq M'_j) \\ \text{for some } M'_0 : \mathbf{event}(e(M'_1, \dots, M'_m)) \in \mathcal{F} \text{ and } (\mathcal{F}, M'_0, \mathcal{I}, \mathcal{V}) \in S $$

$$ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1 \wedge C_2} \phi_1 \wedge \phi_2]\} = \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1} \phi_1]\} \wedge \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_2} \phi_2]\} $$

$$ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1 \vee C_2} \phi_1 \vee \phi_2]\} = \begin{cases} \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1} \phi_1]\} & \text{if } \mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1} \phi_1 \\ \{[\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_2} \phi_2]\} & \text{otherwise} \end{cases} $$

where $\tilde{z} = \mathcal{V}$ and $\tilde{T}''$ are the types of these variables. We also have

$$ \{[\vdash C]\} = \bigwedge_{S \neq \perp} \bigwedge_{\text{leaf of } C(\mathcal{F}, M_0, \mathcal{I}, \mathcal{V}) \in S} \bigwedge_{(\mathcal{F}', M'_0, \mathcal{I}', \mathcal{V}') \in S} \forall \tilde{z} \in \tilde{T}'' , \\ \neg \left( \bigwedge \mathcal{F} \wedge \bigwedge \theta'' \mathcal{F}' \wedge \left( \bigvee_{j \in \text{Dom}(\mathcal{I})} \mathcal{I}(j) \neq \theta'' \mathcal{I}'(j) \right) \wedge M_0 = \theta'' M'_0 \right) $$

where the substitution $\theta''$ is a renaming of variables in $\mathcal{V}'$ to distinct fresh variables, $\tilde{z} = \mathcal{V} \cup \theta''\mathcal{V}'$, and $\tilde{T}''$ are the types of these variables.

We define formula_($\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C} \phi$) as follows:

$$ \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \perp} M) = \theta M $$

$$ \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \perp} \mathbf{event}(e(M_1, \dots, M_m))) = \theta \mathbf{event}(e(M_1, \dots, M_m)) $$

$$ \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, S} \mathbf{inj-event}(e(M_1, \dots, M_m))) = $$

$$ \bigvee_{(\mathcal{F}, N_0, \mathcal{I}, \mathcal{V}) \in S} \exists \tau \in \mathbb{N}, N_0 : \theta \mathbf{event}(e(M_1, \dots, M_m)) @ \tau $$

$$ \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1 \wedge C_2} \phi_1 \wedge \phi_2) = \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_1} \phi_1) \wedge \text{formula}_{\theta}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, C_2} \phi_2) $$
$$ \text{formula}(\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C_1 \lor C_2} \phi_1 \lor \phi_2) = \begin{cases} \text{formula}(\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C_1} \phi_1) & \text{if } \mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C_1} \phi_1 \\ \text{formula}(\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C_2} \phi_2) & \text{otherwise} \end{cases} $$

The formula $\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C} \phi$ generalizes $\theta\phi$ to the case of injective events.

**Lemma 39** $\{[\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C} \phi]\} \Rightarrow \forall \tilde{z} \in \tilde{T}''$, $\neg (\bigwedge \mathcal{F} \wedge \neg \text{formula}(\mathcal{F} \models_{\theta}^{\mathcal{I},\nu,C} \phi))$ where $\tilde{z} = \mathcal{V}$ and $\tilde{T}''$ are the types of these variables.

**Proof** By induction on $\phi$. This result is similar to Lemma 36. The case of injective events is new. The case of disjunction differs, but is straightforward by induction hypothesis. $\square$

The next lemma shows that, for events $e$ in the considered correspondence, two distinct executions of event $e$ have distinct pairs (program point, replication indices). When the term $M$ contains no array accesses, we define $\sigma(M)$ by $\sigma, M \downarrow \sigma(M)$.

**Lemma 40** Assume that the event $e$ is used in the correspondence $\varphi$. Let $Q_0$ be a process that satisfies Property 4. Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. If $\text{initConfig}(C[Q_0]) \xrightarrow{p_1} t_1 \dots \xrightarrow{p_{m-1}} t_{m-1} \in E$, $(\sigma, P), Q, C, \mathcal{T}, \mu\mathcal{E}v, \mu\mathcal{E}v(\tau) = (\mu, \tilde{a}) : e(a_1, \dots, a_m), \mu\mathcal{E}v(\tau') = (\mu', \tilde{a}') : e(a'_1, \dots, a'_m)$, and $\tau \neq \tau'$, then $(\mu, \tilde{a}) \neq (\mu', \tilde{a}')$.

**Proof** Let us fix the event symbol $e$. We define the multisets $\text{Events}(\tilde{a}, M)$, $\text{Events}(\tilde{a}, P)$, and $\text{Events}(\tilde{a}, Q)$ by

$$ \text{Events}(\tilde{a}, \mu i) = \emptyset $$

$$ \text{Events}(\tilde{a}, \mu x[M_1, \dots, M_m]) = \biguplus_{j \in \{1, \dots, m\}} \text{Events}(\tilde{a}, M_j) $$

$$ \text{Events}(\tilde{a}, \mu f(M_1, \dots, M_m)) = \biguplus_{j \in \{1, \dots, m\}} \text{Events}(\tilde{a}, M_j) $$

$$ \text{Events}(\tilde{a}, \mu \text{new } x[\tilde{i}] : T; N) = \text{Events}(\tilde{a}, N) $$

$$ \text{Events}(\tilde{a}, \mu \text{let } x[\tilde{i}] : T = M \text{ in } N) = \text{Events}(\tilde{a}, M) \uplus \text{Events}(\tilde{a}, N) $$

$$ \text{Events}(\tilde{a}, \mu \text{if } M \text{ then } N \text{ else } N') = \text{Events}(\tilde{a}, M) \uplus \max(\text{Events}(\tilde{a}, N), \text{Events}(\tilde{a}, N')) $$

$$ \text{Events}(\tilde{a}, \mu \text{find}[\text{unique}？]) (\bigoplus_{j=1}^{m} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ such that } \text{defined}(\tilde{M}_j) \land M'_j \text{ then } N_j) \text{ else } N') = $$

$$ \biguplus_{j=1}^{m} \biguplus_{\tilde{a}_j \le \tilde{n}_j} \text{Events}((\tilde{a}, \tilde{a}_j), M'_j) \uplus \max(\max_{j=1}^{m} \text{Events}(\tilde{a}, N_j), \text{Events}(\tilde{a}, N')) $$

$$ \text{Events}(\tilde{a}, \mu \text{event } e'(M_1, \dots, M_m); M) = \biguplus_{j \in \{1, \dots, m\}} \text{Events}(\tilde{a}, M_j) \uplus \text{Events}(\tilde{a}, M) \text{ if } e' \neq e $$

$$ \text{Events}(\tilde{a}, \mu \text{event } e(M_1, \dots, M_m); M) = \{ (\mu, \tilde{a}) \} \uplus \biguplus_{j \in \{1, \dots, m\}} \text{Events}(\tilde{a}, M_j) \uplus \text{Events}(\tilde{a}, M) $$

$$ \text{Events}(\tilde{a}, \mu \text{event\_abort } e') = \emptyset \text{ if } e' \neq e $$

$$ \text{Events}(\tilde{a}, \mu \text{event\_abort } e) = \{(\mu, \tilde{a})\} $$

$$ \text{Events}(\tilde{a}, \mu 0) = \emptyset $$

$$ \text{Events}(\tilde{a}, \mu (Q_1 | Q_2)) = \text{Events}(\tilde{a}, Q_1) \uplus \text{Events}(\tilde{a}, Q_2) $$
$$ \mathit{Events}(\tilde{a}, \mu^l i \le n Q) = \biguplus_{a \in [1, n]} \mathit{Events}((\tilde{a}, a), Q) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{newChannel}} c; Q) = \mathit{Events}(\tilde{a}, Q) $$

$$ \mathit{Events}(\tilde{a}, \mu^c[M_1, \dots, M_l](x[i] : T); P) = \biguplus_{j \in \{1, \dots, l\}} \mathit{Events}(\tilde{a}, M_j) \uplus \mathit{Events}(\tilde{a}, P) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\overline{c}[M_1, \dots, M_l]}\langle N \rangle; Q) = \biguplus_{j \in \{1, \dots, l\}} \mathit{Events}(\tilde{a}, M_j) \uplus \mathit{Events}(\tilde{a}, N) \uplus \mathit{Events}(\tilde{a}, Q) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{new}} x[i] : T; P) = \mathit{Events}(\tilde{a}, P) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{let}} x[i] : T = M \text{ in } P) = \mathit{Events}(\tilde{a}, M) \uplus \mathit{Events}(\tilde{a}, P) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{if } M \text{ then } P \text{ else } P'}) = \mathit{Events}(\tilde{a}, M) \uplus \max(\mathit{Events}(\tilde{a}, P), \mathit{Events}(\tilde{a}, P')) $$

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

$$ \mathit{Events}(\tilde{a}, \mu^{\text{event } e'}(M_0, \dots, M_m); P) = \biguplus_{j \in \{1, \dots, m\}} \mathit{Events}(\tilde{a}, M_j) \uplus \mathit{Events}(\tilde{a}, P) \text{ if } e' \neq e $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{event } e}(M_0, \dots, M_m); P) = \{(\mu, \tilde{a})\} \uplus \biguplus_{j \in \{1, \dots, m\}} \mathit{Events}(\tilde{a}, M_j) \uplus \mathit{Events}(\tilde{a}, P) $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{event\_abort } e'}) = \emptyset \text{ if } e' \neq e $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{event\_abort } e}) = \{(\mu, \tilde{a})\} $$

$$ \mathit{Events}(\tilde{a}, \mu^{\text{yield}}) = \emptyset $$

(get and insert are omitted because they do not occur in the game by Property 4.)

We define the multisets

$$ \mathit{Events}(\mu\mathcal{E}v) = \{(\mu, \tilde{a}) \mid (\mu, \tilde{a}) : e(\dots) \in \mu\mathcal{E}v\} $$

$$ \mathit{Events}(E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v) = \mathit{Events}(\mathrm{Im}(\sigma), M) \uplus \mathit{Events}(\mu\mathcal{E}v) $$

$$ \mathit{Events}(E, \mathcal{Q}, \mathcal{Ch}) = \biguplus_{(\sigma', \mathcal{Q}') \in \mathcal{Q}} \mathit{Events}(\mathrm{Im}(\sigma'), \mathcal{Q}') $$

$$ \mathit{Events}(E, (\sigma, P), \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu\mathcal{E}v) = \mathit{Events}(\mathrm{Im}(\sigma), P) \uplus \biguplus_{(\sigma', \mathcal{Q}') \in \mathcal{Q}} \mathit{Events}(\mathrm{Im}(\sigma'), \mathcal{Q}') \uplus \mathit{Events}(\mu\mathcal{E}v) $$

The latter multiset contains all pairs $(\mu, \tilde{a})$ (program point, value of replication indices) for events $e(\dots)$ that may be executed in a trace that contains the configuration $E, (\sigma, P), \mathcal{Q}, \mathcal{Ch}, \mathcal{T}, \mu\mathcal{E}v$.

The multiset $\mathit{Events}(\sigma_0, C[Q_0])$ contains no duplicates. Indeed, we show by induction on $M$ that $\mathit{Events}(\tilde{a}, M)$ is included in the multiset $\{(\mu, \tilde{a}')\}$ where $\mu$ is a program point inside $M$ and $\tilde{a}$ is a prefix of $\tilde{a}'$, and similarly for $P$ and $Q$. That allows to show that all multiset unions in the computation of $\mathit{Events}$ are disjoint unions, since all recursive calls in the computation of $\mathit{Events}$ are either with disjoint processes or terms, or with different extensions of $\tilde{a}$.

Moreover, by induction on the derivations, if $E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v \xrightarrow{p} E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v'$, then $\mathit{Events}(E, \sigma, M, \mathcal{T}, \mu\mathcal{E}v) \supseteq \mathit{Events}(E', \sigma', M', \mathcal{T}', \mu\mathcal{E}v')$; if $E, \mathcal{Q}, \mathcal{Ch} \rightsquigarrow E', \mathcal{Q}', \mathcal{Ch}'$, then $\mathit{Events}(E, \mathcal{Q}, \mathcal{Ch}) \supseteq \mathit{Events}(E', \mathcal{Q}', \mathcal{Ch}')$; and if $\mathrm{Conf} \xrightarrow{p} \mathrm{Conf}'$, then $\mathit{Events}(\mathrm{Conf}) \supseteq \mathit{Events}(\mathrm{Conf}')$.

Therefore, the multiset $\mathit{Events}(\emptyset, \{(\sigma_0, C[Q_0]\}), \mathrm{fc}(C[Q_0]))$ contains no duplicates, and neither do the multisets $\mathit{Events}(\mathrm{reduce}(\emptyset, \{(\sigma_0, C[Q_0]\}), \mathrm{fc}(C[Q_0]))), \mathit{Events}(\mathrm{initConfig}(C[Q_0]))$, and
Events(Conf), where Conf = E, (σ, P), Q, Ch, T, μEv is the final configuration of the consid-
ered trace. Hence, Events(μEv) contains no duplicates, which implies the desired result. □

**Lemma 41** Let $\varphi = [\sqrt{\tilde{x}} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]$ be a correspondence that does not use non-unique events, with $\psi = F_1 \wedge \dots \wedge F_m$, $\tilde{x} = \text{var}(\psi)$, and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Let $Q_0$ be a process that satisfies Properties 4 and 5. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms.

Let $S = \{(\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}\}$. Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. Let $\text{Tr}$ be a full trace of $C[Q_0]$ that does not execute any non-unique event of $Q_0$. If $\text{Tr} \vdash \neg\varphi$, then for any family of substitutions $\theta$ equal to the identity on $\tilde{x}$, for any pseudo-formula $C$, $\text{Tr} \vdash \neg[\text{prove}^{\varphi}(C, \theta, S)]$.

**Proof** By contraposition, we suppose that, $\text{Tr} \vdash [\text{prove}^{\varphi}(C, \theta, S)]$, so for every $\mu_1$ that executes $F_1$, ..., for every $\mu_m$ that executes $F_m$, for every $c_1, \dots, c_m$, $\text{Tr} \vdash [\text{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)]$ and $\text{Tr} \vdash [\vdash C]$, and we show that $\text{Tr} \vdash \varphi$.

Let $\mu \in S$ be the sequence of events in the last configuration of $\text{Tr}$.

We use the notations of Definition 12. We construct the functions $f_1, \dots, f_k$ as follows. Let $\rho$
be a mapping of $\tau_1, \dots, \tau_m$ to elements of $\mathbb{N}$ and of $\tilde{x}$ to elements of $\tilde{T}$. Suppose that $\text{Tr}, \rho \vdash \psi^\tau$.
Then, for all $j \le m$, $\text{Tr}, \rho \vdash F_j^\tau$. By Lemma 37, there exists a program point $\mu_j$ (in $Q_0$) that
executes $F_j$ and a case $c_j$ such that, for any $\theta_j$ renaming of $I_{\mu_j}$ to fresh replication indices,
there exists a mapping $\sigma_j$ with domain $\theta_j I_{\mu_j}$ such that $\mu \in \text{Ev}(\rho(\tau_j)) = (\mu_j, \sigma_j(\theta_j I_{pp_j})) : \dots$ and
$\text{Tr}, \sigma_j \vdash \theta_j \mathcal{F}_{F_j, \mu_j, c_j}$. Let $\rho_1 = \sigma_1 \cup \dots \cup \sigma_m \cup \rho$. We have $\text{Tr}, \rho_1 \vdash \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$.

Let $\mathcal{F}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m) = \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m} \cup \{\text{--formula}(\text{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m))\}$. By Lemma 39, $[\text{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)] \Rightarrow \forall \theta_1 I_{\mu_1}, \dots, \forall \theta_m I_{\mu_m}, \forall \tilde{x} \in \tilde{T}, \neg \bigwedge \mathcal{F}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)$. So $\text{Tr} \vdash \forall \theta_1 I_{\mu_1}, \dots, \forall \theta_m I_{\mu_m}, \forall \tilde{x} \in \tilde{T}, \neg \bigwedge \mathcal{F}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)$.

Then $\text{Tr}, \rho_1 \vdash \neg \bigwedge \mathcal{F}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)$, so $\text{Tr}, \rho_1 \vdash \text{formula}(\text{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m))$, that is, $\text{Tr}, \rho_1 \vdash \text{formula}(\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \mathcal{C}} \phi)$, with $\mathcal{F} = \theta_1 \mathcal{F}_{F_1, \mu_1, c_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m, c_m}$, $\mathcal{I} = \{j \mapsto (\mu_j, \theta_j I_{\mu_j}) \mid F_j \text{ is an injective event}\}$, $\mathcal{V} = \text{var}(\theta_1 I_{\mu_1}) \cup \dots \cup \text{var}(\theta_m I_{\mu_m}) \cup \{\tilde{x}\}$, and $\theta = \theta(\mu_1, c_1, \dots, \mu_m, c_m)$.

Consider an injective event in $\phi$, associated to function $f_l$.

• If that injective event corresponds to

$$
\bigvee_{(\mathcal{F}, N_0, \mathcal{I}, \mathcal{V}) \in \mathcal{S}} \exists \tau \in \mathbb{N}, N_0 : \theta\text{event}(e(M_1, \dots, M_m))@\tau
$$

in formula($\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \mathcal{C}} \phi$), we have

$$
\mathrm{Tr}, \rho_1 \vdash \bigvee_{(\mathcal{F}, N_0, \mathcal{I}, \mathcal{V}) \in \mathcal{S}} \exists \tau \in \mathbb{N}, N_0 : \theta\text{event}(e(M_1, \dots, M_m))@\tau
$$

since formula($\mathcal{F} \models_{\theta}^{\mathcal{I}, \mathcal{V}, \mathcal{C}} \phi$) is a conjunction. So $\text{Tr}, \rho_1[\tau \mapsto a] \vdash N_0 : \theta\text{event}(e(M_1, \dots, M_m))@\tau$ for some $a \in \mathbb{N}$ and some $N_0$ such that $(\mathcal{F}, N_0, \mathcal{I}, \mathcal{V}) \in \mathcal{S}$. We define $f_l(\rho(\tau_1), \dots, \rho(\tau_m), \rho(\tilde{x})) = a$, so that $\text{Tr}, \rho_1 \vdash N_0 : \theta\text{event}(e(M_1, \dots, M_m))@f_l(\tau_1, \dots, \tau_m, \tilde{x})$.

Moreover, if $j \in I$, then $F_j$ is an injective event, $F_j = \text{inj-event}(e_j(M_{j,1}, \dots, M_{j,m}))$.
Moreover, $\text{Tr}, \rho \vdash \psi^\tau$, so $\text{Tr}, \rho \vdash F_j^\tau$, so $\text{Tr}, \rho \vdash \text{event}(e_j(M_{j,1}, \dots, M_{j,m}))@\tau_j$. Since
$\mu \in \text{Ev}(\rho(\tau_j)) = (pp_j, \sigma_j(\theta_j I_{\mu_j})) : \dots = (\mu_j, \rho_1(\theta_j I_{\mu_j})) : \dots$ and $\mathcal{I}(j) = (\mu_j, \theta_j I_{\mu_j})$, we have
$\text{Tr}, \rho_1 \vdash \mathcal{I}(j) : \text{event}(e_j(M_{j,1}, \dots, M_{j,m}))@\tau_j$.
**Proof of Proposition 3** Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. We have

$$
\begin{align*}
\mathrm{Adv}_{Q_0}(C, \varphi, D_{\mathrm{false}}) &= \Pr[C[Q_0] : \neg\varphi \land \neg\mathrm{NonUnique}_{Q_0}] \\
&\leq \Pr[C[Q_0] : \neg[\mathrm{prove}^{\varphi}(C, \theta, S)]] & \text{by Lemma 41} \\
&\leq \Pr[C[Q_0] \leq \neg[\mathrm{prove}^{\varphi}(C, \theta, S)]] & \text{by Lemma 1} \\
&\leq p(C)
\end{align*}
$$

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

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

**Example 7** Let us prove that the example $G_1$ satisfies (6). We prove the correspondence $(\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi) = (\forall x : pkey, y : host, z : nonce; \mathrm{inj-event}(e_B(x, y, z)) \Rightarrow \mathrm{inj-event}(e_A(x, y, z)))$. The program point $\mu_B$ executes $F = \mathrm{event}(e_B(x, y, z))$ and $\mathcal{F} = \theta' \mathcal{F}_{F, \mu_B} \supset \theta' \mathcal{F}_{\mu_B} \{i'_B/i_B\} \cup \{x_{pk_A}[i'_B] = x, B = y, N[i'_B] = z\}$ with $\theta' = \{i'_B/i_B\}$.

As in the proof of $\mathcal{F} \models_{\theta(\mu_B)} \mathrm{event}(e_A(x, y, z))$ in Example 6, we show $\mathcal{F} \models_{\theta(\mu_B)}^{\mathcal{I}, \mathcal{V}, \mathcal{C}} \mathrm{event}(e_A(x, y, z))$ where $\mathcal{I} = \{1 \mapsto (\mu_B, i'_B)\}$ encodes the program points and replication indices of the events of $\psi$, $\mathcal{V} = \{i'_B, x, y, z\}$ contains the replication indices of $\mathcal{F}$ and the variables of $\psi$, $\mathcal{C} = \mathcal{S} = \{(\mathcal{F}, (\mu_A, u[i'_B]), \mathcal{I}, \mathcal{V})\}$. ($\mathcal{C} = \mathcal{S}$ because the formula $\psi$ is reduced to a single event; $M'_0 = (\mu_A, u[i'_B])$ contains the program point and replication indices of the event $e_A$ contained in $\mathcal{F}: (\mu_A, u[i'_B]) : \mathrm{event}(e_A(pk_A, x_B[u[i'_B]], x_N[u[i'_B]])) \in \mathcal{F}$.)

In order to prove injectivity, it remains to show that $\vdash \mathcal{C}$. Let $\theta'' = \{i''_B/i'_B, x''/x, y''/y, z''/z\}$. We need to show that $\mathcal{F} \cup \theta''\mathcal{F} \cup \{(\mu_B, i'_B) \neq (\mu_B, i''_B), (\mu_A, u[i'_B]) = (\mu_A, u[i''_B])\}$ yields a contradiction, that is, if the pairs (program point, replication indices) of the event $e_B$ in $\psi$ are distinct $((\mu_B, i'_B) \neq (\mu_B, i''_B))$, then the pairs (program point, replication indices) of the event $e_A$ in $\phi$ are also distinct $((\mu_A, u[i'_B]) \neq (\mu_A, u[i''_B]))$.

$\mathcal{F}$ contains $N[i'_B] = x_N[u[i'_B]]$, so $\theta''\mathcal{F}$ contains $N[i''_B] = x_N[u[i''_B]]$. These two equalities combined with $u[i'_B] = u[i''_B]$ imply that $N[i'_B] = x_N[u[i'_B]] = x_N[u[i''_B]] = N[i''_B]$. Since $N$ is defined by random choices of the large type nonce, $N[i'_B] = N[i''_B]$ implies $i'_B = i''_B$ up to probability $n^2/2|\text{nonce}|$, by eliminating collisions. This equality contradicts $(\mu_B, i'_B) \neq (\mu_B, i''_B)$, so we obtain the desired injectivity. Therefore, the game $G_1$ satisfies (6) with any public variables $V$ up to probability $n^2/2|\text{nonce}|$.

# 5 Game Transformations

## 5.1 Syntactic Game Transformations

### 5.1.1 auto SArename

The transformation **auto SArename** renames all variables defined in conditions of find, so that they have distinct names. This transformation is a particular case of **SArename** (Section 5.1.7) that is particularly simple because these variables do not have array accesses by Invariant 3.

**Lemma 42** The transformation **auto SArename** requires and preserves Properties 1, 2, 3, and 4. It preserves Property 6. If transformation **auto SArename** transforms $G$ into $G'$, then $D, D_{SNU} : G, D, EvUsed \xrightarrow{V} G', D, EvUsed$ and $G'$ satisfies Property 5.
### 5.1.2 expand_tables [29]

The transformation **expand_tables** transforms **insert** and **get** into **find**, since the other transformations do not support tables. It proceeds by storing the inserted list elements in fresh array variables, and looking up in these arrays instead of performing **get**. More precisely, when **insert** Tbl($M_1, \dots, M_k$); P is under the replications $!^{i_1 \le n_1} \dots !^{i_l \le n_l}$, it is transformed into

$$ \text{let } y_1[i_1, \dots, i_l] = M_1 \text{ in } \dots \text{let } y_k[i_1, \dots, i_l] = M_k \text{ in } P $$

where $y_1, \dots, y_k$ are fresh array variables, and we add $(y_1, \dots, y_k; i_1 \le n_1, \dots, i_l \le n_l)$ in a set $S'$, to remember them. The construct **get**[unique?]** Tbl($x_1 : T_1, \dots, x_k : T_k$) such that M in P else P' is then transformed into

$$ \text{find}[\text{unique?}] \quad \left( \bigoplus_{(y_1, \dots, y_k; i_1 \le n_1, \dots, i_l \le n_l) \in S'} \left( \begin{array}{l} u_1 = i'_1 \le n_1, \dots, u_l = i'_l \le n_l \quad \text{such that} \\ \text{defined}(y_1[\tilde{i}'], \dots, y_k[\tilde{i}']) \land M\{y_1[\tilde{i}']/x_1, \dots, y_k[\tilde{i}']/x_k\} \\ \text{then let } x_1 = y_1[\tilde{u}] \text{ in } \dots \text{let } x_k = y_k[\tilde{u}] \text{ in } P \end{array} \right) \right) \\ \text{else } P' $$

where [unique?] is either [unique<sub>e</sub>] or empty and has the same value at both occurrences, $\tilde{u}$ stands for $u_1, \dots, u_l$, and $\tilde{i}'$ stands for $i'_1, \dots, i'_l$. This construct looks in all arrays used for translating insertion in table Tbl, for indices $\tilde{i}'$ such that $y_1[\tilde{i}']$, $\dots$, $y_k[\tilde{i}']$ are defined, that is, an element has been inserted at indices $\tilde{i}'$, and $M\{y_1[\tilde{i}']/x_1, \dots, y_k[\tilde{i}']/x_k\}$ is true, that is, that element satisfies M. When it finds such an element, it stores it in $x_1, \dots, x_k$, and runs P. (When it finds several elements, one of them is chosen randomly with uniform probability when [unique?] is empty and the non-unique event e is raised when [unique?] is [unique<sub>e</sub>].) When it finds no element, it executes P'. These transformations are described for processes, but similar transformations are performed for **insert** and **get** terms.

After this transformation, **expand_tables** calls **auto_SArename** to guarantee Property 5.

**Lemma 43** The transformation **expand_tables** requires and preserves Properties 1, 2, and 3. It preserves Property 6. If transformation **expand_tables** transforms G into G', then $D, D_{SNU} : G, D, EvUsed \xrightarrow{V \to_p G'} D, EvUsed$, where p is $e_{find}$ times the maximal number of executions of **get** in G that is not obviously unique (that is, such that the **insert** in that table may be executed several times), and G' satisfies Properties 4 and 5.

### 5.1.3 expand

The transformation **expand** transforms terms new, let, if, find, event, and **event_abort** into processes, so that Property 6 is guaranteed. It simplifies the generated game on the fly, using many of the rules of **simplify** (Section 5.1.21), to avoid generating branches that can actually not be executed.

After this transformation, **expand** calls **auto_SArename** to guarantee Property 5.

**Lemma 44** The transformation **expand** requires and preserves Properties 1, 2, 3, 4, and 5. If transformation **expand** transforms G into G', then $D, D_{SNU} : G, D, EvUsed \xrightarrow{V \to_p G'} D, EvUsed$, where p is an upper bound of the probability that the simplification steps modify the execution, and G' satisfies Property 6.
### 5.1.4 prove_unique

The transformation **prove_unique** tries to prove that each find[unique<sub>e</sub>] really has a unique possibility at runtime (up to a small probability), so that event *e* is executed with at most that probability. More precisely, find[unique] are already proved; find[unique<sub>e</sub>] for which no query event(*e*) ⇒ false is active are also considered as already proved (they will be proved elsewhere; with the notations of Definition 6, *e* does not occur in D<sub>1</sub> ∨ D, so *e* occurs in NonUnique<sub>Q,D<sub>1</sub> ∨D</sub>), and they are replaced with find[unique]. That corresponds to renaming event *e* to a special non-unique event that is always in NonUnique<sub>Q,D<sub>1</sub> ∨D</sub>. It remains to prove find[unique<sub>e</sub>] for which a query event(*e*) ⇒ false is active.

Suppose that $P_0 = \text{find}[\text{unique}_e] (\bigoplus_{j=1}^m \tilde{u}_j \tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j) \text{ else } P \text{ is such a find}[\text{unique}_e].$ (The same transformation is performed for find[unique<sub>e</sub>] terms.) CryptoVerif proves uniqueness by proving

* that we obtain a contradiction if the condition of a certain branch holds for two different values of the indices $\tilde{i}_j$, that is, for all $j \in \{1, \dots, m\}$, $\mathcal{F}_{P_0} \cup \{\text{defined}(M_{j1}), \dots, \text{defined}(M_{jl_j})$, $M_j$, $\text{defined}(\theta M_{j1}), \dots, \text{defined}(\theta M_{jl_j})$, $\theta M_j$, $\tilde{\tilde{i}}_j \neq \theta \tilde{\tilde{i}}_j\}$ yields a contradiction, where the substitution $\theta$ maps $\tilde{\tilde{i}}_j$ to fresh replication indices;

* and that we obtain a contradiction if the conditions of two different branches hold simultaneously, that is, for all $j, j' \in \{1, \dots, m\}$ with $j < j'$, $\mathcal{F}_{P_0} \cup \{\text{defined}(M_{j1}), \dots, \text{defined}(M_{jl_j})$, $M_j$, $\text{defined}(\theta M_{j'1}), \dots, \text{defined}(\theta M_{j'l_j})$, $\theta M_{j'}\}$ yields a contradiction, where the substitution $\theta$ maps $\tilde{\tilde{i}}_{j'}$ to fresh replication indices. (The substitution $\theta$ is useful in case the same replication indices are used in both branches $j$ and $j'$.)

When uniqueness is proved, find[unique<sub>e</sub>] is replaced with find[unique]. A subsequent call to **success** (Section 4) will remove the query event(*e*) ⇒ false when event *e* no longer occurs in the game.

**Lemma 45** *The transformation prove_unique requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation prove_unique transforms G into G', then D, D<sub>SNU</sub> : G, D, EvUsed $\xrightarrow{V_p}$ G', D, EvUsed, where p is an upper bound of the probability that some find[unique<sub>e</sub>] proved in the transformation actually executes event e.*

### 5.1.5 remove_assign [24]

The transformation **remove_assign** applied to an assignment let $x[i_1, \dots, i_l] : T = M$ in *P* replaces *x* with its value *M*. (The same transformation is performed for assignment terms.) Precisely, the transformation is performed only when *x* does not occur in *M* (non-cyclic assignment) and *M* contains only variables, function applications, and tests (otherwise, copying the definition of *x* may break the invariant that each variable is assigned at most once). When *x* has several distinct definitions, we simply replace $x[i_1, \dots, i_l]$ with *M* in *P*. (For accesses to *x* guarded by **find**, we do not know which definition of *x* is actually used.) When *x* has a single definition or several identical definitions, we replace everywhere in the game $x[M_1, \dots, M_l]$ with $M\{M_1/i_1, \dots, M_l/i_l\}$. We additionally update the **defined** conditions of **find** to preserve Invariant 2 and to make sure that, if a condition of **find** guarantees that $x[M_1, \dots, M_l]$ is defined in the initial game, then so does the corresponding condition of **find** in the transformed game. (Essentially, when $y[M'_1, \dots, M'_l]$ occurs in *M*, the transformation typically creates new occurrences of $y[M''_1, \dots, M''_l]$ for some $M''_1, \dots, M''_l$, so the condition that $y[M''_1, \dots, M''_l]$ is defined must sometimes be explicitly added to conditions of **find** in order to preserve Invariant 2.) Moreover, we replace as often as possible defined conditions $x[M_1, \dots, M_l]$ with defined conditions
$y[M_1, ..., M_l]$ where $y$ is defined at the same time as $x$. When $x \in V$, its definition is kept unchanged. Otherwise, when $x$ is not referred to at all after the transformation, we remove the definition of $x$. When $x$ is referred to only at the root of defined tests, we replace its definition with a constant. (The definition point of $x$ is important, but not its value.)

This removal of assignments is applied to all variables whose value is not used (those are used only at the root of defined conditions, or not at all). Depending on the argument of the transformation, it is also applied to other assignments:

* **findcond**: all assignments in conditions of find;

* **useless**: assignments that store a variable or a replication index, when the setting `ex-pandAssignXY` is true; otherwise, no other assignment;

* **binder** $x_1 ... x_n$: the assignments to variables $x_1, ..., x_n$.

After this transformation, **remove_assign** calls **auto_SArename** to guarantee Property 5.

With the arguments **findcond** and **useless**, this is repeated as many times as specified by the setting **maxIterRemoveUselessAssign**. Repetition stops if a fixpoint is reached.

**Lemma 46** *The transformation remove_assign requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation remove_assign transforms $G$ into $G'$, then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V} G', D, EvUsed$.*

**Example 8** In the game $G_0$ of Section 4.2.1, the transformation **remove_assign binder** $sk_A$ substitutes $skgen(rk_A)$ for $sk_A$ in the whole process and removes the assignment let $sk_A = skgen(rk_A)$. After this substitution, $sign(concat(pk_A, x_B, x_N), sk_A, r)$ becomes $sign(concat(pk_A, x_B, x_N), skgen(rk_A), r)$ thus exhibiting a term required to apply the security assumption on signatures in the cryptographic transformation of Section 5.2.

### 5.1.6 **use_variable**

The transformation **use_variable** $x_1 ... x_m$ tries to use variables $x_1, ..., x_n$ instead of recomputing their value. More precisely, at each program point that corresponds to a simple term $M$ and where $x_j[\tilde{M}]$ is guaranteed to be defined (because $x_j$ is defined above that program point or directly or indirectly because of defined conditions above that program point), if all definitions of $x_j$ that can be executed before reaching that program point are let $x_j[i] = M_0$ in, then we test whether $M$ is equal to $M_0\{\tilde{M}/i\}$ modulo the built-in equations, and if yes, we replace $M$ with $x_j[\tilde{M}]$.

The **defined** conditions of **find** above the modified program points are updated to make sure that **Invariant 2** is preserved. This is needed in particular to make sure that $x_j[\tilde{M}]$ syntactically occurs in the **defined** conditions when it is used.

**Lemma 47** *The transformation **use_variable** requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation **use_variable** transforms $G$ into $G'$, then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V} G', D, EvUsed$.*

The transformation **use_variable** is a convenient way to perform common subexpression elimination, possibly by first inserting the definition of the desired variable(s) by **insert** (Section 5.1.13). This transformation could be done by several applications of the transformation **replace** (Section 5.1.14). However, **use_variable** is easier to use when it performs the desired
replacement. For performance reasons, the equality tests performed by **use_variable** are considerably less powerful than those performed by **replace**, so if **use_variable** does not replace a term with $x_j[\tilde{M}]$ at some occurrence, it is worth trying **replace**.

### 5.1.7 SArename [24]

The transformation **SArename** $x$ (single assignment rename) aims at renaming $x$ so that distinct definitions of $x$ have different names; this is useful for distinguishing cases depending on which definition of $x$ has set $x[i]$. This transformation can be applied only when $x \notin V$. When $x$ has $m > 1$ definitions, we rename each definition of $x$ to a different variable $x_1, \dots, x_m$. Terms $x[i]$ under a definition of $x_j[i]$ are then replaced with $x_j[i]$. Each branch of find $FB = \tilde{u}[i] = i' \le \tilde{n}$ such that $\text{defined}(M'_1, \dots, M'_{l'}) \land M$ then ... where $x[M_1, \dots, M_l]$ is a subterm of some $M'_k$ for $k \le l'$ is replaced with $m$ branches $FB\{x_j[M_1, \dots, M_l]/x[M_1, \dots, M_l]\}$ for $1 \le j \le m$.

Moreover, the implementation takes into account that some variables cannot be simultaneously defined, to reduce the number of branches of find to generate.

After this transformation, **SArename** calls **auto_SArename** to guarantee Property 5.

As a particular case, **SArename random** performs the following transformation: when $y$ is defined by new $y: T$ and has $m > 1$ definitions and all variable accesses to $y$ are of the form $y[i_1, \dots, i_l]$ under a definition of $y[i_1, \dots, i_l]$, where $i_1, \dots, i_l$ are the current replication indices at this definition of $y$ (that is, $y$ has no array access using find), it renames $y$ to $y_1, \dots, y_m$ with a different name for each definition of $y$ by new $y: T$.

**Lemma 48** The transformation **SArename** requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation **SArename** transforms $G$ into $G'$, then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V} P$ $G', D, EvUsed$, where $P$ is $\epsilon_{find}$ times the maximal number of executions of a modified find that is not proved unique.

**Example 9** Consider the following process

$$ \text{start}(\AA); \text{new } k_A : T_k; \text{new } k_B : T_k; \overline{\text{yield}}(\AA); (Q_K | Q_S) $$

$$ Q_K = !^{i \le n} c[i](h : T_h, k : T_k) $$

if $h = A$ then let $k' : T_k = k_A$ in $\overline{yield}(\AA)$ else

if $h = B$ then let $k' : T_k = k_B$ in $\overline{yield}(\AA)$ else

let $k' : T_k = k$ in $\overline{yield}(\AA)$

$$ Q_S = !^{i' \le n'} c'[i'](h' : T_h); $$

find $u = i'' \le n$ such that $\text{defined}(h[i''], k'[i'']) \land h' = h[i'']$ then $P_1(k'[u])$ else $P_2$

The process $Q_K$ stores in $(h, k')$ a table of pairs (host name, key): the key for $A$ is $k_A$, for $B$, $k_B$, and for any other $h$, the adversary can choose the key $k$. The process $Q_S$ queries this table of keys to find the key $k'[u]$ of host $h'$, then executes $P_1(k'[u])$. If $h'$ is not found, it executes $P_2$.

By the transformation **SArename** $k'$, we can perform a case analysis, to distinguish the cases in which $k' = k_A$, $k' = k_B$, or $k' = k$, by renaming the three definitions of $k'$ to $k'_1$, $k'_2$, and $k'_3$ respectively. After transformation, we obtain the following processes:

$$ Q'_K = !^{i \le n} c[i](h : T_h, k : T_k) $$

if $h = A$ then let $k'_1 : T_k = k_A$ in $\overline{yield}(\AA)$ else

if $h = B$ then let $k'_2 : T_k = k_B$ in $\overline{yield}(\AA)$ else

let $k'_3 : T_k = k$ in $\overline{yield}(\AA)$
$$
\begin{align*}
Q'_S &= !^{i' \le n'} c'[i'](h' : T_h); \\
\begin{split}
\text{find } u &= i'' \le n \text{ suchthat } \begin{aligned}[t]
    \text{defined}(h[i''], k'_1[i'']) \wedge h' &= h[i''] \text{ then } P_1(k'_1[u]) \\
    \text{defined}(h[i''], k'_2[i'']) \wedge h' &= h[i''] \text{ then } P_1(k'_2[u]) \\
    \text{defined}(h[i''], k'_3[i'']) \wedge h' &= h[i''] \text{ then } P_1(k'_3[u]) \end{aligned} \text{ else } P_2
\end{split} \\
&\text{find } u = i'' \le n \text{ suchthat } \begin{aligned}[t]
    \text{defined}(h[i''], k'_1[i'']) \wedge h' &= A \text{ then } P_1(k_A) \\
    \text{defined}(h[i''], k'_2[i'']) \wedge h' &= B \text{ then } P_1(k_B) \\
    \text{defined}(h[i''], k'_3[i'']) \wedge h' &= h[i''] \text{ then } P_1(k[u]) \end{aligned} \text{ else } P_2
\end{align*}
$$

The find in $Q_S$, which looks for elements in array $k'$, is transformed in $Q'_S$ into a find with three branches, one for each new name of $k'$ ($k'_1$, $k'_2$, and $k'_3$ respectively). After the simplification (Section 5.1.21), $Q'_S$ becomes:

$$
\begin{align*}
Q_S'' &= !^{i' \le n'} c'[i'](h' : T_h); \\
\begin{split}
\text{find } u &= i'' \le n \text{ suchthat } \begin{aligned}[t]
    \text{defined}(h[i''], k'_1[i'']) \wedge h' &= A \text{ then } P_1(k_A) \\
    \text{defined}(h[i''], k'_2[i'']) \wedge h' &= B \text{ then } P_1(k_B) \\
    \text{defined}(h[i''], k'_3[i'']) \wedge h' &= h[i''] \text{ then } P_1(k[u]) \end{aligned} \text{ else } P_2
\end{split}
\end{align*}
$$

since, when $k'_1[u]$ is defined, $k'_1[u] = k_A$ and $h[u] = A$, and similarly for $k'_2[u]$ and $k'_3[u]$.

### 5.1.8 move [24]

The transformation **move** moves random choices and assignments downwards in the code as much as possible. A random choice $\mathbf{x}[\tilde{i}] : T$ or assignment let $\mathbf{x}[\tilde{i}] : T = M$ cannot be moved under a replication, or under a parallel composition when both sides use $x$, or a let let $\mathbf{y}[\tilde{i}] : T = M$ in ..., input $c[M_1, \dots, M_l](x_1[\tilde{i}] : T_1, \dots, x_k[\tilde{i}] : T_k)$, output $c[M_1, \dots, M_l]\langle N_1, \dots, N_k \rangle$ when $x$ occurs in $M, M_1, \dots, M_l, N_1, \dots, N_k$, or a find (or if) when the conditions use $x$. It can be moved under the other constructs, duplicating it if necessary, when we move it under a find (or if) that uses $x$ in several branches. Note that when the random choice $\mathbf{x}[\tilde{i}] : T$ or assignment let $\mathbf{x}[\tilde{i}] : T = M$ cannot be moved under an input, a parallel composition, or a replication, it must be written above the output that is located above the considered input, parallel composition or replication, so that the syntax of processes is not violated. When there are array accesses to $x$, the random choice $\mathbf{x}[\tilde{i}] : T$ or assignment let $\mathbf{x}[\tilde{i}] : T = M$ can be moved only inside the same output process, without moving it under an output or under a find that makes an array access to $x$.

The conditions above are necessary for the soundness of the move. Furthermore, the move is considered beneficial when it satisfies the following conditions:

* for random choices, when the random choice can be moved under a find (or if). When this transformation duplicates a $\mathbf{x}[\tilde{i}] : T$ by moving it under a find that uses $x$ in several branches, a subsequent **SArename**($x$) enables us to distinguish several cases depending in which branch $x$ is created, which is useful in some proofs.

* for assignments, when there are no array accesses to $x$, the assignment to $x$ can be moved under a find (or if), and $x$ is used in a single branch of that find (or if). In this case, the assignment can be performed only in the branch that uses $x$, so it will be computed in fewer cases thanks to the move.

The performed moves are determined by the argument of the transformation:

* **all**: moves all random choices and assignments, provided the move is beneficial.

* **noarrayref**: moves all random choices and assignments that do not have array references, provided the move is beneficial.

* **random**: moves all random choices, provided the move is beneficial.
* **random_noarrayref**: moves all random choices that do not have array references, provided the move is beneficial.

* **assign**: moves all assignments, provided the move is beneficial.

* **binder** $x_1 ... x_n$: move the variables $x_1, ..., x_n$ (even when the move is not beneficial).

In all cases, only random choices and assignments at the process level (not inside terms) are moved.

**Lemma 49** *The transformation move requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation move transforms G into G', then $D, D_{SNU} : G, D, EvUsed \xrightarrow{V} G', D, EvUsed$.*

### 5.1.9 move array [25]

The transformation **move array** $X$ delays the generation of a random value $X$ until the point at which it is first used (lazy sampling). This transformation is implemented as a particular case of a cryptographic transformation by the following equivalence:

```
!i \le n \text{new } X : T;
    (!iX \le nX \text{OX()} := \text{return}(X) | 
       !ieq \le neq \text{Oeq}(X' : T) := \text{return}(X' = X))
    \approx \#\text{Oeq}/|T| \text{ [manual]}
!i \le n
    (!iX \le nX \text{OX()} := 
       \begin{find}[unique] } j \le nX \text{ suchthat defined}(Y[j]) 
       \text{then return}(Y[j]) \text{ else new } Y : T; \text{return}(Y) | 
       !ieq \le neq \text{Oeq}(X' : T) := 
       \begin{find}[unique] } j \le nX \text{ suchthat defined}(Y[j]) 
       \text{then return}(X' = Y[j]) \text{ else return}(\text{false}))
```

where $T$ is the type of $X$. Two oracles are defined, OX and Oeq. In the left-hand side, OX returns the random $X$ itself. In the right-hand side, OX uses a lookup to test if the random value was already generated; if yes, it returns the previously generated random value $Y[j]$; if no, it generates a fresh random value $Y$. Transforming the left-hand side into the right-hand side therefore moves the generation of the random number $X$ to the first call to OX, that is, the first usage of $X$. The oracle Oeq provides an optimized treatment of equality tests $X' = X$: when the random value $X$ was not already generated, we return false instead of generating a fresh $X$, so we exclude the case that $X'$ is equal to a fresh $X$. This case has probability $1/|T|$ for each call to Oeq, so the probability of distinguishing the two games is $\#\text{Oeq}/|T|$. (Notice that there never exist several choices of $j$ that satisfy the conditions of the finds in the right-hand side of this equivalence, so these finds can be marked [unique] without modifying their behavior.)

### 5.1.10 move up

The transformation **move up** $x_1 ... x_n$ to $\mu$ moves the random number generations or assignments of $x_1, ..., x_n$ upwards in the syntax tree, to the program point $\mu$. This program point must correspond to an output process.

The program point $\mu$ is an integer, which can be determined using the command **show game occ**: this command displays the current game with the corresponding label $\{\mu\}$ at each program
point. The command **show-game occ** also allows one to inspect the game, for instance to
know the names of fresh variables created by CryptoVerif during previous transformations. Pro-
gram points and variable names may depend on the version of CryptoVerif. Since CryptoVerif
version 2.01, program points can also be designated by expressions like **before regexp**, which
designates the program point at the beginning of the line that matches the regular expression
*regexp*; **after regexp**, which designates the program point just after the line that matches regexp;
**before nth n regexp**, which designates the program point at the beginning of the *n*-th line that
matches the regular expression regexp; **after nth n regexp**, which designates the program point
at the beginning of the first line that has an occurrence number after the *n*-th line that matches
the regular expression regexp; **at n' regexp**, which designates the program point at the *n'*-th oc-
currence number that occurs inside the string that matches the regular expression regexp in the
displayed game; **at nth n' regexp**, which designates the program point at the *n'*-th occurrence
number that occurs inside the string corresponding to the *n*-th match of the regular expression
regexp in the displayed game. This way of designating program points is more stable across
versions of CryptoVerif.

After the game transformation, a variable *x* is defined at program point *μ*, and all other variables *x*<sub>*k*</sub> are defined by let *x*<sub>*k*</sub> = *x* in. The variable *x* is a variable *x*<sub>*k*</sub> itself when *x*<sub>*k*</sub> has no array accesses and the current replication indices at the definition of *x*<sub>*k*</sub> are the same as at *μ*. Otherwise, the variable *x* is a fresh variable.

All variables $x_1, \dots, x_n$ must have the same type. They must not be defined syntactically above the program point $\mu$. The definitions of the variables $x_1, \dots, x_n$ must be in distinct branches of if, find, let, so that they cannot be simultaneously defined. Either all variables $x_1, \dots, x_n$ must be defined by random number generations or all of them must be defined by assignments.

* If $x_1, \dots, x_n$ are defined by random number generations, this transformation performs eager sampling of $x_i$. The random number generation of $x_1, \dots, x_n$ must be executed at most once for each execution of program point $\mu$. This is proved by combining that the definitions of the variables $x_1, \dots, x_n$ are in distinct branches of if, find, let with the fact that each of these definitions (at $\mu_j$) is executed at most once for each value of the current replication indices at $\mu$. To show the latter fact, we notice that, since $\mu_j$ is syntactically under $\mu$, the current replication indices at $\mu$ are a prefix of the replication indices at $\mu_j$. If the replication indices at $\mu_j$ are the same as at $\mu$, then the fact is proved. Otherwise, the replication indices at $\mu_j$ are $\tilde{i}, \tilde{i}_j$ while the replication indices at $\mu$ are $\tilde{i}$ and we show that $\mathcal{F}_{\mu_j} \cup \mathcal{F}_{\mu_j}\{\tilde{i}'_j/\tilde{i}_j\} \cup \{\tilde{i} \neq \tilde{i}'_j\}$ yields a contradiction, where $\tilde{i}'_j$ are fresh replication indices.

* If $x_1, \dots, x_n$ are defined by assignments of terms $M_j$, then all $M_j$ must consist of variables, function applications, and tests; there must be one $M_j$ defined at program point $\mu$, using all defined variables collected in $\mathcal{F}_{\mu}$ (let $M_{j_0}$ be that $M_j$, which will be used as the definition of $x$: let $x = M_{j_0}$ in); and all terms $M_j$ must be equal: for all $j \neq j_0$, $M_j = M_{j_0}$ knowing the facts $\mathcal{F}_{\mu_j}$ that hold at the program point $\mu_j$ of $M_j$.

The *defined* conditions of *find* above $\mu$ are updated to syntactically guarantee the definition of $M_{j_0}$, as required by Invariant 2.

**Lemma 50** *The transformation move up requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6. If transformation move up transforms G into G', then D, D<sub>SNU</sub>: G, D, EvUsed $\xrightarrow{V}$<sub>p</sub> G', D, EvUsed, where p is an upper bound of the probability of collisions eliminated in the proof that each $\mu_j$ is executed at most once for each execution of $\mu$ or that for all $j \neq j_0$, $M_j = M_{j_0}$.*
### 5.1.11 move_if fun

The transformation **move_if fun** moves the predefined function **if fun** or transforms it into a term if ... then ... else... It supports the following variants:

* **move_if fun** loc₁...locₙ, where each locⱼ is either a program point or a function symbol. When locⱼ is a program point, it moves occurrences of **if fun** from inside the term at that program point to the root of that term. (The program point μ is designated as explained in Section 5.1.10.) When locⱼ is a function symbol, it moves occurrences of **if fun** from under that function symbol to just above it. The move corresponds to rewriting C[**if fun**(*M*₁, *M*₂, *M*₃)] into **if fun**(*M*₁, C[*M*₂], C[*M*₃]), where C is a term context built from the following grammar:

<table><tr><td>C ::=</td><td>simple term context</td></tr><tr><td>[]</td><td>hole</td></tr><tr><td>x[*M*₁, ..., *M*<sub>*k*−₁</sub>, C, *M*<sub>*k*+₁</sub>, ..., *M*<sub>*m*</sub>]</td><td>variable</td></tr><tr><td>f(*M*₁, ..., *M*<sub>*k*−₁</sub>, C, *M*<sub>*k*+₁</sub>, ..., *M*<sub>*m*</sub>)</td><td>function application</td></tr></table>

and the root of C corresponds to a locⱼ. (It is at program point locⱼ when locⱼ is a program point; its root symbol is locⱼ when locⱼ is a function symbol.) These moves are possible only when C is a simple term context, since otherwise they might lead to defining several times the same variable or repeating events since the context C is duplicated in the second and third arguments of **if fun** and **if fun** evaluates all its arguments. For simplicity, we allow them only when C[**if fun**(*M*₁, *M*₂, *M*₃)] is a simple term.

* **move_if fun** level *n*, where *n* is a positive integer, moves occurrences of **if fun** *n* function symbols up in the syntax tree (provided those **if fun** occur under at least *n* function symbols). As above, these moves are allowed only when they occur inside a simple term.

* **move_if fun** to term μ₁...μₙ transforms terms **if fun**(*M*₁, *M*₂, *M*₃) that occur at program points μ₁, ..., μₙ into terms if *M*₁ then *M*₂ else *M*₃. When no program point is given, it performs that transformation everywhere in the game.

When *M*₂ and *M*₃ have a visible effect, that is, they define some variable with array accesses (including by their usage in various kinds of secrecy queries) or they execute events, the transformation above would not be correct, because **if fun**(*M*₁, *M*₂, *M*₃) evaluates both *M*₂ and *M*₃ while if *M*₁ then *M*₂ else *M*₃ evaluates either *M*₂ or *M*₃. In this case, we transform **if fun**(*M*₁, *M*₂, *M*₃) into let *xcond* = *M*₁ in let *xthen* = *M*₂ in let *xelse* = *M*₃ in if *xcond* then *xthen else xelse* to make sure that *M*₁, *M*₂, and *M*₃ are always evaluated, and in that order.

When **autoExpand** = true (the default), a call to **expand** is automatically performed after **move_if fun**, which transforms the terms let ... = ... in ... and if ... then ... else ... into processes.

**Lemma 51** The transformation **move_if fun** requires and preserves Properties 1, 2, 3, 4, and 5. The variants **move_if fun** loc₁...locₙ and **move_if fun** level *n* preserve Property 6. If transformation **move_if fun** transforms G into G', then D, D<sub>SNU</sub>: G, D, EvUsed $\xrightarrow{V}$₀ G', D, EvUsed.
### 5.1.12 insert_event [25]

The transformation **insert_event** $e \mu$ inserts **event_abort** $e$ at program point $\mu$. (The program point $\mu$ is designated as explained in Section 5.1.10.)

The transformation **insert_event** $e \mu$ also adds to query **event**(e) ⇒ false in order to bound the probability of event e.

**Lemma 52** *The transformation insert_event requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6 if the event is inserted at the process level. If transformation insert_event $e \mu$ transforms G into $G'$, then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V} e_0 G', D \lor e, EvUsed \cup \{e\}$.*

### 5.1.13 insert [25]

The transformation **insert** $\mu$ **ins** adds instruction **ins** at the program point $\mu$. The program point $\mu$ is designated as explained in Section 5.1.10. The instruction **ins** can for instance be a test, in which case all branches of the test will be copies of the code that follows program point $\mu$ (so that the semantics of the game is unchanged). It can also be an assignment or a random generation of a fresh variable or an **event_abort** instruction. In all cases, CryptoVerif checks that this instruction preserves the semantics of the game except when we execute an inserted Shoup event, and rejects it with an error message if it does not.

After this transformation, **insert** calls **auto_SAname** to guarantee Property 5.

When the user inserts **event_abort** $e$, the transformation **insert** adds a query **event**(e) ⇒ false in order to bound the probability of event e.

When the user inserts a **find[unique_e]** (the user actually types **find[unique]** but CryptoVerif automatically generates a fresh event e and inserts **find[unique_e]** instead, since uniqueness is not proved yet), the transformation **insert** adds a query **event**(e) ⇒ false and calls **prove_unique** (Section 5.1.4) in order to try proving uniqueness.

**Lemma 53** *The transformation insert requires and preserves Properties 1, 2, 3, 4, 5, and 6. If transformation insert transforms G into $G'$, then $D, D_{SNU}: G, D, EvUsed \xrightarrow{V} e_0 G', D \lor e_1 \lor \dots \lor e_m, EvUsed \cup \{e_1, \dots, e_m\}$ where $e_1, \dots, e_m$ are the events in the inserted instruction (**event_abort** $e_j$, **find[unique_e]**) and the probability p comes from **prove_unique**.*

### 5.1.14 replace

The transformation **replace** $\mu M$ replaces the term $M_0$ at program point $\mu$ with the term $M$. ($M_0$ and $M$ must be simple. The program point $\mu$ is designated as explained in Section 5.1.10.) Before performing the replacement, it checks that $M$ is equal to $M_0$ at that program point (up to a small probability): first, it collects all facts $\mathcal{F}_{\mu}$ that hold at program point $\mu$; second, it tests equality between $M_0$ and $M$ using $\mathcal{F}_{\mu}$ and built-in equations (it uses equalities inferred from $\mathcal{F}_{\mu}$ to replace variables with their values, trying to make the terms equal); third, it simplifies $M_0$ and $M$ using user-defined rewrite rules of Section 3.1, and tests equality between the results using $\mathcal{F}_{\mu}$ and built-in equations; fourth, it rewrites $M_0$ and $M$ at most **maxReplaceDepth** times using equalities inferred from $\mathcal{F}_{\mu}$ and user-defined rewrite rules of Section 3.1, until it finds a common term modulo the built-in equations. The transformation is performed as soon as the equality between $M_0$ and $M$ is proved.

The defined conditions of **find** above the program point $\mu$ are updated to make sure that Invariant 2 is preserved. This is needed in particular when $M$ makes array accesses that $M_0$ does not make.
### 5.1.16 merge-arrays [25]

The transformation **merge-arrays** $x_{11} ... x_{1n}, ..., x_{m1} ... x_{mn}$ merges the variables $x_{j1}, ..., x_{jn}$ into a single variable $x_{j1}$ for each $j \le m$. Each variable $x_{jk}$ must have a single definition. For each $j \le n$, the variables $x_{j1}, ..., x_{jn}$ must have the same type and indices of the same type. They must not be defined for the same value of their indices (that is, $x_{jk}$ and $x_{jk'}$ must be defined in different branches of if or find when $k \neq k'$). The arrays $x_{j1}, ..., x_{jn}$ are merged into a single array $x_{j1}$ for each $j \le m$. The transformation proceeds as follows:

* If, for each $k \le n$, $x_{1k}$ is defined above $x_{jk}$ for all $1 < j < m$, we introduce a fresh variable $b_k$ defined by $b_k \leftarrow$ mark just after the definition of $x_{1k}$. We call $b_k$ a branch variable; it is used to detect that $x_{jk}$ has been defined: $x_{jk}[\tilde{M}]$ is defined before the transformation if and only if $x_{j1}[\tilde{M}]$ and $b_k[\tilde{M}]$ are defined after the transformation, and $x_{j1}[\tilde{M}]$ after the transformation is equal to $x_{jk}[\tilde{M}]$ before the transformation.

* For each find that requires that some variables $x_{jk}$ are defined, we leave the branches that do not require the definition of $x_{jk}$ unchanged and we try to transform the other branches $FB_l = (\tilde{u}_l = \tilde{i}_l \le \tilde{n}_l \text{ suchthat } \text{defined}(\tilde{M}_l) \land M_l \text{ then } P_l)$ as follows.

1. We require that, for each $l$, there exists a distinct $k$ such that the defined condition of $FB_l$ refers to $x_{jk}$ for some $j$ but not to $x_{jk'}$ for any other $k'$. (Otherwise, the transformation fails.) We denote by $l(k)$ the value of $l$ that corresponds to $k$.

2. We choose a "target" branch $FB_T = (\tilde{u} = \tilde{i} \le \tilde{n} \text{ suchthat } \text{defined}(\tilde{M}) \land M \text{ then } P)$: if the defined condition of some branch $FB_l$ refers to $x_{j1}$ for some $j$, we choose that branch $FB_l$. Otherwise, we choose any branch $FB_l$ and rename its variables $x_{jk}$ to $x_{j1}$. We require that the references $x_{j1}[\tilde{M}]$ to the variables $x_{j1}$ in the defined condition of the target branch all have the same indices $\tilde{M}$. If the transformation succeeds, we will replace all branches $FB_l$ with the target branch.

3. The branch $FB_T$ after transformation is equivalent to branches $\bigoplus_{k=1}^n FB_T\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ before transformation. We show that these branches are equivalent to the branches $FB_l$.

For each $k \le n$,

- if $l(k)$ exists, then we show that $FB_T\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ is equivalent to $FB_{l(k)}$. Let $l = l(k)$. We first rename the variables $\tilde{u}_l$ of $FB_l$ to the variables $\tilde{u}$ of the target branch. For simplicity, we still denote by $FB_l = (\tilde{u}_l = \tilde{i}_l \le \tilde{n}_l \text{ suchthat } \text{defined}(\tilde{M}_l) \land M_l \text{ then } P_l)$ the obtained branch. Then we show that, if the variables of $\tilde{M}_l$ are defined, then the variables of $\tilde{M}\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ are defined, and conversely; $M_l = M\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ (knowing the equalities that hold at that program point), and $P_l$ and $P\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ execute the same code up to renaming of variables defined in $P_l$ or $P\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ and that do not have array accesses, and up to equality of terms proved using facts $F_\mu$ that hold at the program point $\mu$ of the considered find.

- if $l(k)$ does not exist, then we show that $FB_T\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ can in fact not be executed, because its condition cannot hold: the variables of $\tilde{M}\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ cannot be simultaneously defined or $M\{x_{jk}/x_{j1}, j = 1, \dots, m\}$ cannot hold.

If the transformation above fails and we have introduced branch variables, we replace each condition defined($x_{jk}$[$\tilde{M}$]) with defined($x_{j1}$[$\tilde{M}$], $b_k$[$\tilde{M}$]).
If the transformation above fails and we have not introduced branch variables, the whole **merge arrays** transformation fails.

* The definition of $x_{jk}$ is renamed to $x_{j1}$ and each reference to $x_{jk}[\tilde{M}]$ is renamed to $x_{j1}[\tilde{M}]$.

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

### 5.1.17 guess $i$

When **guessRemoveUnique** = true and some (one-session) secrecy queries are present, the transformation **guess** $i$ first transforms the game $G$ into $G_{RU}$, by replacing all proved find[unique] with find. Lemma 57 shows the soundness of this preliminary transformation. It may be advantageous for (one-session) secrecy proofs because the removed find[unique] do not need to be proved, while the remaining ones must be reproved after the transformation, as we show below.

**Lemma 57** Let $G_{RU}$ be the game obtained from $G$ by replacing all proved find[unique] with find. Let sp be a security property (sp is 1-ses.secr.(x), Secrecy(x), bit secr.(x), or a correspondence $\varphi$, which does not use $\bar{S}$, $\bar{S}$, nor non-unique events). Let $D$ be a disjunction of Shoup events and a subset of non-unique events $e_i$ corresponding to unproved find[unique] in $G$ ($D$ does not contain $S$ nor $\bar{S}$). If $\text{Bound}_{G_{RU}}(V, sp, D, p)$, then $\text{Bound}_G(V, sp, D, p)$.

**Proof** Let $C'$ be an evaluation context acceptable for $C_{sp}[G]$ with public variables $V \setminus V_{sp}$ that does not contain events used by sp or D nor non-unique events in G. Let $C = C'[C_{sp}[]]$. The context $C'$ is also acceptable for $C_{sp}[G_{RU}]$ with public variables $V \setminus V_{sp}$, and a fortiori does not contain non-unique events in $G_{RU}$. Since $\text{Bound}_{G_{RU}}(V, sp, D, p)$, we have $\text{Adv}_{G_{RU}}(C, sp, D) \le p(C)$.

First case: sp is a correspondence $\varphi$. We have

$$ \begin{aligned} \text{Adv}_G(C, sp, D) &= \Pr[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D}] \\ &\le \Pr[C[G_{RU}] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G_{RU},D}] = \text{Adv}_{G_{RU}}(C, sp, D) \end{aligned} $$

because traces of $G$ that satisfy $(\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D}$ correspond to similar traces of $G_{RU}$ that satisfy $(\neg\varphi \lor D) \land \neg\text{NonUnique}_{G_{RU},D}$. Only traces that satisfy $e$ for some proved find[unique] in $G$ are mapped to different traces in $G_{RU}$. These traces satisfy $\text{NonUnique}_{G,D}$.

Second case: sp is 1-ses.secr.(x), Secrecy(x), or bit secr.(x). We have

$$ \Pr[C[G] : S \lor D] \le \Pr[C[G_{RU}] : S \lor D] $$

since the traces of $C[G]$ that execute an event in $S \lor D$ correspond to similar traces of $C[G_{RU}]$ that also execute an event in $S \lor D$ ($S \lor D$ does not contain any proved non-unique event of $G$), and

$$ \Pr[C[G_{RU}] : \bar{S} \lor \text{NonUnique}_{G_{RU},D}] \le \Pr[C[G] : \bar{S} \lor \text{NonUnique}_{G,D}] $$

since the traces of $C[G_{RU}]$ that execute $\bar{S}$ or an event in $\text{NonUnique}_{G_{RU},D}$ correspond to either to similar traces of $C[G]$ that execute the same event or to traces that execute a proved non-unique event in $C[G]$, so an event in $\text{NonUnique}_{G,D}$. Therefore,

$$ \begin{aligned} \text{Adv}_G(C, sp, D) &= \Pr[C[G] : S \lor D] - \Pr[C[G] : \bar{S} \lor \text{NonUnique}_{G,D}] \\ &\le \Pr[C[G_{RU}] : S \lor D] - \Pr[C[G_{RU}] : \bar{S} \lor \text{NonUnique}_{G_{RU},D}] = \text{Adv}_{G_{RU}}(C, sp, D). \end{aligned} $$
In both cases, we obtain $Adv_G(C, sp, D) \le p(C)$ and $Bound_G(V, sp, D, p)$.

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

Next, the main guessing transformation is performed. The transformation **guess** $i$ consists in guessing the tested session of a principal in a protocol, which is a step frequently done in cryptographic proofs. In CryptoVerif, we consider a game $G$ and define a transformed game $G'$ by guessing a replication index $i$: we replace $!^{i \le n} Q$ with $!^{i \le n} Q'$ where $Q'$ is obtained from $Q$ by replacing the processes $P$ under the first inputs with if $i = i_{\text{tested}}$ then $P'$ **else** $P''$ and $i_{\text{tested}}$ is a constant. The constant $i_{\text{tested}}$ is the index of the tested session. We distinguish the process executed in the tested session, $P'$, on which we are going to prove security properties, from the process $P''$ for other sessions which are executed, but for which we do not prove security properties. (In case **diff\_constants** = **true**, the constant $i_{\text{tested}}$ must not be considered different from other constants of the same type.) The process $P'$ is obtained from $P$ by

* duplicating all events: $\text{event } e(\tilde{M})$ is replaced with $\text{event } e(\tilde{M})$; $\text{event } e'(\tilde{M})$ and similarly $\text{event\_abort } e$ is replaced with $\text{event } e$; $\text{event\_abort } e'$. We require that in the game $G$, the same event $e$ cannot occur both under the modified replication $!^{i \le n} Q$ and elsewhere in the game. (Otherwise, queries that use $e$ are left unchanged.)

* duplicating definitions of every variable $x$ used in queries for secrecy and one-session secrecy: let $x' = x$ in is added after each definition of $x$. We require that in the game $G$, the same variable $x$ used in queries for secrecy or one-session secrecy cannot be defined both under the modified replication $!^{i \le n} Q$ and elsewhere in the game. (Otherwise, the considered query is left unchanged.)

The process $P''$ is obtained from $P$ by duplicating definitions of every variable $x$ used in queries for secrecy (not one-session secrecy): let $x'' = x$ in is added after each definition of $x$.

We replace variables $x$ in secrecy and one-session secrecy queries with their duplicated version $x'$. For secrecy queries, the duplicated version $x''$ is added to public variables. In both cases, we prove (one-session) secrecy for the variable $x'$ defined in the tested session. In case of one-session secrecy, that is enough: it shows that $x'$ is indistinguishable from a random value, and that proves one-session secrecy of $x$ for all sessions by symmetry. However, for secrecy, we additionally want to show that the values of $x$ in the various sessions are independent of each other; this is achieved by considering the value of $x$ in sessions other than the tested session (that is, $x''$) as public: if $x'$ is indistinguishable from random even when $x''$ is public, then $x'$ is independent of $x''$.

In non-injective correspondence queries, we replace one non-injective event $e$ before the arrow $\Rightarrow$ with its duplicated version $e'$. Hence, we prove the query for the tested session, which uses event $e'$. The proof is valid for all sessions by symmetry.

The probability of attack must basically be multiplied by $n$ for all modified queries. The proof depends on the considered query and is detailed below.

For queries that are left unchanged, i.e. secrecy and one-session secrecy queries for variables not defined under the modified replication, non-injective correspondence queries with no event before the arrow $\Rightarrow$ under the modified replication (the previous queries prove properties about other roles than the one for which we guess the tested session), bit secrecy queries (because the secret is defined under no replication, so it is not under the guessed replication), as well as injective correspondence queries (see details below), the probability is unchanged. It is clear that these queries are not affected by the transformation.

After this transformation, **guess** calls **auto_SArename** to guarantee Property 5.

**Lemma 58** *The transformation guess $i$ requires and preserves Properties 1, 2, 3, 4, and 5. It preserves Property 6.*
Suppose the game G is transformed into G' by the transformation guess i, where i is a replication index bounded by n. Below, we consider only the modified queries.

Let $\varphi$ and $\varphi'$ be respectively the semantics of a non-injective correspondence and its transformed correspondence. If $\text{Bound}_{G'}(V, \varphi', D_{\text{false}}, p)$ and $p$ is independent of the value of $i_{\text{tested}}$, then $\text{Bound}_G(V, \varphi, D_{\text{false}}, np)$.

If $G'$ satisfies the one-session secrecy of $x'$ with public variables $V$ ($x, x', x'' \notin V$) up to probability $p$ and $p$ is independent of the value of $i_{\text{tested}}$, then $G$ satisfies the one-session secrecy of $x$ with public variables $V$ up to probability $np$.

If $G'$ satisfies the secrecy of $x'$ with public variables $V \cup \{x''\}$ ($x, x', x'' \notin V$) up to probability $p$ and $p$ satisfies Property 7, then $G$ satisfies the secrecy of $x$ with public variables $V$ up to probability $n \times p$ (neglecting a small additional runtime of the context).

If $\text{Bound}_{G'}(V \cup \{x'\}, 1\text{-ses.secr}(x'), \text{NonUnique}_{G'}, p)$ and $p$ satisfies Property 7, then we have $\text{Bound}_G(V \cup \{x\}, 1\text{-ses.secr}(x), D_{\text{false}}, np)$.

If $\text{Bound}_{G'}(V \cup \{x', x''\}, \text{Secrecy}(x'), \text{NonUnique}_{G'}, p)$ and $p$ satisfies Property 7, then we have $\text{Bound}_G(V \cup \{x\}, \text{Secrecy}(x), D_{\text{false}}, np)$ (neglecting a small additional runtime of the context).

Property 7 guarantees that $p$ is independent of the value of $i_{\text{tested}}$, as well as other independence conditions needed for secrecy and for the properties on **Bound** because we modify the context in the proof. Since the third argument of **Bound** is always $D_{\text{false}}$ in the conclusion of Lemma 58, we cannot use the optimization of considering the disjunction of several properties simultaneously, as outlined in Section 2.7.4: we must consider each property and event separately. Indeed, if we applied guessing to several properties at once, we might need to guess the tested session for each property, which would introduce several factors $n$. Since the third argument of **Bound** is $\text{NonUnique}_{G'}$ in the hypothesis of Lemma 58 for (one-session) secrecy properties, uniqueness of find[unique$_e$] must be reproved in game $G'$ after the guess transformation (that is, the probability that these find[unique$_e$] have several successful choices must be bounded again in $G'$).

## Proof

**Non-injective correspondences** We suppose that the events under the transformed replication contain as argument the replication index $i$ of that replication. (CryptoVerif implicitly adds the current program point and replication indices to each event, and uses fresh distinct variables for the added replication indices in the queries. That does not change the meaning of the query.)

Let $\forall i_0 : [1, n], \tilde{x} : \tilde{T}; \text{event}(e(\tilde{M})) \wedge \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ be the initial query and $\forall i_0 : [1, n], \tilde{x} : \tilde{T}; \text{event}(e'(\tilde{M})) \wedge \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ be the transformed query, where $\{i_0, \tilde{x}\} = \text{var}(\text{event}(e'(\tilde{M})) \wedge \psi)$, $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\text{event}(e'(\tilde{M})) \wedge \psi)$, and $i_0$ be the variable for the index of the transformed replication in $\tilde{M}$.

Let $C$ be an evaluation context acceptable for $G$ with public variables $V$ that does not contain events used by $\varphi$.

$$
\begin{align*}
\text{Adv}_G(C, \varphi, D_{\text{false}}) &= \text{Pr}[C[G] : \neg\varphi \wedge \neg\text{NonUnique}_G] \\
&= \text{Pr} \left[ C[G] : (\exists i_0 \in [1, n], \exists \tilde{x} \in \tilde{T}, \text{event}(e(\tilde{M})) \wedge \psi \wedge \neg\exists \tilde{y} \in \tilde{T}', \phi) \wedge \neg\text{NonUnique}_G \right] \\
&= \sum_{i_{\text{val}}=1}^{n} \text{Pr} \left[ C[G] : (\exists i_0 \in [1, n], \exists \tilde{x} \in \tilde{T}, i_0 = i_{\text{val}} \wedge \text{event}(e(\tilde{M})) \wedge \psi \wedge \neg\exists \tilde{y} \in \tilde{T}', \phi) \wedge \neg\text{NonUnique}_G \right] \\
&= \sum_{i_{\text{val}}=1}^{n} \text{Pr} \left[ C[G'] : (\exists i_0 \in [1, n], \exists \tilde{x} \in \tilde{T}, \text{event}(e'(\tilde{M})) \wedge \psi \wedge \neg\exists \tilde{y} \in \tilde{T}', \phi) \wedge \neg\text{NonUnique}_{G'} \right] \quad \text{for } i_{\text{tested}} = i_{\text{val}}
\end{align*}
$$

Inria
$$ = \sum_{i_{\text{val}}=1}^{n} \text{Adv}_{G'}(C, \varphi', D_{\text{false}}) \text{ for } i_{\text{tested}} = i_{\text{val}} $$

Since $\text{Bound}_{G'}(V, \varphi', D_{\text{false}}, p)$, we have $\text{Adv}_{G'}(C, \varphi', D_{\text{false}}) \le p(C)$ and the probability $p$ is independent of the value of $i_{\text{tested}}$, so we obtain $\text{Adv}_G(C, \varphi, D_{\text{false}}) \le n \times p(C)$. Therefore $\text{Bound}_G(V, \varphi, D_{\text{false}}, np)$.

**One-session secrecy** Let $C$ be an evaluation context acceptable for $C_{1-\text{ses.secr.}}(x)[G]$ with public variables $V$ that does not contain $S$ nor $\bar{S}$. Suppose that the modified replication corresponds to the $j$-th index of variable $x$. We have

$$ \begin{aligned} \text{Adv}_G^{1-\text{ses.secr.}}(x)(C) &= \Pr[C[C_{1-\text{ses.secr.}}(x)[G]] : S] - \Pr[C[C_{1-\text{ses.secr.}}(x)[G]] : \bar{S} \\ &= \sum_{v=1}^{n} \Pr[C[C_{1-\text{ses.secr.}}(x)[G]] : S \wedge u_j = v] \\ &\quad - \Pr[C[C_{1-\text{ses.secr.}}(x)[G]] : \bar{S} \wedge u_j = v] \\ &= \sum_{v=1}^{n} \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : S \wedge u_j = v] \\ &\quad - \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : \bar{S} \wedge u_j = v] \quad \text{for } i_{\text{tested}} = v \end{aligned} $$

because in $G'$ with $i_{\text{tested}} = v$, $x'[u_1, \dots, u_m] = x[u_1, \dots, u_m]$ when $u_j = v$, so $C_{1-\text{ses.secr.}}(x)[G]$ behaves like $C_{1-\text{ses.secr.}}(x') [G']$ (the events added in $G'$ are not used).

Moreover, $\Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : S \wedge (u_j \text{ not defined} \lor u_j \neq v)] = \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : \bar{S} \wedge (u_j \text{ not defined} \lor u_j \neq v)]$ when $i_{\text{tested}} = v$. Indeed, when $u_j$ is not defined or $u_j \neq v = i_{\text{tested}}$, the query on $c_s$ either is not executed or always yields, independently of the value of $b$. Hence, changing the value of $b$ just swaps the events $S$ and $\bar{S}$. So

$$ \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : S \wedge (u_j \text{ not defined} \lor u_j \neq v) \wedge b = \text{true}] = \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : \bar{S} \wedge (u_j \text{ not defined} \lor u_j \neq v) \wedge b = \text{false}] $$

$$ \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : \bar{S} \wedge (u_j \text{ not defined} \lor u_j \neq v) \wedge b = \text{true}] = \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : S \wedge (u_j \text{ not defined} \lor u_j \neq v) \wedge b = \text{false}. $$

We obtain the announced result by swapping the two sides of the second equality and adding the first equality to it. (The variable $b$ is always defined when $S$ or $\bar{S}$ is executed.)

Therefore,

$$ \begin{aligned} \text{Adv}_G^{1-\text{ses.secr.}}(x)(C) &= \sum_{v=1}^{n} \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : S] - \Pr[C[C_{1-\text{ses.secr.}}(x') [G')] : \bar{S}] \quad \text{for } i_{\text{tested}} = v \\ &= \sum_{v=1}^{n} \text{Adv}_{G'}^{1-\text{ses.secr.}}(x') (C) \quad \text{for } i_{\text{tested}} = v \end{aligned} $$

Since $G'$ satisfies the one-session secrecy of $x'$ with public variables $V$ up to probability $p$, we have $\text{Adv}_{G'}^{1-\text{ses.secr.}}(x') (C) \le p(C)$ and the probability $p$ is independent of the value of $i_{\text{tested}}$, so we obtain $\text{Adv}_G^{1-\text{ses.secr.}}(x)(C) \le n \times p(C)$. Therefore, $G$ satisfies the one-session secrecy of $x$ with public variables $V$ up to probability $np$.

**Secrecy** Let $C$ be an evaluation context acceptable for $C_{\text{Secrecy}}(x)[G]$ with public variables $V$ that does not contain $S$ nor $\bar{S}$. Suppose that the modified replication corresponds to the $j$-th
index of variable $x$. We have

$$ \begin{aligned} \mathrm{Adv}_G^{\mathrm{Secrecy}(x)}(C) &= \frac{1}{2} \left( \begin{array}{l} \Pr[C[G \mid Q_{\mathrm{Secrecy}(x)}] : \mathcal{S} \mid b = \text{true}] + \Pr[C[G \mid Q_{\mathrm{Secrecy}(x)}] : \mathcal{S} \mid b = \text{false}] \\ - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x)}] : \bar{\mathcal{S}} \mid b = \text{true}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x)}] : \bar{\mathcal{S}} \mid b = \text{false}] \end{array} \right) \end{aligned} $$

Let

$$ \begin{aligned} Q_{\mathrm{Secrecy}(x), \mathrm{real}} &= c_{s0}(\overline{c_{s0}}\langle\rangle; \\ & \quad (!^{i_s \le n_s} c_s[i_s](u_1 : [1, n_1], \dots, u_m : [1, n_m]); \text{if defined}(x[u_1, \dots, u_m]) \text{ then} \\ & \quad \overline{c_s[i_s]}\langle x[u_1, \dots, u_m] \rangle \\ & \quad | c'_s(b' : \mathit{bool}); \text{if } b' \text{ then event\_abort } S \text{ else event\_abort } \bar{S}) \end{aligned} $$

$$ \begin{aligned} Q_{\mathrm{Secrecy}(x), \mathrm{random}} &= c_{s0}(\overline{c_{s0}}\langle\rangle; \\ & \quad (!^{i_s \le n_s} c_s[i_s](u_1 : [1, n_1], \dots, u_m : [1, n_m]); \text{if defined}(x[u_1, \dots, u_m]) \text{ then} \\ & \quad \begin{aligned}[t] \text{find } u'_s &= i'_s \le n_s \quad &\text{suchthat } \overline{\mathrm{defined}}(y[i'_s], u_1[i'_s], \dots, u_m[i'_s]) \\ & \quad \wedge u_1[i'_s] = u_1 \wedge \dots \wedge u_m[i'_s] = u_m \\ & \quad \text{then } \overline{c_s[i_s]}\langle y[u'_s] \rangle \\ & \quad \text{else new } y : T; \overline{c_s[i_s]}\langle y \rangle \\ & \quad | c'_s(b' : \mathit{bool}); \text{if } b' \text{ then event\_abort } S \text{ else event\_abort } \bar{S} \end{aligned} \end{aligned} $$

Then

$$ \mathrm{Adv}_G^{\mathrm{Secrecy}(x)}(C) = \frac{1}{2} \left( \begin{array}{l} \Pr[C[G \mid Q_{\mathrm{Secrecy}(x), \mathrm{real}}] : \bar{\mathcal{S}}] + \Pr[C[G \mid Q_{\mathrm{Secrecy}(x), \mathrm{random}}] : \bar{\mathcal{S}}] \\ - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x), \mathrm{real}}] : \bar{\mathcal{S}}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x), \mathrm{random}}] : \bar{\mathcal{S}}] \end{array} \right) $$

Let

$$ \begin{aligned} Q_{\mathrm{Secrecy}(x),v} &= c_{s0}(\overline{c_{s0}}\langle\rangle; \\ & \quad (!^{i_s \le n_s} c_s[i_s](u_1 : [1, n_1], \dots, u_m : [1, n_m]); \text{if defined}(x[u_1, \dots, u_m]) \text{ then} \\ & \quad \begin{aligned}[t] \text{if } u_j \le v \text{ then } \overline{c_s[i_s]}\langle x[u_1, \dots, u_m] \rangle \text{ else} \\ \text{find } u'_s = i'_s \le n_s \quad &\text{suchthat } \overline{\mathrm{defined}}(y[i'_s], u_1[i'_s], \dots, u_m[i'_s]) \\ & \wedge u_1[i'_s] = u_1 \wedge \dots \wedge u_m[i'_s] = u_m \\ & \text{then } \overline{c_s[i_s]}\langle y[u'_s] \rangle \\ & \text{else new } y : T; \overline{c_s[i_s]}\langle y \rangle \\ & | c'_s(b' : \mathit{bool}); \text{if } b' \text{ then event\_abort } S \text{ else event\_abort } \bar{S} \end{aligned} \end{aligned} $$

The process $Q_{\mathrm{Secrecy}(x),0}$ behaves like $Q_{\mathrm{Secrecy}(x),\mathrm{random}}$ and $Q_{\mathrm{Secrecy}(x),n}$ behaves like $Q_{\mathrm{Secrecy}(x),\mathrm{real}}$ ($n_j = n$). Therefore,

$$ \begin{aligned} \mathrm{Adv}_G^{\mathrm{Secrecy}(x)}(C) &= \frac{1}{2} \left( \begin{array}{l} (\Pr[C[G \mid Q_{\mathrm{Secrecy}(x),n}] : \bar{\mathcal{S}}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x),0}] : \bar{\mathcal{S}}]) \\ - (\Pr[C[G \mid Q_{\mathrm{Secrecy}(x),n}] : \bar{\mathcal{S}}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x),0}] : \bar{\mathcal{S}}]) \\ = \frac{1}{2} \left( \begin{array}{l} \sum_{v=1}^n (\Pr[C[G \mid Q_{\mathrm{Secrecy}(x),v}] : \bar{\mathcal{S}}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x),v-1}] : \bar{\mathcal{S}}]) \\ - \sum_{v=1}^n (\Pr[C[G \mid Q_{\mathrm{Secrecy}(x),v}] : \bar{\mathcal{S}}] - \Pr[C[G \mid Q_{\mathrm{Secrecy}(x),v-1}] : \bar{\mathcal{S}}]) \end{array} \right) \end{aligned} $$
We define a context $C'_v$ that returns a random value for $u_j > v$, the real value of $x$ obtained from the public variable $x''$ in $G'$ for $u_j < v$, and calls $Q_{\text{Secrecy}(x')\text{,real}}$ or $Q_{\text{Secrecy}(x')\text{,random}}$ for $u_j = v$.

$$
\begin{align*}
C'_v &= \text{newChannel } c_{s1}; (\llbracket \rvert !_{i_s} \le n_s c_s[i_s](u_1 : [1, n_1], \dots, u_m : [1, n_m]); \\
&\quad \text{if } u_j = v \text{ then } \overline{c_{s1}[i_s]} \langle u_1, \dots, u_m \rangle; c_{s1}[i_s](z : T); \overline{c_s[i_s]} \langle z \rangle \text{ else} \\
&\quad \text{if defined}(x''[u_1, \dots, u_m]) \text{ then} \\
&\quad \quad \text{if } u_j < v \text{ then } \overline{c_s[i_s]} \langle x''[u_1, \dots, u_m] \rangle \text{ else} \\
&\quad \text{find } u'_s = i'_s \le n_s \text{ suchthat } \overline{\text{defined}(y[i'_s], u_1[i'_s], \dots, u_m[i'_s])} \wedge \\
&\quad \quad u_1[i'_s] = u_1 \wedge \dots \wedge u_m[i'_s] = u_m \\
&\quad \text{then } \overline{c_s[i_s]} \langle y[u'_s] \rangle \\
&\quad \text{else new } y : T; \overline{c_s[i_s]} \langle y \rangle \rangle
\end{align*}
$$

where the processes $Q_{\text{Secrecy}(x')\text{,real}}$ and $Q_{\text{Secrecy}(x')\text{,random}}$ use channel $c_{s1}$ instead of $c_s$. When $u_j = v$, the query on $c_s[i_s]$ is forwarded to $Q_{\text{Secrecy}(x')\text{,real}}$ (resp. $Q_{\text{Secrecy}(x')\text{,random}}$) on channel $c_{s1}[i_s]$. The values of $x$ for sessions other than $v$ are collected in $x''$ by $G'$; these are the values returned by the query on $c_s[i_s]$ when $u_j < v$. Finally, when $u_j > v$, the query on $c_s[i_s]$ is answered with a random value $y$.

Then

$$
\begin{align*}
\Pr[C[G \mid Q_{\text{Secrecy}(x),v}] : S] &= \Pr[C[C'_{v}[G' \mid Q_{\text{Secrecy}(x')\text{,real}}]] : S], \\
\Pr[C[G \mid Q_{\text{Secrecy}(x),v}] : \bar{S}] &= \Pr[C[C'_{v}[G' \mid Q_{\text{Secrecy}(x')\text{,real}}]] : \bar{S}], \\
\Pr[C[G \mid Q_{\text{Secrecy}(x),v-1}] : S] &= \Pr[C[C'_{v}[G' \mid Q_{\text{Secrecy}(x')\text{,random}}]] : S], \quad \text{and} \\
\Pr[C[G \mid Q_{\text{Secrecy}(x),v-1}] : \bar{S}] &= \Pr[C[C'_{v}[G' \mid Q_{\text{Secrecy}(x')\text{,random}}]] : \bar{S}],
\end{align*}
$$

for $i_{\text{tested}} = v$.

Then

$$
\begin{align*}
& \operatorname{Adv}_G^{\operatorname{Secrecy}(x)}(C) \\
&= \sum_{v=1}^{n} \frac{1}{2} \left( \Pr[C[C'_{v}[G' \mid Q_{\operatorname{Secrecy}(x')\text{,real}}]] : S] - \Pr[C[C'_{v}[G' \mid Q_{\operatorname{Secrecy}(x')\text{,random}}]] : S] \right) \\
&\qquad - \Pr[C[C'_{v}[G' \mid Q_{\operatorname{Secrecy}(x')\text{,real}}]] : \bar{S}] + \Pr[C[C'_{v}[G' \mid Q_{\operatorname{Secrecy}(x')\text{,random}}]] : \bar{S}] \\
&\qquad \text{for } i_{\text{tested}} = v \\
&= \sum_{v=1}^{n} \operatorname{Adv}_{G'}^{\operatorname{Secrecy}(x')}(C[C'_{v}]) \text{ for } i_{\text{tested}} = v
\end{align*}
$$

by the link between the advantage for secrecy and $Q_{\text{Secrecy}(x')\text{,real}}$, $Q_{\text{Secrecy}(x')\text{,random}}$ shown above. Since $G'$ satisfies the secrecy of $x'$ with public variables $V \cup \{x''\}$ up to probability $p$ and $C[C'_v]$ is an evaluation context acceptable for $G' \mid Q_{\text{Secrecy}(x')}$ with public variables $V \cup \{x''\}$ that does not contain $S$ nor $\bar{S}$, we have $\operatorname{Adv}_{G'}^{\text{Secrecy}(x')}(C[C'_v]) \le p(C[C'_v])$. Moreover, by Property 7, the probability $p(C[C'_v])$ is independent of $i_{\text{tested}} = v$ (because the type of $i_{\text{tested}}$ is bounded) and depends only on the runtime of $C$, the number of outputs $C$ makes on the various channels (which determine replication bounds), and the length of bitstrings, so we have $p(C[C'_v]) = p(C)$ (the runtime of $C'_v$ can be neglected). Hence, we obtain $\operatorname{Adv}_G^{\text{Secrecy}(x)}(C) \le n \times p(C)$. Therefore, $G$ satisfies the secrecy of $x$ with public variables $V$ up to probability $n \times p$.
**One-session secrecy, secrecy, and bit secrecy** In this lemma, bit secrecy queries do not occur. However, we reuse this proof in Lemmas 59 and 60 where bit secrecy queries occur, so we also handle them here. Let sp be 1-ses.secr.(x), Secrecy(x), or bit secr.(x), and sp' be the same property with x' instead of x. Let V' = V when sp is 1-ses.secr.(x) or bit secr.(x), and V' = V ∪ {x''} when sp is Secrecy(x). Since Bound<sub>G'</sub>(V' ∪ {x'}, sp', NonUnique<sub>G'</sub>, p), then by Lemma 27, Property 1, G' satisfies sp' with public variables V' up to probability p' such that p'(C) = p(C[C<sub>sp'</sub>]). So by the previous result for (one-session or bit) secrecy, G satisfies sp with public variables V up to probability np'. Let C be an evaluation context acceptable for C<sub>sp</sub>[G] with public variables V that does not contain S nor S̄. Hence

$$
\begin{align*}
\mathrm{Adv}_G(C[C_{sp}[]], sp, D_{\mathrm{false}}) \\
&= \mathrm{Pr}[C[C_{sp}[G]] : S] - \mathrm{Pr}[C[C_{sp}[G]] : \bar{S} \lor \mathrm{NonUnique}_G] \\
&\le \mathrm{Pr}[C[C_{sp}[G]] : S] - \mathrm{Pr}[C[C_{sp}[G]] : \bar{S}] \\
&= \mathrm{Adv}_G^{sp}(C) \le n \times p'(C) = n \times p(C[C_{sp}[]])
\end{align*}
$$

Indeed, replacing $C_{sp'}$ with $C_{sp}$ in the argument of $p$ does not change its result, by Property 7.
Therefore, we have $\text{Bound}_G(V \cup \{x\}, sp, D_{\text{false}}, np)$. $\square$

In the guess transformation, we cannot modify injective correspondence queries, because two
executions of some injective event e with different indices i could be mapped to the same events
in the conclusion of the query. In general, it even does not work for non-injective events inside
injective queries. As a counter-example, consider the query: $\forall i : [1, n], x : T'; \text{event}(e_1(i, x)) \wedge$
$\text{inj-event}(e_2(x)) \Rightarrow \text{inj-event}(e_3())$ with events $e_1(i_1, x_1)$, $e_1(i_2, x_2)$, $e_2(x_1)$, $e_2(x_2)$ and $e_3$ each
executed once. This query is false: we have two executions of $e_2$ (with matching executions of
$e_1$) for a single execution of $e_3$. That contradicts injectivity. However, it is true if we restrict
ourselves to one value of i (the index of the tested session), because we consider $e_1(i_1, x_1)$, $e_2(x_1)$
and $e_3$ for $i = i_1$ and $e_1(i_2, x_2)$, $e_2(x_2)$ and $e_3$ for $i = i_2$. Requiring the same value of x in $e_1$ and
$e_2$ restricts the events $e_2$ that we consider when we guess the session for $e_1$. Therefore, proving
the query for the tested session does not allow us to prove it in the initial game.

Hence, for injective correspondence queries $\forall \tilde{x} : \tilde{T} : \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, we proceed as follows: we define a non-injective query noninj($\forall \tilde{x} : \tilde{T} ; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$) simply obtained by replacing injective events with non-injective events, and we try to prove 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$ in the current game. This proof is a modified version of the proof of injective queries (Section 4.2.4): we define the pseudo-formula $\mathcal{C}(\psi, \phi)$ by

$$
\begin{align*}
\mathcal{C}(\psi, M) &= \perp \\
\mathcal{C}(\psi, \text{event}(e(\tilde{M}))) &= \perp \\
\mathcal{C}(\psi, \text{inj-event}(e(\tilde{M}))) &= S \text{ such that assuming } \psi = F_1 \wedge \dots \wedge F_m, \\
&\quad \text{for every } \mu_1 \text{ that executes } F_1, \dots, \text{ for every } \mu_m \text{ that executes } F_m, \text{ letting}
\end{align*}
$$

$$
\mathcal{F} = \theta_1 \mathcal{F}_{F_1, \mu_1} \cup \dots \cup \theta_m \mathcal{F}_{F_m, \mu_m},
$$

$$
\mathcal{I} = \{ j \mapsto (\mu_j, \theta_j I_{\mu_j}) \mid F_j \text{ is an injective event} \},
$$

$$
\mathcal{V} = \text{var}(\theta_1 I_{\mu_1}) \cup \dots \cup \text{var}(\theta_m I_{\mu_m}) \cup \{\tilde{x}, \tilde{y}\},
$$

where for $j \le m$, $\theta_j$ is a renaming of $I_{\mu_j}$ to fresh replication indices,
we have $(\mathcal{F}, (\tilde{M}), \mathcal{I}, \mathcal{V}) \in \mathcal{S}$.

$$
\mathcal{C}(\psi, \phi_1 \wedge \phi_2) = \mathcal{C}(\psi, \phi_1) \wedge \mathcal{C}(\psi, \phi_2)
$$

$$
\mathcal{C}(\psi, \phi_1 \lor \phi_2) = \mathcal{C}(\psi, \phi_1) \lor \mathcal{C}(\psi, \phi_2)
$$

Given a pseudo-formula $\mathcal{C}$, we define $\vdash \mathcal{C}$ as in Section 4.2.4.
**Proposition 4** Let $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ be a correspondence, with $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$. Let $\varphi = [[\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi]]$ be the semantics the correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$ ($\text{Definition 12}$), and $\varphi_{\text{ni}} = [[\text{noninj}(\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi)]]$ be the semantics of the correspondence noninj($\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$). Let $Q_0$ be a process that satisfies Properties 4 and 5. Suppose that, in $Q_0$, the arguments of the events that occur in $\psi$ are always simple terms.

Assume that $\vdash C(\psi, \phi)$ and for all evaluation contexts $C$ acceptable for $Q_0$, $\text{Pr}[C[Q_0] \preceq \neg \{\vdash C(\psi, \phi)\}] \le p(C)$. If $\text{Bound}_{Q_0}(V, \varphi_{\text{ni}}, D_{\text{false}}, p')$, then $\text{Bound}_{Q_0}(V, \varphi, D_{\text{false}}, p' + p)$.

Proposition 4 proves injectivity much like in Section 4.2.4, but using the arguments $\tilde{M}$ of the events in $\phi$ instead of the program points and replication indices at their execution (which we do not have since in $Q_0$ we are not able to prove that these events have been executed; otherwise we would simply prove the correspondence in $Q_0$). Intuitively, $\vdash C(\psi, \phi)$ shows that, if we have different executions of injective events in $\psi$, that is, executions of such events with different pairs (program point, replication indices), then the arguments $\tilde{M}$ of each injective event in $\phi$ must be different, which implies different executions of this event.

**Proof** Let $C$ be an evaluation context acceptable for $Q_0$ with public variables $V$ that does not contain events used by $\varphi$. Let $C = C(\psi, \phi)$. Consider a trace $\text{Tr}$ of $C[Q_0]$ such that $\text{Tr} \vdash \varphi_{\text{ni}}$, $\text{Tr} \vdash \{\vdash C\}$, $\text{Tr}$ does not execute a non-unique event of $Q_0$, and the last configuration of $\text{Tr}$ cannot be reduced. Let $\mu\mathcal{E}v$ be the sequence of events in the last configuration of $\text{Tr}$. Since $\mu\mathcal{E}v \vdash \varphi_{\text{ni}}$,

$$ \mu\mathcal{E}v \vdash \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) $$

with the notations of Definition 12. By defining functions $f_j \in \mathbb{N}^m \times \prod \tilde{T} \to \mathbb{N} \cup \{\perp\}$ that map $\tau_1, \dots, \tau_m, \tilde{x}$ to the execution steps of injective events in the proof of $\phi$, and to $\perp$ when the 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 (25) $$

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 (25), 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 37, 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} \mathcal{F}_{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 \mapsto (\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} \llcorner \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 \mathcal{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} \llcorner \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} \llcorner \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 40), 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 \mathcal{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 \mathcal{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 \mathcal{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 \mathcal{C}\} \wedge \neg\text{NonUnique}_{Q_0}) \wedge \neg\text{NonUnique}_{Q_0} = (\neg\varphi_{\text{ni}} \vee \neg\{\vdash \mathcal{C}\}) \wedge \neg\text{NonUnique}_{Q_0} = (\neg\varphi_{\text{ni}} \wedge \neg\text{NonUnique}_{Q_0}) \vee (\neg\{\vdash \mathcal{C}\} \wedge \neg\text{NonUnique}_{Q_0, \text{D} \text{false}})$, so it satisfies $(\neg\varphi_{\text{ni}} \wedge \neg\text{NonUnique}_{Q_0}) \vee \neg\{\vdash \mathcal{C}\}$. So

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

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

<figure><img src="image_15.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 &amp;&amp; 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**RemoveUnique = 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 57 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

$$ \text{if } x[c_1, \dots, c_m] = v_{\text{tested}} \text{ then } P \text{ else } \text{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 **diffConstants** = 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

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

where *guess*\_defined is a fresh variable, and we add *guess*\_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, \dots, c_m]$ **no_test** that can be applied when there are only correspondence queries and when $x[c_1, \dots, 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_{\text{tested}}$ when $M$ is a simple term and with let *ignore* = $M$ in let $x = v_{\text{tested}}$ otherwise, where *ignore* is a fresh variable whose value is not used.

The transformation **guess** $x[c_1, \dots, 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, \dots, 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, \dots, c_m] = v_{\text{tested}}$.

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

Suppose the game $G$ is transformed into $G'$ by the transformation **guess** $x[c_1, \dots, c_m]$ or **guess** $x[c_1, \dots, 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_{\text{tested}}$, then $\text{Bound}_G(V, \varphi, D, |T|p)$.

Let sp be 1-ses.secr(y), Secrec(y), or bit secr(x). Then $G$ is transformed into $G'$ by the transformation **guess** $x[c_1, \dots, c_m]$. If $G'$ satisfies sp with public variables $V \cup \{\text{guess } x\_defined\}$ ($y \notin V$) up to probability $p$ and $p$ satisfies Property 7, 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\_defined\}, sp, \text{NonUnique}_{G'}, p)$ and $p$ satisfies Property 7, then $\text{Bound}_G(V', sp, D_{\text{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$.

$$
\begin{align*}
\mathrm{Adv}_G(C, \varphi, D) \\
&= \Pr[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G,D}] \\
&= \Pr[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G,D} \land x[c_1, \dots, c_m] \text{ not defined}] + \\
&\qquad \sum_{v \in T} \Pr[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{NonUnique}_{G,D} \land x[c_1, \dots, c_m] = v] \\
&\le \sum_{v \in T} \Pr[C[G] : (\neg\varphi \lor D) \land \neg\mathrm{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*}
\Pr[C[G'] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G',D}] \\
\geq \Pr[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D} \land (x[c_1, \dots, c_m] = v_{\text{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{align*}
\mathrm{Adv}_G(C, \varphi, D) &\le \sum_{v \in T} \Pr[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'}(C, \varphi, D) \text{ for } v_{\text{tested}} = v
\end{align*}
$$

Since $\text{Bound}_{G'}(V, \varphi, D, p)$, we have $\text{Adv}_{G'}(C, \varphi, D) \le p(C)$ and $p$ is independent of the value of $v_{\text{tested}}$, so we obtain $\text{Adv}_G(C, \varphi, D) \le |T| \times p(C)$. Therefore $\text{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}$. We have

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

From the adversary $C$, we define four adversaries $C'$ that output $b''$ instead of $b'$ on channel $c'_s$ ($c''_s$ for bit secrecy), where $b'' = \text{if defined}(\text{guess } x\text{-defined}) \text{ then } f_1(b') \text{ 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 $\text{Adv}_{G'}^{sp}(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}}}$,

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

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$
### 5.1.20 globalDepAnal [24]

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 new $x: 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^{-1}_{|\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 $\text{only\_dep}(x) = S$ when intuitively, only variables in $S$ depend on $x$, and the adversary cannot see the value of $x$. Formally, $\text{only\_dep}(x) = S$ when

* $S \cap V = \emptyset$.

* Variables of $S$ do not occur in input or output channels or messages, that is, they do not occur in the terms $M_1, \dots, M_m, N_1, \dots, N_k$ in the input $c[M_1, \dots, M_m](x_1[i] : T_1, \dots, x_k[i] : T_k)$ or in the output $c[M_1, \dots, M_m](N_1, \dots, N_k)$.

* 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[i] \le \tilde{n}_j$ such that defined($M_{j1}, \dots, M_{jl_j}$) ∧ $M_j$ then $P_j$) else $P'$ are combinations by ∧, ∨, or ¬ of terms that either do not contain variables in $S$ or are of the form $M_1 = M_2$ or $M_1 \ne 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 \ne M_2$ are true except in cases of negligible probability.

In checking the conditions of only\_dep($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($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 \ne 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 61** The transformation global\_dep\_anal requires and preserves Properties 1, 2, 3, 4, 5, and 6. If transformation global\_dep\_anal transforms $G$ into $G'$, then $D, D_{SNU} : G, D, EvUsed \xrightarrow{V} p G', D, EvUsed$, where $p$ is an upper bound on the probability that required equalities do not hold.

### 5.1.21 simplify [24, 25]

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}_{PM}$ (see Sections 3.1 and 3.3) and the rewrite rules obtained from $\mathcal{F}_{PM}$ 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 to true, CryptoVerif tries to prove uniqueness of find[unique$_e$], 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 \text{ does not contain } \text{event_abort} \text{ nor un-proved } \text{find}[\text{unique}_e], u_{jk}[\tilde{i}] \text{ reduces into } M' \text{ by user-defined rewrite rules knowing } \mathcal{F}_{P_j} \text{ (see Sections 3.1 and 3.3) and the rewrite rules obtained from } \mathcal{F}_{P_j}, \text{ and } u_{jk} \text{ does not occur in } M', \text{ then } u_{jk} \text{ is removed from the } j\text{-th branch of this find, } i_{jk} \text{ is replaced with } M'\{i_{j'k'}/u_{j'k'}, j' \le m, k' \le m_j\} \text{ in } M_{j1}, \dots, M_{jl_j}, M_j \text{ and } P_j \text{ is replaced with let } u_{jk}[\tilde{i}] : [1, n_{jk}] = M' \text{ in } P_j. \text{(Intuitively, } u_{jk}[\tilde{i}] = M', \text{ so the value of } u_{jk}[\tilde{i}] \text{ can be computed by evaluating } M' \text{ instead of performing an array lookup. We remove } u_{jk}[\tilde{i}] \text{ from the variables looked up by find and replace } u_{jk}[\tilde{i}] \text{ 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', \text{ there exists a term } M \text{ such that } \text{defined}(M) \in \mathcal{F}_{P_j}, x[N_1, \dots, N_l] \text{ is a subterm of } M, x \ne u_{jk} \text{ for all } k \le m_j, \text{ and none of the following conditions holds: a) } P \text{ is under a definition of } x \text{ in } Q_0; \text{ b) } Q_0 \text{ contains } Q_1 | Q_2 \text{ such that a definition of } x \text{ occurs in } Q_1 \text{ and } P \text{ is under } Q_2 \text{ or a definition of } x \text{ occurs in } Q_2 \text{ and } P \text{ is under } Q_1; \text{ c) } Q_0 \text{ contains } lp+1 \text{ replications above a process } Q \text{ that contains a definition of } x \text{ and } P, \text{ where } lp \text{ is the length of the longest common prefix between } N_1, \dots, N_l \text{ and the current replication indices at the definitions of } x. \text{ Then the } j\text{-th branch of the find is removed. (In this case, } x[N_1, \dots, N_l] \text{ cannot be defined at } P, \text{ so the } j\text{-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 } \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } P_j) \text{ else } P', \text{ there exist terms } M, M' \text{ such that } \text{defined}(M) \in \mathcal{F}_{P_j}, x[N_1, \dots, N_l] \text{ is a subterm of } M, \text{ defined}(M') \in \mathcal{F}_{P_j}, x'[N'_1, \dots, N'_l] \text{ is a subterm of } M', N_k = N'_k \text{ for all } k \le \min(l, l'), x \ne x', \text{ and } x \text{ and } x' \text{ are incompatible, then the } j\text{-th branch of the find is removed. Two variables } x \text{ and } x' \text{ are said to be compatible when either there exists } Q_1 | Q_2 \text{ in the game such that } x \text{ is defined in } Q_1 \text{ and } x' \text{ is defined in } Q_2, \text{ or there is a definition of } x' \text{ under a definition of } x, \text{ or symmetrically.}$

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

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

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

9. If $P = \text{find}[\text{unique?}] \tilde{u}[\tilde{i}] = \tilde{u}' \le \tilde{n} \text{ suchthat } \text{defined}(M_1, \dots, M_l) \wedge M \text{ then } P_1 \text{ else } P'$, $[\text{unique?}]$ is not $[\text{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 } \text{defined}(M_{j1}, \dots, M_{jl_j}) \wedge M_j \text{ then } \overline{\text{yield}}(\langle)) \text{ else } \overline{\text{yield}}(\langle), [\text{unique?}]$ is not $[\text{unique}_e]$ for some non-unique event $e$ that is not proved yet to have negligible probability, the terms $M_j$ do not contain $\text{event_abort}$ nor unproved $\text{find}[\text{unique}_e]$, and the variables in $\tilde{u}_j$ are not used outside $P$ and are not in $V$, then $P$ is replaced with $\overline{\text{yield}}(\langle)$.
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 = \text{new } x : 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<sub>e</sub>], 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}'' \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) $$

$$ \bigoplus (\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} \wedge 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}'' \text{ else } P $$

where

- either for all $j \le k$, $c_j$ does not contain event_abort nor unproved find[unique<sub>e</sub>] 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<sub>e</sub>])

- $\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'}) \wedge \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

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

- $\mathbf{b}(FB, x[\tilde{N}] :: L) = \mathbf{b}(FB, L) \cup \{\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c'\{i/x[\tilde{N}]\} \wedge \tilde{N} = \tilde{i} \text{ then } P' \mid (\tilde{u}' = \tilde{i}' \le \tilde{n}' \text{ suchthat } c' \text{ then } P') \in \mathbf{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'}) \wedge \dots$, we replace this access with $i$, where $i = x\{\tilde{i}_{j_0}/\tilde{u}_{j_0}\}$; this is done in 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'}) \wedge \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 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 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 6. 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_e] 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} \\ \qquad \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 6. 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 62** *The transformation simplify requires and preserves Properties 1, 2, 3, 4, and 5. It preserves 6. 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.*

### 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 Fetters` 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 **new** or by assignments of variables defined by **new**, 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 **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}^\varphi(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$ 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}^-$.

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 new or by assignments of variables defined by new, 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}^{1\text{-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 \neq 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 $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 \neq \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 63** *The transformation success simplify requires and preserves Properties 1, 2, 3, 4, 5, and 6.*

If transformation success simplify transforms $G$ into $G'$, the distinguisher $D$ is a disjunc-
tion of Shoup and non-unique events, the property sp and the disjuncts in $D$ correspond to active
queries, $\mathcal{L}^- = \{(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 evaluation contexts $C$ acceptable for $G$, $\text{Pr}[C[G] \le (\bigvee_{j \in J, k \in K} \exists I_{\mu_k}, \exists V_j, \wedge \mathcal{F}_j \wedge \wedge \mathcal{F}_k^{\text{mod}}) \vee (\bigvee \mathcal{L}^+)] \le p(C)$, and $\text{Bound}_{G'}(V, sp, D, p')$, then $\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(C, sp, D)$ in order to prove the soundness of this transformation. We cannot prove this soundness independently for $\text{Pr}[C[G] : S]$ and for $\text{Pr}[C[G] : \neg \bar{S}]$.

Moreover, in the implementation, for (one-session or bit) secrecy properties, a probability $2p(C)$ is added instead of just $p(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$. Let $\text{Tr}$ be any
full trace of $C[G]$ that does not execute any non-unique event of $G$ and such that $Tr \vdash \neg \varphi$. Then
$Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

**Proof of Fact 1.** By Lemma 41, 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$,

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

So

$$Tr \vdash (\neg\{\text{prove}^{\varphi}(C, \theta, S_1)\}) \lor (\bigvee_{(\mu_1, c_1, \dots, \mu_m, c_m) \in S_0 \setminus S_1} \neg\{\text{prove}^{\varphi}(C, \theta, \mu_1, c_1, \dots, \mu_m, c_m)\}).$$

Moreover, $\neg\{\mathcal{F} \models_{\tilde{\theta}}^{I, \mathcal{V}, C} \phi\} \Rightarrow \exists \tilde{z} \in \tilde{T}''$, $\bigwedge \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}(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}$, $\bigwedge \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

$$Tr \vdash (\neg\{\text{prove}^{\varphi}(C, \theta, S_1)\}) \lor (\bigvee_{(\mu_1, c_1, \dots, \mu_m, c_m) \in S_0 \setminus S_1} \exists \theta_1 I_{\mu_1}, \dots, \exists \theta_m I_{\mu_m}, \exists \tilde{x} \in \tilde{T}, \bigwedge \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}(C, \theta, 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 S_0 \setminus S_1$ (recall that, when $e$ is Shoup event, $e$ is always executed by event_abort $e$) so $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \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$. Let $Tr$ be any full trace of $C[G]$ such that $Tr \vdash e$. Then $Tr \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

**Proof of Fact 2.** By Lemma 37, 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 $Tr, \sigma \vdash \theta' \mathcal{F}_{\text{event}(e), \mu, c}^0$. Let $(\mathcal{V}, \mathcal{F}) = (\theta' I_\mu, \theta' \mathcal{F}_{\text{event}(e), \mu, c}^0)$ be the element of $\mathcal{L}^-$ for $\mu$ and $c$, in the treatment of correspondence event($e$) $\Rightarrow$ false. We have $Tr \vdash \exists \mathcal{V}, \bigwedge \mathcal{F}$. Therefore, $Tr \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j$.

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

**Proof of Fact 3.** By contraposition, if there is a configuration $\text{Conf} = E, \sigma, \mu^k M, \mathcal{T}, \mu \in \mathcal{E}$ or $\text{Conf} = E, (\sigma, \mu^k P), Q, Ch, \mathcal{T}, \mu \in \mathcal{E}$ at a modified program point $\mu_k$ in trace $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 30, $Tr, \rho \vdash \theta \mathcal{F}_{\mu_k}$. So $Tr, \rho \vdash \theta \mathcal{F}_k^{\text{mod}}$, so $Tr \vdash \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$.

We perform the proof for each query separately.
**Case 1:** sp is some correspondence $\varphi$ different from $\forall \tilde{x} \in \tilde{T}, \text{event}(e(\tilde{N})) \Rightarrow \text{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.

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

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

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

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

Case 1.2: Tr executes a non-unique event of G. Then $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 \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}$.

We conclude that

$$
\begin{align*}
\text{Adv}_G(C, \varphi, D) &\le \Pr[C[G] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G,D}] \\
&\le \Pr[C[G] : \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^{\text{mod}} \right) \lor (\bigvee \mathcal{L}^+) \right] \\
&\qquad + \Pr[C[G'] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G',D}] \\
&\le \Pr[C[G] \le \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^{\text{mod}} \right) \lor (\bigvee \mathcal{L}^+) \right] \quad \text{by Lemma 1} \\
&\qquad + \Pr[C[G'] : (\neg\varphi \lor D) \land \neg\text{NonUnique}_{G',D}] \\
&\le p(C) + \text{Adv}_{G'}(C, \varphi, D) \\
&\le p(C) + p'(C) \tag*{since $\text{Bound}_{G'}(V, sp, D, p')$}
\end{align*}
$$

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

**Case 2:** sp is some correspondence $\varphi = \forall \tilde{x} \in \tilde{T}, \text{event}(e(\tilde{N})) \Rightarrow \text{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.

Consider a full trace Tr of C[G] such that $Tr \vdash (\neg \varphi \lor D) \land \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 \land \bigwedge \mathcal{F}_k^{\text{mod}}) \lor (\bigvee \mathcal{L}^+)$ or there is a matching trace in C[G'] that satisfies $(\neg \varphi \lor D) \land \neg \text{NonUnique}_{G',D}$.

We have $Tr \vdash \exists \tilde{x} \in \tilde{T}, \text{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 \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}$.

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}, \text{event}(e(\tilde{N}))$.

Let $\mu\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 37, there exist $\tilde{a}$ and $\tau \in \mathbb{N}$ such that $\rho, \tilde{N} \downarrow \tilde{a}$ and $\mu\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\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 4.)

* Case 2.3.1: In case (Event), we have reductions

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

where $^{\mu}\mathit{event} \ e(\tilde{M}); P$ is a subprocess of $C[G]$ up to renaming of channels, by any number of applications of (Ctx) and a final application of (Event). The terms $\tilde{M}$ are simple terms (when some term in $\tilde{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(\tilde{M}); P), & \mathcal{Q}_0, \mathcal{Ch}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{1} & E_0, (\sigma_0, {}^{\mu}\mathit{event} \ e(\tilde{a}); P), \mathcal{Q}_0, \mathcal{Ch}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{1} & \mathit{Conf}' = E_0, (\sigma_0, P), \mathcal{Q}_0, \mathcal{Ch}_0, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathrm{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), & \mathcal{Q}_0, \mathcal{Ch}_0, \mathcal{T}_0, \mu\mathcal{E}v_0 \\
\xrightarrow{p} & \mathit{Conf}' = E, (\sigma_0, \text{abort}), \mathcal{Q}_0, \mathcal{Ch}_0, \mathcal{T}_0, (\mu\mathcal{E}v_0, (\mu, \mathrm{Im}(\sigma_0)) : e)
\end{align*}
$$

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

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

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

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

$$ 
\begin{align*}
\mathit{Conf} = E_0, \sigma_0, {}^{\mu}\mathit{event} \ e(\tilde{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, \mathrm{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 (CxtT), so we have

$$ 
\begin{gathered}
E_0, (\sigma_0, C_0[C_1[\dots C_k[\mu \text{event } e(\tilde{M}); N]\dots]]), Q_0, Ch_0, \mathcal{T}_0, \mu \mathcal{E}v_0 \\
\xrightarrow{1 \to^*} \text{Conf}' = E_0, (\sigma_0, C_0[C_1[\dots C_k[N]\dots]]), Q_0, Ch_0, \mathcal{T}_0, (\mu \mathcal{E}v_0, (\mu, \text{Im}(\sigma_0)) : e(\tilde{a}))
\end{gathered}
$$

for some $C_0$ context defined in Figure 10, $k \in \mathbb{N}$, and $C_1, \dots, C_k$ contexts defined in Figure 6, by $k$ applications of (CxtT) and one application of (Cxt).

* Case 2.3.4: In case (CxtEvent), we have

$$ \text{Conf} = E_0, \sigma_0, \mu \text{event\_abort } e, \mathcal{T}_0, \mu \mathcal{E}v_0 \xrightarrow{p} t E_0, \sigma_0, \text{event\_abort} (\mu, \text{Im}(\sigma_0)) : e, \mathcal{T}_0, \mu \mathcal{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 $\text{Conf}'$ be the last configuration of Tr.

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

prove$^\varphi(C, \theta_0, \mu, c) = (\theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c})$ 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$ is a pseudo-formula with all leaves $\perp$, so $\{[\vdash C]\} = \text{true}$.

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 37, 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 37, we have $\text{Tr}, \sigma \cup \rho \vdash \theta' \mathcal{F}_{\text{event}(e(\tilde{N})), \mu, c}$, since $\text{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 $\text{Tr} \vdash (\bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j) \lor (\bigvee \mathcal{L}^+)$.

- If $\text{Tr} \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $\text{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 $\text{Tr}$ at a modified program point $\mu_k$, so $\text{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 $\text{Tr}'$ be the prefix of $\text{Tr}$ that stops at $\text{Conf}'$. We have $\text{Conf} \preceq_{\text{Tr}} \text{Conf}'$, so by Corollary 3, $\text{Tr} \preceq \text{Conf}'$, $\sigma \vdash \theta' \mathcal{F}_{\mu, c}$, that is, $\text{Tr}', \sigma \vdash \theta' \mathcal{F}_{\mu, c}$. We have $E_0, \sigma_0, \tilde{M} \downarrow \tilde{a}$, so $E_0, \sigma, \theta' \tilde{M} \downarrow \tilde{a}$. The environment $E_{\text{Tr}'}$ extends $E_0$, so $E_{\text{Tr}'}$, $\sigma, \theta' \tilde{M} \downarrow \tilde{a}$, so $\text{Tr}', \sigma \cup \rho \vdash \theta' \tilde{M} = \tilde{N}$. Since $E_{\text{Tr}'} \preceq \text{Conf}' = E_{\text{Tr}'} \preceq \text{Conf}$ and $\sigma_{\text{Conf}'} = \sigma_{\text{Conf}}$, $\text{Tr}', \sigma \vdash \text{lastdefprogrampoint}(\mu, \theta' \tilde{i})$. Hence $\text{Tr}' \vdash \bigvee_{j \in J} \exists \mathcal{V}_j, \bigwedge \mathcal{F}_j$.

- If $\text{Tr}' \vdash \bigvee_{k \in K} \exists I_{\mu_k}, \bigwedge \mathcal{F}_k^{\text{mod}}$, then $\text{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}^+)$. and $\text{Tr}'$ is a prefix of $\text{Tr}$.