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 ∣ Q$ and $P^{'} ∣ 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, Lee et al., and Juels, Catalano & Jakobsson, and in the vehicular ad-hoc network by Freudiger et al.

Keywords

Applied pi calculus automated reasoning ballot secrecy barrier synchronisation equivalence e-voting privacy receipt-freeness

1. 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 [36,39,54], ideal functionality [4,5,38], and stronger notions of secrecy [1,14,33]. 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 ≈. 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 $\begin{matrix} (1) & V (A, v) ∣ V (B, v^{'}) \approx V (A, v^{'}) ∣ V (B, v) \end{matrix}$ which means that no adversary can distinguish when two voters swap their votes [39]. (We use the applied pi calculus syntax and terminology [4], which we introduce in Section 2.)

1.1. Approaches to proving equivalences

Observational equivalence is the tool introduced for reasoning about security requirements of cryptographic protocols in the spi calculus [5] and in the applied pi calculus [4]. It was originally proved manually, using the notion of labelled bisimilarity [4,6,22] 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 [21,40] 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 [44,48], 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 [32]. These decision procedures are too complex for useful implementations. Practical algorithms have since been proposed and implemented: SPEC [60] for fixed primitives and without else branches, APTE [26] for fixed primitives with else branches and non-determinism, and AKISS [24,31] for a wide variety of primitives and determinate processes.

For an unbounded number of sessions, proving equivalence is an undecidable problem [3,48], 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 [18]. 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 [57] and Tamarin [11] also use that notion, and Baudet [13] showed that diff-equivalence is decidable for a bounded number of sessions and used this technique for proving resistance against off-line guessing attacks [12]. To deal with limitations of diff-equivalence, other sufficient conditions have been designed for particular classes of equivalences, e.g., anonymity and unlinkability [47] and ballot secrecy [35]. These conditions can be checked automatically using tools such as ProVerif. The definition of ballot secrecy in [35] is based on trace equivalence and its relationship with (1) is unknown. 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 [29], which is too complex for useful implementation, and for ping-pong protocols [30], which is implemented in a tool.

1.2. Diff-equivalence and its limitations

In this paper, we focus on proofs of observational equivalence in the applied pi calculus. The main approach to automate proofs of observational equivalence with an unbounded number of sessions is to use diff-equivalence. (In our motivating example (1), a bounded number of sessions is sufficient, but an unbounded number becomes useful in more complex examples, as in Section 4.2.) Diff-equivalence seems well-suited to our motivating example, since the processes $V (A, v) ∣ V (B, v^{'})$ and $V (A, v^{'}) ∣ 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 $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 = V (A, diff [v, v^{'}]) ∣ V (B, diff [v^{'}, v])$ . The two processes represented by a biprocess P are recovered by $fst (P)$ and $snd (P)$ . Hence, $fst (P) = V (A, v) ∣ V (B, v^{'})$ and $snd (P) = V (A, v^{'}) ∣ V (B, v)$ .

Diff-equivalence implies observational equivalence. Hence, the equivalence (1) can be inferred from the diff-equivalence of the biprocess P. 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} ⟨ v ⟩$ . Thus, ballot secrecy can be analysed using the biprocess $P = \overline{c} ⟨ diff [v, v^{'}] ⟩ ∣ \overline{c} ⟨ diff [v^{'}, v] ⟩$ . It is trivial to see that $fst (P) = \overline{c} ⟨ v ⟩ ∣ \overline{c} ⟨ v^{'} ⟩$ is indistinguishable from $snd (P) = \overline{c} ⟨ v^{'} ⟩ ∣ \overline{c} ⟨ v ⟩$ , because any output by $fst (P)$ can be matched by an output from $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} ⟨ diff [v, v^{'}] ⟩$ and $\overline{c} ⟨ diff [v^{'}, v] ⟩$ , each satisfy diff-equivalence, which is false, because $\overline{c} ⟨ v ⟩$ is not equivalent to $\overline{c} ⟨ v^{'} ⟩$ (nor is $\overline{c} ⟨ v^{'} ⟩$ equivalent to $\overline{c} ⟨ v ⟩$ ).

Overcoming the difficulty encountered in Example 1 is straightforward: using the general property that $P ∣ Q \approx Q ∣ P$ , we can instead prove $V (A, v) ∣ V (B, v^{'}) \approx V (B, v) ∣ V (A, v^{'})$ , 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} = \overline{c} ⟨ diff [v, v] ⟩ ∣ \overline{c} ⟨ diff [v^{'}, v^{'}] ⟩$ trivially satisfies diff-equivalence, since $fst (\hat{P}) = 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 [10,39], vehicular ad-hoc networks [36,37], and anonymity networks [27,54,55]) 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} ⟨ A ⟩ . \overline{c} ⟨ v ⟩$ . This example does not satisfy ballot secrecy, because $V (A, v) ∣ V (B, v^{'})$ can output A, v, B, $v^{'}$ on channel c in that order, while $V (A, v^{'}) ∣ 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 [9,23,46,53].
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} ⟨ A ⟩ .1 : : \overline{c} ⟨ v ⟩$ , where $1 : :$ is a barrier synchronisation. Ballot secrecy can then be analysed using biprocess $P_{ex} = \overline{c} ⟨ A ⟩ .1 : : \overline{c} ⟨ diff [v, v^{'}] ⟩ ∣ \overline{c} ⟨ B ⟩ .1 : : \overline{c} ⟨ diff [v^{'}, v] ⟩$ . Synchronisation ensures the output of A and B, prior to v and $v^{'}$ , in both $fst (P_{ex})$ and $snd (P_{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_{ex}^{'} = \overline{c} ⟨ diff [A, B] ⟩ .1 : : \overline{c} ⟨ v ⟩ ∣ \overline{c} ⟨ diff [B, A] ⟩ .1 : : \overline{c} ⟨ v^{'} ⟩$ , which does not satisfy diff-equivalence. Intuitively, we need to swap at the barrier, not at the beginning (cf. $P_{ex}^{'}$ ). In essence, by swapping data between the two voting processes at the barrier, it suffices to prove that the biprocess $P_{ex}^{″} = \overline{c} ⟨ A ⟩ .1 : : \overline{c} ⟨ diff [v, v] ⟩ ∣ \overline{c} ⟨ B ⟩ .1 : : \overline{c} ⟨ diff [v^{'}, v^{'}] ⟩$ satisfies diff-equivalence, which trivially holds since $fst (P_{ex}^{″}) = snd (P_{ex}^{″})$ .

As illustrated in Examples 1 and 3, 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.
1.3. Contributions

First, we extend the process calculus by Blanchet, Abadi & Fournet [18] to capture barriers (Section 2). Secondly, we formally define a compiler that encodes barriers and swapping using private channel communication (Section 3). 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. 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 4).

This manuscript mainly differs from its conference version [19] by the inclusion of proofs and additional examples and explanations.

1.4. Comparison with Smyth et al.

The idea of swapping data at barriers was informally introduced by Delaune, Ryan & Smyth [41,58]. 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 [59, Chapter 5], and Klus, Smyth & Ryan implemented that preliminary compiler [50]. The preliminary compiler differs from the one presented here; moreover, it was not proved sound. In contrast, we prove that the compiler we have implemented in ProVerif is sound.)

2. Process calculus

We recall Blanchet, Abadi & Fournet’s dialect [18] of the applied pi calculus [4,56]. This dialect is particularly useful due to the automated support provided by ProVerif [17,20]. The semantics of the applied pi calculus [4] and the dialect of [18] were defined using structural equivalence. Those semantics have been simplified by semantics with configurations and without structural equivalence, first for trace properties [2], then for equivalences [8,13,15]. 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.

Fig. 1.

Syntax for terms and processes.

2.1. 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 ${M / x}$ replace x with M. Arbitrarily large substitutions can be written as ${M_{1} / x_{1}, \dots, M_{n} / x_{n}}$ and the letters σ and τ range over substitutions. We write $M σ$ for the result of applying σ to the variables of M. Similarly, renamings ${u / 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 $def (g)$ of rewrite rules $g (M_{1}^{'}, \dots, M_{l}^{'}) \to M^{'}$ , where $M_{1}^{'}, \dots, M_{l}^{'}, M^{'}$ are terms that contain only constructors and variables, the variables of $M^{'}$ must be bound in $M_{1}^{'}, \dots, M_{l}^{'}$ , and variables are subject to renaming. The evaluation of expression $g (M_{1}, \dots, M_{l})$ succeeds if there exists a rewrite rule $g (M_{1}^{'}, \dots, M_{l}^{'}) \to M^{'}$ in $def (g)$ and a substitution σ such that $M_{i} = M_{i}^{'} σ$ for all $i \in {1, \dots, l}$ , and in this case $g (M_{1}, \dots, M_{l})$ evaluates to $M^{'} σ$ . In order to avoid distinguishing constructors and destructors in the semantics of expressions, we let $def (f)$ be ${f (x_{1}, \dots, x_{l}) \to f (x_{1}, \dots, x_{l})}$ , where f is a constructor of arity l. In particular, we use n-ary constructors $(| M_{1}, \dots, M_{n} |)$ for tuples, and unary destructors $π_{i, n}$ for projections, with the rewrite rule $π_{i, n} ((| x_{1}, \dots, x_{n} |)) \to x_{i}$ for all $i \in {1, \dots, n}$ . ProVerif supports both rewrite rules and equations [18]; we omit equations in this paper for simplicity. Our proofs can be extended to equations, and our implementation supports them.1

¹
Only a few rules of the operational semantics need to be adapted to equations, as in [17, Section 2.5.1]; the definition of our compiler and many parts of the proofs remain unchanged. A tricky point is that, with equations, the evaluation of expressions may introduce names that do not appear in the initial expression, and these names may collide with other names. There are several ways to solve this technical issue, either by considering a representative in which these names are renamed to avoid such collisions or by restricting ourselves to the equational theories that ProVerif supports, in which the equations can be oriented to avoid such introduction of names. Adapting the proofs to equations is otherwise straightforward.

The grammar for processes is presented in Fig. 1. The process $let x = D in P 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 $if M = N then P else Q$ as $let x = eq (M, N) in P else Q$ , where x is a fresh variable, $eq$ is a binary destructor, and $def (eq) = {eq (y, y) \to y}$ ; we always include $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 [14,15,18]), except for barriers, which we explain next.

Our syntax allows processes to contain barriers $t : : P$ , where $t \in N$ . Intuitively, $t : : P$ blocks P until all processes running in parallel are ready to synchronise at barrier t. In addition, barriers are ordered, so $t : : P$ is also blocked if there are any barriers $t^{'}$ such that $t^{'} < t$ . Blanchet, Abadi & Fournet [18, Section 8] also introduced a notion of synchronisation, named stages. A stage synchronisation can occur at any point, by dropping processes that did not complete the previous stage. By comparison, a barrier synchronisation cannot drop processes. For example, in the process $\overline{c} ⟨ k ⟩ .1 : : \overline{c} ⟨ m ⟩ ∣ 1 : : \overline{c} ⟨ n ⟩$ , the barrier synchronisation cannot occur before the output of k. It follows that the process cannot output n without having previously output k. In contrast, with stage synchronisation, either k is output first, then the process moves to the next stage, then it may output m and n, or the process immediately moves to the next stage by dropping $\overline{c} ⟨ k ⟩ .1 : : \overline{c} ⟨ m ⟩$ , so it may output n without any other output. Our notion of barrier is essential when processes must not be dropped. In particular, it is necessary for proving equivalence properties that require swapping data between two processes, because we must not drop one of these processes.

Given a process P, the multiset $barriers (P)$ collects all barriers that occur in P. Thus, $barriers (t : : Q) = {t} \cup barriers (Q)$ and in all other cases, $barriers (P)$ is the multiset union of the barriers of the immediate subprocesses of P. We naturally extend the function $barriers$ to multisets $P$ of processes by $barriers (P) = ⋃_{P \in P} barriers (P)$ . For each barrier t, the number of processes that must synchronise is equal to the number of elements t in $barriers (P)$ . It follows that the number of barriers which must be reached is defined in advance of execution, and thus branching behaviour may cause blocking. For example, the process $c (x) . if x = k then 1 : : \overline{c} ⟨ m ⟩ else \overline{c} ⟨ n ⟩ ∣ 1 : : \overline{c} ⟨ s ⟩$ contains two barriers that must synchronise. However, when the term bound to x is not k, the else branch is taken and one of the barriers is dropped, so only one barrier remains. In this case, barrier synchronisation blocks forever, and the process never outputs s. The occurrence of barriers under replication is explicitly forbidden, because with barriers under replication, the number of barriers that we need to synchronise is ill-defined. We partly overcome this limitation in Section 3.5.1.

The scope of names and variables is delimited by binders $ν n$ , $M (x)$ , and let $x = D$ in. The set of free names $fn (P)$ contains every name n in P which is not under the scope of the binder $ν n$ . The set of free variables $fv (P)$ contains every variable x in P which is not under the scope of a message input $M (x)$ or an expression evaluation let $x = D$ in. Using similar notation, the set of names in a term M is denoted $fn (M)$ and the set of variables in a term M is denoted $fv (M)$ . We naturally extend these functions to multisets $P$ of processes by $fn (P) = ⋃_{P \in P} fn (P)$ and $fv (P) = ⋃_{P \in P} fv (P)$ . A term M is ground if $fv (M) = \emptyset$ , a substitution ${M / x}$ is ground if M is ground, and a process P is closed if $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.

Fig. 2.

Operational semantics.

The operational semantics is defined by reduction (→) on configurations. A configuration $C$ is a triple $B, E, P$ , where B is a finite multiset of integers, E is a finite set of names, and $P$ is a finite multiset of closed processes. The multiset B contains the barriers that control the synchronisation of processes in $P$ . The set E is initially empty and is extended to include any names introduced during reduction, namely, those names introduced by $(R ED R ES)$ . When $E = {\tilde{a}}$ and $P = {P_{1}, \dots, P_{n}}$ , the configuration $B, E, P$ intuitively stands for $ν \tilde{a} . (P_{1} ∣ \dots ∣ P_{n})$ . We consider configurations as equal modulo any renaming of the names in $E, P$ that leaves $fn (P) ∖ E$ unchanged. The initial configuration for a closed process P is $C_{init} (P) = barriers (P), \emptyset, {P}$ . Figure 2 defines reduction rules for each construct of the language. The rule $(R ED R EPL)$ creates a new copy of the replicated process P. The rule $(R ED R ES)$ reduces $ν n$ by creating a fresh name $n^{'}$ , adding it to E, and substituting it for n. The rule $(R ED I / O)$ performs communication: the term M sent by $\overline{N} ⟨ M ⟩ . P$ is received by $N (x) . Q$ , and substituted for x. The rules $(R ED D ESTR 1)$ and $(R ED D ESTR 2)$ treat expression evaluations. They first evaluate D, using the relation $D ⇓ M$ , which means that the expression D evaluates to the term M, and is also defined in Fig. 2. When this evaluation succeeds, $(R ED D ESTR 1)$ substitutes the result M for x and runs P. When it fails, $(R ED D ESTR 2)$ runs Q. Finally, the new rule $(R ED B AR)$ performs barrier synchronisation: it synchronises on the lowest barrier t in B. If t occurs n times in B, it requires n processes $t : : P_{1}, \dots, t : : 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, P$ is valid when $barriers (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 4.

Let us consider the parallel composition of processes $P = \overline{c} ⟨ k ⟩ .1 : : c (x)$ , $Q = ν n .1 : : \overline{c} ⟨ n ⟩$ , and $R = c (x)$ , which yields the initial configuration ${1^{2}}, \emptyset, {P ∣ Q ∣ R}$ , since the process $P ∣ Q ∣ R$ contains two barriers 1. We have $\begin{array}{l} by (R ED P AR) & {1^{2}}, \emptyset, {P ∣ Q ∣ R} & \overset{}{\to} {1^{2}}, \emptyset, {P, Q ∣ R} \\ by (R ED P AR) & \overset{}{\to} {1^{2}}, \emptyset, {P, Q, R} \\ by (R ED I / O) & \overset{}{\to} {1^{2}}, \emptyset, {1 : : c (x), Q, 0} \\ by (R ED N IL) & \overset{}{\to} {1^{2}}, \emptyset, {1 : : c (x), Q} \\ by (R ED R ES) & \overset{}{\to} {1^{2}}, {n^{'}}, {1 : : c (x), 1 : : \overline{c} ⟨ n^{'} ⟩} \\ by (R ED B AR) & \overset{}{\to} \emptyset, {n^{'}}, {c (x), \overline{c} ⟨ n^{'} ⟩} \\ by (R ED I / O) & \overset{}{\to} \emptyset, {n^{'}}, {0, 0} \\ by (R ED N IL) & \overset{}{\to} \emptyset, {n^{'}}, {0} \\ by (R ED N IL) & \overset{}{\to} \emptyset, {n^{'}}, \emptyset \end{array}$ First, the parallel compositions are expanded (by $(R ED P AR)$ ), then process P sends k to process R, on channel c (first reduction $(R ED I / O)$ ), and a fresh name $n^{'}$ is created by reducing $ν n$ (by $(R ED R ES)$ ). These steps must happen before barrier synchronisation, by $(R ED B AR)$ . After that synchronisation, the communication between $c (x)$ and $\overline{c} ⟨ n^{'} ⟩$ can happen (second reduction $(R ED I / O)$ ).

The semantics permits synchronisation on barrier t, immediately followed by synchronisation on barrier $t + 1$ . For instance, ${1^{2}, 2}, \emptyset, {1 : : c (x) ∣ 1 : : \overline{c} ⟨ n ⟩ ∣ 2 : : \overline{c} ⟨ m ⟩}$ reduces to $\emptyset, \emptyset, {c (x), \overline{c} ⟨ n ⟩, \overline{c} ⟨ m ⟩}$ (by (Red Par) twice and (Red Bar) twice). Hence, communication between $c (x)$ and $\overline{c} ⟨ n ⟩$ , or $c (x)$ and $\overline{c} ⟨ m ⟩$ is possible. To prevent the latter communication, process $1 : : c (x) .2 : : 0 ∣ 1 : : \overline{c} ⟨ n ⟩ .2 : : 0 ∣ 2 : : \overline{c} ⟨ m ⟩$ can be considered.

2.2. Observational equivalence

Intuitively, configurations $C$ and $C^{'}$ 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. [8] 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 $ν \tilde{n} . (_∣ Q)$ with $fv (Q) = \emptyset$ and $barriers (Q) = \emptyset$ . When $C = B, E, P$ and $C [_] = ν \tilde{n} . (_∣ Q)$ is an adversarial context, we define $C [C] = B, E \cup {\tilde{n}}, P \cup {Q}$ , after renaming the names in $E, P$ so that $E \cap fn (Q) = \emptyset$ . A configuration $C = B, E, P$ can output on a channel N, denoted, $C ↓_{N}$ , if there exists $\overline{N} ⟨ M ⟩ . P \in P$ with $fn (N) \cap E = \emptyset$ , for some term M and process P.

Definition 1 (Observational equivalence).

Observational equivalence between configurations ≈ is the largest symmetric relation $R$ between valid configurations such that $C R C^{'}$ implies:

for all N, if $C ↓_{N}$ , then $C^{'} {\overset{}{\to}}^{*} C^{″}$ and $C^{″} ↓_{N}$ for some $C^{″}$ ;

if $C \to C_{1}$ , then $C^{'} \to^{*} C_{1}^{'}$ and $C_{1} R C_{1}^{'}$ for some $C_{1}^{'}$ ;

$C [C] R C [C^{'}]$ for all adversarial contexts $C [_]$ .

Closed processes P and $P^{'}$ are observationally equivalent, denoted $P \approx P^{'}$ , if $C_{init} (P) \approx C_{init} (P^{'})$ .

The definition first formulates observational equivalence on semantic configurations. Item 1 guarantees that, if a configuration $C$ outputs on a public channel, then so does $C^{'}$ . 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.

2.3. 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 $diff [M, M^{'}]$ is a term and $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 $fst (P)$ and $snd (P)$ as follows: $fst (P)$ is obtained by replacing all occurrences of $diff [M, M^{'}]$ with M and $snd (P)$ is obtained by replacing $diff [M, M^{'}]$ with $M^{'}$ . We define $fst (D)$ , $fst (M)$ , $snd (D)$ , and $snd (M)$ similarly, and naturally extend these functions to multisets of biprocesses by $fst (P) = {fst (P) ∣ P \in P}$ and $snd (P) = {snd (P) ∣ P \in P}$ , and to configurations by $fst (B, E, P) = B, E, fst (P)$ and $snd (B, E, P) = B, E, snd (P)$ . The standard definitions of $barriers$ , free names, and free variables apply to biprocesses as well. Adversarial contexts do not contain $diff$ . Observational equivalence can be formalised as a property of biprocesses:

Fig. 3.

Generalised semantics for biprocesses.

Definition 2.

A closed biprocess P satisfies observational equivalence if $fst (P) \approx snd (P)$ .

The semantics for biprocesses includes the rules in Fig. 2, except for (Red I/O), (Red Destr 1), and (Red Destr 2) which are revised in Fig. 3. It follows from this semantics that, if $C \overset{}{\to} C^{'}$ , then $fst (C) \overset{}{\to} fst (C^{'})$ and $snd (C) \overset{}{\to} snd (C^{'})$ . In other words, a biprocess reduces when the two underlying processes reduce in the same way. However, reductions in $fst (C)$ or $snd (C)$ do not necessarily imply reductions in $C$ , that is, there exist configurations $C$ such that $fst (C) \overset{}{\to} fst (C^{'})$ , but there is no such reduction $C \overset{}{\to} C^{'}$ , and symmetrically for $snd (C)$ . For example, given the configuration $C = \emptyset, \emptyset, {\overline{diff [a, c]} ⟨ n ⟩ .0, a (x) .0}$ , we have $fst (C) \overset{}{\to} \emptyset, \emptyset, {0, 0}$ , but there is no reduction $C \overset{}{\to} \emptyset, \emptyset, {0, 0}$ . Formally, this behaviour can be captured using the divergence relation (↑) for configurations (Fig. 4) [13]. Divergence can occur because either: (i) one process can perform a communication and the other cannot, by rule $(D IV I / O)$ ; or (ii) the evaluation of an expression succeeds in one process and fails in the other, by rule $(D IV D ESTR)$ . Using the notion of diff-equivalence (Definition 3), Theorem 1 shows that a biprocess P satisfies observational equivalence when reductions in $C [C_{init} (fst (P))]$ or $C [C_{init} (snd (P))]$ imply reductions in $C [C_{init} (P)]$ for all adversarial contexts $C [_]$ , that is, configurations obtained from $C [C_{init} (P)]$ never diverge.

Fig. 4.

Semantics for divergence.

Definition 3 (Diff-equivalence).

A closed biprocess P satisfies diff-equivalence if for all adversarial contexts $C [_]$ , there is no configuration $C$ such that $C [C_{init} (P)] {\overset{}{\to}}^{*} C$ and $C ↑$ .

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 easily adapting the result of Blanchet [17, Theorem 3.5]. This result itself adapts the result of Blanchet, Abadi & Fournet [18, Theorem 1], initially presented with a semantics based on structural equivalence and reduction, to a semantics based on reduction on configurations.
Example 5.
Let us revisit Example 1. Formally, the biprocess $P = \overline{c} ⟨ diff [v, v^{'}] ⟩ ∣ \overline{c} ⟨ diff [v^{'}, v] ⟩$ does not satisfy diff-equivalence, because the context $C [_] =_∣ c (x) . if x = v then \overline{c} ⟨ n ⟩$ causes divergence: $\begin{array}{l} C [C_{init} (P)] & = \emptyset, \emptyset, {\overline{c} ⟨ diff [v, v^{'}] ⟩ ∣ \overline{c} ⟨ diff [v^{'}, v] ⟩, c (x) . if x = v then \overline{c} ⟨ n ⟩} \\ {\overset{}{\to}}^{} C = \emptyset, \emptyset, {0, \overline{c} ⟨ diff [v^{'}, v] ⟩, if diff [v, v^{'}] = v then \overline{c} ⟨ n ⟩} \end{array}$ by (Red Par) and (Red I/O), and $C ↑$ by (Div Destr). (Recall that the conditional is encoded as a destructor application.)

We can revisit Example 3 similarly. The biprocess $P_{ex} = \overline{c} ⟨ A ⟩ .1 : : \overline{c} ⟨ diff [v, v^{'}] ⟩ ∣ \overline{c} ⟨ B ⟩ .1 : : \overline{c} ⟨ diff [v^{'}, v] ⟩$ does not satisfy diff-equivalence, because the context $C [_] =_∣ c (x) . c (y) . c (z) . if z = v then \overline{c} ⟨ n ⟩$ causes divergence: $\begin{array}{l} C [C_{init} (P)] & = {1^{2}}, \emptyset, {P_{ex}, c (x) . c (y) . c (z) . if z = v then \overline{c} ⟨ n ⟩} \\ by (R ED P AR) (R ED I / O) & {\overset{}{\to}}^{} {1^{2}}, \emptyset, {1 : : \overline{c} ⟨ diff [v, v^{'}] ⟩, 1 : : \overline{c} ⟨ diff [v^{'}, v] ⟩, c (z) . if z = v then \overline{c} ⟨ n ⟩} \\ by (R ED B AR) & \overset{}{\to} \emptyset, \emptyset, {\overline{c} ⟨ diff [v, v^{'}] ⟩, \overline{c} ⟨ diff [v^{'}, v] ⟩, c (z) . if z = v then \overline{c} ⟨ n ⟩} \\ by (R ED I / O) & \overset{}{\to} C = \emptyset, \emptyset, {0, \overline{c} ⟨ diff [v^{'}, v] ⟩, if diff [v, v^{'}] = v then \overline{c} ⟨ n ⟩} \end{array}$ and $C ↑$ as above.
Remark.
We do not allow adversarial contexts to contain barriers. In general, allowing them would enable an adversary to distinguish more processes. For instance, the processes $P = \overline{c} ⟨ n ⟩ . \overline{c} ⟨ m ⟩$ and $Q = \overline{c} ⟨ n ⟩ .1 : : \overline{c} ⟨ m ⟩$ are observationally equivalent with our definition, because the barrier 1 can be executed immediately after outputting n. However, the context $C [_] =_∣ c (x) . c (y) .1 : : \overline{d} ⟨ a ⟩$ would distinguish them: $C [C_{init} (P)] = {1}, \emptyset, {\overline{c} ⟨ n ⟩ . \overline{c} ⟨ m ⟩, c (x) . c (y) .1 : : \overline{d} ⟨ a ⟩} {\overset{}{\to}}^{} \emptyset, \emptyset, {\overline{d} ⟨ a ⟩} ↓_{d}$ , while there is no $C$ such that $C [C_{init} (Q)] = {1^{2}}, \emptyset, {\overline{c} ⟨ n ⟩ .1 : : \overline{c} ⟨ m ⟩, c (x) . c (y) .1 : : \overline{d} ⟨ a ⟩} {\overset{}{\to}}^{} C ↓_{d}$ because the input $c (y)$ cannot be reduced. In contrast, for trace properties, including diff-equivalence, which is a trace property on biprocesses, allowing barriers in adversarial contexts does not give more power to the adversary, because barriers only constrain the possible traces.
3. Automated reasoning

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:

Function $annotate$ annotates barriers with the data to be swapped and channels for sending and receiving such data.

Function $elim - and - swap$ 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 data back to a different barrier.

We introduce annotated barriers (Section 3.1) and define these two steps (Sections 3.2 and 3.3) below. By combining these two steps we obtain our compiler (Section 3.4), which we have implemented in ProVerif (http://proverif.inria.fr/), as of version 1.94. 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.

3.1. Process calculus with annotated barriers

We introduce an annotated barrier construct $t [a, c, ς] : : P$ , which is not present in the syntax introduced in Section 2, 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.2

²
The use of distinct channels helps avoid an incompleteness issue of ProVerif. In essence, ProVerif overapproximates a private channel as a set of messages: an input on a private channel a may receive any message sent on a at any point, in any order. By using distinct channels for barriers, we make sure that there is a single output and a single input for each private channel, so we reduce the effect of this overapproximation to a minimum.

Moreover, the ordered substitution

ς = (M_{1} / x_{1}, \dots, 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 ς is similar to a substitution, except that the elements

M_{1} / x_{1}, \dots, M_{n} / x_{n}

are ordered. (We indicate ordering using parentheses instead of braces.) The ordering is used to designate each variable in the domain unambiguously. We define

dom (ς) = {x_{1}, \dots, x_{n}}

and

range (ς) = {M_{1}, \dots, M_{n}}

. As usual, we require that

fv (range (ς)) \cap dom (ς) = \emptyset

. The annotated barrier

t [a, c, ς] : : P

binds the variables in the domain of ς in P, so we extend the functions

fn

and

fv

to annotated barriers as follows:

\begin{array}{l} fn (t [a, c, ς] : : P) = {a, c} \cup fn (range (ς)) \cup fn (P) \\ fv (t [a, c, ς] : : P) = fv (range (ς)) \cup (fv (P) ∖ dom (ς)) \end{array}

We define the ordered domain of ς,

ordom (ς) = (x_{1}, \dots, x_{n})

, as the tuple containing the variables in the domain of ς, in the same order as in the definition of ς.

We also introduce a domain-barrier construct $t [a, c, \tilde{x}] : : P$ , which is similar to an annotated barrier except that the ordered substitution ς is replaced with a tuple of variables $\tilde{x} = (x_{1}, \dots, x_{n})$ corresponding to the ordered domain of ς. Domain-barriers occur in $barriers (P)$ , but not in processes. We extend function $barriers$ to annotated barriers as follows: $\begin{array}{l} barriers (t [a, c, ς] : : P) = {t [a, c, ordom (ς)] : : P} \cup barriers (P) \end{array}$ Hence, function $barriers$ maps processes to multisets of domain-barriers and integers, and domain-barriers include the process that follows the barrier itself. In addition, we extend $fst$ and $snd$ for configurations as follows: $fst (t [a, c, \tilde{x}] : : P) = t [a, c, \tilde{x}] : : fst (P)$ and $fst (B, E, P) = fst (B), E, fst (P)$ , and similarly for $snd$ .

We introduce the function $channels (B) = {a ∣ t [a, c, \tilde{x}] : : P \in B} \cup {c ∣ t [a, c, \tilde{x}] : : P \in B}$ to recover the multiset of names used by the domain-barriers in B. We implicitly cast $channels (B)$ into a set when we take the intersection with a set, test the inclusion with a set, or use it as a set of names E inside a configuration $B, E, P$ . We also define the function $fn - nobc$ , which returns the free names excluding the channels of barriers, by $fn - nobc (t [a, c, ς] : : P) = fn (range (ς)) \cup fn - nobc (P)$ and, for all other processes, $fn - nobc (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 $C_{init} (P) = barriers (P), channels (barriers (P)), {P}$ . We consider configurations $B, E, P$ with annotated barriers as equal modulo any renaming of the names in $B, E, P$ that leaves $fn (P) ∖ E$ unchanged.

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 (Section 3.2); 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.

Definition 4 (Validity).

A process P is valid if it is closed, $channels (barriers (P)) \cap fn - nobc (P) = \emptyset$ , the elements of $channels (barriers (P))$ are pairwise distinct, and for all annotated barriers in P such that $P = C [t [a, c, ς] : : Q]$ , we have $fv (Q) \subseteq dom (ς)$ and $C [_]$ does not bind a, c, nor the names in $fn (Q)$ above the hole.

A configuration $B, E, P$ is valid if $barriers (P) \subseteq B$ , $channels (B) \subseteq E$ , all processes in $P$ are valid, the elements of $channels (B)$ are pairwise distinct, and $channels (B) \cap fn - nobc (P) = \emptyset$ .

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 fn - nobc (P) = \emptyset$ ; $channels (B) \cap fn - nobc (P) = \emptyset$ ), and free in the processes (for all annotated barriers in P such that $P = C [t [a, c, ς] : : Q]$ , $C [_]$ 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 $t [a, c, ς] : : Q$ , we require that $fv (Q) \subseteq dom (ς)$ 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 $t [a, c, ς] : : Q$ is contained in the ordered substitution ς. The process Q refers to this state using variables in $dom (ς)$ . We consider only valid configurations; Lemma 2 below justifies this point.

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{array}{l} B, E, P \cup {t : : P_{1}, \dots, t : : P_{m}, t [a_{m + 1}, c_{m + 1}, ς_{m + 1}] : : P_{m + 1}, \dots, t [a_{n}, c_{n}, ς_{n}] : : P_{n}} \\ (R ED B AR^{'}) & \to B^{'}, E, P \cup {P_{1}, \dots, P_{m}, P_{m + 1} ς_{m + 1}, \dots, P_{n} ς_{n}} \end{array}$ where $0 ⩽ m ⩽ n$ , $1 ⩽ n$ , $B = {t^{m}, t [a_{m + 1}, c_{m + 1}, ordom (ς_{m + 1})] : : P_{m + 1}, \dots, t [a_{n}, c_{n}, ordom (ς_{n})] : : P_{n}} \cup B^{'}$ , and for all $t^{'}$ such that $t^{'} ⩽ t$ , $t^{'}$ does not appear in $B^{'}$ , i.e., $t^{'} \notin B^{'}$ and $t^{'} [_] : :_\notin B^{'}$ . When all barriers are standard, this rule reduces to $(R ED B AR)$ .

The next lemma allows us to show that all considered configurations are valid.

Lemma 2.
If P is a valid process, then $C_{init} (P)$ is valid. Validity is preserved by reduction, by application of an adversarial context, and by application of $fst$ and $snd$ .

The proof of Lemma 2 is detailed in Appendix B.

We refer to processes in which all barriers are annotated as annotated processes, and processes in which all barriers are standard as standard processes.
3.2. Barrier annotation

Next, we define the first step of our compiler, which annotates barriers with additional information.

Definition 5.
We define function $annotate$ , from standard processes to annotated processes, as follows: $annotate$ transforms $C [t : : Q]$ into $C [t [a, c, ς] : : Q^{'}]$ , where $C [_]$ is any context without replication above the hole, a and c are distinct fresh names, and $(Q^{'}, ς) = split (Q)$ , where the function $split$ 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 $t : : Q$ are already annotated and barriers inside Q are standard.

The function $split$ is defined by $split (Q) = (Q^{'}, ς)$ where $Q^{'}$ is a process and $ς = (M_{1} / x_{1}, \dots, M_{n} / x_{n})$ is an ordered substitution such that terms $M_{1}, \dots, M_{n}$ are the largest subterms of Q that do not contain names or variables bound in Q, variables $x_{1}, \dots, x_{n}$ are fresh, and process $Q^{'}$ is obtained from Q by replacing each $M_{i}$ with $x_{i}$ , so that $Q = Q^{'} ς$ . Moreover, the variables $x_{1}, \dots, x_{n}$ occur in this order in $Q^{'}$ when read from left to right.

Intuitively, the function $split$ separates a process Q into its “skeleton” $Q^{'}$ (a process with variables as placeholders for data) and associated data in the ordered substitution ς. 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 $split$ guarantees that the ordering of variables in the domain of ς is consistent among the various subprocesses. This ordering of variables and the fact that $M_{1}, \dots, M_{n}$ are the largest possible subterms allows the checks in the definition of our compiler (see definition of function $swapper$ in Section 3.3) to succeed more often, and hence increases opportunities for swapping.
Example 6.
We have $\begin{array}{l} split (\overline{c} ⟨ diff [v, v^{'}] ⟩) = (\overline{x} ⟨ y ⟩, (c / x, diff [v, v^{'}] / y)) \\ split (\overline{c} ⟨ diff [v^{'}, v] ⟩) = (\overline{x^{'}} ⟨ y^{'} ⟩, (c / x^{'}, diff [v^{'}, v] / y^{'})) \end{array}$ The process $\overline{c} ⟨ diff [v, v^{'}] ⟩$ is separated into its skeleton $Q^{'} = \overline{x} ⟨ y ⟩$ and the ordered substitution $ς = (c / x, diff [v, v^{'}] / y)$ , which defines the values of the variables x and y such that $\overline{c} ⟨ diff [v, v^{'}] ⟩ = Q^{'} ς$ . The process $\overline{c} ⟨ diff [v^{'}, v] ⟩$ is separated similarly. Using these results, $annotate (P_{ex})$ is defined as $\begin{array}{l} \overline{c} ⟨ A ⟩ .1 [a, b, (c / x, diff [v, v^{'}] / y)] : : \overline{x} ⟨ y ⟩ ∣ \overline{c} ⟨ B ⟩ .1 [a^{'}, b^{'}, (c / x^{'}, diff [v^{'}, v] / y^{'})] : : \overline{x^{'}} ⟨ y^{'} ⟩ \end{array}$ where $a, a^{'}, b, b^{'}$ are fresh names. That is, $annotate (P_{ex})$ is derived by annotating the two barriers in $P_{ex}$ . (Process $P_{ex}$ is given in Example 3.)

The function $split$ can also be formally defined as $split (Q) = split (\emptyset, Q)$ with the definition of $split (U, Q)$ by structural induction on Q given in Fig. 5. 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 $split (\emptyset, Q_{0})$ , in each recursive call $split (U, Q)$ , the set U contains all bound names and variables at the subprocess Q in $Q_{0}$ . Each call to $split (U, Q)$ returns $(Q^{'}, ς)$ 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 $ς = (M_{1} / x_{1}, \dots, M_{n} / x_{n})$ . When Q is a term M, $split (U, Q) = split (U, M)$ behaves as follows

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 $ς = (M / x)$ , hence $split (U, M) = (x, (M / x))$ (rule R1 of Fig. 5).

If M is a variable in U, then it is left unchanged, hence $split (U, u) = (u, \emptyset)$ (rule R2).

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: $split (U, M) = (f (M_{1}^{'}, \dots, M_{n}^{'}), ς_{1} + \dots + ς_{n})$ where for all $i ⩽ n$ , $split (U, M_{i}) = (M_{i}^{'}, ς_{i})$ (rule R3 with context 9). If M is a constructor application $M = f (M_{1}, \dots, M_{n})$ that does not contains names or variables in U, then we always apply rule R1 as mentioned in the first item and never apply rule R3. (As written in Fig. 5, rule R3 is applied with context 9 only when rule R1 does not apply.) The case in which $M = diff [M_{1}, M_{2}]$ is similar, using context 10.

For an expression or process Q, we proceed by induction using the third rule of Fig. 5, and after several recursive calls, we apply $split$ to each term contained in Q.

Fig. 5.
Helper function for barrier annotation.

For soundness of the transformation (Proposition 5), it is sufficient that:
Lemma 3.
If $(Q^{'}, ς) = split (Q)$ , then $Q = Q^{'} ς$ , $fv (Q^{'}) = dom (ς)$ , and $fn (Q^{'}) = \emptyset$ .

This lemma is an immediate corollary of the following result:
Lemma 4.
Let Q be a term, an expression, or a process. If $(Q^{'}, ς) = split (U, Q)$ , then $Q^{'} ς = Q$ , $(fv (range (ς)) \cup fn (range (ς))) \cap U = \emptyset$ , $dom (ς) \subseteq fv (Q^{'}) \subseteq dom (ς) \cup U$ , $fn (Q^{'}) \subseteq U$ , and $dom (ς)$ consists of fresh variables.

Lemma 4 is proved in Appendix C by induction of Q, following the definition of $split$ in Fig. 5.

Intuitively, when reducing the annotated barrier by $(R ED B AR$ ’), we reduce $t [a, c, ς] : : Q^{'}$ to $Q^{'} ς$ , which is equal to Q by Lemma 3, so we recover the process Q we had before annotation. The conditions that $fv (Q^{'}) = dom (ς)$ and $fn (Q^{'}) = \emptyset$ show that no names and variables are free in $Q^{'}$ and bound above the barrier, thus substitution ς contains the whole state of the process $Q = Q^{'} ς$ .

The following proposition shows that annotation does not alter the semantics of processes:
Proposition 5.
If $P_{0}$ is a closed standard biprocess and $P_{0}^{'} = annotate (P_{0})$ , then $P_{0}^{'}$ is valid, $fst (P_{0}^{'}) \approx fst (P_{0})$ , and $snd (P_{0}^{'}) \approx snd (P_{0})$ .
Proof sketch.
The main step of the proof consists in showing that, when $C [t : : P ς]$ and $C [t [a, c, ς] : : P]$ are valid processes, we have $C [t : : P ς] \approx C [t [a, c, ς] : : P]$ . This proof is performed by defining a relation $R$ that satisfies the conditions of Definition 1. By Lemma 3, from the annotated biprocess $P_{0}^{'}$ , we can rebuild the initial process $P_{0}$ by replacing each occurrence of an annotated barrier $t [a, c, ς] : : Q$ with $t : : Q ς$ , so the same replacement also transforms $fst (P_{0}^{'})$ into $fst (P_{0})$ and $snd (P_{0}^{'})$ into $snd (P_{0})$ . By $C [t : : P ς] \approx C [t [a, c, ς] : : P]$ , this replacement preserves the observational behaviour of the processes. This proof is detailed in Appendix D. □
3.3. Barrier elimination and swapping

Next, we define the second step of our compiler, which translates an annotated biprocess into biprocesses without barriers. Each annotated barrier $t [a_{i}, c_{i}, ς_{i}]$ ( $1 ⩽ i ⩽ n$ ) is eliminated by replacing it with an output on channel $a_{i}$ of swappable data, followed by an input on channel $c_{i}$ that receives swapped data. A swapping process is added in parallel, which receives the swappable data on channels $a_{1}, \dots, a_{n}$ for all barriers t, before sending swapped data on channels $c_{1}, \dots, c_{n}$ . Therefore, all inputs on channels $a_{1}, \dots, a_{n}$ must be received before the outputs on channels $c_{1}, \dots, c_{n}$ 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_{i}$ data that comes from channel $a_{j}$ with $j \neq i$ , 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.

3.3.1. Barrier elimination

First, we eliminate barriers.

Definition 6.
The function $bar - elim$ removes annotated barriers, by transforming each annotated barrier $t [a, c, (M_{1} / z_{1}, \dots, M_{n} / z_{n})] : : Q$ into $\overline{a} ⟨ (| M_{1}, \dots, M_{n} |) ⟩ . c (z) . let z_{1} = π_{1, n} (z) in \dots let z_{n} = π_{n, n} (z) in Q$ , where z is a fresh variable.

The definition of function $bar - elim$ ensures that, if the message $(| 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 $bar - elim$ 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 $bar - elim$ are observationally equivalent. Intuitively, the private channel communication provides an opportunity to swap data. The function $bar - elim$ is defined more formally in Fig. 6, by induction on the syntax.

Fig. 6.
Definition of $bar - elim$ .
Example 7.
Using the results of Example 6, eliminating barriers from $annotate (P_{ex})$ yields the process $bar - elim (annotate (P_{ex})) = P_{comp} ∣ P_{comp}^{'}$ , where $\begin{array}{l} P_{comp} = \overline{c} ⟨ A ⟩ . \overline{a} ⟨ (| c, diff [v, v^{'}] |) ⟩ . b (z) . let x = π_{1, 2} (z) in let y = π_{2, 2} (z) in \overline{x} ⟨ y ⟩ \\ P_{comp}^{'} = \overline{c} ⟨ B ⟩ . \overline{a^{'}} ⟨ (| c, diff [v^{'}, v] |) ⟩ . b^{'} (z^{'}) . let x^{'} = π_{1, 2} (z^{'}) in let y^{'} = π_{2, 2} (z^{'}) in \overline{x^{'}} ⟨ y^{'} ⟩ \end{array}$ for some fresh variables z and $z^{'}$ .
3.3.2. Swapping

Next, we define swapping strategies.

Definition 7.
The function $swapper$ is defined over multisets B as follows: if $B = \emptyset$ , then $swapper (B) = {0}$ ; otherwise, $\begin{array}{l} swapper (B) \\ = {a_{1} (x_{1}) . \dots . a_{n} (x_{n}) . \overline{c_{1}} ⟨ diff [x_{1}, x_{f (1)}] ⟩ . \dots . \overline{c_{n}} ⟨ diff [x_{n}, x_{f (n)}] ⟩ . R | \\ B = {t [a_{1}, c_{1}, {\tilde{z}}_{1}] : : Q_{1}, \dots, t [a_{n}, c_{n}, {\tilde{z}}_{n}] : : Q_{n}} \cup B^{'} where t^{'} > t for all t^{'} [a, c, \tilde{z}] : : Q \in B^{'}; \\ function f is a permutation on {1, \dots, n} such that Q_{l} / {\tilde{z}}_{l} =_{ch} Q_{f (l)} / {\tilde{z}}_{f (l)} for all 1 ⩽ l ⩽ n; \\ R \in swapper (B^{'}); and x_{1}, \dots, x_{n} are fresh variables} \end{array}$ where $=_{ch}$ is defined as follows:
$Q =_{ch} Q^{'}$ means that Q equals $Q^{'}$ modulo renaming of channels of annotated barriers and

$Q / \tilde{z} =_{ch} Q^{'} / {\tilde{z}}^{'}$ means that $\tilde{z} = (z_{1}, \dots, z_{k})$ and ${\tilde{z}}^{'} = (z_{1}^{'}, \dots, z_{k}^{'})$ for some integer k, and $Q {y_{1} / z_{1}, \dots, y_{k} / z_{k}} =_{ch} Q^{'} {y_{1} / z_{1}^{'}, \dots, y_{k} / z_{k}^{'}}$ for some fresh variables $y_{1}, \dots, y_{k}$ .

The function $swapper$ builds a set of processes from a multiset of domain-barriers B as follows. We identify integer $t \in N$ and domain-barriers $t [a_{1}, c_{1}, {\tilde{z}}_{1}] : : Q_{1}, \dots, t [a_{n}, c_{n}, {\tilde{z}}_{n}] : : Q_{n}$ in B such that no other barriers with $t^{'} ⩽ t$ appear in B, so that these barriers are reduced before other barriers in B. Among these barriers, we consider barriers $t [a_{i}, c_{i}, {\tilde{z}}_{i}] : : Q_{i}$ and $t [a_{j}, c_{j}, {\tilde{z}}_{j}] : : Q_{j}$ such that $Q_{i} / {\tilde{z}}_{i} =_{ch} Q_{j} / {\tilde{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 ${\tilde{z}}_{i}$ and ${\tilde{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 $diff$ and permuted by f in the second component of $diff$ . The function $swapper$ does not specify an ordering on the pairs of channels $(a_{1}, c_{1}), \dots, (a_{n}, c_{n})$ , since any ordering is correct. Example 8.
We have $barriers (annotate (P_{ex})) = {1 [a, b, (x, y)] : : \overline{x} ⟨ y ⟩, 1 [a^{'}, b^{'}, (x^{'}, y^{'})] : : \overline{x^{'}} ⟨ y^{'} ⟩}$ . Moreover, we trivially have $\overline{x} ⟨ y ⟩ / (x, y) =_{ch} \overline{x} ⟨ y ⟩ / (x, y)$ and $\overline{x^{'}} ⟨ y^{'} ⟩ / (x^{'}, y^{'}) =_{ch} \overline{x^{'}} ⟨ y^{'} ⟩ / (x^{'}, y^{'})$ , because $Q / \tilde{z} =_{ch} Q / \tilde{z}$ for all Q and $\tilde{z}$ . We also have $\overline{x} ⟨ y ⟩ / (x, y) =_{ch} \overline{x^{'}} ⟨ y^{'} ⟩ / (x^{'}, y^{'})$ , because $\begin{matrix} \overline{x} ⟨ y ⟩ {x^{″} / x, y^{″} / y} = \overline{x^{″}} ⟨ y^{″} ⟩ = \overline{x^{'}} ⟨ y^{'} ⟩ {x^{″} / x^{'}, y^{″} / y^{'}} \end{matrix}$ It follows that $swapper (barriers (annotate (P_{ex}))) = {P_{same}, P_{swap}}$ , where $\begin{array}{l} P_{same} = a (z) . a^{'} (z^{'}) . \overline{b} ⟨ diff [z, z] ⟩ . \overline{b^{'}} ⟨ diff [z^{'}, z^{'}] ⟩ \\ P_{swap} = a (z) . a^{'} (z^{'}) . \overline{b} ⟨ diff [z, z^{'}] ⟩ . \overline{b^{'}} ⟨ diff [z^{'}, z] ⟩ \end{array}$ for some fresh variables z and $z^{'}$ . (Note that $diff [z, z]$ could be simplified into z. Similarly, $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.

3.3.3. Combining barrier elimination and swapping

Finally, we derive a set of processes by parallel composition of the process output by $bar - elim$ and the processes output by $swapper$ , under the scope of name restrictions on the fresh channels introduced by $annotate$ . $\begin{matrix} elim - and - swap (P) = \{\begin{matrix} ν \tilde{a} . (bar - elim (P) ∣ R) where B = barriers (P), \\ {\tilde{a}} = channels (B), and R \in swapper (B) \end{matrix}\} \end{matrix}$

Intuitively, function $elim - and - swap$ encodes barrier synchronisation and swapping using private channel communication, thereby preserving the observational behaviour of processes.

Example 9.
Using the results of Examples 7 & 8, applying $elim - and - swap$ to the process $annotate (P_{ex})$ generates two processes $\begin{array}{l} P_{1} = ν a, a^{'}, b, b^{'} . (P_{comp} ∣ P_{comp}^{'} ∣ P_{same}) \\ P_{2} = ν a, a^{'}, b, b^{'} . (P_{comp} ∣ P_{comp}^{'} ∣ P_{swap}) \end{array}$ In the process $P_{1}$ , no data is swapped, so it behaves exactly like $P_{ex}$ : $(| c, diff [v, v^{'}] |)$ is sent on a, sent back on b by $P_{same}$ as $diff [(| c, diff [v, v^{'}] |), (| c, diff [v, v^{'}] |)]$ which simplifies into $(| c, diff [v, v^{'}] |)$ , and after evaluating the projections, $P_{comp}$ reduces into $\overline{c} ⟨ diff [v, v^{'}] ⟩$ , which is the output present in the process $P_{ex}$ . Similarly, $P_{comp}^{'}$ reduces into $\overline{c} ⟨ diff [v^{'}, v] ⟩$ , present in $P_{ex}$ .

By contrast, in process $P_{2}$ , data is swapped: $(| c, diff [v, v^{'}] |)$ is sent on a and $(| c, diff [v^{'}, v] |)$ is sent on $a^{'}$ , and $P_{swap}$ sends back $diff [(| c, diff [v, v^{'}] |), (| c, diff [v^{'}, v] |)]$ on b. The first component of this term is $(| c, v |)$ (obtained by taking the first component of each $diff$ ), and similarly its second component is also $(| c, v |)$ , so this term simplifies into $(| c, v |)$ . After evaluating the projections, $P_{comp}$ reduces into $\overline{c} ⟨ v ⟩$ . Similarly, $P_{comp}^{'}$ reduces into $\overline{c} ⟨ v^{'} ⟩$ . Hence $P_{2}$ behaves like $\overline{c} ⟨ A ⟩ .1 : : \overline{c} ⟨ v ⟩ ∣ \overline{c} ⟨ B ⟩ .1 : : \overline{c} ⟨ v^{'} ⟩$ . In particular, $P_{2}$ outputs A and B before barrier synchronisation and v and $v^{'}$ after synchronisation just like $P_{ex}$ . But $P_{2}$ satisfies diff-equivalence while $P_{ex}$ does not.

The next proposition formalises the preservation of observable behaviour.
Proposition 6.
Let P be a valid, annotated biprocess. If $P^{'} \in elim - and - swap (P)$ , then $fst (P) \approx fst (P^{'})$ and $snd (P) \approx snd (P^{'})$ .

The core argument for the proof of Proposition 6 is the following:
Proposition 7.
Suppose $P_{0}$ is a valid, annotated biprocess. Let $C_{0} = B, E, {P_{0}}$ and $C_{0}^{'} = \emptyset, E, {bar - elim (P_{0}), R}$ , where $B = barriers (P_{0})$ , $E = channels (B)$ , and $R \in swapper (B)$ . We have $fst (C_{0}) \approx fst (C_{0}^{'})$ and $snd (C_{0}) \approx snd (C_{0}^{'})$ .

In this proposition, the configuration $C_{0}$ is the initial configuration of the process $P_{0}$ and the configuration $C_{0}^{'}$ is obtained by reducing the restrictions and the parallel composition at the root of a compiled process in $elim - and - swap (P_{0})$ . The proposition shows that the first components of these two configurations are observationally equivalent, and so are the second components. The proposition is proved by defining a relation $R$ that satisfies the conditions of Definition 1. The proof is fairly long and delicate. It relies on Lemmas 8 and 9, and is detailed in Appendix G.

Lemma 8 proves that $bar - elim$ preserves renaming of names and substitution of terms for variables. (Our operational semantics uses renaming of names and substitution of terms for variables. Implicitly, this includes renaming of variables.)
Lemma 8.
Given an annotated process P and a substitution or renaming σ, we have $bar - elim (P) σ = bar - elim (P σ)$ .

This lemma is proved by induction on process P, in Appendix E.

The second lemma builds upon Lemma 8 to show that function $bar - elim$ preserves reduction, in cases in which barriers are not reduced.
Lemma 9.
Suppose B is a finite set of annotated barriers, E is a finite set of names and $P, Q, Q^{'}$ are finite multisets of processes such that $barriers (Q^{'}) = \emptyset$ . Further suppose that $C = B, E, Q \cup P$ is a valid configuration. Let $C^{'} = \emptyset, E, Q^{'} \cup bar - elim (P)$ . We have the following properties:
If $C \overset{}{\to} C_{1}$ by reducing one or more processes in $P$ such that $C_{1} = B, E_{1}, Q \cup P_{1}$ for some set of names $E_{1}$ and multiset of processes $P_{1}$ , then $C^{'} \overset{}{\to} C_{1}^{'}$ , where $C_{1}^{'} = \emptyset, E_{1}, Q^{'} \cup bar - elim (P_{1})$ .

If $C^{'} \overset{}{\to} C_{1}^{'}$ by reducing one or more processes in $bar - elim (P)$ such that $C_{1}^{'} = \emptyset, E_{1}, Q^{'} \cup P_{1}^{'}$ for some set of names $E_{1}$ and multiset of processes $P_{1}^{'}$ , then there exists a multiset of processes $P_{1}$ such that $P_{1}^{'} = bar - elim (P_{1})$ and $C \overset{}{\to} C_{1}$ , where $C_{1} = B, E_{1}, Q \cup P_{1}$ .

This lemma is proved by cases on the considered reduction, in Appendix F.

We use two additional propositions in order to prove Proposition 6.
Proposition 10.
Let $B, E, {ν n . P} \cup P$ be a valid configuration, and $n^{'}$ be a name, where $n^{'} \notin E \cup fn ({ν n . P} \cup P)$ . We have $B, E, {ν n . P} \cup P \approx B, E \cup {n^{'}}, {P {n^{'} / n}} \cup P$ .
Proposition 11.
Let $B, E, {P ∣ Q} \cup P$ be a valid configuration. We have $B, E, {P ∣ Q} \cup P \approx B, E, {P, Q} \cup P$ .

These propositions follow immediately from the semantics and definition of observational equivalence. They are proved in Appendix H, by defining a relation $R$ that satisfies the conditions of Definition 1.

The proof of Proposition 6 follows from these results. Proof of Proposition 6.
Let $B_{0} = barriers (P)$ , and ${\tilde{a}} = channels (B_{0})$ . By definition of $compiler$ , there exists a biprocess $R \in swapper (B_{0})$ such that $P^{'} = ν \tilde{a} . (bar - elim (P) ∣ R)$ . It follows that $barriers (P^{'}) = \emptyset$ , so we have $\begin{array}{l} C_{init} (fst (P^{'})) & = \emptyset, \emptyset, {fst (P^{'})} \\ by Proposition 10 & \approx \emptyset, {\tilde{a}}, {fst (bar - elim (P) ∣ R)} \\ by Proposition 11 & \approx \emptyset, {\tilde{a}}, {fst (bar - elim (P)), fst (R)} \\ by Proposition 7 & \approx fst (B_{0}), {\tilde{a}}, {fst (P)} = C_{init} (fst (P)) \end{array}$ so $fst (P^{'}) \approx fst (P)$ . The proof of $snd (P) \approx snd (P^{'})$ is similar. □

3.4. Our compiler

We combine the annotation (Section 3.2) and barrier removal (Section 3.3) steps to define our compiler as $\begin{matrix} compiler (P) = elim - and - swap (annotate (P)) \end{matrix}$ We have implemented the compiler in ProVerif, available from: http://proverif.inria.fr/.

By combining Propositions 5 and 6, we immediately obtain:

Corollary 12.
Let P be a closed standard biprocess. If $P^{'} \in compiler (P)$ , then $fst (P) \approx fst (P^{'})$ and $snd (P) \approx snd (P^{'})$ .

This corollary shows that compilation preserves the observational behaviour of processes. The following theorem is an immediate consequence of this corollary:
Theorem 13.
Let P be a closed biprocess. If a biprocess in $compiler (P)$ satisfies observational equivalence, then P satisfies observational equivalence.
Proof.
Suppose that there exists a biprocess $P^{'} \in compiler (P)$ such that $P^{'}$ satisfies observational equivalence, that is, $fst (P^{'}) \approx snd (P^{'})$ . By Corollary 12, $fst (P) \approx fst (P^{'})$ and $snd (P) \approx snd (P^{'})$ , so by transitivity of ≈, we have $fst (P) \approx snd (P)$ , so P satisfies observational equivalence. □

This theorem allows us to prove observational equivalence using swapping: we prove that a biprocess in $compiler (P)$ satisfies observational equivalence using ProVerif (by Theorem 1), and conclude that P satisfies observational equivalence as well. For instance, ProVerif can show that the process $P_{2} \in compiler (P_{ex})$ of Example 9 satisfies observational equivalence, thus $P_{ex}$ satisfies observational equivalence too.

The idea of swapping data at synchronisation points also applies to other tools that prove diff-equivalence (e.g., Maude-NPA [57] and Tamarin [11]). However, a compiler such as ours is not necessarily needed to implement this idea in these tools. For instance, in Tamarin, the swapping can be done directly on the multiset representing the state at the synchronisation point [42]. The idea of swapping 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.
3.5. Extensions

3.5.1. Replicated barriers

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 = P ∣ \dots ∣ P$ with n copies of the process P. We have the following results:

Proposition 14.
Let $C [! Q]$ be a closed standard biprocess, such that the context $C [_]$ does not contain any barrier above the hole. If a biprocess in $compiler (C [! Q])$ satisfies diff-equivalence, then for all n, a biprocess in $compiler (C [!^{n} Q])$ satisfies diff-equivalence.

Proposition 14 shows that, if our approach proves equivalence with unbounded replication, then it also proves equivalence with bounded replication. This proposition and the next one are proved in Appendix I.
Proposition 15.
Let $C [Q]$ be a closed standard biprocess, such that the context $C [_]$ does not contain any replication above the hole. If a biprocess in $compiler (C [Q])$ satisfies diff-equivalence, then a biprocess in $compiler (C [t : : Q])$ satisfies diff-equivalence.

Proposition 15 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:
Corollary 16.
Let $Q_{nobar}$ be obtained from Q by removing all barriers. Let $C [_]$ be a context that does not contain any replication or barrier above the hole. If a biprocess in $compiler (C [! Q_{nobar}])$ satisfies diff-equivalence, then for all n, process $C [!^{n} Q]$ satisfies observational equivalence.
Proof.
If a biprocess in $compiler (C [! Q_{nobar}])$ satisfies diff-equivalence, then by Proposition 14, a biprocess in $compiler (C [!^{n} Q_{nobar}])$ satisfies diff-equivalence. By applying Proposition 15 several times, a biprocess in $compiler (C [!^{n} Q])$ satisfies diff-equivalence. Hence, by Theorem 1, a biprocess in $compiler (C [!^{n} Q])$ satisfies observational equivalence, and by Theorem 13, $C [!^{n} Q]$ satisfies observational equivalence. □

Corollary 16 shows that we can apply our compiler to prove observational equivalence for biprocesses with bounded replication, for any value of the bound. In the context of election schemes, this result allows us to prove privacy for an unbounded number of voters. For instance, in the protocol by Lee et al. (Section 4.2), we consider a process $C [!^{n + 2} Q]$ with $n + 2$ voters each using a process Q, in which two voters A and B swap their votes. We isolate the processes for the voters A and B, writing the process $C [Q_{A} ∣ Q_{B} ∣!^{n} Q]$ . We keep the barriers in $Q_{A}$ and $Q_{B}$ (they are typically useful), but remove them in the other processes $!^{n} Q$ in order to apply Corollary 16: we show that a biprocess in $compiler (C [Q_{A} ∣ Q_{B} ∣! Q_{nobar}])$ satisfies diff-equivalence, and conclude that for all n, process $C [Q_{A} ∣ Q_{B} ∣!^{n} Q]$ satisfies observational equivalence.
3.5.2. 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) [16]. 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. We do not detail the proof of trace properties with barriers further, since it is easier and less important than observational equivalence.

3.5.3. Swapping without explicit synchronisation

Our compiler enables swapping at synchronisation points. Swapping can also be performed immediately under parallel compositions. For instance, in a biprocess $C [P_{1} ∣ \dots ∣ P_{n}]$ , data could be swapped between processes $P_{1}, \dots, P_{n}$ that have the same skeleton, even without explicit synchronisation. We do not perform this swapping in our compiler for several reasons. First, this case is easy to deal with manually: by rewriting $P_{1} ∣ \dots ∣ P_{n}$ as $Q_{1} ∣ \dots ∣ Q_{n}$ , where $fst (Q_{1} ∣ \dots ∣ Q_{n}) = fst (P_{1} ∣ \dots ∣ P_{n})$ and $snd (Q_{1} ∣ \dots ∣ Q_{n})$ is obtained by permuting the parallel processes in $snd (P_{1} ∣ \dots ∣ P_{n})$ . Secondly, such a rewriting is performed by another extension of ProVerif [25, Section 5], to merge processes into biprocesses in order to prove observational equivalence. Finally, this case would lead to useless swapping opportunities, which would slow down the exploration of all swapping possibilities. If swapping is desired in this case, it can be obtained in our approach by adding a synchronisation at the beginning of $P_{1}, \dots, P_{n}$ .

3.5.4. Future work

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. For instance, we could consider a voting system in which voters synchronise at a regional level. In the same direction, we could consider a vehicular network in which vehicles synchronise at the crossroad level (see also Section 4.3). In this case, we would need several swapping processes similar to those generated by $swapper$ , one for each group.

We could also extend our approach to swap data between processes that have the same skeleton only until the next synchronisation. In this case, the swapping must be reversed at the next synchronisation, to recover the initial data. For instance, that would allow us to prove that the biprocess $1 : : \overline{c} ⟨ diff [m, n] ⟩ .2 : : 0 ∣ 1 : : \overline{c} ⟨ diff [n, m] ⟩ .2 : : \overline{c} ⟨ n ⟩$ satisfies observational equivalence. (The synchronisation at barrier 1 could be removed as explained in Section 3.5.3.)

It would also be useful to study heuristics in order to find a successful swapping strategy without trying all of them. Finally, it would be interesting to study the impact of our compiler on the termination and on the precision of ProVerif, especially with the usage of private channels to encode synchronisation and swapping.

4. 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), by Lee et al., along with some of its variants, and by Juels, Catalano & Jakobsson (commonly referred to as JCJ). Our ProVerif scripts are included in ProVerif’s documentation package (http://proverif.inria.fr/). The runtime of these scripts (including compilation of barriers and proof of diff-equivalence by ProVerif) ranges from 0.24 seconds for FOO to 372 seconds to prove coercion-resistance in JCJ, on an Intel Xeon 3.6 GHz under Linux.

4.1. Case study: FOO

4.1.1. Cryptographic primitives

FOO uses commitments and blind signatures. We model commitment with a binary constructor $commit$ , and the corresponding destructor $open$ for opening the commitment, with the following rewrite rule: $\begin{matrix} open (x_{k}, commit (x_{k}, x_{plain})) & \to & x_{plain} \end{matrix}$ Using constructors $sign$ , $blind$ , and $pk$ , we model blind signatures as follows: $sign (x_{sk}, x_{msg})$ is the signature of message $x_{msg}$ under secret key $x_{sk}$ , $blind (x_{k}, x_{msg})$ is the blinding of message $x_{msg}$ with coins $x_{k}$ , and $pk (x_{sk})$ is the public key corresponding to the secret key $x_{sk}$ . We also use three destructors: $checksign$ to verify signatures, $getmsg$ to model that an adversary may recover the message from the signature, even without the public key, and $unblind$ for unblinding, defined by the following rewrite rules: $\begin{matrix} checksign (pk (x_{sk}), sign (x_{sk}, x_{msg})) & \to & x_{msg} \\ getmsg (sign (x_{sk}, x_{msg})) & \to & x_{msg} \\ unblind (x_{k}, sign (x_{sk}, blind (x_{k}, x_{msg}))) & \to & sign (x_{sk}, x_{msg}) \\ unblind (x_{k}, blind (x_{k}, x_{plain})) & \to & x_{plain} \end{matrix}$ 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.

4.1.2. 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.

The registrar creates a signing key pair ${sk}_{R}$ and $pk ({sk}_{R})$ , and publishes the public part $pk ({sk}_{R})$ . In addition, each voter is assumed to have a signing key pair ${sk}_{V}$ and $pk ({sk}_{V})$ , where the public part $pk ({sk}_{V})$ has been published.

The preparation phase then proceeds as follows.

The voter chooses coins k and $k^{'}$ , computes the commitment to her vote $M = commit (k, v)$ and the signed blinded commitment $sign ({sk}_{V}, blind (k^{'}, M))$ , and sends the signature, paired with her public key, to the registrar.

The registrar checks that the signature belongs to an eligible voter and returns the blinded commitment signed by the registrar $sign ({sk}_{R}, blind (k^{'}, M))$ .

The voter verifies the registrar’s signature and unblinds the message to recover $\hat{M} = sign ({sk}_{R}, M)$ , that is, her commitment signed by the registrar.

After a deadline, the protocol enters the commitment phase.

The voter posts her ballot $\hat{M}$ to the bulletin board.

Similarly, the tallying phase begins after a deadline.

The tallier checks validity of all signatures on the bulletin board and prepends an identifier ℓ to each valid entry.

The voter checks the bulletin board for her entry, the pair $ℓ, \hat{M}$ , and appends the commitment factor k.

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 [34] for further discussion on fairness).

4.1.3. 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 8.
The process $P_{foo} (x_{sk}, x_{vote})$ modelling a voter in FOO, with signing key $x_{sk}$ and vote $x_{vote}$ , is defined as follows $\begin{matrix} P_{foo} (x_{sk}, x_{vote}) = & ν k . ν k^{'} . & % Step 2 \\ let M = commit (k, x_{vote}) in \\ let M^{'} = blind (k^{'}, M) in \\ \overline{c} ⟨ (| pk (x_{sk}), sign (x_{sk}, M^{'}) |) ⟩ . \\ c (y) . & % Step 4 \\ let y^{'} = checksign (pk ({sk}_{R}), y) in \\ if y^{'} = M^{'} then \\ let \hat{M} = unblind (k^{'}, y) in \\ 1 : : \overline{c} ⟨ \hat{M} ⟩ . & % Step 5 \\ 2 : : c (z) . & % Step 7 \\ let z_{2} = π_{2, 2} (z) in \\ if z_{2} = \hat{M} then \\ \overline{c} ⟨ (| z, k |) ⟩ \end{matrix}$

The process $P_{foo} ({sk}_{1}, v_{1}) ∣ \dots ∣ P_{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.
4.1.4. Analysis: Ballot secrecy

Based upon [39,51] and as outlined in Section 1, 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_{foo} ({sk}_{A}, diff [v, v^{'}])$ to model A and the biprocess $P_{foo} ({sk}_{B}, diff [v^{'}, v])$ to model B, and formally express ballot secrecy as an equivalence which can be checked using Theorem 13. 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.)

Definition 9 (Ballot secrecy).

FOO preserves ballot secrecy if the biprocess $Q_{foo} = P_{foo} ({sk}_{A}, diff [v, v^{'}]) ∣ P_{foo} ({sk}_{B}, diff [v^{'}, v])$ satisfies observational equivalence.

To provide further insight into how our compiler works, let us consider how to informally prove this equivalence: that $fst (Q_{foo})$ is indistinguishable from $snd (Q_{foo})$ . Before the first barrier, A outputs $\begin{matrix} (| pk ({sk}_{A}), sign ({sk}_{A}, blind (k_{a}^{'}, commit (k_{a}, v))) |) \end{matrix}$ in $fst (Q_{foo})$ and $\begin{matrix} (| pk ({sk}_{A}), sign ({sk}_{A}, blind (k_{a}^{'}, commit (k_{a}, v^{'}))) |) \end{matrix}$ in $snd (Q_{foo})$ , where the name $k_{a}^{'}$ remains secret. By the equational theory for blinding, N can only be recovered from $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 $fst (Q_{foo})$ are mimicked by A moves in $snd (Q_{foo})$ and B moves in $fst (Q_{foo})$ are mimicked by B moves in $snd (Q_{foo})$ .

Let us define $sc (k, v) = sign ({sk}_{R}, commit (k, v))$ . After the first barrier, A outputs $\begin{array}{l} sc (k_{a}, v) and (| (| ℓ_{1}, sc (k_{a}, v) |), k_{a} |) in fst (Q_{foo}) \\ sc (k_{a}, v^{'}) and (| (| ℓ_{1}, sc (k_{a}, v^{'}) |), k_{a} |) in snd (Q_{foo}) \end{array}$ where $ℓ_{1}$ is chosen by the adversary. It follows that A reveals her vote v in $fst (Q_{foo})$ and her vote $v^{'}$ in $snd (Q_{foo})$ , so these messages are distinguishable. However, B outputs $\begin{array}{l} sc (k_{b}, v^{'}) and (| (| ℓ_{2}, sc (k_{b}, v^{'}) |) k_{b} |) in fst (Q_{foo}) \\ sc (k_{b}, v) and (| (| ℓ_{2}, sc (k_{b}, v) |) k_{b} |) in snd (Q_{foo}) \end{array}$ where $ℓ_{2}$ is similarly chosen by the adversary. Hence, B’s messages in $snd (Q_{foo})$ are indistinguishable from A’s messages in $fst (Q_{foo})$ . Therefore, after the first barrier, A moves in $fst (Q_{foo})$ are mimicked by B moves in $snd (Q_{foo})$ and symmetrically, B moves in $fst (Q_{foo})$ are mimicked by A moves in $snd (Q_{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 13. 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 [39,51] present a manual proof of ballot secrecy, Chothia et al. [28] provide an automated analysis in the presence of a passive adversary, and Delaune, Ryan & Smyth [41], Klus, Smyth & Ryan [50], and Chadha, Ciobâcă & Kremer [24,31] provide automated analysis in the presence of an active adversary. More recently, Dreier et al. [42] provided a mechanised analysis in the tool Tamarin 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. [52] uses a hardware device to introduce coins into the ballot that the voter does not know.

4.2. Case study: Lee et al.

4.2.1. 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.

The tallier generates a key pair and publishes the public key.

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.

The voter encrypts her vote and inputs the resulting ciphertext into her tamper-resistant hardware device.

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.

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.

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.)

The tallier decrypts each ciphertext and announces the election outcome.

4.2.2. 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 (1), we formalise ballot secrecy by the equivalence $\begin{matrix} (2) & C [V (A, v) ∣ V (B, v^{'})] \approx C [V (A, v^{'}) ∣ V (B, v)] \end{matrix}$ 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 16 to model an unbounded number of voters by a replicated process. As far as we know, this is the first proof of this result. In order to prove this result, we separate the processes (voter, device, mixnet and tallier) corresponding to voters A and B, from those corresponding to the other voters, as outlined at the end of Section 3.5.1. We keep the synchronisations in the mixnet for A and B and swap data there, and we remove synchronisations in the processes for other voters in order to apply Corollary 16.

With the addition of a 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 [52, Section 6] and formalised in [43]: 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.

4.2.3. Analysis: Receipt-freeness

Following [39], receipt-freeness can be formalised as follows: there exists a process $V^{'}$ such that $\begin{array}{l} (3) & V^{' ∖ chc} \approx V (A, v) \\ (4) & C [V {(A, v^{'})}^{chc} ∣ V (B, v)] \approx C [V^{'} ∣ V (B, v^{'})] \end{array}$ where the context $C [_]$ appears in (2), $chc$ is a public channel, $V^{' ∖ chc} = ν chc . (V ∣! chc (x))$ , which is intuitively equivalent to removing all outputs on channel $chc$ from $V^{'}$ , and $V {(A, v^{'})}^{chc}$ is obtained by modifying $V (A, v^{'})$ as follows: we output on channel $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^{'})}^{chc}$ . The process $V^{'}$ simulates a voter A that votes v, as shown by (3), but outputs messages on channel $chc$ that aim to make the adversary think that it voted $v^{'}$ . The equivalence (4) 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)}^{chc}$ by outputting on $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 (3) holds by construction of $V^{'}$ , because after removing outputs on $chc$ , $V^{'}$ is exactly the same as $V (A, v)$ . We prove (4) 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.

4.2.4. Variant by Dreier, Lafourcade & Lakhnech

Dreier, Lafourcade & Lakhnech [43] 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.

4.2.5. Variant by Delaune, Kremer & Ryan

Protocol description. Delaune, Kremer & Ryan [39] introduced a variant of this protocol in which the hardware devices are replaced with a single administrator, and the voting phase becomes:

The voter encrypts her vote, signs the ciphertext, and sends the ciphertext and signature to the administrator on a private channel.

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.

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:

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 [39]. 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 ∣ Q] \approx C [Q ∣ P]$ , as explained in Section 3.5.3. Furthermore, an extension of ProVerif [25, Section 5] 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 12 minutes 46 seconds, while our implementation with swapping takes 31 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 (3) again holds by construction of $V^{'}$ . To prove (4), much like in [39], we model the collector as parallel processes that each input one ballot, check the signature, decrypt, synchronise together, and output the decrypted vote: $\begin{matrix} c (b); let e v = checksign (p k_{A}, b) in let v = dec ({sk}_{C}, e v) in 2 : : \overline{c} ⟨ v ⟩ \end{matrix}$ 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. Therefore, this check is difficult to implement in the original process fed to our compiler in a way that would allow our approach to conclude. Instead, 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{array}{l} (c (b); let e v = checksign (p k_{A}, b) in \\ let v = dec ({sk}_{C}, e v) in \overline{a_{1}} ⟨ (| b, v |) ⟩; c_{1} (v^{'}); \overline{c} ⟨ v^{'} ⟩) \\ ∣ \\ (c (b); let e v = checksign (p k_{A}, b) in \\ let v = dec ({sk}_{C}, e v) in \overline{a_{2}} ⟨ (| b, v |) ⟩; c_{2} (v^{'}); \overline{c} ⟨ v^{'} ⟩) \\ ∣ \\ (a_{1} ((| b_{1}, v_{1} |)); a_{2} ((| b_{2}, v_{2} |)); \\ (*) & if b_{1} = b_{2} then 0 else \\ \overline{c_{1}} ⟨ diff [v_{1}, v_{2}] ⟩; \overline{c_{2}} ⟨ diff [v_{2}, v_{1}] ⟩) \end{array}$ This code shows the two collectors and the process that swaps data. We use $a ((| b, v |))$ as an abbreviation for $a (x); let b = π_{1, 2} (x) in let v = π_{2, 2} (x) 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 ballots coming from the voters that swap their votes), but it has no means to detect which ones.

4.3. Other examples

The idea of swapping for proving equivalences has been applied by Dahl, Delaune & Steel [36] to prove privacy in a vehicular ad-hoc network [45]. They manually encode swapping based upon the informal idea of [41]. We have repeated their analysis using our approach. Thus, we automate the encoding of swapping in [36], and obtain stronger confidence in the results thanks to our soundness proof.

Backes, Hriţcu & Maffei [10] also manually encode 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 [49]. We removed their manual encoding of swapping and repeated their analysis using our approach. In this case, swapping is done immediately under a parallel composition, so it is particularly easy to encode manually, as explained in Section 3.5.3. (Both our analysis and the one by Backes, Hriţcu & Maffei abstract away the malleability of encryption, because ProVerif does not support it.)

Although the swapping idea also applies to the election scheme Helios [7], we cannot automatically verify it with ProVerif, because ProVerif does not support the equational theory of homomorphic encryption.

5. 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, receipt-freeness, and coercion resistance in election schemes, as well as privacy in a vehicular ad-hoc network. The idea of swapping data at barriers was introduced in [41], without proving its soundness, and similar ideas have been used by several researchers [10,36], so we believe that it is important to provide a strong theoretical foundation to this technique.

Footnotes

Acknowledgments

We are particularly grateful to Tom Chothia, Véronique Cortier, Andy Gordon, Mark Ryan, and the anonymous CSF and JCS 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 Section 3

This appendix proves the results announced in Section 3. Appendix B proves Lemma 2 (validity); Appendix C proves Lemma 4 (soundness of $split$ ); and Appendix D proves Proposition 5 (soundness of $annotate$ ). Appendices E to H are devoted to the proof of results needed for Theorem 13. We show that barrier elimination commutes with renaming and substitution (proof of Lemma 8 in Appendix E) and that it preserves reduction (proof of Lemma 9 in Appendix F). Using these interim results, we prove Proposition 7 (Appendix G). Appendix H proves Propositions 10 and 11. Finally, Appendix I proves our results on replicated barriers (Section 3.5.1).

Proof of Lemma 2 (validity)

Proof of Lemma 4 (soundness of split )

Proof of Proposition 5 (soundness of annotate )

Proof of Lemma 8 (barrier elimination commutes with renaming and substitution)

Proof of Lemma 9 (barrier elimination preserves reduction)

Proof of Proposition 7 (main proposition)

We introduce some rudimentary results (Lemmata 20–22), before proving the main technical result (Proposition 7). An annotated configuration is a configuration in which all processes are annotated.

We define $\begin{array}{rcl} add-lets (Q) & = & {let z_{j} = π_{j, n} ((| M_{1}, \dots, M_{n} |)) in \dots let z_{n} = π_{n, n} ((| M_{1}, \dots, M_{n} |)) in Q^{'} \\ | \begin{matrix} 1 ⩽ j ⩽ n, Q = Q^{'} {M_{j} / z_{j}, \dots, M_{n} / z_{n}}, M_{1}, \dots, M_{n} ground terms, \\ z_{j}, \dots, z_{n} pairwise distinct variables \end{matrix}} \cup {Q} \end{array}$

These results allow us to prove Proposition 7. Proof of Proposition 7.

Suppose the configurations $C_{0}$ and $C_{0}^{'}$ are given in Proposition 7. We will construct a symmetric relation $R$ such that $fst (C_{0}) R fst (C_{0}^{'})$ , $snd (C_{0}) R snd (C_{0}^{'})$ , and $R$ satisfies the three conditions of Definition 1.

Relation $R$ . We first define some functions $\begin{array}{l} {bar - elim}_{in} (\overline{c} ⟨ (| M_{1}, \dots, M_{n} |) ⟩, Q) \\ = {c (z) . let z_{1} = π_{1, n} (z) in \dots let z_{n} = π_{n, n} (z) in bar - elim (Q^{'}) \\ | Q = Q^{'} {M_{1} / z_{1}, \dots, M_{n} / z_{n}}, z, z_{1}, \dots, z_{n} pairwise distinct variables} \\ {bar - elim}_{in}^{'} (t [a, c, ς] : : Q) \\ = {c (z) . let z_{1} = π_{1, n} (z) in \dots let z_{n} = π_{n, n} (z) in bar - elim (Q) \\ | ς = (M_{1} / z_{1} \dots, M_{n} / z_{n}), z variable different from z_{1}, \dots, z_{n}} \\ {swapper}_{1} (\emptyset) = {0} \\ {swapper}_{1} (B) \\ = {a_{1} (x_{1}) . \dots . a_{n} (x_{n}) . \overline{c_{1}} ⟨ x_{f (1)} ⟩ . \dots . \overline{c_{n}} ⟨ x_{f (n)} ⟩ . R \\ | B = {t [a_{1}, c_{1}, {\tilde{z}}_{1}] : : Q_{1}, \dots, t [a_{n}, c_{n}, {\tilde{z}}_{n}] : : Q_{n}} \cup B^{'}, \\ where t^{'} > t for all t^{'} [a, c, \tilde{z}] : : Q \in B^{'}; \\ function f is a permutation of {1, \dots, n} such \\ that Q_{l} / {\tilde{z}}_{l} =_{ch} Q_{f (l)} / {\tilde{z}}_{f (l)} for all 1 ⩽ l ⩽ n; \\ R \in {swapper}_{1} (B^{'}); and x_{1}, \dots, x_{n} are pairwise distinct variables} \\ if B \neq \emptyset \end{array}$ The sets of processes ${bar - elim}_{in} (\overline{c} ⟨ (| M_{1}, \dots, M_{n} |) ⟩, Q)$ and ${bar - elim}_{in}^{'} (t [a, c, ς] : : Q)$ represent partially reduced compiled barriers: the output on channel a has been executed but not the input on channel c. For ${bar - elim}_{in}^{'} (t [a, c, ς] : : Q)$ , this set is computed from the process $t [a, c, ς] : : Q$ before reduction of the barrier. For ${bar - elim}_{in} (\overline{c} ⟨ (| M_{1}, \dots, M_{n} |) ⟩, Q)$ , this set is computed from the process Q after reduction of the barrier. In this case, we need the additional argument $\overline{c} ⟨ (| M_{1}, \dots, M_{n} |) ⟩$ representing the message sent on channel c to know how to compile the barrier. The function ${swapper}_{1} (B)$ is similar to $swapper (B)$ but produces only one component of the $diff$ .

Let us consider the smallest relations $R_{1}$ , $R_{2}$ and $R_{3}$ between configurations such that the conditions below are satisfied.

Suppose that $B, E, P \cup Q$ is a valid annotated configuration, $P = {P_{1}, \dots, P_{m}}$ , $Q = {t [a_{1}, c_{1}, ς_{1}] : : Q_{1}, \dots, t [a_{k}, c_{k}, ς_{k}] : : Q_{k}}$ , $ς_{l} = (M_{l, 1} / z_{l, 1}, \dots, M_{l, | ς_{l} |} / z_{l, | ς_{l} |})$ for all $l ⩽ k$ , $B = {t [a_{1}, c_{1}, {\tilde{z}}_{1}] : : Q_{1}, \dots, t [a_{n}, c_{n}, {\tilde{z}}_{n}] : : Q_{n}} \cup B^{'}$ , $t^{'} > t$ for all $t^{'} [a^{'}, c^{'}, {\tilde{z}}^{'}] : : Q^{'} \in B^{'}$ , $k ⩽ n$ , and ${\tilde{z}}_{l} = (z_{l, 1}, \dots, z_{l, | {\tilde{z}}_{l} |})$ for all $l ⩽ n$ . Finally, suppose f is a permutation of ${1, \dots, n}$ such that, for all $1 ⩽ l ⩽ n$ , we have $Q_{l} / {\tilde{z}}_{l} =_{ch} Q_{f (l)} / {\tilde{z}}_{f (l)}$ . Let $P^{'} = {P_{1}^{'}, \dots, P_{m}^{'}}$ and $Q^{'} = {Q_{1}^{'}, \dots, Q_{k}^{'}}$ , where $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ for all $i ⩽ m$ and $Q_{i}^{'} \in {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{i}] : : Q_{i})$ for all $i ⩽ k$ . We have $\begin{matrix} (B, E, P \cup Q) R_{1} (\emptyset, E, P^{'} \cup Q^{'} \cup {R}) \end{matrix}$ where $\begin{array}{rcl} R & \in & {a_{k + 1} (x_{k + 1}) . \dots . a_{n} (x_{n}) . \overline{c_{1}} ⟨ N_{f (1)} ⟩ . \dots . \overline{c_{n}} ⟨ N_{f (n)} ⟩ . R^{'} \\ | \begin{matrix} N_{l} = (| M_{l, 1}, \dots, M_{l, | ς_{l} |} |) for all l ⩽ k; N_{l} = x_{l} for all l > k; \\ R^{'} \in {swapper}_{1} (B^{'}); and variables x_{k + 1}, \dots, x_{n} are pairwise distinct \end{matrix}} \end{array}$

Remark.

Configuration $C = B, E, P \cup Q$ is waiting to synchronise at barrier t and configuration $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ represents an encoding of such a synchronisation with swapping. Multiset $Q$ contains k processes that are ready to synchronise at barrier t, while n processes are needed for the synchronisation to take place. The multiset $P$ may contain other processes that will synchronise at barrier t. In the configuration $C^{'}$ , the communications that implement the barrier t are partly done: the k processes in $Q^{'}$ , corresponding to the k processes in $Q$ , 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.

Suppose $B, E, P \cup Q$ is a valid annotated configuration, such that $P = {P_{1}, \dots, P_{m}}$ and $Q = {Q_{1}, \dots, Q_{k}}$ . Let $P^{'} = {P_{1}^{'}, \dots, P_{m}^{'}}$ and $Q^{'} = {Q_{1}^{'}, \dots, Q_{k}^{'}}$ , where $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ for all $i ⩽ m$ , and $Q_{i}^{'} \in {bar - elim}_{in} (\overline{c_{i}} ⟨ M_{i} ⟩, Q_{i})$ for all $i ⩽ k$ , for some pairwise distinct names $c_{1}, \dots, c_{k}$ in $E ∖ fn (P \cup Q)$ , and some ground tuples $M_{1}, \dots, M_{k}$ . We have $\begin{matrix} (B, E, P \cup Q) R_{2} (\emptyset, E, P^{'} \cup Q^{'} \cup {R}) \end{matrix}$ where $R \in {\overline{c_{1}} ⟨ M_{1} ⟩ . \dots . \overline{c_{k}} ⟨ M_{k} ⟩ . R^{'} ∣ R^{'} \in {swapper}_{1} (B)}$ .

Remark.

Configuration $C = B, E, P \cup Q$ has just synchronised and configuration $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \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 $Q^{'}$ contains k processes ready to receive these outputs. The condition $Q_{i}^{'} \in {bar - elim}_{in} (\overline{c_{i}} ⟨ M_{i} ⟩, Q_{i})$ constrains $M_{i}$ to be a tuple of terms that occur in $Q_{i}$ , so that $Q_{i}^{'}$ reduces to $bar - elim (Q_{i})$ after receiving $M_{i}$ on channel $c_{i}$ .

Suppose $P = {P_{1}, \dots, P_{m}}$ is a multiset of processes such that $barriers (P) = \emptyset$ , and E is a set of names. Let $P^{'} = {P_{1}^{'}, \dots, P_{m}^{'}}$ be a multiset of processes, where $P_{i}^{'} \in add-lets (P_{i})$ for all $i ⩽ m$ . We have: $\begin{matrix} (\emptyset, E, P) R_{3} (\emptyset, E, P^{'}) \end{matrix}$

Let

R = R_{1} \cup R_{2} \cup R_{3} \cup R_{1}^{- 1} \cup R_{2}^{- 1} \cup R_{3}^{- 1}

Relation $R$ relates $fst (C_{0})$ with $fst (C_{0}^{'})$ and $snd (C_{0})$ with $snd (C_{0}^{'})$ . Recall that $C_{0} = B_{0}, E, {P_{0}}$ and $C_{0}^{'} = \emptyset, E, {bar - elim (P_{0}), R_{0}}$ , where $B_{0} = barriers (P_{0})$ , $E = channels (B_{0})$ , and $R_{0} \in swapper (B_{0})$ . By Lemma 2, $C_{0} = C_{init} (P_{0})$ is valid, so $fst (C_{0})$ and $snd (C_{0})$ are valid. We notice that, if $R_{0} \in swapper (B_{0})$ , then $fst (R_{0}) \in {swapper}_{1} (fst (B_{0}))$ , using the identity function for f, and $snd (R_{0}) \in {swapper}_{1} (snd (B_{0}))$ , using the same function f as in the computation of $R_{0} \in swapper (B_{0})$ . Hence we have $fst (C_{0}) R_{2} fst (C_{0}^{'})$ with $B = fst (B_{0})$ , $k = 0$ , $P = {fst (P_{0})}$ , $P^{'} = bar - elim (P)$ , $Q^{'} = Q = \emptyset$ , $R = fst (R_{0})$ , and $snd (C_{0}) R_{2} snd (C_{0}^{'})$ similarly using $snd$ instead of $fst$ .

Relation $R$ satisfies the conditions of Definition 1 . The relation $R$ is symmetric and it remains to show that $R$ satisfies the three conditions of Definition 1. Let us first introduce the following results about our relation. Fact 1.

Given configurations $C = B, E, P \cup Q$ and $C^{'}$ such that $C R_{2} C^{'}$ , we have $C^{'} {\overset{}{\to}}^{*} \emptyset, E, bar - elim (P \cup Q) \cup {R^{'}}$ , where $R^{'} \in {swapper}_{1} (B)$ .

Proof of Fact 1.

We use the notations of the definition of $R_{2}$ . We transform $C^{'}$ by applying (Red I/O) k times between R and $Q_{i}^{'}$ for i from 1 to k. Then R reduces into $R^{'} \in {swapper}_{1} (B)$ and $Q_{i}^{'}$ reduces into an element of $add-lets (bar - elim (Q_{i}))$ . By Lemma 21, we reduce $P_{i}^{'}$ into $bar - elim (P_{i})$ and further reduce $Q_{i}^{'}$ into $bar - elim (Q_{i})$ , so Fact 1 holds. □

Fact 2.

Given configurations $C$ , $C^{'}$ , and $C_{1}$ such that $C R_{1} C^{'}$ with $k = n$ and $C \overset{}{\to} C_{1}$ by (Red Bar′), we have $C_{1} R_{2} C^{'}$ .

Fact 2 handles the swapping of data at barriers, so it is a key step of the proof. Proof of Fact 2.

We use the notations of the definition of $R_{1}$ . Since $Q$ contains n barriers, we have $C \overset{}{\to} C_{1} = B^{'}, E, P \cup {Q_{1} ς_{1}, \dots, Q_{n} ς_{n}}$ by (Red Bar′). We have $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ and since $k = n$ , we have $R = \overline{c_{1}} ⟨ N_{f (1)} ⟩ . \dots . \overline{c_{n}} ⟨ N_{f (n)} ⟩ . R^{'}$ with $N_{l} = (| M_{l, 1}, \dots, M_{l, | ς_{l} |} |)$ for all $l ⩽ n$ and $R^{'} \in {swapper}_{1} (B^{'})$ . Moreover, $Q^{'} = {Q_{1}^{'}, \dots, Q_{n}^{'}}$ with $Q_{i}^{'} \in {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{i}] : : Q_{i})$ for all $i ⩽ n$ . Since for all $1 ⩽ l ⩽ n$ , $Q_{l} / {\tilde{z}}_{l} =_{ch} Q_{f (l)} / {\tilde{z}}_{f (l)}$ , we have $\begin{matrix} Q_{l} {y_{1} / z_{l, 1}, \dots, y_{| {\tilde{z}}_{l} |} / z_{l, | {\tilde{z}}_{l} |}} =_{ch} Q_{f (l)} {y_{1} / z_{f (l), 1}, \dots, y_{| {\tilde{z}}_{l} |} / z_{f (l), | {\tilde{z}}_{l} |}}, \end{matrix}$ where $y_{1}, \dots, y_{| {\tilde{z}}_{l} |}$ are fresh variables, so we have $\begin{matrix} Q_{l} {y_{1} / z_{l, 1}, \dots, y_{| {\tilde{z}}_{l} |} / z_{l, | {\tilde{z}}_{l} |}} = Q_{f (l)} {y_{1} / z_{f (l), 1}, \dots, y_{| {\tilde{z}}_{l} |} / z_{f (l), | {\tilde{z}}_{l} |}} ρ_{l}, \end{matrix}$ for some renaming $ρ_{l}$ of channels of annotated barriers. (Recall that processes are considered equal modulo renaming of bound names and variables.) The renaming $ρ_{l}$ maps names in $channels (barriers (Q_{f (l)}))$ to names in $channels (barriers (Q_{l}))$ . Since the names in $channels (barriers (P \cup Q))$ are pairwise distinct, for $l \neq l^{'}$ , $channels (barriers (Q_{l})) \cap channels (barriers (Q_{l^{'}})) = \emptyset$ , so we can merge all functions $ρ_{l}$ for $1 ⩽ l ⩽ n$ into a single function ρ. Since furthermore f is a permutation, ρ is a permutation of $channels (B^{'})$ and leaves other names unchanged. Since the names in $channels (barriers (P \cup Q))$ are pairwise distinct, ρ leaves unchanged the names in $channels (barriers (P))$ and $a_{1}$ , $c_{1}$ , …, $a_{n}$ , $c_{n}$ . Hence, we obtain $\begin{matrix} bar - elim (Q_{i}) {y_{1} / z_{i, 1}, \dots, y_{| {\tilde{z}}_{i} |} / z_{i, | {\tilde{z}}_{i} |}} = bar - elim (Q_{f (i)}) {y_{1} / z_{f (i), 1}, \dots, y_{| {\tilde{z}}_{l} |} / z_{f (i), | {\tilde{z}}_{l} |}} ρ \end{matrix}$ for all $i ⩽ n$ by Lemma 8, so $\begin{matrix} {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{i}] : : Q_{i}) = {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{f (i)}] : : Q_{f (i)}) ρ \end{matrix}$ for all $i ⩽ n$ . (Recall that processes are considered equal modulo renaming of bound variables.) So $Q_{i}^{'} \in {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{f (i)}] : : Q_{f (i)}) ρ$ . Therefore, $Q_{i}^{'} \in {bar - elim}_{in} (\overline{c_{i}} ⟨ N_{f (i)} ⟩, Q_{f (i)} ς_{f (i)}) ρ$ , so $Q_{i}^{'} ρ^{- 1} \in {bar - elim}_{in} (\overline{c_{i}} ⟨ N_{f (i)} ⟩, Q_{f (i)} ς_{f (i)})$ . We define $Q_{1} = {Q_{1} ς_{1}, \dots, Q_{n} ς_{n}} = {Q_{f (1)} ς_{f (1)}, \dots, Q_{f (n)} ς_{f (n)}}$ since f is a permutation of ${1, \dots, n}$ , $Q_{1}^{'} = {Q_{1}^{'} ρ^{- 1}, \dots, Q_{n}^{'} ρ^{- 1}} = Q^{'} ρ^{- 1}$ , and $R_{1} = R ρ^{- 1} = \overline{c_{1}} ⟨ N_{f (1)} ⟩ . \dots . \overline{c_{n}} ⟨ N_{f (n)} ⟩ . R_{1}^{'}$ , where $R_{1}^{'} = R^{'} ρ^{- 1} \in {swapper}_{1} (B^{'} ρ^{- 1})$ since $R^{'} \in {swapper}_{1} (B^{'})$ . Moreover, $B^{'} ρ^{- 1} = B^{'}$ since $ρ^{- 1}$ maps a barrier of $Q_{l}$ to a barrier of $Q_{f (l)}$ for all $l ⩽ n$ and leaves other barriers unchanged. Therefore, $R_{1}^{'} \in {swapper}_{1} (B^{'})$ . Moreover, since $C$ is valid, the elements of $channels (B)$ are pairwise distinct so $c_{1}, \dots, c_{n}$ are pairwise distinct names. By Lemma 22, for all $i ⩽ n$ , $c_{i} \notin fn ({Q_{i} ς_{i}} \cup P \cup Q ∖ {t [a_{i}, c_{i}, ς_{i}] : : Q_{i}}) \supseteq fn (P \cup Q_{1})$ . Furthermore, $c_{1}, \dots, c_{n}$ are in $channels (B)$ , so they are in E since $C$ is valid, hence they are in $E ∖ fn (P \cup Q_{1})$ . We have $C^{'} = (\emptyset, E, P^{'} \cup Q^{'} \cup {R}) = (\emptyset, E ρ^{- 1}, P^{'} ρ^{- 1} \cup Q^{'} ρ^{- 1} \cup {R ρ^{- 1}})$ since configurations are considered equal modulo renaming, so $C^{'} = (\emptyset, E, P^{'} \cup Q_{1}^{'} \cup {R_{1}})$ . It follows that $C_{1} = (B^{'}, E, P \cup Q_{1}) R_{2} C^{'} = (\emptyset, E, P^{'} \cup Q_{1}^{'} \cup {R_{1}})$ using $N_{f (i)}$ for $M_{i}$ for all $i ⩽ n$ . □

We proceed with the proof of Proposition 7 by showing that $R$ satisfies the three conditions of Definition 1.

Condition 1. We show that, if $C R^{'} C^{'}$ and $C ↓_{N}$ , then $C^{'} {\overset{}{\to}}^{*} ↓_{N}$ , where $R^{'} \in {R_{1}, R_{2}, R_{3}, R_{1}^{- 1}, R_{2}^{- 1}, R_{3}^{- 1}}$ , by distinguishing the following cases:

In this case, $C = B, E, P \cup Q$ and $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ . By inspection of $P \cup Q$ , we have $P_{i} = \overline{N} ⟨ M ⟩ . Q \in P$ for some index i, process Q, and term M, with $fn (N) \cap E = \emptyset$ . It follows that $bar - elim (P_{i}) = \overline{N} ⟨ M ⟩ . bar - elim (Q)$ and by Lemma 21, $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ reduces into $bar - elim (P_{i})$ inside $C^{'}$ , hence $C^{'} {\overset{}{\to}}^{*} ↓_{N}$ .

In this case, $C = B, E, P \cup Q$ , where $\overline{N} ⟨ M ⟩ . Q \in P \cup Q$ for some process Q and term M, with $fn (N) \cap E = \emptyset$ . It follows that $\overline{N} ⟨ M ⟩ . bar - elim (Q) \in bar - elim (P \cup Q)$ . By Fact 1, we have $C^{'} {\overset{}{\to}}^{*} C_{1}^{'} = \emptyset, E, bar - elim (P \cup Q) \cup {R^{'}}$ , where $R^{'} \in {swapper}_{1} (B)$ and, moreover, $C_{1}^{'} ↓_{N}$ , hence, $C^{'} {\overset{}{\to}}^{*} ↓_{N}$ .

In this case, $C = \emptyset, E, P$ and $C^{'} = \emptyset, E, P^{'}$ , where $P_{i} = \overline{N} ⟨ M ⟩ . Q \in P$ for some index i, process Q and term M, with $fn (N) \cap E = \emptyset$ . We have $P_{i}^{'} \in add-lets (P_{i})$ , so by Lemma 21, $P_{i}^{'}$ reduces into $P_{i}$ inside $C^{'}$ . It follows immediately that $C^{'} {\overset{}{\to}}^{*} ↓_{N}$ .

In this case, $C = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ and $C^{'} = B, E, P \cup Q$ . We have $\overline{N} ⟨ M ⟩ . Q \in P^{'} \cup Q^{'} \cup {R}$ for some process Q and term M, with $fn (N) \cap E = \emptyset$ . The process R cannot be the output $\overline{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 $P^{'} \cup Q^{'} \cup {R}$ , we have $P_{i}^{'} = \overline{N} ⟨ M ⟩ . Q = bar - elim (P_{i}) \in P^{'}$ for some index i, and $C^{'} ↓_{N}$ by Lemma 20.

In this case $C = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ and $C^{'} = B, E, P \cup Q$ . We have $\overline{N} ⟨ M ⟩ . Q \in P^{'} \cup Q^{'} \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 ∖ fn (P \cup Q)$ . 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 $\overline{N} ⟨ M ⟩ . Q$ . Therefore, by inspection of $P^{'} \cup Q^{'} \cup {R}$ , we have $P_{i}^{'} = \overline{N} ⟨ M ⟩ . Q = bar - elim (P_{i}) \in P^{'}$ for some index i, and $C^{'} ↓_{N}$ by Lemma 20.

In this case, $C = \emptyset, E, P^{'}$ and $C^{'} = \emptyset, E, P$ . By inspection of $P^{'}$ , it follows that $P_{i}^{'} = \overline{N} ⟨ M ⟩ . Q = P_{i} \in P$ for some index i, process Q, and term M, with $fn (N) \cap E = \emptyset$ , and, hence, $C^{'} ↓_{N}$ .

Condition 2. We show that, if $C R^{'} C^{'}$ and $C \overset{}{\to} C_{1}$ , then $C^{'} {\overset{}{\to}}^{*} C_{1}^{'}$ and $C_{1} R C_{1}^{'}$ for some $C_{1}^{'}$ , where $R^{'} \in {R_{1}, R_{2}, R_{3}, R_{1}^{- 1}, R_{2}^{- 1}, R_{3}^{- 1}}$ , by distinguishing the following cases:

We have $C = B, E, P \cup Q$ and $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ , with the conditions given in the definition of $R_{1}$ . Let us distinguish two cases:

Case I: $C \overset{}{\to} C_{1}$ by $(R ED B AR$ ’). In this case, $C = B, E, P \cup Q$ , $Q = {t [a_{1}, c_{1}, ς_{1}] : : Q_{1}, \dots, t [a_{k}, c_{k}, ς_{k}] : : Q_{k}}$ , $P = P_{1} \cup {t [a_{k + 1}, c_{k + 1}, ς_{k + 1}] : : Q_{k + 1}, \dots, t [a_{n}, c_{n}, ς_{n}] : : Q_{n}}$ , and $C_{1} = B^{'}, E, P_{1} \cup {Q_{1} ς_{1}, \dots, Q_{n} ς_{n}}$ , where $B^{'} = B ∖ {t [a_{1}, c_{1}, {\tilde{z}}_{1}] : : Q_{1}, \dots, t [a_{n}, c_{n}, {\tilde{z}}_{n}] : : Q_{n}}$ and ${\tilde{z}}_{i} = ordom (ς_{i})$ for all $i ⩽ n$ . For a suitable numbering of processes, we have $P_{i} = t [a_{k + i}, c_{k + i}, ς_{k + i}] : : Q_{k + i}$ for $i = 1, \dots, n - k$ and $P_{1} = {P_{n - k + 1}, \dots, P_{m}}$ . Since $C R_{1} C^{'}$ , we have $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ where $P^{'} = {P_{1}^{'}, \dots, P_{m}^{'}}$ with $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ for all $i ⩽ m$ and $Q^{'} = {Q_{1}^{'}, \dots, Q_{k}^{'}}$ with $Q_{i}^{'} \in {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{i}] : : Q_{i})$ for all $i ⩽ k$ . By Lemma 21, we can reduce the lets so that $C^{'} {\overset{}{\to}}^{*} C_{2}^{'} = \emptyset, E, P_{2}^{'} \cup Q^{'} \cup {R}$ where $P_{2}^{'} = {P_{1}^{″}, \dots, P_{m}^{″}}$ with $P_{i}^{″} = bar - elim (P_{i})$ for all $i ⩽ m$ . Furthermore, we can reduce each $P_{i}^{″} \in bar - elim (t [a_{k + i}, c_{k + i}, ς_{k + i}] : : Q_{k + i})$ for $i = 1, \dots, n - k$ with R by (Red I/O), so that $C_{2}^{'} {\overset{}{\to}}^{n - k} C_{1}^{'} = \emptyset, E, P_{1}^{'} \cup Q_{1}^{'} \cup {R_{1}}$ , where $P_{1}^{'} = {P_{n - k + 1}^{″}, \dots, P_{m}^{″}}$ with $P_{i}^{″} = bar - elim (P_{i})$ for $i = n - k + 1, \dots, m$ , $Q_{1}^{'} = {Q_{1}^{'}, \dots, Q_{n}^{'}}$ with $Q_{i}^{'} \in {bar - elim}_{in}^{'} (t [a_{i}, c_{i}, ς_{i}] : : Q_{i})$ for all $i ⩽ n$ , and $R_{1} = \overline{c_{1}} ⟨ N_{f (1)} ⟩ . \dots . \overline{c_{n}} ⟨ N_{f (n)} ⟩ . R^{'}$ where $N_{l} = (| M_{l, 1}, \dots, M_{l, | ς_{l} |} |)$ for all $l ⩽ n$ and $R^{'} \in {swapper}_{1} (B^{'})$ . After these reductions, we obtain $C R_{1} C_{1}^{'}$ with $k = n$ . By Fact 2, we have $C_{1} R_{2} C_{1}^{'}$ . Therefore, $C_{1} R C_{1}^{'}$ and $C^{'} {\overset{}{\to}}^{*} C_{1}^{'}$ .

Case II: $C \overset{}{\to} C_{1}$ without application of $(R ED B AR)$ . By inspection of our reduction rules, the reduction $C \overset{}{\to} C_{1}$ is obtained by reducing processes in $P$ and $C_{1} = B, E_{1}, P_{1} \cup Q$ for some multiset of processes $P_{1}$ and set of names $E_{1}$ . By Lemma 21, we can reduce the lets in $P^{'}$ so that $C^{'} \to^{*} C_{2}^{'} = B, E_{1}, bar - elim (P) \cup Q^{'} \cup {R}$ . By Lemma 9(1), $C_{2}^{'} \overset{}{\to} C_{1}^{'}$ , where $C_{1}^{'} = \emptyset, E_{1}, bar - elim (P_{1}) \cup Q^{'} \cup {R}$ . Hence, $C_{1} R_{1} C_{1}^{'}$ (with k, n, f unchanged), therefore, $C_{1} R C_{1}^{'}$ and $C^{'} {\overset{}{\to}}^{*} C_{1}^{'}$ .

We have $C = B, E, P \cup Q$ and $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ , with the conditions given in the definition of $R_{2}$ . By Fact 1, we have $C^{'} {\overset{}{\to}}^{*} C_{2}^{'} = \emptyset, E, bar - elim (P \cup Q) \cup {R^{'}}$ , where $R^{'} \in {swapper}_{1} (B)$ .

Case I: $B = \emptyset$ . Since $C$ is a valid configuration, we have $barriers (P \cup Q) \subseteq B$ , so $P$ and $Q$ contain no barrier, therefore, $P \cup Q = bar - elim (P \cup Q)$ by definition of $bar - elim$ (Fig. 6). By definition of ${swapper}_{1}$ , we have $R^{'} = {0}$ . Hence, $C^{'} {\overset{}{\to}}^{*} C_{2}^{'} = \emptyset, E, P \cup Q \cup {0} \overset{}{\to} C = \emptyset, E, P \cup Q$ . Since $C \overset{}{\to} C_{1}$ , we have $C^{'} {\overset{}{\to}}^{*} C_{1}$ . Moreover, we have $C_{1} R_{3} C_{1}$ , so $C_{1} R C_{1}$ , and we conclude with $C_{1}^{'} = C_{1}$ .

Case II: $B \neq \emptyset$ . We have $C R_{1} C_{2}^{'}$ with $k = 0$ by expanding the definition of ${swapper}_{1} (B)$ , and we conclude by the case $R^{'} = R_{1}$ above.

We have $C = \emptyset, E, P$ and $C^{'} = \emptyset, E, P^{'}$ with $barriers (P) = \emptyset$ and $P_{i}^{'} \in add-lets (P_{i})$ for all $i ⩽ m$ . By Lemma 21, we can reduce the lets in $P^{'}$ so that $C^{'} {\overset{}{\to}}^{*} C = \emptyset, E, P$ . Since $C \overset{}{\to} C_{1}$ , we have $C^{'} {\overset{}{\to}}^{*} C_{1}$ . Moreover, we have $C_{1} R_{3} C_{1}$ , so $C_{1} R C_{1}$ , and we conclude with $C_{1}^{'} = C_{1}$ .

We have $C = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ and $C^{'} = B, E, P \cup Q$ , with the conditions given in the definition of $R_{1}$ .

Case I: $k = n$ . Since $Q$ contains n barriers, we have $C^{'} \overset{}{\to} C_{2}^{'} = B^{'}, E, P \cup {Q_{1} ς_{1}, \dots, Q_{n} ς_{n}}$ by (Red Bar′). By Fact 2, we have $C_{2}^{'} R_{2} C$ , so we conclude by the case $R^{'} = R_{2}^{- 1}$ (below).

Case II: $k < n$ .

Case II.1: $C \overset{}{\to} C_{1}$ by reducing at least R. Since R starts with an input on $a_{k + 1}$ , it can only reduce by (Red I/O) with an output on $a_{k + 1}$ . The processes in $Q^{'}$ start with an input, so they cannot reduce with R. Hence R reduces with a process $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ in $P^{'}$ . If $P_{i}^{'}$ starts with a let, it cannot reduce by (Red I/O), so we have $P_{i}^{'} = bar - elim (P_{i})$ . Since $a_{k + 1} \in channels (B)$ and $C^{'}$ is valid, $a_{k + 1} \notin fn - nobc (P \cup Q)$ , so $a_{k + 1}$ occurs free in $P \cup Q$ only as channel of a barrier in $P \cup Q$ . Since $P_{i}^{'} = bar - elim (P_{i})$ starts with an output on $a_{k + 1}$ and $barriers (P_{i}) \subseteq B$ , we have $P_{i} = t [a_{k + 1}, c_{k + 1}, ς_{k + 1}] : : Q_{k + 1}$ for some $ς_{k + 1} = (M_{k + 1, 1} / z_{k + 1, 1}, \dots, M_{k + 1, | ς_{k + 1} |} / z_{k + 1, | ς_{k + 1} |})$ . Let $N_{k + 1}^{'} = (| M_{k + 1, 1}, \dots, M_{k + 1, | ς_{k + 1} |} |)$ and for all $l \neq k + 1$ , $N_{l}^{'} = N_{l}$ . We have $\begin{array}{l} P_{i}^{'} = & \overline{a_{k + 1}} ⟨ N_{k + 1}^{'} ⟩ . c_{k + 1} (z) . let z_{k + 1, 1} = π_{1, | ς_{k + 1} |} (z) in \dots \\ let z_{k + 1, | ς_{k + 1} |} = π_{| ς_{k + 1} |, | ς_{k + 1} |} (z) in bar - elim (Q_{k + 1}) . \end{array}$ Let $\begin{array}{rcl} Q_{k + 1}^{'} & = & c_{k + 1} (z) . let z_{k + 1, 1} = π_{1, | ς_{k + 1} |} (z) in \dots \\ let z_{k + 1, | ς_{k + 1} |} = π_{| ς_{k + 1} |, | ς_{k + 1} |} (z) in bar - elim (Q_{k + 1}) \\ \in {bar - elim}_{in}^{'} (t [a_{k + 1}, c_{k + 1}, ς_{k + 1}] : : Q_{k + 1}) . \end{array}$ After reduction by (Red I/O), $P_{i}^{'}$ becomes $Q_{k + 1}^{'}$ and R becomes $R_{1} = a_{k + 2} (x_{k + 2}) . \dots . a_{n} (x_{n}) . \overline{c_{1}} ⟨ N_{f (1)}^{'} ⟩ . \dots . \overline{c_{n}} ⟨ N_{f (n)}^{'} ⟩ . R^{'}$ . Let $P_{1} = P ∖ {P_{i}}$ , $Q_{1} = Q^{'} \cup {P_{i}} = Q^{'} \cup {t [a_{k + 1}, c_{k + 1}, ς_{k + 1}] : : Q_{k + 1}}$ , $P_{1}^{'} = P^{'} ∖ {P_{i}^{'}}$ , and $Q_{1}^{'} = Q^{'} \cup {Q_{k + 1}^{'}}$ . Then we have $C = (\emptyset, E, P^{'} \cup Q^{'} \cup {R}) \overset{}{\to} C_{1} = (\emptyset, E, P_{1}^{'} \cup Q_{1}^{'} \cup {R_{1}})$ and $C^{'} = (B, E, P_{1} \cup Q_{1}) R_{1} C_{1} = (\emptyset, E, P_{1}^{'} \cup Q_{1}^{'} \cup {R_{1}})$ (with m decreased by one, k increased by one, and f unchanged), so we conclude with $C_{1}^{'} = C^{'}$ .

Case II.2: $C \overset{}{\to} C_{1}$ by reducing at least a process in $Q^{'}$ . Since we reduce $Q_{i}^{'} \in Q^{'}$ , which starts with an input on $c_{i}$ , this process can only reduce by (Red I/O), with an output on $c_{i}$ . If it reduced with $P_{j}^{'} \in P^{'}$ , since $P_{j}^{'} \in add-lets (bar - elim (P_{j}))$ , we would actually have $P_{j}^{'} = bar - elim (P_{j})$ . Since $C$ is valid, by Lemma 22, $c_{i} \notin fn (P)$ , so $c_{i} \notin fn (P_{j}^{'}) = fn (bar - elim (P_{j})) = fn (P_{j})$ , hence $Q_{i}^{'}$ cannot reduce with a process $P_{j}^{'} \in P^{'}$ . It also cannot reduce with R or with another process in $Q^{'}$ since they start with an input. Therefore, this case cannot happen.

Case II.3: $C \overset{}{\to} C_{1}$ by reducing only processes in $P^{'}$ .

Case II.3.1: a reduced process is $P_{i}^{'} \neq bar - elim (P_{i})$ . We have $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ . By Lemma 21, $C_{1} = \emptyset, E, (P^{'} ∖ {P_{i}^{'}}) \cup {P_{i}^{″}} \cup Q^{'} \cup {R}$ with $P_{i}^{″} \in add-lets (bar - elim (P_{i}))$ , so we still have $C^{'} R_{1} C_{1}$ , so we conclude with $C_{1}^{'} = C^{'}$ .

Case II.3.2: the reduced process(es) are $P_{i}^{'} = bar - elim (P_{i})$ and possibly $P_{j}^{'} = bar - elim (P_{j})$ . Let $P_{red}^{'} = {P_{i}^{'}}$ or $P_{red}^{'} = {P_{i}^{'}, P_{j}^{'}}$ be the multiset of reduced processes, such that $P_{red}^{'} = bar - elim (P_{red})$ , $P^{'} = P_{stay}^{'} \cup P_{red}^{'}$ , $P = P_{stay} \cup P_{red}$ . We have $C = (\emptyset, E, P_{stay}^{'} \cup bar - elim (P_{red}) \cup Q^{'} \cup {R}) \overset{}{\to} C_{1} = (\emptyset, E_{1}, P_{stay}^{'} \cup P_{red 1}^{'} \cup Q^{'} \cup {R})$ by reducing one or more processes in $bar - elim (P_{red})$ , so by Lemma 9(2), there exists $P_{red 1}$ such that $P_{red 1}^{'} = bar - elim (P_{red 1})$ and $C^{'} = (B, E, P_{stay} \cup P_{red} \cup Q) \overset{}{\to} C_{1}^{'} = (B, E, P_{stay} \cup P_{red 1} \cup Q)$ . Letting $P_{1} = P_{stay} \cup P_{red 1}$ and $P_{1}^{'} = P_{stay}^{'} \cup P_{red 1}^{'}$ , we obtain that $C_{1}^{'} = (B, E, P_{1} \cup Q) R_{1} C_{1} = (\emptyset, E_{1}, P_{1}^{'} \cup Q^{'} \cup {R})$ (with f, k, n unchanged), so $C_{1} R C_{1}^{'}$ .

We have $C = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ and $C^{'} = B, E, P \cup Q$ , with the conditions given in the definition of $R_{2}$ . We distinguish several cases.

Case I: $C \overset{}{\to} C_{1}$ by reducing at least R.

Case I.1: $k = 0$ . In this case, $Q = Q^{'} = \emptyset$ .

Case I.1.1: $B = \emptyset$ . Then $R = 0$ , so $C \overset{}{\to} C_{1} = \emptyset, E, P^{'}$ , $C^{'} = \emptyset, E, P$ , and furthermore since $B = \emptyset$ , we have $barriers (P) = \emptyset$ , so $P_{i}^{'} \in add-lets (bar - elim (P_{i})) = add-lets (P_{i})$ , so $C^{'} R_{3} C_{1}$ , so $C_{1} R C^{'}$ . We conclude with $C_{1}^{'} = C^{'}$ .

Case I.1.2: $B \neq \emptyset$ . Then we have $C^{'} R_{1} C$ by expanding the definition of ${swapper}_{1} (B)$ , we conclude by using the case $R^{'} = R_{1}^{- 1}$ , Case II.1 ( $k < n$ , $C \overset{}{\to} C_{1}$ by reducing R, above).

Case I.2: $k > 0$ . The process R starts with an output on $c_{1}$ , hence it can only reduce by (Red I/O) with an input on $c_{1}$ . If R reduced with $P_{i}^{'} \in P^{'}$ , since $P_{i}^{'} \in add-lets (bar - elim (P_{i}))$ , we would actually have $P_{i}^{'} = bar - elim (P_{i})$ . By definition of $R_{2}$ , $c_{1} \notin fn (P_{i})$ , so $c_{1} \notin fn (P_{i}^{'}) = fn (bar - elim (P_{i})) = fn (P_{i})$ , hence R cannot reduce with $P_{i}^{'} \in P^{'}$ . 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 (Red I/O). After reduction, R is transformed into $\begin{matrix} R_{1} = \overline{c_{2}} ⟨ M_{2} ⟩ . \dots . \overline{c_{k}} ⟨ M_{k} ⟩ . R^{'} \end{matrix}$ with $R^{'} \in {swapper}_{1} (B)$ , and since $Q_{1}^{'} \in {bar - elim}_{in} (\overline{c_{1}} ⟨ M_{1} ⟩, Q_{1})$ , $\begin{matrix} Q_{1}^{'} = c_{1} (z) . let z_{1} = π_{1, n} (z) in \dots let z_{n} = π_{n, n} (z) in bar - elim (Q^{'}) \end{matrix}$ with $M_{1} = (| N_{1}, \dots, N_{n} |)$ , $Q_{1} = Q^{'} {N_{1} / z_{1}, \dots, N_{n} / z_{n}}$ , and $z, z_{1}, \dots, z_{n}$ pairwise distinct variables is transformed into $\begin{array}{l} P_{m + 1}^{'} & = let z_{1} = π_{1, n} (M_{1}) in \dots let z_{n} = π_{n, n} (M_{1}) in bar - elim (Q^{'}) \\ \in add-lets (bar - elim (Q_{1})) \end{array}$ because $bar - elim (Q_{1}) = bar - elim (Q^{'}) {N_{1} / z_{1}, \dots, N_{n} / z_{n}}$ by Lemma 8. We let $P_{1} = P \cup {Q_{1}}$ , $Q_{1} = Q ∖ {Q_{1}}$ , $P_{1}^{'} = P^{'} \cup {P_{m + 1}^{'}}$ , and $Q_{1}^{'} = Q^{'} ∖ {Q_{1}^{'}}$ . Then we have $C = (\emptyset, E, P^{'} \cup Q^{'} \cup {R}) \overset{}{\to} C_{1} = (\emptyset, E, P_{1}^{'} \cup Q_{1}^{'} \cup {R_{1}})$ and $C^{'} = (B, E, P \cup Q) = (B, E, P_{1} \cup Q_{1}) R_{2} C_{1} = (\emptyset, E, P_{1}^{'} \cup Q_{1}^{'} \cup {R_{1}})$ (with k decreased by one and m increased by one), so we conclude with $C_{1}^{'} = C^{'}$ .

Case II: $C \overset{}{\to} C_{1}$ by reducing at least a process in $Q^{'}$ and not reducing R. Since we reduce $Q_{i}^{'} \in Q^{'}$ , which starts with an input on $c_{i}$ , this process can reduce only by (Red I/O), with an output on $c_{i}$ . If it reduced with $P_{j}^{'} \in P^{'}$ , since $P_{j}^{'} \in add-lets (bar - elim (P_{j}))$ , we would actually have $P_{j}^{'} = bar - elim (P_{j})$ . By definition of $R_{2}$ , $c_{i} \notin fn (P_{j})$ , so $c_{i} \notin fn (P_{j}^{'}) = fn (bar - elim (P_{j})) = fn (P_{j})$ , hence $Q_{i}^{'}$ cannot reduce with a process $P_{j}^{'} \in P^{'}$ . Moreover, $Q_{i}^{'}$ cannot reduce with another process in $Q^{'}$ because all these processes start with inputs. Therefore, this case is impossible.

Case III: $C \overset{}{\to} C_{1}$ by reducing only processes in $P^{'}$ . This case is similar to the case $R^{'} = R_{1}^{- 1}$ , Case II.3.

We have $C = \emptyset, E, P^{'}$ and $C^{'} = \emptyset, E, P$ with $barriers (P) = \emptyset$ , $P = {P_{1}, \dots, P_{m}}$ , $P^{'} = {P_{1}^{'}, \dots, P_{m}^{'}}$ , and for all $i ⩽ m$ , $P_{i}^{'} \in add-lets (P_{i})$ .

Case I: a reduced process is $P_{i}^{'} \neq P_{i}$ . We have $P_{i}^{'} \in add-lets (P_{i})$ . By Lemma 21, $C_{1} = \emptyset, E, (P^{'} ∖ {P_{i}^{'}}) \cup {P_{i}^{″}}$ with $P_{i}^{″} \in add-lets (P_{i})$ , so we still have $C^{'} R_{3} C_{1}$ , so we conclude with $C_{1}^{'} = C^{'}$ .

Case II: the reduced process(es) are $P_{i}^{'} = P_{i}$ and possibly $P_{j}^{'} = P_{j}$ . Let $P_{red} = {P_{i}}$ or $P_{red} = {P_{i}, P_{j}}$ be the multiset of reduced processes, $P^{'} = P_{stay}^{'} \cup P_{red}$ , and $P = P_{stay} \cup P_{red}$ . We have $C = (\emptyset, E, P_{stay}^{'} \cup P_{red}) \overset{}{\to} C_{1} = (\emptyset, E_{1}, P_{stay}^{'} \cup P_{red 1})$ by reducing one or more processes in $P_{red}$ . Since the reduction rules are independent of the non-reduced processes, we also have $C^{'} = (\emptyset, E, P_{stay} \cup P_{red}) \overset{}{\to} C_{1}^{'} = (\emptyset, E_{1}, P_{stay} \cup P_{red 1})$ and furthermore $C_{1}^{'} R_{3} C_{1}$ , so $C_{1} R C_{1}^{'}$ .

Condition 3. We show that, if $C R_{i} C^{'}$ and $C [_]$ is an adversarial context, then $C [C] R_{i} C [C^{'}]$ , for $i \in {1, 2, 3}$ . Let $C [_] = ν \tilde{n} . (_∣ Q)$ with $fv (Q) = \emptyset$ and $barriers (Q) = \emptyset$ . We rename E in $C$ and $C^{'}$ so that $E \cap fn (Q) = \emptyset$ .

We have $C = B, E, P \cup Q$ and $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ . Let $P_{1} = P \cup {Q}$ , $P_{1}^{'} = P^{'} \cup {Q}$ , and $E_{1} = E \cup {\tilde{n}}$ . Since Q contains no barrier, we have $bar - elim (Q) = Q$ , so $Q \in add-lets (bar - elim (Q))$ , hence $C [C] = (B, E_{1}, P_{1} \cup Q) R_{1} C [C^{'}] = (\emptyset, E_{1}, P_{1}^{'} \cup Q^{'} \cup {R})$ (with m increased by one and k, n, f unchanged).

We have $C = B, E, P \cup Q$ and $C^{'} = \emptyset, E, P^{'} \cup Q^{'} \cup {R}$ . Let $P_{1} = P \cup {Q}$ , $P_{1}^{'} = P^{'} \cup {Q}$ , and $E_{1} = E \cup {\tilde{n}}$ . Since Q contains no barrier, we have $bar - elim (Q) = Q$ , so $Q \in add-lets (bar - elim (Q))$ , hence $C [C] = (B, E_{1}, P_{1} \cup Q) R_{2} C [C^{'}] = (\emptyset, E_{1}, P_{1}^{'} \cup Q^{'} \cup {R})$ (with m increased by one and k unchanged.)

We have $C = B, E, P$ and $C^{'} = \emptyset, E, P^{'}$ . Let $P_{1} = P \cup {Q}$ , $P_{1}^{'} = P^{'} \cup {Q}$ , and $E_{1} = E \cup {\tilde{n}}$ . We have $Q \in add-lets (Q)$ , so $C [C] = (B, E_{1}, P_{1}) R_{3} C [C^{'}] = (\emptyset, E_{1}, P_{1}^{'})$ (with m increased by one).

Conclusion. Since $R$ is symmetric and satisfies the three conditions of Definition 1, we have $R \subseteq \approx$ . Since $fst (C_{0}) R fst (C_{0}^{'})$ and $snd (C_{0}) R snd (C_{0}^{'})$ , we conclude that $fst (C_{0}) \approx fst (C_{0}^{'})$ and $snd (C_{0}) \approx snd (C_{0}^{'})$ . □

Proofs of Propositions 10 and 11

Proofs for Section 3.5.1 (replicated barriers)

References

Abadi , Security protocols and their properties, in: Foundations of Secure Computation, NATO Science Series, IOS Press, 2000, pp. 39–60.

Abadi and

Blanchet , Computer-assisted verification of a protocol for certified email, Science of Computer Programming 58(1–2) (2005), 3–27, Special issue SAS’03. doi:10.1016/j.scico.2005.02.002.

Abadi and

Cortier , Deciding knowledge in security protocols under equational theories, Theoretical Computer Science 367(1–2) (2006), 2–32. doi:10.1016/j.tcs.2006.08.032.

Abadi and

Fournet , Mobile values, new names, and secure communication, in: POPL’01: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 2001, pp. 104–115. doi:10.1145/360204.360213.

Abadi and

A.D.

Gordon , A calculus for cryptographic protocols: The spi calculus, in: CCS’97: 4th ACM Conference on Computer and Communications Security, ACM Press, 1997, pp. 36–47. doi:10.1145/266420.266432.

Abadi and

A.D.

Gordon , A bisimulation method for cryptographic protocols, Nordic Journal of Computing 5(4) (1998), 267–303.

Adida ,

de Marneffe ,

Pereira and

J.-J.

Quisquater , Electing a university president using open-audit voting: Analysis of real-world use of Helios, in: EVT/WOTE’09: Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, USENIX Association, 2009.

Arapinis ,

Liu ,

Ritter and

Ryan , Stateful applied pi calculus, in: POST’14: 3rd Conference on Principles of Security and Trust, LNCS, Vol. 8414, Springer, 2014, pp. 22–41. doi:10.1007/978-3-642-54792-8_2.

N.S.

Arenstorf and

H.F.

Jordan , Comparing barrier algorithms, International Journal of Parallel Computing 12(2) (1989), 157–170. doi:10.1016/0167-8191(89)90050-1.

10.

Backes ,

Hriţcu and

Maffei , Automated verification of remote electronic voting protocols in the applied pi-calculus, in: CSF’08: 21st IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2008, pp. 195–209.

11.

Basin ,

Dreier and

Casse , Automated symbolic proofs of observational equivalence, in: CCS’15: 22nd ACM Conference on Computer and Communications Security, ACM, 2015, pp. 1144–1155. doi:10.1145/2810103.2813662.

12.

Baudet , Deciding security of protocols against off-line guessing attacks, in: CCS’05: 12th ACM Conference on Computer and Communications Security, ACM Press, 2005, pp. 16–25. doi:10.1145/1102120.1102125.

13.

Baudet , Sécurité des protocoles cryptographiques: aspects logiques et calculatoires, PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, 2007.

14.

Blanchet , Automatic proof of strong secrecy for security protocols, in: S&P’04: 25th IEEE Symposium on Security and Privacy, IEEE Computer Society, 2004, pp. 86–100.

15.

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

16.

Blanchet , Automatic verification of correspondences for security protocols, Journal of Computer Security 17(4) (2009), 363–434. doi:10.3233/JCS-2009-0339.

17.

Blanchet , Modeling and verifying security protocols with the applied pi calculus and ProVerif, Foundations and Trends in Privacy and Security 1(1–2) (2016), 1–135. doi:10.1561/3300000004.

18.

Blanchet ,

Abadi and

Fournet , Automated verification of selected equivalences for security protocols, Journal of Logic and Algebraic Programming 75(1) (2008), 3–51. doi:10.1016/j.jlap.2007.06.002.

19.

Blanchet and

Smyth , Automated reasoning for equivalences in the applied pi calculus with barriers, in: CSF’16: 29th Computer Security Foundations Symposium, IEEE Computer Society, 2016, pp. 310–324.

20.

Blanchet ,

Smyth and

Cheval , ProVerif 1.96: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2016, Originally appeared as Bruno Blanchet and Ben Smyth (2011) ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial.

21.

Borgström ,

Briais and

Nestmann , Symbolic bisimulation in the spi calculus, in: CONCUR’04: 15th International Conference on Concurrency Theory, LNCS, Vol. 3170, Springer, 2004, pp. 161–176.

22.

Borgström and

Nestmann , On bisimulations for the spi calculus, Mathematical Structures in Computer Science 15(3) (2005), 487–552. doi:10.1017/S0960129505004706.

23.

E.D.

Brooks III , The butterfly barrier, International Journal of Parallel Programming 15(4) (1986), 295–307. doi:10.1007/BF01407877.

24.

Chadha ,

Ciobâca and

Kremer , Automated verification of equivalence properties of cryptographic protocols, in: ESOP’12: 21st European Symposium on Programming, LNCS, Vol. 7211, Springer, 2012, pp. 108–127.

25.

Cheval and

Blanchet , Proving more observational equivalences with ProVerif, in: POST’13: 2nd Conference on Principles of Security and Trust, LNCS, Vol. 7796, Springer, 2013, pp. 226–246. doi:10.1007/978-3-642-36830-1_12.

26.

Cheval ,

Comon-Lundh and

Delaune , Trace equivalence decision: Negative tests and non-determinism, in: CCS’11: Proceedings of the 18th ACM Conference on Computer and Communications Security, ACM Press, 2011, pp. 321–330. doi:10.1145/2046707.2046744.

27.

Chothia , Analysing the MUTE anonymous file-sharing system using the pi-calculus, in: FORTE’06: 26th International Conference on Formal Techniques for Networked and Distributed Systems, LNCS, Vol. 4229, Springer, 2006, pp. 115–130.

28.

Chothia ,

Orzan ,

Pang and

M.T.

Dashti , A framework for automatically checking anonymity with μCRL, in: TGC’06: 2nd Symposium on Trustworthy Global Computing, LNCS, Vol. 4661, Springer, 2007, pp. 301–318. doi:10.1007/978-3-540-75336-0_19.

29.

Chrétien ,

Cortier and

Delaune , Decidability of trace equivalence for protocols with nonces, in: CSF’15: Proceedings of the 28th IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2015, pp. 170–184.

30.

Chrétien ,

Cortier and

Delaune , From security protocols to pushdown automata, ACM Transactions on Computational Logic 17(1) (2015), 3.

31.

Ciobâca , Verification and Composition of Security Protocols with Applications to Electronic Voting, PhD thesis, Laboratoire Spécification et Vérification, ENS Cachan & CNRS & INRIA, 2011.

32.

Cortier and

Delaune , A method for proving observational equivalence, in: CSF’09: 22nd IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2009, pp. 266–276.

33.

Cortier ,

Rusinowitch and

Zǎlinescu , Relating two standard notions of secrecy, Logical Methods in Computer Science 3(3) (2007). doi:10.2168/LMCS-3(3:2)2007.

34.

Cortier and

Smyth , Attacking and fixing Helios: An analysis of ballot secrecy, Journal of Computer Security 21(1) (2013), 89–148. doi:10.3233/JCS-2012-0458.

35.

Cremers and

Hirschi , Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy, 2017.

36.

Dahl ,

Delaune and

Steel , Formal analysis of privacy for vehicular mix-zones, in: ESORICS’10: 15th European Symposium on Research in Computer Security, LNCS, Vol. 6345, Springer, 2010, pp. 55–70.

37.

Dahl ,

Delaune and

Steel , Formal analysis of privacy for anonymous location based services, in: TOSCA’11: Proceedings of the Workshop on Theory of Security and Applications, LNCS, Vol. 6993, Springer, 2011, pp. 98–112. doi:10.1007/978-3-642-27375-9_6.

38.

Delaune ,

Kremer and

Pereira , Simulation based security in the applied pi calculus, in: FSTTCS: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Leibniz International Proceedings in Informatics, Vol. 4, Leibniz-Zentrum für Informatik, 2009, pp. 169–180.

39.

Delaune ,

Kremer and

M.D.

Ryan , Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security 17(4) (2009), 435–487. doi:10.3233/JCS-2009-0340.

40.

Delaune ,

Kremer and

M.D.

Ryan , Symbolic bisimulation for the applied pi calculus, Journal of Computer Security 18(2) (2010), 317–377. doi:10.3233/JCS-2010-0363.

41.

Delaune ,

M.D.

Ryan and

Smyth , Automatic verification of privacy properties in the applied pi-calculus, in: IFIPTM’08: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security, International Federation for Information Processing, Vol. 263, Springer, 2008, pp. 263–278.

42.

Dreier ,

Duménil ,

Kremer and

Sasse , Beyond subterm-convergent equational theories in automated verification of stateful protocols, in: 6th International Conference on Principles of Security and Trust (POST),

Maffei and

Ryan, eds, LNCS, Vol. 10204, Springer, Uppsala, Sweden, 2017, pp. 117–140. doi:10.1007/978-3-662-54455-6_6.

43.

Dreier ,

Lafourcade and

Lakhnech , Vote-independence: A powerful privacy notion for voting protocols, in: FPS’11: 4th Workshop on Foundations & Practice of Security, LNCS, Vol. 6888, Springer, 2011, pp. 164–180. doi:10.1007/978-3-642-27901-0_13.

44.

Durante ,

Sisto and

Valenzano , Automatic testing equivalence verification of spi calculus specifications, ACM Transactions on Software Engineering and Methodology 12(2) (2003), 222–284. doi:10.1145/941566.941570.

45.

Freudiger ,

Raya ,

Félegyházi ,

Papadimitratos and

J.-P.

Hubaux , Mix-zones for location privacy in vehicular networks, in: WiN-ITS’07: 1st International Workshop on Wireless Networking for Intelligent Transportation Systems, 2007.

46.

Hensgen ,

Finkel and

Manber , Two algorithms for barrier synchronization, International Journal of Parallel Programming 17(1) (1988), 1–17. doi:10.1007/BF01379320.

47.

Hirschi ,

Baelde and

Delaune , A method for verifying privacy-type properties: The unbounded case, in: Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P’16), IEEE Computer Society, 2016, pp. 564–581.

48.

Hüttel , Deciding framed bisimilarity, Electronic Notes in Theoretical Computer Science 68(6) (2003), 1–20, Special issue Infinity’02: 4th International Workshop on Verification of Infinite-State Systems. doi:10.1016/S1571-0661(04)80530-9.

49.

Juels ,

Catalano and

Jakobsson , Coercion-resistant electronic elections, in: Towards Trustworthy Elections: New Directions in Electronic Voting, LNCS, Vol. 6000, Springer, 2010, pp. 37–63. doi:10.1007/978-3-642-12980-3_2.

50.

Klus ,

Smyth and

M.D.

Ryan , ProSwapper: Improved equivalence verifier for ProVerif, 2010.

51.

Kremer and

M.D.

Ryan , Analysis of an electronic voting protocol in the applied pi calculus, in: ESOP’05: 14th European Symposium on Programming, LNCS, Vol. 3444, Springer, 2005, pp. 186–200.

52.

Lee ,

Boyd ,

Dawson ,

Kim ,

Yang and

Yoo , Providing receipt-freeness in mixnet-based voting protocols, in: ICISC’03: 6th International Conference on Information Security and Cryptology, LNCS, Vol. 2971, Springer, 2004, pp. 245–258.

53.

B.D.

Lubachevsky , Synchronization barrier and related tools for shared memory parallel programming, International Journal of Parallel Programming 19(3) (1990), 225–250. doi:10.1007/BF01407956.

54.

Pfitzmann and

Köhntopp , Anonymity, unobservability, and pseudonymity – a proposal for terminology, in: International Workshop on Design Issues in Anonymity and Unobservability, LNCS, Vol. 2009, Springer, 2001, pp. 1–9.

55.

M.K.

Reiter and

A.D.

Rubin , Crowds: Anonymity for web transactions, ACM Transactions on Information and System Security 1(1) (1998), 66–92. doi:10.1145/290163.290168.

56.

M.D.

Ryan and

Smyth , Applied pi calculus, in: Formal Models and Techniques for Analyzing Security Protocols, IOS Press, 2011, Chap. 6.

57.

Santiago ,

Escobar ,

Meadows and

Meseguer , A formal definition of protocol indistinguishability and its verification using Maude-NPA, in: STM’14: Security and Trust Management, LNCS, Vol. 8743, Springer, 2014, pp. 162–177.

58.

Smyth , Automatic verification of privacy properties in the applied pi calculus, in: Formal Protocol Verification Applied: Abstracts Collection, Dagstuhl Seminar Proceedings, 2007.

59.

Smyth , Formal verification of cryptographic protocols with automated reasoning, PhD thesis, School of Computer Science, University of Birmingham, 2011.

60.

Tiu and

Dawson , Automating open bisimulation checking for the spi calculus, in: CSF’10: 23rd IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2010, pp. 307–321.