that is,

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

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

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

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

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

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

so

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

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

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

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

Property 2: Obvious.

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

Let $C$ be any evaluation context acceptable for $Q$ and $Q''$ with public variables $V$ that does not contain events in $\mathrm{EvUsed}''$. After renaming the variables of $C$ that do not occur in $Q$ and $Q''$ and the tables of $C$ that do not occur in $Q$ and $Q''$ so that they do not occur in $Q'$, $C$ is also acceptable for $Q'$ with public variables $V$. Furthermore, by Property 7, this renaming does not change the probabilities. Since $\mathrm{EvUsed}' \subseteq \mathrm{EvUsed}'$, $C$ does not contain events in $\mathrm{EvUsed}'$.

Let $D_0 \in \mathcal{D} \cup \{D_{\mathrm{false}}\}$ that runs in time at most $t_{D_0}$. Let $D_1$ be a disjunction of events of
$D_{SNU}$. Then we have:

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

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

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

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

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

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

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

$$
\begin{align}
& \Pr[\sigma^{-1}C'[\sigma^{-1}C[Q]] : (D_0 \lor D_1 \lor D)] \land \neg \text{NonUnique}_{Q, D_1 \lor D}] \nonumber \\
& \le \Pr[\sigma^{-1}C'[\sigma^{-1}C[Q')] : (D_0 \lor D_1 \lor D')] \land \neg \text{NonUnique}_{Q', D_1 \lor D'}] + p(\sigma^{-1}(C'[C[]]), t_{D_0}) \tag{3}
\end{align}
$$
Let $D'_0 \in \mathcal{D}_{\neg\sigma\mathit{EvUsed}'} \cup \{D_{\mathit{false}}\}$ that runs in time at most $t_{D_0}$, Let $D'_1$ be a disjunction of events in $\sigma\mathcal{D}_{\mathit{SNU}} \cup \mathcal{D}'_{\mathit{SNU}}$. We can write $D'_1$ under the form $D'_1 = D'_2 \lor D'_3$ where $D'_2$ is a disjunction of events in $\sigma\mathcal{D}_{\mathit{SNU}}$ and $D'_3$ is a disjunction of events in $\mathcal{D}'_{\mathit{SNU}}$.

By applying (3) to $D_0 = (D'_0 \circ \sigma \lor D'_3 \circ \sigma) \land \neg\mathit{NonUnique}_{\sigma^{-1}C,D'_3\circ\sigma}$, which uses events not in $\mathit{EvUsed}'$, and to $D_1 = D'_2 \circ \sigma$, we get

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

since $D_0$ can be implemented to run in the same time as $D'_0$. By applying $\sigma$, we have

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

Since the events of C are in $\mathit{EvUsed}^+$, the events of $\mathbf{NonUnique}_{C,D'_3}$ are disjoint from those in $(D'_2 \lor D \circ \sigma^{-1})$, so $(\neg\mathbf{NonUnique}_{C,D'_3}) \lor (D'_2 \lor D \circ \sigma^{-1}) = \neg\mathbf{NonUnique}_{C,D'_3}$ and similarly $(\neg\mathbf{NonUnique}_{C,D'_3}) \lor (D'_2 \lor D' \circ \sigma^{-1}) = \neg\mathbf{NonUnique}_{C,D'_3}$. So we have

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

that is

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

Properties 5 and 6: Obvious. $\square$

When CryptoVerif transforms a game G into a game $G'$, in most cases, we have $G \approx_p^{V,\mathcal{E}} G'$, where $p$ is the probability difference coming from the transformation, and computed by CryptoVerif, which implies $D, \mathcal{D}_{\mathit{SNU}} : G, D, \mathit{EvUsed} \xrightarrow{V} p G', D, \mathit{EvUsed}$, for all $D, \mathcal{D}_{\mathit{SNU}}, D$ such that $\mathit{event}(D) \cap \mathit{EvUsed} \subseteq \mathcal{E}, \mathcal{D}_{\mathit{SNU}} \subseteq \mathcal{E}$, $\mathit{event}(D) \subseteq \mathcal{E}$ by Lemma 19, Property 1a. However, there are exceptions to this situation:

* transformations that exploit the uniqueness of $\mathit{find}[\mathit{unique}_e]$ or $\mathit{get}[\mathit{unique}_e]$, which are valid only when event $e$ is not executed. These events are taken into account by $\mathit{NonUnique}_{Q,D}$.

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

$$ \mathcal{D}_{\neg EvUsed_R}, \emptyset : L, D_{\text{false}}, \emptyset \to_p R, D_R, EvUsed_R $$

where $L$ does not contain events, $D_R = \bigvee \{e \mid \text{event\_abort } e \text{ occurs in } R\}$ and $EvUsed_R = \{e \text{ that occur in } R\}$ (both event\_abort $e$ and [unique$_e$]). By Lemma 19, Property 4, we infer

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

where $\sigma$ is a renaming of the events in $EvUsed_R$ to events not in $EvUsed$, $C$ is a context acceptable for $L$ and $R$ such that the events that occur in $C$ are in $EvUsed$, $\mathcal{D}_{\text{SNU}}$ is a set of Shoup and non-unique events in $EvUsed$, $p'(C', t_{D_0}) = p(\sigma^{-1}(C'[C[]]), t_{D_0})$, and $V \subseteq \text{var}(C)$.

Distinguishers in $\mathcal{D}_{\neg \sigma EvUsed_R}$ include distinguishers that use events in $EvUsed$, in particular distinguishers for correspondences in $G$, as well as distinguishers in $\mathcal{D}_{\neg (EvUsed \cup \sigma EvUsed_R)}$ used for secrecy and indistinguishability.

* transformations that prove the absence of some events (up to some probability). For such transformations, we have $\mathcal{D}$, $\mathcal{D}_{\text{SNU}}: G, e, EvUsed \xrightarrow{V} p G, D_{\text{false}}, EvUsed$ where $p$ is an upper bound of the probability of event $e$ in $G$. For Shoup events, this generally happens when $G$ does not contain $e$ and $p(C, t_{D_0}) = 0$. For non-unique events, $p$ is the probability that the find[unique$_e$] or get[unique$_e$] yields several possible choices; after this step, the event $e$ is in NonUnique$_{G,D}$, so we can exploit uniqueness of find[unique$_e$] or get[unique$_e$].

That is why, in general, when CryptoVerif transforms a game $G$ into a game $G'$, we have $\mathcal{D}$, $\mathcal{D}_{\text{SNU}}: G, D, EvUsed \xrightarrow{V} p G', D', EvUsed'$.

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

### 2.7.1 Secrecy

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

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

$$ \begin{array}{l} Q_{1\text{-ses.secr.}(x)} = c_{s0}(\emptyset); \text{ new } b: \mathit{bool}; \overline{c_{s0}}(\langle\rangle); \\ \qquad (c_s(u_1: [1, n_1], \dots, u_m: [1, n_m]); \text{ if defined}(x[u_1, \dots, u_m]) \text{ then} \\ \qquad \qquad \text{ if } b \text{ then } \overline{c_s}\langle x[u_1, \dots, u_m] \rangle \text{ else new } y: T; \overline{c_s}\langle y \rangle \\ \qquad | c'_s(b': \mathit{bool}); \text{ if } b = b' \text{ then } \text{event\_abort } S \text{ else } \text{event\_abort } \bar{S} \end{array} $$
$$
\begin{align*}
Q_{\text{Secrecy}(x)} &= c_{s0}(); \text{ new } b: \mathbf{bool}; \overline{c_{s0}}\langle\rangle; \\
&\quad (\neg i_s \le n_s \quad 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} \\
&\qquad \text{ if } b \text{ then } \overline{c_s[i_s]}\langle x[u_1, \dots, u_m] \rangle \text{ else} \\
&\qquad \text{ find } u'_s = i'_s \le n_s \text{ such that } \overline{\text{defined}}(y[i'_s], u_1[i'_s], \dots, u_m[i'_s]) \land \\
&\qquad \qquad u_1[i'_s] = u_1 \land \dots \land u_m[i'_s] = u_m \\
&\qquad \text{ then } \overline{c_s[i_s]}\langle y[u'_s] \rangle \\
&\qquad \text{ else new } y: T; \overline{c_s[i_s]}\langle y \rangle \\
&\quad | c'_s(b': \mathbf{bool}); \text{ if } b = b' \text{ then } \text{event_abort S else } \text{event_abort } \overline{S}
\end{align*}
$$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Suppose that $Q \approx_p^{V \cup \{x\}, \mathcal{E}} Q'$ and $Q$ satisfies sp with public variables $V$ up to probability $p'$. Let $C$ be an acceptable evaluation context for $C_{sp}[Q']$ with public variables $V$ that does not contain $S$ nor $\bar{S}$.

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

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

### 2.7.2 Secrecy for a Bit

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

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

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

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

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

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

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

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

**Proof** Let $C$ be any acceptable evaluation context for $Q \mid Q_{\text{bit secr.}(b_0)}$ with public variables $V$. Let

$$C' = C[- | c_s''(b'_0 : \mathbf{bool}); \overline{c_{s0}}(\langle\rangle); c_{s0}(\langle\rangle); \overline{c_s}(\langle\rangle); c_s(b''_0 : \mathbf{bool}); \overline{c'_s}(\langle b'_0 = b''_0 \rangle)].$$

We execute $C'[Q \mid Q_{\text{1-ses.secr.}(b_0)}]$.

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

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

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

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

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

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

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

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

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

- $b''_0 = \neg b'_0$ with probability 1/4, so $b' = \text{false}$ and $S$ is executed.
So

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

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

Finally, we obtain

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

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

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

In the rest of Section 2.7.2, we consider a process

$$ Q = c(); \text{ new } b_0 : \text{bool}; \bar{c}(\langle); Q' $$

and let $Q_L = Q'\{\text{true}/b_0\}$ and $Q_R = Q'\{\text{false}/b_0\}$, so that $Q$ chooses a random bit $b_0$ and runs as $Q_L$ when $b_0$ is true and as $Q_R$ when $b_0$ is false. We assume that $Q_L$ and $Q_R$ never abort, that is, they contain neither event_abort nor find[unique$_e$]. Moreover, they do not use the variable $b_0$. We assume that the channels of the inputs at the root of $Q_L$ and $Q_R$ are not used elsewhere in $Q_L$ or $Q_R$. We have the following lemmas.

**Lemma 22** If $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then $Q_L \approx_{p'}^{V, \emptyset} Q_R$ where $p'(C, t_D) = p(C + t_D)$ and the context $C + t_D$ runs in time $t_C + t_D$ and its other parameters (replication bounds, lengths of bitstrings) are the same as for $C$.

The processes $Q_L$ and $Q_R$ can execute different events without breaking the bit secrecy of $b_0$, because the adversary for the bit secrecy of $b_0$ does not have access to the events executed by $Q$. Hence, $Q_L \approx_{p'}^V Q_R$ would not hold in general.

**Proof** Let $C$ be any acceptable evaluation context for $Q_L$ and $Q_R$ with public variables $V$, and $D$ a distinguisher such that $\text{event}(D) \cap \text{event}(Q_L, Q_R) = \emptyset$. Let $c$ and $c_s''$ be a channel that $C$ does not use.

Let $C'$ be a context that outputs on channel $c$, inputs on channel $c$, runs $C$ but stores events executed by $C$ in its internal state instead of actually executing events, computes $D$ on the stored sequence of events executed by $C$ and stores the result in $b'_0$, and sends $b'_0$ on channel $c_s''$. Such a context $C'$ exists because it can be encoded as a probabilistic Turing machine adversary, which can itself be encoded as a context in CryptoVerif, as shown in Section 2.8.

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

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

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

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

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

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

Finally, we obtain

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

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

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

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

**Lemma 23** If $Q_L \approx_p^{V,\emptyset} Q_R$ then $Q \approx_{p/2}^{V \cup \{b_0\},\emptyset} c()$; new $b_0 : \text{bool}$; $\bar{c}(\langle) ; Q_R$.

**Proof** Let $C$ be an evaluation context acceptable for $Q$ and $c()$; new $b_0 : \text{bool}$; $\bar{c}(\langle) ; Q_R$ with public variables $V \cup \{b_0\}$ and $D$ be a distinguisher. We have

$$ \begin{aligned} & |\Pr[C[Q] : D] - \Pr[C[c()]; \text{new } b_0 : \text{bool}; \bar{c}(\langle); Q_R] : D| \\ & \le \frac{1}{2}|\Pr[C[Q] : D/b_0 = \text{true}] - \Pr[C[c()]; \text{new } b_0 : \text{bool}; \bar{c}(\langle); Q_R] : D/b_0 = \text{true}| \\ & \quad + \frac{1}{2}|\Pr[C[Q] : D/b_0 = \text{false}] - \Pr[C[c()]; \text{new } b_0 : \text{bool}; \bar{c}(\langle); Q_R] : D/b_0 = \text{false}| \\ & \le \frac{1}{2}|\Pr[C[c()]; \text{let } b_0 = \text{true in } \bar{c}(\langle); Q_L] : D] - \Pr[C[c()]; \text{let } b_0 = \text{true in } \bar{c}(\langle); Q_R] : D| \\ & \le \frac{1}{2}p(C, t_D) \end{aligned} $$

<footnote n="1">¹if\_fun($b_0, M, M'$) differs from if $b_0$ then $M$ else $M'$ in that it evaluates both $M$ and $M'$. Since diff[$M, M'$] evaluates either $M$ or $M'$ but not both, we translate it into if $b_0$ then $M$ else $M'$ when the evaluation of $M$ or $M'$ may modify the semantic state, e.g. by executing an event or by defining a variable. The evaluation of simple terms does not modify the semantic state.</footnote>
Indeed, $\Pr[C[c()]; \text{let } b_0 = \text{true in } \bar{c}(\langle\rangle; Q_L] : D] = \Pr[C''[Q_L] : D]$ (and similarly for $Q_R$), where $C'' = C[\text{newChannel } \tilde{c}'; (F_{\tilde{c}, \tilde{c}'} | \text{newChannel } \tilde{c}; (c() ; \text{let } b_0 = \text{true in } \bar{c}(\langle\rangle; F_{\tilde{c}', \tilde{c}}) | [])]$, $\tilde{c}$ are the channels of the inputs at the root of $Q_L$ and $Q_R$ (which we assume not to be used elsewhere in $Q_L, Q_R$), $\tilde{c}'$ are fresh channels corresponding to channels in $\tilde{c}$, and $F_{\tilde{c}', \tilde{c}}$ forwards all messages sent on a channel in $\tilde{c}'$ to the corresponding channel in $\tilde{c}$, with replication bounds corresponding to the maximum of the replication bounds in $Q_L$ and $Q_R$. (All messages on channels in $\tilde{c}$ are forwarded to channels in $\tilde{c}'$ and then back on channels in $\tilde{c}$ provided the code $c()$; $\text{let } b_0 = \text{true in } \bar{c}(\langle\rangle)$ has already been executed. That prevents executing $Q_L$ or $Q_R$ before $c()$; $\text{let } b_0 = \text{true in } \bar{c}(\langle\rangle)$.) By Property 7, replacing $C''$ with $C$ as argument of $p(C, t_D)$ does not affect the probability. (We neglect the additional runtime of $C''$.) $\square$

Lemma 24 is the converse of Lemma 22.

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

**Proof** If $Q_L \approx_p^{V, \emptyset} Q_R$, then by Lemma 23, $Q \approx_{p/2}^{V \cup \{b_0\}, \emptyset} c()$; new $b_0 : \mathit{bool}$; $\bar{c}(\langle\rangle)$; $Q_R$. Moreover, $c()$; new $b_0 : \mathit{bool}$; $\bar{c}(\langle\rangle)$; $Q_R$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability 0. (Since $Q_R$ does not use $b_0$, the variable $b'$ in $Q_{\text{bit secr.}(b_0)}$ is independent of $b_0$, so a trace that executes $S$ corresponds to a trace of the same probability and that executes $\bar{S}$ by changing the value of $b_0$, so $\Pr[C[c()]; \text{new } b_0 : \mathit{bool}; \bar{c}(\langle\rangle; Q_R \mid Q_{\text{bit secr.}(b_0)}) : S] = \Pr[C[c()]; \text{new } b_0 : \mathit{bool}; \bar{c}(\langle\rangle; Q_R \mid Q_{\text{bit secr.}(b_0)}) : \bar{S}]$.) So by Lemma 20 (version for bit secrecy), $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p'$. $\square$

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

**Lemma 25** If $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then $Q$ preserves the one-session secrecy of $b_0$ with public variables $V$ up to probability $p$.

**Proof** If $Q$ preserves the bit secrecy of $b_0$ with public variables $V$ up to probability $p$, then by Lemma 22, $Q_L \approx_{p', \emptyset}^{V, \emptyset} Q_R$ where $p'(C, t_D) = p(C + t_D)$. By Lemma 23, $Q \approx_{p'/2}^{V \cup \{b_0\}, \emptyset} c()$; new $b_0 : \mathit{bool}$; $\bar{c}(\langle\rangle)$; $Q_R$.

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

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

### 2.7.3 Correspondences

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

<table><tr><td>φ ::=</td><td>formula</td></tr><tr><td>M</td><td>term</td></tr><tr><td>event(e(M<sub>1</sub>, ..., M<sub>m</sub>))</td><td>event</td></tr><tr><td>φ<sub>1</sub> ∧ φ<sub>2</sub></td><td>conjunction</td></tr><tr><td>φ<sub>1</sub> ∨ φ<sub>2</sub></td><td>disjunction</td></tr></table>

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

**Definition 9** The semantics of the correspondence $\forall \tilde{x} : \tilde{T} : \psi \Rightarrow \exists \tilde{y} : \tilde{T}' : \phi$, also written $\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'$; $\psi \Rightarrow \phi$ in a less explicit syntax, is $[\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi] = [\tilde{x} : \tilde{T}, \tilde{y} : \tilde{T}'; \psi \Rightarrow \phi] = \forall \tilde{x} \in \tilde{T}, (\psi \Rightarrow \exists \tilde{y} \in \tilde{T}', \phi)$, where $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$.

The formula $M$ holds when $M$ evaluates to true. The formula $\text{event}(e(M_1, ..., M_n))$ holds when the event $e(M_1, ..., M_n)$ has been executed. Conjunction, disjunction, implication, existential and universal quantifications are defined as usual. More formally, we write $\rho, \mathcal{E}v \vdash \varphi$ when the sequence of events $\mathcal{E}v$ satisfies the formula $\varphi$, in the environment $\rho$ that maps variables to their values. We define $\rho, \mathcal{E}v \vdash \varphi$ as follows:

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

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

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

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

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

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

When sp is a correspondence $\varphi$, we define $C_{sp} = []$ and the events used by sp are the events that occur in the formula $\varphi$. Therefore, the definition of "Q satisfies the correspondence $\varphi$" matches the definition of "Q satisfies sp" given in Definition 7.
A process satisfies $\varphi$ up to probability $p$ when the probability that it generates a sequence of events $\mathcal{E}v$ that does not satisfy $\varphi$ is at most $p(C)$, in the presence of an adversary represented by the context $C$.

**Example 2** The semantics of the correspondence

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

is

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

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

The semantics of the correspondence

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

is

$$ \forall x \in T, \mathbf{event}(e_1(x)) \wedge \mathbf{event}(e_2(x)) \Rightarrow \exists y \in T', \mathbf{event}(e_3(x)) \vee (\mathbf{event}(e_4(x, y)) \wedge \mathbf{event}(e_5(x, y))) $$

It means that, with overwhelming probability, for all $x$, if $e_1(x)$ and $e_2(x)$ have been executed, then $e_3(x)$ has been executed or there exists $y$ such that both $e_4(x, y)$ and $e_5(x, y)$ have been executed.

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

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

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

With this definition, we have:

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

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

where $\tilde{x} = \text{var}(\psi)$, $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$, $\psi = F_1 \wedge \dots \wedge F_m$, $\psi^\tau = F_1^\tau \wedge \dots \wedge F_m^\tau$, $F_j^\tau = \text{event}(e(\tilde{M}))@\tau_j$ if $F_j = \text{event}(e(\tilde{M}))$ or $F_j = \text{inj-event}(e(\tilde{M}))$, $I = \{j | F_j = \text{inj-event}(\dots)\}$, $\phi^\tau$ is obtained from $\phi$ by replacing each injective event $\text{inj-event}(e(\tilde{M}))$ with $\text{event}(e(\tilde{M}))@f_j(\tau_1, \dots, \tau_m, \tilde{x})$ using a distinct function $f_j$ for each injective event in $\phi^\tau$, and $\text{Inj}(I, f)$ if and only if $f(\tau_1, \dots, \tau_m, \tilde{x}) = f(\tau_1', \dots, \tau_m', \tilde{x}') \neq \perp \Rightarrow \forall j \in I, \tau_j = \tau_j'$.
In $\psi^\tau$ and $\phi^\tau$, events are labeled with their associated execution step, $\tau_j$ for the events in $\psi^\tau$ and $f_j(\tau_1, \dots, \tau_m, \tilde{x})$ for the injective events in $\phi^\tau$. Therefore, the functions $f_j$ map the execution steps of events in $\psi, \tau_1, \dots, \tau_m$, and the values of the variables in $\psi, \tilde{x}$, to the associated execution steps of injective events in $\phi$. (The result $\perp$ corresponds to the case in which the event in $\phi$ is not executed: in case of disjunctions, not all events in $\phi$ are required to be executed.) The correspondence is injective when these functions $f_j$ are injective in their arguments that correspond to injective events in $\psi$. The indices of injective events in $\psi$ are collected in the set $I$, and injectivity is guaranteed by $\text{Inj}(I, f_j)$, which means that, ignoring the result $\perp$, $f_j$ is injective in its arguments of indices in $I$.

Definition 11 is unchanged for injective correspondences.

**Example 3** The semantics of the correspondence

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

is

$$ \exists f \in \mathbb{N} \times pkey \times host \times nonce \rightarrow \mathbb{N} \cup \{\perp\}, \text{Inj}(\{1\}, f) \wedge \\ \forall \tau \in \mathbb{N}, \forall x \in pkey, \forall y \in host, \forall z \in nonce, \\ \text{event}(e_B(x, y, z))@\tau \Rightarrow \text{event}(e_A(x, y, z))@f(\tau, x, y, z) \quad (7) $$

It means that, with overwhelming probability, each execution of $e_B(x, y, z)$ corresponds to a distinct execution of $e_A(x, y, z)$. In this case, $f$ is a function that maps the execution step $\tau$ of $e_B(x, y, z)$ and the variables $x, y, z$ to the execution step of $e_A(x, y, z)$. (This step is never $\perp$.) This function is injective in its first argument, the step $\tau$, so if there are $n$ executions of $e_B(x, y, z)$, at steps $\tau_1, \dots, \tau_n$, then there are at least $n$ executions of $e_A(x, y, z)$, at steps $f(\tau_1, x, y, z), \dots, f(\tau_n, x, y, z)$ and these steps are distinct by injectivity of $f$ in its first argument.

The semantics of the correspondence

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

is

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

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

When no injective event occurs in $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, Definition 12 reduces to the definition of non-injective correspondences: there are no functions $f_j$, $\phi^\tau = \phi$, and $\text{event}(e(\tilde{M}))@\tau$ holds for some $\tau$ if and only if $\text{event}(e(\tilde{M}))$ holds, so $\psi^\tau$ holds for some $\tau_1, \dots, \tau_m$ if and only if $\psi$ holds.
**Well-formedness condition** When we consider a correspondence $\forall \tilde{x} : \tilde{T}; \psi \Rightarrow \exists \tilde{y} : \tilde{T}'; \phi$, with $\tilde{x} = \text{var}(\psi)$ and $\tilde{y} = \text{var}(\phi) \setminus \text{var}(\psi)$, we should have

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

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

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

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

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

and

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

for any function $f$: (10) requires that event $e(y)$ is never executed with $y$ in the image of $f$, and (11) requires that $e'(y)$ is executed when $e(y)$ is executed with $y$ in the image of $f$.

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

## Property

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

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

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

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

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

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

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

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

$$ 
\begin{aligned}
\mathrm{Adv}_{Q'}^{\varphi}(C) &= \mathrm{Pr}[C'[Q'] : \neg\varphi] \\
&\leq \mathrm{Pr}[C'[Q] : \neg\varphi] + |\mathrm{Pr}[C'[Q'] : \neg\varphi] - \mathrm{Pr}[C'[Q] : \neg\varphi]| \\
&\leq p'(C) + p(C, t_{\varphi})
\end{aligned}
$$

Indeed, by renaming the variables and tables of $C$ that do not appear in $Q'$ to variables and tables that also do not occur in $Q$, $C$ is also an acceptable evaluation context for $Q$ with public variables $V$. Furthermore, by Property 7, this renaming does not change the probabilities. $\square$

**Reachability secrecy** Reachability secrecy aims to show that the adversary cannot compute the secret value. This notion is standard in the symbolic model, but less common than the notion of secrecy as “the adversary cannot distinguish the secret from a random value” (Section 2.7.1) in the computational model. It is still used, e.g. in the property of one-wayness or in the computational Diffie-Hellman assumption.

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

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

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

$$ 
\begin{aligned}
Q_{\text{1-ses.reach.secr.}(x)} &= !^{i_t \le n_t} c_s[i_t](x' : T, u_1 : [1, n_1], \dots, u_m : [1, n_m]); \\
&\quad \text{if } \text{defined}(x[u_1, \dots, u_m]) \land x' = x[u_1, \dots, u_m] \text{ then } \text{adv\_has\_x} \\
Q_{\text{Reach.secr.}(x)} &= !^{i_r \le n_r} c_r[i_r](u'_1 : [1, n_1], \dots, u'_m : [1, n_m]); \text{ if } \text{defined}(x[u'_1, \dots, u'_m]) \text{ then} \\
&\quad \text{let } \text{reveal} : \mathbf{bool} = \text{true} \text{ in } \overline{c_r[i_r]} \langle x[u'_1, \dots, u'_m] \rangle \\
&\quad | !^{i_t \le n_t} c_s(x' : T, u_1 : [1, n_1], \dots, u_m : [1, n_m]); \\
&\quad \text{find } i \le i_r \text{ suchthat } \text{defined}(\text{reveal}[i], u'_1[i], \dots, u'_m[i]) \land \\
&\quad \phantom{\text{find } i \le i_r \text{ suchthat }} u'_1[i] = u_1 \land \dots \land u'_m[i] = u_m \text{ then yield else} \\
&\quad \text{if } \text{defined}(x[u_1, \dots, u_m]) \land x' = x[u_1, \dots, u_m] \text{ then } \text{adv\_has\_x}
\end{aligned}
$$
where $c_s, c_r \notin \text{fc}(Q)$, $x', u_1, \dots, u_m, u'_1, \dots, u'_m$, reveal $\notin \text{var}(Q) \cup V$, $\text{adv\_has\_x}$ does not occur in $Q$, and $\mathcal{E}(x) = [1, n_1] \times \dots \times [1, n_m] \to T$.

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

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

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

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

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

### 2.7.4 Computation of Advantages

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

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

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

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

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

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

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

**Lemma 27** 1. In the initial game Q, let $D_U = \bigvee\{e \mid \text{unique}_e \text{ occurs in } Q\} = \text{NonUnique}_Q$.

If $\text{Bound}_Q(V, sp, D_U, p)$, then Q satisfies property sp with public variables $V \setminus V_{sp}$ up to probability $p'$ where $p'(C') = p(C'[C_{sp}[]])$.
2. If $D, D_{\text{SNU}}: Q, D, \text{EvUsed} \xrightarrow{V} p Q', D', \text{EvUsed}',$ the events $S$ and $\bar{S}$ are not in $\text{EvUsed}', \text{Bound}_Q(V, sp, D', p')$, and

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

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

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

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

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

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

4. If $D, D_{\text{SNU}}: Q, D, \text{EvUsed} \xrightarrow{V} p Q', D', \text{EvUsed}',$ the distinguisher $D''$ is a disjunction of Shoup and non-unique events in $\text{EvUsed}$ that does not contain $S$ nor $\bar{S}$, and $\text{Bound}_Q(V, \text{true}, D'', p')$, then $D, D_{\text{SNU}}: Q, D \lor D'', \text{EvUsed} \xrightarrow{V} p_{+p'} Q', D', \text{EvUsed}'$.

**Proof** Property 1: We have $\text{NonUnique}_{Q,D_U} = D_{\text{false}}$. Let $C'$ be an evaluation context acceptable for $C_{sp}[Q]$ with public variables $V \setminus V_{sp}$ that does not contain events used by $sp$, and $C = C'[C_{sp}[]]$. Since $\text{Bound}_Q(V, sp, D_U, p)$, we have $\text{Adv}_Q(C, sp, D_U) \le p(C)$.

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

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

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

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

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

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

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

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

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

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

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

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

$$ \begin{align*} &= \Pr[C''[Q] : (S \lor D) \land \neg \text{NonUnique}_{Q,D}] \\ &\quad - \Pr[C'''[Q] : (\bar{S} \land \neg D) \lor \text{NonUnique}_{Q,D}] \end{align*} $$

since $S \lor D$ is equivalent to $(S \lor D) \land \neg \text{NonUnique}_{Q,D}$ and $\bar{S}$ is equivalent to $\bar{S} \land \neg D$: the game aborts immediately after executing $S, \bar{S}$, and the events in $D$ and $\text{NonUnique}_{Q,D}$ so only one of them can be executed

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

$$ \begin{align*} &\le \Pr[C''[Q'] : (S \lor D') \land \neg \text{NonUnique}_{Q',D'}] + p(C'', t_S) \\ &\quad - \Pr[C'''[Q'] : (\bar{S} \land \neg D') \lor \text{NonUnique}_{Q',D'}] + p(C'', t_S) \\ &\le \Pr[C''[Q'] : S \lor D'] - \Pr[C'''[Q'] : \bar{S} \lor \text{NonUnique}_{Q',D'}] + 2p(C'', t_S) \end{align*} $$

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

$$ \begin{align*} &\le \text{Adv}_{Q'}(C'', sp, D') + 2p(C'', t_S) \\ &\le p'(C'') + 2p(C'', t_S) \qquad \text{since } \text{Bound}_{Q'}(V, sp, D', p') \\ &\le p'(C) + 2p(C, t_S) \end{align*} $$

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

$$ \le p''(C) $$

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

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

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

Inria
In particular, $Adv_Q(C, true, D) = Pr[C[Q] : D]$. Hence

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

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

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

$$
\mathbf{Adv}_Q(C, sp, D) = \Pr[C[Q] : \mathcal{S} \lor D] - \Pr[C[Q] : \bar{\mathcal{S}} \lor (\mathbf{NonUnique}_Q \wedge \neg D)]
$$

Hence

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

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

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

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

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

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

since $\mathbf{Bound}_Q(V, true, D'', p')$. (Note that the context $C$ does not contain events used by $D''$ nor non-unique events of $Q$.) $\square$
This lemma allows one to bound the advantage of the adversary against secrecy and correspondences. Property 1 is used in the initial game, to express the desired probability from $\text{Bound}_Q(V, sp, D_U, p)$. (Using the distinguisher $D_U$ can also be understood by saying that we consider that the adversary wins if some non-unique event is executed, that is, if a find or get declared unique by the user actually has several possible choices. That allows the implementation to make any choice when a find[unique$_e$] or get[unique$_e$] has several possible choices: the security proof remains valid. In particular, a find[unique$_e$] or get[unique$_e$] can be implemented by always choosing the first found element.) Property 2 is used when a game $Q$ is transformed into a game $Q'$ during the proof. It allows one to bound the probability in $Q$ from a bound in $Q'$. Property 3 is useful when distinct sequences of games are used for bounding the probabilities of breaking sp and of $D$ on one side and of $D'$ on the other side. We bound these two probabilities by $\text{Bound}_Q(V, sp, D, p)$ and $\text{Bound}_Q(V, \text{true}, D', p')$ separately, then obtain a bound $\text{Bound}_Q(V, sp, D \lor D', p''')$ by computing a sum. (When we deal with secrecy and $D'_{\text{NU}} \neq D_{\text{false}}$, the probability of $D'_{\text{NU}}$ can be bounded by looking at the proof for $D'$.)

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

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

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

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

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

When an edge labeled with $(sp'', D'', p'')$ has a source node labeled with $(Q, V, \dots, EvUsed)$ and target nodes labeled with $(Q_j, V_j, sp'_j, D_j, EvUsed_j)$ for $j \in \{1, \dots, l\}$ (Figure 13(a)), the bound associated to the edge can be computed from the bound associated to the target nodes by the probability formula $p''$ that labels the edge: if $\text{Bound}_{Q_j}(V_j, sp'_j, D_j, p_j)$ for $j \in \{1, \dots, l\}$, then $\text{Bound}_Q(V, sp'', D'', p)$ where $p(C) = p''(C, p_1(C), \dots, p_l(C))$. This situation corresponds to a game transformation that transforms game $Q$ into games $Q_j$ ($j \in \{1, \dots, l\}$). We can distinguish several cases depending on where the edge comes from:

* For most game transformations, the edge has a single target node ($l=1$), $V_1 = V$, $sp'_1 = sp''$, and the game transformation transforms $Q$ into $Q_1$ and satisfies $D_1, \emptyset$: $Q, D'', EvUsed \xrightarrow{V} p'_1 Q_1, D_1, EvUsed_1$ where $D_1 = \{\neg sp''\}$ when $sp''$ is a trace property, $D_1 = \{S, \neg \bar{S}\}$ when $sp''$ is 1-ses.secr$(x)$, Secrecy$(x)$, or bit secr$(x)$, and $D_1 = \emptyset$ when $sp''$ is true. (During the building of the proof tree, we have $D, D_{SNU}: Q, D, EvUsed \xrightarrow{V} p'_1 Q_1, D', EvUsed_1$, where the distinguishers $D$ correspond to the active queries not for introduced Shoup and non-unique events, so $D_1 \subseteq D, D_{SNU}$ are the active queries for Shoup and non-unique events both before and after this step so $D''$ and $D_1$ are disjunctions of events in
<figure><img src="image_11.png" /><figcaption>Figure 13: Structure of a proof tree</figcaption></figure>

$D_{\text{SNU}}$, $D = D'' \wedge \neg D_1$ are the Shoup/non-unique events proved at this step, $D' = D_1 \wedge \neg D''$ are the Shoup/non-unique events introduced at this step. By applying several times Lemma 19, Property 5, we obtain $D, D_{\text{SNU}} : Q, D'', EvUsed \xrightarrow{V} p' Q_1, D_1, EvUsed_1$. By Lemma 19, Property 6, we obtain $D_1, \emptyset : Q, D'', EvUsed \xrightarrow{V} p' Q_1, D_1, EvUsed_1$.) The bound is inferred by Lemma 27, Property 2.

If $sp''$ is a trace property and $\text{Bound}_{Q_1}(V, sp'', D_1, p_1)$, then $\text{Bound}_Q(V, sp'', D'', p)$ where $p(C) = p'(C, t_{\neg sp''}) + p_1(C)$, so we can define $p''(C, p_t) = p'(C, t_{\neg sp''}) + p_t$.

If $sp''$ is 1-ses.secr.(x), Secrecy(x), or bit secr.(x) and $\text{Bound}_{Q_1}(V, sp'', D_1, p_1)$, then we have $\text{Bound}_Q(V, sp'', D'', p)$ where $p(C) = 2p'(C, t_S) + p_1(C)$, so we can define $p''(C, p_t) = 2p'(C, t_S) + p_t$.

To unify these two cases, we define

$$ \text{pstd}_{p'}^{sp''}(C, p_t) = \begin{cases} p'(C, t_{\neg sp''}) + p_t & \text{when } sp'' \text{ is a trace property} \\ 2p'(C, t_S) + p_t & \text{when } sp'' \text{ is 1-ses.secr.}(x), \text{ Secrecy}(x), \text{ or bit secr.}(x) \end{cases} $$

so that, when an edge comes from a transformation $D_1, \emptyset : Q, D'', EvUsed \xrightarrow{V} p' Q_1, D_1, EvUsed_1$ and the considered security property is $sp''$, the edge can be labeled with the probability formula $\text{pstd}_{p'}^{sp''}$. If $\text{Bound}_{Q_1}(V, sp'', D_1, p_1)$, then $\text{Bound}_Q(V, sp'', D'', p)$ where $p(C) = \text{pstd}_{p'}^{sp''}(C, p_1(C))$.

* When a query is proved (by the command **success**, Section 4), the edge has no target node ($l = 0$), and we simply obtain $\text{Bound}_Q(V, sp'', D'', p'')$. The probability $p''$ that labels the edge is determined by the **success** command (Proposition 1, 2, or 3).

These propositions require that $D'' = D_{\text{false}}$. This is obtained by splitting the properties to prove one property at a time (with one edge for each property starting from the source node), yielding bounds of the form $\text{Bound}_Q(V, sp'', D_{\text{false}}, p'')$ or $\text{Bound}_Q(V, \text{true}, e, p'')$. For the first form, $p''$ can immediately be computed from Proposition 1, 2, or 3. For the
<figure><img src="image_12.png" /><figcaption>Figure 14: Examples of proof trees</figcaption></figure>

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

Lemma 27 allows us to obtain more precise probability bounds than the standard computation of probabilities generally done by cryptographers, when we use Shoup's lemma [63]. By Shoup's lemma, if $G'$ is obtained from $G$ by inserting an event $e$ and modifying the code executed after $e$, the probability of distinguishing $G'$ from $G$ is bounded by the probability of executing $e$: for all contexts $C$ acceptable for $G$ and $G'$ (with any public variables) and all distinguishers $D$, $|\Pr[C[G] : D] - \Pr[C[G'] : D]| \le \Pr[C[G'] : e]$. Hence,

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

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

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

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

* Since $e_0$ does not occur in $G_2$, we have $\text{Adv}_{G_2}(C, sp, D_{\text{false}}) = 0$ for all evaluation contexts $C$ acceptable for $G_2$ with public variables $V$ that do not contain event $e_0$. So $\text{Bound}_{G_2}(V,$
since $\mathbf{NonUnique}_{G_0, D_{U0}} = D_{\text{false}}$, and for all evaluation contexts $C$ acceptable for $G_1$ and $G_2$ with public variables $V$ that do not contain events in $\mathit{EvUsed}'_1$, and all distinguishers $D_0 \in \mathcal{D}$ that run in time at most $t_{D_0}$,

$$ \Pr[C[G_1] : D_0 \lor D_{U1}] \le \Pr[C[G_2] : (D_0 \lor D_2) \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p'(C, t_{D_0}). \quad (15) $$

Let $C$ be an evaluation context acceptable for $G_0$ and $G_1$ with public variables $V$. After renaming the variables of $C$ that do not occur in $G_0$ and $G_1$ and the tables of $C$ that do not occur in $G_0$ and $G_1$ so that they do not occur in $G_2$, $C$ is also acceptable for $G_2$ with public variables $V$. Furthermore, by Property 7, this renaming does not change the probabilities. Let $D_0 \in \mathcal{D}$ be a distinguisher that runs in time at most $t_{D_0}$. We rename the events of $C$ in $\mathit{EvUsed}'$ or $\mathit{EvUsed}'_1$ to some fresh events, and modify $D_0$ so that it considers the renamed events as if they were the original events. That does not change the probability $|\Pr[C[G_0] : D_0] - \Pr[C[G_1] : D_0]|$, and guarantees that $C$ does not contain events in $\mathit{EvUsed}'$ nor in $\mathit{EvUsed}'_1$. So

$$ \begin{aligned} \Pr[C[G_0] : D_0] &\le \Pr[C[G_0] : D_0 \lor D_{U0}] \\ &\le \Pr[C[G_2] : (D_0 \lor D_2) \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) \\ &\le \Pr[C[G_2] : ((D_0 \land \neg D_2) \lor D_2) \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) \\ &\le \Pr[C[G_2] : (D_0 \land \neg D_2) \land \neg \mathbf{NonUnique}_{G_2, D_2}] \\ &\qquad + \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) \\ &\le \Pr[C[G_2] : D_0 \land \neg D_2] + \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) \end{aligned} $$

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

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

so

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

so

$$ \Pr[C[G_0] : D_0] - \Pr[C[G_1] : D_0] \le \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) + p'(C, t_{D_0}) $$

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

$$ \Pr[C[G_1] : D_0] - \Pr[C[G_0] : D_0] \le \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) + p'(C, t_{D_0}) $$

so

$$ | \Pr[C[G_0] : D_0] - \Pr[C[G_1] : D_0] | \le \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) + p'(C, t_{D_0}) $$
so $G_0 \approx_{p''}^V G_1$ where $p''(C, t_{D_0}) = \Pr[C[G_2] : D_2 \land \neg \mathbf{NonUnique}_{G_2, D_2}] + p(C, t_{D_0}) + p'(C, t_{D_0})$.
### 2.7.6 Proof of query-equiv

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

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

$$ \Pr[C[G_0] : D_0] \le \Pr[C[G_1] : (D_0 \lor D_1) \land \neg \text{NonUnique}_{G_1, D_1}] + p(C, t_{D_0}) $$

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

$$ \Pr[C[G_0] : D_0] \le \Pr[C[G_2] : (D_0 \lor D_2) \land \neg \text{NonUnique}_{G_2, D_2}] + p_0(C, t_{D_0}) $$

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

$$ \Pr[C[G_1] : D_0 \lor D_{U1}] \le \Pr[C[G_2] : (D_0 \lor D'_2) \land \neg \text{NonUnique}_{G_2, D'_2}] + p_1(C, t_{D_0}) $$

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

$$ \Pr[C[G_1] : (\neg D_0 \land \neg D_1) \lor D_{U1}] \le \Pr[C[G_2] : ((\neg D_0 \land \neg D_1) \lor D'_2) \land \neg \text{NonUnique}_{G_2, D'_2}] + p_1(C, t_{D_0}) $$

so

$$ \Pr[C[G_2] : ((D_0 \lor D_1) \land \neg D'_2) \lor \text{NonUnique}_{G_2, D'_2}] \le \Pr[C[G_1] : (D_0 \lor D_1) \land \neg D_{U1}] + p_1(C, t_{D_0}) $$

Then we get

$$ \begin{align*} \Pr[C[G_0] : D_0] & \le \Pr[C[G_2] : (D_0 \lor D_2) \land \neg \text{NonUnique}_{G_2, D_2}] + p_0(C, t_{D_0}) \\ & \le \Pr[C[G_2] : (D_0 \lor D_1 \lor D'_2) \land \neg \text{NonUnique}_{G_2, D'_2}] + p_0(C, t_{D_0}) \\ & \le \Pr[C[G_2] : ((D_0 \lor D_1) \land \neg D'_2) \lor \text{NonUnique}_{G_2, D'_2}] \\ & \quad + \Pr[C[G_2] : D'_2 \land \neg \text{NonUnique}_{G_2, D'_2}] + p_0(C, t_{D_0}) \\ & \le \Pr[C[G_1] : (D_0 \lor D_1) \land \neg D_{U1}] \\ & \quad + p_1(C, t_{D_0}) + \Pr[C[G_2] : D'_2 \land \neg \text{NonUnique}_{G_2, D'_2}] + p_0(C, t_{D_0}) \\ & \le \Pr[C[G_1] : (D_0 \lor D_1) \land \neg \text{NonUnique}_{G_1, D_1}] \\ & \quad + p_1(C, t_{D_0}) + \Pr[C[G_2] : D'_2 \land \neg \text{NonUnique}_{G_2, D'_2}] + p_0(C, t_{D_0}) \end{align*} $$

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

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

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

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

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

We bound

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

From this bound, we infer the desired property.

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

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

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

$$ \Pr[C[G'_0] : D_0] \le \Pr[C[G'_3] : D_0 \lor D_1 \lor D_{U1}] $$

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

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

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

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

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

## 2.8 Turing Machine Adversary

In CryptoVerif, the adversary is modeled as an evaluation context. However, usually, in cryptographic results, an adversary is a bounded-time probabilistic Turing machine. In this section, we explain how any bounded-time probabilistic Turing machine that communicates on channels can be represented as a CryptoVerif evaluation context.

Let $Q_0$ be the initial game that interacts with an adversary. Let $c_1, \dots, c_k$ be the channels used in $Q_0$. Let $T_{\text{all}}$ be the union of all types that occur in $Q_0$. Let $T'_{\text{all}}$ be the type of pairs containing the encoding a channel as first component and an element of $T_{\text{all}}$ as second component. The encoding of a channel is either the constant *yield* or a tuple of integers $(j, i_1, \dots, i_{k'})$ with $1 \le j \le k$. (We assume that unambiguous tuples can be encoded as CryptoVerif values, and that the constant *yield* is different from a tuple.) Let $d_0, d_1$, and $d_2$ be channels that do not occur in $Q_0$.

Let $Q_1$ be a process that contains the parallel composition of processes

$$ !^{i_1 \le n_1} \dots !^{i_{k'} \le n_{k'}} c_j[i_1, \dots, i_{k'}](x : T_{\text{all}}). \overline{d_0}((j, i_1, \dots, i_{k'}), x) $$

for each output $c_j[i'_1, \dots, i'_{k'}] \langle N \rangle$ that occurs under $!^{i'_1 \le n_1} \dots !^{i'_{k'} \le n_{k'}}$ in $Q_0$. Since, in the initial game $Q_0$, the channels of all outputs use the current replication indices as channel indices, as in $c_j[i'_1, \dots, i'_{k'}]$, a single output is executed for each value of the indices and for each syntactic occurrence of the output, so the inputs in $Q_1$ can receive all outputs made by $Q_0$. The process $Q_1$ forwards all these outputs to the same channel $d_0$, with a message that specifies both the channel $c_j[i_1, \dots, i_{k'}]$ on which $Q_0$ emitted (encoded as a bitstring) and the message $x$ sent by $Q_0$.

In addition, $Q_1$ also contains the parallel composition of processes

$$ !^{i_1 \le n_1} \dots !^{i_{k'} \le n_{k'}} yield(). \overline{d_0}((yield, ())), $$

for each occurrence of *yield* that occurs under $!^{i'_1 \le n_1} \dots !^{i'_{k'} \le n_{k'}}$ in $Q_0$, to receive all outputs that come from the *yield* construct.

Let $C = \text{newChannel } d_0; \text{newChannel } d_1; \text{newChannel } d_2; (\text{start}(\cdot).\overline{d_1}[1]\langle s_0 \rangle | Q_1 | Q_2 | [])$, where the process $Q_2$ is defined in Figure 16. Let us explain how the context $C$ can simulate any Turing machine interacting with the process $Q_0$.

The current state of the Turing machine is sent on channel $d_1[i]$ where $i$ is a loop index that starts at 1 and increases during execution. As shown in the semantics of CryptoVerif, upon
1 $Q_2 = !^{i \le n} d_1[i](s: \text{bitstring});$

2 let $(s', o, v) = f(s)$ in
Lines 3–6 are repeated for each $j \le k$ and each $k'$
such that there is an input on channel $c_j[i'_1, \dots, i'_{k'}]$ in $Q_0$.

3 if $o = (j, k')$ then

4 let $(a_1, \dots, a_{k'}, b) = v$ in $\overline{c_j[a_1, \dots, a_{k'}]}(b)$;

5 $d_0(s'' : T'_{\text{all}}); \overline{d_1[i+1]}(f'(s', s''))$

6 else

7 if $o = \text{random}$ then

8 new $x: \text{bool}$; $\overline{d_1[i+1]}(f''(s', x))$

9 else

10 if $o = \text{abort}$ then

11 event_abort e

12 else

13 $\overline{d_2}(\langle)$

<caption>Figure 16: Looping process</caption>

startup, a message is sent on channel *start*. When *C* receives that message, it sends the initial state of the Turing machine *s*₀ on channel *d*₁[1]. This message is received by process *Q*₂ (line 1). Then *Q*₂ calls the function *f* on the current state *s* of the Turing machine (line 2). This function executes the Turing machine, until one of the following situations happens:

* The Turing machine sends a message *b* on a channel *c*<sub>j</sub>[*a*<sub>1</sub>, ..., *a*<sub>*k*'</sub>]; in this case, *f* returns (*s*', (*j*, *k*'), (*a*<sub>1</sub>, ..., *a*<sub>*k*'</sub>, *b*)), where *s*' is the new state of the Turing machine. The test at line 3 is then going to succeed for the appropriate value of *j*, *k*', and the desired message is going to be sent at line 4. After receiving a message, the process *Q*<sub>0</sub> always replies by sending a message (except if it aborts). This message is going to be received by *Q*<sub>1</sub>, which is going to forward on *d*<sub>0</sub> the channel and the received message. These channel and message are then received as *s*'' at line 5. Then *f*'(*s*', *s*'') is the new state of the Turing machine after receiving that message. This state is sent on channel *d*<sub>1</sub>[*i* + 1], which restarts a new iteration of *Q*<sub>2</sub>.

* The Turing machine generates a fresh random bit; in this case, *f* returns (*s*', random, ()) where *s*' is the new state of the Turing machine. The test at line 7 is then going to succeed. At line 8, a random bit *x* is chosen. Then *f*''(*s*', *x*) is the new state of the Turing machine with that random bit. This state is sent on channel *d*₁[*i* + 1], which restarts a new iteration of *Q*₂ as in the previous case.

* The Turing machine aborts; in this case, *f* returns (*s*', *abort*, ()). The test at line 10 is then going to succeed, and the process aborts at line 11. (The event *e* is any event not used elsewhere; the event is not really useful, it is present because the CryptoVerif language always executes an event before aborting.)
* The Turing machine stops; in this case, $f$ returns $(s', stop,())$. No test succeeds, so line 13 is executed. The process tries to send a message on channel $d_2$, but there is no input on this channel, so the process blocks.

The constants random, abort, and stop are assumed to be pairwise distinct, and distinct from all pairs.

The function $f$ is a CryptoVerif primitive, because it can be implemented by a deterministic bounded-time Turing machine. (Recall that $f$ stops when the initial probabilistic Turing machine makes a random choice, and the random choice is performed by CryptoVerif at lines 7–8.) Similarly, the function $f'$ that computes the new state of the Turing machine from the old state and the received message, and the function $f''$ that computes the new state of the Turing machine from the old state and a random bit are CryptoVerif primitives.

The replication bound $n$ (used in $Q_2$, line 1) is chosen large enough so that the loop never stops due to that bound: the Turing machine aborts or stops before the bound is reached. This is possible since the Turing machine runs in bounded time, so sends a bounded number of messages and chooses a bounded number of random bits.

Notice that, if $Q_0$ sends and receives messages on the same channels, it may happen that a message sent by $Q_0$ is immediately received by $Q_0$ without being intercepted by the adversary. In this case, since both $Q_0$ and $Q_1$ are going to listen on the same channels, the destination of the message (either the honest process $Q_0$ or the adversary $Q_1$) is chosen randomly with uniform probability, depending on the number of available receivers. Therefore, adding more copies of the receiving processes in $Q_1$ increases the probability that the adversary receives the message. Moreover, when the same channel is used for both inputs and outputs, the messages sent by $Q_2$ at line 4 may be received back by the adversary via $Q_1$, instead of being received by $Q_0$. We recommend avoiding this strange situation, by using distinct channels for inputs on the one hand and outputs on the other hand. More generally, we recommend using distinct channels for each input and output, so that the adversary gets full control of the network, as already mentioned page 13.

As a slight extension, it would still be possible to allow $Q_0$ to output on $c_j[i_1, \dots, i_{k'}]$ after receiving a message on the same channel $c_j[i_1, \dots, i_{k'}]$. In this case, a message sent by $Q_0$ on $c_j[i_1, \dots, i_{k'}]$ cannot be received by $Q_0$, because the input on $c_j[i_1, \dots, i_{k'}]$ is no longer available when the output on $c_j[i_1, \dots, i_{k'}]$ is performed by $Q_0$. Moreover, the problem that messages sent by $Q_2$ at line 4 may be received back by the adversary via $Q_1$, instead of being received by $Q_0$, can be avoided by putting the receiver process

$$c_j[a_1, \dots, a_{k'}](x : T_{\text{all}}).\overline{d_0}\langle\langle(j, a_1, \dots, a_{k'}), x\rangle\rangle$$

after $\overline{c_j[a_1, \dots, a_{k'}]}\langle b\rangle$ in parallel with $d_0(s'' : T'_{\text{all}}); \overline{d_1[i+1]}\langle f'(s', s'')\rangle$ in $Q_2$, instead of including

$$!^{i_1 \le n_1} \dots !^{i_{k'} \le n_{k'}} c_j[i_1, \dots, i_{k'}](x : T_{\text{all}}). \overline{d_0}\langle\langle(j, i_1, \dots, i_{k'}), x\rangle\rangle$$

in $Q_1$.

The context $C$ does not allow the Turing machine to execute events of its choice, while a CryptoVerif context can execute events. We could obviously extend the model to allow the Turing machine to execute events, but this is not needed for the cases we consider. Indeed, if the adversary represented as a CryptoVerif context executes events, these events can be deleted without changing the final result returned by the distinguisher: for correspondences, by Definition 11, the context is not allowed to contain events used by $\varphi$, and all other events are ignored by the distinguisher $\neg\varphi$; for one-session secrecy, secrecy, and bit secrecy, by Definitions 7 and 8, the context is not allowed to contain $S$ nor $\bar{S}$, and all other events are ignored by the distinguishers $S$ and $\bar{S}$.
To sum up, the context given in this section allows us to run any probabilistic bounded-time Turing machine as a CryptoVerif context, so CryptoVerif contexts are powerful enough to represent the adversaries usually considered by cryptographers.

## 3 Collecting True Facts

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

Given a configuration Conf = E, σ, N, T, μEv or Conf = E, (σ, P), Q, Ch, T, μEv or Conf = E, Q, Ch, we denote by EConf the environment E in configuration Conf. We denote by E<sub>Tr</sub>≤Conf the union of E<sub>Conf</sub>' for all configurations Conf' ≤<sub>Tr</sub> Conf in Tr. It is a set of mappings x[~a] ↦→ b. At this stage, it may include conflicting mappings x[~a] ↦→ b and x[~a] ↦→ b' with b ̸= b'. We prove below (Lemma 28) that this situation never happens. The notation E<sub>Tr</sub>≤Conf is useful because the environment computed in the semantics does not keep the values of variables defined in conditions of find after these conditions are evaluated. Considering the union of all environments of previous configurations allows us to recover the values of these variables, and to use them in the facts that we collect. Given a configuration Conf = E, σ, N, T, μEv or Conf = E, (σ, P), Q, Ch, T, μEv, we denote by σ<sub>Conf</sub> the mapping sequence for replication indices σ in the configuration Conf and by μEv<sub>Conf</sub> the sequence of events μEv in configuration Conf.

Let us define Defined as in Section 2.4.3, except that

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

$$ \text{Defined}(\sigma, \mu\text{find}[\text{unique}?]) (\bigoplus_{j=1}^{m} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \text{ suchthat } \text{defined}(\tilde{M}_j) \wedge M_j \text{ then } P_j) \text{ else } P) = $$

$$ \left( \biguplus_{j=1}^{m} \biguplus_{\tilde{a} \le \tilde{n}_j} \text{Defined}(\sigma[\tilde{i}_j \mapsto \tilde{a}], M_j) \right) \uplus \max \left( \max_{j=1}^{m} (\{\tilde{u}_j[\sigma(\tilde{i})]\} \uplus \text{Defined}(\sigma, P_j)), \text{Defined}(\sigma, P) \right) $$

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

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

**Lemma 28** Let Q₀ be a process that satisfies Properties 4 and 5. Let Tr be a trace of Q₀ and Conf be a configuration in the derivation of Tr. Then the following properties hold:

1. Defined(Tr ≤ Conf) does not contain duplicate elements.

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

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

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

We show by induction on the derivations that, if $\text{Conf} \xrightarrow{p} t \text{ Conf}'$, then $\text{Defined}(\text{Tr} \preceq \text{Conf}) \supset \text{Defined}(\text{Tr} \preceq \text{Conf}')$ and for all semantic configurations $\text{Conf}''$ in the derivation of $\text{Conf} \xrightarrow{p} t \text{ Conf}'$, $\text{Defined}(\text{Tr} \preceq \text{Conf}) \supset \text{Defined}(\text{Tr} \preceq \text{Conf}'')$, and similarly with $\rightsquigarrow$ instead of $\xrightarrow{p} t$.

The first result follows: since $Q_0$ satisfies Invariant 1, $\text{Defined}(\sigma_0, Q_0)$ does not contain duplicate elements, where $\sigma_0$ is the empty mapping sequence. Let $\text{Conf}_0 = \emptyset, \{(\sigma_0, Q_0)\}, \text{fc}(Q_0)$, $\text{Conf}_1 = \text{reduce}(\emptyset, \{(\sigma_0, Q_0)\}, \text{fc}(Q_0))$, $\text{Conf}_2 = \text{initConfig}(Q_0)$, and $\text{Conf}_3$ be any other configuration of $\text{Tr}$. Then $\text{Defined}(\text{Tr} \preceq \text{Conf}_0)$, $\text{Defined}(\text{Tr} \preceq \text{Conf}_1)$, $\text{Defined}(\text{Tr} \preceq \text{Conf}_2)$, and therefore $\text{Defined}(\text{Tr} \preceq \text{Conf}_3)$ do not contain duplicate elements.

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

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

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

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

**Proof sketch** By induction on the derivation. □

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

We use facts the represent properties that hold at certain program points in processes. We consider the following facts:

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

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

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

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

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

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

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

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

* $\text{lastdefprogrampoint}(\mu, \tilde{M})$ means that program point $\mu$ has been executed with replication indices equal to $\tilde{M}$ and the values of variables and replication indices are unchanged since that program point (that is, no variable definition nor output that changes the replication indices was executed since that program point).

Given an environment $E$ mapping process variables to their values, an environment $\rho$ mapping replication indices and non-process variables of the formula $\varphi$ to their values, and a sequence of events $\mu\varepsilon v$, we define $E, \rho, \mu\varepsilon v \vdash \varphi$, meaning that $E, \rho, \mu\varepsilon v$ satisfy $\varphi$, as follows:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Additionally, we define the following facts:

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

* $[\text{elselet}(\tilde{x} : \tilde{T}, N, M)] = \forall \tilde{x} \in \tilde{T}, N \neq M$.
## 3.1 User-defined Rewrite Rules

The user can give two kinds of information:

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

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

They are translated into rewrite rules as follows:

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

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

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

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

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

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

where $\mathcal{A}$ is a probabilistic Turing machine.

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

This claim is translated into the rewrite rule new $y_1 : T'_1, \dots, \mathrm{new} \ y_l : T'_l, \forall x_1 : T_1, \dots, \forall x_m : T_m : T_1, M_1 \to M_2$.

The prover has built-in rewrite rules for defining boolean functions:

$$ \neg \mathrm{true} \to \mathrm{false} \qquad \neg \mathrm{false} \to \mathrm{true} \qquad \forall x : \mathit{bool}, \neg(\neg x) \to x $$

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

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

$$ \forall x : T, x = x \to \mathrm{true} \qquad \forall x : T, x \neq x \to \mathrm{false} $$

$$ \forall x : \mathit{bool}, \forall y : \mathit{bool}, \neg(x \land y) \to (\neg x) \lor (\neg y) $$

$$ \forall x : \mathit{bool}, \forall y : \mathit{bool}, \neg(x \lor y) \to (\neg x) \land (\neg y) $$

$$ \forall x : \mathit{bool}, x \land \mathrm{true} \to x \qquad \forall x : \mathit{bool}, x \land \mathrm{false} \to \mathrm{false} $$

$$ \forall x : \mathit{bool}, x \lor \mathrm{true} \to \mathrm{true} \qquad \forall x : \mathit{bool}, x \lor \mathrm{false} \to x $$

$$ \forall x : T, \forall y : T, \mathrm{if\_fun}(\mathrm{true}, x, y) \to x \qquad \forall x : T, \forall y : T, \mathrm{if\_fun}(\mathrm{false}, x, y) \to y $$
$$ 
\begin{array}{l}
\forall x : \mathit{bool}, \forall y : T, \mathit{if\_fun}(x, y, y) \to y \\
\forall x_1 : T_1, \dots, \forall x_m : T_m, \forall x : \mathit{bool}, \forall y : T_k, \forall z : T_k, \\
\qquad f(x_1, \dots, x_{k-1}, \mathit{if\_fun}(x, y, z), x_{k+1}, \dots, x_m) \to \\
\qquad \qquad \mathit{if\_fun}(x, f(x_1, \dots, x_{k-1}, y, x_{k+1}, \dots, x_m), f(x_1, \dots, x_{k-1}, z, x_{k+1}, \dots, x_m)) \\
\qquad \text{when } f : T_1 \times \dots \times T_m \to T \text{ has option } \mathbf{autoSwapIf}
\end{array}
$$

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

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

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

$$ 
\begin{array}{l}
\forall m : \mathit{bitstring}; \forall k : T_k, \forall r : T_r, \\
\qquad \mathit{dec}(\mathit{enc}(m, k, r), k) = \mathit{i}_{\perp}(m) \qquad (\mathit{enc})
\end{array}
$$

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

$$ 
\begin{array}{l}
\forall x : T_k, \forall y : T_k, (\mathit{k2b}(x) = \mathit{k2b}(y)) = (x = y) \\
\forall x : T_k, \mathit{k2b}^{-1}(\mathit{k2b}(x)) = x \qquad (\mathit{k2b})
\end{array}
$$

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

## 3.2 Collecting True Facts from a Game

CryptoVerif collects a set of facts $\mathcal{F}_{\mu}$ that hold at each program point $\mu$ in the current game $Q_0$. Additionally, CryptoVerif also collects facts $\mathcal{F}_{\mu}^{\text{Fut}}$ (future facts at $\mu$), which hold at the end of the block of code that contains $\mu$ and ends with an output or an event_abort instruction that aborts the end. For instance, $\mathcal{F}_{\mu}^{\text{Fut}}$ may contain equalities that come from assignments performed after $\mu$ in the same block of code. (However, the facts in $\mathcal{F}_{\mu}^{\text{Fut}}$ may not hold in case a find[unique_e] aborts because several choices make the conditions of that find succeed.) These sets of facts may contain facts $M$, defined($M$), $M_1$: event($e(\tilde{M})$), and programpoint($\mu, \tilde{M}$). In these sets of facts, all terms $M$ must be simple.

Previous versions of the algorithm that collects facts were presented in [24, Appendix C.2] and [23, Appendix B.2]. The current algorithm is an extension that relies on the same principles. The facts programpoint($\mu, \tilde{M}$) is new. In particular, we have programpoint($\mu, I_{\mu}) \in \mathcal{F}_{\mu}$. The algorithm that collects facts satisfies the following properties.

**Lemma 30** Let $C$ be an evaluation context acceptable for $Q_0$, $Tr$ be a trace of $C[Q_0]$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_{\mu}$ be computed in $Q_0$. If a configuration Conf is at program point $\mu$ in $Tr$, then $Tr \leq Conf \vdash \mathcal{F}_{\mu}$.
Additionally, there is a more precise version of $\mathcal{F}_\mu$ that distinguishes cases depending on the program points at which the various variables are defined, generating several $\mathcal{F}_{\mu,c}$ for the various cases c. For this version, we have:

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

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

**Corollary 3** Let $C$ be an evaluation context acceptable for $Q_0$, $Tr$ be a trace of $C[Q_0]$, $\mu$ be a program point in $Q_0$, and $\mathcal{F}_\mu$ (resp. $\mathcal{F}_{\mu,c}$) be computed in $Q_0$. Let Conf be a configuration at program point $\mu$ in $Tr$. Let $\theta$ be a renaming of $I_\mu$ to fresh replication indices and $\rho = \{\theta I_\mu \mapsto \sigma_{\text{Conf}} I_\mu\}$. Let Conf' be a term or output process configuration in $Tr$ such that $\text{Conf} \preceq_{\text{Tr}} \text{Conf}'$. We have $\text{Tr} \preceq \text{Conf}'$, $\rho \vdash \theta \mathcal{F}_\mu$ and there exists a $c$ such that $\text{Tr} \preceq \text{Conf}'$, $\rho \vdash \theta \mathcal{F}_{\mu,c}$. In particular, $\text{Tr}, \rho \vdash \theta \mathcal{F}_\mu$ and there exists a $c$ such that $\text{Tr}, \rho \vdash \theta \mathcal{F}_{\mu,c}$.

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

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

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

### 3.3 Equational Prover

In order to reason on facts, CryptoVerif uses an equational prover: from a set of facts $\mathcal{F}$, this equational prover tries to derive a contradiction by rewriting terms, using an algorithm inspired by Knuth-Bendix completion. It also eliminates collisions between independent random values, thus the contradiction is obtained up to the probability of the eliminated collisions, that is, the probability that $\mathcal{F}$ holds is bounded by the probability of these collisions. When this algorithm succeeds, we say that "$\mathcal{F}$ yields a contradiction in game $Q_0$", and CryptoVerif computes the probability of the eliminated collisions. (We may omit the current game $Q_0$ when it is clear from the context.) Previous versions of this algorithm were presented in [24, Appendix C.5] and [23, Appendix B.3]. Those versions did not evaluate the probability because they considered
asymptotic security: they showed that the probability was negligible in the security parameter. Here, we use exact security: we compute the value of the probabilities, so the soundness of this algorithm can be expressed by the following lemma, adapted from [23, Proposition 7].

**Lemma 33** If for all $j \in J$, $\mathcal{F}_j$ yields a contradiction in a game $Q_0$, then CryptoVerif returns a probability $p$ such that for all evaluation contexts $C$ acceptable for $Q_0$ with any public variables, $\Pr[C[Q_0] \le \bigvee_{j \in J} \exists \tilde{x}_j \in \tilde{T}_j, \wedge \mathcal{F}_j] \le p(C)$, where $\tilde{x}_j$ are the replication indices and non-process variables that occur in $\mathcal{F}_j$ and $\tilde{T}_j$ are their types.

In particular, the lemma states that, when several sets of facts $\mathcal{F}_j$ yield a contradiction in the same game, CryptoVerif counts only once in the probability $p$ the collisions that are eliminated in proofs that $\mathcal{F}_j$ yields a contradiction for several $j$.

More generally, let us consider an algorithm $\varphi$ built from the following grammar:

<table><tr><td>ϕ ::=</td><td>algorithm</td></tr><tr><td>  F yields a contradiction</td><td>equational proof</td></tr><tr><td>  ϕ<sub>1</sub> ∧ ϕ<sub>2</sub></td><td>conjunction</td></tr><tr><td>  ϕ<sub>1</sub> ∨ ϕ<sub>2</sub></td><td>disjunction</td></tr><tr><td>ψ</td><td>mathematical formula</td></tr><tr><td>if ψ then ϕ<sub>1</sub> else ϕ<sub>2</sub></td><td>test</td></tr></table>

The mathematical formulas $\psi$ in such algorithms must not depend on the executed trace. (They may depend on the syntax of the game $Q_0$ or on the set of public variables $V$, for instance.)

We translate such algorithms into logical formulas on traces:

$$ \{\mathcal{F} \text{ yields a contradiction}\} = \neg \exists \tilde{x} \in \tilde{T}, \wedge \mathcal{F} \text{ where } \tilde{x} \text{ are the replication indices and non-process variables that occur in } \mathcal{F} \text{ and } \tilde{T} \text{ are their types.} $$

$$ \{\varphi_1 \wedge \varphi_2\} = \{\{\varphi_1\} \wedge \{\{\varphi_2\}\} $$

$$ \{\varphi_1 \vee \varphi_2\} = \begin{cases} \{\{\varphi_1\}\} & \text{if } \varphi_1 \\ \{\{\varphi_2\}\} & \text{otherwise} \end{cases} $$

$$ \{\psi\} = \psi $$

$$ \{\text{if } \psi \text{ then } \varphi_1 \text{ else } \varphi_2\} = \text{if } \psi \text{ then } \{\{\varphi_1\}\} \text{ else } \{\{\varphi_2\}\} $$

Intuitively, when algorithm $\varphi$ returns true, CryptoVerif shows that the formula $\{\{\varphi\}\}$ holds for most traces. It bounds the probability of the traces for which this formula does not hold, as shown by the following lemma.

**Lemma 34** If algorithm $\varphi$ returns true in a game $Q_0$, then CryptoVerif returns a probability $p$ such that for all evaluation contexts $C$ acceptable for $Q_0$ with any public variables, $\Pr[C[Q_0] \le \neg \{\{\varphi\}\}] \le p(C)$.

**Proof** We show by induction on the definition of $\varphi$ that, if $\varphi$ returns true and $\text{Tr} \vdash \neg \{\{\varphi\}\}$, then there exists $\mathcal{F}$ such that “$\mathcal{F}$ yields a contradiction” has been called in the evaluation of $\varphi$ and returned true, and $\text{Tr} \vdash \exists \tilde{x} \in \tilde{T}, \wedge \mathcal{F}$ where $\tilde{x}$ are the replication indices and non-process variables that occur in $\mathcal{F}$ and $\tilde{T}$ are their types.

* Case $\varphi = (\mathcal{F} \text{ yields a contradiction})$: obvious.
* Case $\varphi = \varphi_1 \wedge \varphi_2$: Since $\varphi$ returns true, $\varphi_1$ and $\varphi_2$ both return true. Since $\mathrm{Tr} \vdash \neg(\{[\varphi_1]\} \wedge \{[\varphi_2]\})$, we have either $\mathrm{Tr} \vdash \neg\{[\varphi_1]\}$ or $\mathrm{Tr} \vdash \neg\{[\varphi_2]\}$. In the first case, by induction hypothesis on $\varphi_1$, there exists $\mathcal{F}$ such that "$\mathcal{F}$ yields a contradiction" has been called in the evaluation of $\varphi_1$ and returned true, and $\mathrm{Tr} \vdash \exists \tilde{x} \in \tilde{T}, \wedge \mathcal{F}$ where $\tilde{x}$ are the replication indices and non-process variables that occur in $\mathcal{F}$ and $\tilde{T}$ are their types. Moreover, "$\mathcal{F}$ yields a contradiction" has been called in the evaluation of $\varphi$. The second case is symmetric.

* Case $\varphi = \varphi_1 \vee \varphi_2$: If $\varphi_1$ returns true, then $\{[\varphi]\} = \{[\varphi_1]\}$, so $\mathrm{Tr} \vdash \neg\{[\varphi_1]\}$. We conclude by induction hypothesis on $\varphi_1$, as above. If $\varphi_1$ returns false, then $\varphi_2$ returns true, since $\varphi$ returns true. Hence $\{[\varphi]\} = \{[\varphi_2]\}$, so $\mathrm{Tr} \vdash \neg\{[\varphi_2]\}$. We conclude by induction hypothesis on $\varphi_2$.

* Case $\varphi = \psi$: since $\psi$ evaluates to true, there is no trace $\mathrm{Tr}$ such that $\mathrm{Tr} \vdash \neg\psi$, so the property holds trivially.

* Case $\varphi =$ if $\psi$ then $\varphi_1$ else $\varphi_2$: if $\psi$ evaluates to true, then we conclude by induction hypothesis on $\varphi_1$. Indeed, since $\varphi$ returns true, $\varphi_1$ returns true. Since $\mathrm{Tr} \vdash \neg\{[\varphi]\}$, we have $\mathrm{Tr} \vdash \neg\{[\varphi_1]\}$. By induction hypothesis, there exists $\mathcal{F}$ such that "$\mathcal{F}$ yields a contradiction" has been called in the evaluation of $\varphi_1$ and returned true, and $\mathrm{Tr} \vdash \exists \tilde{x} \in \tilde{T}, \wedge \mathcal{F}$ where $\tilde{x}$ are the replication indices and non-process variables that occur in $\mathcal{F}$ and $\tilde{T}$ are their types. Then "$\mathcal{F}$ yields a contradiction" has also been called in the evaluation of $\varphi$. Similarly, if $\psi$ evaluates to false, then we conclude by induction hypothesis on $\varphi_2$.

We conclude by Lemma 33. $\square$

# 4 success: Criteria for Proving Security Properties

The command **success** tries to prove the active queries, as explained below. We consider a process $Q_0$ that satisfies Properties 4 and 5, and prove secrecy and correspondence properties for $Q_0$.

## 4.1 Secrecy

Let us now define syntactic criteria that allow us to prove secrecy properties of protocols. We first define the function noleak in Figure 17 and explain it below. This function implicitly depends on the current game $Q_0$ and the public variables $V$. The function call noleak($x[\tilde{M}']$, $\mathcal{I}$, $\mathcal{F}$) shows that $x[\tilde{M}']$ does not leak to the adversary, assuming $\mathcal{F}$ holds. The set $\mathcal{I}$ contains all replication indices that appear in $\mathcal{F}$. If $\mathcal{F}$ yields a contradiction, noleak is true, since it shows the absence of leak *assuming* $\mathcal{F}$ holds. Otherwise, $x[\tilde{M}']$ may leak either because $x \in V$ so $x$ is a public variable, or because of an occurrence of a term $x[\tilde{M}]$ in the game that reads $x[\tilde{M}']$ (so $\tilde{M} = \tilde{M}'$ holds) and such that the result of $x[\tilde{M}]$ leaks.

* In case $x[\tilde{M}]$ occurs in the term $M$ in an assignment let $y[i] = M$, the function noleak recursively tries to prove that $y[i]$ does not leak, when $y[i]$ may use $x[\tilde{M}']$, that is, when $\tilde{M}' = \tilde{M}$. The fact $\tilde{M}' = \tilde{M}$ and the facts $\mathcal{F}_\mu$ that hold at the program point $\mu$ of $x[\tilde{M}]$ are added to the known facts $\mathcal{F}$ in the recursive call. Indeed, these facts are known to hold in this case. The replication indices are renamed to fresh indices in order to avoid using the same index variable for indices that can actually take different values.
$$ \text{noleak}(x[\widetilde{M}'], \mathcal{I}, \mathcal{F}) = (\mathcal{F} \text{ yields a contradiction}) \lor ((x \notin V) \land \bigwedge_{\mu x[\widetilde{M}] \text{ in } Q_0} $$

– if $^\mu x[\widetilde{M}]$ is in $M$ in an assignment let $y[\tilde{i}] = M$ in $Q_0$, $M$ is built from replication indices, variables, function applications, and conditionals, and the current call is not inside a call to noleak($y[-], -, -$), then

$$ \text{noleak}(y[\theta\tilde{i}], \mathcal{I} \cup \{\theta\tilde{i}\}, \mathcal{F} \cup \theta\mathcal{F}_{\mu} \cup \{\theta\widetilde{M} = \widetilde{M}'\}) $$

where $\theta$ is a renaming of $\tilde{i}$ to fresh replication indices

– if $^\mu x[\widetilde{M}]$ is in event $e(M_1, \dots, M_{k-1}, C[^\mu x[\widetilde{M}]], M_{k+1}, \dots, M_m)$ in $Q_0$ for $C$ defined in Figure 18, then true

– otherwise, $\mathcal{F} \cup \theta\mathcal{F}_{\mu} \cup \{\theta\widetilde{M} = \widetilde{M}'\}$ yields a contradiction

where $\theta$ is a renaming of $I_\mu$ to fresh replication indices)

<caption>Figure 17: Function noleak</caption>

* In case $x[\widetilde{M}]$ occurs in the arguments of an event, the arguments of the event do not leak to the adversary, so this occurrence of $x[\widetilde{M}]$ does not make $x[\widetilde{M}']$ leak.

* In all other cases, we consider that the result of $x[\widetilde{M}]$ may leak, so, in order to prove that $x[\widetilde{M}']$ does not leak, we show that the occurrence of $x[\widetilde{M}]$ at $\mu$ cannot read $x[\widetilde{M}']$, by showing that $\widetilde{M} = \widetilde{M}', \mathcal{F}_{\mu}$, and $\mathcal{F}$ together yield a contradiction.

**Definition 15 (μ follows a definition of x)** We say that μ follows a definition of x when new $x[\tilde{i}] : T;^\mu \dots$, let $x[\tilde{i}] = M$ in $^\mu \dots$, find[unique?] ($\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j$ suchthat defined($\widetilde{M}_j$) ∧ $M_j$ then $^\mu j \dots$) else $\dots$ with $\mu_j = \mu$ and $x$ in $\tilde{u}_j$ for some $j \le m$, or $c[\widetilde{M}](x[\tilde{i}] : T);^\mu P$ occurs in $Q_0$.

We do not mention get in the previous definition, because it is excluded by Property 4. For each $\mu$ that follows a definition of $x$ in $Q_0$, we define $\text{defRand}_\mu(x)$ as follows:

$$ \text{defRand}_{\mu}(x) = \begin{cases} x[\tilde{i}] & \text{if } \text{new } x[\tilde{i}] : T;^\mu \dots \text{ occurs in } Q_0 \\ y[\widetilde{M}] & \text{if let } x[\tilde{i}] : T = y[\widetilde{M}] \text{ in } ^\mu \dots \text{ occurs in } Q_0 \text{ and} \\ & y \text{ is defined only by random choices in } Q_0 \end{cases} $$

In all other cases, $\text{defRand}_\mu(x)$ is not defined. The variable $\text{defRand}_\mu(x)$ is the random variable that defines $x$ just before program point $\mu$. When $x$ itself is chosen randomly at that point, $\text{defRand}_\mu(x)$ is simply $x[\tilde{i}]$, where $\tilde{i}$ are the current replication indices. When $x$ is defined by an assignment of a variable $y[\widetilde{M}]$ that is random, $\text{defRand}_\mu(x)$ is that variable. Otherwise, we give up and do not define $\text{defRand}_\mu(x)$.

$$ \begin{array}{l} \text{prove}^{1\text{-ses.secr.}(x)}(\mu) = \text{defRand}_{\mu}(x) \text{ is defined and} \\ \text{noleak}(\theta\text{defRand}_{\mu}(x), \{\theta I_{\mu}\}, \theta\mathcal{F}_{\mu}) \\ \text{where } \theta \text{ is a renaming of } I_{\mu} \text{ to fresh replication indices} \end{array} $$

$$ \text{prove}^{1\text{-ses.secr.}(x)}(S) = \bigwedge_{\mu \in S} \text{prove}^{1\text{-ses.secr.}(x)}(\mu) $$
$$
\begin{align*}
C &::= [] \\
  &\quad y[M_1, \dots, M_{k-1}, C, M_{k+1}, \dots, M_m] \\
  &\quad f(M_1, \dots, M_{k-1}, C, M_{k+1}, \dots, M_m) \\
  &\quad \mathit{new} \ y[\tilde{i}] : T; C \\
  &\quad \mathit{let} \ y[\tilde{i}] = M \ \mathit{in} \ C \\
  &\quad \mathit{if} \ M \ \mathit{then} \ C \ \mathit{else} \ N' \\
  &\quad \mathit{if} \ M \ \mathit{then} \ N \ \mathit{else} \ C \\
  &\quad \mathit{find}[\mathit{unique?}] \ (\bigoplus_{j=1, \dots, m; j \neq k} \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \ \mathit{suchthat} \ \mathit{defined}(\tilde{M}_j) \land M_j \ \mathit{then} \ N_j) \\
  &\quad \qquad \oplus \tilde{u}_k[\tilde{i}] = \tilde{i}_k \le \tilde{n}_k \ \mathit{suchthat} \ \mathit{defined}(\tilde{M}_k) \land M_k \ \mathit{then} \ C \ \mathit{else} \ N \\
  &\quad \mathit{find}[\mathit{unique?}] \ (\bigoplus_{j=1}^m \tilde{u}_j[\tilde{i}] = \tilde{i}_j \le \tilde{n}_j \ \mathit{suchthat} \ \mathit{defined}(\tilde{M}_j) \land M_j \ \mathit{then} \ N_j) \ \mathit{else} \ C \\
  &\quad \mathit{event} \ e(\tilde{M}); C
\end{align*}
$$

<caption>Figure 18: Event contexts</caption>

The function call prove<sup>1-ses.secr.</sup>(x)(μ) proves one-session secrecy for the definition of x just before program point μ. It considers only the cases in which x is defined either by a random choice or by an assignment from a random choice. In other cases, the proof fails. (These other cases can typically be handled by first removing assignments as needed.) Intuitively, prove<sup>1-ses.secr.</sup>(x)(μ) guarantees that, when x[i] is defined just before program point μ, the random variable defRand<sub>μ</sub>(x) that defines x[i] does not leak, knowing that the facts F<sub>μ</sub> hold. Only events and variables y[i'] that do not leak depend on the random choice that defines x[i]; the sent messages and the control flow of the process are independent of x[i], so the adversary obtains no information on x[i]. That guarantees the one-session secrecy of x[i] when it is defined just before μ. This is verified for all program points in S by prove<sup>1-ses.secr.</sup>(x)(S). When x is defined by assignment of z[M], this proof of one-session secrecy allows some array cells of z to leak, provided the array cells z[M] used to define x do not leak.

In order to prove secrecy, we also define prove<sup>distinct</sup>(x)(μ₁, μ₂) = (z₁ ≠ z₂) ∨ (θ₁F<sub>μ₁</sub> ∪ θ₂F<sub>μ₂</sub> ∪ {θ₁M̃<sub>1</sub> = θ₂M̃<sub>2</sub>, ĩ₁ ≠ ĩ₂}) yields a contradiction), where defRand<sub>μ₁</sub>(x) = z₁[M̃<sub>1</sub>], defRand<sub>μ₂</sub>(x) = z₂[M̃<sub>2</sub>], ĩ are the current replication indices at the definition of x, θ₁ and θ₂ are two distinct renamings of ĩ to fresh replication indices, ĩ₁ = θ₁ĩ, and ĩ₂ = θ₂ĩ. Intuitively, prove<sup>distinct</sup>(x)(μ₁, μ₂) guarantees that, if x[ĩ₁] is defined at μ₁, so x[ĩ₁] = z₁[θ₁M̃<sub>1</sub>], and x[ĩ₂] is defined at μ₂, so x[ĩ₂] = z₂[θ₂M̃<sub>2</sub>], with ĩ₁ ≠ ĩ₂, then the random variables that define x in these two cases, z₁[θ₁M̃<sub>1</sub>] and z₂[θ₂M̃<sub>2</sub>], are different, that is, z₁ ≠ z₂ or θ₁M̃<sub>1</sub> ≠ θ₂M̃<sub>2</sub>. Therefore, z₁[θ₁M̃<sub>1</sub>] is independent of z₂[θ₂M̃<sub>2</sub>], so x[ĩ₁] is independent of x[ĩ₂]. Combining this information with the proof of one-session secrecy, we can prove secrecy of x: we define

$$
\text{prove}^{\text{Secrecy}}(x)(S) = \text{prove}^{\text{1-ses.secr.}}(x)(S) \wedge \bigwedge_{\mu_1, \mu_2 \in S} \text{prove}^{\text{distinct}}(x)(\mu_1, \mu_2)
$$

The proof of bit secrecy is the same as for one-session secrecy:

$$
\mathrm{prove}^{\mathrm{bit\ } \mathrm{secr.}}(x)(S) = \mathrm{prove}^{\mathrm{1-ses.secr.}}(x)(S)
$$
The proof of (one-session or bit) secrecy is justified by the following proposition.

**Proposition 1 (One-session or bit) secrecy)** Consider a process $Q_0$ that satisfies Properties 4 and 5. Let sp be 1-ses.secr.(x), Secrecy(x), or bit secr.(x). Let $S = \{\mu | \mu$ follows a definition of x\}.

If prove<sup>sp</sup>(S) and for all evaluation contexts C acceptable for $Q_0$, Pr[C[$Q_0$] $\le$ not{prove<sup>sp</sup>(S)}] $\le$ p(C), then $Q_0$ satisfies sp with public variables V ($x \notin V$) up to probability p' such that p'(C) = p(C[$C_{sp}$]) and Bound<sub>$Q_0$</sub>(V $\cup$ {x}, sp, D<sub>false</sub>, p).

The proof of Proposition 1 relies on the following definitions and lemma. We have

$$ \{\text{noleak}(x[\widetilde{M}'], \mathcal{I}, \mathcal{F})\} = (\forall \mathcal{I}, \neg \bigwedge \mathcal{F}) \vee ((x \notin V) \wedge \bigwedge_{\mu} x[\widetilde{M}] \text{ in } Q_0) $$

– if $^{\mu}x[\widetilde{M}]$ is in $M$ in an assignment let $y[i] = M$, $M$ is built from replication indices, variables, function applications, and conditionals, and the current call is not inside a call to nolek(y, -, -), then

$$ \{\text{noleak}(y[\theta i], \mathcal{I} \cup \{\theta i\}, \mathcal{F} \cup \theta \mathcal{F}_{\mu} \cup \{\theta \widetilde{M} = \widetilde{M'}\})\} $$
where $\theta$ is a renaming of $\tilde{i}$ to fresh replication indices

– if $^{\mu}x[\widetilde{M}]$ is in event $e(M_1, \dots, M_{k-1}, C[^{\mu}x[\widetilde{M}]], M_{k+1}, \dots, M_m)$ for $C$ defined in Figure 18, then true

– otherwise, $\forall (\mathcal{I} \cup \theta I_{\mu}), \neg \bigwedge (\mathcal{F} \cup \theta \mathcal{F}_{\mu} \cup \{\theta \widetilde{M} = \widetilde{M'}\})$
where $\theta$ is a renaming of $I_{\mu}$ to fresh replication indices)

$\{\text{noleak}(x[\widetilde{M}'], \mathcal{I}, \mathcal{F})\}$ is the logical formula that is guaranteed when nolek($x[\widetilde{M}']$, $\mathcal{I}$, $\mathcal{F}$) succeeds, up to a small probability computed by the equational prover and that bounds Pr[$C[Q_0]$ $\le$ not{$\{\text{noleak}(x[\widetilde{M}'], \mathcal{I}, \mathcal{F})\}$}]. It is obtained by collecting formulas guaranteed by each call to "$\mathcal{F}$ yields a contradiction": such a call guarantees $\forall \tilde{z} \in \tilde{T}''$, $\neg \bigwedge \mathcal{F}$ up to a small probability that it evaluates, where $\tilde{z}$ are the non-process variables in $\mathcal{F}$ and $\tilde{T}''$ are their types. In the definition of $\{\text{noleak}(x[\widetilde{M}'], \mathcal{I}, \mathcal{F})\}$, the notation $\forall \mathcal{I}$ means that all variables in $\mathcal{I}$ are universally quantified in their respective types. The notation $\forall (\mathcal{I} \cup \theta I_{\mu})$ is similar. We have similarly

$$ \{\text{prove}^{\text{1-ses.secr.}}(x)(\mu)\} = \begin{cases} \{\text{noleak}(\theta \text{defRand}_{\mu}(x), \{\theta I_{\mu}\}, \theta \mathcal{F}_{\mu})\} & \text{if } \text{defRand}_{\mu}(x) \text{ is defined,} \\ \text{where } \theta \text{ is a renaming of } I_{\mu} \text{ to fresh replication indices} & \text{false otherwise} \end{cases} $$

$$ \{\text{prove}^{\text{1-ses.secr.}}(x)(S)\} = \bigwedge_{\mu \in S} \{\text{prove}^{\text{1-ses.secr.}}(x)(\mu)\} $$

$$ \{\text{prove}^{\text{distinct}}(x)(\mu_1, \mu_2)\} = (z_1 \neq z_2) \vee (\forall \tilde{i}_1, \forall \tilde{i}_2, \neg \bigwedge \theta_1 \mathcal{F}_{\mu_1} \cup \theta_2 \mathcal{F}_{\mu_2} \cup \{\theta_1 \widetilde{M}_1 = \theta_2 \widetilde{M}_2, \tilde{i}_1 \neq \tilde{i}_2\}) $$

$$ \{\text{prove}^{\text{Secrecy}}(x)(S)\} = \{\text{prove}^{\text{1-ses.secr.}}(x)(S)\} \wedge \bigwedge_{\mu_1, \mu_2 \in S} \{\text{prove}^{\text{distinct}}(x)(\mu_1, \mu_2)\} $$

$$ \{\text{prove}^{\text{bit secr.}}(x)(S)\} = \{\text{prove}^{\text{1-ses.secr.}}(x)(S)\} $$

The only semantic rules that can add $x[\tilde{a}]$ to the environment $E$ are (NewT), (LetT), (FindT1), (New), (Let), (Find1), and (Output). (get is excluded by Property 4.) By Corollary 1, the target term or process of these rules is a subterm or subprocess of $Q_0$ up to renaming of channels. Hence, the target configuration Conf of these rules is at some program point $\mu$ in
Tr. In this case, we say that $x[\tilde{a}]$ is defined just before $\mu$ in a trace Tr. Furthermore, given $x[\tilde{a}]$ and Tr, there is at most one program point $\mu$ such that $x[\tilde{a}]$ is defined just before $\mu$ in Tr, by Lemma 28.

Let sp be 1-ses.secr.(x), Secrecy(x), or bit secr.(x). Let Tr be a trace of $C[C_{sp}[Q_0]]$. Let $E = E_{Tr}$. We define the set Tidx(Tr) of indices of successful test queries as follows:

* When sp is 1-ses.secr.(x): Let $\mu_t$ be the program point of the input that performs the test query in $Q_{1-ses.secr.}(x): \mu_t c_s(u_1: [1, n_1], ..., u_m: [1, n_m])$. If there is an (Output) reduction in Tr with $\mu' = \mu_t$, we define $E'$ to be the environment after that reduction. If $x[E(u_1), ..., E(u_m)] \in \text{Dom}(E')$, we let $\text{Tidx}(Tr) = \{\epsilon\}$ (the empty sequence of indices). Otherwise, $\text{Tidx}(Tr) = \emptyset$.

* When sp is Secrecy(x): Let $\mu_t$ be the program point of the input that performs the test query in $Q_{\text{Secrecy}}(x): \mu_t c_s(u_1: [1, n_1], ..., u_m: [1, n_m])$. Let $\text{Tidx}(Tr) = \{a \in [1, n_s] | \text{ there is an (Output) reduction in Tr with } \mu' = \mu_t, \sigma'(\tilde{i}) = a, \text{ and } x[E(u_1[a]), ..., E(u_m[a])] \in \text{Dom}(E') \text{ where } E' \text{ is the environment after that reduction, and for all (Output) reductions in Tr before the latter reduction, with } \mu' = \mu_t, \sigma'(\tilde{i}) = a', E(u_1[a']) = E(u_1[a]), ..., \text{ and } E(u_m[a']) = E(u_m[a]), \text{ we have } x[E(u_1[a]), ..., E(u_m[a])] \notin \text{Dom}(E'') \text{ where } E'' \text{ is the environment after that reduction.} \}$.

The test query with index a is the first successful test query for $x[E(u_1[a]), ..., E(u_m[a])]$, so $x[E(u_1[a]), ..., E(u_m[a])]$ is defined at that test query, that is, $x[E(u_1[a]), ..., E(u_m[a])] \in \text{Dom}(E')$. For all previous test queries on the same indices, $x[E(u_1[a]), ..., E(u_m[a])]$ was not defined, that is, $x[E(u_1[a]), ..., E(u_m[a])] \notin \text{Dom}(E'')$. The bound $n_s$ and the variables $u_1, ..., u_m$ come from $Q_{\text{Secrecy}}(x)$.

* When sp is bit secr.(x): Let $\mu_t$ be the program point of the input in $Q_{\text{bit secr.}}(x): \mu_t c_s''(b' : \text{bool})$. If there is an (Output) reduction in Tr with $\mu' = \mu_t$, we define $E'$ to be the environment after that reduction. If $x \in \text{Dom}(E')$, we let $\text{Tidx}(Tr) = \{\epsilon\}$. Otherwise, $\text{Tidx}(Tr) = \emptyset$.

Let $\text{Tpp}(Tr) = \{\mu | \exists a \in \text{Tidx}(Tr), x[E(u_1[a]), ..., E(u_m[a])] \text{ is defined just before } \mu \text{ in Tr}\}$. When sp is bit secr.(x), $m = 0$, so this definition reduces to $\text{Tpp}(Tr) = \emptyset$ if $\text{Tidx}(Tr) = \emptyset$ and $\text{Tpp}(Tr) = \{\mu_\epsilon\}$ where $x$ is defined just before $\mu_\epsilon$ in Tr otherwise. We write $Tr \vdash sp$ when $Tr \vdash [[\text{prove}^{sp}(\text{Tpp}(Tr))]]$.

**Lemma 35** Consider a process $Q_0$ that satisfies Properties 4 and 5. Let sp be 1-ses.secr.(x), Secrecy(x), or bit secr.(x). Let C be an evaluation context acceptable for $C_{sp}[Q_0]$ with any public variables V ($x \notin V$) that does not contain S nor $\bar{S}$. We have

$$ \Pr[C[C_{sp}[Q_0]] : S \wedge sp] = \Pr[C[C_{sp}[Q_0]] : \bar{S} \wedge sp]. $$

**Proof of the cases** sp = 1-ses.secr.(x) and sp = Secrecy(x) Let Tr be a full trace of $C[C_{sp}[Q_0]]$ such that $Tr \vdash sp$ and $b$ is defined in Tr, that is, $b \in \text{Dom}(E_{Tr})$.

Let $E = E_{Tr}$. Let $\tilde{i}$ be the current replication indices at the definition of $x$ in $Q_0$. For $j \in \text{Tidx}(Tr)$, let $\tilde{a}_j = E(u_1[j]), ..., E(u_m[j])$, so that the test query at index $j$ tests $x[\tilde{a}_j]$. Let $\text{Conf}_j$ be the target configuration of the semantic rule that adds $x[\tilde{a}_j]$ to $E$, and $\mu_j$ be such that $x[\tilde{a}_j]$ is defined just before $\mu_j$ in Tr. So $\text{Conf}_j$ is at program point $\mu_j$ in Tr. Let $z_j[\tilde{M}_j] = \text{defRand}_{\mu_j}(x)$ (which is always defined since $\mu_j \in \text{Tpp}(Tr)$ and $Tr \vdash sp$, so $Tr \vdash [[\text{prove}^{1-ses.secr.}(x)(\mu_j)]]$). Let $\tilde{b}_j$ be such that $E, \{\tilde{i} \mapsto \tilde{a}_j\}, \tilde{M}_j \Downarrow \tilde{b}_j$. Then $x[\tilde{a}]$ is added to the environment $E$ by (NewT), (LetT), (New), or (Let), we have $E(x[\tilde{a}_j]) = E(z_j[\tilde{b}_j])$, and $z_j[\tilde{b}_j]$ is chosen at random by (NewT)
or (New) in Tr by definition of $\text{defRand}_{\mu_j}(x)$. Let us prove that, for all $j_1 \neq j_2$ in $\text{Tidx}(Tr)$, we have $z_{j_1} \neq z_{j_2}$ or $\tilde{b}_{j_1} \neq \tilde{b}_{j_2}$.

* When sp is 1-ses.secr.(x), this is trivially true since $\text{Tidx}(Tr)$ contains at most one element.

* When sp is Secrecy(x), we have $\mu_{j_1}, \mu_{j_2} \in \text{Tpp}(Tr)$ and $\text{Tr} \vdash \text{Secrecy}(x)$, so we have $\text{Tr} \vdash \{[\text{prove}^{\text{distinct}}(x)(\mu_{j_1}, \mu_{j_2})]\}$, so $z_{j_1} \neq z_{j_2}$ or $\text{Tr} \vdash \forall \tilde{i}_1, \forall \tilde{i}_2, \neg \bigwedge \theta_1 \mathcal{F}_{\mu_{j_1}} \cup \theta_2 \mathcal{F}_{\mu_{j_2}} \cup \{\theta_1 \tilde{M}_{j_1} = \theta_2 \tilde{M}_{j_2}, \tilde{i}_1 \neq \tilde{i}_2\}$ where $\theta_1$ and $\theta_2$ are two distinct renamings of $\tilde{i}$ to fresh replication indices, $\tilde{i}_1 = \theta_1 \tilde{i}$, and $\tilde{i}_2 = \theta_2 \tilde{i}$. In the latter case, let $\rho = \{\tilde{i}_1 \mapsto \tilde{a}_{j_1}, \tilde{i}_2 \mapsto \tilde{a}_{j_2}\}$. We have $\sigma_{\text{Conf}_{j_1}} = [\tilde{i} \mapsto \tilde{a}_{j_1}]$. By Corollary 3, $\text{Tr}, \rho \vdash \theta_1 \mathcal{F}_{\mu_{j_1}}$. Similarly, $\text{Tr}, \rho \vdash \theta_2 \mathcal{F}_{\mu_{j_2}}$. Since $j_1 \neq j_2$, $\tilde{a}_{j_1} \neq \tilde{a}_{j_2}$. (By construction of $\text{Tidx}(Tr)$, we consider only the first successful test query for a certain $x[\tilde{a}_j]$.) So $\text{Tr}, \rho \vdash \tilde{i}_1 \neq \tilde{i}_2$. Therefore, $\text{Tr}, \rho \vdash \theta_1 \tilde{M}_{j_1} \neq \theta_2 \tilde{M}_{j_2}$, so $\tilde{b}_{j_1} \neq \tilde{b}_{j_2}$.

For $j \in \text{Tidx}(Tr)$, let us choose elements $v_j$ in $T$, where $T$ is the type of $x$. Let us consider the following two sets of traces:

1. $\text{Tr}$ modified by choosing $b = \text{true}$ and $z_j[\tilde{b}_j] = v_j$ for all $j \in \text{Tidx}(Tr)$. (The variable $b$ is chosen and used in $Q_{sp}$. Note that the variable $y$ of $Q_{sp}$ is not defined when $b = \text{true}$. This set contains a single trace.)

2. $\text{Tr}$ modified by choosing $b = \text{false}$ and $y[j] = v_j$ and $z_j[\tilde{b}_j] = v'_j$ for any $v'_j \in T$, for all $j \in \text{Tidx}(Tr)$. (This set contains $|T|^{\text{Tidx}(Tr)}$ traces.)

The trace $\text{Tr}$ is one of the traces in these two sets: just choose the values of $b$, $z_j[\tilde{b}_j]$, and $y[j]$ if $b$ is false that are used in $\text{Tr}$.

We show by induction on the derivation of these traces $\text{Tr}_s$ ($\text{Tr}_1$ is in set 1 and $\text{Tr}_2$ is in set 2) that they have matching configurations $\text{Conf}'_s = E_s, \sigma, M_s, \mathcal{T}, \mu\mathcal{E}v_s, \text{Conf}'_s = E_s, Q_s, \text{Ch}, \text{or } \text{Conf}'_s = E_s, (\sigma, P_s), Q_s, \text{Ch}, \mathcal{T}, \mu\mathcal{E}v_s$ for $s \in \{1, 2\}$ that differ as follows:

* $E_1(b) = \text{true}$ while $E_2(b) = \text{false}$.

* $E_1(u'_s[j])$ when sp is Secrecy(x) and $E_1(y[j])$ are undefined even when $E_2(u'_s[j])$ and $E_2(y[j])$ are defined for some indices $j \in \text{Tidx}(Tr)$.

* $E_1(z[\tilde{a}])$ differs from $E_2(z[\tilde{a}])$ for some $z$ and $\tilde{a}$ such that for some $\tilde{M}, \mathcal{I}, \mathcal{F}$, we have $\text{Tr} \vdash \{[\text{noleak}(z[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\text{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{a}) \wedge \neg \mathcal{F}$.

* Values inside $M_1$ and $M_2$ may differ when $\text{Conf}'_s$ (for $s \in \{1, 2\}$) occurs in the derivation of

$$E_s, \sigma, \text{let } y[\tilde{i}] = M \text{ in } M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma\tilde{i}] \mapsto a_s], \sigma, M', \mathcal{T}, \mu\mathcal{E}v_s$$

or of $E_s, (\sigma, \text{let } y[\tilde{i}] = M \text{ in } P), Q_s, \text{Ch}, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma\tilde{i}] \mapsto a_s], (\sigma, P), Q_s, \text{Ch}, \mathcal{T}, \mu\mathcal{E}v_s$

where $M$ is built from replication indices, variables, function applications, and conditionals and for some $\tilde{M}, \mathcal{I}, \mathcal{F}$, we have $\text{Tr} \vdash \{[\text{noleak}(y[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\text{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \sigma\tilde{i}) \wedge \neg \mathcal{F}$.

* Terms $M_1$ and $M_2$ may differ when $\text{Conf}'_s$ (for $s \in \{1, 2\}$) occurs in the derivation of

$$E_s, \sigma, \text{event } e(\tilde{M}_s); M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, \text{event } e(\tilde{M}'_s); M', \mathcal{T}, \mu\mathcal{E}v_s$$

or of $E_s, (\sigma, \text{event } e(\tilde{M}_s); P), Q_s, \text{Ch}, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, (\sigma, \text{event } e(\tilde{M}'_s); P), Q_s, \text{Ch}, \mathcal{T}, \mu\mathcal{E}v_s$
where the terms $M_s$ match and the only rules above this reduction and under $Conf'_s$ are (CtxT) with matching simple contexts any number of times followed by (CtxT) with context **event** $e(a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_l)$; $N$ or (Ctx) with context **event** $e(a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_l)$; $P$ once, where

- a simple context is a context of the form $x[a_1, \dots, a_{k-1}, \dots, N_{k+1}, \dots, N_m]$ or $f(a_1, \dots, a_{k-1}, \dots, N_{k+1}, \dots, N_m)$ for some $x, f, k, m, a_1, \dots, a_{k-1}, N_{k+1}, \dots, N_m$,

- simple contexts $C_s$ (for $s \in \{1, 2\}$) match when $C_s = x[a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_m]$ or $C_s = f(a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_m)$ for some $x, f, k, m, a_{s,1}, \dots, a_{s,k-1}, N_{k+1}, \dots, N_m$, and

- terms $M_s$ (for $s \in \{1, 2\}$) match when $M_s = a_{s,0}$, or $M_s = x[a_{s,1}, \dots, a_{s,k-1}, M'_s, N_{k+1}, \dots, N_m]$ or $M_s = f(a_{s,1}, \dots, a_{s,k-1}, M'_s, N_{k+1}, \dots, N_m)$ for some $x, f, k, m, a_{s,0}, a_{s,1}, \dots, a_{s,k-1}, N_{k+1}, \dots, N_m$ and matching $M'_s$.

* Terms $M_1$ and $M_2$ (resp. processes $P_1$ and $P_2$) may differ when

$$M_s = C_1[\dots C_k[\text{event } e(\tilde{M}_s); M']\dots],$$

$$P_s = C_0[C_1[\dots C_k[\text{event } e(\tilde{M}_s); M']\dots]],$$

$$\text{or } P_s = \text{event } e(\tilde{M}_s); P$$

where $k \in \mathbb{N}$, $C_1, \dots, C_k$ are term contexts defined in Figure 6, $C_0$ is a process context defined in Figure 10, and the terms $\tilde{M}_s$ match, for $s \in \{1, 2\}$.

* Arguments of events in $\mu\mathcal{E}v_1$ and $\mu\mathcal{E}v_2$ may differ.

* The events $S$ and $\bar{S}$ are swapped: when $\mu\mathcal{E}v_1$ contains $S$, $\mu\mathcal{E}v_2$ contains $\bar{S}$, and conversely.

* Some additional configurations corresponding to the execution $Q_{sp}$ differ.

The proof can be sketched as follows. The different choice of $b$ leads to $E_1(b) = \text{true}$ and $E_2(b) = \text{false}$. The only semantic rule that reads the environment is (Var), when it evaluates an occurrence of the variable in question. By Definition 7, $b \notin \text{var}(Q_0) \cup V$, so the only occurrences of $b$ are in $Q_{sp}$.

If the adversary sends $\tilde{a}$ on channel $c_s$ and $x[\tilde{a}]$ is not defined, then $Q_{sp}$ simply yields. If the adversary sends $\tilde{a}$ on channel $c_s$ and $x[\tilde{a}]$ is defined, then $\tilde{a} = \tilde{a}_j$ for some $j \in \text{Tidx}(\text{Tr})$. In set 1, $E_1(b) = \text{true}$, so $Q_{sp}$ outputs $E_1(x[\tilde{a}_j]) = E_1(z_j[\tilde{b}_j]) = v_j$. In set 2, $E_2(b) = \text{false}$, so when it is the first time that the adversary sends $\tilde{a}$ on channel $c_s$ and $x[\tilde{a}]$ is defined, $Q_{sp}$ chooses a fresh $y[j]$ equal to $v_j$, and outputs $E_2(y[j]) = v_j$; when the adversary sends again $\tilde{a}$ on channel $c_s$, $Q_{sp}$ finds $u'_s = j$ (by construction of $\text{Tidx}(\text{Tr}))$, and outputs $E_2(y[j]) = v_j$. So in both sets, $Q_{sp}$ outputs the same value.

If the adversary sends $b'$ to $c'_s$, then the result of the test $b' = b$ differs between set 1 and set 2, since $E_1(b) \neq E_2(b)$, so if set 1 executes $S$, then set 2 executes $\bar{S}$ and conversely. That is why the events $S$ and $\bar{S}$ are swapped.

By Definition 7, $u'_s, y \notin \text{var}(Q_0) \cup V$, so the only occurrences of $u'_s$ and $y$ are in $Q_{sp}$. Therefore, the changes that come from differences in the definition of $u'_s$ and $y$ are already taken into account above.

The value of $E_1(z_j[\tilde{b}_j])$ is different from the one of $E_2(z_j[\tilde{b}_j])$. Since $\text{Tr} \vdash \text{sp}$, we have $\text{Tr} \vdash \{[\text{prove}^{1-\text{ses.secr.}}(x)(\mu_j)]\}$, so $\text{Tr} \vdash \{[\text{noleak}(\theta z_j[\tilde{M}_j], \{\theta I_{\mu_j}\}, \theta \mathcal{F}_{\mu_j})]\}$ where $\theta$ is a renaming of $I_{\mu_j}$ to fresh replication indices. We have $\sigma_{Conf_j} = [I_{\mu_j} \mapsto \tilde{a}_j]$. Let $\rho = \{\theta I_{\mu_j} \mapsto \tilde{a}_j\}$. By Corollary 3, $\text{Tr}, \rho \vdash \theta \mathcal{F}_{\mu_j}$. Moreover, $\text{Tr}, \rho \vdash \theta \tilde{M}_j = \tilde{b}_j$. So $\text{Tr} \vdash \exists \theta I_{\mu_j}, (\theta \tilde{M}_j = \tilde{b}_j) \wedge \neg \theta \mathcal{F}_{\mu_j}$.
Hence, for $\tilde{M} = \theta\tilde{M}_j$, $\mathcal{I} = \{\theta I_{\mu_j}\}$, and $\mathcal{F} = \theta\mathcal{F}_{\mu_j}$, we have $\mathrm{Tr} \vdash \{[\mathrm{noleak}(z_j[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\mathrm{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{b}_j) \wedge \wedge \mathcal{F}$.

The difference between $E_1(z[\tilde{a}])$ and $E_2(z[\tilde{a}])$ for $z$ and $\tilde{a}$ such that for some $\tilde{M}, \mathcal{I}, \mathcal{F}$, we have $\mathrm{Tr} \vdash \{[\mathrm{noleak}(z[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\mathrm{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{a}) \wedge \wedge \mathcal{F}$ has consequences when (Var) evaluates $z[\tilde{a}]$:

$$E_s, \sigma, \mu z[\tilde{a}], \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, E_s(z[\tilde{a}]), \mathcal{T}, \mu\mathcal{E}v_s.$$

By Lemma 8, Property 5 applied to the configuration $\mathrm{Conf} = E_s, \sigma, \mu z[\tilde{a}], \mathcal{T}, \mu\mathcal{E}v_s$ with $l = 0$, we have

$$E'_s, \sigma, \mu z[\tilde{M}'], \mathcal{T}', \mu\mathcal{E}v'_s \xrightarrow{1} E'_s, \sigma, \mu z[\tilde{a}], \mathcal{T}, \mu\mathcal{E}v_s$$

by any number of applications of (CxtT), where $\mu z[\tilde{M}']$ is a subterm of $C[C_{sp}[Q_0]]$. Furthermore, if the evaluation of $\tilde{M}'$ itself uses (Var) that evaluates a $z[\tilde{a}]$ that differs, we replace $z[\tilde{M}']$ by the smallest subterm of $\tilde{M}'$ that evaluates a $z[\tilde{a}]$ that differs. By this replacement, we guarantee that the evaluation of $\tilde{M}'$ proceeds in the same way in set 1 and set 2 and yields the same $\tilde{a}$. Recall that $\tilde{M}'$ are simple terms by Invariants 2 and 5, so the evaluation of $\tilde{M}'$ does not change $E_s, \mathcal{T}, \mu\mathcal{E}v_s$. So we have

$$E_s, \sigma, \mu z[\tilde{M}'], \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, \mu z[\tilde{a}], \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, E_s(z[\tilde{a}]), \mathcal{T}, \mu\mathcal{E}v_s$$

for $s \in \{1, 2\}$, where $\mu z[\tilde{M}']$ is a subterm of $C[C_{sp}[Q_0]]$, by any number of applications of (CxtT) followed by one application of (Var). Let $\theta$ be a renaming of $I_\mu$ to fresh replication indices and $\rho = \{\theta I_\mu \mapsto \sigma I_\mu\}$. By Corollary 3, $\mathrm{Tr}_s, \rho \vdash \theta\mathcal{F}_\mu$. Moreover, $E_s, \sigma, \tilde{M}' \Downarrow \tilde{a}$, so $E_s, \rho, \theta\tilde{M}' \Downarrow \tilde{a}$. Since $E_{\mathrm{Tr}_s}$ extends $E_s$, we have $\mathrm{Tr}_s, \rho \vdash \theta\tilde{M}' = \tilde{a}$. Since $\mathrm{Tr}$ is among the traces $\mathrm{Tr}_s$, we have $\mathrm{Tr}, \rho \vdash \theta\mathcal{F}_\mu$ and $\mathrm{Tr}, \rho \vdash \theta\tilde{M}' = \tilde{a}$. There exists $\rho'$ with domain $\mathcal{I}$ such that $\mathrm{Tr}, \rho' \vdash (\tilde{M} = \tilde{a}) \wedge \wedge \mathcal{F}$. So $\mathrm{Tr}, \rho \vdash \rho' \vdash (\mathcal{F} \cup \theta\mathcal{F}_\mu \cup \{\theta\tilde{M}' = \tilde{a}, \tilde{M} = \tilde{a}\})$. Since $\mathrm{Tr} \vdash \{[\mathrm{noleak}(z[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\mathrm{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{a}) \wedge \wedge \mathcal{F}$, we have $\mathrm{Tr} \vdash \neg(\forall \mathcal{I}, \neg \wedge \mathcal{F})$, so $\mathrm{Tr}$ satisfies the second disjunct of $\{[\mathrm{noleak}(z[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$. Therefore, $z \notin V$, so the occurrence of $\mu z[\tilde{M}']$ evaluated above is either in $Q_{sp}$, and in this case $z$ is actually $x$ and this case has already been studied above, or in $Q_0$. In the latter situation, we are in one of the following three cases:

* $\mu z[\tilde{M}']$ is in $M$ in an assignment $\mu' \mathrm{let} y[\tilde{i}] = M$ in $Q_0$, $M$ is built from replication indices, variables, function applications, and conditionals and $\mathrm{Tr} \vdash \{[\mathrm{noleak}(y[\theta\tilde{i}], \mathcal{I} \cup \{\theta\tilde{i}\}, \mathcal{F} \cup \theta\mathcal{F}_\mu \cup \{\theta\tilde{M}' = \tilde{M}\})]\}$ where $\theta$ is a renaming of $\tilde{i}$ to fresh replication indices. Let $\tilde{M}'' = \theta\tilde{i}$, $\mathcal{I}' = \mathcal{I} \cup \{\theta\tilde{i}\}$, and $\mathcal{F}' = \mathcal{F} \cup \theta\mathcal{F}_\mu \cup \{\theta\tilde{M}' = \tilde{M}\}$. Since $\mu'$ is above $\mu$, by Lemma 6, there is a configuration inside $\mu'$ before $\mathrm{Conf}$ in $\mathrm{Tr}$. By Lemma 8 applied to that configuration (Property 1 when the assignment is a process, Property 5 with $l = 0$ when it is a term), the assignment $\mu' \mathrm{let} y[\tilde{i}] = M$ is evaluated by

$$E_s, \sigma, \mu' \mathrm{let} y[\tilde{i}] = M \text{ in } M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma\tilde{i}] \mapsto a_s], \sigma, M', \mathcal{T}, \mu\mathcal{E}v_s$$

$$\text{or } E_s, (\sigma, \mu' \mathrm{let} y[\tilde{i}] = M \text{ in } P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma\tilde{i}] \mapsto a_s], (\sigma, P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s$$

for $s \in \{1, 2\}$. We have $\mathrm{Tr} \vdash \{[\mathrm{noleak}(y[\tilde{M}''], \mathcal{I}', \mathcal{F}')]\}$. Moreover $\tilde{i} = I_\mu$ and $\mathrm{Tr}, \rho \cup \rho' \vdash \theta\tilde{i} = \sigma\tilde{i}$ by definition of $\rho$. Hence $\mathrm{Tr}, \rho \cup \rho' \vdash \tilde{M}'' = \sigma\tilde{i}$ and $\mathrm{Tr}, \rho \cup \rho' \vdash \mathcal{F}'$, so $\mathrm{Tr} \vdash \exists \mathcal{I}', (\tilde{M}'' = \sigma\tilde{i}) \wedge \wedge \mathcal{F}'$. Hence we are in a case in which different values inside terms $M_1$ and $M_2$ are allowed. Furthermore, the added values $E_s(y[\sigma\tilde{i}]) = a_s$ may differ. Let $\tilde{a}' = \sigma\tilde{i}$. We have $\mathrm{Tr} \vdash \{[\mathrm{noleak}(y[\tilde{M}''], \mathcal{I}', \mathcal{F}')]\}$ and $\mathrm{Tr} \vdash \exists \mathcal{I}', (\tilde{M}'' = \tilde{a}') \wedge \wedge \mathcal{F}',$ so $E_1(y[\tilde{a}'])$ is indeed allowed to differ from $E_2(y[\tilde{a}'])$.
• $^{µ}z[\widetilde{M}']$ is in $^{µ'}$event $e(M_1, \dots, M_{k-1}, C[^{µ}z[\widetilde{M}']], M_{k+1}, \dots, M_m)$ in $Q_0$, for $C$ defined in Figure 18. Since $µ'$ is above $µ$, by Lemma 6, there is a configuration inside $µ'$ before Conf in Tr. By Lemma 8 applied to that configuration (Property 1 when the event is a process, Property 5 with $l = 0$ when it is a term), the evaluation of the event starts from a configuration at $µ'$ in Tr. The evaluation of event $e(M_1, \dots, M_{k-1}, C[^{µ}z[\widetilde{M}']], M_{k+1}, \dots, M_m)$ first evaluates $M_1, \dots, M_{k-1}$ to values using (CtxT) or (Ctx) with an event context. (If they evaluated to abort event values, $C[^{µ}z[\widetilde{M}']]$ would not be evaluated.) Then if evaluates the context $C$: new $y[i] : T$; $C$ is evaluated by (NewT), let $y[i] = M$ in $C$ is evaluated by (LetT), if $M$ then $C$ else $N'$ is evaluated by (IfT1) ($M$ must evaluate to true because otherwise, $^{µ}z[\widetilde{M}']$ would not be evaluated), if $M$ then $N$ else $C$ is evaluated by (IfT2) ($M$ must not evaluate to true because otherwise, $^{µ}z[\widetilde{M}']$ would not be evaluated), event $e(\widetilde{M})$; $C$ is evaluated by (EventT), and find contexts are evaluated by rules for find, until we reach

$$ \text{event } e(a_{s,1}, \dots, a_{s,k-1}, C_{s,1}[\dots C_{s,l}[^{\mu}z[\widetilde{M}']]\dots], M_{k+1}, \dots, M_m) $$

for $s \in \{1, 2\}$, where $C_{s,1}, \dots, C_{s,l}$ are matching simple contexts. (Values may differ in case $M_1, \dots, M_{k-1}$, or terms in $C$ contain other occurrences of variables whose value differs.) At this point, the reduction proceeds as follows:

$$ \begin{array}{l} E_s, \sigma, \text{ event } e(\widetilde{M}_s); M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, \text{ event } e(\widetilde{M}'_s); M', \mathcal{T}, \mu\mathcal{E}v_s \\ \text{or } E_s, (\sigma, \text{ event } e(\widetilde{M}_s); P), Q_s, \mathcal{Ch}, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, (\sigma, \text{ event } e(\widetilde{M}'_s); P), Q_s, \mathcal{Ch}, \mathcal{T}, \mu\mathcal{E}v_s \end{array} $$

by (Var), (CtxT) with matching simple contexts any number of times followed by (CtxT) or (Ctx) with context event $e(a_{s,1}, \dots, a_{s,k-1}, [], M_{k+1}, \dots, M_m)$; ... once, where

$$ \begin{array}{l} \widetilde{M}_s = a_{s,1}, \dots, a_{s,k-1}, C_{s,1}[\dots C_{s,l}[^{\mu}z[\widetilde{M}']]\dots], M_{k+1}, \dots, M_m \\ \text{and } \widetilde{M}'_s = a_{s,1}, \dots, a_{s,k-1}, C_{s,1}[\dots C_{s,l}[a_s]\dots], M_{k+1}, \dots, M_m \end{array} $$

for $s \in \{1, 2\}$. Further reductions still manipulate configurations of the same form until the event itself is executed by (EventT) or (Event), which adds the event $e$ with possibly different arguments to $\mu\mathcal{E}v_s$.

• $Tr \vdash \forall (\mathcal{I} \cup \theta I_\mu), \neg \bigwedge (\mathcal{F} \cup \theta \mathcal{F}_\mu \cup \{\theta \widetilde{M}' = \widetilde{M}\})$ where $\theta$ is a renaming of $I_\mu$ to fresh replication indices. We have $Tr, \rho \cup \rho' \vdash \neg \bigwedge (\mathcal{F} \cup \theta \mathcal{F}_\mu \cup \{\theta \widetilde{M}' = \widetilde{M}\})$. That yields a contradiction, so this case does not happen.

The sequence of events $\mu\mathcal{E}v_1$ (resp. $\mu\mathcal{E}v_2$) is never read by the semantic rules. It is only read by the distinguisher. Therefore, changes in this sequence of events do not modify the rest of the trace.

That concludes the proof that traces in set 1 and set 2 match.

Furthermore, the trace in set 1 and the traces in set 2 have the same probability. All full traces of $C[C_{sp}[Q_0]]$ that define $b$ and that satisfy sp belong to set 1 or to set 2 for some Tr (for instance using the trace in question as Tr). Therefore, these sets form a partition of the full traces of $C[C_{sp}[Q_0]]$ that define $b$ and that satisfy sp, and the sets that execute S have the same probability as the sets that execute $\bar{S}$. Moreover, the traces of $C[C_{sp}[Q_0]]$ that do not define $b$ execute neither S nor $\bar{S}$. So $\text{Pr}[C[C_{sp}[Q_0]] : S \land sp] = \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \land sp]$. $\square$

**Proof of the case** sp = bit secr.(x) Let Tr be a full trace of $C[C_{sp}[Q_0]]$ such that $Tr \vdash sp$. Let $E = E_{Tr}$.
If $Tidx(Tr) = \emptyset$, then $Tr$ executes neither $S$ nor $\bar{S}$.

Otherwise, $Tidx(Tr) = \{\epsilon\}$ and $x$ is defined in $Tr$, that is, $x \in \text{Dom}(E)$. Let $Conf_{\epsilon}$ be the target configuration of the semantic rule that adds $x$ to $E$, and $\mu_{\epsilon}$ be such that $x$ is defined just before $\mu_{\epsilon}$ in $Tr$. So $Conf_{\epsilon}$ is at program point $\mu_{\epsilon}$ in $Tr$. Let $z_{\epsilon}[\widetilde{M}_{\epsilon}] = \text{defRand}_{\mu_{\epsilon}}(x)$ (which is always defined since $\mu_{\epsilon} \in \text{Tpp}(Tr)$ and $Tr \vdash sp$, so $Tr \vdash \{[\text{prove}^{1\text{-ses.secr.}(x)}(\mu_{\epsilon})]\}$). Let $\tilde{b}_{\epsilon}$ be such that $E, \emptyset, \widetilde{M}_{\epsilon} \vdash \tilde{b}_{\epsilon}$. Then $x$ is added to the environment $E$ by (NewT), (LetT), (New), or (Let), we have $E(x) = E(z_{\epsilon}[\tilde{b}_{\epsilon}])$, and $z_{\epsilon}[\tilde{b}_{\epsilon}]$ is chosen at random by (NewT) or (New) in $Tr$ by definition of $\text{defRand}_{\mu_{\epsilon}}(x)$.

Let us consider the following two traces:

1. $Tr_1$ is $Tr$ modified by choosing $z_{\epsilon}[\tilde{b}_{\epsilon}] = \text{true}$.

2. $Tr_2$ is $Tr$ modified by choosing $z_{\epsilon}[\tilde{b}_{\epsilon}] = \text{false}$.

The trace $Tr$ is one of these two traces: just choose the value $z_{\epsilon}[\tilde{b}_{\epsilon}]$ that is used in $Tr$.

We show by induction on the derivation of these traces $Tr_s$ that they have matching configurations $Conf'_s = E_s, \sigma, M_s, \mathcal{T}, \mu\mathcal{E}v_s, Conf'_s = E_s, Q_s, Ch, \text{ or } Conf'_s = E_s, (\sigma, P_s), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s$ for $s \in \{1, 2\}$ that differ as follows:

* $E_1(z[\tilde{a}])$ differs from $E_2(z[\tilde{a}])$ for some $z$ and $\tilde{a}$ such that for some $\widetilde{M}, \mathcal{I}, \mathcal{F}$, we have $Tr \vdash \{[\text{noleak}(z[\widetilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $Tr \vdash \exists \mathcal{I}, (\widetilde{M} = \tilde{a}) \wedge \mathcal{F}$.

* Values inside $M_1$ and $M_2$ may differ when $Conf'_s$ (for $s \in \{1, 2\}$) occurs in the derivation of

$$E_s, \sigma, \text{let } y[i] = M \text{ in } M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma i] \mapsto a_s], \sigma, M', \mathcal{T}, \mu\mathcal{E}v_s$$

$$\text{or of } E_s, (\sigma, \text{let } y[i] = M \text{ in } P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s[y[\sigma i] \mapsto a_s], (\sigma, P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s$$

where $M$ is built from replication indices, variables, function applications, and conditionals and for some $\widetilde{M}, \mathcal{I}, \mathcal{F}$, we have $Tr \vdash \{[\text{noleak}(y[\widetilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $Tr \vdash \exists \mathcal{I}, (\widetilde{M} = \sigma i) \wedge \mathcal{F}$.

* Terms $M_1$ and $M_2$ may differ when $Conf'_s$ (for $s \in \{1, 2\}$) occurs in the derivation of

$$E_s, \sigma, \text{event } e(\widetilde{M}_s); M', \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, \sigma, \text{event } e(\widetilde{M}'_s); M', \mathcal{T}, \mu\mathcal{E}v_s$$

$$\text{or of } E_s, (\sigma, \text{event } e(\widetilde{M}_s); P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s \xrightarrow{1} E_s, (\sigma, \text{event } e(\widetilde{M}'_s); P), Q_s, Ch, \mathcal{T}, \mu\mathcal{E}v_s$$

where the terms $M_s$ match and the only rules above this reduction and under $Conf'_s$ are (CtxT) with matching simple contexts any number of times followed by (CtxT) with context $\text{event } e(a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_l); N$ or (Ctx) with context $\text{event } e(a_{s,1}, \dots, a_{s,k-1}, \dots, N_{k+1}, \dots, N_l); P$ once, where simple contexts and matching are defined as in the cases $sp = \text{1-ses.secr.}(x)$ and $sp = \text{Secrecy}(x)$.

* Terms $M_1$ and $M_2$ (resp. processes $P_1$ and $P_2$) may differ when

$$M_s = C_1[\dots C_k[\text{event } e(\widetilde{M}_s); M']\dots],$$

$$P_s = C_0[C_1[\dots C_k[\text{event } e(\widetilde{M}_s); M']\dots]],$$

$$\text{or } P_s = \text{event } e(\widetilde{M}_s); P$$

where $k \in \mathbb{N}$, $C_1, \dots, C_k$ are term contexts defined in Figure 6, $C_0$ is a process context defined in Figure 10, and the terms $\widetilde{M}_s$ match, for $s \in \{1, 2\}$.
* Arguments of events in $\mu\mathcal{E}v_1$ and $\mu\mathcal{E}v_2$ may differ.

* The events $S$ and $\bar{S}$ are swapped: when $\mu\mathcal{E}v_1$ contains $S$, $\mu\mathcal{E}v_2$ contains $\bar{S}$, and conversely.

* Some additional configurations corresponding to the execution $Q_{sp}$ differ.

The proof can be sketched as follows.

If the adversary sends $b'$ to $c''_s$, then $x$ is defined (since $\text{Tidx}(\text{Tr}) = \{\epsilon\}$) and the result of the test $x = b'$ differs between $\text{Tr}_1$ and $\text{Tr}_2$, since $E_1(x) = E_1(z_\epsilon[\tilde{b}_\epsilon]) = \text{true} \neq E_2(x) = E_2(z_\epsilon[\tilde{b}_\epsilon]) = \text{false}$, so if $\text{Tr}_1$ executes $S$, then $\text{Tr}_2$ executes $\bar{S}$ and conversely. That is why the events $S$ and $\bar{S}$ are swapped.

The value of $E_1(z_\epsilon[\tilde{b}_\epsilon])$ is different from the one of $E_2(z_\epsilon[\tilde{b}_\epsilon])$. Since $\text{Tr} \vdash \text{sp}$, we have $\text{Tr} \vdash \{[\text{prove}^{1\text{-ses.secr.}(x)}(\mu_\epsilon)]\}$, so $\text{Tr} \vdash \{[\text{noleak}(\theta z_\epsilon[\tilde{M}_\epsilon], \{\theta I_{\mu_\epsilon}\}, \theta \mathcal{F}_{\mu_\epsilon})]\}$ where $\theta$ is a renaming of $I_{\mu_\epsilon}$ to fresh replication indices. Here, $I_{\mu_\epsilon}$ is empty since $x$ is defined under no replication. We have $\sigma_{Conf_\epsilon} = []$. Let $\rho = \emptyset$. By Corollary 3, $\text{Tr}, \rho \vdash \theta \mathcal{F}_{\mu_\epsilon}$. Moreover, $\text{Tr}, \rho \vdash \theta \tilde{M}_\epsilon = \tilde{b}_\epsilon$. So $\text{Tr} \vdash \exists \theta I_{\mu_\epsilon}, (\theta \tilde{M}_\epsilon = \tilde{b}_\epsilon) \wedge \bigwedge \theta \mathcal{F}_{\mu_\epsilon}$. Hence, for $\tilde{M} = \theta \tilde{M}_\epsilon$, $\mathcal{I} = \{\theta I_{\mu_\epsilon}\}$, and $\mathcal{F} = \theta \mathcal{F}_{\mu_\epsilon}$, we have $\text{Tr} \vdash \{[\text{noleak}(z_\epsilon[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\text{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{b}_\epsilon) \wedge \bigwedge \mathcal{F}$.

The difference between $E_1(z[\tilde{a}])$ and $E_2(z[\tilde{a}])$ for $z$ and $\tilde{a}$ such that for some $\tilde{M}, \mathcal{I}, \mathcal{F}$, we have $\text{Tr} \vdash \{[\text{noleak}(z[\tilde{M}], \mathcal{I}, \mathcal{F})]\}$ and $\text{Tr} \vdash \exists \mathcal{I}, (\tilde{M} = \tilde{a}) \wedge \bigwedge \mathcal{F}$ has consequences when (Var) evaluates $z[\tilde{a}]$, as in the cases $\text{sp} = \text{1-ses.secr.}(x)$ and $\text{sp} = \text{Secrecy}(x)$. That concludes the proof that traces $\text{Tr}_1$ and $\text{Tr}_2$ match.

Furthermore, the traces $\text{Tr}_1$ and $\text{Tr}_2$ have the same probability. All full traces of $C[C_{sp}[Q_0]]$ such that $\text{Tidx}$ is non-empty and that satisfy $\text{sp}$ are $\text{Tr}_1$ or $\text{Tr}_2$ for some $\text{Tr}$ (for instance using the trace in question as $\text{Tr}$). Therefore, $\text{Tr}_1$ and $\text{Tr}_2$ form a partition of the full traces of $C[C_{sp}[Q_0]]$ such that $\text{Tidx}$ is non-empty and that satisfy $\text{sp}$, and half of these traces execute $S$, the other half execute $\bar{S}$. Moreover, the traces of $C[C_{sp}[Q_0]]$ such that $\text{Tidx}$ is empty execute neither $S$ nor $\bar{S}$. So $\text{Pr}[C[C_{sp}[Q_0]] : S \wedge \text{sp}] = \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \wedge \text{sp}]$. $\square$

**Proof of Proposition 1** Let $\text{sp}$ be $\text{1-ses.secr.}(x)$, $\text{Secrecy}(x)$, or bit $\text{secr.}(x)$. Let $C$ be an evaluation context acceptable for $C_{sp}[Q_0]$ with public variables $V$ ($x \notin V$) that does not contain $S$ nor $\bar{S}$. We have

$$
\begin{align*}
\text{Adv}_{Q_0}^{sp}(C) &= \text{Pr}[C[C_{sp}[Q_0]] : S] - \text{Pr}[C[C_{sp}[Q_0]] : \bar{S}] \\
&= \text{Pr}[C[C_{sp}[Q_0]] : S \wedge \text{sp}] + \text{Pr}[C[C_{sp}[Q_0]] : S \wedge \neg \text{sp}] \\
&\quad - \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \wedge \text{sp}] - \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \wedge \neg \text{sp}] \\
&= \text{Pr}[C[C_{sp}[Q_0]] : S \wedge \neg \text{sp}] - \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \wedge \neg \text{sp}] \quad \text{by Lemma 35} \\
&\leq \text{Pr}[C[C_{sp}[Q_0]] : \neg \text{sp}] \\
&\leq \text{Pr}[C[C_{sp}[Q_0]] : \neg \{[\text{prove}^{sp}(\{\mu \mid \mu \text{ follows a definition of } x\})]\}] \\
&\qquad \text{because, for all } \text{Tr}, \text{Tpp}(\text{Tr}) \subseteq \{\mu \mid \mu \text{ follows a definition of } x\} \\
&\leq \text{Pr}[C[C_{sp}[Q_0]] \leq \neg \{[\text{prove}^{sp}(\{\mu \mid \mu \text{ follows a definition of } x\})]\}] \quad \text{by Lemma 1} \\
&\leq p(C[C_{sp}[]]) = p'(C)
\end{align*}
$$

So $Q_0$ satisfies $\text{sp}$ with public variables $V$ up to probability $p'$. Moreover,

$$
\begin{align*}
\text{Adv}_{Q_0}(C[C_{sp}[], \text{sp}, \text{Dfalse}] &= \text{Pr}[C[C_{sp}[Q_0]] : S] - \text{Pr}[C[C_{sp}[Q_0]] : \bar{S} \lor \text{NonUnique}_{Q_0}] \\
&\leq \text{Adv}_{Q_0}^{sp}(C) \leq p(C[C_{sp}[]])
\end{align*}
$$

so $\text{Bound}_{Q_0}(V \cup \{x\}, \text{sp}, \text{Dfalse}, p)$. $\square$
**Example 5** Using assumptions on cryptographic primitives, the process $Q_0$ of Example 1 can be transformed into the following process $Q_0''$:

$$ 
\begin{align*}
Q_0'' &= start(); \text{ new } x_k : T_k; \text{ new } x_{mk} : T_{mk}; \bar{c}\langle\rangle; (Q_A'' | Q_B'') \\
Q_A'' &= !^{i \le n} c_A[i](\cdot); \text{ new } x'_k : T_k; \text{ new } x_r : T_r; \\
\text{let } x_m &\text{: bitstring} = \text{enc}'(Z_k, k, x'_r) \text{ in} \\
&\overline{c_A[i]\langle x_m, \text{mac}'(x_m, x_{mk})\rangle} \\
Q_B'' &= !^{i' \le n} c_B[i'](x'_m, x_{ma}); \\
\text{find } u \le n &\text{ suchthat } \text{defined}(x_m[u], x'_k[u]) \land \\
&x'_m = x_m[u] \land \text{verify}'(x'_m, x_{mk}, x_{ma}) \text{ then} \\
\text{let } x_k'' &\text{: } T_k = x'_k[u] \text{ in } \overline{c_B[i']\langle\rangle}
\end{align*}
$$

and $Q_0 \stackrel{x_k''}{\approx} Q_0''$. In order to prove the one-session secrecy of $x_k''$, we notice that $x_k''$ is defined by let $x_k'' : T_k = x'_k[u]$, the only variable access to $x_k''$ in $Q_0''$ is let $x_k'' : T_k = x'_k[u]$, and $x_k''$ is not used in $Q_0''$. So by Proposition 1, $Q_0''$ satisfies the one-session secrecy of $x_k''$ without public variables up to probability 0. (We have $\text{defRand}_\mu(x_k'') = x'_k[u]$ and $\text{[noleak}(x_k'[\theta i], \mathcal{I}, \mathcal{F})\text{]} = (\forall \mathcal{I}, \neg \bigwedge \mathcal{F}) \lor ((x_k'' \notin \mathcal{V}) \land \text{[noleak}(x_k''[\theta i], \mathcal{I}', \mathcal{F}')\text{]}) = \text{true}$ since $x_k'' \notin \mathcal{V}$, $x_k'' \notin \mathcal{V}$, and $\text{[noleak}(x_k''[\theta i], \mathcal{I}', \mathcal{F}')\text{]} = (\forall \mathcal{I}', \neg \bigwedge \mathcal{F}') \lor ((x_k'' \notin \mathcal{V}) \land \text{true}) = \text{true}$. So $\text{Pr}[C[Q_0''] \le \text{[prove}^{1-\text{ses.secr.}(x_k'')}(S)\text{]}] = 0$.) By Lemma 20, the process $Q_0$ of Example 1 also satisfies the one-session secrecy of $x_k''$ without public variables up to probability $p'(C) = 2p(C[C_{1-\text{ses.secr.}(x_k'')}][\cdot], t_S)$. However, this process does not preserve the secrecy of $x_k''$, because the adversary can force several sessions of $B$ to use the same key $x_k''$, by replaying the message sent by $A$. (Accordingly, $\text{prove}^{\text{Secrecy}(x)}(S)$ is not satisfied.)

The criteria given in this section might seem restrictive, but in fact, they should be sufficient for all protocols, provided the previous transformation steps are powerful enough to transform the protocol into a simpler protocol, on which these criteria can then be applied.

## 4.2 Correspondences

### 4.2.1 Example

We illustrate the proof of correspondences on the following example, inspired by the corrected Woo-Lam public key protocol [68]:

$$ 
\begin{align*}
B \to A & : (N, B) \\
A \to B & : \{pk_A, B, N\}_{sk_A}
\end{align*}
$$

This protocol is a simple nonce challenge: $B$ sends to $A$ a fresh nonce $N$ and its identity. $A$ replies by signing the nonce $N$, $B$'s identity, and $A$'s public key (which we use here instead of $A$'s identity for simplicity: this avoids having to relate identities and keys; CryptoVerif can obviously also handle the version with $A$'s identity). The signatures are assumed to be (existentially) unforgeable under chosen message attacks (UF-CMA) [45], so, when $B$ receives the signature, $B$ is convinced that $A$ is present. The signature cannot be a replay because the nonce $N$ is signed.

In our calculus, this protocol is encoded by the following process $G_0$, explained below:

$$ 
\begin{align*}
G_0 &= c_0(); \text{ new } rk_A : \text{keyseed}; \text{ let } pk_A = \text{pkgen}(rk_A) \text{ in} \\
    &\text{let } sk_A = \text{skgen}(rk_A) \text{ in } \overline{c_1\langle pk_A\rangle}; (Q_A | Q_B)
\end{align*}
$$
$$
\begin{align*}
Q_A &= !^{i_A \le n} c_2[i_A](x_N : \text{nonce}, x_B : \text{host}); \\
    &\quad \text{event } e_A(pk_A, x_B, x_N); \text{ new } r : \text{seed}; \\
    &\quad \overline{c_3[i_A]} \langle \text{sign}(\text{concat}(pk_A, x_B, x_N), sk_A, r) \rangle \\
Q_B &= !^{i_B \le n} c_4[i_B](x_{pk_A} : \text{pkey}); \text{ new } N : \text{nonce}; \\
    &\quad \overline{c_5[i_B]} \langle N, B \rangle; c_6[i_B](s : \text{signature}); \\
    &\quad \text{if verify}(\text{concat}(x_{pk_A}, B, N), x_{pk_A}, s) \text{ then} \\
    &\quad \text{if } x_{pk_A} = pk_A \text{ then event } e_B(x_{pk_A}, B, N)
\end{align*}
$$

The process $G_0$ is assumed to run in interaction with an adversary, which also models the network. $G_0$ first receives an empty message on channel $c_0$, sent by the adversary. Then, it chooses randomly with uniform probability a bitstring $rk_A$ in the type *keyseed*, by the construct new $rk_A$ : *keyseed*. Then, $G_0$ generates the public key $pk_A$ corresponding to the coins $rk_A$, by calling the public-key generation algorithm *pkgen*. Similarly, $G_0$ generates the secret key $sk_A$ by calling skgen. It outputs the public key $pk_A$ on channel $c_1$, so that the adversary has this public key.

After outputting this message, the control passes to the receiving process, which is part of the adversary. Several processes are then made available, which represent the roles of A and B in the protocol: the process $Q_A | Q_B$ is the parallel composition of $Q_A$ and $Q_B$; it makes simultaneously available the processes defined in $Q_A$ and $Q_B$. Let $Q'_A$ and $Q'_B$ be such that $Q_A = !^{i_A \le n} Q'_A$ and $Q_B = !^{i_B \le n} Q'_B$. The replication $!^{i_A \le n} Q'_A$ represents $n$ copies of the process $Q'_A$, indexed by the replication index $i_A$. The process $Q'_A$ begins with an input on channel $c_2[i_A]$; the channel is indexed with $i_A$ so that the adversary can choose which copy of the process $Q'_A$ receives the message by sending it on channel $c_2[i_A]$ for the appropriate value of $i_A$. The situation is similar for $Q'_B$, which expects a message on channel $c_4[i_B]$. The adversary can then run each copy of $Q'_A$ or $Q'_B$ simply by sending a message on the appropriate channel $c_2[i_A]$ or $c_4[i_B]$.

The process $Q'_B$ first expects on channel $c_4[i_B]$ a message $x_{pk_A}$ in the type *pkey* of public keys. This message is not really part of the protocol. It serves for starting a new session of the protocol, in which *B* interacts with the participant of public key $x_{pk_A}$. For starting a session between *A* and *B*, this message should be $pk_A$. Then, $Q'_B$ chooses randomly with uniform probability a nonce *N* in the type *nonce*. The type *nonce* is *large*: collisions between independent random numbers chosen uniformly in a large type are eliminated by CryptoVerif. $Q'_B$ sends the message (*N*, *B*) on channel $c_5[i_B]$. The control then passes to the receiving process, included in the adversary. This process is expected to forward this message (*N*, *B*) on channel $c_2[i_A]$, but may proceed differently in order to mount an attack against the protocol.

Upon receiving a message $(x_N, x_B)$ on channel $c_2[i_A]$, where the bitstring $x_N$ is in the type *nonce* and $x_B$ in the type *host*, the process $Q'_A$ executes the event $e_A(pk_A, x_B, x_N)$. This event does not change the state of the system. Events just record that a certain program point has been reached, with certain values of the arguments of the event. Then, $Q'_A$ chooses randomly with uniform probability a bitstring $r$ in the type *seed*; this random bitstring is next used as coins for the signature algorithm. Finally, $Q'_A$ outputs the signed message $\{pk_A, x_B, x_N\}_{sk_A}$. (The function *concat* concatenates its arguments, with information on the length of these arguments, so that the arguments can be recovered from the concatenation.) The control then passes to the receiving process, which should forward this message on channel $c_6[i_B]$ if it wishes to run the protocol correctly.

Upon receiving a message $s$ on $c_6[i_B]$, $Q'_B$ verifies that the signature $s$ is correct and, if $x_{pk_A} = pk_A$, that is, if $B$ runs a session with $A$, it executes the event $e_B(x_{pk_A}, B, N)$. Our goal is to prove that, if event $e_B$ is executed, then event $e_A$ has also been executed. However, when $B$ runs a session with a participant other than $A$, it is perfectly correct that $B$ terminates without