# Automated reasoning for equivalences in the applied pi calculus with barriers
,
## Abstract
Observational equivalence allows us to study important security properties such as anonymity. Unfortunately, the difficulty of proving observational equivalence hinders analysis. Blanchet, Abadi & Fournet simplify its proof by introducing a sufficient condition for observational equivalence, called diff-equivalence, which is a reachability condition that can be proved automatically by ProVerif. However, diff-equivalence is a very strong condition, which often does not hold even if observational equivalence does. In particular, when proving equivalence between processes that contain several parallel components, e.g., $P \mid Q$ and $P' \mid Q'$, diff-equivalence requires that $P$ is equivalent to $P'$ and $Q$ is equivalent to $Q'$. To relax this constraint, Delaune, Ryan & Smyth introduced the idea of swapping data between parallel processes $P'$ and $Q'$ at synchronisation points, without proving its soundness. We extend their work by formalising the semantics of synchronisation, formalising the definition of swapping, and proving its soundness. We also relax some restrictions they had on the processes to which swapping can be applied. Moreover, we have implemented our results in ProVerif. Hence, we extend the class of equivalences that can be proved automatically. We showcase our results by analysing privacy in election schemes by Fujioka, Okamoto & Ohta and Lee *et al.*, and in the vehicular ad-hoc network by Freudiger *et al*.
# Introduction
Cryptographic protocols are required to satisfy a plethora of security requirements. These requirements include classical properties such as secrecy and authentication, and emerging properties including anonymity (**Pfitzmann01?**; **DKR08?**; **Delaune10:Vanets?**), ideal functionality (**SpiCalculus?**; **AppliedPi?**; **Delaune09:SimulationBasedAppliedPi?**), and stronger notions of secrecy (**Abadi99?**; **Blanchet04?**; **Cortier07:NotionsSecrecy?**). These security requirements can generally be classified as *indistinguishability* or *reachability* properties. Reachability properties express requirements of a protocol’s reachable states. For example, secrecy can be expressed as the inability of deriving a particular value from any possible protocol execution. By comparison, indistinguishability properties express requirements of a protocol’s observable behaviour. Intuitively, two protocols are said to be indistinguishable if an observer has no way of telling them apart. Indistinguishability enables the formulation of more complex properties. For example, anonymity can be expressed as the inability to distinguish between an instance of the protocol in which actions are performed by a user, from another instance in which actions are performed by another user.
Indistinguishability can be formalised as observational equivalence, denoted $\approx$. As a motivating example, consider an election scheme, in which a voter $A$ voting $v$ is formalised by a process $V(A, v)$. Ballot secrecy can be formalised by the equivalence $$V(A, v) \mid V(B, v') \approx V(A, v') \mid V(B, v)
\label{eq:motiv}$$ which means that no adversary can distinguish when two voters swap their votes (**DKR08?**). (We use the applied pi calculus syntax and terminology (**AppliedPi?**), which we introduce in Section [sec:obs:proverif].)
## Approaches to proving equivalences
Observational equivalence is the tool introduced for reasoning about security requirements of cryptographic protocols in the spi calculus (**SpiCalculus?**) and in the applied pi calculus (**AppliedPi?**). It was originally proved manually, using the notion of labelled bisimilarity (**AG98b?**; **Borgstrom05:SpiBisimulation?**; **AppliedPi?**) to avoid universal quantification over adversaries.
Manual proofs of equivalence are long and difficult, so automating these proofs is desirable. Automation often relies on symbolic semantics (**Borgstrom04:SpiSymbolic?**; **DKR10:Symbolic?**) to avoid the infinite branching due to messages sent by the adversary by treating these messages as variables. For a bounded number of sessions, several decision procedures have been proposed for processes without else branches, first for a fixed set of primitives (**Huttel03:BisimilaritySpi?**; **Durante03:Spi?**), then for a wide variety of primitives with the restriction that processes are determinate, that is, their execution is entirely determined by the adversary inputs (**Cortier09?**). These decision procedures are too complex for useful implementations. Practical algorithms have since been proposed and implemented: SPEC (**Tiu10?**) for fixed primitives and without else branches, APTE (**Cheval11?**) for fixed primitives with else branches and non-determinism, and AKISS (**Kremer12:AKISS?**; **Stefan11:thesis?**) for a wide variety of primitives and determinate processes.
For an unbounded number of sessions, proving equivalence is an undecidable problem (**Huttel03:BisimilaritySpi?**; **Abadi06?**), so automated proof techniques are incomplete. ProVerif automatically proves an equivalence notion, named diff-equivalence, between processes $P$ and $Q$ that share the same structure and differ only in the choice of terms (**BlanchetJLAP07?**). Diff-equivalence requires that the two processes always reduce in the same way, in the presence of any adversary. In particular, the two processes must have the same branching behaviour. Hence, diff-equivalence is much stronger than observational equivalence. Maude-NPA (**Santiago14?**) and Tamarin (**Basin15?**) also use that notion, and Baudet (**Baudet07:thesis?**) showed that diff-equivalence is decidable for a bounded number of sessions and used this technique for proving resistance against off-line guessing attacks (**Baudet05?**). Decision procedures also exist for restricted classes of protocols: for an unbounded number of sessions, trace equivalence has a decision procedure for symmetric-key, type-compliant, acyclic protocols (**Chretien15b?**), which is too complex for useful implementation, and for ping-pong protocols (**Chretien15?**), which is implemented in a tool.
## Diff-equivalence and its limitations
The main approach to automate proofs of observational equivalence with an unbounded number of sessions is to use diff-equivalence. (In our motivating example [eq:motiv], a bounded number of sessions is sufficient, but an unbounded number becomes useful in more complex examples, as in Section [sec:lee].) Diff-equivalence seems well-suited to our motivating example, since the processes $V(A, v) \mid V(B, v')$ and $V(A, v') \mid V(B, v)$ differ only by their terms. Such a pair of processes can be represented as a *biprocess* which has the same structure as each of the processes and captures the differences in terms using the construct $\mathsf{diff}[M,M']$, denoting the occurrence of a term $M$ in the first process and a term $M'$ in the second. For example, the pair of processes in our motivating example can be represented as the biprocess $P_1 \triangleq V(A, \mathsf{diff}[v,v']) \mid V(B, \mathsf{diff}[v',v])$. The two processes represented by a biprocess $P$ are recovered by $\mathsf{fst}(P)$ and $\mathsf{snd}(P)$. Hence, $\mathsf{fst}(P_1) = V(A, v) \mid V(B, v')$ and $\mathsf{snd}(P_1) = V(A, v') \mid V(B, v)$.
Diff-equivalence implies observational equivalence. Hence, the equivalence [eq:motiv] can be inferred from the diff-equivalence of the biprocess $P_1$. However, diff-equivalence is so strong that it does not hold for biprocesses modelling even trivial schemes, as the following example demonstrates.
**Example 1**. *Consider an election scheme that instructs voters to publish their vote on an anonymous channel. The voter’s role can be formalised as $V(A, v) = \overline{c}\langle v\rangle$. Thus, ballot secrecy can be analysed using the biprocess $P \triangleq \overline{c}\langle\mathsf{diff}[v,v']\rangle\mid\overline{c}\langle\mathsf{diff}[v',v]\rangle$. It is trivial to see that $\mathsf{fst}(P) = \overline{c}\langle v\rangle\mid\overline{c}\langle v'\rangle$ is indistinguishable from $\mathsf{snd}(P) = \overline{c}\langle v'\rangle\mid\overline{c}\langle v\rangle$, because any output by $\mathsf{fst}(P)$ can be matched by an output from $\mathsf{snd}(P)$, and vice-versa. However, the biprocess $P$ does not satisfy diff-equivalence. Intuitively, this is because diff-equivalence requires that the subprocesses of the parallel composition, namely, $\overline{c}\langle\mathsf{diff}[v,v']\rangle$ and $\overline{c}\langle\mathsf{diff}[v',v]\rangle$, each satisfy diff-equivalence, which is false, because $\overline{c}\langle v\rangle$ is not equivalent to $\overline{c}\langle v'\rangle$ (nor is $\overline{c}\langle v'\rangle$ equivalent to $\overline{c}\langle v\rangle$).*
Overcoming the difficulty encountered in Example 1 is straightforward: using the general property that $P \mid Q \approx Q \mid P$, we can instead prove $$V(A, v) \mid V(B, v') \approx V(B, v) \mid V(A, v')
%\label{eq:motiv2}$$ which, in the case of Example 1, is proved by noticing that the two sides of the equivalence are equal, i.e., by noticing that the biprocess $\hat P \triangleq \overline{c}\langle\mathsf{diff}[v,v]\rangle\mid\overline{c}\langle\mathsf{diff}[v',v']\rangle$ trivially satisfies diff-equivalence, since $\mathsf{fst}(\hat P)=\mathsf{snd}(\hat P)$. However, this technique cannot be applied to more complex examples, as we show below.
Some security properties (e.g., privacy in elections (**DKR08?**; **Backes08:Voting?**), vehicular ad-hoc networks (**Delaune10:Vanets?**; **Delaune11:Vanets?**), and anonymity networks (**RR98?**; **Pfitzmann01?**; **Chothia06:Mute?**)) can only be realised if processes synchronise their actions in a specific manner.
**Example 2**. *Building upon Example 1, suppose each voter sends their identity, then their vote, both on an anonymous channel, i.e., $V(A, v) = \overline{c}\langle A\rangle.\overline{c}\langle v\rangle$. This example does not satisfy ballot secrecy, because $V(A, v) \mid V(B, v')$ can output $A$, $v$, $B$, $v'$ on channel $c$ in that order, while $V(A, v') \mid V(B, v)$ cannot.*
To modify this example so that it satisfies ballot secrecy, we use the notion of barrier synchronisation, which ensures that a process will block, when a barrier is encountered, until all other processes executing in parallel reach this barrier (**Brooks86:Barriers?**; **Hensgen88:Barriers?**; **Arenstorf89:Barriers?**; **Lubachevsky89:Barriers?**).
**Example 3**. *Let us modify the previous example so that voters publish their identity, synchronise with other voters, and publish their vote on an anonymous channel. The voter’s role can be formalised as process $V(A, v) = \overline{c}\langle A\rangle.1\textnormal{::}\,\overline{c}\langle v\rangle$, where $1\textnormal{::}\,$ is a barrier synchronisation. Ballot secrecy can then be analysed using biprocess $P_{\sf ex}\triangleq \overline{c}\langle A\rangle.1\textnormal{::}\,\overline{c}\langle\mathsf{diff}[v,v']\rangle\mid\overline{c}\langle B\rangle.1\textnormal{::}\,\overline{c}\langle\mathsf{diff}[v',v]\rangle$. Synchronisation ensures the output of $A$ and $B$, prior to $v$ and $v'$, in both $\mathsf{fst}(P_{\sf ex})$ and $\mathsf{snd}(P_{\sf ex})$, so that ballot secrecy holds, but diff-equivalence does not hold.*
The technique used to overcome the difficulty in Example 1 cannot be applied here, because swapping the two voting processes leads to the biprocess $P_{\sf ex}' \triangleq \overline{c}\langle\mathsf{diff}[A,B]\rangle.1\textnormal{::}\,\overline{c}\langle v\rangle\mid\overline{c}\langle\mathsf{diff}[B,A]\rangle.1\textnormal{::}\,\overline{c}\langle v'\rangle$, which does not satisfy diff-equivalence. Intuitively, we need to swap at the barrier, not at the beginning (cf. $P_{\sf ex}'$). In essence, by swapping data between the two voting processes at the barrier, it suffices to prove that the biprocess $P_{\sf ex}'' \triangleq \overline{c}\langle A\rangle.1\textnormal{::}\,\overline{c}\langle\mathsf{diff}[v,v]\rangle\mid\overline{c}\langle B\rangle.1\textnormal{::}\,\overline{c}\langle\mathsf{diff}[v',v']\rangle$ satisfies diff-equivalence, which trivially holds since $\mathsf{fst}(P_{\sf ex}'')=\mathsf{snd}(P_{\sf ex}'')$.
As illustrated in , diff-equivalence is a sufficient condition for observational equivalence, but it is not necessary, and this precludes the analysis of interesting security properties. In this paper, we will partly overcome this limitation: we weaken the diff-equivalence requirement by allowing swapping of data between processes at barriers.
## Contributions
First, we extend the process calculus by Blanchet, Abadi & Fournet (**BlanchetJLAP07?**) to capture barriers (Section [sec:obs:proverif]). Secondly, we formally define a compiler that encodes barriers and swapping using private channel communication (Section [sec:proswapper]). As a by-product, if we compile without swapping, we also obtain an encoding of barriers into the calculus without barriers, via private channel communication. Thirdly, we provide a detailed soundness proof for this compiler. (Details of the proof are in the long version of this paper (**LongVersion?**).) Fourthly, we have implemented our compiler in ProVerif. Hence, we extend the class of equivalences that can be proved automatically. Finally, we analyse privacy in election schemes and in a vehicular ad-hoc network to showcase our results (Section [sec:obs:example]).
## Comparison with Delaune, Ryan & Smyth
The idea of swapping data at barriers was informally introduced by Delaune, Ryan & Smyth (**Smyth08:Obs?**; **Smyth07:Obs:Dagstuhl?**). Our contributions improve upon their work by providing a strong theoretical foundation to their idea. In particular, they do not provide a soundness proof, we do; they prohibit replication and place restrictions on control flow and parallel composition, we relax these conditions; and they did not implement their results, we implement ours. (Smyth presented a preliminary version of our compiler in his thesis (**Smyth10:thesis?**), and Klus, Smyth & Ryan implemented that compiler (**Smyth10:ObsA?**).)
# Process calculus
We recall Blanchet, Abadi & Fournet’s dialect (**BlanchetJLAP07?**) of the applied pi calculus (**AppliedPi?**; **SmythPi10?**). This dialect is particularly useful due to the automated support provided by ProVerif (**Smyth10:ProVerifManual?**). The semantics of the applied pi calculus (**AppliedPi?**) and the dialect of (**BlanchetJLAP07?**) were defined using structural equivalence. Those semantics have been simplified by semantics with configurations and without structural equivalence, first for trace properties (**Abadi04f?**), then for equivalences (**Baudet07:thesis?**; **BlanchetHDR08?**; **ArapinisLiuRitterRyanPOST14?**). In this paper, we use the latter semantics. In addition, we extend the calculus to capture barrier synchronisation, by giving the syntax and formal semantics of barriers.
## Syntax and semantics
The calculus assumes an infinite set of *names*, an infinite set of *variables*, and a finite set of *function symbols* (*constructors* and *destructors*), each with an associated arity. We write $f$ for a constructor, $g$ for a destructor, and $h$ for a constructor or destructor; constructors are used to build terms, whereas destructors are used to manipulate terms in expressions. Thus, *terms* range over names, variables, and applications of constructors to terms, and *expressions* allow applications of function symbols to expressions (Fig. 1). We use metavariables $u$ and $w$ to range over both names and variables. *Substitutions* $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ replace $x$ with $M$. Arbitrarily large substitutions can be written as $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}},\ldots,\textnormal{\raisebox{2pt}{\footnotesize $M_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_n$}}\}$ and the letters $\sigma$ and $\tau$ range over substitutions. We write $M\sigma$ for the result of applying $\sigma$ to the variables of $M$. Similarly, *renamings* $\{\textnormal{\raisebox{2pt}{\footnotesize $u$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $w$}}\}$ replace $w$ with $u$, where $u$ and $w$ are both names or both variables.
The semantics of a destructor $g$ of arity $l$ are given by a finite set $\mathsf{def}(g)$ of rewrite rules $g(M'_1, \ldots, M'_l) \rightarrow M'$, where $M'_1,\ldots, M'_l, M'$ are terms that contain only constructors and variables, the variables of $M'$ must be bound in $M'_1, \ldots, M'_l$, and variables are subject to renaming. The evaluation of expression $g(M_1, \ldots, M_l)$ succeeds if there exists a rewrite rule $g(M'_1,
\ldots, M'_l) \rightarrow M'$ in $\mathsf{def}(g)$ and a substitution $\sigma$ such that $M_i = M'_i\sigma$ for all $i \in \{ {1}, \ldots, {l}\}$, and in this case $g(M_1, \ldots, M_l)$ evaluates to $M'\sigma$. In order to avoid distinguishing constructors and destructors in the semantics of expressions, we let $\mathsf{def}(f)$ be $\{f(x_1,\dots,x_l)\rightarrow f(x_1,\dots,x_l)\}$, where $f$ is a constructor of arity $l$. In particular, we use $n$-ary constructors $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1,\dots,\allowbreak M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ for tuples, and unary destructors $\pi_{i,n}$ for projections, with the rewrite rule $\pi_{i,n}(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{x_1,\dots,\allowbreak x_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}) \rightarrow x_i$ for all $i \in \{1, \dots, n\}$. ProVerif supports both rewrite rules and equations (**BlanchetJLAP07?**); we omit equations in this paper for simplicity. It is straightforward to extend our proofs to equations, and our implementation supports them.
The grammar for *processes* is presented in Fig. 1. The process $\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q$ tries to evaluate $D$; if this succeeds, then $x$ is bound to the result and $P$ is executed, otherwise, $Q$ is executed. We define the conditional $\textnormal{if } M=N \textnormal{ then } P \textnormal{ else }Q$ as $\textnormal{let } x=\mathsf{eq}(M,N) \textnormal{ in } P \textnormal{ else }Q$, where $x$ is a fresh variable, $\mathsf{eq}$ is a binary destructor, and $\mathrm{def}(\mathsf{eq}) = \{\mathsf{eq}(y,y) \rightarrow y\}$; we always include $\mathsf{eq}$ in our set of function symbols. The else branches may be omitted when $Q$ is the null process. The rest of the syntax is standard (see (**BlanchetHDR08?**; **BlanchetJLAP07?**; **Blanchet04?**)), except for barriers, which we explain below.
̄ ̄ ̄
M, N : :=terms a, b, c, …, k, …, m, n, …, sname x, y, zvariable f(M1, …, Ml)constructor application D : :=expressions Mterm h(D1, …, Dl)function evaluation P, Q, R : :=processes 0null process P ∣ Qparallel composition !Preplication νa.Pname restriction M(x).Pmessage input $\overline{M}\langle N\rangle.P$message output $\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q$expression evaluation $t\textnormal{::}\,{P}$barrier
Syntax for terms and processes
Our syntax allows processes to contain barriers $t\textnormal{::}\,P$, where $t\in\mathbb{N}$. Intuitively, $t\textnormal{::}\,P$ blocks $P$ until all processes running in parallel are ready to synchronise at barrier $t$. In addition, barriers are ordered, so $t\textnormal{::}\,P$ is also blocked if there are any barriers $t'$ such that $t'[sec:syncelim].
The *scope* of names and variables is delimited by binders $\nu\,n$, $M(x)$, and $\textnormal{let } x=D \textnormal{ in}$. The set of free names $\mathsf{fn}(P)$ contains every name $n$ in $P$ which is not under the scope of the binder $\nu\,n$. The set of free variables $\mathsf{fv}(P)$ contains every variable $x$ in $P$ which is not under the scope of a message input $M(x)$ or an expression evaluation $\textnormal{let } x=D \textnormal{ in}$. Using similar notation, the set of names in a term $M$ is denoted $\mathsf{fn}(M)$ and the set of variables in a term $M$ is denoted $\mathsf{fv}(M)$. We naturally extend these functions to multisets ${\mathcal P}$ of processes by $\mathsf{fn}({\mathcal P}) = \bigcup_{P\in{\mathcal P}} \mathsf{fn}(P)$ and $\mathsf{fv}({\mathcal P}) = \bigcup_{P\in{\mathcal P}} \mathsf{fv}(P)$. A term $M$ is ground if $\mathsf{fv}(M) = \emptyset$, a substitution $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ is ground if $M$ is ground, and a process $P$ is closed if $\mathsf{fv}(P) = \emptyset$. Processes are considered equal modulo renaming of bound names and variables. As usual, substitutions avoid name and variable capture, by first renaming bound names and variables to fresh names and variables, respectively.
M ⇓ M(M is a term, so it does not contain destructors) h(D1, …, Dl) ⇓ Nσ if
there exist h(N1, …, Nl) → N ∈ def(h) and σ such that
for all i ∈ {1, …, l} we have Di ⇓ Mi and Mi = Niσ$$\begin{aligned}
&B,E,{\mathcal P}\cup \{0\}\;\rightarrow\;B,E,{\mathcal P}\tag*{{\ensuremath{\mbox{\sc (Red Nil)}}}}\\[3mm]
&B,E,{\mathcal P}\cup \{P \mid Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{P,Q\} \tag*{{\ensuremath{\mbox{\sc (Red Par)}}}}\\[3mm]
&B,E,{\mathcal P}\cup \{!P\}\;\rightarrow\;B,E,{\mathcal P}\cup \{P,!P\} \tag*{{\ensuremath{\mbox{\sc (Red Repl)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\nu\,n.P\}\;\rightarrow\;B,E \cup \{n'\},{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $n'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $n$}}\}\}\\
&\textrm{for some name }n'\textrm{ such that }n'\not\in E \cup \mathsf{fn}({\mathcal P}\cup \{\nu\,n.P\})
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Res)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N(x).Q\}\;\rightarrow\\
&\qquad\qquad B,E,{\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red I/O)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\\
&\qquad\qquad B,E,{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}\\
&\textrm{if }D\Downarrow M
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Destr 1)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{Q\}\\
&\textrm{if there is no $M$ such that }D\Downarrow M
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Destr 2)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{t\textnormal{::}\,P_1,\dots,t\textnormal{::}\,P_n\} \;\rightarrow\\
&\qquad\qquad B\backslash\{t^n\},E,{\mathcal P}\cup \{P_1,\dots,P_n\}\\
&\textrm{if $n\geq 1$ and for all $t'$ such that $t' \leq t$, we have}\\
&\textrm{$t'\not\in B\backslash\{t^n\}$, where $t^n$ denotes $n$ copies of $t$.}
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Bar)}}}}
\end{aligned}$$
Operational semantics
The operational semantics is defined by reduction ($\rightarrow$) on *configurations*. A configuration $\Conf$ is a triple $B,E,{\mathcal P}$, where $B$ is a finite multiset of integers, $E$ is a finite set of names, and ${\mathcal P}$ is a finite multiset of closed processes. The multiset $B$ contains the barriers that control the synchronisation of processes in ${\mathcal P}$. The set $E$ is initially empty and is extended to include any names introduced during reduction, namely, those names introduced by ${\ensuremath{\mbox{\sc (Red Res)}}}$. When $E = \{\tilde a\}$ and ${\mathcal P}= \{P_1, \dots, P_n\}$, the configuration $B,E,{\mathcal P}$ intuitively stands for $\nu\,\tilde a.(P_1 \mid \dots \mid P_n)$. We consider configurations as equal modulo any renaming of the names in $E, {\mathcal P}$ that leaves $\mathsf{fn}({\mathcal P})\setminus E$ unchanged. The initial configuration for a closed process $P$ is $\Initconf{P} = \mathsf{barriers}(P), \emptyset, \{P\}$. Fig. 2 defines reduction rules for each construct of the language. The rule ${\ensuremath{\mbox{\sc (Red Repl)}}}$ creates a new copy of the replicated process $P$. The rule ${\ensuremath{\mbox{\sc (Red Res)}}}$ reduces $\nu\,n$ by creating a fresh name $n'$, adding it to $E$, and substituting it for $n$. The rule ${\ensuremath{\mbox{\sc (Red I/O)}}}$ performs communication: the term $M$ sent by $\overline{N}\langle M\rangle.P$ is received by $N(x).Q$, and substituted for $x$. The rules ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$ and ${\ensuremath{\mbox{\sc (Red Destr 2)}}}$ treat expression evaluations. They first evaluate $D$, using the relation $D \Downarrow M$, which means that the expression $D$ evaluates to the term $M$, and is also defined in Fig. 2. When this evaluation succeeds, ${\ensuremath{\mbox{\sc (Red Destr 1)}}}$ substitutes the result $M$ for $x$ and runs $P$. When it fails, ${\ensuremath{\mbox{\sc (Red Destr 2)}}}$ runs $Q$. Finally, the new rule ${\ensuremath{\mbox{\sc (Red Bar)}}}$ performs barrier synchronisation: it synchronises on the lowest barrier $t$ in $B$. If $t$ occurs $n$ times in $B$, it requires $n$ processes $t\textnormal{::}\,P_1,\dots,t\textnormal{::}\,P_n$ to be ready to synchronise, and in this case, it removes barrier $t$ both from $B$ and from these processes, which can then further reduce. A configuration $B,E,{\mathcal P}$ is *valid* when $\mathsf{barriers}({\mathcal P}) \subseteq B$. It is easy to check that the initial configuration is valid and that validity is preserved by reduction. We shall only manipulate valid configurations.
**Example 1**. *Let us consider the parallel composition of processes $P\triangleq\overline{c}\langle k\rangle.1\textnormal{::}\,c(x)$, $Q\triangleq\nu\,n.1\textnormal{::}\,\overline{c}\langle n\rangle$, and $R\triangleq c(x)$, which yields the initial configuration $\Conf = \{1^2\},\;\emptyset,\;\{P\mid Q \mid R\}$, since the process $P\mid Q \mid R$ contains two barriers 1. We have $$\begin{aligned}
\Conf &= \{1^2\},\;\emptyset,\;\{P\mid Q \mid R\}\\
&\xrightarrow{}\{1^2\},\emptyset,\{P,\;Q \mid R\} \tag*{by {\ensuremath{\mbox{\sc (Red Par)}}}} \\
&\xrightarrow{}\{1^2\},\emptyset,\{P,\;Q,\;R\} \tag*{by {\ensuremath{\mbox{\sc (Red Par)}}}} \\
&\xrightarrow{}\{1^2\},\emptyset,\{1\textnormal{::}\,c(x),\;Q,\; 0\} \tag*{by {\ensuremath{\mbox{\sc (Red I/O)}}}} \\
&\xrightarrow{}\{1^2\},\emptyset,\{1\textnormal{::}\,c(x),\;Q\} \tag*{by {\ensuremath{\mbox{\sc (Red Nil)}}}} \\
&\xrightarrow{}\{1^2\},\{n'\},\{1\textnormal{::}\,c(x),\;1\textnormal{::}\,\overline{c}\langle n'\rangle\} \tag*{by {\ensuremath{\mbox{\sc (Red Res)}}}} \\
&\xrightarrow{}\emptyset,\{n'\},\{c(x),\;\overline{c}\langle n'\rangle\} \tag*{by {\ensuremath{\mbox{\sc (Red Bar)}}}} \\
&\xrightarrow{}\emptyset,\{n'\},\{0,\; 0\} \tag*{by {\ensuremath{\mbox{\sc (Red I/O)}}}} \\
&\xrightarrow{}\emptyset,\{n'\},\{0\} \tag*{by {\ensuremath{\mbox{\sc (Red Nil)}}}} \\
&\xrightarrow{}\emptyset,\{n'\},\emptyset \tag*{by {\ensuremath{\mbox{\sc (Red Nil)}}}}
\end{aligned}$$*
## Observational equivalence
Intuitively, configurations $\Conf$ and $\Conf'$ are observationally equivalent if they can output on the same channels in the presence of any adversary. Formally, we adapt the definition of observational equivalence by Arapinis *et al.* (**ArapinisLiuRitterRyanPOST14?**) to consider barriers rather than mutable state. We define a *context* $C[\_]$ to be a process with a hole. We obtain $C[P]$ as the result of filling $C[\_]$’s hole with process $P$. We define *adversarial contexts* as contexts $\nu\,\tilde n.(\_ \mid Q)$ with $\mathsf{fv}(Q) = \emptyset$ and $\mathsf{barriers}(Q) = \emptyset$. When $\Conf = B, E, {\mathcal P}$ and $C[\_]= \nu\,\tilde n.(\_ \mid Q)$ is an adversarial context, we define $C[\Conf] = B,E \cup \{\tilde n\},{\mathcal P}\cup\{Q\}$, after renaming the names in $E,{\mathcal P}$ so that $E \cap \mathsf{fn}(Q) = \emptyset$. A configuration $\Conf = B,E,{\mathcal P}$ can output on a channel $N$, denoted, $\Conf\downarrow_N$, if there exists $\overline{N}\langle M\rangle.P\in{\mathcal P}$ with $\mathsf{fn}(N) \cap E = \emptyset$, for some term $M$ and process $P$.
**Definition 1** (Observational equivalence). *Observational equivalence between configurations $\approx$ is the largest symmetric relation $\mathrel{\mathcal{R}}$ between valid configurations such that $\Conf \mathrel{\mathcal{R}}\Conf'$ implies:*
1. *if $\Conf\downarrow_N$, then $\Conf'\xrightarrow{}^*\downarrow_N$, for all $N$;*
2. *if $\Conf \rightarrow \Conf_1$, then $\Conf' \rightarrow^* \Conf_1'$ and $\Conf_1 \mathrel{\mathcal{R}}\Conf_1'$, for some $\Conf_1'$.*
3. *$C[\Conf] \mathrel{\mathcal{R}}C[\Conf']$ for all adversarial contexts $C[\_]$.*
*Closed processes $P$ and $P'$ are *observationally equivalent*, denoted $P \approx P'$, if $\Initconf{P} \approx\Initconf{P'}$.*
The definition first formulates observational equivalence on semantic configurations. Item 1 guarantees that, if a configuration $\Conf$ outputs on a public channel, then so does $\Conf'$. Item 2 guarantees that this property is preserved by reduction, and Item 3 guarantees that it is preserved in the presence of any adversary. Finally, observational equivalence is formulated on closed processes.
## Biprocesses
The calculus defines syntax to model pairs of processes that have the same structure and differ only by the terms that they contain. We call such a pair of processes a *biprocess*. The grammar for biprocesses is an extension of Fig. 1, with additional cases so that $\mathsf{diff}[M,M']$ is a term and $\mathsf{diff}[D,D']$ is an expression. (We occasionally refer to processes and biprocesses as processes when it is clear from the context.) Given a biprocess $P$, we define processes $\mathsf{fst}(P)$ and $\mathsf{snd}(P)$ as follows: $\mathsf{fst}(P)$ is obtained by replacing all occurrences of $\mathsf{diff}[M,M']$ with $M$ and $\mathsf{snd}(P)$ is obtained by replacing $\mathsf{diff}[M,M']$ with $M'$. We define $\mathsf{fst}(D)$, $\mathsf{fst}(M)$, $\mathsf{snd}(D)$, and $\mathsf{snd}(M)$ similarly, and naturally extend these functions to multisets of biprocesses by $\mathsf{fst}({\mathcal P}) = \{\mathsf{fst}(P) \mid P\in{\mathcal P}\}$ and $\mathsf{snd}({\mathcal P}) = \{\mathsf{snd}(P) \mid P\in{\mathcal P}\}$, and to configurations by $\mathsf{fst}(B,E,{\mathcal P}) = B,E,\mathsf{fst}({\mathcal P})$ and $\mathsf{snd}(B,E,{\mathcal P}) = B,E,\mathsf{snd}({\mathcal P})$. The standard definitions of $\mathsf{barriers}$, free names, and free variables apply to biprocesses as well. Observational equivalence can be formalised as a property of biprocesses:
$$\begin{aligned}
\begin{split}
&B,E,{\mathcal P}\cup \{\overline{N}\langle M\rangle.P, N'(x).Q\}\;\rightarrow\\
&\qquad\qquad B,E,{\mathcal P}\cup \{P,Q\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}\\
&\textrm{if }\mathsf{fst}(N)=\mathsf{fst}(N')\textrm{ and }\mathsf{snd}(N)=\mathsf{snd}(N')
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red I/O)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\\
&\qquad \qquad B,E,{\mathcal P}\cup \{P\{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{diff}[M,M']$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}\}\\
&\textrm{if }\mathsf{fst}(D)\Downarrow M\textrm{ and }\mathsf{snd}(D)\Downarrow M'
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Destr 1)}}}}\\[3mm]
\begin{split}
&B,E,{\mathcal P}\cup \{\textnormal{let } x=D \textnormal{ in } P \textnormal{ else }Q\}\;\rightarrow\;B,E,{\mathcal P}\cup \{Q\}\\
&\textrm{if there is no $M$ such that }\mathsf{fst}(D)\Downarrow M\\
&\textrm{and no $M'$ such that }\mathsf{snd}(D)\Downarrow M'
\end{split}\tag*{{\ensuremath{\mbox{\sc (Red Destr 2)}}}}
\end{aligned}$$
The semantics for biprocesses includes the rules in Fig. 2, except for $\mbox{\sc (Red I/O)}$, $\mbox{\sc (Red Destr 1)}$, and $\mbox{\sc (Red Destr 2)}$ which are revised in Fig. 3. It follows from this semantics that, if $\Conf \xrightarrow{}\Conf'$, then $\mathsf{fst}(\Conf) \xrightarrow{}\mathsf{fst}(\Conf')$ and $\mathsf{snd}(\Conf) \xrightarrow{}\mathsf{snd}(\Conf')$. In other words, a biprocess reduces when the two underlying processes reduce in the same way. However, reductions in $\mathsf{fst}(\Conf)$ or $\mathsf{snd}(\Conf)$ do not necessarily imply reductions in $\Conf$, that is, there exist configurations $\Conf$ such that $\mathsf{fst}(\Conf) \xrightarrow{}\mathsf{fst}(\Conf')$, but there is no such reduction $\Conf \xrightarrow{}\Conf'$, and symmetrically for $\mathsf{snd}(\Conf)$. For example, given the configuration $\Conf = \emptyset,\emptyset,\{\overline{\mathsf{diff}[a,c]}\langle n\rangle.0,a(x).0\}$, we have $\mathsf{fst}(\Conf) \xrightarrow{}\emptyset,\emptyset,\{0,0\}$, but there is no reduction $\Conf \xrightarrow{}\emptyset,\emptyset,\{0,0\}$. Formally, this behaviour can be captured using the *divergence* relation ($\uparrow$) for configurations (Fig. 4) (**Baudet07:thesis?**). Divergence can occur because either: i) one process can perform a communication and the other cannot, by rule ${\ensuremath{\mbox{\sc (Div I/O)}}}$; or ii) the evaluation of an expression succeeds in one process and fails in the other, by rule ${\ensuremath{\mbox{\sc (Div Destr)}}}$. Using the notion of *diff-equivalence* (Definition 3), Theorem 1 shows that a biprocess $P$ satisfies observational equivalence when reductions in $C[\Initconf{\mathsf{fst}(P)}]$ or $C[\Initconf{\mathsf{snd}(P)}]$ imply reductions in $C[\Initconf{P}]$ for all adversarial contexts $C[\_]$, that is, configurations obtained from $C[\Initconf{P}]$ never diverge.
**Definition 3** (Diff-equivalence). *A closed biprocess $P$ satisfies *diff-equivalence* if for all adversarial contexts $C[\_]$, there is no configuration $\Conf$ such that $C[\Initconf{P}] \xrightarrow{}^*\Conf$ and $\Conf \uparrow$.*
**Theorem 1**. *Let $P$ be a closed biprocess without barriers. If $P$ satisfies diff-equivalence, then $P$ satisfies observational equivalence.*
Theorem 1 can be proved by adapting the proof of Blanchet, Abadi & Fournet (**BlanchetJLAP07?**, Theorem 1), which presents a similar result using a semantics based on structural equivalence and reduction instead of reduction on configurations.
# Automated reasoning
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 684, column 15): unexpected end of input expecting \end{IEEEproof} ^`
``` latex
\section{Automated reasoning}\label{sec:proswapper}
To prove equivalence, we define a compiler from a biprocess (containing barriers)
to a set of biprocesses without barriers.
The biprocesses in that set permit various swapping strategies.
We show that if one of these biprocesses satisfies diff-equivalence,
then the original biprocess satisfies observational equivalence.
The compiler works in two steps:
\begin{enumerate}
\item Function $\precompilerSymb$ annotates barriers with the data to be swapped
and channels for sending and receiving such data.
\item Function $\stageElimSecondSymb$ translates the biprocess with annotated barriers
into biprocesses without barriers, which encode barriers using
communication (inputs and outputs). We exploit this communication
to allow swapping, by sending back data to a different barrier.
\end{enumerate}
We introduce annotated barriers (\S\ref{sec:barrannot}) and
define these two steps (\Ss\ref{sec:barrierAnnotation} and~\ref{sec:compiler}) below.
By combining these two steps we obtain our compiler (\S\ref{sec:completeCompiler}),
which we have implemented in ProVerif~1.94 (\url{http://proverif.inria.fr/}).
The proof of soundness shows that these two steps preserve the
observational behaviour of the biprocesses, so that if a compiled biprocess satisfies
observational equivalence, then so does the initial biprocess.
\subsection{Process calculus with annotated barriers}\label{sec:barrannot}
% Barrier annotation}\label{sec:barrannot}
We introduce an \emph{annotated barrier} construct $\sstageA{t}{a,\allowbreak c,\allowbreak \varsigma}P$, which is not present in the syntax introduced in \S\ref{sec:obs:proverif}, but is used by our compiler. In this construct, $a$ and $c$ are distinct channel names: channel $a$ will be used for sending swappable data, and channel $c$ for receiving swapped data.\ifLONG\footnote{The use of distinct channels is not strictly necessary, but aids automation, in particular, it helps avoid an incompleteness issue of ProVerif that arises because ProVerif assumes that a message output on channel $a$ may be received at any input on channel $a$, even when the output and the input in question cannot appear in parallel.}\fi\
%% \bb{If we have space, I would be happy to keep the footnote in the conference version.\\
%% BS: I dropped the footnote because it is an implementation detail, rather than a theoretical detail.
%% We could drop it entirely, but it is rather important. If there are any other key implementation
%% details, then we could include those too. (We have some notes about such details in the tex files.)
%% If you think we should include the footnote in the conference version, then please include it.}
Moreover, the \emph{ordered substitution}
$\varsigma = (\subst{M_1}{x_1}, \ldots, \subst{M_n}{x_n})$ collects swappable data
$M_1, \dots, M_n$ and associates these terms with variables $x_1, \dots, x_n$;
the process $P$ uses these variables instead of the terms $M_1, \dots, M_n$.
The ordered substitution $\varsigma$ is similar to a substitution, except that the
elements $\subst{M_1}{x_1}, \ldots, \subst{M_n}{x_n}$ are ordered. %, hence the name ordered substitution.
(We indicate ordering using parentheses instead of braces.) The ordering is used to designate each variable in the
domain unambiguously.
We define $\dom{\varsigma} = \{x_1, \ldots, x_n\}$ and
$\range{\varsigma} = \{ M_1, \ldots, M_n \}$.
The annotated barrier $\sstageA{t}{a,c,\varsigma}P$ binds the variables in the domain of $\varsigma$ in $P$, so we extend the functions $\kwf{fn}$ and $\kwf{fv}$ to annotated barriers as follows:
\begin{align*}
& \fn{\sstageA{t}{a,c,\varsigma}P} = \{a, c \} \cup \fn{\range{\varsigma}} \cup \fn{P}\\
& \fv{\sstageA{t}{a,c,\varsigma}P} = \fv{\range{\varsigma}} \cup (\fv{P}\setminus \dom{\varsigma})
\end{align*}
We define the \emph{ordered domain} of $\varsigma$,
$\ordom{\varsigma} = (x_1, \allowbreak \dots, \allowbreak x_n)$, as the tuple containing the variables in the domain of $\varsigma$, in the same order as in the definition of $\varsigma$.
We also introduce a \emph{domain-barrier} construct $\sstageA{t}{a,\allowbreak c,\allowbreak \tup{x}}P$, which is similar to an annotated barrier except that the ordered substitution $\varsigma$ is replaced with a tuple of variables $\tup{x} = (x_1, \dots, x_n)$ corresponding to the ordered domain of $\varsigma$.
%$\ordom{\varsigma}$.
Domain-barriers occur in $\barriers{P}$, but not in processes.
We extend function $\barSym$ to annotated barriers as follows:
\begin{align*}
\begin{split}
& \barriers{\sstageA{t}{a,c,\varsigma}P} = \{ \sstageA{t}{a,c,\ordom{\varsigma}}P \} \cup {}\\
&\phantom{\barriers{\sstageA{t}{a,c,\varsigma}P} = {}\quad}\barriers{P}
\end{split}
\end{align*}
Hence, function $\barSym$ maps processes to multisets of domain-barriers and integers, and domain-barriers include the process that follows the barrier itself.
In addition, we extend $\fstSymb$ and $\sndSymb$ for configurations as follows: $\fst{\sstageA{t}{a,c,\tup{x}}P} = \sstageA{t}{a,c,\tup{x}}\fst{P}$ and $\fst{B, E, \Pcal} = \fst{B}, E, \fst{\Pcal}$, and similarly for $\sndSymb$.
The operational semantics for processes with both standard and annotated barriers
extends the semantics for processes with only standard barriers, with the following rule:
\begin{equation}
\begin{split}
&B,E,\Pcal \cup \{\sstage{t}P_1,\dots,\sstage{t}P_m, \sstageA{t}{a_{m+1},c_{m+1},\varsigma_{m+1}}P_{m+1},\\
&\phantom{B,E,\Pcal \cup \{}\dots, \sstageA{t}{a_n,c_n,\varsigma_n}P_n\} \\
&\rightarrow\;B',E,\Pcal \cup \{P_1,\dots,P_m,P_{m+1}\varsigma_{m+1},\dots,P_n\varsigma_n\}
\end{split}\tag*{\RBarII}
\end{equation}
where $0 \leq m \leq n$, $1 \leq n$, $B = \{ t^m, \allowbreak \sstageA{t}{a_{m+1},\allowbreak c_{m+1},\allowbreak \ordom{\varsigma_{m+1}}}P_{m+1},\allowbreak \dots,\allowbreak \sstageA{t}{a_n,\allowbreak c_n,\allowbreak \ordom{\varsigma_n}}P_n \}\allowbreak \cup\allowbreak B'$, and for all $t'$ such that $t' \leq t$, $t'$ does not appear in $B'$, i.e., $t'\notin B'$ and $\sstageA{t'}{\_}\_ \notin B'$.
When all barriers are standard, this rule reduces to $\RBar$.
We introduce the function $\channels{B} = \{a \mid \sstageA{t}{a,\allowbreak c, \allowbreak \tup{x}}P\in B\} \cup \{c \mid \sstageA{t}{a,c,\tup{x}}P\in B\}$ to recover the multiset of names used by the domain-barriers in $B$.
%
We also define the function $\fnnobcSymb$, which returns the free names excluding the channels of barriers, by $\fnnobc{\sstageA{t}{a,c,\varsigma}P} = \fn{\range{\varsigma}} \cup \fnnobc{P}$ and, for all other processes, $\fnnobc{P}$ is defined inductively like $\fn{P}$. (The acronym ``nobc'' stands for ``no barrier channels''.)
%
The initial configuration for a closed process $P$ with annotated barriers is
$\Initconf{P} = \barriers{P}, \channels{\barriers{P}}, \{P\}$.
We introduce the following validity condition to ensure that channels of annotated barriers are not mixed with other names: they are fresh names when they are introduced by barrier annotation (\S\ref{sec:barrierAnnotation}); they should remain pairwise distinct and distinct from other names. Their scope is global, but they are private, that is, the adversary does not have access to them.
\begin{definition}[Validity]\label{def:validity}
A process $P$ is \emph{valid} if it is closed,
the elements of $\channels{\barriers{P}}$ are pairwise distinct,
$\channels{\barriers{P}} \cap \fnnobc{P} = \emptyset$, and
for all annotated barriers in $P$ such that $P = \context[\sstageA{t}{a,c,\varsigma}Q]$,
we have $\fv{Q} \subseteq \dom{\varsigma}$ and
$\context$ does not bind $a$, $c$, nor the names in $\fn{Q}$ above the hole.
A configuration $B,E,\Pcal$ is \emph{valid} if
$\barriers{\Pcal} \subseteq B$,
$\channels{B} \subseteq E$,
all processes in $\Pcal$ are valid,
the elements of $\channels{B}$ are pairwise distinct, and
$\channels{B} \cap \fnnobc{\Pcal} = \emptyset$.
\end{definition}
Validity guarantees that channels used in annotated barriers are pairwise
distinct (the elements of $\channels{\barriers{P}}$ are pairwise distinct;
the elements of $\channels{B}$ are pairwise distinct), distinct
from other names ($\channels{\barriers{P}} \cap \fnnobc{P} = \emptyset$;
$\channels{B} \cap \fnnobc{\Pcal} = \emptyset$), and free in the processes
(for all annotated barriers in $P$ such that $P = \context[\sstageA{t}{a,c,\varsigma}Q]$, $\context$ does not bind $a$ nor $c$ above the hole).
These channels must be in $E$
($\channels{B} \subseteq E$), which corresponds to the intuition that
they are global
but private.
Furthermore, for each annotated barrier $\sstageA{t}{a,c,\varsigma}Q$,
we require that $\fv{Q} \subseteq \dom{\varsigma}$ and the names in
$\fn{Q}$ are not bound above the barrier, that is, they are global.
This requirement ensures that the local
state of the process $\sstageA{t}{a,c,\varsigma}Q$ is contained
in the ordered substitution $\varsigma$. The process $Q$ refers to
this state using variables in $\dom{\varsigma}$.
The next lemma allows us to show that all considered configurations
are valid.
\begin{lemma}\label{lem:validity}
If $P$ is a valid process, then $\Initconf{P}$ is valid.
Validity is preserved by reduction, by application
of an adversarial context, and by application of $\fstSymb$ and $\sndSymb$.
\end{lemma}
\noindent
The proof of Lemma~\ref{lem:validity} and all other proofs are detailed in
\ifLONG Appendix~\ref{app-swap-proof}\else the long version of this paper~\cite{LongVersion}\fi.
We refer to processes in which all barriers are annotated as \emph{annotated processes}, and processes in
which all barriers are standard as \emph{standard processes}.
%BB: Moved to appendix (not used in the body of the paper).
%An \emph{annotated configuration} is a configuration in which all processes are annotated.
\subsection{Barrier annotation}\label{sec:barrierAnnotation}
Next, we define the first step of our compiler, which annotates
barriers with additional information.
\begin{definition}
We define function $\precompilerSymb$, from standard processes to annotated processes, as follows:
$\precompilerSymb$ transforms $\context[\sstage{t}Q]$ into $\context[\sstageA{t}{a,c,\varsigma}Q']$, where $\context$ is any context without replication above the hole, $a$ and $c$ are distinct fresh names, and $(Q', \varsigma) = \splitprocemp{Q}$,
where the function $\splitprocSymb$ is defined below.
%
The transformations are performed until all barriers are annotated, in a top-down order, so that in the transformation above, all barriers above $\sstage{t}Q$ are already annotated and barriers inside $Q$ are standard.
The function $\splitprocSymb$ is defined by $\splitprocemp{Q} = (Q', \varsigma)$ where $Q'$ is a process and $\varsigma = (\subst{M_1}{x_1},\dots,\subst{M_n}{x_n})$ is an ordered substitution such that terms $M_1, \ldots, M_n$ are the largest subterms of $Q$ that do not contain names or variables previously bound in $Q$, variables $x_1, \ldots, x_n$ are fresh, and process $Q'$ is obtained from $Q$ by replacing each $M_i$ with $x_i$, so that $Q = Q'\varsigma$. Moreover, the variables $x_1, \dots, x_n$ occur in this order in $Q'$ when read from left to right.
\end{definition}
Intuitively, the function $\splitprocSymb$ separates a process $Q$ into its ``skeleton'' $Q'$ (a process with variables as placeholders for data) and associated data in the ordered substitution $\varsigma$. Such data can be swapped with another process that has the same skeleton.
The ordering of $x_1, \dots, x_n$ chosen in the definition of $\splitprocSymb$ guarantees that the ordering of variables in the domain of $\varsigma$ is consistent among the various subprocesses. This ordering of variables and the fact that $M_1, \ldots, M_n$ are the largest possible subterms allows the checks in the definition of our compiler (see definition of function $\synchSymb$ in \S\ref{sec:compiler}) to succeed more often, and hence increases opportunities for swapping.
\ifLONG
An inductive definition of $\splitprocSymb$ is given in Appendix~\ref{app:splitfinal}.
\fi
\begin{example}\label{example:split}\label{ex:annotate}
We have
\begin{align*}
\splitprocemp{\Out{\diff{\vA}{\vB}}}
&= (\Out[x]{y}, (\subst{c}{x},\subst{\diff{\vA}{\vB}}{y}))\\
\splitprocemp{\Out{\diff{\vB}{\vA}}} &= (\Out[x']{y'},(\subst{c}{x'},\allowbreak\subst{\diff{\vB}{\vA}}{y'}))
\end{align*}
The process $\Out{\diff{\vA}{\vB}}$ is separated into its skeleton
$Q' = \Out[x]{y}$ and the ordered substitution
$\varsigma = (\subst{c}{x},\allowbreak \subst{\diff{\vA}{\vB}}{y})$, which defines the
values of the variables $x$ and $y$ such that
$\Out{\diff{\vA}{\vB}} = Q'\varsigma$.
The process $\Out{\diff{\vB}{\vA}}$ is separated similarly.
Using these results, $\precompiler{\Pex}$ is defined as
\begin{align*}
&\Out{\idA}.\sstageA{1}{a,b,(\subst{c}{x},\subst{\diff{\vA}{\vB}}{y})}\Out[x]{y} \mathrel\mid {}\\
&\Out{\idB}.\sstageA{1}{a',b',(\subst{c}{x'},\allowbreak\subst{\diff{\vB}{\vA}}{y'})}\Out[x']{y'}
\end{align*}
where $a,a',b,b'$ are fresh names.
That is, $\precompiler{\Pex}$ is derived by annotating the two
barriers in $\Pex$.
(Process $\Pex$ is given in Example~\ref{ex:diff-limitations-b}.)
\end{example}
For soundness of the transformation (Proposition~\ref{prop:standard-to-annotated-all}), it is sufficient that:
\begin{lemma}\label{lem:splitfinal}
If $(Q', \varsigma) = \splitprocemp{Q}$, then $Q = Q'\varsigma$, $\fv{Q'} = \dom{\varsigma}$, and $\fn{Q'} = \emptyset$.
\end{lemma}
Intuitively, when reducing the annotated barrier by $\RBarII$, we reduce
$\sstageA{t}{a,c,\varsigma}Q'$ to $Q'\varsigma$, which is equal to $Q$
by Lemma~\ref{lem:splitfinal}, so we recover the process $Q$ we had before
annotation.
The conditions that $\fv{Q'} = \dom{\varsigma}$ and $\fn{Q'} = \emptyset$ show that no names and variables are free in $Q'$ and bound above the barrier, thus substitution $\varsigma$ contains the whole state of the process $Q = Q'\varsigma$.
The following proposition shows that annotation does not alter the semantics of processes:
\begin{proposition}\label{prop:standard-to-annotated-all}
If $P_0$ is a closed standard biprocess and $P'_0 = \precompiler{P_0}$, then
$P'_0$ is valid, $\fst{P'_0} \approx \fst{P_0}$, and
$\snd{P'_0} \approx \snd{P_0}$.
\end{proposition}
\begin{proof}[Proof sketch]
The main step of the proof consists in showing that, when
$\context[\sstage{t}P\varsigma]$ and $\context[\sstageA{t}{a,c,\varsigma}P]$ are valid processes, we have
\begin{equation}
\context[\sstage{t}P\varsigma] \approx \context[\sstageA{t}{a,c,\varsigma}P]
\label{eq:equiv-prop:standard-to-annotated-all}
\end{equation}
This proof is performed by defining a relation $\Rel$ that satisfies the conditions of Definition~\ref{def:proverif:obs}.
By Lemma~\ref{lem:splitfinal}, from the annotated biprocess $P'_0$, we can rebuild the initial process $P_0$ by replacing each occurrence of an annotated barrier $\sstageA{t}{a,c,\varsigma}Q$ with $Q\varsigma$, so the same replacement also transform $\fst{P'_0}$ into $\fst{P_0}$ and $\snd{P'_0}$ into $\snd{P_0}$. By~\eqref{eq:equiv-prop:standard-to-annotated-all}, this replacement preserves the observational behaviour of the processes.
\end{proof}
\subsection{Barrier elimination and swapping}\label{sec:compiler}
Next, we define the second step of our compiler, which translates an
annotated biprocess into biprocesses without barriers. Each annotated
barrier $t[a,c,\varsigma]$ is eliminated by replacing it with an
output on channel $a$ of swappable data, followed by an input on
channel $c$ that receives swapped data. A swapping process is added
in parallel, which receives the swappable data on channels $a$ for
all barriers $t$, before sending swapped data on channels $c$.
Therefore, all inputs on channels $a$ must be received before
the outputs on channels $c$ are sent and the processes that
follow the barriers can proceed, thus the synchronisation between
the barriers is guaranteed. Moreover, the swapping process may permute data,
sending on channel $c$ data that comes from channel $a'$ with $a' \neq a$,
thus implementing swapping. This swapping is allowed only when the
processes that follow the barriers are identical (up to renaming of
some channel names and variables), so that swapping preserves the observational
behaviour of the processes. We detail this construction below.
%% \bb{I am hesitating between $a_i$, $c_i$ and just $a$, $c$.
%% If you think $a$, $c$ is understandable, let's leave as it is.
%% It is lighter.\\
%% BS: I replaced $a_i$ and $c_i$ with $a$ and $c$ since the
%% use of subscript $i$ suggests that the integer $i$ is somehow
%% important. Since we only require that channel names are distinct,
%% I think the lighter version is easier to read. That said, I don't
%% mind reverting.}
\iffalse
\begin{definition}%\label{def:proswapper}
We define
\[\begin{split}
&\stageElimSecondFunc{P} = {}\\
&\quad \left\{\begin{array}{@{}l@{}}
\new{\tilde{a}}.(\compiler{P} \mid R) \text{ where } B = \barriers{P}, \\
\{\tilde{a}\} = \channels{B}, \textrm{ and } R \in \synch{B}
\end{array}\right\}
\end{split}\]
where functions $\compilerISymb$ and $\synchSymb$ are defined below.
\end{definition}
\fi
\subsubsection{Barrier elimination}
First, we eliminate barriers.
\begin{definition}
The function $\compilerISymb$ removes annotated barriers, by transforming
each annotated barrier
$\sstageA{t}{a,\allowbreak c,\allowbreak (\subst{M_1}{z_1},\allowbreak \dots,\allowbreak \subst{M_n}{z_n})}Q$ into
$\Out[a]{\tuple{M_1,\dots,M_n}}.\allowbreak \In[c]{z}.\allowbreak \Letin{z_1}{\projnew 1 n z} \allowbreak \cdots\ \Letin{z_n}{\projnew n n z} Q$,
where $z$ is a fresh variable.
\end{definition}
%% \bbnote{In the implementation, there is no explicit $\new{\tilde{a}}$. The
%% elements of $\tilde{a}$ are private free names.
%% Moreover, the function $\compilerISymb$ uses pattern-matching inside
%% inputs, so that
%% $\compilerI{\sstageA{t}{a,c,\varsigma}Q} = \Out[a]{\tuple{M_1,\dots,M_n}}.\In[c]{\tuple{z_1,\dots,z_n}}. \compilerI{Q}$
%% where $\varsigma = (\subst{M_1}{z_1}, \dots, \subst{M_n}{z_n})$.
%% We can omit these details in the paper, I think.}%
The definition of function $\compilerISymb$ ensures that,
if the message $\tuple{M_1,\dots,M_n}$ on the private
channel $a$ is simply forwarded to
the private channel $c$, then the process derived by application of $\compilerISymb$ binds $z_i$ to $M_i$ for each $i\in\{1,\dots,n\}$, like the annotated barrier, so the original process and the process derived by application $\compilerISymb$
are observationally equivalent.
Intuitively, the private channel communication provides an
opportunity to swap data.
\begin{example}\label{ex:barElim}
Using the results of Example~\ref{ex:annotate},
eliminating barriers from $\precompiler{\Pex}$ results in
$
\compilerI{\precompiler{\Pex}} = \Pcomp \mid \Pcomp'
$,
where
\begin{align*}
\Pcomp \triangleq {} &\Out{\idA}.\Out[a]{\tuple{c,\diff{\vA}{\vB}}}.\In[b]{z}.\\
&\Letin{x}{\projnew 1 2 z} \Letin{y}{\projnew 2 2 z} \Out[x]{y}\\
\Pcomp' \triangleq {} &\Out{\idB}.\Out[a']{\tuple{c,\diff{\vB}{\vA}}}.\In[b']{z'}.\\
&\Letin{x'}{\projnew 1 2 {z'}} \Letin{y'}{\projnew 2 2 {z'}}\Out[x']{y'}
\end{align*}
for some fresh variables $z$ and $z'$.
\end{example}
\subsubsection{Swapping}
Next, we define swapping strategies.
\begin{definition}\label{def:synch}
The function $\synchSymb$ is defined as follows:
%
\[
\begin{array}{@{}l@{}l@{}}
\multicolumn{2}{@{}l@{}}{ \synch{\emptyset} = \{ 0 \}}\\
\multicolumn{2}{@{}l@{}}{ \synch{B} ={}}\\
\hspace*{0.4cm} &\ \big\{\In[a_1]{x_1}\mathrel. \cdots \mathrel. \In[a_n]{x_n}.\\
&\phantom{\ \big\{}\Out[c_1]{\diff{x_1}{x_{f(1)}}}\mathrel. \cdots \mathrel. \Out[c_n]{\diff{x_n}{x_{f(n)}}}.R\\
&\ \big|\hspace*{0.05em} \textrm{$B = \{\sstageA{t}{a_1,c_1,\tup{z}_1} Q_1,\dots,\sstageA{t}{a_n,c_n,\tup{z}_n} Q_n\} \cup B'$}\\
&\quad\!\textrm{where, for all $\sstageA{t'}{a,c,\tup{z}}Q\in B'$, we have $t'>t$;}\\
& \quad\!\textrm{$f$ is a permutation of $\{1,\dots,n\}$ such that,}\\
& \quad\!\textrm{for all $1 \leq l \leq n$, we have $Q_l/\tup{z}_l \eqren Q_{f(l)}/\tup{z}_{f(l)}$;}\\
& \quad\!\textrm{$R \in \synch{B'}$;}\\
&\quad\!\textrm{and $x_1, \dots, x_n$ are fresh variables}\big\}\\
& \text{if $B \neq \emptyset$}
\end{array}
\]
where $\eqren$ is defined as follows:
\begin{itemize}
\item $Q \eqren Q'$ means that $Q$ equals $Q'$ modulo renaming of channels of annotated barriers and
\item $Q/\tup{z} \eqren Q'/\tup{z}'$
means that $\tup{z} = (z_1, \dots, z_k)$ and $\tup{z}' = (z'_1, \dots, z'_k)$
for some integer $k$, and
$Q\{\subst{y_1}{z_1},\dots,\subst{y_k}{z_k}\} \eqren Q'\{\subst{y_1}{z'_1},\dots,\subst{y_k}{z'_k}\}$
for some fresh variables $y_1, \dots, y_k$.
\end{itemize}
\end{definition}
The function $\synchSymb$
builds a set of processes from a multiset of domain-barriers $B$ as follows.
We identify integer $t\in\mathbb N$ and domain-barriers
$\sstageA{t}{a_1,c_1,\tup{z}_1}Q_1,\allowbreak\dots,\allowbreak
\sstageA{t}{a_n,c_n,\tup{z}_n}Q_n$ in $B$ such that
no other barriers with $t'\leq t$ appear in $B$,
so that these barriers are reduced before other barriers in $B$.
%
Among these barriers, we consider barriers $\sstageA{t}{a_i,c_i,\tup{z}_i}Q_i$
and $\sstageA{t}{a_j,c_j,\tup{z}_j}Q_j$ such that
$Q_i/\tup{z}_i \eqren Q_j/\tup{z}_j$, that is,
the processes $Q_i$ and $Q_j$
are equal modulo renaming of channels of annotated barriers,
after renaming the variables in $\tup{z}_i$ and $\tup{z}_j$
to the same variables, and we allow swapping data between such
barriers using the permutation $f$.
We then construct a set of processes which enable swapping,
by receiving data to be swapped on channels $a_1$, \dots, $a_n$,
and sending it back on channels $c_1$, \dots, $c_n$,
in the same order in the first component of $\diffSymb$ and
permuted by $f$ in the second component of $\diffSymb$.
The function $\synchSymb$ does not specify an ordering on the pairs of channels $(a_1,c_1),\allowbreak\dots,\allowbreak(a_n,c_n)$, since any ordering is correct.
\begin{example}\label{ex:swap}
We have
$\barriers{\precompiler{\Pex}} =
\{ \sstageA{1}{a,b,(x,y)}\Out[x]{y},
\sstageA{1}{a',b',(x',y')}\Out[x']{y'} \}$.
Moreover, we trivially have
$\Out[x]{y}/(x,y) \allowbreak\eqren\allowbreak \Out[x]{y}/(x,y)$ and
$\Out[x']{y'}/(x',y') \allowbreak\eqren\allowbreak \Out[x']{y'}/(x',y')$,
because $Q/\tilde z \eqren Q/\tilde z$ for all $Q$ and
$\tilde z$. We also have
$\Out[x]{y}/(x,y) \eqren\allowbreak \Out[x']{y'}/(x',y')$,
because
\[\Out[x]{y}\{\subst{x''}{x},\subst{y''}{y}\} =
\Out[x'']{y''} = \Out[x']{y'}\{\subst{x''}{x'},\subst{y''}{y'}\}\]
It follows that $\synch{\barriers{\precompiler{\Pex}}} = \{ \Psame, \allowbreak \Pswap \}$,
where
\begin{align*}
&\Psame \triangleq \In[a]{z}. \In[a']{z'}.\Out[b]{\diff{z}{z}}. \Out[b']{\diff{z'}{z'}}\\
&\Pswap \triangleq \In[a]{z}. \In[a']{z'}.\Out[b]{\diff{z}{z'}}. \Out[b']{\diff{z'}{z}}
\end{align*}
for some fresh variables $z$ and $z'$. (Note that $\diff{z}{z}$ could be
simplified into $z$.) This set considers the two
possible swapping strategies: the strategy that does not
swap any data and the strategy that swaps data between the two processes
at the barrier.
\end{example}
\subsubsection{Combining barrier elimination and swapping}
Finally, we derive a set of processes by parallel
composition of the process output by $\compilerSymb$ and the processes
output by $\synchSymb$, under the scope of name restrictions on the
fresh channels introduced by $\precompilerSymb$.
%
\[\begin{split}
&\stageElimSecondFunc{P} = {}\\
&\quad \left\{\begin{array}{@{}l@{}}
\new{\tilde{a}}.(\compiler{P} \mid R) \text{ where } B = \barriers{P}, \\
\{\tilde{a}\} = \channels{B}, \textrm{ and } R \in \synch{B}
\end{array}\right\}
\end{split}\]
%Intuitively, function $\stageElimSecondSymb$ preserves the behaviour of barrier synchronisation: processes which synchronise at a particular barrier all output messages on private channels and then await input on private channels; once all such messages have been sent, each process receives a response (by definition of $\synchSymb$)
%\bb{Fixed reference to removed figure.}%(cf. lines 3--4 of Figure~\ref{fig:proswapperCompilation})
%and, hence, may proceed. For example, given a process $P$ such that $\precompiler{P} =
%\sstageA{t}{a_1,c_1,\varsigma_1}P_1 \mid \dots \mid\sstageA{t}{a_n,c_n,\varsigma_n}P_n$, we are assured that there will be $n$ outputs on channels $a_1,\dots,a_n$ before any responses are sent on channels $c_1,\dots,c_n$; it follows that, prior to the responses being sent, the processes $P_1,\dots,P_n$ are awaiting input on a private channel and hence block.
%
%Moreover, swapping preserves the observational behaviour of processes, because data is only moved between
%processes that share the same skeleton.
Intuitively, function $\stageElimSecondSymb$ encodes barrier synchronisation
and swapping using private channel communication, thereby preserving the
observational behaviour of processes.
\begin{example}\label{ex:compiler}
Using the results of Examples~\ref{ex:barElim} \&~\ref{ex:swap},
applying $\stageElimSecondSymb$ to the process $\precompiler{\Pex}$ generates two processes
\begin{align*}
P_1 \triangleq \new{a,a',b,b'}.(\Pcomp \mid \Pcomp' \mid \Psame)\\
P_2 \triangleq \new{a,a',b,b'}.(\Pcomp \mid \Pcomp' \mid \Pswap)
\end{align*}
In the process $P_1$, no data is swapped, so it behaves exactly like $\Pex$:
$\tuple{c,\diff{\vA}{\vB}}$ is sent on $a$, sent back on $b$ by $\Psame$
as
$\diff{\tuple{c,\diff{\vA}{\vB}}}{\tuple{c,\diff{\vA}{\vB}}}$ which simplifies
into $\tuple{c,\diff{\vA}{\vB}}$,
and after evaluating the projections, $\Pcomp$ reduces
into $\Out{\diff{\vA}{\vB}}$, which is the output present in the
process $\Pex$.
Similarly, $\Pcomp'$ reduces into $\Out{\diff{\vB}{\vA}}$, present in $\Pex$.
By contrast, in process $P_2$, data is swapped:
$\tuple{c,\diff{\vA}{\vB}}$ is sent on $a$ and
$\tuple{c,\diff{\vB}{\vA}}$ is sent on $a'$, and
$\Pswap$ sends back $\diff{\tuple{c,\diff{\vA}{\vB}}}{\allowbreak \tuple{c,\diff{\vB}{\vA}}}$
on $b$. The first component of this term is $\tuple{c,\vA}$ (obtained by taking
the first component of each $\diffSymb$), and similarly its second component
is also $\tuple{c,\vA}$, so this term simplifies into $\tuple{c,\vA}$.
After evaluating the projections, $\Pcomp$ reduces
into $\Out{\vA}$.
Similarly, $\Pcomp'$ reduces into $\Out{\vB}$.
Hence $P_2$ behaves like $\Out{\idA}.\sstage{1}\Out{\vA}\mid\Out{\idB}.\sstage{1}\Out{\vB}$.
In particular, $P_2$ outputs $\idA$ and $\idB$ before barrier synchronisation and $\vA$ and $\vB$ after synchronisation
just like $\Pex$. But $P_2$ satisfies diff-equivalence while $\Pex$ does not.
\end{example}
The next proposition formalises this preservation of observable behaviour.
\begin{proposition}\label{prop:preserve-compil-second}
Let $P$ be a valid, annotated biprocess.
If $P' \in \stageElimSecondFunc{P}$, then $\fst{P} \approx \fst{P'}$
and $\snd{P} \approx \snd{P'}$.
\end{proposition}
\begin{proof}[Proof sketch]
This proof is performed by defining a relation $\Rel$ that satisfies the conditions of Definition~\ref{def:proverif:obs}. The proof is fairly long and delicate, and relies on preliminary lemmas that show that barrier elimination commutes with renaming and substitution, and that it preserves reduction when barriers are not reduced.
\end{proof}
\subsection{Our compiler}\label{sec:completeCompiler}
We combine the annotation (\S\ref{sec:barrierAnnotation}) and
removal of barrier (\S\ref{sec:compiler}) steps to define our compiler as
$$\stageElimFunc{P} = \stageElimSecondFunc{\precompiler{P}}$$
We have implemented the compiler in ProVerif, which is available from: \url{http://proverif.inria.fr/}.
% By default, it considers all possible swapping strategies until it finds
% one for which ProVerif succeeds in proving observational equivalence.
% This is what we do in our case studies.
% However, it is also possible for the user to specify the desired
% swapping strategy, in the input file or interactively.
% BB: Should we mention [noswap], removal
% of some synchronizations? (It helps reducing the number of possible
% swapping strategies.)
By combining Propositions~\ref{prop:standard-to-annotated-all}
and~\ref{prop:preserve-compil-second},
we immediately obtain:
\begin{proposition}\label{prop:preserve-compil}
Let $P$ be a closed standard biprocess.
If $P' \in \stageElimFunc{P}$, then $\fst{P} \approx \fst{P'}$
and $\snd{P} \approx \snd{P'}$.
\end{proposition}
\noindent This proposition shows that compilation
preserves the observational behaviour of processes.
The following theorem is an immediate consequence of this proposition:
\begin{theorem}\label{thm:soundnessSwapping}
Let $P$ be a closed biprocess. If a biprocess in
$\stageElimFunc{P}$ satisfies observational
equivalence, then $P$ satisfies observational equivalence.
\end{theorem}
\noindent This theorem allows us to prove observational equivalence
using swapping: we prove that a biprocess in $\stageElimFunc{P}$
satisfies observational equivalence using ProVerif (by
Theorem~\ref{theorem:Bruno}), and conclude that $P$ satisfies
observational equivalence as well.
%
For instance, ProVerif can show
that the process $P_2 \in \stageElimFunc{\Pex}$ of Example~\ref{ex:compiler} satisfies observational equivalence, thus $\Pex$ satisfies observational equivalence too.
Our compiler could be implemented in other tools that prove diff-equivalence
(e.g., Maude-NPA~\cite{Santiago14} and Tamarin~\cite{Basin15}),
by adapting the input language.
It could also be applied to other methods of proving equivalence.
However, it may be less useful in these cases, since it might not
permit the proof of more equivalences in such cases.
\subsection{Extensions}
\subsubsection{Replicated barriers}\label{sec:syncelim}
While our calculus does not allow barriers under replication,
we can still prove equivalence with barriers under bounded replication,
for any bound. We define bounded replication by
$!^n P \triangleq P \mid \dots \mid P$ with $n$ copies of the process $P$.
We have the following results:
\begin{proposition}\label{prop:bounded-repl}
Let $\context[!Q]$ be a closed standard biprocess,
such that the context $\context$ does not contain any barrier above the hole.
If a biprocess in $\stageElimFunc{\context[!Q]}$ satisfies diff-equivalence,
then for all $n$, a biprocess in $\stageElimFunc{\context[!^n Q]}$ satisfies diff-equivalence.
\end{proposition}
Proposition~\ref{prop:bounded-repl} shows that, if our approach proves
equivalence with unbounded replication, then it also proves equivalence
with bounded replication.
\begin{proposition}\label{prop:syncelim}
Let $\context[Q]$ be a closed standard biprocess,
such that the context $\context$ does not contain any replication
above the hole.
If a biprocess in $\stageElimFunc{\context[Q]}$ satisfies diff-equivalence,
then a biprocess in $\stageElimFunc{\context[\sstage{t}Q]}$ satisfies diff-equivalence.
\end{proposition}
Proposition~\ref{prop:syncelim} shows that, if our approach proves equivalence
after removing a barrier, then it also proves equivalence with the barrier.
By combining these two results, we obtain:
\begin{corollary}\label{cor:boundrepl}
Let $Q_{\textnormal{nobar}}$ be obtained from $Q$ by removing
all barriers. Let $\context$ be a context that
does not contain any replication or barrier above the hole.
If a biprocess in $\stageElimFunc{\context[!Q_{\textnormal{nobar}}]}$ satisfies diff-equivalence,
then for all $n$, process $\context[!^n Q]$ satisfies observational equivalence.
\end{corollary}
% \noindent
% It may be possible to generalise this proposition to any context
% $\context$. The case in which $\context$ does not contain any barrier
% above the hole is simpler and sufficient for our purpose.
%Hence, we can prove observational equivalence for the biprocess
%$P'(n)$ with bounded replication, for any bound $n$, by applying our
%approach to the biprocess $P$.
Hence, we can apply our compiler to prove observational equivalence
for biprocesses with bounded replication, for any value of the bound.
In the case of election schemes,
this result allows us to prove privacy for an unbounded
number of voters, for instance in the protocol by Lee \emph{et al.}
(\S\ref{sec:lee}).
%% \bbnote{In fact, for our trivial example and for FOO, we do not need this
%% result for proving ballot secrecy for an unbounded number of voters,
%% because we can consider that all voters except the two that swap their
%% votes are included in the adversary.}
\subsubsection{Local synchronisation}
Our results could be extended to systems in which several groups
of participants synchronise locally inside each group, but do not
synchronise with other groups. In this case, we would need several swapping
processes similar to those generated by $\synchSymb$, one for each group.
\subsubsection{Trace properties}
ProVerif also supports the proof of trace properties (reachability and correspondence properties of the form ``if some event has been executed, then some other events must have been executed'', which serve for formalising authentication)~\cite{BlanchetJCS09}.
Our implementation extends this support to processes with barriers, by compiling them to processes without barriers, and applying ProVerif to the compiled processes. In this case, swapping does not help, so our compiler does not swap.
%Cut to shorten
\iffalse
so $\precompilerSymb$ annotates barriers just by replacing $\sstage{t}P$ with $\sstageA{t}{a,c,()}P$ where $a$ and $c$ are fresh channels, and
\[
\begin{array}{@{}l@{}l@{}}
% \synch{\emptyset} &{}= \{ 0 \}\\
\multicolumn{2}{@{}l@{}}{\synch{B} ={}}\\
\hspace*{0.3cm} &\ \big\{\ \In[a_1]{x_1}\mathrel. \cdots \mathrel. \In[a_n]{x_n}\mathrel.\Out[c_1]{()}\mathrel. \cdots \mathrel. \Out[c_n]{()}.R\\
&\ \big|\ \textrm{$B = \{\sstageA{t}{a_1,c_1,()} Q_1,\dots,\sstageA{t}{a_n,c_n,()} Q_n\} \cup B'$}\\
&\quad\textrm{where, for all $\sstageA{t'}{a,c,()}Q\in B'$, we have $t'>t$;}\\
& \quad\textrm{$R \in \synch{B'}$; and $x_1, \dots, x_n$ are fresh variables}\big\}\\
& \text{if $B \neq \emptyset$}
\end{array}
\]
The synchronisation is enforced because all inputs on $a_1, \dots a_n$
must be performed before the outputs on $c_1, \dots c_n$ are
performed, and the processes after the barriers can proceed.
\fi
We do not detail the proof of trace properties with barriers
further, since it is easier and less important than observational
equivalence.
```
# Privacy in elections
Elections enable voters to choose representatives. Choices should be made freely, and this has led to the emergence of ballot secrecy as a *de facto* standard privacy requirement of elections. Stronger formulations of privacy, such as receipt-freeness, are also possible.
- Ballot secrecy: a voter’s vote is not revealed to anyone.
- Receipt-freeness: a voter cannot prove how she voted.
We demonstrate the suitability of our approach for analysing privacy requirements of election schemes by Fujioka, Okamoto & Ohta, commonly referred to as FOO, and Lee *et al.*, along with some of its variants. Our ProVerif scripts are included in ProVerif’s documentation package (). The runtime of these scripts (including compilation of barriers and proof of diff-equivalence by ProVerif) ranges from 0.14 seconds for FOO to 90 seconds for the most complex variant of the Lee *et al*. protocol, on an Intel Xeon 3.6 GHz under Linux.
## Case study: FOO
### Cryptographic primitives
FOO uses commitments and blind signatures. We model commitment with a binary constructor $\mathsf{commit}$, and the corresponding destructor $\mathsf{open}$ for opening the commitment, with the following rewrite rule: $$\begin{array}{@{}r@{}c@{}l@{}}
\mathsf{open}(x_{\mathsf{k}},\mathsf{commit}(x_{\mathsf{k}},x_{\mathsf{plain }})) &{}\rightarrow{}& x_{\mathsf{plain }}
\end{array}$$ Using constructors $\mathsf{sign}$, $\mathsf{blind}$, and $\mathsf{pk}$, we model blind signatures as follows: $\mathsf{sign}(x_{\mathsf{sk }}, x_{\mathsf{msg }})$ is the signature of message $x_{\mathsf{msg }}$ under secret key $x_{\mathsf{sk }}$, $\mathsf{blind}(x_{\mathsf{k}}, x_{\mathsf{msg }})$ is the blinding of message $x_{\mathsf{msg }}$ with coins $x_{\mathsf{k}}$, and $\mathsf{pk}(x_{\mathsf{sk }})$ is the public key corresponding to the secret key $x_{\mathsf{sk }}$. We also use three destructors: $\mathsf{checksign}$ to verify signatures, $\mathsf{getmsg}$ to model that an adversary may recover the message from the signature, even without the public key, and $\mathsf{unblind}$ for unblinding, defined by the following rewrite rules: $$\begin{array}{@{}r@{}c@{}l@{}}
\mathsf{checksign}(\mathsf{pk}(x_{\mathsf{sk }}),\mathsf{sign}(x_{\mathsf{sk }},x_{\mathsf{msg }})) &{}\rightarrow{}& x_{\mathsf{msg }}\\
\mathsf{getmsg}(\mathsf{sign}(x_{\mathsf{sk }},x_{\mathsf{msg }})) &\rightarrow& x_{\mathsf{msg }}\\
\mathsf{unblind}(x_{\mathsf{k}},\mathsf{sign}(x_{\mathsf{sk }},\mathsf{blind}(x_{\mathsf{k}},x_{\mathsf{msg }}))) &\rightarrow& \mathsf{sign}(x_{\mathsf{sk }},x_{\mathsf{msg }}) \\
\mathsf{unblind}(x_{\mathsf{k}},\mathsf{blind}(x_{\mathsf{k}},x_{\mathsf{plain }})) &\rightarrow& x_{\mathsf{plain }}
\end{array}$$ With blind signatures, a signer may sign a blinded message without learning the plaintext message, and the signature on the plaintext message can be recovered by unblinding, as shown by the third rewrite rule.
### Protocol description
The protocol uses two authorities, a *registrar* and a *tallier*, and it is divided into four phases, *setup*, *preparation*, *commitment*, and *tallying*. The setup phase proceeds as follows.
1. The registrar creates a signing key pair $sk_R$ and $\mathsf{pk}(sk_R)$, and publishes the public part $\mathsf{pk}(sk_R)$. In addition, each voter is assumed to have a signing key pair $sk_V$ and $\mathsf{pk}(sk_V)$, where the public part $\mathsf{pk}(sk_V)$ has been published.
The preparation phase then proceeds as follows.
2. The voter chooses coins $k$ and $k'$, computes the commitment to her vote $M = \mathsf{commit}(k,v)$ and the signed blinded commitment $\mathsf{sign}(sk_V,\mathsf{blind}(k',M))$, and sends the signature, paired with her public key, to the registrar.
3. The registrar checks that the signature belongs to an eligible voter and returns the blinded commitment signed by the registrar $\mathsf{sign}(sk_R,\mathsf{blind}(k',M))$.
4. The voter verifies the registrar’s signature and unblinds the message to recover $\hat M = \mathsf{sign}(sk_R,M)$, that is, her commitment signed by the registrar.
After a deadline, the protocol enters the commitment phase.
5. The voter posts her ballot $\hat M$ to the bulletin board.
Similarly, the tallying phase begins after a deadline.
6. The tallier checks validity of all signatures on the bulletin board and prepends an identifier $\ell$ to each valid entry.
7. The voter checks the bulletin board for her entry, the pair $\ell, \hat M$, and appends the commitment factor $k$.
8. Finally, using $k$, the tallier opens all of the ballots and announces the election outcome.
The distinction between phases is essential to uphold the protocol’s security properties. In particular, voters must synchronise before the commitment phase to ensure ballot secrecy (observe that without synchronisation, traffic analysis may allow the voter’s signature to be linked with the commitment to her vote – this is trivially possible when a voter completes the commitment phase before any other voter starts the preparation phase, for instance – which can then be linked to her vote) and before the tallying phase to avoid publishing partial results, that is, to ensure *fairness* (see Cortier & Smyth (**Smyth12:Helios?**) for further discussion on fairness).
### Model
To analyse ballot secrecy, it suffices to model the participants that must be honest (i.e., must follow the protocol description) for ballot secrecy to be satisfied. All the remaining participants are controlled by the adversary. The FOO protocol assures ballot secrecy in the presence of dishonest authorities if the voter is honest. Hence, it suffices to model the voter’s part of FOO as a process.
**Definition 1**. *The process $P_{\sf foo}(x_{\mathsf{sk }}, x_{\mathsf{vote} })$ modelling a voter in FOO, with signing key $x_{\mathsf{sk }}$ and vote $x_{\mathsf{vote} }$, is defined as follows $$\begin{array}{@{}l@{}l}
\nu\,k.\nu\,k'. &\textrm{\% Step 2}\\%&\textrm{\%Coins}\\
\textnormal{let } M=\mathsf{commit}(k,x_{\mathsf{vote} }) \textnormal{ in } \\%&\textrm{\%Commitment}\\
\textnormal{let } {M'}=\mathsf{blind}(k',M) \textnormal{ in } \\%&\textrm{\%Blind commitment}\\
\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(x_{\mathsf{sk }}),\mathsf{sign}(x_{\mathsf{sk }},{M'})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle. \\%&\textrm{\%Output for registrar}\\
%
c(y). &\textrm{\% Step 4}\\%&\textrm{\%Input (registrar's) response}\\
\textnormal{let } y'=\mathsf{checksign}(\mathsf{pk}(sk_R),y) \textnormal{ in } \\%&\textrm{\%Registrar's signature?}\\
\textnormal{if } y'=M' \textnormal{ then } \\%&\textrm{\%Signature on ${M'}$?}\\
\textnormal{let } \hat M=\mathsf{unblind}(k',y) \textnormal{ in } \\%&\textrm{\%Signed commitment}\\
1\textnormal{::}\, \overline{c}\langle\hat M\rangle . &\textrm{\% Step 5}\\%&\textrm{\%Output for board}\\
%
2\textnormal{::}\, c(z) .\textnormal{let } z_2=\pi_{2,2}(z) \textnormal{ in } &\textrm{\% Step 7}\\%&\textrm{\%Input (board's) response}\\
%&\textrm{\%Ballot}\\
\textnormal{if } z_2=\hat M \textnormal{ then } %&\textrm{\%Voter's ballot?}\\
\overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{z,k}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle \\%&\textrm{\%Output for board}
\end{array}$$*
The process $P_{\sf foo}(sk_1, v_1) \mid\dots\mid P_{\sf foo}(sk_n, v_n)$ models an election with $n$ voters casting votes $v_1,\dots,v_n$ and encodes the separation of phases using barriers.
### Analysis: ballot secrecy
Based upon (**KR05:vote-privacy?**; **DKR08?**) and as outlined in Section [sec:intro], we formalise ballot secrecy for two voters $A$ and $B$ with the assertion that an adversary cannot distinguish between a situation in which voter $A$ votes for candidate $v$ and voter $B$ votes for candidate $v'$, from another one in which $A$ votes $v'$ and $B$ votes $v$. We use the biprocess $P_{\sf foo}(sk_A, \mathsf{diff}[v,v'])$ to model $A$ and the biprocess $P_{\sf foo}(sk_B, \mathsf{diff}[v',v])$ to model $B$, and formally express ballot secrecy as an equivalence which can be checked using Theorem [thm:soundnessSwapping]. Voters’ keys are modelled as free names, since ballot secrecy can be achieved without confidentiality of these keys. (Voters’ keys *must* be secret for other properties.)
To provide further insight into how our compiler works, let us consider how to informally prove this equivalence: that $\mathsf{fst}(Q_{\sf foo})$ is indistinguishable from $\mathsf{snd}(Q_{\sf foo})$. Before the first barrier, $A$ outputs $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_A),\;\mathsf{sign}(sk_A,\mathsf{blind}(k'_a,\mathsf{commit}(k_a,v)))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ in $\mathsf{fst}(Q_{\sf foo})$ and $$\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{pk}(sk_A),\;\mathsf{sign}(sk_A,\mathsf{blind}(k'_a,\mathsf{commit}(k_a,v')))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ in $\mathsf{snd}(Q_{\sf foo})$, where the name $k'_a$ remains secret. By the equational theory for blinding, $N$ can only be recovered from $\mathsf{blind}(M,N)$ if $M$ is known, so these two messages are indistinguishable. The situation is similar for $B$. Therefore, before the first barrier, $A$ moves in $\mathsf{fst}(Q_{\sf foo})$ are mimicked by $A$ moves in $\mathsf{snd}(Q_{\sf foo})$ and $B$ moves in $\mathsf{fst}(Q_{\sf foo})$ are mimicked by $B$ moves in $\mathsf{snd}(Q_{\sf foo})$.
Let us define $\mathsf{sc}({k},{v}) \triangleq \mathsf{sign}(sk_R,\mathsf{commit}(k,v))$. After the first barrier, $A$ outputs $$\begin{aligned}
&\mathsf{sc}({k_a},{v}) \textrm{ and } \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell_1,\;\mathsf{sc}({k_a},{v})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\;k_a}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}
\text{ in $\mathsf{fst}(Q_{\sf foo})$}\\
&\mathsf{sc}({k_a},{v'}) \textrm{ and } \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell_1,\;\mathsf{sc}({k_a},{v'})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$},\;k_a}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}
\text{ in $\mathsf{snd}(Q_{\sf foo})$}
\end{aligned}$$ where $\ell_1$ is chosen by the adversary. It follows that $A$ reveals her vote $v$ in $\mathsf{fst}(Q_{\sf foo})$ and her vote $v'$ in $\mathsf{snd}(Q_{\sf foo})$, so these messages are distinguishable. However, $B$ outputs $$\begin{aligned}
&\mathsf{sc}({k_b},{v'}) \textrm{ and } \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell_2,\;\mathsf{sc}({k_b},{v'})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\;k_b}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \text{ in $\mathsf{fst}(Q_{\sf foo})$}\\
&\mathsf{sc}({k_b},{v}) \textrm{ and } \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\ell_2,\;\mathsf{sc}({k_b},{v})}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\;k_b}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$} \text{ in $\mathsf{snd}(Q_{\sf foo})$}
\end{aligned}$$ where $\ell_2$ is similarly chosen by the adversary. Hence, $B$’s messages in $\mathsf{snd}(Q_{\sf foo})$ are indistinguishable from $A$’s messages in $\mathsf{fst}(Q_{\sf foo})$. Therefore, after the first barrier, $A$ moves in $\mathsf{fst}(Q_{\sf foo})$ are mimicked by $B$ moves in $\mathsf{snd}(Q_{\sf foo})$ and symmetrically, $B$ moves in $\mathsf{fst}(Q_{\sf foo})$ are mimicked by $A$ moves in $\mathsf{snd}(Q_{\sf foo})$, that is, the roles are swapped at the first barrier. Our compiler encodes the swapping, hence we can show that FOO satisfies ballot secrecy using Theorem [thm:soundnessSwapping]. Moreover, ProVerif proves this result automatically. This proof is done for two honest voters, but it generalises immediately to any number of possibly dishonest voters, since other voters can be part of the adversary.
Showing that FOO satisfies ballot secrecy is not new: Delaune, Kremer & Ryan (**KR05:vote-privacy?**; **DKR08?**) present a manual proof of ballot secrecy, Chothia *et al.* (**Chothia06:FOO?**) provide an automated analysis in the presence of a passive adversary, and Delaune, Ryan & Smyth (**Smyth08:Obs?**), Klus, Smyth & Ryan (**Smyth10:ObsA?**), and Chadha, Ciobâcă & Kremer (**Kremer12:AKISS?**; **Stefan11:thesis?**) provide automated analysis in the presence of an active adversary. Nevertheless, our analysis is useful to demonstrate our approach.
FOO does not satisfy receipt-freeness, because each voter knows the coins used to construct their ballot and these coins can be used as a witness to demonstrate how they voted. In an effort to achieve receipt-freeness, the protocol by Lee *et al.* (**Lee04?**) uses a hardware device to introduce coins into the ballot that the voter does not know.
## Case study: Lee *et al.*
### Protocol description
The protocol uses a registrar and some talliers, and it is divided into three phases, *setup*, *voting*, and *tallying*. For simplicity, we assume there is a single tallier. The setup phase proceeds as follows.
1. The tallier generates a key pair and publishes the public key.
2. Each voter is assumed to have a signing key pair and an offline tamper-resistant hardware device. The registrar is assumed to know the public keys of voters and devices. The registrar publishes those public keys.
The voting phase proceeds as follows.
3. The voter encrypts her vote and inputs the resulting ciphertext into her tamper-resistant hardware device.
4. The hardware device re-encrypts the voter’s ciphertext, signs the re-encryption, computes a Designated Verifier Proof that the re-encryption was performed correctly, and outputs these values to the voter.
5. If the signature and proof are valid, then the voter outputs the re-encryption and signature, along with her signature of these elements.
The hardware device re-encrypts the voter’s encrypted choice to ensure that the voter’s coins cannot be used as a witness demonstrating how the voter voted. Moreover, the device is offline, thus communication between the voter and the device is assumed to be untappable, hence, the only meaningful relation between the ciphertexts input and output by the hardware device is due to the Designated Verifier Proof, which can only be verified by the voter.
Finally, the tallying phase proceeds as follows.
6. Valid ballots (that is, ciphertexts associated with valid signatures) are input to a mixnet and the mixnet’s output is published. We model the mixnet as a collection of parallel processes that each input a ballot, verify the signatures, synchronise with the other processes, and finally output the ciphertext on an anonymous channel.
7. The tallier decrypts each ciphertext and announces the election outcome.
### Analysis: ballot secrecy
In this protocol, the authorities and hardware devices must be honest for ballot secrecy to be satisfied, so we need to explicitly model them. Therefore, building upon ([eq:motiv]), we formalise ballot secrecy by the equivalence $$C[V(A, v) \mid V(B, v')] \approx C[V(A, v') \mid
V(B, v)]\label{eq:ballotsecrecysystem}$$ where the process $V(A, v)$ models a voter with identity $A$ (including its private key, its device public key, and its private channel to the device) voting $v$, and the context $C$ models all other participants: authorities and hardware devices. (Other voters are included in $C$ for privacy results concerning more than two voters.) With two voters, we prove ballot secrecy by swapping data at the synchronisation in the mixnet. With an unbounded number of honest voters, we prove ballot secrecy using Corollary [cor:boundrepl] to model an unbounded number of voters by a replicated process. As far as we know, this is the first proof of this result.
With an additional dishonest voter, the proof of ballot secrecy fails. This failure does not come from a limitation of our approach, but from a ballot copying attack, already mentioned in the original paper (**Lee04?**) and formalised in (**Dreier11:PrivacyWithCorruptVoters?**): the dishonest voter can copy $A$’s vote, as follows. The adversary observes $A$’s encrypted vote on the bulletin board (since it is accompanied by the voter’s signature), inputs the ciphertext to the adversary’s tamper-resistant hardware device, uses the output to derive a related ballot, and derives $A$’s vote from the election outcome, which contains two copies of $A$’s vote.
### Analysis: receipt-freeness
Following (**DKR08?**), receipt-freeness can be formalised as follows: there exists a process $V'$ such that $$\begin{aligned}
V'^{\backslash \mathit{chc}} &\approx V(A, v)\label{eq:recfree1}\\
C[V(A, v')^{\mathit{chc}} \mid V(B, v)] &\approx C[V' \mid V(B, v')]\label{eq:recfree2}
\end{aligned}$$ where the context $C[\_]$ appears in [eq:ballotsecrecysystem], $\mathit{chc}$ is a public channel, $V'^{\backslash \mathit{chc}} = \nu\,\mathit{chc}.(V \mid !\mathit{chc}(x))$, which is intuitively equivalent to removing all outputs on channel $\mathit{chc}$ from $V'$, and $V(A, v')^{\mathit{chc}}$ is obtained by modifying $V(A, v')$ as follows: we output on channel $\mathit{chc}$ the private key of $A$, its device public key, all restricted names created by $V$, and messages received by $V$. Intuitively, the voter $A$ tries to prove to the adversary how she voted, by giving the adversary all its secrets, as modelled by $V(A, v')^{\mathit{chc}}$. The process $V'$ simulates a voter $A$ that votes $v$, as shown by [eq:recfree1], but outputs messages on channel $\mathit{chc}$ that aim to make the adversary think that it voted $v'$. The equivalence [eq:recfree2] shows that the adversary cannot distinguish voter $A$ voting $v'$ and trying to prove it to the adversary and voter $B$ voting $v$, from $V'$ and voter $B$ voting $v'$, so $V'$ successfully votes $v$ and deceives the adversary in thinking that it voted $v'$.
In the case of the Lee *et al*. protocol, $V'$ is derived from $V(A, v)^{\mathit{chc}}$ by outputting on $\mathit{chc}$ a fake Designated Verifier Proof that simulates a proof of re-encryption of a vote for $v'$, instead of the Designated Verifier Proof that it receives from the device. Intuitively, the adversary cannot distinguish a fake proof from a real one, because only the voter can verify the proof.
The equivalence [eq:recfree1] holds by construction of $V'$, because after removing outputs on $\mathit{chc}$, $V'$ is exactly the same as $V(A, v)$. We prove [eq:recfree2] using our approach, for an unbounded number of honest voters. Hence, this protocol satisfies receipt-freeness for an unbounded number of honest voters. As far as we know, this is the first proof of this result. Obviously, receipt-freeness does not hold with dishonest voters, because it implies ballot secrecy.
### Variant by Dreier, Lafourcade & Lakhnech
Dreier, Lafourcade & Lakhnech (**Dreier11:PrivacyWithCorruptVoters?**) introduced a variant of this protocol in which, in step 3, the voter additionally signs the ciphertext containing her vote, and in step 4, the hardware device verifies this signature. We have also analysed this variant using our approach. It is sufficiently similar to the original protocol that we obtain the same results for both.
### Variant by Delaune, Kremer, & Ryan
### Protocol description
Delaune, Kremer, & Ryan (**DKR08?**) introduced a variant of this protocol in which the hardware devices are replaced with a single administrator, and the voting phase becomes:
3. The voter encrypts her vote, signs the ciphertext, and sends the ciphertext and signature to the administrator on a private channel.
4. The administrator verifies the signature, re-encrypts the voter’s ciphertext, signs the re-encryption, computes a Designated Verifier Proof of re-encryption, and outputs these values to the voter.
5. If the signature and proof are valid, then the voter outputs her ballot, consisting of the signed re-encryption (via an anonymous channel).
The mixnet is replaced with the anonymous channel, and the tallying phase becomes:
6. The collector checks that the ballots are pairwise distinct, checks the administrator’s signature on each of the ballots, and, if valid, decrypts the ballots and announces the election outcome.
### Analysis: ballot secrecy
We have shown that this variant preserves ballot secrecy, with two honest voters, using our approach. In this proof, all keys are public and the collector is not trusted, so it is included in the adversary. Since the keys are public, any number of dishonest voters can also be included in the adversary, so the proof with two honest voters suffices to imply ballot secrecy for any number of possibly dishonest voters. Hence, this variant avoids the ballot copying attack and satisfies a stronger ballot secrecy property than the original protocol. Thus, we automate the proof made manually in (**DKR08?**). For this variant, the swapping occurs at the beginning of the voting process, so we can actually prove the equivalence by proving diff-equivalence after applying the general property that $C[P \mid Q] \approx C[Q \mid P]$, much like for Example [ex:diff-limitations]. Furthermore, an extension of ProVerif (**Cheval13?**) takes advantage of this property to merge processes into biprocesses in order to prove observational equivalence. The approach outlined in that paper also succeeds in proving ballot secrecy for this variant. It takes 13 minutes 22 seconds, while our implementation with swapping takes 34 seconds. It spends most of the time computing the merged biprocesses; this is the reason why it is slower.
### Analysis: receipt-freeness
We prove receipt-freeness for two honest voters. The administrator and voter keys do need to be secret, and all authorities need to be explicitly modelled. The process $V'$ is built similarly to the one for the original protocol by Lee *et al*. Equivalence [eq:recfree1] again holds by construction of $V'$. To prove [eq:recfree2], much like in (**DKR08?**), we model the collector as parallel processes that each input one ballot, check the signature, decrypt, synchronise together, and output the decrypted vote: $$\begin{aligned}
&c(b);\textnormal{let } ev=\mathsf{checksign}(pk_A,b) \textnormal{ in }\\
&\textnormal{let } v=\mathsf{dec}(sk_C,ev) \textnormal{ in }2\textnormal{::}\,\overline{c}\langle v\rangle
\end{aligned}$$ There are as many such processes as there are voters, two in our case. However, such a collector does not check that the ballots are pairwise distinct: each of the two parallel processes has access to a single ballot, so each process individually cannot check that the two ballots are distinct. We implemented this necessary check by manually modifying the code generated by our compiler, by adding a check that the ballots are distinct in the process that swaps data. An excerpt of the obtained code follows: $$\begin{aligned}
&(c(b);\textnormal{let } ev=\mathsf{checksign}(pk_A,b) \textnormal{ in }\\
&\phantom{(}\textnormal{let } v=\mathsf{dec}(sk_C,ev) \textnormal{ in }\overline{a_1}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{b, v}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle;c_1(v');\overline{c}\langle v'\rangle)\\
{}\mid{} &(c(b);\textnormal{let } ev=\mathsf{checksign}(pk_A,b) \textnormal{ in }\\
&\phantom{(}\textnormal{let } v=\mathsf{dec}(sk_C,ev) \textnormal{ in }\overline{a_2}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{b, v}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle;c_2(v');\overline{c}\langle v'\rangle)\\
{}\mid {}&(a_1(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{b_1, v_1}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$});a_2(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{b_2, v_2}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$});\\
(*)\quad &\phantom{(}\textnormal{if } b_1=b_2 \textnormal{ then } 0 \textnormal{ else }\\
&\phantom{(}\overline{c_1}\langle\mathsf{diff}[v_1,v_2]\rangle;\overline{c_2}\langle\mathsf{diff}[v_2,v_1]\rangle)
\end{aligned}$$ This code shows the two collectors and the process that swaps data. We use $a(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{b, v}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})$ as an abbreviation for $a(x);\allowbreak \textnormal{let } b=\pi_{1,2}(x) \textnormal{ in }
\textnormal{let } v=\pi_{2,2}(x) \textnormal{ in}$. The ballots are sent on channels $a_1$ and $a_2$ in addition to the decrypted votes, and we check that the two ballots are distinct at line $(*)$. With this code, ProVerif proves the diff-equivalence, so we have shown receipt-freeness for two honest voters. This proof is difficult to generalise to more voters in ProVerif, because in this case the collector should swap two ballots among the ones it has received (the two coming to the voters that swap their voters), but it has no means to detect which ones.
## Other examples
The idea of swapping for proving equivalences has been applied by Dahl, Delaune & Steel (**Delaune10:Vanets?**) to prove privacy in a vehicular ad-hoc network (**Freudiger07?**). They manually encode swapping based upon the informal idea of (**Smyth08:Obs?**). We have repeated their analysis using our approach. Thus, we automate the encoding of swapping in (**Delaune10:Vanets?**), and obtain stronger confidence in the results thanks to our soundness proof.
Backes, Hriţcu & Maffei (**Backes08:Voting?**) also applied the idea of swapping, together with other encoding tricks, to prove a privacy notion stronger than receipt-freeness, namely *coercion resistance*, of the protocol by Juels, Catalano & Jakobsson (**JCJ10?**). We did not try to repeat their analysis using our approach.
# Conclusion
We extend the applied pi calculus to include barrier synchronisation and define a compiler to the calculus without barriers. Our compiler enables swapping data between processes at barriers, which simplifies proofs of observational equivalence. We have proven the soundness of our compiler and have implemented it in ProVerif, thereby extending the class of equivalences that can be automatically verified. The applicability of the results is demonstrated by analysing ballot secrecy and receipt-freeness in election schemes, as well as privacy in a vehicular ad-hoc network. The idea of swapping data at barriers was introduced in (**Smyth08:Obs?**), without proving its soundness, and similar ideas have been used by several researchers (**Backes08:Voting?**; **Delaune10:Vanets?**), so we believe that it is important to provide a strong theoretical foundation to this technique.
### Acknowledgements
We are particularly grateful to Tom Chothia, Véronique Cortier, Andy Gordon, Mark Ryan, and the anonymous CSF reviewers, for their careful reading of preliminary drafts which led to this paper; their comments provided useful guidance. Birmingham’s *Formal Verification and Security Group* provided excellent discussion and we are particularly grateful to: Myrto Arapinis, Sergiu Bursuc, Dan Ghica, and Eike Ritter, as well as, Mark and Tom, whom we have already mentioned. Part of the work was conducted while the authors were at École Normale Supérieure, Paris, France and while Smyth was at Inria, Paris, France and the University of Birmingham, Birmingham, UK.
# Proofs for \S\ref{sec:proswapper
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 1761, column 15): unexpected end of input expecting \end{IEEEproof} \end{document} ^`
``` latex
\section{Proofs for \S\ref{sec:proswapper}}\label{app-swap-proof}
This appendix proves the results announced in \S\ref{sec:proswapper}.
Appendix~\ref{app:validity} proves Lemma~\ref{lem:validity} (validity);
Appendix~\ref{app:splitfinal} proves Lemma~\ref{lem:splitfinal} (soundness of $\splitprocSymb$);
Appendix~\ref{app:basicobs} proves three basic properties of
observational equivalence useful in order to prove the other results;
Appendix~\ref{app:standard-to-annotated-all} proves Proposition~\ref{prop:standard-to-annotated-all} (soundness of $\precompilerSymb$).
%
The rest of the appendix is devoted to the proof of Theorem~\ref{thm:soundnessSwapping}.
We show that barrier elimination commutes renaming with renaming and substitution (Appendix~\ref{app:renaming})
and that it preserves reduction
(Appendix~\ref{app:reduction}). Using these interim results, we prove Proposition~\ref{prop:preserve-compil-second}
(Appendix~\ref{app:prop:soundnessSwapping}) and, finally, Theorem~\ref{thm:soundnessSwapping} (Appendix~\ref{app:thm:soundnessSwapping}).
\subsection{Proof of Lemma~\ref{lem:validity} (Validity)}\label{app:validity}
\begin{lemma}\label{lem:valid-subst}
If $\context[Q]$ is valid, $\sigma$ is a ground substitution, $\context$ binds the variables in $\dom{\sigma}$ and no other variable above the hole, and $\fn{\range{\sigma}} \cap \channels{\barriers{Q}} = \emptyset$, then $\barriers{Q\sigma} = \barriers{Q}$ and $Q \sigma$ is valid.
\end{lemma}
\begin{proof}
The process $Q\sigma$ is closed because $\fv{Q\sigma} \subseteq \fv{Q} \setminus \dom{\sigma} \cup \fv{\range{\sigma}} \subseteq \fv{\context[Q]} \cup \fv{\range{\sigma}} = \emptyset$ since $\context[Q]$ is closed and $\sigma$ is ground.
Consider an annotated barrier in $Q$, such that $Q = \contextI[\sstageA{t}{a,c,\varsigma}Q']$. We rename the bound variables so that the variables in $\dom{\sigma}$ are not bound by $\contextI$ and the bound names so that the names in the range of $\sigma$ are not bound by $\contextI$. Since $\context[Q]$ is valid, we have $\fv{Q'} \subseteq \dom{\varsigma}$, so $(\sstageA{t}{a,c,\varsigma}Q')\sigma = \sstageA{t}{a,c,\varsigma\sigma}Q'$, so
\begin{align*}
&\barriers{(\sstageA{t}{a,c,\varsigma}Q')\sigma}\\
&\quad =\barriers{\sstageA{t}{a,c,\varsigma\sigma}Q'}\\
&\quad =\{\sstageA{t}{a,c,\ordom{\varsigma\sigma}}Q'\} \cup \barriers{Q'}\\
&\quad =\{\sstageA{t}{a,c,\ordom{\varsigma}}Q'\} \cup \barriers{Q'}\\
&\quad =\barriers{\sstageA{t}{a,c,\varsigma}Q'}
\end{align*}
Therefore, $\barriers{Q\sigma} = \barriers{Q}$.
Hence, the elements of $\channels{\barriers{Q\sigma}} = \channels{\barriers{Q}} \subseteq \channels{\barriers{\context[Q]}}$ are pairwise distinct, and
\begin{align*}
&\channels{\barriers{Q\sigma}} \cap \fnnobc{Q\sigma}\\
&\quad \subseteq \channels{\barriers{Q}} \cap (\fnnobc{Q} \cup \fn{\range{\sigma}})\\
&\quad \subseteq \channels{\barriers{\context[Q]}} \cap \fnnobc{Q} = \emptyset\,.
\end{align*}
Consider an annotated barrier in $Q\sigma$, such that $Q\sigma = \contextI[\sstageA{t}{a,c,\varsigma}Q']$. Then $Q = \contextII[\sstageA{t}{a,c,\varsigma'}Q'']$, $\contextI = \contextII\sigma$, $\varsigma = \varsigma'\sigma$, and $Q' = Q''\sigma$, after renaming the bound variables so that the variables in $\dom{\sigma}$ are not bound by $\contextII$ nor by $\varsigma'$ and the bound names so that the names in the range of $\sigma$ are not bound by $\contextII$. Since $\context[Q]$ is valid, $\fv{Q''} \subseteq \dom{\varsigma'}$, so $Q' = Q''\sigma = Q''$.
%
We have $\fv{Q'} = \fv{Q''} \subseteq \dom{\varsigma'} = \dom{\varsigma}$, $\contextI$ does not bind $a$, $c$, and the names in $\fn{Q'} = \fn{Q''}$ since $\context[\contextII]$ does not bind $a$, $c$, and the names in $\fn{Q''}$ and $\contextI$ binds the same names as $\contextII$.
\end{proof}
\medskip
\begin{proof}[Proof of Lemma~\ref{lem:validity}]
We prove each of the properties.
\emph{If every process in $P$ is valid, then $\Initconf{P}$ is valid.}
Suppose that $P$ is valid.
As defined in \S\ref{sec:barrannot}, we have $\Initconf{P} = B, E, \Pcal$,
where $B = \barriers{P}$, $E = \channels{B}$, and $\Pcal = \{ P\}$, so a fortiori
$\barriers{\Pcal} \subseteq B$,
$\channels{B} \subseteq E$,
all processes in $\Pcal$ are valid,
the elements of $\channels{B} = \channels{\barriers{P}}$ are pairwise distinct,
and $\channels{B} \cap \fnnobc{\Pcal} =
\channels{\barriers{P}} \cap \fnnobc{P} = \emptyset$.
Therefore, $\Initconf{P}$ is valid.
\emph{Validity is preserved by reduction.}
We proceed by cases on the reduction rule.
\begin{itemize}[labelindent=0pt]
\item Cases {\RNil} and {\RPar} are easy.
\item Case \RRepl: Since barriers never occur under replication, the transformed process $!P$ contains no barrier. Preservation of validity follows easily.
\item Case \RRes: Suppose that
$B,E,\Pcal \cup \{\new{n}.P\}\;\rightarrow\;B,E \cup \{n'\},\Pcal \cup \{P\activesubst{n'}{n}\}$ by {\RRes}, for some name $n'$ such that $n'\not\in E \cup \fn{\Pcal \cup \{\new{n}.P\}}$, and $B,E,\Pcal \cup \{\new{n}.P\}$ is a valid configuration.
Suppose that an annotated barrier $\sstageA{t}{a,c,\varsigma}Q$ occurs in $P$, so that $P = \context[\sstageA{t}{a,c,\varsigma}Q]$. Since $\new{n}.P$ is valid, $\new{n}.\context$ does not bind the names $a$, $c$, and $\fn{Q}$ above the hole, hence $n\notin\{a,c\}\cup\fn{Q}$, so
\[(\sstageA{t}{a,c,\varsigma}Q)\activesubst{n'}{n} = \sstageA{t}{a,c,\varsigma\activesubst{n'}{n}}Q\,,\]
so
\begin{align*}
&\barriers{(\sstageA{t}{a,c,\varsigma}Q)\activesubst{n'}{n}}\\
&\quad =\barriers{\sstageA{t}{a,c,\varsigma\activesubst{n'}{n}}Q}\\
&\quad =\{\sstageA{t}{a,c,\ordom{\varsigma\activesubst{n'}{n}}}Q\} \cup \barriers{Q}\\
&\quad =\{\sstageA{t}{a,c,\ordom{\varsigma}}Q\} \cup \barriers{Q}\\
&\quad =\barriers{\sstageA{t}{a,c,\varsigma}Q}
\end{align*}
Therefore, $\barriers{P\activesubst{n'}{n}} = \barriers{P} = \barriers{\new{n}.P}$.
Hence, we have $\barriers{\Pcal \cup \{P\activesubst{n'}{n}\}} = \barriers{\Pcal \cup \{\new{n}.P\}} \subseteq B$ and $\channels{B} \subseteq E \subseteq E \cup \{ n'\}$.
The processes in $\Pcal$ are valid. Let us show that the process $P\activesubst{n'}{n}$ is valid. The process $P\activesubst{n'}{n}$ is closed because $\new{n}.P$ is closed.
%
The elements of $\channels{\barriers{P\activesubst{n'}{n}}} = \channels{\barriers{\new{n}.P}}$ are pairwise distinct.
%
We have
\begin{align*}
&\channels{\barriers{P\activesubst{n'}{n}}} \cap \fnnobc{P\activesubst{n'}{n}}\\
&\quad \subseteq \channels{\barriers{\new{n}.P}}\\
&\qquad {} \cap (\fnnobc{\new{n}.P} \cup \{ n'\})\\
&\quad = \emptyset
\end{align*}
because $n' \notin \channels{\barriers{\new{n}.P}}$ since
\[\channels{\barriers{\new{n}.P}} \subseteq \channels{B} \subseteq E\]
and $n' \notin E$.
%
Consider an annotated barrier in $P\activesubst{n'}{n}$, such that $P\activesubst{n'}{n} = \context[\sstageA{t}{a,c,\varsigma}Q]$. Since $n' \notin \fn{\new{n}.P} = \fn{P} \setminus\{n\}$, $\new{n}.P = \new{n}.(P\activesubst{n'}{n}\activesubst{n}{n'}) =\new{n}.(\context[\sstageA{t}{a,c,\varsigma}Q]\activesubst{n}{n'})$. We rename the bound names in $\context$ so that they are different from $n$ and $n'$, and let $\contextI = \context\activesubst{n}{n'}$. Then $\new{n}.P = \new{n}.\contextI[\sstageA{t}{a\activesubst{n}{n'},\allowbreak c\activesubst{n}{n'},\allowbreak \varsigma\activesubst{n}{n'}}\allowbreak Q\activesubst{n}{n'}]$.
%
Since $\new{n}.P$ is valid, we have $\fv{Q} = \fv{Q\activesubst{n}{n'}} \subseteq \dom{\varsigma\activesubst{n}{n'}} = \dom{\varsigma}$ and
$\context$ does not bind $a$, $c$, and the names in $\fn{Q}$ above the hole since $\new{n}.\contextI$ does not bind $a\activesubst{n}{n'}$, $c\activesubst{n}{n'}$, and the names of $\fn{Q\activesubst{n}{n'}}$ above the hole.
The elements of $\channels{B}$ are pairwise distinct by hypothesis, and
\begin{align*}
&\channels{B} \cap \fnnobc{\Pcal \cup \{P\activesubst{n'}{n}\}}\\
&\quad \subseteq \channels{B} \cap (\fnnobc{\Pcal \cup \{ \new{n}.P \}} \cup \{ n'\})\\
&\quad = \emptyset
\end{align*}
because $n' \notin \channels{B}$ since $\channels{B} \subseteq E$
and $n' \notin E$.
\item Case \RIO: Suppose that
$B,E,\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}\;\rightarrow\;B,E,\Pcal \cup \{P,Q\activesubst{M}{x}\}$ by {\RIO} and $B,E,\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}$ is a valid configuration.
The term $M$ is ground since $\Out[N]{M}.P$ is closed. Moreover,
$\channels{\barriers{Q}} \cap \fn{M} = \emptyset$ since
$\channels{\barriers{\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}}}
\cap \fnnobc{\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}} = \emptyset$.
Hence, by Lemma~\ref{lem:valid-subst}, we have $\barriers{\Pcal \cup \{P,Q\activesubst{M}{x}\}} = \barriers{\Pcal \cup \{P,Q\}} = \barriers{\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}} \subseteq B$. We have $\channels{B} \subseteq E$.
%
The processes in $\Pcal$ are valid. The validity of $P$ follows easily from the validity of $\Out[N]{M}.P$. The process $Q\activesubst{M}{x}$ is valid by Lemma~\ref{lem:valid-subst}.
%
The elements of $\channels{B}$ are pairwise distinct by hypothesis, and
$\channels{B} \cap \fnnobc{\Pcal \cup \{P,Q\activesubst{M}{x}\}}
\subseteq \channels{B} \cap \fnnobc{\Pcal \cup \{\Out[N]{M}.P, \In[N]{x}.Q\}} = \emptyset$.
%
Therefore, $B,E,\Pcal \cup \{P,Q\activesubst{M}{x}\}$ is valid.
\item Case \RDestrI: Suppose that $B,E,\Pcal \cup \{\Letinelse{x}{D}{P}Q\}\;\rightarrow\;B,E,\Pcal \cup \{P\activesubst{M}{x}\}$ by {\RDestrI}, where $D\Downarrow M$, and $B,E,\Pcal \cup \{\Letinelse{x}{D}{P}Q\}$ is a valid configuration.
The term $M$ is ground since $D$ is ground, and $\channels{\barriers{P}} \cap \fn{M} = \emptyset$ since $\channels{\barriers{P}} \cap \fn{D} = \emptyset$, since $\channels{\barriers{\Letinelse{x}{D}{P}Q}} \cap \fnnobc{\Letinelse{x}{D}{P}Q} = \emptyset$ by validity of $\Letinelse{x}{D}{P}Q$.
Hence, by Lemma~\ref{lem:valid-subst}, we have
\begin{align*}
&\barriers{\Pcal \cup \{P\activesubst{M}{x}\}}\\
&\quad = \barriers{\Pcal \cup \{P\}} \\
&\quad \subseteq \barriers{\Pcal \cup \{\Letinelse{x}{D}{P}Q\}}\\
&\quad \subseteq B\,.
\end{align*}
We have $\channels{B} \subseteq E$.
%
The processes in $\Pcal$ are valid. The process $P\activesubst{M}{x}$ is valid by Lemma~\ref{lem:valid-subst}.
%
The elements of $\channels{B}$ are pairwise distinct by hypothesis, and
$\channels{B} \cap \fnnobc{\Pcal \cup \{P\activesubst{M}{x}\}}
\subseteq \channels{B} \cap \fnnobc{\Pcal \cup \{\Letinelse{x}{D}{P}Q\}} =
\emptyset$.
%
Therefore, $B,E,\Pcal \cup \{P\activesubst{M}{x}\}$ is valid.
\item Case \RDestrII: Suppose that $B,E,\Pcal \cup \{\Letinelse{x}{D}{P}Q\}\;\rightarrow\;B,E,\Pcal \cup \{Q\}$ by {\RDestrII} and $B,E,\Pcal \cup \{\Letinelse{x}{D}{P}Q\}$ is a valid configuration.
We have $\barriers{\Pcal \cup \{Q\}} \subseteq \barriers{\Pcal \cup \{\Letinelse{x}{D}{P}Q\}} \subseteq B$ and
$\channels{B} \subseteq E$.
%
The processes in $\Pcal$ are valid. The validity of $Q$ follows easily from the validity of $\Letinelse{x}{D}{P}Q$.
%
The elements of $\channels{B}$ are pairwise distinct, and
$\channels{B} \cap \fnnobc{\Pcal \cup \{ Q\}} \subseteq \channels{B} \cap \fnnobc{\Pcal \cup \{\Letinelse{x}{D}{P}Q\}} = \emptyset$.
%
Therefore, $B,E,\Pcal \cup \{Q\}$ is valid.
\item Case \RBarII: Let $\Pcal_1 = \Pcal \cup \{\sstage{t}P_1,\allowbreak \dots,\allowbreak \sstage{t}P_m, \allowbreak \sstageA{t}{a_{m+1},c_{m+1},\varsigma_{m+1}}P_{m+1}, \allowbreak \dots, \allowbreak \sstageA{t}{a_n,c_n,\varsigma_n}P_n\}$, $\Pcal_2 = \Pcal \cup \{P_1,\allowbreak \dots,\allowbreak P_m,\allowbreak P_{m+1}\varsigma_{m+1},\allowbreak \dots,\allowbreak P_n\varsigma_n\}$, and
suppose that
$B,E,\Pcal_1 \rightarrow\;B',E,\Pcal_2$
by {\RBarII}, where $B = \{ t^m, \sstageA{t}{a_{m+1},c_{m+1},\ordom{\varsigma_{m+1}}}P_{m+1}, \allowbreak \dots, \allowbreak \sstageA{t}{a_n,c_n,\ordom{\varsigma_n}}P_n \} \cup B'$; for all $t'$ such that $t' \leq t$, we have $t'\notin B'$ and $\sstageA{t'}{\_}\_ \notin B'$; and $B,E,\Pcal_1$ is a valid configuration.
The substitution $\varsigma_i$ is ground since $\sstageA{t}{a_i,c_i,\varsigma_i}P_i$ is closed and $\channels{\barriers{P_i}} \cap \fn{\range{\varsigma_i}} = \emptyset$ since $\channels{\barriers{\sstageA{t}{a_i,c_i,\varsigma_i}P_i}} \cap \fnnobc{\sstageA{t}{a_i,c_i,\varsigma_i}P_i} = \emptyset$ since $\sstageA{t}{a_i,c_i,\varsigma_i}P_i$ is valid.
By Lemma~\ref{lem:valid-subst}, we have
\begin{align*}
&\barriers{\Pcal_2}\\
&\quad = \barriers{\Pcal \cup \{P_1, \dots, P_n\}}\\
&\quad = \barriers{\Pcal_1} \setminus {}\\
&\qquad\qquad \{ t^m, \sstageA{t}{a_{m+1},c_{m+1},\ordom{\varsigma_{m+1}}}P_{m+1}, \\
&\phantom{\qquad\qquad \{} \dots, \sstageA{t}{a_n,c_n,\ordom{\varsigma_n}}P_n \}\\
&\quad \subseteq B\setminus \{ t^m, \sstageA{t}{a_{m+1},c_{m+1},\ordom{\varsigma_{m+1}}}P_{m+1}, \\
&\phantom{\quad\subseteq B\setminus \{} \dots, \allowbreak \sstageA{t}{a_n,c_n,\ordom{\varsigma_n}}P_n \}\\
&\quad = B'
\end{align*}
and
$\channels{B'} \subseteq \channels{B} \subseteq E$.
%
The processes in $\Pcal$ are valid. The validity of $P_i$ for $i \leq m$ follows easily from the validity of $\sstage{t}P_i$. The process $P_i \varsigma_i$ for $i > m$ is valid by Lemma~\ref{lem:valid-subst}.
%
The elements of $\channels{B'} \subseteq \channels{B} $ are pairwise distinct, and
$\channels{B'} \cap \fnnobc{\Pcal_2} \subseteq \channels{B} \cap \fnnobc{\Pcal_1} = \emptyset$.
\end{itemize}
\emph{Validity is preserved by application of an
adversarial context.}
Let $\Conf = B, E, \Pcal$ be a valid configuration
and $\context$ be an adversarial context.
We have $\context = \new{\tilde n}.(\_ \mid Q)$ with $\fv{Q} = \emptyset$
and $\barriers{Q} = \emptyset$. We suppose that the names in $E$
have been renamed so that $\fn{Q} \cap E = \emptyset$.
Then we have $\context[\Conf] = B,E \cup \{\tilde n\},\Pcal\cup\{Q\}$.
Let us show that $\context[\Conf]$ is valid.
We have
\begin{align*}
&\barriers{\Pcal\cup\{Q\}} = \barriers{\Pcal} \subseteq B\\
&\channels{B} \subseteq E \subseteq E \cup \{\tilde n\}
\end{align*}
All processes in $\Pcal$ are valid and $Q$ is valid since it is closed and contains no barriers.
The elements of $\channels{B}$ are pairwise distinct by hypothesis, and
$\channels{B} \cap \fnnobc{\Pcal \cup \{Q\}} = \emptyset$ because
$\channels{B} \cap \fnnobc{\Pcal} = \emptyset$ and
$\channels{B} \cap \fnnobc{Q} \subseteq E \cap \fn{Q} = \emptyset$.
Therefore, $\context[\Conf]$ is valid.
\emph{Validity is preserved by application of $\fstSymb$ and $\sndSymb$.}
We consider the case of $\fstSymb$. The case of $\sndSymb$ is symmetric.
We first show that, if biprocess $P$ is valid, then $\fst{P}$ is valid.
Suppose that $P$ is valid. Since $P$ is closed and $\fv{\fst{P}} \subseteq \fv{P}$, the process $\fst{P}$ is also closed.
The elements of $\channels{\barriers{\fst{P}}} = \channels{\barriers{P}}$ are pairwise distinct.
We have $\channels{\barriers{\fst{P}}} \cap \fnnobc{\fst{P}} \subseteq \channels{\barriers{P}} \cap \fnnobc{P} = \emptyset$.
Consider an annotated barrier in $\fst{P}$, such that $\fst{P} = \context[\sstageA{t}{a,c,\varsigma}Q]$. Then $P = \contextI[\sstageA{t}{a,c,\varsigma'}Q']$ such that $\context = \fst{\contextI}$, $\varsigma = \fst{\varsigma'}$, and $Q = \fst{Q'}$. We have $\fv{Q} \subseteq \fv{Q'} \subseteq \dom{\varsigma'} = \dom{\varsigma}$, $\contextI$ does not bind $a$, $c$, nor the names in $\fn{Q'}$ above the hole, so $\context$ does not bind $a$, $c$, nor the names in $\fn{Q} \subseteq \fn{Q'}$ above the hole, because $\context$ binds the same names as $\contextI$. So $\fst{P}$ is valid.
Next, we show that, if a configuration $B, E, \Pcal$ is valid, then $\fst{B, E, \Pcal} = \fst{B}, E, \fst{\Pcal}$ is valid.
Suppose that $B, E, \Pcal$ is valid.
We have
\begin{align*}
&\barriers{\fst{\Pcal}} = \fst{\barriers{\Pcal}} \subseteq \fst{B}\,,\\
&\channels{\fst{B}} = \channels{B} \subseteq E\,,
\end{align*}
all processes in $\fst{\Pcal}$ are valid since all processes in $\Pcal$ are valid,
the elements of $\channels{\fst{B}} = \channels{B}$ are pairwise distinct, and
$\channels{\fst{B}} \cap \fnnobc{\fst{\Pcal}} \subseteq \channels{B} \cap \fnnobc{\Pcal} = \emptyset$.
So $\fst{B, E, \Pcal}$ is valid.
\end{proof}
\iffalse
\begin{proof}[Proof of Proposition~\ref{prop:let-intro}]
We define the relation $\Rel$ by
\[
(B, E, \{C_i[\Letin{x_i}{M_i}Q_i] \mid i \leq n \} \cup \Pcal) \Rel
(B, E, \{ C_i[Q_i\activesubst{M_i}{x_i}] \mid i \leq n \} \cup \Pcal)
\]
where $n \geq 0$ and $B, E, \{C_i[\Letin{x_i}{M_i}Q_i] \mid i \leq n \} \cup \Pcal $ and $B, E, \{ C_i[Q_i\activesubst{M_i}{x_i}] \mid i \leq n \} \cup \Pcal$ are valid configurations. We show that $\Rel \cup \Rel^{-1}$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}. Hence ${\Rel \cup \Rel^{-1}} \subseteq {\approxconfig}$. In particular, if $P_0 = \context[Q\activesubst{M}{x}]$ is a closed standard process and $P'_0 = \context[\Letin{x}{M}Q]$, then $P_0$ and $P'_0$ are valid since they do not contain annotated barriers, so $\Initconf{P_0} = B, E, \{P_0\}$ and $\Initconf{P'_0} = B, E, \{P'_0\}$, where $B = \barriers{P_0} = \barriers{P'_0}$ and $E = \channels{\annbarriers{P_0}} = \channels{\annbarriers{P'_0}} = \emptyset$ are valid configurations by Lemma~\ref{lem:validity}. We have $\Initconf{P_0} \Rel \Initconf{P'_0}$, so $\Initconf{P_0} \approxconfig \Initconf{P'_0}$, hence $P_0 \approx P'_0$.
When $P_0 = \context[Q\activesubst{M}{x}]$ is a closed standard biprocess and $P'_0 = \context[\Letin{x}{M}Q]$, we obtain $\fst{P'_0} \approx \fst{P_0}$, and $\snd{P'_0} \approx \snd{P_0}$ by applying the previous result to $\fst{P_0}$ and $\snd{P_0}$.
\end{proof}
\fi
\subsection{Proof of Lemma~\ref{lem:splitfinal} (Soundness of $\splitprocSymb$)}\label{app:splitfinal}
\begin{figure}
\begin{align*}
\begin{split}
&\splitproc{M} = (x, (\subst{M}{x})) \text{ where $x$ is a fresh variable,}\\
&\qquad \text{if $(\fv{M} \cup \fn{M}) \cap U = \emptyset$}
\end{split}\\
&\splitproc{u} = (u, \emptyset)\text{ if $u \in U$}\\
&\splitproc{\context[Q_1, \dots, Q_n]} = (\context[Q'_1,\dots,Q'_n], \varsigma)\text{ where}\\
&\quad \text{for all }i \leq n, \splitproc[U \cup U_i]{Q_i} = (Q'_i, \varsigma_i)\\
\begin{split}
&\quad \text{$\context[\_,\dots,\_]$ binds the names and variables in $U_i$ above}\\
&\quad \text{the $i$-th hole}
\end{split}\\
&\quad \text{$\varsigma = \varsigma_1 + \dots + \varsigma_n$, where }\\
\begin{split}
&\qquad
(\subst{M_1}{x_1}, \dots, \subst{M_n}{x_n}) + (\subst{M_{n+1}}{x_{n+1}}, \dots, \subst{M_m}{x_m})\\
&\qquad {} = (\subst{M_1}{x_1}, \dots, \subst{M_m}{x_m})
\end{split}\\
&\quad \text{$Q_i$ may be a term, an expression, or a process}\\
&\quad \text{$\context[\_,\dots,\_]$ is one of the following contexts:}\\
&\quad \begin{array}{r l r l}
1.& 0 & 6. &\Out[{[\_]}]{[\_]}.[\_]\\
2.&[\_] \mid [\_] & 7. &\Letinelse{x}{[\_]}{[\_]}{[\_]}\\
3.&![\_] & 8. &\sstage{t}{[\_]}\\
4.&\new{a}.[\_] & 9. &h([\_],\dots,[\_])\\
5.&\In[{[\_]}]{x}.[\_]\qquad{} & 10.&\diff{[\_]}{[\_]}
\end{array}\\
&\quad \begin{array}{@{}l@{}}
\text{Context~4 binds $a$ above its hole;}\\
\text{context~5 binds $x$ above its second hole; }\\
\text{context~7 binds $x$ above its second hole;}\\
\text{contexts~9 and~10 are used only when the first rule of}\\
\text{the definition of $\splitprocSymb$ does not apply.}
\end{array}
\end{align*}
\caption{Helper function for barrier annotation}
\label{fig:split}
\end{figure}
The function $\splitprocSymb$ can be defined as $\splitprocemp{Q} =
\splitproc[\emptyset]{Q}$ with the definition of $\splitproc{Q}$ by
structural induction on $Q$ given in Figure~\ref{fig:split}.
In that definition, we use contexts with multiple holes.
%
All inductive cases for terms, expressions, and processes
have the same form, so we exceptionally use the same notation $Q$ for
a term, an expression, and a process.
%
Assuming we initially call $\splitproc[\emptyset]{Q_0}$, in each
recursive call $\splitproc{Q}$, the set $U$ contains all bound names and
variables at the subprocess $Q$ in $Q_0$.
%
Each call to $\splitproc{Q}$ returns $(Q', \varsigma)$ where $Q'$ is obtained from $Q$ by replacing the largest subterms $M_i$ of $Q$ that do not contain names or variables in $U$ or previously bound in $Q$ with fresh variables $x_i$, and recording the replacement in the ordered substitution $\varsigma = (\subst{M_1}{x_1}, \dots, \subst{M_n}{x_n})$.
When $Q$ is a term $M$, $\splitproc{Q} = \splitproc{M}$ behaves as follows
\begin{itemize}
\item If $M$ does not contain names or variables in $U$, then $M$ is replaced with a fresh variable $x$, and the replacement is recorded in $\varsigma = (\subst{M}{x})$, hence $\splitproc{M} = (x, (\subst{M}{x}))$ (first rule of Figure~\ref{fig:split}).
\item If $M$ is a variable in $U$, then it is left unchanged, hence $\splitproc{u} = (u, \emptyset)$ (second rule).
\item If $M$ is a constructor application $M = f(M_1, \dots, M_n)$ that contains names or variables in $U$, then we cannot replace $M$ itself with a variable, but we perform the replacement on the largest possible subterms of $M$ by induction: $\splitproc{M}= (f(M'_1, \dots, M'_n), \varsigma_1 + \dots + \varsigma_n)$ where
for all $i \leq n$, $\splitproc{M_i} = (M'_i, \varsigma_i)$ (third rule with context~9); the case in which $M = \diff{M_1}{M_2}$ is similar, using context~10.
\end{itemize}
\noindent
For an expression or process $Q$, we proceed by induction using the third rule of Figure~\ref{fig:split}, and after several recursive calls, we apply $\splitprocSymb$ to each term contained in $Q$.
\begin{lemma}\label{lem:split}
Let $Q$ be a term, an expression, or a process.
%
If $(Q',\varsigma) = \splitproc{Q}$, then $Q'\varsigma = Q$,
$(\fv{\range{\varsigma}} \cup \fn{\range{\varsigma}}) \cap U =
\emptyset$, $\dom{\varsigma} \subseteq \fv{Q'}\subseteq
\dom{\varsigma} \cup U$, $\fn{Q'} \subseteq U$, and
$\dom{\varsigma}$ consists of fresh variables.
\end{lemma}
\begin{proof}
The proof proceeds by induction on $Q$.
\begin{itemize}
\item Case $Q = M$ with $(\fv{M} \cup \fn{M}) \cap U = \emptyset$.
We have $\splitproc{M} = (x, (\subst{M}{x}))$ where $x$ is a fresh variable,
so $Q' = x$ and $\varsigma = (\subst{M}{x})$.
%
Hence $Q'\varsigma = M = Q$, $(\fv{\range{\varsigma}} \cup
\fn{\range{\varsigma}}) \cap U = (\fv{M} \cup \fn{M}) \cap
U = \emptyset$, $\fv{Q'} = \dom{\varsigma} = \{x\}$, $\fn{Q'} =
\emptyset$, and $\dom{\varsigma}$ consists of fresh variables.
\item Case $Q = u$ with $u \in U$.
We have $\splitproc{u} = (u, \emptyset)$, so $Q' = u$ and $\varsigma = \emptyset$.
%
Hence $Q'\varsigma = u = Q$, $\fv{\range{\varsigma}} \cup \fn{\range{\varsigma}} = \emptyset$,
$\dom{\varsigma} = \emptyset$, $\fv{Q'} \subseteq U$, and $\fn{Q'} \subseteq U$.
\item Case $Q = \context[Q_1, \dots, Q_n]$.
The considered contexts $\context$ do not have any free names or variables.
We have $\splitproc{\context[Q_1, \dots, Q_n]} = (\context[Q'_1,\dots,Q'_n], \varsigma)$
where for all $i \leq n$, $\splitproc[U \cup U_i]{Q_i} = (Q'_i, \varsigma_i)$,
$\context[\_,\dots,\_]$ binds the names and variables in $U_i$ above the $i$-th hole,
and $\varsigma = \varsigma_1 + \dots + \varsigma_n$, so $Q' = \context[Q'_1,\dots,Q'_n]$.
%
Hence $Q' \varsigma = \context[Q'_1\varsigma_1,\dots,Q'_n\varsigma_n]$
because $Q'_i \varsigma = Q'_i \varsigma_i$, since $\fv{Q'_i} \subseteq \dom{\varsigma_i} \cup U$
and, for all $j \neq i$, $\dom{\varsigma_j}$ consists of fresh variables, so it does not intersect $\dom{\varsigma_i} \cup U$,
and $\context[\_,\dots,\_]$ does not capture names nor variables because $(\fv{\range{\varsigma_i}} \cup \fn{\range{\varsigma_i}}) \cap U_i =
\emptyset$ and $\dom{\varsigma_i} \cap U_i = \emptyset$.
%
Moreover, $(\fv{\range{\varsigma}} \cup \fn{\range{\varsigma}}) \cap U \subseteq \bigcup_{i \leq n} (\fv{\range{\varsigma_i}} \cup \fn{\range{\varsigma_i}}) \cap (U \cup U_i) = \emptyset$.
%
For all $i \leq n$, $\dom{\varsigma_i} \subseteq \fv{Q'_i}\subseteq
\dom{\varsigma_i} \cup U \cup U_i$,
so $\dom{\varsigma_i} \subseteq \fv{Q'_i} \setminus U_i \subseteq
\dom{\varsigma_i} \cup U$ since $\dom{\varsigma_i} \cap U_i = \emptyset$,
so by taking the union over $i \leq n$,
$\dom{\varsigma} \subseteq \fv{Q'} \subseteq \dom{\varsigma} \cup U$.
%
For all $i \leq n$, $\fn{Q'_i} \subseteq U \cup U_i$, so
$\fn{Q'_i} \setminus U_i \subseteq U$, so
by taking the union over $i \leq n$, $\fn{Q'} \subseteq U$.
%
Finally, for all $i \leq n$, $\dom{\varsigma_i}$ consists of fresh variables,
so $\dom{\varsigma}$ consists of fresh variables.
\qedhere
\end{itemize}
\noqed
\end{proof}
\begin{proof}[Proof of Lemma~\ref{lem:splitfinal}]
Lemma~\ref{lem:splitfinal} is an immediate corollary of Lemma~\ref{lem:split}.
\end{proof}
\subsection{Basic Properties of Observational Equivalence}\label{app:basicobs}
Propositions \ref{prop:1} -- \ref{prop:3} follow immediately from the semantics and definition of observational equivalence.
\begin{proposition}\label{prop:1}
Let $B, E, \{\new{n}.P\}\cup\Pcal$ be a valid configuration, and
$n'$ be a name, where $n'\not\in E \cup \fn{\{\new{n}.P\}\cup\Pcal}$.
We have $B, E, \{\new{n}.P\}\cup\Pcal \approxconfig B, E\cup\{n'\}, \{P\activesubst{n'}{n}\}\cup\Pcal$.
\end{proposition}
\begin{proof}
We have $B, E, \{\new{n}.P\}\cup\Pcal \;\rightarrow\; B, E\cup\{n'\}, \{P\activesubst{n'}{n}\}\cup\Pcal$ by \RRes, so by Lemma~\ref{lem:validity}, $B, E\cup\{n'\}, \{P\activesubst{n'}{n}\}\cup\Pcal$ is also a valid configuration.
We define the relations $\Rel_0$ and $\Rel_1$ by
\begin{align*}
\Conf &\Rel_0 \Conf\\
(B, E, \{\new{n}.P\}\cup\Pcal) &\Rel_1 (B, E\cup\{n'\}, \{P\activesubst{n'}{n}\}\cup\Pcal)
\end{align*}
for any $\Conf$, $B$, $E$, $n$, $n'$, $P$, $\Pcal$ such that $n'\not\in E \cup \fn{\{\new{n}.P\}\cup\Pcal}$ and $\Conf$, $(B, E, \{\new{n}.P\}\cup\Pcal)$, and $(B, E\cup\{n'\}, \{P\activesubst{n'}{n}\}\cup\Pcal)$ are valid configurations. We have that $\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}. Hence ${\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}} \subseteq {\approxconfig}$. This property implies the desired equivalence.
\end{proof}
\begin{proposition}\label{prop:2}
Let $B, E, \Pcal$ be a valid configuration, and
$n$ be a name, where $n \notin \fn{\Pcal}$.
We have $B, E, \Pcal \approxconfig B, E \cup \{n\}, \Pcal$.
\end{proposition}
\begin{proof}
If $ n\in E$, the result is obvious. Let us prove it when $n \notin E \cup \fn{\Pcal}$.
When $B, E, \Pcal$ is valid, $B, E \cup \{n\}, \Pcal$ is a fortiori valid.
We define the relation $\Rel$ by
\[
(B, E, \Pcal) \Rel (B, E \cup \{n\}, \Pcal)
\]
for any $B$, $E$, $\Pcal$, $n$ such that $n \notin E \cup \fn{\Pcal}$, and $B, E, \Pcal$ and $B, E \cup \{n\}, \Pcal $ are valid configurations. We have that $\Rel \cup \Rel^{-1}$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}. Hence ${\Rel \cup \Rel^{-1}} \subseteq {\approxconfig}$. This property implies the desired equivalence.
%\bbnote{I removed the renaming $\alpha$ because I now consider configurations equal modulo renaming.}%
\end{proof}
\begin{proposition}\label{prop:3}
Let $B, E, \{P \mid Q\} \cup \Pcal$ be a valid configuration.
We have $B, E, \{P \mid Q\} \cup \Pcal \approxconfig B, E, \{P, Q\} \cup \Pcal$.
\end{proposition}
\begin{proof}
We have $B, E, \{P \mid Q\} \cup \Pcal \;\rightarrow\; B, E, \{P, Q\} \cup \Pcal$ by \RPar, so by Lemma~\ref{lem:validity}, $B, E, \{P, Q\} \cup \Pcal$ is also a valid configuration.
We define the relations $\Rel_0$ and $\Rel_1$ by
\begin{align*}
\Conf &\Rel_0 \Conf\\
(B, E, \{P \mid Q\} \cup \Pcal) &\Rel_1 (B, E, \{P, Q\} \cup \Pcal)
\end{align*}
for any $\Conf$, $B$, $E$, $P$, $Q$, $\Pcal$ such that $\Conf$, $(B, E, \{P \mid Q\} \cup \Pcal)$, and $(B, E, \{P, Q\} \cup \Pcal)$ are valid configurations. We have that $\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}. Hence ${\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}} \subseteq {\approxconfig}$. This property implies the desired equivalence.
\end{proof}
\subsection{Proof of Proposition~\ref{prop:standard-to-annotated-all} (Soundness of $\precompilerSymb$)}\label{app:standard-to-annotated-all}
\begin{proposition}\label{prop:standard-to-annotated-one}
For any context $\context$ without replication above the hole, any process $P$, stage $t$, names $a, c$, ordered substitution $\varsigma$ such that $\context[\sstage{t}P\varsigma]$ and $\context[\sstageA{t}{a,c,\varsigma}P]$ are valid processes, we have
\[\context[\sstage{t}P\varsigma] \approx \context[\sstageA{t}{a,c,\varsigma}P]\]
\end{proposition}
\begin{proof}
We define the relations $\Rel_0$ and $\Rel_1$ by
\begin{align*}
(B, E, \Pcal) &\Rel_0 (B', E, \Pcal)\\
(B, E, \{\context[\sstage{t}P\varsigma]\} \cup \Pcal) &\Rel_1 (B', E, \{\context[\sstageA{t}{a,c,\varsigma}P]\} \cup \Pcal)
\end{align*}
where $(B, E, \Pcal)$, $(B', E, \Pcal)$, $(B, E, \{\context[\sstage{t}P\varsigma]\} \cup \Pcal)$, and $(B', E, \{\context[\sstageA{t}{a,c,\varsigma}P]\} \cup \Pcal)$ are valid configurations and for all $t'$, $B_{|t'} = B'_{|t'}$,
where $B_{|t'}$ denotes the total number of barriers of the form $t'$ or $\sstageA{t'}{a',c',\tup{x}}P'$ in $B$. We show that ${\Rel} = {\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}}$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}. Conditions~1 and~3 are obvious.
%\bbnote{More sketchy than some other proofs, but giving more details would be painful and would not help, I believe.}%
To prove Condition~2, we notice that,
when $(B, E, \Pcal) \Rel (B', E, \Pcal')$, $\RBarII$ is enabled for barrier $t'$
%\bbnote{Is ``barrier $t'$'' clear? I use $t'$ instead of $t$ because it is not necessarily the $t$ of the definition of $\Rel_1$. Ben: looks clear.}%
in $(B, E, \Pcal)$ if and only if
it is enabled in $(B', E, \Pcal')$. Indeed, $\RBarII$ is enabled for barrier $t'$ in $(B, E, \Pcal)$ when $B_{|t''} = 0$ for all $t'' < t'$ and $\Pcal$ contains $B_{|t'}$ processes of form $\sstage{t'}P$ or $\sstageA{t'}{a,c,\varsigma}P$. (Validity ensures that $\barriers{\Pcal}\subseteq B$, so for barrier $t'$, $B$ and $\Pcal$ contain the same number of standard, resp. annotated, barriers and the content of annotated barriers also matches.)
From this property, we prove Condition~2:
\begin{itemize}
\item Case~1: $(B, E, \Pcal) \Rel_0 (B', E, \Pcal)$ and $(B, E, \Pcal) \reduc \Conf_1$.
If this reduction is by $\RBarII$ for barrier $t'$, then $\Conf_1 = (B_1, E, \Pcal_1)$ where $B_1$ is obtained from $B$ by removing all (standard or annotated) barriers $t'$. Let $B'_1$ be obtained from $B'$ by removing all (standard or annotated) barriers $t'$. Then we have $(B', E, \Pcal) \reduc (B'_1, E, \Pcal_1)$ and $(B_1, E, \Pcal_1) \Rel_0 (B'_1, E, \Pcal_1)$.
Otherwise, $\Conf_1 = (B, E_1, \Pcal_1)$, $(B', E, \Pcal) \reduc (B', \allowbreak E_1, \allowbreak \Pcal_1)$ by the same reduction and $(B, \allowbreak E_1, \allowbreak \Pcal_1) \Rel_0 (B', \allowbreak E_1, \allowbreak \Pcal_1)$.
\item Case~2: $(B, E, \{\context[\sstage{t}P\varsigma]\} \cup \Pcal) \Rel_1 (B', \allowbreak E, \allowbreak \{\context[\sstageA{t}{a,c,\varsigma}P]\} \cup \Pcal)$ and $(B, \allowbreak E, \allowbreak \{\context[\sstage{t}P\varsigma]\} \cup \Pcal) \reduc \Conf_1$.
If this reduction reduces only processes in $\Pcal$, then the same reduction applies on the other side, much like in Case~1, and the reduced processes are in $\Rel_1$.
If this reduction reduces $\context[\sstage{t}P\varsigma]$ and is not $\RBarII$ for barrier $t$, then the same reduction also applies on the other side. If the reduction eliminates $\sstage{t}P\varsigma$ (so the reduction reduces $\context[\sstage{t}P\varsigma]$ by $\RDestrI$ or $\RDestrII$), then the reduced processes are in $\Rel_0$. Otherwise, the reduced processes are still in $\Rel_1$, and any substitutions are applied to $\varsigma$. (By validity, $\fv{P} \subseteq \dom{\varsigma}$, so substitutions leave $P$ unchanged.)
If this reduction is $\RBarII$ for barrier $t$, then context $\context$ is empty. (When $n$ barriers $t$ reduce, $\Pcal_0 = \{\context[\sstage{t}P\varsigma]\} \cup \Pcal$ contains $n$ barriers $t$ at toplevel and $B$ contains $n$ barriers $t$. Since $\barriers{\Pcal_0}\subseteq B$ by validity, all barriers $t$ in $\Pcal_0$ are at toplevel and are reduced.) The reduction transforms $\sstage{t}P\varsigma$ into $P\varsigma$. The same reduction also applies on the other side, and transforms
$\sstageA{t}{a,c,\varsigma}P$ into $P\varsigma$, so the reduced processes are in $\Rel_0$.
\item Case~3: $(B', E, \{\context[\sstageA{t}{a,c,\varsigma}P]\} \cup \Pcal) \Rel_1^{-1} (B, E, \{\context[\sstage{t}P\varsigma]\} \cup \Pcal)$ and $(B, \allowbreak E, \allowbreak \{\context[\sstageA{t}{a,c,\varsigma}P]\} \cup \Pcal) \reduc \Conf_1$. This case can be treated similarly to Case~2.
\end{itemize}
Hence ${\Rel_0 \cup \Rel_1 \cup \Rel_1^{-1}} \subseteq {\approxconfig}$.
Let
\begin{align*}
&B = \barriers{\context[\sstage{t}P\varsigma]}\,,\\
&B' = \barriers{\context[\sstageA{t}{a,c,\varsigma}P]}\,,\\
&E = \channels{B}\,\text{, and}\\
&E' = \channels{B'} = E \cup \{a,c\}\,.
\end{align*}
We have
\begin{align*}
&\Initconf{\context[\sstage{t}P\varsigma]} = B, E, \{\context[\sstage{t}P\varsigma]\}\text{ and}\\
&\Initconf{\context[\sstageA{t}{a,c,\varsigma}P]} = B', E', \{\context[\sstageA{t}{a,c,\varsigma}P]\}\,.
\end{align*}
By Lemma~\ref{lem:validity}, these configurations are valid. Furthermore, since $B, E, \{\context[\sstage{t}P\varsigma]\}$ is valid,
$B, E', \{\context[\sstage{t}P\varsigma]\}$ is a fortiori valid, and since $\context[\sstageA{t}{a,c,\varsigma}P]$ is valid,
\[\begin{split}
&\channels{\barriers{\context[\sstageA{t}{a,c,\varsigma}P]}} \cap {}\\
&\quad \fnnobc{\context[\sstageA{t}{a,c,\varsigma}P]} = \emptyset\,,
\end{split}\]
so $\{a,c\} \cap \fnnobc{\context[\sstage{t}P\varsigma]} = \emptyset$ and the elements of multiset $\channels{\barriers{\context[\sstageA{t}{a,c,\varsigma}P]}}$ are pairwise distinct, so $\{a,c\} \cap \channels{\barriers{\context[\sstage{t}P\varsigma]}} = \emptyset$, so $\{a,c \} \cap \fn{\context[\sstage{t}P\varsigma]} = \emptyset$.
By Proposition~\ref{prop:2},
\[B, E, \{\context[\sstage{t}P\varsigma]\} \approxconfig B, E', \{\context[\sstage{t}P\varsigma]\}\,.\]
By the result shown above,
\[B, E', \{\context[\sstage{t}P\varsigma]\} \approxconfig B', E', \{\context[\sstageA{t}{a,c,\varsigma}P]\}\,,\]
so by transitivity of $\approxconfig$,
\[\Initconf{\context[\sstage{t}P\varsigma]} \approxconfig \Initconf{\context[\sstageA{t}{a,c,\varsigma}P]}\,,\]
which proves the desired result.
\end{proof}
\medskip
\begin{proof}[Proof of Proposition~\ref{prop:standard-to-annotated-all}]
Let us first show that $P'_0$ is valid.
The transformation performed by $\precompilerSymb$ preserves validity:
if $\context[\sstage{t}Q]$ is valid, then $\context[\sstageA{t}{a,c,\varsigma}Q']$ is also valid. Indeed, $\fv{\sstageA{t}{a,c,\varsigma}Q'} = \fv{\range{\varsigma}} \cup (\fv{Q'} \setminus \dom{\varsigma}) = \fv{Q'\varsigma} = \fv{Q}$ since $\fv{Q'} = \dom{\varsigma}$ by Lemma~\ref{lem:splitfinal}. Therefore, if $\context[\sstage{t}Q]$ is closed, then $\context[\sstageA{t}{a,c,\varsigma}Q']$ is also closed.
Since barriers are transformed in a top-down order, the barriers in $Q$ and $Q'$ are standard, so we have
\[\begin{split}
&\channels{\barriers{\context[\sstageA{t}{a,c,\varsigma}Q']}}\\
&{} = \{ a, c\} \cup \channels{\barriers{\context[\sstage{t}Q]}}\,.
\end{split}\]
Since $a$ and $c$ are distinct fresh names, the elements of $\channels{\barriers{\context[\sstageA{t}{a,c,\varsigma}Q']}}$ are pairwise distinct, and
\[\begin{split}
&\channels{\barriers{\context[\sstageA{t}{a,c,\varsigma}Q']}} \cap {}\\
&\quad\qquad \fnnobc{\context[\sstageA{t}{a,c,\varsigma}Q']} \\
&\quad \subseteq (\{a, c\} \cup \channels{\barriers{\context[\sstage{t}Q]}}) \cap {}\\
&\quad\qquad \fnnobc{\context[\sstage{t}Q]}\\
&\quad = \emptyset\,.
\end{split}\]
\begin{itemize}
\item
For the transformed barrier, $a$ and $c$ are fresh names, so $\context$ does not bind $a$ nor $c$ above the hole. Moreover, by Lemma~\ref{lem:splitfinal}, $\fv{Q'} \subseteq \dom{\varsigma}$ and $\context$ does not bind the names in $\fn{Q'}$ above the hole, since $\fn{Q'} = \emptyset$.
\item
For the annotated barriers that already occur in $\context[\sstage{t}Q]$, we have $\context[\sstage{t}Q] = \contextI[\sstageA{t'}{a',c',\varsigma'}Q'']$. Since barriers are transformed in a top-down order, the barriers in $Q$ are standard, so the annotated barriers in question occur in $\context$, and two cases may happen:
\begin{itemize}
\item The transformed barrier is under $t'[a',c',\varsigma']$, inside $Q''$:
\begin{align*}
\context[\sstage{t}Q] &= \contextI[\sstageA{t'}{a',c',\varsigma'}\contextII[\sstage{t}Q]]\\
\context[\sstageA{t}{a,c,\varsigma}Q'] &= \contextI[\sstageA{t'}{a',c',\varsigma'}\contextII[\sstageA{t}{a,c,\varsigma}Q']]
\end{align*}
for some context $\contextII$.
Since $\contextI[\sstageA{t'}{a',\allowbreak c',\allowbreak \varsigma'}\allowbreak \contextII[\sstage{t}Q]]$ is valid, we have
$\fv{\contextII[\sstage{t}Q]} \subseteq \dom{\varsigma'}$ and $\contextI$ does not bind $a'$, $c'$, nor the names in $\fn{\contextII[\sstage{t}Q]}$ above the hole. Furthermore, $\fv{\sstageA{t}{a,c,\varsigma}Q'} = \fv{Q} = \fv{\sstage{t}Q}$, so $\fv{\contextII[\sstageA{t}{a,c,\varsigma}Q']} \subseteq \dom{\varsigma'}$.
Moreover,
\begin{align*}
\fn{\sstageA{t}{a,c,\varsigma}Q'} &= \{a,c\} \cup \fn{Q'\varsigma}\\
&= \{a,c\} \cup \fn{Q} \\
&= \{a,c\} \cup \fn{\sstage{t}Q}\,,
\end{align*}
so $\fn{\contextII[\sstageA{t}{a,c,\varsigma}Q']} = \{a,c\} \cup \fn{\contextII[\sstage{t}Q]}$.
%\bbnote{$a$ and $c$ are not bound by $\contextII$ because they are fresh.}%
Since $a$ and $c$ are fresh, they are not bound by $\contextI$, so $\contextI$ does not bind the names in $\fn{\contextII[\sstageA{t}{a,c,\varsigma}Q']}$ above the hole.
\item The transformed barrier and the barrier $t'[a',c',\varsigma']$
are not under one another:
\begin{align*}
\context[\sstage{t}Q] &= \contextII[\sstageA{t'}{a',c',\varsigma'}Q'', \sstage{t}Q]\\
\context[\sstageA{t}{a,c,\varsigma}Q'] &= \contextII[\sstageA{t'}{a',c',\varsigma'}Q'', \sstageA{t}{a,c,\varsigma}Q']
\end{align*}
for some context $\contextII[\_,\_]$ with two holes.
Since $\contextII[\sstageA{t'}{a',c',\varsigma'}Q'', \sstage{t}Q]$ is valid,
we have $\fv{Q''} \subseteq \dom{\varsigma'}$ and $\contextII[\_,\_]$ does not bind $a'$, $c'$, nor the names in $\fn{Q''}$ above its first hole.
\end{itemize}
\end{itemize}
In all cases, $\context[\sstageA{t}{a,c,\varsigma}Q']$ is valid.
Since $P_0$ is a closed standard biprocess, it contains no annotated barrier, hence it is valid. We can then conclude that $P'_0 = \precompiler{P_0}$ is valid as well.
From an annotated biprocess $P'_0 = \precompiler{P_0}$, we can rebuild $P_0$ by replacing each occurrence of an annotated barrier $\sstageA{t}{a,c,\varsigma}Q$ with $Q\varsigma$, by Lemma~\ref{lem:splitfinal}. Therefore, we can also rebuild $\fst{P_0}$ from $\fst{P'_0}$ by replacing each occurrence of an annotated barrier $\sstageA{t}{a,c,\varsigma}Q$ (in $\fst{P'_0}$) with $Q\varsigma$. Furthermore, since validity is preserved by application of $\fstSymb$ (Lemma~\ref{lem:validity}), the considered processes are valid.
Hence by applying several times Proposition~\ref{prop:standard-to-annotated-one} and by transitivity of $\approx$, we obtain that $\fst{P'_0} \approx \fst{P_0}$. We obtain $\snd{P'_0} \approx \snd{P_0}$ symmetrically.
\end{proof}
\subsection{Barrier elimination commutes with renaming and substitution}\label{app:renaming}\label{app:substNames}\label{app:substTerms}
\begin{figure}
\[
\begin{array}{@{}l@{\;}c@{\;}l@{}}
\compilerI{\nill} &=& \nill\\
\compilerI{Q \mid R} &=& \compilerI{Q} \mid \compilerI{R}\\
\compilerI{!Q} &=&!\compilerI{Q} \\
\compilerI{\new{n}.Q} &=& \new{n}.\compilerI{Q}\\
\compilerI{\In[M]{x}.Q} &=& \In[M]{x}.\compilerI{Q}\\
\compilerI{\Out[M]{N}.Q}\qquad \null &=& \Out[M]{N}.\compilerI{Q}\\
\multicolumn{3}{@{}l@{}}{ \compilerI{\Letinelse{x}{D}{Q}R} ={}}\\
\multicolumn{3}{@{}l@{}}{\qquad \Letinelse{x}{D}{\compilerI{Q}} \compilerI{R}}\\
\multicolumn{3}{@{}l@{}}{ \compilerI{\sstageA{t}{a,c,(\subst{M_1}{z_1}, \dots, \subst{M_n}{z_n})}Q}={}}\\
\multicolumn{3}{@{}l@{}}{\qquad \Out[a]{\tuple{M_1,\dots,M_n}}.\In[c]{z}.\Letin{z_1}{\projnew 1 n z} \cdots}\\
\multicolumn{3}{@{}l@{}}{\qquad \Letin{z_n}{\projnew n n z} \compilerI{Q}}\\
\multicolumn{3}{@{}l@{}}{\qquad \textrm{where $z$ is a fresh variable}}
\end{array}
\]
\caption{Definition of $\compilerSymb$}
\label{fig:def:compiler}
\end{figure}
Our operational semantics uses renaming of names and substitution of
terms for variables (implicitly, this includes renaming of
variables). The next lemma proves that $\compilerSymb$ preserves
renaming of names and substitution of terms for variables.
In this lemma, we use the formal definition of $\compilerSymb$
by induction on the syntax, given in Figure~\ref{fig:def:compiler}.
\begin{lemma}\label{lem:substIbb}\label{lem:substIIb}
Given an annotated process $P$ and substitution or renaming $\sigma$,
we have $\compilerI{P}\sigma = \compilerI{P\sigma}$.
\end{lemma}
\begin{figure}
\[
\begin{array}{l}
\compilerI{!Q}\sigma \\
\quad= {(!\compilerI{Q})\sigma} \\
\quad= {!(\compilerI{Q}\sigma)} \\
\quad= {!\compilerI{Q\sigma}} \\
\quad= \compilerI{!(Q\sigma)} \\
\quad= \compilerI{(!Q)\sigma} \\[1em]
%
%%%%%
%
\compilerI{\new{n}.Q}\sigma \\
\quad= (\new{n}.\compilerI{Q})\sigma \\%&&\textrm{by definition of $\compilerISymb$} \\
\quad= \new{n'}.(\compilerI{Q}\activesubst{n'}{n}\sigma)\\%&&\textrm{by application of $\sigma$} \\
\quad= \new{n'}.(\compilerI{Q\activesubst{n'}{n}}\sigma)\\%&&\textrm{by Lemma~\ref{lem:substIbb}} \\
\quad= \new{n'}.\compilerI{Q\activesubst{n'}{n}\sigma}\\%&&\textrm{by induction hypothsis} \\
\quad= \compilerI{\new{n'}.(Q\activesubst{n'}{n}\sigma)}\\%&&\textrm{by definition of $\compilerISymb$} \\
\quad= \compilerI{(\new{n}.Q)\sigma}\\[1em]%&&\textrm{by application of $\sigma$}
%
%%%%%
%
\compilerI{\In[M]{x}.Q}\sigma \\
\quad= (\In[M]{x}.\compilerI{Q})\sigma \\% &&\textrm{by definition of $\compilerISymb$}\\
\quad= \In[M\sigma]{x'}.(\compilerI{Q}\activesubst{x'}{x}\sigma) \\% &&\textrm{by application of $\sigma$} \\
\quad= \In[M\sigma]{x'}.\compilerI{Q\activesubst{x'}{x}\sigma} \\% &&\textrm{by induction hypothsis}\\
\quad= \compilerI{\In[M\sigma]{x'}.(Q\activesubst{x'}{x}\sigma)} \\% &&\textrm{by definition of $\compilerISymb$}\\
\quad= \compilerI{(\In[M]{x}.Q)\sigma} \\[1em]%&&\textrm{by application of $\sigma$} \\
%
%%%%%
%
\compilerI{\Out[M]{N}.Q}\sigma \\
\quad= (\Out[M]{N}.\compilerI{Q})\sigma \\
\quad= \Out[M]{N}\sigma.\compilerI{Q}\sigma \\
\quad= \Out[M]{N}\sigma.\compilerI{Q\sigma} \\
\quad= \compilerI{\Out[M]{N}\sigma.Q\sigma} \\
\quad= \compilerI{(\Out[M]{N}.Q)\sigma} \\[1em]
%
\compilerI{\sstageA{t}{a,c,(\subst{M_1}{z_1}, \dots, \subst{M_n}{z_n} )}Q}\sigma \\
\quad= (\Out[a]{\tuple{M_1,\dots,M_n}}.\In[c]{z}.\Letin{z_1}{\projnew{1}{n}{z}} \dots \\
\quad\phantom{= (} \Letin{z_n}{\projnew{n}{n}{z}}\compilerI{Q})\sigma \\
\quad= \Out[a]{\tuple{M_1\sigma,\dots,M_n\sigma}}.\In[c]{z}.\Letin{z'_1}{\projnew{1}{n}{z}} \dots\\
\quad\phantom{= {}} \Letin{z'_n}{\projnew{n}{n}{z}}\compilerI{Q}\{\subst{z'_1}{z_1},\dots,\subst{z'_n}{z_n}\}\sigma \\
\quad= \Out[a]{\tuple{M_1\sigma,\dots,M_n\sigma}}.\In[c]{z}.\Letin{z'_1}{\projnew{1}{n}{z}} \dots\\
\quad\phantom{= {}} \Letin{z'_n}{\projnew{n}{n}{z}}\compilerI{Q\{\subst{z'_1}{z_1},\dots,\subst{z'_n}{z_n}\}\sigma} \\
\quad= \compilerI{\sstageA{t}{a,c,(\subst{M_1\sigma}{z'_1}, \dots, \subst{M_n\sigma}{z'_n} )}\\
\quad\phantom{= \delta(} Q\{\subst{z'_1}{z_1},\dots,\subst{z'_n}{z_n}\}\sigma} \\
\quad= \compilerI{(\sstageA{t}{a,c,(\subst{M_1}{z_1}, \dots, \subst{M_n}{z_n} )}Q)\sigma} \\[1em]
%
%%%%%
%
\compilerI{\Letinelse{x}{D}{Q}R}\sigma \\
\quad= (\Letinelse{x}{D}{\compilerI{Q}}\compilerI{R})\sigma \\
% &&\textrm{by definition of $\compilerISymb$}\\
\quad = \Letinelse{x'}{D\sigma}{\compilerI{Q}\activesubst{x'}{x}\sigma}\\
\phantom{\quad ={}}\compilerI{R}\sigma \\
% &&\textrm{by application of $\sigma$} \\
\quad= \Letinelse{x'}{D\sigma}{\compilerI{Q\activesubst{x'}{x}\sigma}}\\
\phantom{\quad ={}}\compilerI{R\sigma} \\
% &&\textrm{by induction hypothesis}\\
\quad= \compilerI{\Letinelse{x'}{D\sigma}{Q\activesubst{x'}{x}\sigma}R\sigma} \\
% &&\textrm{by definition of $\compilerISymb$}\\
\quad= \compilerI{(\Letinelse{x}{D}{Q}R)\sigma} \\[1em]
% &&\textrm{by application of $\sigma$}
%
%%%%%
%
\compilerI{Q \mid R}\sigma \\
\quad= (\compilerI{Q} \mid \compilerI{R}) \sigma \\
\quad= \compilerI{Q}\sigma \mid \compilerI{R} \sigma \\
\quad= \compilerI{Q\sigma} \mid \compilerI{R \sigma} \\
\quad= \compilerI{Q\sigma \mid R \sigma} \\
\quad= \compilerI{(Q \mid R) \sigma}
\end{array}
\]
\caption{Derivations for the inductive case of Lemma~\ref{lem:substIIb}}
\label{fig:substIIb}
\end{figure}
\begin{proof}
Let us proceed by structural induction on $P$. In the base case,
we derive
$
\compilerI{0}\sigma
= 0\sigma
= 0
= \compilerI{0}
= \compilerI{0\sigma}
$ by definition of $\compilerISymb$ and
application of $\sigma$.
The inductive cases (Figure~\ref{fig:substIIb}) additionally
apply the induction hypothesis.
In Figure~\ref{fig:substIIb},
we assume name $n'$ is fresh in the name restriction case; variable $x'$ is fresh in the input and expression evaluation cases; variables $z, z'_1, \dots, z'_n$ are fresh in the barrier case. We rename bound names and variables to fresh names and variables respectively, to avoid any name or variable capture.
\end{proof}
\subsection{Barrier elimination preserves reduction}\label{app:reduction}
Reduction captures the dynamic behaviour of a process with respect to control flow and communication. In this section, we build upon Lemma~\ref{lem:substIbb} to show that function $\compilerISymb$ preserves reduction, in cases in which barriers are not reduced.
\begin{lemma}\label{lem:red}
Suppose $B$ is a finite set of annotated barriers, $E$ is a finite set of names and $\Pcal,\Qcal,\Qcal'$ are finite multisets of processes such that $\barriers{\Qcal'} = \emptyset$.
Further suppose that $\Conf = B, E, \Qcal \cup \Pcal$ is a valid configuration.
Let $\Conf' = \emptyset, E,\Qcal' \cup\compiler{\Pcal}$.
We have the following properties:
\begin{enumerate}
\item\label{prop1} If $\Conf \reduc \Conf_1$ by reducing one or more processes in $\Pcal$ such that $\Conf_1 = B, E_1, \Qcal\cup \Pcal_1$
for some set of names $E_1$ and multiset of processes $\Pcal_1$, then
$\Conf' \reduc \Conf'_1$, where $\Conf'_1 = \emptyset, E_1,\Qcal' \cup\compiler{\Pcal_1}$.
\item\label{prop2} If $\Conf' \reduc \Conf'_1$ by reducing one or more processes in $\compiler{\Pcal}$ such that $\Conf'_1 = \emptyset, E_1,\Qcal' \cup \Pcal'_1$ for some set of names $E_1$ and multiset of processes $\Pcal'_1$, then there exists a multiset of processes $\Pcal_1$ such that
$\Pcal'_1 = \compiler{\Pcal_1}$ and $\Conf \reduc \Conf_1$, where $\Conf_1 = B, E_1, \Qcal\cup \Pcal_1$.
\end{enumerate}
\end{lemma}
\begin{proof}
Suppose configurations $\Conf$, $\Conf'$, $\Conf_1$ and $\Conf'_1$ are given above. We proceed by case analysis of our reduction rules. First, we consider Property~\ref{prop1}.
\begin{description}
\item[$\RNil$] In this case, $\Pcal = \Pcal_1 \cup \{0\}$ and $E = E_1$. It follows that $\compiler{\Pcal} = \compiler{\Pcal_1} \cup \{0\}$, hence, $\Conf'\reduc\Conf_1'$.
\item[$\RRepl$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal_0$ and a process $R$ such that $\Pcal = \Pcal_0 \cup \{!R\}$ and $\Pcal_1 = \Pcal_0 \cup \{R,!R\}$.
%%It follows that $\compiler{\Pcal} = \{!R\} \cup \compiler{\Pcal_0}$.
%%Since barriers under replication are forbidden (\S\ref{sec:syntax}),
%%we have $R$ does not contain barriers and, therefore, $\compiler{R} = R$.
It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\compiler{!R}\}$ and
$\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R},\compiler{!R}\}$.
Moreover, since $\compiler{!R} = {!\compiler{R}}$, we have $\Conf' \reduc \Conf_1'$.
\item[$\RPar$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal_0$ and processes $R$ and $R'$ such that $\Pcal = \Pcal_0 \cup \{R \mid R'\}$ and $\Pcal_1 = \Pcal_0 \cup \{R,R'\}$. It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\compiler{R} \mid \compiler{R'}\}$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R}, \compiler{R'}\}$, hence, $\Conf' \reduc \Conf_1'$.
\item[$\RRes$] In this case, there exist a multiset of processes $\Pcal_0$,
a process $R$ and names $n$ and $n'$ such that $\Pcal = \Pcal_0 \cup \{\new{n}.R\}$,
$E_1 = E \cup \{n'\}$ and $\Pcal_1 = \Pcal_0 \cup \{R\activesubst{n'}{n}\}$,
where $n'\not\in E \cup \fn{\Pcal}$.
It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\new{n}.\compiler{R}\}$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R\activesubst{n'}{n}}\}$.
We have $\compiler{R\activesubst{n'}{n}} = \compiler{R}\activesubst{n'}{n}$ by \Cref{lem:substIbb},
hence, $\Conf'\rightarrow\Conf'_1$.
\item[$\RIO$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal_0$, processes $R$ and $R'$, terms $M$ and $N$, and a variable $x$ such that $\Pcal = \Pcal_0 \cup \{\Out[N]{M}.R, \In[N]{x}.R'\}$ and $\Pcal_1 = \Pcal_0 \cup \{R,R'\activesubst{M}{x}\}$. It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\Out[N]{M}.\compiler{R}, \In[N]{x}.\compiler{R'}\}$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R}, \compiler{R'\activesubst{M}{x}}\}$.
Moreover, we have $\compiler{R'\activesubst{M}{x}} = \compiler{R'}\activesubst{M}{x}$ by \Cref{lem:substIIb},
hence, $\Conf'\rightarrow\Conf'_1$.
\item[$\RDestrI$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal_0$, processes $R$ and $R'$, an expression $D$, a term $M$, and a variable $x$ such that $\Pcal = \Pcal_0 \cup \{\Letinelse{x}{D}{R}R'\}$ and $\Pcal_1 = \Pcal_0 \cup \{R\activesubst{M}{x}\}$, where $D\Downarrow M$.
It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\Letinelse{x}{D}{\compiler{R}}\compiler{R'}\}$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R\activesubst{M}{x}}\}$.
Moreover, we have $\compiler{R\activesubst{M}{x}} = \compiler{R}\activesubst{M}{x}$ by \Cref{lem:substIIb},
hence, $\Conf'\rightarrow\Conf'_1$.
\item[$\RDestrII$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal_0$, processes $R$ and $R'$, an expression $D$, and a variable $x$ such that $\Pcal = \Pcal_0 \cup \{\Letinelse{x}{D}{R}R'\}$ and $\Pcal_1 = \Pcal_0 \cup \{R'\}$, where there is no $M$ such that $D\Downarrow M$. It follows that $\compiler{\Pcal} = \compiler{\Pcal_0} \cup \{\Letinelse{x}{D}{\compiler{R}}\compiler{R'}\}$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{R'}\}$, hence, $\Conf' \reduc \Conf_1'$.
\item[$\RBarII$] By inspection of our reduction rules, the reduction $\Conf \reduc \Conf_1$ cannot apply $\RBarII$, since $B$ remains constant in the configurations $\Conf$ and $\Conf_1$.
\end{description}
\noindent Secondly, we consider Property~\ref{prop2}.
\begin{description}
\item[$\RNil$] In this case, $E = E_1$, $0\in\compiler{\Pcal}$, and $\Pcal'_1 = \compiler{\Pcal} \backslash\{0\}$. By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), it follows immediately that $0\in\Pcal$ and hence $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$ and $\Pcal_1 = \Pcal\backslash\{0\}$. Moreover, since $\compiler{0} = 0$, we have $\Pcal'_1 = \compiler{\Pcal_1}$.
\item[$\RRepl$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal'_0$ and a process $R$ such that $\compiler{\Pcal} = \Pcal'_0 \cup \{!R\}$ and $\Pcal'_1 = \Pcal'_0 \cup \{R,{!R}\}$.
So there are $\Pcal_0$ and $R_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$ and $!R = \compiler{R_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}),
there exists a process $\hat R$ such that $\compiler{\hat R} = R$ and $R_0 = !\hat R$, so
$\Pcal = \Pcal_0 \cup \{!\hat R\}$.
Let $\Pcal_1 = \Pcal_0 \cup \{\hat R, {! \hat R}\}$.
It follows immediately that $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$ and $\Pcal'_1 = \compiler{\Pcal_1}$.
\item[$\RPar$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal'_0$ and processes $R$ and $R'$ such that $\compiler{\Pcal} = \Pcal'_0 \cup \{R \mid R'\}$ and $\Pcal'_1 = \Pcal'_0 \cup \{R,R'\}$.
So there are $\Pcal_0$ and $R_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$ and $R \mid R' = \compiler{R_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), there exist processes $\hat R$ and $\hat R'$ such that $\compiler{\hat R} = R$, $\compiler{\hat R'} = R'$, and $R_0 = \hat R \mid \hat R'$,
so $\Pcal = \Pcal_0 \cup \{\hat R \mid \hat R'\}$. Let $\Pcal_1 = \Pcal_0 \cup \{\hat R,\hat R'\}$. It follows immediately that $\Pcal'_1 = \compiler{\Pcal_1}$ and $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$.
\item[$\RRes$] In this case, there exist a multiset of processes $\Pcal'_0$,
a process $R$ and names $n$ and $n'$ such that $E_1 = E \cup \{n'\}$,
$\compiler{\Pcal} = \Pcal'_0 \cup \{\new{n}.R\}$,
and $\Pcal'_1 = \Pcal'_0 \cup \{R\activesubst{n'}{n}\}$,
where $n'\not\in E \cup \fn{\Pcal'_0 \cup \{\new{n}.R\}}$.
So there are $\Pcal_0$ and $R_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$ and $\new{n}.R = \compiler{R_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), there exists
a process $\hat R$ such that $R = \compiler{\hat R}$ and $R_0 = \new{n}.\hat R$,
so $\Pcal = {\Pcal_0} \cup \{\new n.\hat R\}$.
Let $\Pcal_1 = \Pcal_0 \cup \{\hat R\activesubst{n'}{n}\}$.
It follows that $\Conf \reduc \Conf_1$ and $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{\hat R\activesubst{n'}{n}}\}$.
Moreover, we have $\Pcal'_1 = \compiler{\Pcal_1}$ by \Cref{lem:substIbb}.
\item[$\RIO$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal'_0$, processes $R$ and $R'$, terms $M$ and $N$, and a variable $x$ such that $\compiler{\Pcal} = \Pcal'_0 \cup \{\Out[N]{M}.R, \allowbreak \In[N]{x}.R'\}$ and $\Pcal'_1 = \Pcal'_0 \cup \{R,R'\activesubst{M}{x}\}$.
So there are $\Pcal_0$, $R_0$, and $R'_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0, R'_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$, $\Out[N]{M}.R = \compiler{R_0}$,
and $\In[N]{x}.R' = \compiler{R'_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), $\In[N]{x}.R' = \compiler{R'_0}$ implies $\In[N]{x}.\hat R' = R'_0$ for some process $\hat R'$ such that $\compiler{\hat R'} = R'$.
Moreover, $\Out[N]{M}.R = \compiler{R_0}$ implies: 1) there exists a process $\hat R$ such that $R_0 = \Out[N]{M}.\hat R$, where $\compiler{\hat R} = R$; or
2) $N$ is a name and there exist a barrier $t$, name $c$, ordered substitution $\varsigma$, process $R''$, variable $z$, and integer $n$, such that $R_0 = \sstageA{t}{N,c,\varsigma}R''$, and $R = \In[c]{z}.\Letin{z_1}{\projnew 1 n z} \cdots\ \Letin{z_n}{\projnew n n z}\compilerI{R''}$.
In the first case,
$\Pcal = \Pcal_0 \cup \{\Out[N]{M}.\hat R, \In[N]{x}.\hat R'\}$.
Let $\Pcal_1 = \Pcal_0 \cup \{\hat R, \hat R'\activesubst{M}{x}\}$. It follows that $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$.
Moreover, we have $\compiler{\hat R'\activesubst{M}{x}} = \compiler{\hat R'}\activesubst{M}{x}$ by \Cref{lem:substIIb}, hence, $\Pcal'_1 = \compiler{\Pcal_1}$.
We show that the second case cannot arise.
Since $N$ is a name, we have $N \in \fnnobc{\In[N]{x}.\hat R'} = \fnnobc{R'_0} \subseteq \fnnobc{\Qcal \cup \Pcal}$. Furthermore,
$N \in \channels{\barriers{\sstageA{t}{N,c,\varsigma}R''}} = \channels{\barriers{R_0}} \subseteq \channels{\barriers{\Qcal\cup \Pcal}}$ and
since $\Conf$ is a valid configuration, we have
$\channels{\barriers{\Qcal\cup \Pcal}} \cap \fnnobc{\Qcal\cup \Pcal} = \emptyset$, thereby deriving a contradiction.
\item[$\RDestrI$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal'_0$, processes $R$ and $R'$, an expression $D$, a term $M$, and a variable $x$ such that $\compiler{\Pcal} = \Pcal'_0 \cup \{\Letinelse{x}{D}{R}{R'}\}$ and $\Pcal'_1 = \Pcal'_0 \cup \{R\activesubst{M}{x}\}$, where $D\Downarrow M$.
So there are $\Pcal_0$ and $R_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$ and $\Letinelse{x}{D}{R}{R'} = \compiler{R_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), there exist
processes $\hat R$ and $\hat R'$ such that
$\compiler{\hat R} = R$, $\compiler{\hat R'} = R'$, and
$R_0 = \Letinelse{x}{D}{\hat R}{\hat R'}$, so
$\Pcal = \Pcal_0 \cup \{\Letinelse{x}{D}{\hat R}{\hat R'}\}$.
Let $\Pcal_1 = \Pcal_0 \cup \{\hat R\activesubst{M}{x}\}$. It follows that $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$.
Moreover, we have $\compiler{\Pcal_1} = \compiler{\Pcal_0} \cup \{\compiler{\hat R\activesubst{M}{x}}\}$.
Furthermore, we have $\compiler{\hat R\activesubst{M}{x}} = \compiler{\hat R}\activesubst{M}{x}$ by \Cref{lem:substIIb}, hence, $\Pcal'_1 = \compiler{\Pcal_1}$.
\item[$\RDestrII$] In this case, $E = E_1$ and there exist a multiset of processes $\Pcal'_0$, processes $R$ and $R'$, an expression $D$, and a variable $x$ such that $\compiler{\Pcal} = \Pcal'_0 \cup \{\Letinelse{x}{D}{R}{R'}\}$ and $\Pcal'_1 = \Pcal'_0 \cup \{R'\}$, where there is no $M$ such that $D\Downarrow M$.
So there are $\Pcal_0$ and $R_0$ such that
$\Pcal = \Pcal_0 \cup \{R_0\}$ with $\Pcal'_0 = \compiler{\Pcal_0}$ and $\Letinelse{x}{D}{R}{R'} = \compiler{R_0}$.
By definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}), there exist
processes $\hat R$ and $\hat R'$ such that
$\compiler{\hat R} = R$, $\compiler{\hat R'} = R'$, and
$R_0 = \Letinelse{x}{D}{\hat R}{\hat R'}$, so
$\Pcal = \Pcal_0 \cup \{\Letinelse{x}{D}{\hat R}\hat R'\}$.
Let $\Pcal_1 = \Pcal_0 \cup \{\hat R'\}$. It follows immediately that $\Pcal'_1 = \compiler{\Pcal_1}$ and $\Conf \reduc \Conf_1$, where $\Conf_1 = B,E_1,\Qcal \cup \Pcal_1$.
\item[$\RBarII$] By definition of $\compilerSymb$, configuration $\Conf'$ does not contain barriers and therefore we do not consider applications of the rule $\RBarII$.\qedhere
\end{description}
\noqed
\end{proof}
\noindent \Cref{lem:red} will be used in the following section to prove Proposition~\ref{prop:soundnessSwapping}.
\subsection{Proof of Proposition~\ref{prop:preserve-compil-second}}\label{app:prop:soundnessSwapping}
We introduce some rudimentary results (\Cref{lem:outputCh,lem:addlets,lem:valid-no-fn}), before proving the main technical result (Proposition~\ref{prop:soundnessSwapping}), which leads to Proposition~\ref{prop:preserve-compil-second}. An \emph{annotated configuration} is a configuration in which all processes are annotated.
\begin{lemma} \label{lem:outputCh}
Suppose $\Conf = B,E,\Pcal$ is a valid annotated configuration such that
$\compiler{P} = \Out[N]{M}.Q$ for some processes $P \in \Pcal$ and $Q$, and terms $M$ and $N$, where $\fn{N}\cap E = \emptyset$. We have $\Conf\downarrow_N$.
\end{lemma}
\begin{proof}
By definition of $\compilerSymb$, either: 1) $P = \Out[N]{M}.R\in \Pcal$ for some process $R$ such that $\compiler{R} = Q$; or 2) $P = \sstageA{t}{N,c,\varsigma}R\in \Pcal$ for some barrier $t$, channel name $c$, ordered substitution $\varsigma$, and process $R$. In the first case, it follows immediately that $\Conf\downarrow_N$. We show that the second case cannot arise. By definition of a valid configuration (Definition~\ref{def:validity}), $\channels{\barriers{\Pcal}} \subseteq E$, so $N \in E$, which contradicts the assumption $\fn{N}\cap E = \emptyset$.
\end{proof}
We define
\begin{align*}
&\addLets{Q} = \Biggl\{
\begin{array}{l}
\Letin{z_j}{\projnew{j}{n}{\tuple{M_1, \dots, M_n}}} \cdots\\
\Letin{z_n}{\projnew{n}{n}{\tuple{M_1, \dots, M_n}}}Q'
\end{array}\\
&\quad \mathrel{\Bigg|}
\begin{array}{l}
1 \leq j \leq n, Q = Q'\{\subst{M_j}{z_j}, \dots, \subst{M_n}{z_n}\},\\
M_1, \ldots, M_n \text{ ground terms}, \\
z_j, \dots, z_n \text{ pairwise distinct variables}
\end{array}
\Biggr\} \cup \{ Q \}
\end{align*}
\begin{lemma}\label{lem:addlets}
Let $Q' \in \addLets{Q}$ and $B, E, \Pcal \cup \{Q'\}$ be a valid configuration.
We have $B, E, \Pcal \cup \{Q'\} \reduc^* B, E, \Pcal \cup \{ Q\}$. Furthermore, if $Q' \neq Q$
and $B, E, \Pcal \cup \{Q'\} \reduc B, E, \Pcal \cup \{Q''\}$ by reducing $Q'$, then $Q'' \in \addLets{Q}$.
\end{lemma}
\begin{proof}
If $Q' = Q$, then we have obviously $B, E, \Pcal \cup \{Q'\} \reduc^* B, E, \Pcal \cup \{ Q\}$,
with no reduction.
Otherwise,
\[\begin{split}
Q' = {}&\Letin{z_j}{\projnew{j}{n}{\tuple{M_1, \dots, M_n}}} \cdots\\
&\Letin{z_n}{\projnew{n}{n}{\tuple{M_1, \dots, M_n}}}Q_1
\end{split}\]
where $Q = Q_1\{\subst{M_j}{z_j}, \dots, \subst{M_n}{z_n}\}$, $M_1, \ldots, M_n$ are ground terms,
$z_j, \dots, z_n$ are pairwise distinct variables, and $1 \leq j \leq n$.
Then $B, E, \Pcal \cup \{Q'\} \reduc^* B, E, \Pcal \cup \{ Q\}$ by $n-j+1$ applications of $\RDestrI$.
If $B, E, \Pcal \cup \{Q'\} \reduc B, E, \Pcal \cup \{Q''\}$ by reducing $Q'$, then this reduction is obtained
by one application of $\RDestrI$, so
\[\begin{split}
Q'' = {}&\Letin{z_{j+1}}{\projnew{j+1}{n}{\tuple{M_1, \dots, M_n}}} \cdots\\
& \Letin{z_n}{\projnew{n}{n}{\tuple{M_1, \dots, M_n}}}Q_2
\end{split}\]
where $Q_2 = Q_1\{\subst{M_j}{z_j}\}$, so
\begin{align*}
Q & = Q_1\{\subst{M_j}{z_j}, \dots, \subst{M_n}{z_n}\}\\
& = Q_2\{\subst{M_{j+1}}{z_{j+1}}, \dots, \subst{M_n}{z_n}\}\,.
\end{align*}
If $jt$;}\\
\quad\textrm{$f$ is a permutation of $\{1,\dots,n\}$ such that,}\\
\quad\textrm{for all $1 \leq l \leq n$, we have $Q_l/\tup{z}_l \eqren Q_{f(l)}/\tup{z}_{f(l)}$}\\
\quad\textrm{$R \in \synchoneside{B'}$;}\\
\quad\textrm{and $x_1, \dots, x_n$ are pairwise distinct variables}\big\}\\
\textrm{if $B \neq \emptyset$}
\end{array}
\end{align*}}%
%\bbnote{$\compilerInI{\sstageA{t}{a,c,\varsigma}Q}$ could be a single process rather than a set.}%
Let us consider the
smallest relations $\Rel_1$, $\Rel_2$ and $\Rel_3$ between configurations such that the conditions
below are satisfied.
\begin{enumerate}
\item Suppose that $B, E, \Pcal \cup \Qcal$ is a valid annotated configuration,
$\Pcal = \{P_1, \allowbreak \dots, \allowbreak P_m\}$,
$\Qcal = \{\sstageA{t}{a_1,c_1,\varsigma_1}Q_1,\allowbreak \dots,\allowbreak \sstageA{t}{a_k,c_k,\varsigma_k}Q_k\}$,
$\varsigma_l = (\subst{M_{l,1}}{z_{l,1}},\allowbreak \dots,\allowbreak \subst{M_{l,|\varsigma_l|}}{z_{l,|\varsigma_l|}})$ for all $l \leq k$,
$B = \{\sstageA{t}{a_1,c_1,\tup{z}_1}Q_1,\allowbreak \dots,\allowbreak \sstageA{t}{a_n,c_n,\tup{z}_n}Q_n\} \cup B'$,
$t' > t$ for all $\sstageA{t'}{a',c',\tup{z}'}Q' \in B'$, and
$\tup{z}_{l} = (z_{l,1}, \dots, z_{l,|\tup{z}_{l}|})$ for all $l \leq n$.
Finally, suppose $f$ is a permutation of $\{1,\dots,n\}$ such that,
for all $1\leq l \leq n$, we have $Q_l/\tup{z}_l \eqren Q_{f(l)}/\tup{z}_{f(l)}$.
Let $\Pcal' = \{P'_1, \dots, P'_m\}$ and $\Qcal' = \{Q'_1, \dots, Q'_k\}$,
where $P'_i \in \compilerLets{P_i}$ for all $i \leq m$ and
$Q'_i \in \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i}$ for all $i \leq k$.
We have
\[
\Big( B,E,\Pcal \cup \Qcal\Big) \Rel_1
\Big(\emptyset, E,\Pcal' \cup \Qcal' \cup \{R\} \Big)
\]
where
\[
\begin{split}
R &{} \in \Biggl\{\begin{array}{l}
\In[a_{k+1}]{x_{k+1}}\mathrel.\cdots\mathrel.\In[a_n]{x_n}\mathrel.\\
\Out[c_{1}]{ {N_{f(1)}}}\mathrel.\cdots\mathrel.\Out[c_n]{{N_{f(n)}}}\mathrel.R'
\end{array}\\
&\Bigg|\begin{array}{l@{}}
\textrm{$N_{l} = \tuple{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}$ for all $l\leq k$;}\\
\textrm{$N_{l} = x_l$ for all $l > k$; $R' \in \synchoneside{B'}$; and} \\
\textrm{variables $x_{k+1},\allowbreak\dots,\allowbreak{}x_n$ are pairwise distinct}
\end{array}\Biggr\}
\end{split}\]
\subsubsection*{Remark} Configuration $\Conf = B,E,\Pcal \cup \Qcal$ is
waiting to synchronise at barrier $t$ and
configuration $\Conf' = \emptyset, E,\Pcal' \cup \Qcal' \cup \{R\}$
represents an encoding of such a synchronisation with swapping.
Multiset $\Qcal$ contains $k$ processes that are ready to synchronise at barrier $t$, while $n$ processes are needed for the synchronisation to take place.
The multiset $\Pcal$ may contain other processes that will synchronise at barrier $t$.
%
In the configuration $\Conf'$, the communications that implement the
barrier $t$ are partly done: the $k$ processes in $\Qcal'$,
corresponding to the $k$ processes in $\Qcal$, have output messages on
private channels and are awaiting input on private channels, i.e., the
processes are ready to synchronise at $t$. Process $R$ has received
$k$ private channel inputs and is awaiting for a further $n-k$ private
inputs; once all inputs have been received, process $R$ will respond
to all processes waiting to synchronise.
\item Suppose $B, E, \Pcal \cup \Qcal$ is a valid annotated configuration,
such that $\Pcal = \{P_1, \dots, P_m\}$ and $\Qcal = \{Q_1, \dots, Q_k\}$.
Let $\Pcal' = \{P'_1, \ldots, P'_m\}$ and $\Qcal' = \{Q'_1, \dots, Q'_k\}$,
where $P'_i \in \compilerLets{P_i}$ for all $i \leq m$, and
$Q'_i \in \compilerIn{\Out[c_i]{M_i}}{Q_i}$ for all $i \leq k$,
for some pairwise distinct names $c_1, \dots, c_k$ in $E \setminus \fn{\Pcal \cup \Qcal}$, and some
ground tuples $M_1, \dots, M_k$.
We have
\[
\Big( B,E,\Pcal \cup \Qcal\Big) \Rel_2
\Big(\emptyset, E,\Pcal' \cup \Qcal' \cup \{ R\}\Big)
\]
where $R \in \{\Out[c_1]{M_1}\mathrel.\cdots\mathrel.\Out[c_k]{M_k}\mathrel.R' \mid R' \in \synchoneside{B} \}$.
\subsubsection*{Remark} Configuration $\Conf = B,E,\Pcal \cup \Qcal$
has just synchronised and configuration $\Conf' = \emptyset, E, \Pcal' \cup \Qcal' \cup \{R\}$ represents an encoding of such a synchronisation with swapping.
When $k > 0$, the communications that implement the last barrier upon which synchronisation happened are not fully done yet: $k$ outputs remain in $R$, and correspondingly $\Qcal'$ contains $k$ processes ready to receive these outputs.
\item Suppose $\Pcal = \{P_1, \ldots, P_m\}$ is a multiset of processes such that $\barriers{\Pcal} = \emptyset$,
and $E$ is a set of names. Let $\Pcal' = \{P'_1, \dots, P'_m\}$ be a multiset of processes, where $P'_i \in \addLets{P_i}$ for all $i \leq m$. We have:
\[
\Big(\emptyset, E, \Pcal\Big) \Rel_3 \Big(\emptyset, E, \Pcal'\Big)
\]
\end{enumerate}
\noindent Let ${\Rel} = {\Rel_1 \cup \Rel_2 \cup \Rel_3 \cup \Rel_1^{-1} \cup \Rel_2^{-1} \cup \Rel_3^{-1}}$.
\subsubsection*{Relation $\Rel$ relates $\fst{\Conf_0}$ with $\fst{\Conf'_0}$ and $\snd{\Conf_0}$ with $\snd{\Conf'_0}$}
Recall that $\Conf_0 = B_0,E,\{P_0\}$ and
$\Conf'_0 = \emptyset, E,\{\compiler{P_0}, R_0\}$,
where $B_0 = \barriers{P_0}$, $E = \channels{B_0}$, and $R_0\in\synch{B_0}$.
By Lemma~\ref{lem:validity}, $\Conf_0 = \Initconf{P_0}$ is valid, so
$\fst{\Conf_0}$ and $\snd{\Conf_0}$ are valid.
We notice that, if $R_0 \in \synch{B_0}$, then $\fst{R_0} \in \synchoneside{\fst{B_0}}$, using the identity function for $f$,
and $\snd{R_0} \in \synchoneside{\snd{B_0}}$, using the same function $f$ as in the computation of $R_0 \in \synch{B_0}$.
Hence we have $\fst{\Conf_0}\Rel_2\fst{\Conf'_0}$ with
$B = \fst{B_0}$, $k = 0$,
$\Pcal = \{\fst{P_0}\}$,
$\Pcal' = \compiler{\Pcal}$,
$\Qcal' = \Qcal = \emptyset$,
$R = \fst{R_0}$,
and $\snd{\Conf_0} \Rel_2 \snd{\Conf'_0}$ similarly using $\sndSymb$ instead of $\fstSymb$.
\subsubsection*{Relation $\Rel$ satisfies the conditions of Definition~\ref{def:proverif:obs}}
The relation $\Rel$ is symmetric and it remains to show that $\Rel$ satisfies the three conditions of Definition~\ref{def:proverif:obs}. Let us first introduce the
following results about our relation.
\begin{fact}\label{fact:extraSteps}
Given configurations $\Conf = B,E,\Pcal \cup \Qcal$ and
$\Conf'$
such that $\Conf \Rel_2 \Conf'$, we have
$\Conf' \reduc^* \emptyset, E, \compiler{\Pcal\cup\Qcal} \cup \{ R' \}$,
where $R' \in \synchoneside{B}$.
\end{fact}
\begin{proof}[Proof of Fact~\ref{fact:extraSteps}]\noqed
We use the notations of the definition of $\Rel_2$.
We transform $\Conf'$ by applying {\RIO} $k$ times between $R$ and $Q'_i$ for
$i$ from 1 to $k$. Then $R$ reduces into $R' \in \synchoneside{B}$ and
$Q'_i$ reduces into an element of $\addLets{\compiler{Q_i}}$. By Lemma~\ref{lem:addlets}, we reduce $P'_i$ into $\compiler{P_i}$ and further reduce $Q'_i$ into $\compiler{Q_i}$, so Fact~\ref{fact:extraSteps} holds.
\end{proof}
\begin{fact}\label{fact:rbar}
Given configurations $\Conf$, $\Conf'$, and $\Conf_1$
such that $\Conf \Rel_1 \Conf'$ with $k = n$ and $\Conf \reduc \Conf_1$
by {\RBarII}, we have $\Conf_1 \Rel_2 \Conf'$.
\end{fact}
%
Fact~\ref{fact:rbar} handles the swapping of data at barriers,
so it is a key step of the proof.
\medskip
\begin{proof}[Proof of Fact~\ref{fact:rbar}]\noqed
We use the notations of the definition of $\Rel_1$.
Since $\Qcal$ contains $n$ barriers, we have $\Conf \reduc \Conf_1 = B', E, \Pcal \cup \{ Q_1\varsigma_1, \dots, Q_n\varsigma_n \}$ by {\RBarII}.
We have $\Conf' = \emptyset, E,\Pcal' \cup \Qcal' \cup \{R\}$
and since $k = n$, we have $R = \Out[c_{1}]{ {N_{f(1)}}}\mathrel.\cdots\mathrel.\Out[c_n]{{N_{f(n)}}}\mathrel.R'$ with
$N_{l} = \tuple{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}$ for all $l \leq n$ and
$R' \in \synchoneside{B'}$.
Moreover, $\Qcal' = \{Q'_1, \dots, Q'_n\}$ with $Q'_i \in \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i}$ for all $i \leq n$.
Since for all $1\leq l \leq n$, $Q_l/\tup{z}_l \eqren Q_{f(l)}/\tup{z}_{f(l)}$,
we have
\[\begin{split}
&Q_{l} \{\subst{y_1}{z_{l,1}},\dots,\subst{y_{|\tup{z}_{l}|}}{z_{l,|\tup{z}_{l}|}}\} \eqren {}\\
&\quad Q_{f(l)} \{\subst{y_1}{z_{f(l),1}},\dots,\subst{y_{|\tup{z}_{l}|}}{z_{f(l),|\tup{z}_{l}|}}\}\,,
\end{split}\]
where $y_1,\dots,y_{|\tup{z}_l|}$ are fresh variables, so we have
\[\begin{split}
&Q_{l} \{\subst{y_1}{z_{l,1}},\dots,\subst{y_{|\tup{z}_{l}|}}{z_{l,|\tup{z}_{l}|}}\} = {}\\
&\quad Q_{f(l)} \{\subst{y_1}{z_{f(l),1}},\dots,\subst{y_{|\tup{z}_{l}|}}{z_{f(l),|\tup{z}_{l}|}}\}\rho_l\,,
\end{split}\]
for some renaming $\rho_l$ of channels of annotated barriers. (Recall that processes are considered equal modulo renaming of bound names and variables.)
The renaming $\rho_l$ maps names in $\channels{\barriers{Q_l}}$ to names
in $\channels{\barriers{Q_{f(l)}}}$. Since the names in $\channels{\barriers{\Pcal \cup \Qcal}}$ are pairwise distinct, for $l \neq l'$, $\channels{\barriers{Q_l}} \cap \channels{\barriers{Q_{l'}}} = \emptyset$, so we can merge all functions $\rho_l$ for $1 \leq l \leq n$ into a single function $\rho$. Since furthermore $f$ is a permutation, $\rho$ is a permutation of $\channels{B'}$ and leaves other names unchanged.
Since the names in $\channels{\barriers{\Pcal \cup \Qcal}}$ are pairwise distinct, $\rho$ leaves unchanged the names in $\channels{\barriers{\Pcal}}$ and $a_1$, $c_1$, \dots, $a_n$, $c_n$.
Hence, we obtain
\[\begin{split}
&\compilerI{Q_{i}} \{\subst{y_1}{z_{i,1}},\dots,\subst{y_{|\tup{z}_{i}|}}{z_{i,|\tup{z}_{i}|}}\} = {}\\
&\quad \compilerI{Q_{f(i)}}\{\subst{y_1}{z_{f(i),1}},\dots,\subst{y_{|\tup{z}_{l}|}}{z_{f(i),|\tup{z}_{l}|}}\}\rho
\end{split}\]
for all $i \leq n$ by Lemma~\ref{lem:substIbb}, so
\[\begin{split}
&\compilerInI{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i} = {}\\
&\quad \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_{f(i)}}Q_{f(i)}}\rho
\end{split}\]
for all $i \leq n$. (Recall that processes are considered equal modulo renaming of bound variables.)
So $Q'_i \in \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_{f(i)}}Q_{f(i)}}\rho$.
Therefore, $Q'_i \in \compilerIn{\Out[c_i]{N_{f(i)}}}{\allowbreak Q_{f(i)}\varsigma_{f(i)}}\rho$,
so $Q'_i \rho^{-1} \in \compilerIn{\Out[c_i]{N_{f(i)}}}{Q_{f(i)}\varsigma_{f(i)}}$.
We define $\Qcal_1 = \{ Q_{1}\varsigma_1,\allowbreak\dots,\allowbreak Q_n\varsigma_n \}
= \{ Q_{f(1)} \varsigma_{f(1)}, \dots, Q_{f(n)} \varsigma_{f(n)} \}$
since $f$ is a permutation of $\{1,\dots,n\}$,
$\Qcal'_1 = \{ Q'_1\rho^{-1}, \dots, Q'_n \rho^{-1}\} = \Qcal'\rho^{-1}$, and
$R_1 = R\rho^{-1} = \Out[c_{1}]{ {N_{f(1)}}}\mathrel.\cdots\mathrel.\Out[c_n]{{N_{f(n)}}}\mathrel.R'_1$, where $R'_1 = R'\rho^{-1} \in \synchoneside{B'\rho^{-1}}$ since $R' \in \synchoneside{B'}$.
Moreover, $B'\rho^{-1} = B'$ since $\rho^{-1}$ maps a barrier of $Q_l$ to a barrier of $Q_{f(l)}$ for all $l \leq n$ and leaves other barriers unchanged.
Therefore, $R'_1 \in \synchoneside{B'}$.
%
Moreover, since $\Conf$ is valid, the elements of $\channels{B}$ are pairwise distinct so $c_1, \dots, c_n$ are pairwise distinct names. By Lemma~\ref{lem:valid-no-fn}, for all $i \leq n$, $c_i \notin \fn{\{Q_i\varsigma_i\} \cup \Pcal \cup \Qcal \setminus \{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i\}} \supseteq \fn{\Pcal \cup \Qcal_1}$. Furthermore, $c_1, \dots, c_n$ are in $\channels{B}$, so they are in $E$ since $\Conf$ is valid, hence they are in $E \setminus \fn{\Pcal \cup \Qcal_1}$.
%
We have $\Conf' = (\emptyset, E, \Pcal' \cup \Qcal' \cup \{R\}) = (\emptyset, E\rho^{-1}, \Pcal' \rho^{-1}\cup \Qcal'\rho^{-1} \cup \{R\rho^{-1}\})$ since configurations are considered equal modulo renaming, so $\Conf' = (\emptyset, E, \Pcal' \cup \Qcal'_1 \cup \{R_1\})$.
%
It follows that $\Conf_1 = (B', E, \Pcal \cup \Qcal_1) \Rel_2 \Conf' = (\emptyset, E, \Pcal' \cup \Qcal'_1 \cup \{R_1\})$ using $N_{f(i)}$ for $M_i$ for all $i \leq n$.
\end{proof}
\noindent We proceed with the proof of Proposition~\ref{prop:soundnessSwapping} by showing that
$\Rel$ satisfies
the three conditions of Definition~\ref{def:proverif:obs}.
\subsubsection*{Condition~1} We show that, if $\Conf \Rel' \Conf'$ and $\Conf\downarrow_N$, then $\Conf'\reduc^*\downarrow_N$, where $\Rel' \in
\{{\Rel_1}, {\Rel_2}, {\Rel_3}, \Rel_1^{-1}, \Rel_2^{-1}, \Rel_3^{-1}\}$, by distinguishing the following cases:
\begin{description}
\item[${\Rel'}={\Rel_1}$.] In this case, $\Conf = B,E,\Pcal \cup \Qcal$ and $\Conf' = \emptyset, E,\Pcal'\cup \Qcal' \cup\{R\}$. By inspection of $\Pcal \cup \Qcal$, we have $P_i = \Out[N]{M}.Q \in \Pcal$ for some index $i$, process $Q$, and term $M$, with $\fn{N} \cap E = \emptyset$. It follows that $\compiler{P_i} = \Out[N]{M}.\compiler{Q}$ and by Lemma~\ref{lem:addlets}, $P'_i \in \addLets{\compiler{P_i}}$ reduces into $\compiler{P_i}$ inside $\Conf'$, hence $\Conf'\reduc^*\downarrow_N$.
\item[${\Rel'}={\Rel_2}$.] In this case, $\Conf = B,E,\Pcal \cup \Qcal$, where $\Out[N]{M}.Q\in\Pcal \cup \Qcal$ for some process $Q$ and term $M$, with $\fn{N} \cap E = \emptyset$. It follows that $\Out[N]{M}.\compiler{Q} \in \compiler{\Pcal\cup\Qcal}$. By Fact~\ref{fact:extraSteps}, we have $\Conf' \reduc^* \Conf'_1\emptyset, E,\compiler{\Pcal\cup\Qcal} \cup \{ R' \}$, where $R' \in \synchoneside{B}$ and, moreover, $\Conf'_1\downarrow_N$, hence, $\Conf'\reduc^*\downarrow_N$.
\item[${\Rel'}={\Rel_3}$.] In this case, $\Conf = \emptyset, E, \Pcal$ and $\Conf' = \emptyset, E, \Pcal'$, where $P_i = \Out[N]{M}.Q\in\Pcal$ for some index $i$, process $Q$ and term $M$, with $\fn{N} \cap E = \emptyset$. We have $P'_i \in \addLets{P_i}$, so by Lemma~\ref{lem:addlets}, $P'_i$ reduces into $P_i$ inside $\Conf'$. It follows immediately that $\Conf'\reduc^*\downarrow_N$.
\item[${\Rel'}={\Rel_1^{-1}}$.] In this case, $\Conf = \emptyset,E,\Pcal' \cup \Qcal' \cup\{R\}$ and $\Conf' = B, E,\Pcal \cup \Qcal$.
We have $\Out[N]{M}.Q \in \Pcal'\cup \Qcal' \cup \{R\}$ for some process $Q$ and term $M$, with $\fn{N} \cap E = \emptyset$.
The process $R$ cannot be the output $\Out[N]{M}.Q$ because if $k \neq n$, then $R$ starts with an input and if $k = n$, then $R$ starts with an output on channel $c_1 \in E$ since $\channels{B} \subseteq E$.
Therefore, by inspection of $\Pcal' \cup \Qcal' \cup\{R\}$, we have $P'_i = \Out[N]{M}.Q = \compiler{P_i} \in \Pcal'$ for some index $i$, and $\Conf'\downarrow_N$ by \Cref{lem:outputCh}.
\item[${\Rel'}={\Rel_2^{-1}}$.] In this case $\Conf = \emptyset,E,\Pcal' \cup \Qcal' \cup \{R\}$ and $\Conf' = B, E,\Pcal\cup\Qcal$.
We have $\Out[N]{M}.Q \in \Pcal'\cup \Qcal' \cup \{R\}$ for some process $Q$ and term $M$, with $\fn{N} \cap E = \emptyset$.
If $k > 0$, then
$R$ starts with an output on $c_1\in E\setminus\fn{\Pcal \cup \Qcal}$. It follows immediately that $N\neq c_1$, since $\fn{N} \cap E = \emptyset$.
If $k = 0$, then $R$ is either 0 or starts with an input, so in all cases, $R$ does not start with the output $\Out[N]{M}.Q$.
Therefore, by inspection of $\Pcal' \cup \Qcal' \cup\{R\}$, we have $P'_i = \Out[N]{M}.Q = \compiler{P_i} \in \Pcal'$ for some index $i$, and $\Conf'\downarrow_N$ by \Cref{lem:outputCh}.
\item[${\Rel'}={\Rel_3^{-1}}$.] In this case, $\Conf = \emptyset, E, \Pcal'$ and $\Conf' = \emptyset, E, \Pcal$. By inspection of $\Pcal'$, it follows that $P'_i = \Out[N]{M}.Q = P_i \in\Pcal$ for some index $i$, process $Q$, and term $M$, with $\fn{N} \cap E = \emptyset$, and, hence, $\Conf'\downarrow_N$.
\end{description}
\subsubsection*{Condition~2} We show that, if $\Conf \Rel' \Conf'$ and $\Conf\reduc\Conf_1$, then $\Conf'\reduc^*\Conf'_1$ and $\Conf_1 \Rel \Conf'_1$ for some $\Conf'_1$, where $\Rel' \in
\{{\Rel_1}, {\Rel_2}, {\Rel_3}, \Rel_1^{-1}, \Rel_2^{-1}, \Rel_3^{-1}\}$, by distinguishing the following cases:
\begin{description}
\item[${\Rel'}={\Rel_1}$.] We have $\Conf = B,E,\Pcal \cup \Qcal$ and $\Conf' = \emptyset, E, \Pcal'\cup \Qcal' \cup\{ R\}$, with the conditions given in the definition of $\Rel_1$.
Let us distinguish two cases:
\begin{itemize}
\item Case I: $\Conf \reduc \Conf_1$ by $\RBarII$.
In this case, $\Conf = B, E, \Pcal \cup \Qcal$,
$\Qcal = \{\sstageA{t}{a_1,c_1, \varsigma_1}Q_1,\allowbreak\dots,\allowbreak\sstageA{t}{a_k,c_k,\varsigma_k}Q_k\}$,
$\Pcal = \Pcal_1 \cup \{ \sstageA{t}{a_{k+1},c_{k+1}, \varsigma_{k+1}}Q_{k+1},\allowbreak\dots,\allowbreak\sstageA{t}{a_n,c_n,\varsigma_n}Q_n\}$,
and
$\Conf_1 =B',E,\Pcal_1 \cup \{Q_{1}\varsigma_1,\dots,Q_n\varsigma_n\}$,
where $B' = B \setminus \{\sstageA{t}{a_1,c_1,\tup{z}_1} Q_1,\dots,\sstageA{t}{a_n,c_n,\tup{z}_n} Q_n\}$ and $\tup{z}_i = \ordom{\varsigma_i}$ for all $i \leq n$.
For a suitable numbering of processes, we have $P_i = \sstageA{t}{a_{k+i},c_{k+i}, \varsigma_{k+i}}Q_{k+i}$ for $i = 1, \dots, n-k$ and $\Pcal_1 = \{P_{n-k+1}, \dots, P_m\}$.
%
Since $\Conf \Rel_1 \Conf'$, we have $\Conf' = \emptyset, E, \Pcal' \cup \Qcal' \cup \{R\}$ where $\Pcal' = \{P'_1, \dots, P'_m\}$ with $P'_i \in \addLets{\compilerI{P_i}}$ for all $i \leq m$ and $\Qcal' = \{Q'_1, \dots, Q'_k\}$ with $Q'_i \in \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i}$ for all $i \leq k$.
%
By Lemma~\ref{lem:addlets}, we can reduce the lets so that $\Conf' \reduc^* \Conf'_2 = \emptyset, E, \Pcal'_2 \cup \Qcal' \cup \{R\}$ where $\Pcal'_2 = \{P''_1, \dots, P''_m\}$ with $P''_i = \compilerI{P_i}$ for all $i \leq m$.
%
Furthermore, we can reduce each $P''_i \in \compilerI{\sstageA{t}{a_{k+i},c_{k+i}, \varsigma_{k+i}}Q_{k+i}}$ for $i = 1, \dots, n-k$ with $R$ by {\RIO}, so that $\Conf'_2 \reduc^{n-k} \Conf'_1 = \emptyset, E, \Pcal'_1 \cup \Qcal'_1 \cup \{R_1\}$, where
$\Pcal'_1 = \{ P''_{n-k+1}, \ldots, P''_m\}$ with $P''_i = \compilerI{P_i}$ for $i = n-k+1, \dots, m$, $\Qcal'_1 = \{Q'_1, \dots, Q'_n\}$ with $Q'_i \in \compilerInI{\sstageA{t}{a_i,c_i,\varsigma_i}Q_i}$ for all $i \leq n$,
and $R_1 = \Out[c_{1}]{ {N_{f(1)}}}.\cdots.\Out[c_n]{{N_{f(n)}}}.R'$
where $N_{l} = \tuple{M_{l,1},\dots,M_{l,|\varsigma_{l}|}}$ for all $l \leq n$
and $R' \in \synchoneside{B'}$.
%
After these reductions, we obtain $\Conf \Rel_1 \Conf'_1$ with $k = n$.
By Fact~\ref{fact:rbar}, we have $\Conf_1 \Rel_2 \Conf'_1$.
Therefore, $\Conf_1 \Rel \Conf'_1$ and $\Conf' \reduc^* \Conf'_1$.
\item Case II: $\Conf \reduc \Conf_1$ without application of $\RBar$. By inspection of our reduction rules, the reduction $\Conf \reduc \Conf_1$ is obtained by reducing processes in $\Pcal$ and $\Conf_1 = B,E_1,\Pcal_1 \cup \Qcal$ for some multiset of processes $\Pcal_1$ and set of names $E_1$. By Lemma~\ref{lem:addlets}, we can reduce the lets in $\Pcal'$ so that $\Conf' \rightarrow^* \Conf'_2 = B, E_1, \compiler{\Pcal} \cup \Qcal' \cup \{R\}$. By Lemma~\ref{lem:red}\eqref{prop1},
$\Conf'_2\reduc\Conf'_1$, where $\Conf'_1 = \emptyset,E_1, \compiler{\Pcal_1}\cup \Qcal' \cup \{ R \}$.
Hence, $\Conf_1\Rel_1\Conf'_1$ (with $k$, $n$, $f$ unchanged), therefore, $\Conf_1 \Rel \Conf_1'$ and $\Conf' \reduc^* \Conf'_1$.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[${\Rel'} = {\Rel_2}$.] We have $\Conf = B,E,\Pcal \cup \Qcal$ and $\Conf' = \emptyset, E, \Pcal' \cup \Qcal' \cup \{ R\}$, with the conditions given in the definition of $\Rel_2$.
By Fact~\ref{fact:extraSteps}, we have $\Conf' \reduc^* \Conf'_2 = \emptyset, E,\compiler{\Pcal\cup\Qcal}\cup\{ R'\}$, where $R' \in \synchoneside{B}$.
\begin{itemize}
\item
Case I: $B = \emptyset$.
Since $\Conf$ is a valid configuration, we have $\barriers{\Pcal\cup\Qcal} \subseteq B$, so $\Pcal$ and $\Qcal$ contain no barrier, therefore, $\Pcal \cup \Qcal = \compiler{\Pcal\cup\Qcal}$ by definition of $\compilerSymb$ (Figure~\ref{fig:def:compiler}).
By definition of $\synchSymb_1$, we have $R' = \{0\}$.
Hence, $\Conf' \reduc^* \Conf'_2 = \emptyset, E,\Pcal\cup\Qcal\cup\{ 0\} \reduc \Conf = \emptyset, E,\Pcal\cup\Qcal$.
Since $\Conf \reduc \Conf_1$, we have $\Conf' \reduc^* \Conf_1$.
Moreover, we have $\Conf_1 \Rel_3 \Conf_1$, so $\Conf_1 \Rel \Conf_1$,
and we conclude with $\Conf'_1 = \Conf_1$.
\item Case II: $B \neq \emptyset$.
We have $\Conf \Rel_1 \Conf'_2$ with $k = 0$ by expanding
the definition of $\synchoneside{B}$,
and we conclude by the case ${\Rel'} = {\Rel_1}$ above.
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[${\Rel'} = {\Rel_3}$.] We have $\Conf = \emptyset,E,\Pcal$ and $\Conf' = \emptyset, E,\Pcal'$ with $\barriers{\Pcal} = \emptyset$ and $P'_i \in \addLets{P_i}$ for all $i \leq m$.
By Lemma~\ref{lem:addlets}, we can reduce the lets in $\Pcal'$ so
that $\Conf' \reduc^* \Conf = \emptyset, E,\Pcal$.
Since $\Conf \reduc \Conf_1$, we have $\Conf' \reduc^* \Conf_1$.
Moreover, we have $\Conf_1 \Rel_3 \Conf_1$, so $\Conf_1 \Rel \Conf_1$,
and we conclude with $\Conf'_1 = \Conf_1$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[${\Rel'} = {\Rel_1^{-1}}$.] We have $\Conf = \emptyset, E,\Pcal' \cup \Qcal' \cup \{R\}$ and $\Conf' = B,E,\Pcal \cup \Qcal$, with the conditions given in the definition of $\Rel_1$.
\begin{itemize}
\item Case I: $k = n$.
Since $\Qcal$ contains $n$ barriers, we have $\Conf' \reduc \Conf'_2 = B', E, \Pcal \cup \{ Q_1\varsigma_1, \dots, Q_n\varsigma_n \}$ by {\RBarII}.
By Fact~\ref{fact:rbar}, we have $\Conf'_2 \Rel_2 \Conf$, so we conclude by the case ${\Rel'} = {\Rel_2^{-1}}$ (below).
\item Case II: $k < n$.
\begin{itemize}
\item Case II.1: $\Conf\reduc\Conf_1$ by reducing at least $R$. Since $R$ starts with an input on $a_{k+1}$, it can only reduce by {\RIO} with an output on $a_{k+1}$. The processes in $\Qcal'$ start with an input, so they cannot reduce with $R$. Hence $R$ reduces with a process $P'_i \in \addLets{\compilerI{P_i}}$ in $\Pcal'$. If $P'_i$ starts with a let, it cannot reduce by {\RIO}, so we have $P'_i = \compilerI{P_i}$. Since $a_{k+1} \in \channels{B}$ and $\Conf'$ is valid, $a_{k+1} \notin \fnnobc{\Pcal \cup \Qcal}$, so $a_{k+1}$ occurs free in $\Pcal \cup \Qcal$ only as channel of a barrier in $\Pcal \cup \Qcal$.
Since $P'_i = \compilerI{P_i}$ starts with an output on $a_{k+1}$ and $\barriers{P_i} \subseteq B$, we have $P_i = \sstageA{t}{a_{k+1},c_{k+1},\varsigma_{k+1}}Q_{k+1}$ for some $\varsigma_{k+1} = (\subst{M_{k+1,1}}{z_{k+1,1}}, \allowbreak \dots, \allowbreak \subst{M_{k+1,|\varsigma_{k+1}|}}{z_{k+1,|\varsigma_{k+1}|}})$.
Let $N'_{k+1} = \tuple{M_{k+1,1},\dots,M_{k+1,|\varsigma_{k+1}|}}$ and for all $l \neq k+1$, $N'_l = N_l$.
We have
\begin{align*}
P'_i = {}&\Out[a_{k+1}]{N'_{k+1}}.\In[c_{k+1}]{z}.\\
&\Letin{z_{k+1,1}}{\projnew 1 {|\varsigma_{k+1}|} z}\ \cdots\\
&\Letin{z_{k+1,|\varsigma_{k+1}|}}{\projnew {|\varsigma_{k+1}|} {|\varsigma_{k+1}|} z}\\
&\compilerI{Q_{k+1}}\,.
\end{align*}
Let
\begin{align*}
Q'_{k+1} &= \In[c_{k+1}]{z}.\Letin{z_{k+1,1}}{\projnew 1 {|\varsigma_{k+1}|} z}\cdots\\
&\phantom{{} = {}}\Letin{z_{k+1,|\varsigma_{k+1}|}}{\projnew {|\varsigma_{k+1}|} {|\varsigma_{k+1}|} z}\\
&\phantom{{} = {}}\compilerI{Q_{k+1}}\\
& \in \compilerInI{\sstageA{t}{a_{k+1},c_{k+1},\varsigma_{k+1}}Q_{k+1}}\,.
\end{align*}
After reduction by {\RIO}, $P'_i$ becomes $Q'_{k+1}$ and $R$ becomes $R_1 = \In[a_{k+2}]{x_{k+2}}\mathrel.\cdots\mathrel.\In[a_n]{x_n}\mathrel.\Out[c_{1}]{ {N'_{f(1)}}}\mathrel.\cdots\mathrel.\Out[c_n]{{N'_{f(n)}}}\mathrel.R'$.
Let $\Pcal_1 = \Pcal \setminus \{P_i\}$, $\Qcal_1 = \Qcal' \cup \{P_i\} = \Qcal' \cup \{ \sstageA{t}{a_{k+1},c_{k+1},\varsigma_{k+1}}Q_{k+1} \}$,
$\Pcal'_1 = \Pcal' \setminus \{ P'_i\}$, and $\Qcal'_1 = \Qcal' \cup \{Q'_{k+1}\}$.
Then we have $\Conf = (\emptyset, E,\Pcal' \cup \Qcal' \cup \{R\}) \reduc \Conf_1 = (\emptyset, E, \Pcal'_1 \cup \Qcal'_1 \cup \{R_1\})$ and $\Conf' = (B, E, \Pcal_1 \cup \Qcal_1) \Rel_1 \Conf_1 = (\emptyset, E, \Pcal'_1 \cup \Qcal'_1 \cup \{R_1\})$ (with $m$ decreased by one, $k$ increased by one, and $f$ unchanged), so we conclude with $\Conf'_1 = \Conf'$.
\item Case II.2: $\Conf\reduc\Conf_1$ by reducing at least a process in $\Qcal'$. Since we reduce $Q'_i \in \Qcal'$, which starts with an input on $c_i$, this process can only reduce by {\RIO}, with an output on $c_i$. If it reduced with $P'_j \in \Pcal'$, since $P'_j \in \addLets{\compiler{P_j}}$, we would actually have $P'_j = \compiler{P_j}$. Since $\Conf$ is valid, by Lemma~\ref{lem:valid-no-fn}, $c_i \notin \fn{\Pcal}$, so $c_i \notin \fn{P'_j} = \fn{\compiler{P_j}} = \fn{P_j}$, hence $Q'_i$ cannot reduce with a process $P'_j \in \Pcal'$. It also cannot reduce with $R$ or with another process in $\Qcal'$ since they start with an input. Therefore, this case cannot happen.
\item Case II.3: $\Conf\reduc\Conf_1$ by reducing only processes in $\Pcal'$.
\begin{itemize}
\item Case II.3.1: a reduced process is $P'_i \neq \compilerI{P_i}$.
We have $P'_i \in \addLets{\compilerI{P_i}}$.
By Lemma~\ref{lem:addlets},
$\Conf_1 = \emptyset, E,(\Pcal' \setminus \{P'_i\}) \cup \{P''_i\} \cup \Qcal' \cup \{R\}$ with $P''_i \in \addLets{\compilerI{P_i}}$, so we still have $\Conf' \Rel_1 \Conf_1$, so we conclude with $\Conf'_1 = \Conf'$.
\item Case II.3.2: the reduced process(es) are $P'_i = \compilerI{P_i}$ and possibly $P'_j = \compilerI{P_j}$.
Let $\Pred' = \{P'_i\}$ or $\Pred' = \{P'_i, P'_j\}$ be the multiset of reduced processes, such that $\Pred' = \compilerI{\Pred}$,
$\Pcal' = \Pstay' \cup \Pred'$, $\Pcal = \Pstay \cup \Pred$.
We have $\Conf = (\emptyset, E, \Pstay' \cup \compilerI{\Pred} \cup \Qcal' \cup \{R\}) \reduc \Conf_1 = (\emptyset, E_1, \Pstay' \cup \Predone' \cup \Qcal' \cup \{R\})$ by reducing one or more processes in $\compilerI{\Pred}$, so by Lemma~\ref{lem:red}\eqref{prop2}, there exists $\Predone$ such that $\Predone' = \compilerI{\Predone}$
and $\Conf' = (B, E, \Pstay \cup \Pred \cup \Qcal) \reduc \Conf'_1 = (B, E, \Pstay \cup \Predone \cup \Qcal)$.
Letting $\Pcal_1 = \Pstay \cup \Predone$ and $\Pcal'_1 = \Pstay' \cup \Predone'$, we obtain that $\Conf'_1 = (B, E, \Pcal_1 \cup \Qcal)\Rel_1 \Conf_1 = (\emptyset, E_1, \Pcal'_1 \cup \Qcal' \cup \{R\})$ (with $f$, $k$, $n$ unchanged), so $\Conf_1 \Rel \Conf'_1$.
\end{itemize}
\end{itemize}
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[${\Rel'} = {\Rel_2^{-1}}$.] We have $\Conf=\emptyset, E, \Pcal' \cup \Qcal' \cup \{ R\}$ and $\Conf' = B,E,\Pcal \cup \Qcal$, with the conditions given in the definition of $\Rel_2$. We distinguish several cases.
\begin{itemize}
\item Case I: $\Conf\reduc \Conf_1$ by reducing at least $R$.
\begin{itemize}
\item Case I.1: $k = 0$. In this case, $\Qcal = \Qcal' = \emptyset$.
\begin{itemize}
\item Case I.1.1: $B = \emptyset$. Then $R = 0$, so $\Conf\reduc \Conf_1 =\emptyset, E, \Pcal'$, $\Conf' = \emptyset,E,\Pcal$, and furthermore since $B = \emptyset$, we have $\barriers{\Pcal} = \emptyset$, so $P'_i \in \addLets{\compilerI{P_i}} = \addLets{P_i}$, so $\Conf' \Rel_3 \Conf_1$, so $\Conf_1 \Rel \Conf'$. We conclude with $\Conf'_1 = \Conf'$.
\item Case I.1.2: $B \neq \emptyset$. Then we have $\Conf' \Rel_1 \Conf$ by expanding the definition of $\synchoneside{B}$, we conclude by using the case ${\Rel'} = {\Rel_1^{-1}}$, Case II.1 ($k < n$, $\Conf \reduc \Conf_1$ by reducing $R$, above).
\end{itemize}
\item Case I.2: $k > 0$.
The process $R$ starts with an output on $c_1$, hence it can only reduce by {\RIO} with an input on $c_1$.
If $R$ reduced with $P'_i \in \Pcal'$, since $P'_i \in \addLets{\compiler{P_i}}$, we would actually have $P'_i = \compiler{P_i}$. By definition of $\Rel_2$, $c_1 \notin \fn{P_i}$, so $c_1 \notin \fn{P'_i} = \fn{\compiler{P_i}} = \fn{P_i}$, hence $R$ cannot reduce with $P'_i \in \Pcal'$.
It cannot reduce with $Q'_i$ for $i > 1$ because $c_1, \dots, c_k$ are pairwise distinct.
Therefore, $R$ reduces with $Q'_1$ by {\RIO}. After reduction,
$R$ is transformed into
\[R_1 = \Out[c_2]{M_2}\mathrel.\cdots\mathrel.\Out[c_k]{M_k}\mathrel.R'\]
with $R' \in \synchoneside{B}$, and since $Q'_1 \in \compilerIn{\Out[c_1]{M_1}}{Q_1}$,
\[\begin{split}
Q'_1 = {}&\In[c_1]{z}.\Letin{z_1}{\projnew{1}{n}{z}} \cdots\\
& \Letin{z_n}{\projnew{n}{n}{z}}\compilerI{Q'}
\end{split}\]
with $M_1 = \tuple{N_1,\dots, N_n}$, $Q_1 = Q'\{\subst{N_1}{z_1}, \dots, \subst{N_n}{z_n}\}$, and $z, \allowbreak z_1, \allowbreak \dots, \allowbreak z_n$ pairwise distinct variables is transformed into
\begin{align*}
P'_{m+1} &= \Letin{z_1}{\projnew{1}{n}{M_1}} \cdots\\
&\phantom{{}={}} \Letin{z_n}{\projnew{n}{n}{M_1}}\compilerI{Q'}\\
&\in \addLets{\compilerI{Q_1}}
\end{align*}
because $\compilerI{Q_1} = \compilerI{Q'}\{\subst{N_1}{z_1}, \dots, \subst{N_n}{z_n}\}$ by Lemma~\ref{lem:substIIb}.
We let $\Pcal_1 = \Pcal \cup \{Q_1\}$, $\Qcal_1 = \Qcal \setminus \{Q_1\}$,
$\Pcal'_1 = \Pcal' \cup \{P'_{m+1}\}$, and $\Qcal'_1 = \Qcal' \setminus \{Q'_1\}$.
Then we have $\Conf = (\emptyset, E, \Pcal' \cup \Qcal' \cup \{ R\}) \reduc
\Conf_1 = (\emptyset, E, \Pcal'_1 \cup \Qcal'_1 \cup \{ R_1\})$
and
$\Conf' = (B,E,\Pcal \cup \Qcal) = (B,E,\Pcal_1 \cup \Qcal_1)
\Rel_2 \Conf_1 = (\emptyset, E, \Pcal'_1 \cup \Qcal'_1 \cup \{ R_1\})$
(with $k$ decreased by one and $m$ increased by one),
so we conclude with $\Conf'_1 = \Conf'$.
\end{itemize}
\item Case II: $\Conf\reduc \Conf_1$ by reducing at least a process in $\Qcal'$ and not reducing $R$. Since we reduce $Q'_i \in \Qcal'$, which starts with an input on $c_i$, this process can reduce only by {\RIO}, with an output on $c_i$. If it reduced with $P'_j \in \Pcal'$, since $P'_j \in \addLets{\compiler{P_j}}$, we would actually have $P'_j = \compilerI{P_j}$. By definition of $\Rel_2$, $c_i \notin \fn{P_j}$, so $c_i \notin \fn{P'_j} = \fn{\compiler{P_j}} = \fn{P_j}$, hence $Q'_i$ cannot reduce with a process $P'_j \in \Pcal'$. Moreover, $Q'_i$ cannot reduce with another process in $\Qcal'$ because all these processes start with inputs. Therefore, this case is impossible.
\item Case III: $\Conf\reduc \Conf_1$ by reducing only processes in $\Pcal'$.
This case is similar to the case ${\Rel'} = {\Rel_1^{-1}}$, Case II.3.
\iffalse
\begin{itemize}
\item Case III.1: a reduced process is $P'_i \neq \compilerI{P_i}$.
We have $P'_i \in \addLets{\compilerI{P_i}}$.
By Lemma~\ref{lem:addlets},
$\Conf_1 = \emptyset, E,(\Pcal' \setminus \{P'_i\} \cup \{P''_i\}) \cup \Qcal' \cup \{R\}$ with $P''_i \in \addLets{\compilerI{P_i}}$, so we still have $\Conf' \Rel_2 \Conf_1$, so we conclude with $\Conf'_1 = \Conf'$.
\item Case III.2: the reduced process(es) are $P'_i = \compilerI{P_i}$ and possibly $P'_j = \compilerI{P_j}$.
Let $\Pred' = \{P'_i\}$ or $\Pred' = \{P'_i, P'_j\}$ be the multiset of reduced processes, such that $\Pred' = \compilerI{\Pred}$,
$\Pcal' = \Pstay' \cup \Pred'$, $\Pcal = \Pstay \cup \Pred$.
We have $\Conf = (\emptyset, E, \Pstay' \cup \compilerI{\Pred} \cup \Qcal' \cup \{R\}) \reduc \Conf_1 = (\emptyset, E_1, \Pstay' \cup \Predone' \cup \Qcal' \cup \{R\})$ by reducing one or more processes in $\compilerI{\Pred}$, so by Lemma~\ref{lem:red}\eqref{prop2}, there exists $\Predone$ such that $\Predone' = \compilerI{\Predone}$
and $\Conf' = (B, E, \Pstay \cup \Pred \cup \Qcal) \reduc \Conf'_1 = (B, E, \Pstay \cup \Predone \cup \Qcal)$.
Letting $\Pcal_1 = \Pstay \cup \Predone$ and $\Pcal'_1 = \Pstay' \cup \Predone'$, we obtain that $\Conf'_1 = (B, E, \Pcal_1 \cup \Qcal)\Rel_2 \Conf_1 = (\emptyset, E_1, \Pcal'_1 \cup \Qcal' \cup \{R\})$ (with $k$ unchanged), so $\Conf_1 \Rel \Conf'_1$.
\end{itemize}
\fi
\end{itemize}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\item[${\Rel'} = {\Rel_3^{-1}}$.] We have $\Conf = \emptyset, E, \Pcal'$ and $\Conf' = \emptyset, E, \Pcal$ with $\barriers{\Pcal} = \emptyset$, $\Pcal = \{P_1, \ldots, P_m\}$, $\Pcal' = \{P'_1, \dots, P'_m\}$, and for all $i \leq m$, $P'_i \in \addLets{P_i}$.
\begin{itemize}
\item Case I: a reduced process is $P'_i \neq P_i$.
We have $P'_i \in \addLets{P_i}$.
By Lemma~\ref{lem:addlets},
$\Conf_1 = \emptyset, E,(\Pcal' \setminus \{P'_i\}) \cup \{P''_i\}$ with $P''_i \in \addLets{P_i}$, so we still have $\Conf' \Rel_3 \Conf_1$, so we conclude with $\Conf'_1 = \Conf'$.
\item Case II: the reduced process(es) are $P'_i = P_i$ and possibly $P'_j = P_j$.
Let $\Pred = \{P_i\}$ or $\Pred = \{P_i, P_j\}$ be the multiset of reduced processes,
$\Pcal' = \Pstay' \cup \Pred$, and $\Pcal = \Pstay \cup \Pred$.
We have $\Conf = (\emptyset, E, \Pstay' \cup \Pred) \reduc \Conf_1 = (\emptyset, E_1, \Pstay' \cup \Predone)$ by reducing one or more processes in $\Pred$.
Since the reduction rules are independent of the non-reduced processes, we also have
$\Conf' = (\emptyset, E, \Pstay \cup \Pred) \reduc \Conf'_1 = (\emptyset, E_1, \Pstay \cup \Predone)$ and furthermore $\Conf'_1 \Rel_3 \Conf_1$,
so $\Conf_1 \Rel \Conf'_1$.
\end{itemize}
\end{description}
\subsubsection*{Condition~3} We show that, if $\Conf \Rel_i \Conf'$ and $\context$ is an adversarial context, then $\context[\Conf] \Rel_i \context[\Conf']$, for $i \in \{1, 2, 3\}$. Let $\context = \new{\tilde n}.(\_ \mid Q)$ with $\fv{Q} = \emptyset$ and $\barriers{Q} = \emptyset$. We rename $E$ in $\Conf$ and $\Conf'$ so that $E \cap \fn{Q} = \emptyset$.
\begin{description}
\item[$i = 1$.] We have $\Conf = B, E, \Pcal \cup \Qcal$
and $\Conf' = \emptyset, E, \Pcal' \cup \Qcal' \cup \{R\}$.
Let $\Pcal_1 = \Pcal \cup \{Q\}$, $\Pcal'_1 = \Pcal' \cup \{Q\}$,
and $E_1 = E \cup \{\tilde n\}$.
Since $Q$ contains no barrier, we have $\compilerI{Q} = Q$,
so $Q \in \addLets{\compilerI{Q}}$,
hence $\context[\Conf] = (B, E_1, \Pcal_1 \cup \Qcal) \Rel_1 \context[\Conf'] = (\emptyset, E_1, \Pcal'_1 \cup \Qcal' \cup \{R\})$ (with $m$ increased by one and $k$, $n$, $f$ unchanged).
\item[$i = 2$.] We have $\Conf = B, E, \Pcal \cup \Qcal$
and $\Conf' = \emptyset, E, \Pcal' \cup \Qcal' \cup \{R\}$.
Let $\Pcal_1 = \Pcal \cup \{Q\}$, $\Pcal'_1 = \Pcal' \cup \{Q\}$,
and $E_1 = E \cup \{\tilde n\}$.
Since $Q$ contains no barrier, we have $\compilerI{Q} = Q$,
so $Q \in \addLets{\compilerI{Q}}$,
hence $\context[\Conf] = (B, E_1, \Pcal_1 \cup \Qcal) \Rel_2 \context[\Conf'] = (\emptyset, E_1, \Pcal'_1 \cup \Qcal' \cup \{R\})$ (with $m$ increased by one and $k$ unchanged.)
\item[$i = 3$.] We have $\Conf = B, E, \Pcal$
and $\Conf' = \emptyset, E, \Pcal'$.
Let $\Pcal_1 = \Pcal \cup \{Q\}$, $\Pcal'_1 = \Pcal' \cup \{Q\}$,
and $E_1 = E \cup \{\tilde n\}$.
We have $Q \in \addLets{Q}$, so
$\context[\Conf] = (B, E_1, \Pcal_1) \Rel_3 \context[\Conf'] = (\emptyset, E_1, \Pcal'_1)$ (with $m$ increased by one).
\end{description}
\subsubsection*{Conclusion}
Since $\Rel$ is symmetric and satisfies the three conditions of Definition~\ref{def:proverif:obs}, we have ${\Rel} \subseteq {\approx}$.
Since $\fst{\Conf_0}\Rel\fst{\Conf'_0}$ and
$\snd{\Conf_0}\Rel\snd{\Conf'_0}$, we conclude that
$\fst{\Conf_0}\approx\fst{\Conf'_0}$ and
$\snd{\Conf_0}\approx\snd{\Conf'_0}$.
\end{proof}
\medskip
\begin{proof}[Proof of Proposition~\ref{prop:preserve-compil-second}]
Let $B_0 = \barriers{P}$, and
$\{\tilde{a}\} = \channels{B_0}$.
By definition of $\stageElimSymb$,
there exists a biprocess $R \in \synch{B_0}$ such that
$P' = \new{\tilde{a}}.(\compiler{P} \mid R)$.
It follows that $\barriers{P'} = \emptyset$, so we have
\begin{align*}
\Initconf{\fst{P'}}
&= \emptyset, \emptyset, \{\fst{P'}\} \\
&\approxconfig \emptyset,\{\tilde a\},\{\fst{\compiler{P} \mid R}\}
\tag*{by Proposition~\ref{prop:1}}\\
&\approxconfig \emptyset,\{\tilde a\},\{\fst{\compiler{P}}, \fst{R}\}
\tag*{by Proposition~\ref{prop:3}}\\
&\approxconfig \fst{B_0},\{\tilde a\},\{\fst{P}\} = \Initconf{\fst{P}}
\tag*{by Proposition~\ref{prop:soundnessSwapping}}
\end{align*}
so $\fst{P'} \approx \fst{P}$.
The proof of $\snd{P} \approx \snd{P'}$ is similar.
\end{proof}
\subsection{Proof of Theorem~\ref{thm:soundnessSwapping}}\label{app:thm:soundnessSwapping}
\begin{proof}[Proof of Theorem~\ref{thm:soundnessSwapping}]
Suppose that there exists a biprocess $P'\in\stageElimFunc{P}$ such
that $P'$ satisfies observational equivalence, that is,
$\fst{P'}\approx\snd{P'}$. By Proposition~\ref{prop:preserve-compil},
$\fst{P} \approx \fst{P'}$ and $\snd{P} \approx \snd{P'}$, so by
transitivity of $\approx$, we have $\fst{P} \approx \snd{P}$, so $P$
satisfies observational equivalence.
\end{proof}
\subsection{Proofs for \S\ref{sec:syncelim}}
\begin{proof}[Proof sketch of Proposition~\ref{prop:bounded-repl}]
Since barriers are forbidden under replication, the process $Q$
does not contain any barrier.
We have $\precompiler{\context[!Q]} = \contextA[!Q]$
and $\precompiler{\context[!^n Q]} = \contextA[!^n Q]$,
for some $\contextA$ obtained by annotating the barriers in $\context$.
By induction on $\contextA$, we have
$\compiler{\contextA[!Q]} = \contextB[!Q]$ and
$\compiler{\contextA[!^n Q]} = \contextB[!^n Q]$
for some $\contextB$.
Let $B = \barriers{\contextA[!Q]} = \barriers{\contextA[!^n Q]}$
and $\{\tilde a\} = \channels{B}$.
So $\stageElimFunc{\context[!Q]} = \stageElimSecondFunc{\contextA[!Q]} = \{ \contextC[!Q] \mid \contextC = \new{\tilde a}.(\contextB \mid R), R \in \synch{B} \}$
and $\stageElimFunc{\context[!^n Q]} = \stageElimSecondFunc{\contextA[!^n Q]} = \{ \contextC[!^n Q] \mid \contextC = \new{\tilde a}.(\contextB \mid R), R \in \synch{B} \}$.
Let $\contextD = \new{\tilde n}.(\_ \mid Q')$ be an adversarial context.
We have $\contextD[\Initconf{\contextC[!^n Q]}] = \emptyset, \{\tilde n\}, \{\contextC[!^n Q], Q'\}$
and similarly $\contextD[\Initconf{\contextC[!Q]}] = \emptyset, \{\tilde n\}, \{\contextC[!Q], Q'\}$.
Moreover, for any context $\contextC$,
all traces of $\emptyset, \{\tilde n\}, \{\contextC[!^n Q], Q'\}$ are matched by
traces of $\emptyset, \{\tilde n\}, \{\contextC[!Q], Q'\}$, by expanding the replication $!Q$ $n$
times when it appears at the root of a process in a semantic
configuration.
Therefore, if $\emptyset, \{\tilde n\}, \{\contextC[!^n Q], Q'\} \rightarrow^* \uparrow$,
then $\emptyset, \{\tilde n\}, \{\contextC[! Q], Q'\} \rightarrow^* \uparrow$.
Hence,
if $\contextC[!Q]$ satisfies diff-equivalence,
then $\contextC[!^n Q]$ satisfies diff-equivalence.
So we conclude that,
if some process in $\stageElimFunc{\context[!Q]}$ satisfies diff-equivalence,
then some process in $\stageElimFunc{\context[!^n Q]}$ satisfies diff-equivalence.
\end{proof}
\medskip
\begin{proof}[Proof sketch of Proposition~\ref{prop:syncelim}]
Let $P = \context[Q]$ and $P' = \context[\sstage{t}Q]$.
Since annotation proceeds from top to bottom, we annotate the barriers in $\context$ first, transforming $P = \context[Q]$ into $\contextA[Q_1]$ and $P' = \context[\sstage{t}Q]$ into $\contextA[\sstage{t}Q_1]$. Then we annotate $\sstage{t}Q_1$, transforming $P'$ into $\contextA[\sstageA{t}{a,c,\varsigma}Q'_1]$ where $Q_1 = Q_1'\varsigma$. Then we annotate the barriers in $Q_1$, respectively $Q'_1$.
If $\splitproc{Q} = (Q', \varsigma')$ and $(\fv{\range{\varsigma}} \cup \fn{\range{\varsigma}} \cup \dom{\varsigma}) \cap U = \emptyset$, then
$\splitproc{Q\varsigma} = (Q', \varsigma'\varsigma)$, by induction on $Q$.
Let $Q'_1 = \context[\sstage{t'}Q_2]$.
Then $Q_1 = C\varsigma[\sstage{t'}Q_2\varsigma]$, after renaming the bound names and variables of $\context$ so that they do not occur in $\varsigma$, and we have $\splitproc[\emptyset]{Q_2} = (Q_3, \varsigma')$, so $\splitproc[\emptyset]{Q_2\varsigma} = (Q_3, \varsigma'\varsigma)$. Therefore, by annotating $\sstage{t'}Q_2$, $Q'_1$ becomes $Q_4' = \context[\sstageA{t'}{a',c',\varsigma'}Q_3]$ and $Q_1$ becomes $C\varsigma[\sstageA{t'}{a',c',\varsigma'\varsigma}Q_3] = Q_4'\varsigma$ since $\fv{Q_3} \subseteq \dom{\varsigma'}$.
Hence, the property that $P'$ is transformed into $\contextA[\sstageA{t}{a,c,\varsigma}Q_1']$ and $P$ is transformed into $\contextA[Q'_1\varsigma]$ for some $\contextA$, $\varsigma$, $Q_1'$, and fresh names $a$, $c$ is preserved by annotation of $Q'_1$, respectively $Q_1'\varsigma$.
Therefore,
\begin{align*}
&P'_1 \triangleq \precompiler{P'} = \contextA[\sstageA{t}{a,c,\varsigma}Q_1']\\
&P_1 \triangleq \precompiler{P} = \contextA[Q'_1\varsigma]
\end{align*}
for some $\contextA$, $\varsigma$, $Q_1'$, and fresh names $a$, $c$ that
do not occur in $\contextA$, $\varsigma$, and $Q_1'$.
Let us define
\begin{align*}
&\addinlet{Q}{a,c,\varsigma} \triangleq {}\\
&\quad\In[c]{z}.\Letin{z_1}{\projnew 1 n z}\cdots
\Letin{z_n}{\projnew n n z}Q\\
&\addoutinlet{Q}{a,c,\varsigma} \triangleq {}\\
&\quad\Out[a]{\tuple{M_1, \dots,
M_n}}.\addinlet{Q}{a,c,\varsigma}
\end{align*}
where $\varsigma = (\subst{M_1}{z_1}, \dots, \subst{M_n}{z_n})$
and $z$ is a fresh variable.
We have
\begin{align*}
&\compilerI{\contextA[\sstageA{t}{a,c,\varsigma}Q_1']} = {}\\
&\quad \contextB[\addoutinlet{\compilerI{Q_1'}}{a,c,\varsigma}]\\
&\compilerI{\contextA[Q_1'\varsigma]} =
\contextB[\compilerI{Q_1'\varsigma}]
\end{align*} for some $\contextB$ such that $a$ and $c$ do not occur
in $\contextB$,
by induction on $\contextA$.
Furthermore, $\contextA$ and $\contextB$ do not contain replications
above the hole, since barriers never occur under replication.
So
\begin{align*}
&\compilerI{P_1'} =
\contextB[\addoutinlet{\compilerI{Q_1'}}{a,c,\varsigma}]\\
&\compilerI{P_1} =
\contextB[\compilerI{Q_1'\varsigma}] =
\contextB[\compilerI{Q_1'}\varsigma]
\end{align*} by Lemma~\ref{lem:substIbb}.
Moreover,
\[\barriers{P_1'} = \{ \sstageA{t}{a,c,\ordom{\varsigma}}Q'_1 \}
\cup \barriers{P_1}\,.\]
So, considering permutations $f$ that leave $j$ unchanged when the
$j$-th barrier is $\sstageA{t}{a,c,\ordom{\varsigma}}Q'_1$, we have that
\begin{align*}
&\synch{\barriers{P_1'}} \supseteq {}\\
&\quad \{
C_{3,i}[\In[a]{x}.C_{4,i}[\Out[c]{x}.Q_{2,i}]] \mid i = 1, \dots, n \}\\
&\synch{\barriers{P_1}} = \{
C_{3,i}[C_{4,i}[Q_{2,i}]] \mid i = 1, \dots, n \}
\end{align*}
for some families of contexts $C_{3,i}[\_]$ and $C_{4,i}[\_]$ and processes
$Q_{2,i}$, such that $C_{3,i}[\_]$ and $C_{4,i}[\_]$ do not bind $x$
and do not contain replications,
$x$ is not free in $C_{4,i}$ and $Q_{2,i}$, and $a$ and $c$ do not occur in
$C_{3,i}[\_]$, $C_{4,i}[\_]$, and $Q_{2,i}$.
We make a small abuse here: we write $\Out[c]{x}.Q_{2,i}$
instead of $\Out[c]{\diff{x}{x}}.Q_{2,i}$. It is clear that the
replacement of $\diff{x}{x}$ with $x$ does not change the behaviour
of the process.
Let $\{\tilde a\} = \channels{\barriers{P_1}}$.
We have $\channels{\barriers{P'_1}} = \{\tilde a, a, c\}$.
We finally obtain that
\begin{align*}
&\stageElimFunc{P'} = \stageElimSecondFunc{P'_1} \supseteq \{P'_{2,i} \mid i = 1, \dots, n \}\\
&\stageElimFunc{P} = \stageElimSecondFunc{P_1} = \{P_{2,i} \mid i = 1, \dots, n \}
\end{align*}
where
\begin{align*}
&P'_{2,i} \triangleq \new{\tilde a, a, c}.(\contextB[\addoutinlet{Q_2'}{a,c,\varsigma}] \mid {}\\
&\phantom{P'_{2,i} \triangleq \new{\tilde a, a, c}.(}
C_{3,i}[\In[a]{x}.C_{4,i}[\Out[c]{x}.Q_{2,i}]])\\
&P_{2,i} \triangleq \new{\tilde a}.(\contextB[Q_2'\varsigma]
\mid C_{3,i}[C_{4,i}[Q_{2,i}]])
\end{align*}
for some $\contextB$, $Q_2'$, $C_{3,i}[\_]$, $C_{4,i}[\_]$, $Q_{2,i}$, $\varsigma$, $\tilde a$, $a$, $c$, $x$, such that $\contextB$ does not contain replications above the hole, $C_{3,i}[\_]$ and $C_{4,i}[\_]$ do not bind $x$
and do not contain replications,
$x$ is not free in $C_{4,i}$ and $Q_{2,i}$, and $a$ and $c$ do not occur in
$\contextB$, $Q_2'$, $C_{3,i}[\_]$, $C_{4,i}[\_]$, $Q_{2,i}$, $\varsigma$,
and $\tilde a$.
Let $C_5[\_] = \new{n}.(\_ \mid Q')$ be an adversarial context.
We have $C_5[\Initconf{P'_{2,i}}] = \emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\}$
and similarly $C_5[\Initconf{P_{2,i}}] = \emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}$.
We show that all traces of $\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\}$ are matched by traces of $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}$.
Formally, if $\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\} \rightarrow^* \Conf$,
then one of the following cases occurs:
\begin{enumerate}
\item $\Conf = \emptyset, E', \{ \new{\tilde b'}.(\contextB[\addoutinlet{Q_2'}{a,c,\varsigma}] \mid {}$\\
$\phantom{\Conf = \emptyset, E', \{ \new{\tilde b'}.(}C_{3,i}[\In[a]{x}.C_{4,i}[\Out[c]{x}.Q_{2,i}]]) \} \cup \Pcal$\\[1mm]
$\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{\new{\tilde b}.(\contextB[Q_2'\varsigma] \mid {}$\\
$\phantom{\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{\new{\tilde b}.(}C_{3,i}[C_{4,i}[Q_{2,i}]])\} \cup \Pcal$\\[2mm]
for some $E$, $E'$, $\tilde b$, $\tilde b'$, and $\Pcal$ such that
$\{a,c\} \cap (E \cup \{\tilde b\}) = \emptyset$,
$E' \cup \{\tilde b'\} = E \cup \{\tilde b, a, c\}$,
and $a$ and $c$ do not occur in $\Pcal$.
\item $\Conf = \emptyset, E \cup \{a, c\}, \{ \contextB[\addoutinlet{Q_2'}{a,c,\varsigma}],$\\
$\phantom{\Conf = \emptyset, E \cup \{a, c\}, \{} \contextC[\In[a]{x}.\contextD[\Out[c]{x}.Q_2]]) \} \cup \Pcal$\\[1mm]
$\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{ \contextB[Q_2'\varsigma], \contextC[\contextD[Q_2]] \} \cup \Pcal$\\[2mm]
for some $E$, $\contextB$, $Q_2'$, $\contextC$, $\contextD$, $Q_2$, $\varsigma$, $\Pcal$
such that $\contextB$ does not contain replications above the hole, $\contextC$ and $\contextD$ do not bind $x$
and do not contain replications, $x$ is not free in $\contextD$ and $Q_2$,
and $a$ and $c$ do not occur in
$\contextB$, $Q_2'$, $\contextC$, $\contextD$, $Q_2$, $\Pcal$, $\varsigma$,
and $E$. ($\contextB$, $\varsigma$, and $Q_2$ may be different from the initial ones.)
\item $\Conf = \emptyset, E \cup \{a, c\}, \{ \addinlet{Q_2'}{a,c,\varsigma},$\\
$\phantom{\Conf = \emptyset, E \cup \{a, c\}, \{}
\contextD[\Out[c]{\tuple{M_1, \dots, M_n}}.Q_2] \} \cup \Pcal$\\[1mm]
$\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{ Q_2'\varsigma, \contextD[Q_2] \} \cup \Pcal$\\[2mm]
for some $E$, $Q_2'$, $\contextD$, $Q_2$, $\varsigma$, $M_1$, \dots, $M_n$,
$\Pcal$
such that $\varsigma = ( \subst{M_1}{z_1}, \dots, \subst{M_n}{z_n} )$,
$\contextD$ does not contain replications, and $a$ and $c$ do not occur in
$Q_2'$, $\contextD$, $Q_2$, $\Pcal$, $\varsigma$,
and $E$. ($\varsigma$ and $Q_2$ may be different from the initial ones.)
\item $\Conf = \emptyset, E \cup \{a, c\}, \{ Q_4 \} \cup \Pcal$
and $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\}\rightarrow^* \emptyset, E, \{Q_3\} \cup \Pcal$
for some $E$, $Q_3$, $Q_4$, and $\Pcal$ such that $Q_4 \in \addLets{Q_3}$.
\end{enumerate}
This property is proved by induction on the length of the trace
$\emptyset, \{\tilde n\}, \{P'_{2,i}, Q'\} \rightarrow^* \Conf$.
By inspecting all cases, we conclude that, if
$\emptyset, \allowbreak \{\tilde n\}, \allowbreak \{P'_{2,i}, Q'\} \rightarrow^* \uparrow$,
then $\emptyset, \{\tilde n\}, \{P_{2,i}, Q'\} \rightarrow^* \uparrow$.
Hence, if $P_{2,i}$ satisfies diff-equivalence, then
$P'_{2,i}$ also satisfies diff-equivalence.
So,
if some process in $\stageElimFunc{P}$ satisfies diff-equivalence,
then some process in $\stageElimFunc{P'}$ satisfies diff-equivalence.
\end{proof}
\medskip
\begin{proof}[Proof of Corollary~\ref{cor:boundrepl}]
If a biprocess in $\stageElimFunc{P}$ satisfies diff-equivalence,
then by Proposition~\ref{prop:bounded-repl},
a biprocess in $\stageElimFunc{\context[!^n Q_{\textnormal{nobar}}]}$ satisfies diff-equivalence,
so by Proposition~\ref{prop:syncelim} applied several times,
a biprocess in $\stageElimFunc{P'(n)}$ satisfies diff-equivalence,
so by Theorem~\ref{theorem:Bruno},
a biprocess in $\stageElimFunc{P'(n)}$ satisfies observational equivalence,
so by Theorem~\ref{thm:soundnessSwapping},
$P'(n)$ satisfies observational equivalence.
\end{proof}
%\input{app-DKR}
\fi
\bibliographystyle{IEEEtran}
\bibliography{thesis}
```