different trade-offs. For instance, Maude-NPA (Meadows, 1996; Escobar et al., 2006) and Tamarin (Schmidt et al., 2012) support more equational theories, at the cost of a more costly verification or by requiring user intervention.

These limitations suggest areas for future work. For instance, we might improve the precision of the analysis to avoid false attacks, by adding more information into the clauses. We might support more equational theories, by implementing unification and resolution modulo associativity and commutativity. We might improve the support for mutable state, possibly by integrating StatVerif (Arapinis et al., 2011) and extending it. The proof of equivalences is also an area in which further research could be done, perhaps by combining manual and automatic proofs. For instance, a proof of observational equivalence could be decomposed into a family of static equivalences (Abadi and Fournet, 2001) (equivalences between messages), proved automatically by ProVerif, and a manual bisimulation proof. On a more technical side, the user interface of ProVerif could be improved, for instance by displaying attacks graphically. The subsumption tests could be parallelized to improve performance on machines with multiple cores.

Finally, ProVerif verifies specifications of protocols in the symbolic model. One may go further in several directions. First, one may verify specifications of protocols in a more concrete model, such as the computational model, used by cryptographers. Several tools exist for verifying cryptographic primitives and protocols in this model, in particular, CertiCrypt (Barthe et al., 2009; Béguelin et al., 2009) and its successor EasyCrypt (Barthe et al., 2011; Barthe et al., 2014b), and CryptoVerif (Blanchet, 2008a). They are generally more delicate to use than symbolic protocol verifiers. We plan to modify ProVerif and CryptoVerif to make their input languages compatible, so that the same input file can be used to verify a protocol in both tools, to find attacks or obtain a symbolic proof in ProVerif, or obtain a computational proof in CryptoVerif. Second, instead of verifying specifications, one may verify runnable implementations of protocols. This verification is important because new attacks may appear in the implementation. Some tools for verifying implementations rely on ProVerif as a back-end (see §5.3).
There exist other approaches, by extracting models from implementations for other symbolic (O’Shea, 2008) or computational (Bhargavan et al., 2007; Aizatulin et al., 2012) verifiers, by generating implementations from models by compilation (Song et al., 2001; Milicia, 2002; Pozza et al., 2004; Pironti and Sisto, 2010; Almeida et al., 2013; Cadé and Blanchet, 2013; Cadé and Blanchet, 2015), or by direct verification of the implementation, for instance by typing (Bengtson et al., 2011; Bhargavan et al., 2010; Swamy et al., 2011; Fournet and Kohlweiss, 2011; Bhargavan et al., 2013), by model-checking (Chaki and Datta, 2009), or by the general-purpose C verifier VCC (Dupressoir et al., 2011). Going even further, one may wish to take into account side-channels attacks, that is, physical attacks, which may rely for instance on timing, power consumption, or fault injection, and are not considered in the computational model. Taking such attacks into account in mechanized verification tools is still at its beginning (Barthe et al., 2014a).
Acknowledgments

This survey borrows material from previous surveys (Blanchet, 2012b; Blanchet, 2014) and from my habilitation thesis (Blanchet, 2008b).

Much research on ProVerif has been done with co-authors: in alpha-
betical order, Martín Abadi, Xavier Allamigeon, Vincent Cheval, Cédric
Fournet, Andreas Podelski, and Ben Smyth. I would like to thank them
for their contributions. I also thank Ben Smyth for helpful comments
on a draft of this survey.
# Appendices
Proof of Theorem 3.5

**Theorem 3.5.** Let $P_0$ be a closed biprocess and $\mathcal{N}_{\text{priv}}$ be a set of names. If $P_0$ satisfies diff-equivalence with private names $\mathcal{N}_{\text{priv}}$, then $P_0$ satisfies observational equivalence with private names $\mathcal{N}_{\text{priv}}$.

*Proof.* Let us define the relation $\mathcal{R}$ by $C \mathcal{R} C'$ if and only if there exists a configuration $C''$ such that $C = \text{fst}(C'')$, $C' = \text{snd}(C'')$, and for all adversarial contexts $C_1[\_], \dots, C_k[\_]$, there exists no $C_{\text{bad}}$ such that $C_1[\dots C_k[C'')] \to^* C_{\text{bad}} \uparrow$. The relation $\mathcal{R}$ is symmetric and satisfies the three conditions of Definition 3.6:

1. Suppose $C = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $P \downarrow_a$ and $C \nrightarrow C'$. For some term $M$ and process $P$, we have $\text{out}(a, M)$; $P \in P$ with $a \in \mathcal{N}_{\text{pub}}$. Moreover, there exists a configuration $C''$ such that $C = \text{fst}(C'')$, $C' = \text{snd}(C'')$, and for all adversarial contexts $C_1[\_], \dots, C_k[\_]$, there exists no $C_{\text{bad}}$ such that $C_1[\dots C_k[C']] \to^* C_{\text{bad}} \uparrow$. Hence $C'' = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $P_0$ with $\text{out}(N_0, M_0)$; $P_0 \in P_0$ and $\text{fst}(N_0) = a$. Let $C[\_] = \_ | \text{in}(a, x)$; $\mathbf{0}$. We have $C[C''] = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $P_0 \cup \{\text{in}(a, x); \mathbf{0}\}$ since $a \in \mathcal{N}_{\text{pub}}$. Since $C \nrightarrow C'$, $C[C'']$ does not diverge, so $\text{fst}(N_0) = \text{fst}(a)$ if and only if $\text{snd}(N_0) = \text{snd}(a)$. Therefore, $\text{snd}(N_0) = a$, so $C' = \text{snd}(C'') = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\text{snd}(P_0)$ with $\text{out}(a, \text{snd}(M_0))$; $\text{snd}(P_0) \in \text{snd}(P_0)$, so $C' \downarrow_a$.
$$ \{\alpha_1 \dots \alpha_k P_0\} \cup \{\alpha_1 \dots \alpha_{i-1} Q_i \mid i \in \{1, \dots, k\}\}, $$

where $\alpha_i$ is a bijective renaming of the names in $\alpha_{i+1} \dots \alpha_k \mathcal{N}_{\text{priv}} \cup \bigcup_{j=i+1}^k \alpha_{i+1} \dots \alpha_{j-1} \tilde{n}_j$ to names not in $\text{fn}(Q_i)$ that leaves names in $\mathcal{N}_{\text{pub}}_{i+1}$ unchanged. So

$$ \begin{aligned} (\alpha_1 \dots \alpha_k)^{-1} C_1[\dots C_k[\mathcal{C}'']] = & \\ & ((\alpha_1 \dots \alpha_k)^{-1} \mathcal{N}_{\text{pub}}_1, \mathcal{N}_{\text{priv}} \cup \bigcup_{i=1}^k (\alpha_i \dots \alpha_k)^{-1} \tilde{n}_i), \\ & \{P_0\} \cup \{(\alpha_i \dots \alpha_k)^{-1} Q_i \mid i \in \{1, \dots, k\}\}. \end{aligned} $$

We write $\prod_{i=1}^k P_i$ for $P_1 \mid \dots \mid P_k$. Let $Q' = \prod_{i=1}^k (\alpha_i \dots \alpha_k)^{-1} Q_i$, $\{\tilde{n}\} = \text{fn}(Q') \setminus \mathcal{N}_{\text{pub}}$ and $Q = \text{new } \tilde{n}; Q'$. The process $Q$ is an $\mathcal{N}_{\text{pub}}$-adversary. Moreover, let us show that $\{\tilde{n}\} \cap \mathcal{N}_{\text{priv}} = \emptyset$. Suppose that $a \in \{\tilde{n}\} \cap \mathcal{N}_{\text{priv}}$. Since $\mathcal{N}_{\text{pub}} \cap \mathcal{N}_{\text{priv}} = \emptyset$, for some $i \in \{1, \dots, n\}$, $a \in \text{fn}((\alpha_i \dots \alpha_k)^{-1} Q_i) \cap \mathcal{N}_{\text{priv}}$, so $\alpha_i \dots \alpha_k a \in \text{fn}(Q_i) \cap \alpha_i \dots \alpha_k \mathcal{N}_{\text{priv}}$. Since $\alpha_i \dots \alpha_k a \in \text{fn}(Q_i)$, $\alpha_{i+1} \dots \alpha_k a \notin \alpha_{i+1} \dots \alpha_k \mathcal{N}_{\text{priv}}$, since $\alpha_i$ renames names in $\alpha_{i+1} \dots \alpha_k \mathcal{N}_{\text{priv}}$ to names not in $\text{fn}(Q_i)$. Therefore, $\alpha_i \dots \alpha_k a \notin \alpha_i \dots \alpha_k \mathcal{N}_{\text{priv}}$. Contradiction. Hence we have proved $\{\tilde{n}\} \cap \mathcal{N}_{\text{priv}} = \emptyset$.

Moreover, we have the following property: if $(\mathcal{N}_{\text{pub}}', \mathcal{N}_{\text{priv}}')$, $\mathcal{P} \to^{*\uparrow}$, then $(\mathcal{N}_{\text{pub}}'', \mathcal{N}_{\text{priv}}'')$, $\alpha \mathcal{P} \to^{*\uparrow}$, where $\mathcal{N}_{\text{pub}}'' \cap \mathcal{N}_{\text{priv}}'' = \emptyset$, $\alpha$ is a bijective renaming, and $\text{fn}(\alpha \mathcal{P}) \subseteq \mathcal{N}_{\text{pub}}'' \cup \mathcal{N}_{\text{priv}}''$. This property is easy to prove by induction on the length of the trace. From this property and $C_1[\dots C_k[\mathcal{C}'']] \to^{*\uparrow}$, we derive

$$ (\alpha_1 \dots \alpha_k)^{-1} C_1[\dots C_k[\mathcal{C}'']] \to^{*\uparrow}, $$

so

$$ \begin{aligned} & (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \{P_0, Q\} \to^* \\ & (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}} \cup \{\tilde{n}\}), \{P_0\} \cup \{(\alpha_i \dots \alpha_k)^{-1} Q_i \mid i \in \{1, \dots, k\}\} \to^{*\uparrow}. \end{aligned} $$

This property contradicts the hypothesis of theorem. This contradiction allows us to conclude the proof. $\square$
Proofs for Chapter 4

These proofs use the notations and definitions of (Abadi et al., 2016). In particular, they use the notion of extended processes A (Abadi et al., 2016, §2.1), with associated domain dom(A) (Abadi et al., 2016, §2.1), structural equivalence ≡ and reduction relation → (Abadi et al., 2016, §2.2); simple contexts (Abadi et al., 2016, §A); partial normal forms, with associated structural equivalence ≁ and reduction relation →$_{◦}$ (Abadi et al., 2016, §B.2); and the labeled semantics α →$_{◦}$ of (Abadi et al., 2016, §B.2).

**B.1 Proof of Proposition 4.1**

**Lemma B.1.** If $E, \mathcal{P} \to E', \mathcal{P}'$, then $[E, \mathcal{P}] \stackrel{\wedge}{\equiv} [E', \mathcal{P}']$ or $[E, \mathcal{P}] \to_{\diamond} [E', \mathcal{P}']$.

*Proof.* By cases on the applied reduction rule.

* Case (Red Nil). We have $\mathcal{P} = \mathcal{P}' \cup \{0\}$. When $\mathcal{P}' \neq \emptyset$, we have $[E, \mathcal{P}] \stackrel{\wedge}{\equiv} [E', \mathcal{P}']$ by PAR-0. When $\mathcal{P}' = \emptyset$, we have $[E, \mathcal{P}] = [E', \mathcal{P}']$, so we also have $[E, \mathcal{P}] \stackrel{\wedge}{\equiv} [E', \mathcal{P}']$.

* Case (Red Par). We have $[E, \mathcal{P}] \stackrel{\wedge}{\equiv} [E', \mathcal{P}']$ by PAR-A and PAR-C.
* Case (Red Repl). We have $[[E, \mathcal{P}]] \stackrel{\wedge}{=} [[E', \mathcal{P}')]$ by REPL.

* Case (Red Res). We have $[[E, \mathcal{P}]] \stackrel{\wedge}{=} [[E', \mathcal{P}]]$ by NEW-PAR.

* Case (Red I/O''). Recall that the channels and output message do not contain destructors, so we have

$$E, \mathcal{P} = E, \mathcal{P}_0 \cup \{ \text{out}(N, M); Q, \text{in}(N', x); P \} \to \\ E, \mathcal{P}_0 \cup \{ Q, P^{M/x} \} = E', \mathcal{P}'$$

where $N =_{\epsilon} N'$. By REWRITE, we can replace $N'$ with $N$ in the input channel of the encoded process, so we have $[[E, \mathcal{P}]] \to_{\diamond} [[E', \mathcal{P}]]$ by COMM.

* Case (Red Cond 1''). We have

$$E, \mathcal{P} = E, \mathcal{P}_0 \cup \{ \text{if } D \text{ then } P \text{ else } Q \} \to E, \mathcal{P}_0 \cup \{ P \} = E', \mathcal{P}'$$

where $D \Downarrow M'$ and $M' =_{\epsilon} true$. Recall that all conditions are of the form $D = (M = N)$. Since $D \Downarrow M'$ and $M' =_{\epsilon} true$, we have $M =_{\epsilon} N$. By REWRITE, we can replace $N$ with $M$ in the condition of the encoded process, so we have $[[E, \mathcal{P}]] \to_{\diamond} [[E', \mathcal{P}]]$ by THEN.

* Case (Red Cond 2''). We have

$$E, \mathcal{P} = E, \mathcal{P}_0 \cup \{ \text{if } D \text{ then } P \text{ else } Q \} \to E, \mathcal{P}_0 \cup \{ Q \} = E', \mathcal{P}'$$

where $D \Downarrow M$ and $M \neq_{\epsilon} true$. Recall that all conditions are of the form $D = (M = N)$. Since $D \Downarrow M'$ and $M' \neq_{\epsilon} true$, we have $M \neq_{\epsilon} N$. The terms $M$ and $N$ are ground since configurations contain closed processes, so we have $[[E, \mathcal{P}]] \to_{\diamond} [[E', \mathcal{P}]]$ by ELSE.

All cases may use PAR-A and PAR-C to reorganize parallel compositions and NEW-C to reorder restrictions. □

We write $\prod_{i=1}^n P_i$ for any parallel composition $P_1 | \cdots | P_n$ modulo associativity and commutativity. We define the property $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P')$ by $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P')$ if and only if $E = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\})$, $\mathcal{P} = \{P_1, \dots, P_n\}$, and
1. $\mathcal{P}_{\text{red}} = \{P_i\}, [[P_i]] \xrightarrow{\diamond} P''$ and $P' \equiv \nu\tilde{a}.(P'' | \prod_{j \neq i} [[P_j]])$ for some $i \in \{1, \dots, n\}$ and $P'',$ or

2. $\mathcal{P}_{\text{red}} = \{P_i, P_j\}, [[P_i]] \xrightarrow{N(x)} P'', [[P_j]] \xrightarrow{\nu x \cdot \overline{N}(x)} A'', \text{ and } P' \equiv \nu\tilde{a}, x.((P'' | A'') | \prod_{k \neq i, j} [[P_k]])$ for some $i, j \in \{1, \dots, n\}, P'', A'', x,$ and ground term $N$.

Intuitively, this property means that $[[E, \mathcal{P}]] \xrightarrow{\diamond} P'$ by reducing the processes in $\mathcal{P}_{\text{red}}$.

**Lemma B.2.** If $[[E, \mathcal{P}]] \xrightarrow{\diamond} P$, then $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P)$ for some $\mathcal{P}_{\text{red}}$.

*Proof.* Let $E = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\})$ and $\mathcal{P} = \{P_1, \dots, P_n\}$. We have $\nu\tilde{a}.([P_1] | \dots | [P_n]) \xrightarrow{\diamond} P$. By (Abadi et al., 2016, Lemma B.21(2)), $[[P_1]] | \dots | [[P_n]] \xrightarrow{\diamond} P'$ and $P \equiv \nu\tilde{a}.P'$ for some $P'$.

We show the following property by induction on the cardinal of $I$, using (Abadi et al., 2016, Lemma B.18(1)):

P1. if $\prod_{i \in I} P_i$ is closed, $\alpha$ is $\nu x \cdot \overline{N}(x)$ or $N(M)$ for some ground $N$ and $\prod_{i \in I} P_i \xrightarrow{\alpha} \diamond P'$, then there exist $i \in I$ and $P''$ such that $P_i \xrightarrow{\alpha} \diamond P''$ and $P' \equiv P'' | \prod_{j \in I \setminus \{i\}} P_j$

Next, we show the following property:

P2. if $\prod_{i \in I} P_i$ is closed and $\prod_{i \in I} P_i \xrightarrow{\diamond} P'$, then either there exist $i \in I$ and $P''$ such that $P_i \xrightarrow{\alpha} \diamond P''$ and $P' \equiv P'' | \prod_{j \in I \setminus \{i\}} [[P_j]]$, or there exist $i, j \in I$, $P'', A'', x$ and a ground term $N$ such that $P_i \xrightarrow{N(x)} \diamond P'', P_j \xrightarrow{\nu x \cdot \overline{N}(x)} \diamond A'', \text{ and } P' \equiv \nu x.((P'' | A'') | \prod_{k \in I \setminus \{i, j\}} P_k)$.

by induction on the cardinal of $I$. If $|I| = 1$, then the first case obviously holds. If $|I| > 1$, then $\prod_{i \in I} P_i = (\prod_{i \in I_1} P_i) | (\prod_{i \in I_2} P_i)$ for two disjoint non-empty sets $I_1$ and $I_2$ such that $I = I_1 \cup I_2$. By (Abadi et al., 2016, Lemma B.21(1)), one of the following four cases holds:

1. $\prod_{i \in I_1} P_i \xrightarrow{\diamond} P''$ and $P' \equiv P'' | (\prod_{i \in I_2} P_i)$ for some $P''$;

2. $\prod_{i \in I_2} P_i \xrightarrow{\diamond} P''$ and $P' \equiv P'' | (\prod_{i \in I_1} P_i)$ for some $P''$;

3. $\prod_{i \in I_1} P_i \xrightarrow{N(x)} \diamond P'', \prod_{i \in I_2} P_i \xrightarrow{\nu x \cdot \overline{N}(x)} \diamond A'', \text{ and } P' \equiv \nu x.(P'' | A'')$ for some $P'', A'', x$, and ground term $N$;
4. $\prod_{i \in I_1} P_i \xrightarrow{\nu x \cdot \overline{N\langle x \rangle}} \diamond A'', \prod_{i \in I_2} P_i \xrightarrow{N(x)} \diamond P'', \text{ and } P' \equiv \nu x.(P'' | A'')$ for some $P'', A'', x$, and ground term $N$.

In the first two cases, we conclude by induction hypothesis. In the last two cases, we conclude by P1.

By applying P2 to $\prod_{i=1}^n [[P_i]] \to_{\diamond} P'$, either there exist $i \in \{1, \dots, n\}$ and $P''$ such that $[[P_i]] \to_{\diamond} P''$ and $P' \equiv P'' | \prod_{j \neq i} [[P_j]]$, or there exist $i, j \in \{1, \dots, n\}, P'', A'', x$, and a ground term $N$ such that $[[P_i]] \xrightarrow{N(x)} \diamond P'', [[P_j]] \xrightarrow{\nu x \cdot \overline{N\langle x \rangle}} \diamond A'', \text{ and } P' \equiv \nu x.((P'' | A'') | \prod_{k \neq i, j} [[P_k]])$. In the first case, we obtain $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P)$ with $\mathcal{P}_{\text{red}} = \{P_i\}$, and in the second case, we obtain $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P)$ with $\mathcal{P}_{\text{red}} = \{P_i, P_j\}$. $\square$

As in (Abadi et al., 2016), we define the size of processes by induction on the syntax, such that $size(!P) = 1 + 2 \times size(P)$ and, when $P$ is not a replication, $size(P)$ is one plus the size of the immediate subprocesses of $P$. When $\mathcal{P} = \{P_1, \dots, P_n\}$ is a multiset of processes, we define $size(\mathcal{P}) = size(P_1) + \dots + size(P_n)$.

**Lemma B.3.** If $[[E, \mathcal{P}]] \to_{\diamond} P'$, then $E, \mathcal{P} \to^* E', \mathcal{P}'$ and $P' \stackrel{\diamond}{=} [[E', \mathcal{P}']]$ for some $E', \mathcal{P}'$.

*Proof.* Let $E = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\})$ and $\mathcal{P} = \{P_1, \dots, P_n\}$. By Lemma B.2, there exists $\mathcal{P}_{\text{red}}$ such that $\text{Prop}(E, \mathcal{P}, \mathcal{P}_{\text{red}}, P')$. We proceed by induction on $size(\mathcal{P}_{\text{red}})$.

* Case $\mathcal{P}_{\text{red}} = \{P_i\}$, $[[P_i]] \to_{\diamond} P''$, and $P' \equiv \nu \tilde{a}.(P'' | \prod_{j \neq i} [[P_j]])$ for some $i \in \{1, \dots, n\}$ and $P''$. By (Abadi et al., 2016, Lemma B.21), we have the following cases:

1. $[[P_i]] = Q_1 | Q_2$ for some $Q_1$ and $Q_2$, and one of the following cases holds:

(a) $Q_1 \to_{\diamond} Q'_1$ and $P'' \equiv Q'_1 | Q_2$ for some $Q'_1$,

(b) $Q_1 \xrightarrow{N(x)} \diamond A$, $Q_2 \xrightarrow{\nu x \cdot \overline{N\langle x \rangle}} \diamond B$, and $P'' \equiv \nu x.(A | B)$ for some $A, B, x$, and ground term $N$,

and two symmetric cases obtained by swapping $Q_1$ and $Q_2$.
By definition of $[[\cdot]]$, we have $P_i = Q_1'' | Q_2'', Q_1 = [[Q_1'']]$, and $Q_2 = [[Q_2'']]$ for some $Q_1''$ and $Q_2''$. By (Red Par), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q_1'', Q_2''\}$. We have $\text{Prop}(E, \mathcal{P}', \mathcal{P}'_{\text{red}}, P')$ with $\mathcal{P}'_{\text{red}} = \{Q_1''\}$ (case a), $\mathcal{P}'_{\text{red}} = \{Q_2''\}$ (symmetric of case a), or $\mathcal{P}'_{\text{red}} = \{Q_1'', Q_2''\}$ (case b and its symmetric), and $\text{size}(\mathcal{P}'_{\text{red}}) < \text{size}(\mathcal{P}_{\text{red}})$ in all cases, so we conclude by induction hypothesis.

2. $[[P_i]] = \nu n.Q, Q \to_{\diamond} Q', \text{ and } P'' \equiv \nu n.Q'$ for some $n, Q$, and $Q'$.

We have $P_i = \text{new } n; Q''$ and $Q = [[Q'']]$ for some $Q''$. By (Red Res), $E, \mathcal{P} \to E', \mathcal{P}'$ where $E' = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\} \cup \{n'\})$, $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q''^{n'/n}\}$, and $n' \notin \mathcal{N}_{\text{pub}} \cup \{\tilde{a}\}$. We have $[[Q''^{n'/n}]] = Q^{n'/n} \to_{\diamond} Q'^{n'/n}$. (We show by induction on the derivation of $Q \to_{\diamond} Q'$ that, if $Q \to_{\diamond} Q'$, then $\sigma Q \to_{\diamond} \sigma Q'$ where $\sigma$ is a bijective renaming.) So we have $\text{Prop}(E', \mathcal{P}', \mathcal{P}'_{\text{red}}, P')$ with $\mathcal{P}'_{\text{red}} = \{Q''^{n'/n}\}$ and $\text{size}(\mathcal{P}'_{\text{red}}) < \text{size}(\mathcal{P}_{\text{red}})$, so we conclude by induction hypothesis.

3. $[[P_i]] = !Q, Q \mid Q \to_{\diamond} Q', \text{ and } P'' \equiv Q' \mid !Q$ for some $Q$ and $Q'$.

We have $P_i = !Q''$ and $Q = [[Q'']]$ for some $Q''$. By (Red Repl) twice, $E, \mathcal{P} \to^* E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \cup \{Q'', Q''\}$. Since $Q \mid Q \to_{\diamond} Q'$, by (Abadi et al., 2016, Lemma B.21), one of the following cases holds:

(a) $Q \to_{\diamond} Q'_1$ and $Q' \equiv Q'_1 \mid Q$ for some $Q'_1$,

(b) $Q \xrightarrow{N(x)}_{\diamond} A, Q \xrightarrow{\nu x \cdot \overline{N\langle x \rangle}}_{\diamond} B$, and $Q' \equiv \nu x.(A \mid B)$ for some $A, B, x$, and ground term $N$,

so we have $\text{Prop}(E, \mathcal{P}', \mathcal{P}'_{\text{red}}, P')$ with $\mathcal{P}'_{\text{red}} = \{Q''\}$ (case a) or $\mathcal{P}'_{\text{red}} = \{Q'', Q''\}$ (case b), and $\text{size}(\mathcal{P}'_{\text{red}}) < \text{size}(\mathcal{P}_{\text{red}})$ in all cases, so we conclude by induction hypothesis.

4. $[[P_i]] = \text{if } M = N \text{ then } Q_1 \text{ else } Q_2 \text{ and either } M =_{\mathcal{E}} N \text{ and } P'' \equiv Q_1, \text{ or } M \neq_{\mathcal{E}} N \text{ and } P'' \equiv Q_2, \text{ for some } M, N, Q_1, \text{ and } Q_2$.
We have $P_i$ = if $M = N$ then $Q'_1$ else $Q'_2$, $Q_1 = [[Q'_1]]$, and $Q_2 = [[Q'_2]]$ for some $Q'_1$ and $Q'_2$.

If $M = \varepsilon N$, then by (Red Cond 1''), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q'_1\}$. We have $[[E, \mathcal{P}')] = \text{new } \tilde{a}; ([[Q'_1]] | \prod_{j \neq i} [P_j]) = \text{new } \tilde{a}; (Q_1 | \prod_{j \neq i} [P_j])$ and $P' \equiv \nu \tilde{a}. (P'' | \prod_{j \neq i} [P_j]) \equiv [[E, \mathcal{P}]]$.

If $M \neq \varepsilon N$, then by (Red Cond 2''), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q'_2\}$. We have $[[E, \mathcal{P}]] = \text{new } \tilde{a}; ([[Q'_2]] | \prod_{j \neq i} [P_j]) = \text{new } \tilde{a}; (Q_2 | \prod_{j \neq i} [P_j])$ and $P' \equiv \nu \tilde{a}. (P'' | \prod_{j \neq i} [P_j]) \equiv [[E, \mathcal{P}]]$.

* Case $\mathcal{P}_{\text{red}} = \{P_i, P_j\}$, $[[P_i]] \xrightarrow{N(x)} \mathcal{P}''$, $[[P_j]] \xrightarrow{\nu x.\bar{N}\langle x \rangle} \mathcal{A}''$, and $\mathcal{P}' \equiv \nu \tilde{a}, x.((\mathcal{P}'' | \mathcal{A}'') | \prod_{k \neq i, j} [P_k])$ for some $i, j \in \{1, \dots, n\}, \mathcal{P}'', \mathcal{A}''$, $x$, and ground term $N$. By (Abadi et al., 2016, Lemma B.18) applied to the transition $[[P_i]] \xrightarrow{N(x)} \mathcal{P}''$, we have the following cases:

1. $[[P_i]] = Q_1 | Q_2$ and either $Q_1 \xrightarrow{N(x)} \mathcal{A}'$ and $\mathcal{P}'' \equiv \mathcal{A}' | Q_2$, or $Q_2 \xrightarrow{N(x)} \mathcal{A}'$ and $\mathcal{A} \equiv Q_1 | \mathcal{A}',$ for some $Q_1, Q_2$, and $\mathcal{A}'$.

We have $P_i = Q'_1 | Q'_2$, $Q_1 = [[Q'_1]]$, and $Q_2 = [[Q'_2]]$ for some $Q'_1$ and $Q'_2$. By (Red Par), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q'_1, Q'_2\}$. We have $\text{Prop}(E, \mathcal{P}', \mathcal{P}'_{\text{red}}, \mathcal{P}')$ with $\mathcal{P}'_{\text{red}} = \{Q'_1, P_j\}$ or $\mathcal{P}'_{\text{red}} = \{Q'_2, P_j\}$ and $\text{size}(\mathcal{P}'_{\text{red}}) < \text{size}(\mathcal{P}_{\text{red}})$, so we conclude by induction hypothesis.

2. $[[P_i]] = \nu n.Q, Q \xrightarrow{N(x)} \mathcal{A}',$ and $\mathcal{P}'' \equiv \nu n.A'$ for some $Q, A'$, and $n$ that does not occur in $N(x)$.

We have $P_i = \text{new } n; Q'$ and $Q = [[Q')]$ for some $Q'$. By (Red Res), $E, \mathcal{P} \to E', \mathcal{P}'$ where $E' = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\} \cup \{n'\})$, $\mathcal{P}' = \mathcal{P} \setminus \{P_i\} \cup \{Q'\{n'/n\}\}$, and $n' \notin \mathcal{N}_{\text{pub}} \cup \{\tilde{a}\}$. We have $[[Q'\{n'/n\}]] = Q\{n'/n\} \xrightarrow{N(x)} \mathcal{A}'\{n'/n\}$. (We show by induction on the derivation of $Q \xrightarrow{N(x)} \mathcal{A}'$ that, if $Q \xrightarrow{N(x)} \mathcal{A}'$, then $\sigma Q \xrightarrow{\sigma N(x)} \sigma \mathcal{A}'$ where $\sigma$ is a bijective renaming.) So we have $\text{Prop}(E', \mathcal{P}', \mathcal{P}'_{\text{red}}, \mathcal{P}')$ with $\mathcal{P}'_{\text{red}} = \{Q'\{n'/n\}, P_j\}$
and $size(P'_{\text{red}}) < size(P_{\text{red}})$, so we conclude by induction hypothesis.

3. $[[P_i]] = !Q, Q \xrightarrow{N(x)} \diamond A', \text{ and } P'' \equiv A' | !Q$ for some $Q$ and $A'$. We have $P_i = !Q'$ and $Q = [[Q']]$ for some $Q'$. By (Red Repl), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \cup \{Q'\}$. We have $\text{Prop}(E', \mathcal{P}', \mathcal{P}'_{\text{red}}, P')$ with $\mathcal{P}'_{\text{red}} = \{Q', P_j\}$ and $\text{size}(\mathcal{P}'_{\text{red}}) < \text{size}(\mathcal{P}_{\text{red}})$, so we conclude by induction hypothesis.

4. $[[P_i]] = N'(x') \cdot Q_1, N =_{\varepsilon} N', \text{ and } P'' \equiv Q_1\{x/x'\}$ for some $Q_1, N'$, and $x'$.

By (Abadi et al., 2016, Lemma B.18) applied to the transition $[[P_j]] \xrightarrow{\nu x. \overline{N}(x)} \diamond A'',$ we distinguish cases on $[[P_j]]$. The first three cases are similar to those for $[[P_i]]$. The last case is $[[P_j]] = \overline{N''}\langle M'' \rangle \cdot Q_2, N =_{\varepsilon} N'', x \notin \text{fv}([P_j])$, and $A'' \equiv Q_2 | \{M''/x\}$ for some $N'', M''$, and $Q_2$.

We have $P_i = \text{in}(N', x'); Q'_1$ and $Q_1 = [[Q'_1]]$ for some $Q'_1$. We also have $P_j = \text{out}(N'', M''); Q'_2$ and $Q_2 = [[Q'_2]]$ for some $Q'_2$. By (Red I/O''), $E, \mathcal{P} \to E, \mathcal{P}'$ where $\mathcal{P}' = \mathcal{P} \setminus \{P_i, P_j\} \cup \{Q'_1\{M''/x'\}, Q'_2\}$ since $N' =_{\varepsilon} N''$. Therefore,

$$ 
\begin{aligned}
[[E, \mathcal{P}')] &= \nu \tilde{a}. ([[Q'_1\{M''/x'\}] | [[Q'_2]] | \prod_{k \neq i, j} [[P_k]]) \\
&= \nu \tilde{a}. (Q_1\{M''/x'\} | Q_2 | \prod_{k \neq i, j} [[P_k]]).
\end{aligned}
$$

Moreover,

$$ 
\begin{aligned}
P' &\equiv \nu \tilde{a}, x. ((P'' | A'') | \prod_{k \neq i, j} [[P_k]]) \\
&\equiv \nu \tilde{a}, x. (Q_1\{x/x'\} | Q_2 | \{M''/x\} | \prod_{k \neq i, j} [[P_k]]) \\
P' &\equiv \nu \tilde{a}. (Q_1\{M''/x'\} | Q_2 | \prod_{k \neq i, j} [[P_k]]
\end{aligned}
$$

since $x$ does not occur free in $Q_2$ and $P_k$ for $k \neq i, j$ since these are closed processes. So $P' = [[E, \mathcal{P}]]$. $\square$

**Proposition 4.1.** If $C \to^* C'$, then $[[C]] \to^* \hat{=} [[C')]$.

Conversely, if $[[C]] \to^* P'$, then $C \to^* C'$ and $P' \hat{=} [[C')]$ for some $C'$.
*Proof.* The first point is proved by induction on the number of steps of $C \to^* C'$, using Lemma B.1. The second point is proved by induction on the number of steps of $[[C]] \to_*^* P'$, using Lemma B.3. $\square$

## B.2 Proof of Propositions 4.2 and 4.3

Let replication contexts $C_i[\_\_]$ be plain contexts generated by the following grammar:

<table><tr><td>$C_i[\_] ::= $</td><td>replication contexts</td></tr><tr><td>$\bar{P} | C_i[\_] $</td><td>hole</td></tr><tr><td>$C_i[\_] | P $</td><td>parallel composition</td></tr><tr><td>$\nu a.C_i[\_] $</td><td>parallel composition</td></tr><tr><td>$!C_i[\_] $</td><td>restriction</td></tr><tr><td>$!C_i[\_] $</td><td>replication</td></tr></table>

We use replication contexts to characterize $P \downarrow_a^\diamond$ without using structural equivalence, by the following lemma:

**Lemma B.4.** We have $P \stackrel{\diamond}{=} C[\bar{a}\langle M\rangle.Q]$ for some $M, Q$, and evaluation context $C[\_]$ that does not bind $a$ if and only if $P = C'_i[\bar{N}'\langle M'\rangle.Q']$ and $N' =_\epsilon a$ for some $N', M', Q'$, and replication context $C'_i[\_]$ that does not bind $a$.

*Proof.* The implication from left to right is an immediate consequence of the following property: If $P \stackrel{\diamond}{=} C_i[\bar{N}\langle M\rangle.Q]$ and $N =_\epsilon a$ for some $N, M, Q$, and replication context $C_i[\_]$ that does not bind $a$, then $P = C'_i[\bar{N}'\langle M'\rangle.Q']$ and $N' =_\epsilon a$ for some $N', M', Q'$, and replication context $C'_i[\_]$ that does not bind $a$. This property is proved by induction on the derivation of $P \stackrel{\diamond}{=} C_i[\bar{a}\langle M\rangle.Q]$.

The converse is proved by unfolding replications in $C'_i$ by REPL and by replacing $N'$ with $a$ by REWRITE. $\square$

**Lemma B.5.** Let $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}$ be a valid configuration and $a \in \mathcal{N}_{\text{pub}}$. If $C_i[\bar{N}\langle M\rangle.Q] = [[P]]$, and $N =_\epsilon a$ for some $P \in \mathcal{P}$, $N, M, Q$, and replication context $C_i$ that does not bind $a$, then $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P} \to^* (\mathcal{N}_{\text{pub}}, \mathcal{N}'_{\text{priv}}), \mathcal{P}'$ with $\bar{N}'\langle M'\rangle.Q' = [[P']]$ and $N' =_\epsilon a$ for some $\mathcal{N}'_{\text{priv}}, \mathcal{P}', P' \in \mathcal{P}', N', M', Q'$.
*Proof.* This lemma is proved by reducing the context $C_!$ by (Red Par), (Red Res), and (Red Repl). More formally, the proof proceeds by induction on the size of the replication context $C_!$[].

* If $C_!$[] = ___, the result is obvious.

* If $C_!$[] = $P'$ | $C'_!$[], then $P = P'_1$ | $P_1$ with $[[P'_1]] = P'$ and $[[P_1]] = C'_![\overline{N}\langle M\rangle.Q]$. We have $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P}_0 \cup \{P'_1|$ $P_1\} \to (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P}_0 \cup \{P'_1, P_1\}$ by (Red Par). We conclude by induction hypothesis with $P_1$ instead of $P$.

* The case $C_!$[] = $C'_!$[] | $P'$ is similar.

* If $C_!$[] = $\nu b \cdot C'_!$[], then $P = \text{new } b$; $P_1$ with $[[P_1]] = C'_![\overline{N}\langle M\rangle.Q]$. We have

$$ (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}}), \mathcal{P}_0 \cup \{\text{new } b; P_1\} \\ \to (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}} \cup \{b'\}), \mathcal{P}_0 \cup \{P_1\{b'/b\}\} $$

for some $b' \notin \mathcal{N}_{\text{pub}} \cup \mathcal{N}_{\text{priv}}$ by (Red Res). We have $[[P_1\{b'/b\}]] = C'_!\{b'/b\}[\overline{N\{b'/b\}}\langle M\{b'/b\}\rangle.Q\{b'/b\}]$ and $N\{b'/b\} = \epsilon$ a since $a \neq b$ because $C_!$ does not bind $a$. We conclude by induction hypothesis with $P_1\{b'/b\}$ instead of $P$.

* If $C_!$[] = $!C'_!$[], then $P = !P_1$ with $[[P_1]] = C'_![\overline{N}\langle M\rangle.Q]$. We have $(\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P} = (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P}_0 \cup \{!P_1\} \to (\mathcal{N}_{\text{pub}}, \mathcal{N}_{\text{priv}})$, $\mathcal{P}_0 \cup \{!P_1, P_1\}$ by (Red Repl). We conclude by induction hypothesis with $P_1$ instead of $P$. $\square$

**Lemma B.6.** Let $E, \mathcal{P}$ be a valid configuration. We have $[[E, \mathcal{P}]] \downarrow_a^\diamond$ if and only if $E, \mathcal{P} \to^* \downarrow_a$.

*Proof.* Suppose $[[E, \mathcal{P}]] \downarrow_a^\diamond$. We have $[E, \mathcal{P}] \to^* \downarrow_a^\diamond \equiv C[\bar{a}\langle M\rangle.P]$ for some $M, P$ and evaluation context $C$[] that does not bind $a$. By Proposition 4.1, $E, \mathcal{P} \to^* E', P'$ and $[[E', P']^\diamond] \equiv C[\bar{a}\langle M\rangle.P]$ for some $E', P'$. By Lemma B.4, $[[E', P']^\diamond] = C'_![\overline{N'}\langle M'\rangle.P']$ and $N' = \epsilon$ a for some $N', M', P'$, and replication context $C'_!$ that does not bind $a$. Let $E' = (\mathcal{N}_{\text{pub}}, \{\tilde{a}\})$ and $P' = \{P_1, \dots, P_n\}$. We have $[[E', P']^\diamond] = \nu\tilde{a}.([P_1]^\diamond | \dots | [P_n]^\diamond)). Then $[[P_i]] = C''_![\overline{N'}\langle M'\rangle.P']$ for some replication context $C''_!$ that does not
bind $a$ and $P_i \in \mathcal{P}'$, and $a \notin \tilde{a}$. Since $N' =_{\varepsilon} a$, we have $a \in \mathrm{fn}(N')$. (Otherwise, we would have $N'\{N''/a\} =_{\varepsilon} a\{N''/a\}$ for all $N''$, since equality is preserved by substitution of terms for names because the equations do not contain names, so $N' =_{\varepsilon} N''$, which contradicts the assumption that the equational theory is non trivial.) So $a \in \mathrm{fn}(P_i)$, so $a \in \mathrm{fn}(\mathcal{P}')$. Since $\mathrm{fn}(\mathcal{P}') \subseteq \mathcal{N}_{\mathrm{pub}} \cup \{\tilde{a}\}$ and $a \notin \tilde{a}$, we have $a \in \mathcal{N}_{\mathrm{pub}}$. By Lemma B.5, $E', \mathcal{P}' \to^* E'', \mathcal{P}'', \overline{N''}\langle M''\rangle \cdot \mathcal{P}'' = [[Q]]$, and $N'' =_{\varepsilon} a$ for some $E'' = (\mathcal{N}_{\mathrm{pub}}, \mathcal{N}'_{\mathrm{priv}})$, $\mathcal{P}'', Q \in \mathcal{P}'', N'', M''$, and $\mathcal{P}''$. Therefore $Q = \mathrm{out}(N'', M'')$; $Q' \in \mathcal{P}''$ for some $Q'$, $N'' =_{\varepsilon} a$, and $a \in \mathcal{N}_{\mathrm{pub}}$, so $E'', \mathcal{P}'' \downarrow_a$, so $E, \mathcal{P} \to^* \downarrow_a$.

Conversely, suppose $E, \mathcal{P} \to^* \downarrow_a$. We have $E, \mathcal{P} \to^* E', \mathcal{P}'$ and $E', \mathcal{P}' \downarrow_a$ for some $E', \mathcal{P}'$. So we have $E' = (\mathcal{N}_{\mathrm{pub}}, \{\tilde{a}\})$, $a \in \mathcal{N}_{\mathrm{pub}}$, $\mathrm{out}(N, M)$; $Q \in \mathcal{P}'$, and $N =_{\varepsilon} a$ for some $\mathcal{N}_{\mathrm{pub}}$, $\tilde{a}$, $N$, $M$, and $Q$. We have $[[E', \mathcal{P}')] = \nu\tilde{a}.([P_1] | \cdots | [P_n])$ where $\mathcal{P}' = \{P_1, \ldots, P_n\}$, and $[[\mathrm{out}(N, M); Q]] = \overline{N}\langle M\rangle \cdot [[Q]]$, so $[[E', \mathcal{P}')] = C[\overline{N}\langle M\rangle \cdot [[Q]]]$ where $C[\_\_]$ is an evaluation context that does not bind $a$, since $a \notin \tilde{a}$. So $[[E', \mathcal{P}]] \stackrel{\circ}{=} C[\bar{a}\langle M\rangle \cdot [[Q]]]$ by RENAME. By Proposition 4.1, $[[E, \mathcal{P}] \to^* \circ] = [[E', \mathcal{P}]] \stackrel{\circ}{=} C[\bar{a}\langle M\rangle \cdot [[Q]]]$, so $[[E, \mathcal{P}] \downarrow_a^\circ]$. $\square$

We define the encoding of contexts as the encoding of processes, with additionally $[[\_\_] = \_\_.$

**Lemma B.7.** Let $C[\_\_]$ be an adversarial context. We have $[[C[C]] \stackrel{\circ}{=} [[C][C]]]$.

*Proof.* Let $C[\_\_] = \text{new } \tilde{n}$; ($\_\_ | Q$) with $fv(Q) = \emptyset$ and $C = (\mathcal{N}_{\mathrm{pub}}, \mathcal{N}_{\mathrm{priv}})$, $\mathcal{P}$. We rename the names in $\mathcal{N}_{\mathrm{priv}}$ so that $\mathcal{N}_{\mathrm{priv}} \cap \mathrm{fn}(Q) = \emptyset$. Let $\mathcal{N}_{\mathrm{priv}} = \{\tilde{a}\}$ and $\mathcal{P} = \{P_1, \ldots, P_n\}$. We have $C[C] = ((\mathcal{N}_{\mathrm{pub}} \cup \mathrm{fn}(Q)) \setminus \{\tilde{n}\}, \mathcal{N}_{\mathrm{priv}} \cup \{\tilde{n}\})$, $\mathcal{P} \cup \{Q\}$, so

$$ \begin{align*} [[C[C]]] &= \nu\tilde{a}, \tilde{n}.([P_1] | \cdots | [P_n] | [[Q]]) \\ &\stackrel{\circ}{=} \nu\tilde{n}.(\nu\tilde{a}.([P_1] | \cdots | [P_n]) | [[Q]]) = [[C][[C]]. \end{align*} $$

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

**Proposition 4.2.** Let $C$ and $C'$ be valid configurations. If $C \approx C'$, then $[[C]] \stackrel{\circ}{=} [[C']].$
*Proof.* We define a relation $\mathcal{R}$ between closed processes by $P \mathcal{R} Q$ if and only if $P \stackrel{\approx}{=} [C]$, $Q \stackrel{\approx}{=} [C']$, and $C \approx C'$ for some $C$ and $C'$. The relation $\mathcal{R}$ is symmetric. Let us show that it satisfies the three conditions of Definition 4.1:

1. If $P \mathcal{R} Q$ and $P \downarrow_a^{\diamond}$, then $P \stackrel{\approx}{=} [C]$, $Q \stackrel{\approx}{=} [C']$, and $C \approx C'$ for some $C$ and $C'$, so $[C] \downarrow_a^{\diamond}$, so by Lemma B.6, $C \to^{*} \downarrow_a$. Since $C \approx C'$, we have $C' \to^{*} \downarrow_a$, so by Lemma B.6, $[C'] \downarrow_a^{\diamond}$, so $Q \downarrow_a^{\diamond}$.

2. Suppose $P \mathcal{R} Q$, $P \to_{\diamond} P'$, and $P'$ is closed. We have $P \stackrel{\approx}{=} [C]$, $Q \stackrel{\approx}{=} [C']$, and $C \approx C'$ for some $C$ and $C'$. If $P = P'$, then $Q \to_{\diamond} P'$ and $P' \stackrel{\approx}{=} [C_1]$ for some $C_1$. Hence $C' \to^{*} C'_1$ and $C_1 \approx C'_1$ for some $C'_1$. By Proposition 4.1, $[C'] \to_{\diamond} P' \stackrel{\approx}{=} [C'_1]$.

If there is no reduction $\to_{\diamond}$ in this trace, we define $Q' = Q$. We have $Q \to_{\diamond} P' \stackrel{\approx}{=} [C'_1]$, $C_1 \approx C'_1$, and $Q' = Q \stackrel{\approx}{=} [C'] \stackrel{\approx}{=} [C'_1]$, so $P' \mathcal{R} Q'$.

If there is at least one reduction $\to_{\diamond}$ in this trace, we define $Q' = [C'_1]$. We have $Q \stackrel{\approx}{=} [C'] \to_{\diamond} P' \stackrel{\approx}{=} [C'_1] = Q'$, so $Q \to_{\diamond} P' \stackrel{\approx}{=} [C'_1]$.

3. Let us finally show that, if $P \mathcal{R} Q$ and $C[\_\_]$ is a closed evaluation context, then $C[P] \mathcal{R} C[Q]$. Up to structural equivalence $\stackrel{\approx}{=}$, the context $C[\_\_]$ can be decomposed into several closed contexts of the form $\nu\tilde{n}.(_|Q)$, so it is enough to show the desired property for such contexts. For such a context $C[\_\_]$, there exists an ad-versarial context $C'[\_\_]$ such that $[C'[\_\_]] = C[\_\_]$. Since $P \mathcal{R} Q$, we have $P \stackrel{\approx}{=} [C]$, $Q \stackrel{\approx}{=} [C']$, and $C \approx C'$ for some $C$ and $C'$. Then $C[P] \stackrel{\approx}{=} [C'][[C]] \stackrel{\approx}{=} [C'[C]]$ and $C[Q] \stackrel{\approx}{=} [C'][[C']] \stackrel{\approx}{=} [C'[C]]$ by Lemma B.7. Moreover, $C[C] \approx C'[C']$, so $C[P] \mathcal{R} C[Q]$.

Since $\stackrel{\approx}{\approx}$ is the largest such relation, we have $\mathcal{R} \subseteq \stackrel{\approx}{\approx}$. If $C \approx C'$, then $[C] \mathcal{R} [C']$, so $[C] \stackrel{\approx}{=} [C']$. $\square$

**Lemma B.8.** If $P$ and $Q$ are closed processes and $P \stackrel{\approx}{=} Q$, then $P \stackrel{\approx}{=} Q$.
*Proof.* We define the relation $\mathcal{R}$ between closed processes by $P \mathcal{R} Q$ if and only if $P \stackrel{\sim}{\hat{\approx}} \stackrel{\sim}{\hat{\approx}} Q$. The relation $\mathcal{R}$ is symmetric and satisfies the three conditions of Definition 4.1, so $\mathcal{R} \subseteq \stackrel{\sim}{\approx}$. This property proves the lemma. $\square$

**Proposition 4.3.** Let $C$ and $C'$ be valid configurations. If $[[C]] \stackrel{\sim}{\approx} [[C']],$ then $C \approx C'$.

*Proof.* Since the contexts in Definition 3.6 may be any ProVerif adversarial contexts, we need to encode all ProVerif constructs into the subset already encoded by $[[\cdot]]$. In this proof, we consider the core ProVerif language with equations and enriched terms. Pattern-matching and tables can be defined as an encoding into that subset, so the result extends to them. We do not consider phases. We define this encoding as follows: $[P]_{\text{PV}}$ is the process obtained from $P$ by performing the following replacements:

* If fail occurs in $D$ or $D'$ (in the output case), then replace $\text{out}(D, D')$; $P$, $\text{in}(D, x: T)$; $P$, and if $D$ then $P$ else $Q$ with $\mathbf{0}$, and replace $\text{let } x: T = D$ in $P$ else $Q$ with $Q$.

* If $D$ is not of the form $D_1 = D_2$, then replace if $D$ then $P$ else $Q$ with if $D = \text{true}$ then $P$ else $Q$.

* If $P_1 = P_0\{D_1=D_2/x\}$, $P_0$ is $\text{out}(D, D')$; $P$, $\text{in}(D, y: T)$; $P$, if $D = D'$ then $P$ else $Q$, or let $y: T = D$ in $P$ else $Q$, $x$ occurs only in $D$ or $D'$ and exactly once, and fail does not occur in any of $D$, $D'$, $D_1$, $D_2$, then replace $P_1$ with if $D_1 = D_2$ then $P_0\{\text{true}/x\}$ else $P_0\{\text{false}/x\}$.

* Replace $\text{let } x: T = M$ in $P$ else $Q$ with $P\{M/x\}$.

We define $[C]_{\text{PV}}$ similarly, and $[E, P]_{\text{PV}} = E, \{[P]_{\text{PV}} | P \in P\}$.

We show that the encoding preserves observational equivalence. In the next properties, $C$ denotes any context (any process with a hole, not only an adversarial context). We define $\text{gen}(P, P') = \{((E, \{P_1, \dots, P_n\}), (E, \{P'_1, \dots, P'_n\})) \mid (E, \{P_1, \dots, P_n\}) \text{ and } (E, \{P'_1, \dots, P'_n\}) \text{ are}$ valid configurations, for all $i \le n$, $P_i = C_i[\sigma_i P]$ and $P'_i = C_i[\sigma_i P']$ for
some context $C_i$ and substitution $\sigma_i$, or $P_i = P'_i$. If $(C, C') \in \text{gen}(P, P')$ and $C \to C_1$ by a reduction that does not reduce processes $P_i$ with an empty context $C_i$, then for some $C'_1$, $C' \to C'_1$ by the same reduction rule and $(C_1, C'_1) \in \text{gen}(P, P')$. The symmetric property also holds, and $\text{gen}(P, P')$ is closed under application of adversarial contexts. Because of these properties, $\text{gen}(P, P')$ is a good starting point for building relations used for proving observational equivalence.

We prove the following properties:

P1. If fail occurs in $D$, then $D \Downarrow$ fail. If fail does not occur in $D$, then $D \Downarrow M$ for some term $M$. These properties are proved by induction on $D$. They come from the fact that equality is the only considered destructor, and it evaluates to fail if and only if one of its arguments evaluates to fail.

P2. If $P_0$ is out($D, D'$); $P$, in($D, x: T$); $P$, or if $D$ then $P$ else $Q$ and fail occurs in $D$ or $D'$, then $E, P \cup \{C[P_0]\} \approx E, P \cup \{C[0]\}$. This property is proved by defining a relation $\mathcal{R}$ between valid configurations by $E, P \cup \{\sigma_1 P_0, \dots, \sigma_n P_0\} \mathcal{R} E, P'$ when $((E, P), (E, P')) \in \text{gen}(P_0, 0)$, and showing that $\mathcal{R} \cup \mathcal{R}^{-1}$ is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that $P_0$ never reduces.

P3. If fail occurs in $D$, then $E, P \cup \{C[\text{let } x: T = D \text{ in } P \text{ else } Q]\} \approx E, P \cup \{C[Q]\}$. This property is proved by defining a relation $\mathcal{R} = \text{gen}(\text{let } x: T = D \text{ in } P \text{ else } Q, Q)$, and showing that $\mathcal{R} \cup \mathcal{R}^{-1}$ is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that $\text{let } x: T = D \text{ in } P \text{ else } Q$ reduces to $Q$ since $D \Downarrow$ fail by P1.

P4. We have $E, P \cup \{C[\text{if } D \text{ then } P \text{ else } Q]\} \approx E, P \cup \{C[\text{if } D = \text{true} \text{ then } P \text{ else } Q]\}$. This property is proved by defining a relation $\mathcal{R} = \text{gen}(\text{if } D \text{ then } P \text{ else } Q$, if $D = \text{true}$ then $P \text{ else } Q)$, and showing that $\mathcal{R} \cup \mathcal{R}^{-1}$ is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that if $D$ then $P$ else $Q$ and if $D = \text{true}$ then $P$ else $Q$ either both reduce to $P$ or both reduce to $Q$, because $D \Downarrow M$ with $M =_{\epsilon} \text{true}$ if and only if $(D = \text{true}) \Downarrow M'$ with $M' =_{\epsilon} \text{true}$.
P5. If $P_0$ is out($D, D'$); $P$, in($D, y: T$); $P$, if $D = D'$ then $P$ else $Q$, or let $y: T = D$ in $P$ else $Q$, $x$ occurs only in $D$ or $D'$ and exactly once, and fail does not occur in any of $D, D', D_1, D_2$, then $E, \mathcal{P} \cup \{C[P_0\{D_1=D_2/x\}]\} \approx E, \mathcal{P} \cup \{C[\text{if } D_1 = D_2 \text{ then } P_0\{\text{true}/x\} \text{ else } P_0\{\text{false}/x\}]\}$. This property is proved by defining a relation $\mathcal{R}$ between valid configurations by $E, \mathcal{P} \cup \{\sigma_1 P_0\{D_1=D_2/x\}, \dots, \sigma_n P_0\{D_1=D_2/x\}\} \mathcal{R} E, \mathcal{P}' \cup \{\sigma_1 P_0\{M_1/x\}, \dots, \sigma_n P_0\{M_n/x\}\}$ when $((E, \mathcal{P}), (E, \mathcal{P}')) \in \text{gen}(P_0\{D_1=D_2/x\}, \text{if } D_1 = D_2 \text{ then } P_0\{\text{true}/x\} \text{ else } P_0\{\text{false}/x\})$ and for all $i \le n$, $\sigma_i(D_1 = D_2) \Downarrow M_i$, and showing that $\mathcal{R} \cup \mathcal{R}^{-1}$ is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that $\sigma_i(\text{if } D_1 = D_2 \text{ then } P_0\{\text{true}/x\} \text{ else } P_0\{\text{false}/x\})$ reduces to $\sigma_i P_0\{M_i/x\}$ when $\sigma_i(D_1 = D_2) \Downarrow M_i$, and that this process behaves like $\sigma_i P_0\{D_1=D_2/x\}$.

P6. We have $E, \mathcal{P} \cup \{C[\text{let } x: T = M \text{ in } P \text{ else } Q]\} \approx E, \mathcal{P} \cup \{C[P\{M/x\}]\}$. This property is proved by defining a relation $\mathcal{R} = \text{gen}(\text{let } x: T = M \text{ in } P \text{ else } Q, P\{M/x\})$ and showing that $\mathcal{R} \cup \mathcal{R}^{-1}$ is symmetric and satisfies the three conditions of Definition 3.6. The main argument is that $\text{let } x: T = M \text{ in } P \text{ else } Q$ reduces to $P\{M/x\}$.

P7. We have $\mathcal{C} \approx [\mathcal{C}]_{\mathbf{PV}}$ by P2-P6.

We define a relation $\mathcal{R}$ between valid configurations by $\mathcal{C}, \mathcal{R}, \mathcal{C}'$ if and only if $\mathcal{C} \approx \mathcal{C}_e, [[\mathcal{C}_e]] \stackrel{\wedge}{\approx} [[\mathcal{C}'_e]]$, and $\mathcal{C}'_e \approx \mathcal{C}'$ for some $\mathcal{C}_e$ and $\mathcal{C}'_e$. The relation $\mathcal{R}$ is symmetric. Let us show that it satisfies the three conditions of Definition 3.6:

1. If $\mathcal{C}, \mathcal{R}, \mathcal{C}'$ and $\mathcal{C} \downarrow_a$, then $\mathcal{C}_e \to^* \downarrow_a$, so by Lemma B.6, $[[\mathcal{C}_e]] \Downarrow_a^{\wedge}$, so $[[\mathcal{C}'_e]] \Downarrow_a^{\wedge}$, so by Lemma B.6, $\mathcal{C}'_e \to^* \downarrow_a$, so $\mathcal{C}' \to^* \downarrow_a$.

2. If $\mathcal{C}, \mathcal{R}, \mathcal{C}'$ and $\mathcal{C} \to C_1$, then $\mathcal{C}_e \to^* C_1$ and $C_1 \approx C_1$ for some $C_1$. By Proposition 4.1, $[[\mathcal{C}_e]] \to_{\diamond} \mathcal{C}'$.

If no reduction $\to_{\diamond}$ is performed, then $[[C_1]] \stackrel{\wedge}{\approx} [[\mathcal{C}_e]] \stackrel{\wedge}{\approx} [[\mathcal{C}'_e]]$ so by Lemma B.8, $[[\mathcal{C}_1]] \stackrel{\wedge}{\approx} [[\mathcal{C}'_e]]$, so $C_1 \mathcal{R} \mathcal{C}'_1$ and $\mathcal{C}' \to^* \mathcal{C}'_1$ with $\mathcal{C}'_1 = \mathcal{C}'$.

If at least one reduction $\to_{\diamond}$ is performed, then $[[\mathcal{C}_e]] \to_{\diamond} \mathcal{C}'$ and $[[\mathcal{C}_1]] \stackrel{\wedge}{\approx} Q'$ for some $Q'$. By Proposition 4.1, so $[[\mathcal{C}'_e]] \to_{\diamond} Q'$.
$C'_e \to^* C'_{1e}$ and $Q' \stackrel{\sim}{=} [[C'_{1e}]]$ for some $C'_{1e}$, so by Lemma B.8, $[[C_{1e}]] \stackrel{\sim}{=} [[C'_{1e}]]$. Moreover, since $C'_e \to^* C'_{1e}$ and $C'_e \approx C'$, we have $C' \to^* C'_1$ and $C'_{1e} \approx C'_1$ for some $C'_1$. So $C_1 \mathcal{R} C'_1$.

3. If $C \mathcal{R} C'$ and $C$ is an adversarial context, then by P7, $C[C] \approx C[C_e] \approx C'[C_e]$ and $C[C'] \approx C[C'_e] \approx C'[C'_e]$, where $C' = [C]_{PV}$. By Lemma B.7 and since $[[C')]$ is a closed evaluation context, $[[C'[C_e]]] \stackrel{\sim}{=} [[C']][[C_e]] \stackrel{\sim}{=} [[C']][[C'_e]] \stackrel{\sim}{=} [[C'[C'_e]]]$ so by Lemma B.8, $[[C'[C_e]]] \stackrel{\sim}{=} [[C'[C'_e]]]$, so $C[C] \mathcal{R} C[C']$.

Since $\approx$ is the largest such relation, we have $\mathcal{R} \subseteq \approx$. If $[[C]] \stackrel{\sim}{=} [[C')]$, then $C \mathcal{R} C'$, so $C \approx C'$. $\square$

## B.3 Relating definitions of observational equivalence

Let $\approx_\pi$ be observational equivalence as defined in (Abadi et al., 2016, Definition 4.1). Let us show that, for plain processes, $\approx_\pi$ is equal to $\stackrel{\circ}{\approx}$, defined in Definition 4.1.

**Lemma B.9.** If $A \stackrel{\circ}{=} B$ and $dom(A) = \emptyset$, then $dom(B) = \emptyset$ and $A \stackrel{\circ}{=} B$. If $A \to_\circ B$ and $dom(A) = \emptyset$, then $dom(B) = \emptyset$ and $A \to_{\diamond} B$.

*Proof.* When $dom(\sigma) = \emptyset$, that is, $\sigma = \mathbf{0}$, the rules of $\stackrel{\circ}{\cong}$ reduce to:

PLAIN'' $\nu\tilde{n}.(\mathbf{0}|P) \stackrel{\circ}{\cong} \nu\tilde{n}.(\mathbf{0}|P')$ when $P \stackrel{\circ}{=} P'$

NEW-C'' $\nu\tilde{n}.(\mathbf{0}|P) \stackrel{\circ}{\cong} \nu\tilde{n}'.(\mathbf{0}|P)$ when $\tilde{n}'$ is a reordering of $\tilde{n}$

NEW-PAR'' $\nu\tilde{n}.(\mathbf{0}|\nu n'.P) \stackrel{\circ}{\cong} \nu\tilde{n}, n'.(\mathbf{0}|P)$

REWRITE'' $\nu\tilde{n}.(\mathbf{0}|P) \stackrel{\circ}{\cong} \nu\tilde{n}.(\mathbf{0}|P)$

so in all cases, if $A \stackrel{\circ}{=} B$ and $dom(A) = \emptyset$, then $dom(B) = \emptyset$ and $A \stackrel{\circ}{=} B$. Hence we have the first property.

Suppose $A \to_\circ B$ and $dom(A) = \emptyset$. We have $A \stackrel{\circ}{=} \nu\tilde{n}.(\sigma|P)$, $P \to_\diamond P'$ and $\nu\tilde{n}.(\sigma|P') \stackrel{\circ}{=} B$. By the first property, $\sigma = \mathbf{0}$ and $A \stackrel{\circ}{=} \nu\tilde{n}.(\mathbf{0}|P) \to_\diamond \nu\tilde{n}.(\mathbf{0}|P') \stackrel{\circ}{=} B$, so $A \to_\diamond B$. $\square$

**Lemma B.10.** Let $P$ be a plain process. If $P \equiv A$, then pnf($A$) is a plain process and $P \stackrel{\circ}{=} pnf(A)$. If $P \to A$, then pnf($A$) is a plain process and $P \to_\diamond pnf(A)$.
*Proof.* Suppose $P \equiv A$. By (Abadi et al., 2016, Lemma B.5), pnf($P$) $\hat{\equiv}$ pnf($A$). We have pnf($P$) = $\mathbf{0}$ | $P \hat{\equiv} P$ and dom(pnf($P$)) = $\emptyset$. By Lemma B.9, we conclude that dom(pnf($A$)) = $\emptyset$ and pnf($P$) $\hat{\equiv}$ pnf($A$), so pnf($A$) is a plain process and $P \hat{\equiv}$ pnf($A$).

Suppose $P \to A$. By (Abadi et al., 2016, Lemma B.8), pnf($P$) $\to_{\diamond}$ pnf($A$). We have pnf($P$) = $\mathbf{0}$ | $P \hat{\equiv} P$ and dom(pnf($P$)) = $\emptyset$. By Lemma B.9, we conclude that dom(pnf($A$)) = $\emptyset$ and pnf($P$) $\to_{\diamond}$ pnf($A$), so pnf($A$) is a plain process and $P \to_{\diamond}$ pnf($A$). $\square$

**Lemma B.11.** Let $P$ and $Q$ be closed processes and $\sigma$ be a bijective renaming. If $P \hat{\equiv} Q$, then $\sigma P \hat{\equiv} \sigma Q$. If $P \to_{\diamond} Q$, then $\sigma P \to_{\diamond} \sigma Q$.

*Proof.* By induction on the derivations. $\square$

**Lemma B.12.** Let $P$ and $Q$ be closed processes and $\sigma$ be a bijective renaming. If $P \stackrel{\sim}{\approx} Q$, then $\sigma P \stackrel{\sim}{\approx} \sigma Q$.

*Proof.* We define a relation $\mathcal{R}$ by $P \mathcal{R} Q$ if and only if $\sigma^{-1}P \stackrel{\sim}{\approx} \sigma^{-1}Q$. The relation $\mathcal{R}$ is symmetric. Let us show that it satisfies the three properties of Definition 4.1:

1. If $P \mathcal{R} Q$ and $P \downarrow_a^{\diamond}$, then by Lemma B.11, $\sigma^{-1}P \downarrow_{\sigma^{-1}a}^{\diamond}$, so we have $\sigma^{-1}Q \downarrow_{\sigma^{-1}a}^{\diamond}$, so by Lemma B.11, $Q \downarrow_a^{\diamond}$.

2. If $P \mathcal{R} Q$, $P \to_{\diamond}^* P'$, and $P'$ is closed, then by Lemma B.11, $\sigma^{-1}P \to_{\diamond}^* \sigma^{-1}P'$ and $\sigma^{-1}P'$ is closed, so $\sigma^{-1}Q \to_{\diamond}^* Q_1$ and $\sigma^{-1}P' \stackrel{\sim}{\approx} Q_1$ for some $Q_1$. Let $Q' = \sigma Q_1$. By Lemma B.11, we have $Q \to_{\diamond}^* \sigma Q_1 = Q'$ and since $\sigma^{-1}P' \stackrel{\sim}{\approx} \sigma^{-1}Q'$, we have $P' \mathcal{R} Q'$.

3. If $P \mathcal{R} Q$ and $C[\_\_]$ is a closed evaluation context, then $\sigma^{-1}P \stackrel{\sim}{\approx} \sigma^{-1}Q$ so $\sigma^{-1}(C[P]) = \sigma^{-1}C[\sigma^{-1}P] \stackrel{\sim}{\approx} \sigma^{-1}C[\sigma^{-1}Q] = \sigma^{-1}(C[Q])$, so $C[P] \mathcal{R} C[Q]$. (The application of $\sigma^{-1}$ to $C[\_\_]$ is defined by renaming both free and bound names of $C[\_\_]$ by $\sigma^{-1}$.)

Hence $\mathcal{R} \subseteq \stackrel{\sim}{\approx}$. If $P \stackrel{\sim}{\approx} Q$, then $\sigma P \mathcal{R} \sigma Q$, so $\sigma P \stackrel{\sim}{\approx} \sigma Q$. $\square$

**Proposition B.1.** Let $P$ and $Q$ be plain processes. We have $P \stackrel{\sim}{\approx} Q$ if and only if $P \stackrel{\sim}{\approx}_{\pi} Q$.
*Proof.* The relation $\approx_{\pi}$ restricted to closed plain processes is symmetric. Let us show that it satisfies the three conditions of Definition 4.1:

1. If $P \approx_{\pi} Q$ and $P \Downarrow_{a}^{\diamond}$, then by (Abadi et al., 2016, Lemmas B.9 and B.7), $P \Downarrow_{a}$, so $Q \Downarrow_{a}$, that is, $Q \to^{*} C[\bar{a}\langle M\rangle.Q']$ for some $M$, $Q'$, and evaluation context $C[\_\_]$ that does not bind $a$, so by Lemma B.10, $Q \to_{\diamond}^{*} \hat{=} \text{pnf}(C[\bar{a}\langle M\rangle.Q']) = C'[\bar{a}\langle M'\rangle.Q'']$ for some $M'$, $Q''$, and plain evaluation context $C'[\_\_]$ that does not bind $a$, so $Q \Downarrow_{a}^{\diamond}$.

2. If $P \approx_{\pi} Q$, $P \to_{\diamond}^{*} P'$, and $P'$ is closed, then by (Abadi et al., 2016, Lemma B.9), $P \to^{*} P'$, so $Q \to^{*} B'$ and $P' \approx_{\pi} B'$ for some $B'$. By Lemma B.10, $\text{pnf}(B')$ is a plain process and $Q \to_{\diamond}^{*} \text{pnf}(B')$. By (Abadi et al., 2016, Lemma B.2), $\text{pnf}(B') \equiv B'$, so $P' \approx_{\pi} \text{pnf}(B')$. So we have $Q \to_{\diamond}^{*} Q'$ and $P' \approx_{\pi} Q'$ for $Q' = \text{pnf}(B')$.

3. If $P \approx_{\pi} Q$, then $C[P] \approx_{\pi} C[Q]$ for all plain closed evaluation contexts $C[\_\_]$, since these contexts are closing for $P$ and $Q$.

Since $\hat{=}^\approx$ is the largest such relation, we conclude that, if $P \approx_{\pi} Q$, then $P \approx^\approx Q$.

Let us define the relation $\mathcal{R}$ by $A \mathcal{R} B$ if and only if $A \equiv \nu\tilde{n}.(\sigma | P)$, $B \equiv \nu\tilde{n}.(\sigma | Q)$, and $P \approx^\approx Q$, for some $\tilde{n}$, closed substitution $\sigma$, and closed processes $P$ and $Q$. The relation $\mathcal{R}$ is symmetric. Let us show that it satisfies the three conditions of (Abadi et al., 2016, Definition 4.1):

1. If $A \mathcal{R} B$ and $A \Downarrow_{a}$, then $\nu\tilde{n}.(\sigma | P) \to^{*} C[\bar{a}\langle M\rangle.P']$ for some $M$, $P'$, and evaluation context $C[\_\_]$ that does not bind $a$. By (Abadi et al., 2016, Lemma B.8), $\nu\tilde{n}.(\sigma | P) \to_{\diamond}^{*} C[\bar{a}\langle M\rangle.P']$, and by (Abadi et al., 2016, Lemma B.23), $P \to_{\diamond}^{*} P_1$ and $C[\bar{a}\langle M\rangle.P'] \equiv \nu\tilde{n}.(\sigma | P_1)$ for some $P_1$. Let $\text{dom}(\sigma) = \{\tilde{x}\}$. We have $\nu\tilde{n}.P_1 \equiv \nu\tilde{x}.\tilde{n}.(\sigma | P_1) \equiv \nu\tilde{x}.C[\bar{a}\langle M\rangle.P']$, so by Lemma B.10, $\nu\tilde{n}.P_1 \stackrel{\diamond}{=} \text{pnf}(\nu\tilde{x}.C[\bar{a}\langle M\rangle.P']) = C'[\bar{a}\langle M'\rangle.P'']$ for some $M'$, $P''$, and plain evaluation context $C'[\_\_]$ that does not bind $a$. We rename $\tilde{n}$ so that $a \notin \{\tilde{n}\}$. By Lemma B.4, $\nu\tilde{n}.P_1 = C'_![\tilde{N}''\langle M''\rangle.P''']$ and $\tilde{N}'' =_{\mathcal{E}} a$ for some $\tilde{N}''$, $M''$, $P'''$, and replication context $C'_![\_\_]$ that does not bind $a$. So $P_1 = C'_![\tilde{N}''\langle M''\rangle.P''']$ for some replication context $C'_![\_\_]$ that does not bind $a$, so $P_1 \stackrel{\diamond}{=} C''[\bar{a}\langle M''\rangle.P''']$ for
some plain evaluation context $C''[\phantom{\sigma}]$ that does not bind $a$, by Lemma B.4. Hence $P \downarrow_a^\diamond$. Since $P \stackrel{\diamond}{\approx} Q$, we have $Q \downarrow_a^\diamond$, that is, $Q \to^* \diamond \stackrel{\diamond}{\cong} C_1[\bar{a}\langle M_1\rangle \cdot Q_1]$ for some $M_1, Q_1$, and plain evaluation context $C_1[\phantom{\sigma}]$ that does not bind $a$. Hence $B \equiv \nu\tilde{n}.(\sigma | Q) \to^* \equiv \nu\tilde{n}.(\sigma | C_1[\bar{a}\langle M_1\rangle \cdot Q_1])$. Since $a \notin \{\tilde{n}\}, \nu\tilde{n}.(\sigma | C_1[\phantom{\sigma}])$ is an evaluation context that does not bind $a$, so $B \downarrow_a$.

2. If $A \nparallel B$, $A \to^* A'$, and $A'$ is closed, then $\nu\tilde{n}.(\sigma | P) \equiv \to^* A'$. If $A' = A$, then we have $A' \nparallel B'$ and $B \to^* B'$ for $B' = B$. Otherwise, $\nu\tilde{n}.(\sigma | P) \to^+ A'$, so by (Abadi et al., 2016, Lemma B.8), $\nu\tilde{n}.(\sigma | P) \to_o^+ \text{pnf}(A')$, and by (Abadi et al., 2016, Lemma B.23), $P \to_o^+ P'$ and $\text{pnf}(A') \equiv \nu\tilde{n}.(\sigma | P')$ for some $P'$. Since $P \stackrel{\diamond}{\approx} Q$, we have $Q \to^* Q'$ and $P' \stackrel{\diamond}{\approx} Q'$ for some $Q'$. Let $B' = \nu\tilde{n}.(\sigma | Q')$. We have $B \to^* B'$. Moreover, $A' \equiv \text{pnf}(A') \equiv \nu\tilde{n}.(\sigma | P')$, $B' = \nu\tilde{n}.(\sigma | Q')$, and $P' \stackrel{\diamond}{\approx} Q'$, so $A' \nparallel B'$.

3. Suppose $A \nparallel B$ and $C[\phantom{\sigma}]$ is a closing evaluation context for $A$ and $B$. We want to show that $C[A] \nparallel C[B]$. We first rename the free names and variables of $C[\phantom{\sigma}]$, so that the obtained context is simple. By (Abadi et al., 2016, Lemma C.11), it is sufficient to show $C[A] \nparallel C[B]$ for the renamed context. By (Abadi et al., 2016, Lemma A.1), there exists a context $C'[\phantom{\sigma}]$ of the form $\nu\tilde{a}, \tilde{x}.(\phantom{\sigma}A')$ such that $C[\phantom{\sigma}] \equiv C'[\phantom{\sigma}]$ and all subcontexts of $C'[\phantom{\sigma}]$ are simple for $A$. Let $\text{pnf}(A') = \nu\tilde{n}.(\sigma' | P')$. We have $C[A] \equiv C'[A] \equiv \nu\tilde{a}, \tilde{x}.(A | A') \equiv \nu\tilde{a}, \tilde{x}.(\nu\tilde{n}.(\sigma | P) | \nu\tilde{n}.(\sigma' | P'))$. We rename $\tilde{n}$ and $\tilde{n}'$ so that $\{\tilde{n}\} \cap \{\tilde{n}'\} = \emptyset$, the names in $\tilde{n}$ do not occur in $\sigma'$ and $P'$, and the names in $\tilde{n}'$ do not occur in $\sigma$ and $P$. By Lemma B.12, the property $P \stackrel{\diamond}{\approx} Q$ is preserved by the renaming of $\tilde{n}$. We obtain $C[A] \equiv \nu\tilde{a}, \tilde{n}, \tilde{n}'.((\sigma | \sigma\sigma')_{dom(\sigma) \cup dom(\sigma') \setminus \{\tilde{x}\}} | P | \sigma P')$, where $(\sigma | \sigma\sigma')_{dom(\sigma) \cup dom(\sigma') \setminus \{\tilde{x}\}}$ and $\sigma P'$ are closed. (The substitution $\sigma'$ does not affect $\sigma$ nor $P$ because they are closed.) Similarly, $C[B] \equiv \nu\tilde{a}, \tilde{n}, \tilde{n}'.((\sigma | \sigma\sigma')_{dom(\sigma) \cup dom(\sigma') \setminus \{\tilde{x}\}} | Q | \sigma P')$. Since $P \stackrel{\diamond}{\approx} Q$ and $\phantom{|}_{\sigma}P'$ is a closed evaluation context, we have $P | \sigma P' \stackrel{\diamond}{\approx} Q | \sigma P'$. Therefore, $C[A] \nparallel C[B]$.

Since $\approx_\pi$ is the largest such relation, $\mathcal{R} \subseteq \approx_\pi$. In particular, if $P \stackrel{\diamond}{\approx} Q$, then $P \nparallel Q$, so $P \approx_\pi Q$. $\square$
References

Abadi, M. 1999. "Secrecy by Typing in Security Protocols". *Journal of the ACM*. 46(5): 749-786.

Abadi, M. and B. Blanchet. 2005a. "Analyzing Security Protocols with Secrecy Types and Logic Programs". *Journal of the ACM*. 52(1): 102-146.

Abadi, M. and B. Blanchet. 2005b. "Computer-Assisted Verification of a Protocol for Certified Email". *Science of Computer Programming*. 58(1-2): 3-27. Special issue SAS'03.

Abadi, M., B. Blanchet, and C. Fournet. 2007. "Just Fast Keying in the Pi Calculus". *ACM Transactions on Information and System Security (TISSEC)*. 10(3): 1-59.

Abadi, M., B. Blanchet, and C. Fournet. 2016. "The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication". Report arXiv:1609.03003v1. Available at http://arxiv.org/abs/1609.03003v1.

Abadi, M. and V. Cortier. 2006. "Deciding Knowledge in Security Protocols under Equational Theories". *Theoretical Computer Science*. 367(1-2): 2-32.

Abadi, M. and C. Fournet. 2001. "Mobile Values, New Names, and Secure Communication". In: *28th ACM Symposium on Principles of Programming Languages (POPL'01)*. London, UK: ACM. 104-115.
Abadi, M. and C. Fournet. 2004. "Private authentication". *Theoretical Computer Science*. 322(3): 427-476.

Abadi, M., N. Glew, B. Horne, and B. Pinkas. 2002. "Certified Email with a Light On-line Trusted Third Party: Design and Implementation". In: *11th International World Wide Web Conference*. Honolulu, Hawaii: ACM. 387-395.

Abadi, M. and A. D. Gordon. 1998. "A Bisimulation Method for Cryptographic Protocols". *Nordic Journal of Computing*. 5(4): 267-303.

Abadi, M. and A. D. Gordon. 1999. "A Calculus for Cryptographic Protocols: The Spi Calculus". *Information and Computation*. 148(1): 1-70. An extended version appeared as Digital Equipment Corporation Systems Research Center report No. 149, January 1998.

Abadi, M. and R. Needham. 1996. "Prudent Engineering Practice for Cryptographic Protocols". *IEEE Transactions on Software Engineering*. 22(1): 6-15.

Abadi, M. and P. Rogaway. 2002. "Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption)". *Journal of Cryptology*. 15(2): 103-127.

Abdalla, M., P.-A. Fouque, and D. Pointcheval. 2005. "Password-Based Authenticated Key Exchange in the Three-Party Setting". In: *2005 International Workshop on Practice and Theory in Public Key Cryptography (PKC'05)*. Ed. by S. Vaudenay. Vol. 3386. *Lecture Notes in Computer Science*. Les Diablerets, Switzerland: Springer. 65-84.

Adrian, D., K. Bhargavan, Z. Durumeric, P. Gaudry, M. Green, J. A. Halderman, N. Heninger, D. Springall, E. Thomé, L. Valenta, B. VanderSloot, E. Wustrow, S. Zanella-Béguelin, and P. Zimmermann. 2015. "Imperfect Forward Secrecy: How Diffie-Hellman Fails in Practice". In: *22nd ACM Conference on Computer and Communications Security*.

Aiello, W., S. M. Bellovin, M. Blaze, R. Canetti, J. Ioannidis, K. Keromytis, and O. Reingold. 2004. "Just Fast Keying: Key Agreement in a Hostile Internet". *ACM Transactions on Information and System Security*. 7(2): 242-273.
Aizatulin, M., A. D. Gordon, and J. Jürjens. 2011. "Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution". In: *18th ACM Conference on Computer and Communications Security (CCS'11)*. Chicago, IL, USA: ACM. 331–340.

Aizatulin, M., A. D. Gordon, and J. Jürjens. 2012. "Computational Verification of C Protocol Implementations by Symbolic Execution". In: *19th ACM Conference on Computer and Communications Security (CCS'12)*. Raleigh, NC, USA: ACM. 712–723.

Allamigeon, X. and B. Blanchet. 2005. "Reconstruction of Attacks against Cryptographic Protocols". In: *18th IEEE Computer Security Foundations Workshop (CSFW-18)*. Aix-en-Provence, France: IEEE. 140–154.

Almeida, J. B., M. Barbosa, G. Barthe, and F. Dupressoir. 2013. "Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations". In: *ACM Conference on Computer and Communications Security (CCS'13)*. Berlin, Germany: ACM. 1217–1230.

Arapinis, M. and M. Duflot. 2007. "Bounding Messages for Free in Security Protocols". In: *27th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'07)*. Ed. by V. Arvind and S. Prasad. Vol. 4855. *Lecture Notes in Computer Science*. New Delhi, India: Springer. 376–387.

Arapinis, M., J. Liu, E. Ritter, and M. Ryan. 2014. "Stateful Applied Pi Calculus". In: *Principles of Security and Trust—Third International Conference*. Ed. by M. Abadi and S. Kremer. Vol. 8414. *Lecture Notes in Computer Science*. Springer. 22–41.

Arapinis, M., E. Ritter, and M. D. Ryan. 2011. "StatVerif: Verification of stateful processes". In: *24th Computer Security Foundations Symposium (CSF'11)*. IEEE. Cernay-la-Ville, France. 33–47.
Armando, A., D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. H. Drielsma, P.-C. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganó, and L. Vigneron. 2005. "The AVISPA tool for Automated Validation of Internet Security Protocols and Applications". In: *Computer Aided Verification, 17th International Conference, CAV 2005*. Ed. by K. Etessami and S. K. Rajamani. Vol. 3576. *Lecture Notes in Computer Science*. Edinburgh, Scotland: Springer. 281–285.

Armando, A., R. Carbone, and L. Compagna. 2014. "SATMC: a SAT-based Model Checker for Security-critical Systems". In: *Tools and Algorithms for the Construction and Analysis of Systems, 20th International Conference, TACAS 2014*. Ed. by E. Ábrahám and K. Havelund. Vol. 8413. *Lecture Notes in Computer Science*. Grenoble, France: Springer. 31–45. DOI: 10.1007/978-3-642-54862-8_3.

Avalle, M., A. Pironti, R. Sisto, and D. Pozza. 2011. "The JavaSPI Framework for Security Protocol Implementation". In: *International Conference on Availability, Reliability and Security (ARES'11)*. IEEE. 746–751.

Bachmair, L. and H. Ganzinger. 2001. "Resolution Theorem Proving". In: *Handbook of Automated Reasoning*. Ed. by A. Robinson and A. Voronkov. Vol. 1. North Holland. Chap. 2. 19–100.

Backes, M., F. Bendun, M. Maffei, E. Mohammadi, and K. Pecina. 2015. "Symbolic Malleable Zero-Knowledge Proofs". In: *28th IEEE Computer Security Foundations Symposium (CSF'15)*. Verona, Italy: IEEE. 412–480.

Backes, M., C. Hritcu, and M. Maffei. 2008a. "Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus". In: *21st IEEE Computer Security Foundations Symposium (CSF'08)*. Pittsburgh, PA: IEEE Computer Society. 195–209.

Backes, M., M. Maffei, and D. Unruh. 2008b. "Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol". In: *29th IEEE Symposium on Security and Privacy*. Technical report version available at http://eprint.iacr.org/2007/289. IEEE. Oakland, CA. 202–215.
Backes, M., E. Mohammadi, and T. Ruffing. 2014. "Computational Soundness Results for ProVerif: Bridging the Gap from Trace Properties to Uniformity". In: *Principles of Security and Trust (POST'14)*. Ed. by M. Abadi and S. Kremer. Vol. 8414. *Lecture Notes in Computer Science*. Grenoble, France: Springer. 42-62.

Bansal, C., K. Bhargavan, A. Delignat-Lavaud, and S. Maffeis. 2013. "Keys to the Cloud: Formal Analysis and Concrete Attacks on Encrypted Web Storage". In: *Principles of Security and Trust (POST 2013)*. Ed. by D. Basin and J. Mitchell. Vol. 7796. *Lecture Notes in Computer Science*. Rome, Italy: Springer. 126-146.

Bansal, C., K. Bhargavan, and S. Maffeis. 2012. "Discovering Concrete Attacks on Website Authorization by Formal Analysis". In: *25th IEEE Computer Security Foundations Symposium (CSF'12)*. IEEE. Cambridge, MA, USA. 247-262.

Barthe, G., F. Dupressoir, P.-A. Fouque, B. Grégoire, M. Tibouchi, and J.-C. Zapalowicz. 2014a. "Making RSA-PSS Provably Secure against Non-random Faults". In: *Cryptographic Hardware and Embedded Systems (CHES'14)*. Ed. by L. Batina and M. Robshaw. Vol. 8731. *Lecture Notes in Computer Science*. Busan, South Korea: Springer. 206-222.

Barthe, G., F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt, and P.-Y. Strub. 2014b. "EasyCrypt: A Tutorial". In: *Foundations of Security Analysis and Design VII*. Ed. by A. Aldini, J. Lopez, and F. Martinelli. Vol. 8604. *Lecture Notes in Computer Science*. Springer. 146-166.

Barthe, G., B. Grégoire, S. Heraud, and S. Z. Béguelin. 2011. "Computer-Aided Security Proofs for the Working Cryptographer". In: *Advances in Cryptology - CRYPTO 2011*. Ed. by P. Rogaway. Vol. 6841. *Lecture Notes in Computer Science*. Santa Barbara, CA, USA: Springer. 71-90.

Barthe, G., B. Grégoire, and S. Zanella. 2009. "Formal Certification of Code-Based Cryptographic Proofs". In: *36th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'09)*. Savannah, Georgia: ACM. 90-101.
Basin, D., J. Dreier, and R. Casse. 2015. "Automated Symbolic Proofs of Observational Equivalence". In: *22nd ACM Conference on Computer and Communications Security (CCS'15)*. Denver, CO: ACM. 1144–1155.

Basin, D., S. Mödersheim, and L. Viganò. 2005. "OFMC: A symbolic model checker for security protocols". *International Journal of Information Security*. 4(3): 181–208.

Baudet, M. 2007. "Sécurité des protocoles cryptographiques: aspects logiques et calculatoires". *PhD thesis*. Ecole Normale Supérieure de Cachan.

Béguelin, S. Z., B. Grégoire, G. Barthe, and F. Olmedo. 2009. "Formally Certifying the Security of Digital Signature Schemes". In: *30th IEEE Symposium on Security and Privacy, S&P 2009*. Oakland, CA: IEEE. 237–250.

Bellovin, S. M. and M. Merritt. 1992. "Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks". In: *1992 IEEE Computer Society Symposium on Research in Security and Privacy*. 72–84.

Bellovin, S. M. and M. Merritt. 1993. "Augmented Encrypted Key Exchange: a Password-Based Protocol Secure Against Dictionary Attacks and Password File Compromise". In: *First ACM Conference on Computer and Communications Security*. 244–250.

Bengtson, J., K. Bhargavan, C. Fournet, A. Gordon, and S. Maffeis. 2011. "Refinement Types for Secure Implementations". *ACM Transactions on Programming Languages and Systems*. 33(2).

Beurdouche, B., K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P.-Y. Strub, and J. K. Zinzindohoue. 2015. "A Messy State of the Union: Taming the Composite State Machines of TLS". In: *IEEE Symposium on Security & Privacy 2015 (Oakland'15)*. IEEE.

Bhargavan, K., R. Corin, and C. Fournet. 2007. "Crypto-Verifying Protocol Implementations in ML". http://doc.utwente.nl/64107/1/fs2cv.pdf.
Bhargavan, K., R. Corin, C. Fournet, and E. Zălinescu. 2008. "Cryp-
tographically Verified Implementations for TLS". In: *15th ACM
Conference on Computer and Communications Security (CCS'08)*.
ACM. 459-468.

Bhargavan, K., C. Fournet, and A. Gordon. 2004. "Verifying Policy-
Based Security for Web Services". In: *ACM Conference on Computer
and Communications Security (CCS'04)*. Washington DC: ACM.
268-277.

Bhargavan, K., C. Fournet, and A. Gordon. 2010. "Modular Verification of Security Protocol Code by Typing". In: *ACM Symposium on Principles of Programming Languages (POPL'10)*. Madrid, Spain: ACM. 445-456.

Bhargavan, K., C. Fournet, A. Gordon, and S. Tse. 2006. "Verified interoperable implementations of security protocols". In: *19th IEEE Computer Security Foundations Workshop (CSFW'06)*. Venice, Italy: IEEE Computer Society. 139-152.

Bhargavan, K., C. Fournet, M. Kohlweiss, A. Pironti, and P.-Y. Strub. 2013. "Implementing TLS with Verified Cryptographic Security". In: *IEEE Symposium on Security & Privacy*. 445-462.

Blanchet, B. 2004. "Automatic Proof of Strong Secrecy for Security Protocols". In: *IEEE Symposium on Security and Privacy*. Oakland, California. 86-100.

Blanchet, B. 2008a. "A Computationally Sound Mechanized Prover for Security Protocols". *IEEE Transactions on Dependable and Secure Computing*. 5(4): 193-207.

Blanchet, B. 2008b. "Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire". *Mémoire d'habilitation à diriger des recherches*. Université Paris-Dauphine.

Blanchet, B. 2009. "Automatic Verification of Correspondences for Security Protocols". *Journal of Computer Security*. 17(4): 363-434.

Blanchet, B. 2011. "Using Horn Clauses for Analyzing Security Protocols". In: *Formal Models and Techniques for Analyzing Security Protocols*. Ed. by V. Cortier and S. Kremer. Vol. 5. *Cryptology and Information Security Series*. IOS Press. 86-111.
Blanchet, B. 2012a. "Mechanizing Game-Based Proofs of Security Protocols". In: *Software Safety and Security - Tools for Analysis and Verification*. Ed. by T. Nipkow, O. Grumberg, and B. Hauptmann. Vol. 33. *NATO Science for Peace and Security Series - D: Information and Communication Security*. Proceedings of the 2011 MOD summer school. IOS Press. 1-25.

Blanchet, B. 2012b. "Security Protocol Verification: Symbolic and Computational Models". In: *First Conference on Principles of Security and Trust (POST'12)*. Ed. by P. Degano and J. Guttman. Vol. 7215. *Lecture Notes in Computer Science*. Tallinn, Estonia: Springer. 3-29.

Blanchet, B. 2014. "Automatic Verification of Security Protocols in the Symbolic Model: the Verifier ProVerif". In: *Foundations of Security Analysis and Design VII, FOSAD Tutorial Lectures*. Ed. by A. Aldini, J. Lopez, and F. Martinelli. Vol. 8604. *Lecture Notes in Computer Science*. Springer. 54-87.

Blanchet, B., M. Abadi, and C. Fournet. 2008. "Automated Verification of Selected Equivalences for Security Protocols". *Journal of Logic and Algebraic Programming*. 75(1): 3-51.

Blanchet, B. and A. Chaudhuri. 2008. "Automated Formal Analysis of a Protocol for Secure File Sharing on Untrusted Storage". In: *IEEE Symposium on Security and Privacy*. IEEE. Oakland, CA. 417-431.

Blanchet, B. and A. Podelski. 2005. "Verification of Cryptographic Protocols: Tagging Enforces Termination". *Theoretical Computer Science*. 333(1-2): 67-90. Special issue FoSSaCS'03.

Blanchet, B. and B. Smyth. 2016. "Automated reasoning for equivalences in the applied pi calculus with barriers". In: *29th IEEE Computer Security Foundations Symposium (CSF'16)*. Lisboa, Portugal: IEEE. 310-324.

Blanchet, B., B. Smyth, and V. Cheval. 2016. "ProVerif 1.94pl1: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial". Available at http://proverif.inria.fr/manual.pdf.

Boichut, Y., N. Kosmatov, and L. Vigneron. 2006. "Validation of Prouvé protocols using the automatic tool TA4SP". In: *Third Taiwanese-French Conference on Information Technology (TFIT 2006)*. Nancy, France. 467-480.
Bruni, A., S. Mödersheim, F. Nielson, and H. R. Nielson. 2015. "Set-Pi: Set Membership Pi-Calculus". In: *28th IEEE Computer Security Foundations Symposium (CSF'15)*. Verona, Italy: IEEE. 185-198.

Cadé, D. and B. Blanchet. 2013. "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH". *Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)*. 4(1): 4-31.

Cadé, D. and B. Blanchet. 2015. "Proved Generation of Implementations from Computationally Secure Protocol Specifications". *Journal of Computer Security*. 23(3): 331-402.

Canetti, R. and J. Herzog. 2006. "Universally Composable Symbolic Analysis of Mutual Authentication and Key Exchange Protocols". In: *Proceedings, Theory of Cryptography Conference (TCC'06)*. Ed. by S. Halevi and T. Rabin. Vol. 3876. *Lecture Notes in Computer Science*. Extended version available at http://eprint.iacr.org/2004/334. New York, NY: Springer. 380-403.

Chadha, R., S. Ciobâca, and S. Kremer. 2012. "Automated Verification of Equivalence Properties of Cryptographic Protocols". In: *21st European Symposium on Programming (ESOP'12)*. Vol. 7211. *Lecture Notes in Computer Science*. Springer. 108-127.

Chaki, S. and A. Datta. 2009. "ASPIER: An Automated Framework for Verifying Security Protocol Implementations". In: *22nd IEEE Computer Security Foundations Symposium (CSF'09)*. Port Jefferson, NY, USA. 172-185.

Cheval, V. and B. Blanchet. 2013. "Proving More Observational Equivalences with ProVerif". In: *2nd Conference on Principles of Security and Trust (POST 2013)*. Ed. by D. Basin and J. Mitchell. Vol. 7796. *Lecture Notes in Computer Science*. Rome, Italy: Springer. 226-246.

Cheval, V., H. Comon-Lundh, and S. Delaune. 2011. "Trace Equivalence Decision: Negative Tests and Non-determinism". In: *Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS'11)*. Chicago, Illinois, USA: ACM. 321-330.
Chevalier, Y., R. Küsters, M. Rusinowitch, and M. Turuani. 2003. "Deciding the Security of Protocols with Diffie-Hellman Exponentiation and Products in Exponents". In: *FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science, 23rd Conference*. Ed. by P. K. Pandya and J. Radhakrishnan. Vol. 2914. Lecture Notes in Computer Science. Mumbai, India: Springer. 124-135.

Chevalier, Y., R. Küsters, M. Rusinowitch, and M. Turuani. 2005. "An NP decision procedure for protocol insecurity with XOR". *Theoretical Computer Science*. 338(1-3): 247-274.

Chothia, T., B. Smyth, and C. Staite. 2015. "Automatically Checking Commitment Protocols in ProVerif without False Attacks". In: *Principles of Security and Trust, 4th International Conference, POST 2015*. Ed. by R. Focardi and A. Myers. Vol. 9036. Lecture Notes in Computer Science. London, UK: Springer. 137-155.

Chrétien, R., V. Cortier, and S. Delaune. 2015a. "Decidability of trace equivalence for protocols with nonces". In: *28th IEEE Computer Security Foundations Symposium (CSF'15)*. Verona, Italy: IEEE Computer Society. 170-184. doi: 10.1109/CSF.2015.19

Chrétien, R., V. Cortier, and S. Delaune. 2015b. "From security protocols to pushdown automata". *ACM Transactions on Computational Logic*. 17(1:3). doi: 10.1145/2811262.

Ciobâcă, Ş. 2011. "Automated Verification of Security Protocols with Applications to Electronic Voting". *PhD thesis*. ENS Cachan.

Cohen, E. 2002. "Proving Protocols Safe from Guessing". In: *Foundations of Computer Security*. Copenhagen, Denmark.

Comon-Lundh, H. and V. Cortier. 2003. "New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols". In: *14th Int. Conf. Rewriting Techniques and Applications (RTA'2003)*. Ed. by R. Nieuwenhuis. Vol. 2706. Lecture Notes in Computer Science. Valencia, Spain: Springer. 148-164.
Comon-Lundh, H. and S. Delaune. 2005. "The finite variant property: How to get rid of some algebraic properties". In: *Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA'05)*. Ed. by J. Giesl. Vol. 3467. *Lecture Notes in Computer Science*. Nara, Japan: Springer. 294-307.

Comon-Lundh, H. and V. Shmatikov. 2003. "Intruder deductions, constraint solving and insecurity decision in presence of exclusive or". In: *Symposium on Logic in Computer Science (LICS'03)*. Ottawa, Canada: IEEE Computer Society. 271-280.

Corin, R., J. M. Doumen, and S. Etalle. 2004. "Analysing Password Protocol Security Against Off-line Dictionary Attacks". In: *2nd Int. Workshop on Security Issues with Petri Nets and other Computational Models (WISP)*. *Electronic Notes in Theoretical Computer Science*.

Corin, R., S. Malladi, J. Alves-Foss, and S. Etalle. 2003. "Guess What? Here is a New Tool that Finds some New Guessing Attacks". In: *Workshop on Issues in the Theory of Security (WITS'03)*. Ed. by R. Gorrieri. Warsaw, Poland.

Cortier, V., H. Hördegen, and B. Warinschi. 2006. "Explicit Randomness is not Necessary when Modeling Probabilistic Encryption". In: *Workshop on Information and Computer Security (ICS 2006)*. Ed. by C. Dima, M. Minea, and F. Tiplea. Vol. 186. *Electronic Notes in Theoretical Computer Science*. Timisoara, Romania: Elsevier. 49-65.

Cortier, V., S. Kremer, and B. Warinschi. 2011. "A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems". *Journal of Automated Reasoning*. 46(3-4): 225-259.

Cortier, V., M. Rusinowitch, and E. Zălinescu. 2007. "Relating two standard notions of secrecy". *Logical Methods in Computer Science*. 3(3).

Cortier, V. and C. Wiedling. 2012. "A formal analysis of the Norwegian E-voting protocol". In: *Proceedings of the 1st International Conference on Principles of Security and Trust (POST'12)*. Ed. by P. Degano and J. D. Guttman. Vol. 7215. *Lecture Notes in Computer Science*. Tallinn, Estonia: Springer. 109-128.
Cremers, C. J. 2008. "Unbounded verification, falsification, and characterization of security protocols by pattern refinement". In: *15th ACM conference on Computer and Communications Security (CCS'08)*. Alexandria, Virginia, USA: ACM. 119-128.

Delaune, S. and F. Jacquemard. 2004. "A Theory of Dictionary Attacks and its Complexity". In: *17th IEEE Computer Security Foundations Workshop*. Pacific Grove, CA: IEEE. 2-15.

Delaune, S., S. Kremer, and M. D. Ryan. 2009. "Verifying Privacy-type Properties of Electronic Voting Protocols". *Journal of Computer Security*. 17(4): 435-487.

Delaune, S., S. Kremer, M. D. Ryan, and G. Steel. 2011. "Formal analysis of protocols based on TPM state registers". In: *Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF'11)*. Cernay-la-Ville, France: IEEE Computer Society. 66-82.

Delaune, S., M. Ryan, and B. Smyth. 2008. "Automatic verification of privacy properties in the applied pi calculus". In: *Second Joint iTrust and PST Conferences on Privacy, Trust Management and Security (IFIPTM'08)*. Ed. by Y. Karabulut, J. Mitchell, P. Herrmann, and C. D. Jensen. Vol. 263. *IFIP Advances in Information and Communication Technology*. Trondheim, Norway: Springer. 263-278.

Denning, D. E. and G. M. Sacco. 1981. "Timestamps in Key Distribution Protocols". *Communications of the ACM*. 24(8): 533-536.

Diffie, W. and M. Hellman. 1976. "New Directions in Cryptography". *IEEE Transactions on Information Theory*. IT-22(6): 644-654.

Dolev, D. and A. C. Yao. 1983. "On the Security of Public Key Protocols". *IEEE Transactions on Information Theory*. IT-29(12): 198-208.

Dreier, J., P. Lafourcade, and Y. Lakhnech. 2013. "Formal Verification of e-Auction Protocols". In: *Principles of Security and Trust (POST'13)*. Ed. by D. Basin and J. Mitchell. Vol. 7796. *Lecture Notes in Computer Science*. Rome, Italy: Springer. 247-266.
Drielsma, P. H., S. Mödersheim, and L. Viganò. 2005. "A Formalization of Off-line Guessing for Security Protocol Analysis". In: *Logic for Programming, Artificial Intelligence, and Reasoning: 11th International Conference, LPAR 2004*. Ed. by F. Baader and A. Voronkov. Vol. 3452. *Lecture Notes in Computer Science*. Montevideo, Uruguay: Springer. 363–379.

Dupressoir, F., A. D. Gordon, J. Jürjens, and D. A. Naumann. 2011. "Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols". In: *24th IEEE Symposium on Computer Security Foundations (CSF'11)*. Paris, France: IEEE Computer Society. 3–17.

Durgin, N., P. Lincoln, J. C. Mitchell, and A. Scedrov. 2004. "Multiset Rewriting and the Complexity of Bounded Security Protocols". *Journal of Computer Security*. 12(2): 247–311.

Escobar, S., J. Hendrix, C. Meadows, and J. Meseguer. 2007. "Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer". In: *Proc. 2nd International Workshop on Security and Rewriting Techniques (SecReT 2007)*.

Escobar, S., D. Kapur, C. Lynch, C. Meadows, J. Meseguer, P. Narendran, and R. Sasse. 2011. "Protocol analysis in Maude-NPA using unification modulo homomorphic encryption". In: *13th international ACM SIGPLAN symposium on Principles and practices of declarative programming (PPDP'11)*. Odense, Denmark: ACM. 65–76.

Escobar, S., C. Meadows, and J. Meseguer. 2006. "A rewriting-based inference system for the NRL Protocol Analyzer and its meta-logical properties". *Theoretical Computer Science*. 367(1-2): 162–202.

Fournet, C. and M. Kohlweiss. 2011. "Modular Cryptographic Verification by Typing". In: *7th Workshop on Formal and Computational Cryptography (FCC'11)*. Paris, France.

Godskesen, J. C. 2006. "Formal Verification of the ARAN Protocol Using the Applied Pi-calculus". In: *Sixth International IFIP WG 1.7 Workshop on Issues in the Theory of Security (WITS'06)*. Vienna, Austria. 99–113.

Gordon, A. and A. Jeffrey. 2004. "Types and Effects for Asymmetric Cryptographic Protocols". *Journal of Computer Security*. 12(3/4): 435–484.
Goubault-Larrecq, J. 2005. "Deciding $H_1$ by resolution". *Information Processing Letters*. 95(3): 401-408.

Goubault-Larrecq, J. and F. Parrennes. 2005. "Cryptographic Protocol Analysis on Real C Code". In: *6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05)*. Ed. by R. Cousot. Vol. 3385. *Lecture Notes in Computer Science*. Paris, France: Springer. 363-379.

Heather, J., G. Lowe, and S. Schneider. 2000. "How to Prevent Type Flaw Attacks on Security Protocols". In: *13th IEEE Computer Security Foundations Workshop (CSFW-13)*. Cambridge, England. 255-268.

Hüttel, H. 2003. "Deciding Framed Bisimilarity". *Electronic Notes in Theoretical Computer Science*. 68(6): 1-20. Special issue Infinity'02: 4th International Workshop on Verification of Infinite-State Systems.

Kallahalla, M., E. Riedel, R. Swaminathan, Q. Wang, and K. Fu. 2003. "Plutus: Scalable secure file sharing on untrusted storage". In: *2nd Conference on File and Storage Technologies (FAST'03)*. San Francisco, CA: Usenix. 29-42.

Khurana, H. and H.-S. Hahm. 2006. "Certified Mailing Lists". In: *ACM Symposium on Communication, Information, Computer and Communication Security (ASIACCS'06)*. Taipei, Taiwan: ACM. 46-58.

Kowalski, R. 1974. "Predicate Logic as Programming Language". In: *Proceedings IFIP Congress*. Stockholm: North Holland. 569-574.

Kremer, S. and R. Künnemann. 2014. "Automated Analysis of Security Protocols with Global State". In: *35th IEEE Symposium on Security and Privacy (S&P'14)*. San Jose, CA, USA: IEEE Computer Society.

Kremer, S. and M. D. Ryan. 2005. "Analysis of an Electronic Voting Protocol in the Applied Pi Calculus". In: *Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005*. Ed. by M. Sagiv. Vol. 3444. *Lecture Notes in Computer Science*. Edimbourg, UK: Springer. 186-200.

Küsters, R. and T. Truderung. 2008. "Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach". In: *15th ACM conference on Computer and communications security (CCS'08)*. Alexandria, Virginia, USA: ACM. 129-138.
Küsters, R. and T. Truderung. 2009. "Using ProVerif to Analyze Protocols with Diffie-Hellman Exponentiation". In: *22nd IEEE Computer Security Foundations Symposium (CSF'09)*. Port Jefferson, New York, USA: IEEE. 157-171.

Lowe, G. 1996. "Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR". In: *Tools and Algorithms for the Construction and Analysis of Systems*. Vol. 1055. Lecture Notes in Computer Science. Springer. 147-166.

Lowe, G. 1997. "A Hierarchy of Authentication Specifications". In: *10th Computer Security Foundations Workshop (CSFW '97)*. IEEE Computer Society. Rockport, Massachusetts. 31-43.

Lowe, G. 2002. "Analyzing Protocols Subject to Guessing Attacks". In: *Workshop on Issues in the Theory of Security (WITS'02)*. Portland, Oregon.

Lux, K. D., M. J. May, N. L. Bhattad, and C. A. Gunter. 2005. "WSE-mail: Secure Internet Messaging Based on Web Services". In: *International Conference on Web Services (ICWS'05)*. Orlando, Florida: IEEE Computer Society. 75-82.

Meadows, C. A. 1996. "The NRL Protocol Analyzer: An Overview". *Journal of Logic Programming*. 26(2): 113-131.

Meadows, C. and P. Narendran. 2002. "A Unification Algorithm for the Group Diffie-Hellman Protocol". In: *Workshop on Issues in the Theory of Security (WITS'02)*. Portland, Oregon.

Meier, S., C. Cremers, and D. Basin. 2010. "Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs". In: *23rd IEEE Computer Security Foundations Symposium (CSF'10)*. Edinburgh, UK: IEEE. 231-245.

Milicia, G. 2002. "χ-Spaces: Programming Security Protocols". In: *14th Nordic Workshop on Programming Theory (NWPT'02)*. Tallinn, Estonia.

Millen, J. 1999. "A Necessarily Parallel Attack". In: *Workshop on Formal Methods and Security Protocols (FMSP'99)*. Trento, Italy.

Milner, R., J. Parrow, and D. Walker. 1992. "A Calculus of Mobile Processes, parts I and II". *Information and Computation*. 100(Sept.): 1-40 and 41-77.
Mödersheim, S. 2010. "Abstraction by Set-Membership: Verifying Security Protocols and Web Services with Databases". In: *17th ACM Conference on Computer and Communications Security (CCS 2010)*. ACM. Chicago, IL, USA. 351-360.

Mödersheim, S. and L. Viganò. 2009. "The Open-source Fixed-point Model Checker for Symbolic Analysis of Security Protocols". In: *Foundations of Security Analysis and Design V, FOSAD 2007 / 2008 / 2009 Tutorial Lectures*. Ed. by A. Aldini, G. Barthe, and R. Gorrieri. Vol. 5705. *Lecture Notes in Computer Science*. Springer. 166-194.

Monniaux, D. 2003. "Abstracting Cryptographic Protocols with Tree Automata". *Science of Computer Programming*. 47(2-3): 177-202.

Mukhamedov, A., A. D. Gordon, and M. Ryan. 2013. "Towards a Verified Reference Implementation of a Trusted Platform Module". In: *Security Protocols XVII*. Ed. by B. Christianson, J. A. Malcolm, V. Matyáš, and M. Roe. Vol. 7028. *Lecture Notes in Computer Science*. Springer. 69-81.

Needham, R. M. and M. D. Schroeder. 1978. "Using Encryption for Authentication in Large Networks of Computers". *Communications of the ACM*. 21(12): 993-999.

O'Shea, N. 2008. "Using Elyjah to Analyse Java Implementations of Cryptographic Protocols". In: *Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS'08)*. Pittsburgh, PA, USA.

Pankova, A. and P. Laud. 2012. "Symbolic Analysis of Cryptographic Protocols Containing Bilinear Pairings". In: *25th IEEE Computer Security Foundations Symposium (CSF'12)*. Cambridge, MA: IEEE. 63-77.

Paulson, L. C. 1998. "The Inductive Approach to Verifying Cryptographic Protocols". *Journal of Computer Security*. 6(1-2): 85-128.

Pironti, A. and R. Sisto. 2010. "Provably Correct Java Implementations of Spi Calculus Security Protocols Specifications". *Computers and Security*. 29(3): 302-314.
Pottier, F. 2002. "A Simple View of Type-Secure Information Flow in the π-Calculus". In: *15th IEEE Computer Security Foundations Workshop*. Cape Breton, Nova Scotia. 320-330.

Pottier, F. and V. Simonet. 2002. "Information Flow Inference for ML". In: *29th ACM Symposium on Principles of Programming Languages (POPL'02)*. Portland, Oregon. 319-330.

Pozza, D., R. Sisto, and L. Durante. 2004. "Spi2Java: Automatic cryptographic protocol Java code generation from spi calculus". In: *18th International Conference on Advanced Information Networking and Applications (AINA'04)*. Vol. 1. Fukuoka, Japan: IEEE Computer Society. 400-405.

Ramanujam, R. and S. Suresh. 2003. "Tagging Makes Secrecy Decidable with Unbounded Nonces as Well". In: *FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science*. Ed. by P. Pandya and J. Radhakrishnan. Vol. 2914. Lecture Notes in Computer Science. Mumbai, India: Springer. 363-374.

Rusinowitch, M. and M. Turuani. 2003. "Protocol Insecurity with Finite Number of Sessions is NP-complete". *Theoretical Computer Science*. 299(1-3): 451-475.

Santiago, S., S. Escobar, C. Meadows, and J. Meseguer. 2014. "A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA". In: *Security and Trust Management (STM'14)*. Ed. by S. Mauw and C. D. Jensen. Vol. 8743. Lecture Notes in Computer Science. Wroclaw, Poland: Springer. 162-177.

Schmidt, B., S. Meier, C. Cremers, and D. Basin. 2012. "Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties". In: *25th IEEE Computer Security Foundations Symposium (CSF'12)*. Cambridge, MA, USA: IEEE Computer Society. 78-94.

Schmidt, B., R. Sasse, C. Cremers, and D. Basin. 2014. "Automated Verification of Group Key Agreement Protocols". In: *2014 IEEE Symposium on Security and Privacy*. San Jose, CA: IEEE. 179-194.

Smyth, B., M. D. Ryan, and L. Chen. 2015. "Formal analysis of privacy in Direct Anonymous Attestation schemes". *Science of Computer Programming*. 111(2): 300-317.
Song, D., A. Perrig, and D. Phan. 2001. "AGVI—Automatic Generation, Verification, and Implementation of Security Protocols". In: *Computer Aided Verification (CAV'01)*. Ed. by G. Berry, H. Comon, and A. Finkel. Vol. 2102. *Lecture Notes in Computer Science*. Paris, France: Springer. 241–245.

Swamy, N., J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. 2011. "Secure Distributed Programming with Value-dependent Types". In: *16th International Conference on Functional Programming (ICFP 2011)*. Tokyo, Japan: ACM. 266–278.

Tiu, A. and J. Dawson. 2010. "Automating Open Bisimulation Checking for the Spi Calculus". In: *23rd IEEE Computer Security Foundations Symposium (CSF'10)*. Edinburgh, UK: IEEE. 307–321.

Turuani, M. 2006. "The CL-Atse Protocol Analyser". In: *Term Rewriting and Applications, 17th International Conference, RTA 2006*. Ed. by F. Pfenning. Vol. 4098. *Lecture Notes in Computer Science*. Seattle, WA: Springer. 277–286.

Weidenbach, C. 1999. "Towards an Automatic Analysis of Security Protocols in First-Order Logic". In: *16th International Conference on Automated Deduction (CADE-16)*. Ed. by H. Ganzinger. Vol. 1632. *Lecture Notes in Artificial Intelligence*. Trento, Italy: Springer. 314–328.

Woo, T. Y. C. and S. S. Lam. 1993. "A Semantic Model for Authentication Protocols". In: *IEEE Symposium on Research in Security and Privacy*. Oakland, California. 178–194.