Bruno Blanchet
email: bruno.blanchet@inria.fr

Ben Smyth

Automated reasoning for equivalences in the applied pi calculus with barriers

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, diffequivalence 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 and Lee et al., and in the vehicular ad-hoc network by Freudiger et al.

I. 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 [START_REF] Pfitzmann | Anonymity, Unobservability, and Pseudonymity -A Proposal for Terminology[END_REF], [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], [START_REF] Dahl | Formal Analysis of Privacy for Vehicular Mix-Zones[END_REF], ideal functionality [START_REF] Abadi | A Calculus for Cryptographic Protocols: The Spi Calculus[END_REF], [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], [START_REF] Delaune | Simulation based security in the applied pi calculus[END_REF], and stronger notions of secrecy [START_REF] Abadi | Security Protocols and their Properties[END_REF], [START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF], [START_REF] Cortier | Relating two standard notions of secrecy[END_REF]. 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

V (A, v) | V (B, v ) ≈ V (A, v ) | V (B, v) (1)
which means that no adversary can distinguish when two voters swap their votes [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]. (We use the applied pi calculus syntax and terminology [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], which we introduce in Section II.)

A. Approaches to proving equivalences

Observational equivalence is the tool introduced for reasoning about security requirements of cryptographic protocols in the spi calculus [START_REF] Abadi | A Calculus for Cryptographic Protocols: The Spi Calculus[END_REF] and in the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. It was originally proved manually, using the notion of labelled bisimilarity [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], [START_REF] Abadi | A Bisimulation Method for Cryptographic Protocols[END_REF], [START_REF] Borgström | On bisimulations for the spi calculus[END_REF] 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 [START_REF] Borgström | Symbolic Bisimulation in the Spi Calculus[END_REF], [START_REF] Delaune | Symbolic Bisimulation for the Applied Pi Calculus[END_REF] 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 [START_REF] Hüttel | Deciding Framed Bisimilarity[END_REF], [START_REF] Durante | Automatic Testing Equivalence Verification of Spi Calculus Specifications[END_REF], 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 [START_REF] Cortier | A method for proving observational equivalence[END_REF]. These decision procedures are too complex for useful implementations. Practical algorithms have since been proposed and implemented: SPEC [START_REF] Tiu | Automating open bisimulation checking for the spi calculus[END_REF] for fixed primitives and without else branches, APTE [START_REF] Cheval | Trace equivalence decision: Negative tests and non-determinism[END_REF] for fixed primitives with else branches and non-determinism, and AKISS [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF], [START_REF] Ciobâca | Verification and Composition of Security Protocols with Applications to Electronic Voting[END_REF] for a wide variety of primitives and determinate processes.

For an unbounded number of sessions, proving equivalence is an undecidable problem [START_REF] Hüttel | Deciding Framed Bisimilarity[END_REF], [START_REF] Abadi | Deciding knowledge in security protocols under equational theories[END_REF], 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 [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]. 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 [START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF] and Tamarin [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF] also use that notion, and Baudet [START_REF] Baudet | Sécurité des protocoles cryptographiques : aspects logiques et calculatoires[END_REF] showed that diff-equivalence is decidable for a bounded number of sessions and used this technique for proving resistance against off-line guessing attacks [START_REF]Deciding security of protocols against off-line guessing attacks[END_REF]. Decision procedures also exist for restricted classes of protocols: for an unbounded number of sessions, trace equivalence has a decision procedure for symmetrickey, type-compliant, acyclic protocols [START_REF] Chrétien | Decidability of trace equivalence for protocols with nonces[END_REF], which is too complex for useful implementation, and for ping-pong protocols [START_REF]From security protocols to pushdown automata[END_REF], which is implemented in a tool.

B. Diff-equivalence and its limitations

The main approach to automate proofs of observational equivalence with an unbounded number of sessions is to use diff-equivalence. (In our motivating example [START_REF] Pfitzmann | Anonymity, Unobservability, and Pseudonymity -A Proposal for Terminology[END_REF], a bounded number of sessions is sufficient, but an unbounded number becomes useful in more complex examples, as in Section IV-B.) 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 [v , v]). The two processes represented by a biprocess P are recovered by fst(P ) and snd(P ). Hence, fst(P 1 ) = V (A, v) | V (B, v ) and snd(P 1 ) = V (A, v ) | V (B, v).

P 1 V (A, diff[v, v ]) | V (B, diff
Diff-equivalence implies observational equivalence. Hence, the equivalence (1) can be inferred from the diffequivalence of the biprocess P 1 . However, diff-equivalence is so strong that it does not hold for biprocesses modelling even trivial schemes, as the following example demonstrates. Example 1. Consider an election scheme that instructs voters to publish their vote on an anonymous channel. The voter's role can be formalised as V (A, v) = c v . Thus, ballot secrecy can be analysed using the biprocess

P c diff[v, v ] | c diff[v , v]
. It is trivial to see that fst(P ) = c v | c v is indistinguishable from snd(P ) = c v | c v , because any output by fst(P ) can be matched by an output from snd(P ), and viceversa. However, the biprocess P does not satisfy diffequivalence. Intuitively, this is because diff-equivalence requires that the subprocesses of the parallel composition, namely,

c diff[v, v ] and c diff[v , v] , each satisfy diff- equivalence, which is false, because c v is not equivalent to c v (nor is c v equivalent to c v ).
Overcoming the difficulty encountered in Example 1 is straightforward: using the general property that

P | Q ≈ Q | P , we can instead prove V (A, v) | V (B, v ) ≈ 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 P

c diff[v, v] | c diff[v , v
] trivially satisfies diff-equivalence, since fst( P ) = snd( P ). However, this technique cannot be applied to more complex examples, as we show below. Some security properties (e.g., privacy in elections [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus[END_REF], vehicular ad-hoc networks [START_REF] Dahl | Formal Analysis of Privacy for Vehicular Mix-Zones[END_REF], [START_REF] Dahl | Formal Analysis of Privacy for Anonymous Location Based Services[END_REF], and anonymity networks [START_REF] Pfitzmann | Anonymity, Unobservability, and Pseudonymity -A Proposal for Terminology[END_REF], [START_REF] Reiter | Crowds: Anonymity for web transactions[END_REF], [START_REF] Chothia | Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus[END_REF]) 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) = c A .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 [START_REF] Brooks | The Butterfly Barrier[END_REF], [START_REF] Hensgen | Two Algorithms for Barrier Synchronization[END_REF], [START_REF] Arenstorf | Comparing barrier algorithms[END_REF], [START_REF] Lubachevsky | Synchronization Barrier and Related Tools for Shared Memory Parallel Programming[END_REF].

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) = c A .1:: c v , where 1:: is a barrier synchronisation. Ballot secrecy can then be analysed using biprocess

P ex c A .1:: c diff[v, v ] | c B .1:: 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 A] .1:: 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 c diff[A, B] .1:: c v | c diff[B,
P ex c A .1:: c diff[v, v] | c B .1:: c diff[v , v
] satisfies diffequivalence, which trivially holds since fst(P ex ) = snd(P ex ).

As illustrated in Examples 1 & 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.

C. Contributions

First, we extend the process calculus by Blanchet, Abadi & Fournet [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] to capture barriers (Section II). Secondly, we formally define a compiler that encodes barriers and swapping using private channel communication (Section III). As a by-product, if we compile without swapping, we also obtain an encoding of barriers into the calculus without barriers, via private channel communication. Thirdly, we provide a detailed soundness proof for this compiler. (Details of the proof are in the long version of this paper [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF].) 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 IV).

D. Comparison with Delaune, Ryan & Smyth

The idea of swapping data at barriers was informally introduced by Delaune, Ryan & Smyth [START_REF] Delaune | Automatic verification of privacy properties in the applied pi-calculus[END_REF], [START_REF] Smyth | Automatic verification of privacy properties in the applied pi calculus[END_REF]. 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 [START_REF]Formal verification of cryptographic protocols with automated reasoning[END_REF]Chapter 5], and Klus, Smyth & Ryan implemented that compiler [START_REF] Klus | ProSwapper: Improved equivalence verifier for ProVerif[END_REF].)

II. PROCESS CALCULUS

We recall Blanchet, Abadi & Fournet's dialect [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] of the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], [START_REF] Ryan | Applied pi calculus[END_REF]. This dialect is particularly useful due to the automated support provided by ProVerif [START_REF] Blanchet | ProVerif 1.93: Automatic cryptographic protocol verifier, user manual and tutorial[END_REF]. The semantics of the applied pi calculus [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] and the dialect of [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF] were defined using structural equivalence. Those semantics have been simplified by semantics with configurations and without structural equivalence, first for trace properties [START_REF] Abadi | Computer-assisted verification of a protocol for certified email[END_REF], then for equivalences [START_REF] Baudet | Sécurité des protocoles cryptographiques : aspects logiques et calculatoires[END_REF], [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques: modèle formel et modèle calculatoire[END_REF], [START_REF] Arapinis | Stateful applied pi calculus[END_REF]. 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.

A. 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 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 , . . . , M l ) → M , where M 1 , . . . , M l , M are terms that contain only constructors and variables, the variables of M must be bound in M 1 , . . . , M l , and variables are subject to renaming. The evaluation of expression g(M 1 , . . . , M l ) succeeds if there exists a rewrite rule g(M 1 , . . . , M l ) → M in def(g) and a substitution σ such that M i = M i σ for all i ∈ {1, . . . , l}, and in this case g(M 1 , . . . , 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 , . . . , x l ) → f (x 1 , . . . , x l )}, where f is a constructor of arity l. In particular, we use n-ary constructors (M 1 , . . . , M n ) for tuples, and unary destructors π i,n for projections, with the rewrite rule π i,n ((x 1 , . . . , x n )) → x i for all i ∈ {1, . . . , n}. ProVerif supports both rewrite rules and equations [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]; we omit equations in this paper for simplicity. It is straightforward to extend our proofs to equations, and our implementation supports them.

The grammar for processes is presented in Fig. 1. The process 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) → 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 [START_REF] Blanchet | Automatic Proof of Strong Secrecy for Security Protocols[END_REF], [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF], [START_REF] Blanchet | Vérification automatique de protocoles cryptographiques: modèle formel et modèle calculatoire[END_REF]), except for barriers, which we explain below.

Our syntax allows processes to contain barriers t:: P , where t ∈ 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 [START_REF] Blanchet | Automated verification of selected equivalences for security protocols[END_REF]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 c k .1:: c m | 1:: 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 c k .1:: c m , so it may output n without any other output. Our notion of barrier is essential for 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} ∪ 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 ∈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:: c m else c n | 1:: 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 III-E1.

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 ∈P fn(P ) and fv(P) = P ∈P fv(P ). A term M is ground if fv(M ) = ∅, a substitution { M / x } is ground if M is ground, and a M ⇓ M (M is a term, so it does not contain destructors) h(D 1 , . . . , D l ) ⇓ N σ if there exist h(N 1 , . . . , N l ) → N ∈ def(h) and σ such that for all i ∈ {1, . . . , l} we have

D i ⇓ M i and M i = N i σ B, E, P ∪ {0} → B, E, P (RED NIL) B, E, P ∪ {P | Q} → B, E, P ∪ {P, Q} (RED PAR) B, E, P ∪ {!P } → B, E, P ∪ {P, !P } (RED REPL) B, E, P ∪ {ν n.P } → B, E ∪ {n }, P ∪ {P { n / n }} for some name n such that n ∈ E ∪ fn(P ∪ {ν n.P }) (RED RES) B, E, P ∪ {N M .P, N (x).Q} → B, E, P ∪ {P, Q{ M / x }} (RED I/O) B, E, P ∪ {let x = D in P else Q} → B, E, P ∪ {P { M / x }} if D ⇓ M (RED DESTR 1) B, E, P ∪ {let x = D in P else Q} → B, E, P ∪ {Q} if there is no M such that D ⇓ M (RED DESTR 2)
B, E, P ∪ {t:: P 1 , . . . , t:: 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 (RED RES). When E = {ã} and P = {P 1 , . . . , P n }, the configuration B, E, P intuitively stands for ν ã.(P 1 | • • • | 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 ), ∅, {P }. Fig. 2 defines reduction rules for each construct of the language. The rule (RED REPL) creates a new copy of the replicated process P . The rule (RED RES) reduces ν n by creating a fresh name n , adding it to E, and substituting it for n. The rule (RED I/O) performs communication: the term M sent by N M .P is received by N (x).Q, and substituted for x. The rules (RED DESTR 1) and (RED DESTR 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, (RED DESTR 1) substitutes the result M for x and runs P . When it fails, (RED DESTR 2) runs Q. Finally, the new rule (RED BAR) performs barrier synchronisation: it synchronises on the lowest barrier t in B. If t occurs n times in B, it requires n processes t:: P 1 , . . . , 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) ⊆ 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.

P n } → B\{t n },
= {1 2 }, ∅, {P | Q | R}, since the process P | Q | R contains two barriers 1. We have C = {1 2 }, ∅, {P | Q | R} - → {1 2 }, ∅, {P, Q | R} by (RED PAR) - → {1 2 }, ∅, {P, Q, R} by (RED PAR) - → {1 2 }, ∅, {1:: c(x), Q, 0} by (RED I/O) - → {1 2 }, ∅, {1:: c(x), Q} by (RED NIL) - → {1 2 }, {n }, {1:: c(x), 1:: c n } by (RED RES) - → ∅, {n }, {c(x), c n } by (RED BAR) - → ∅, {n }, {0, 0} by (RED I/O) - → ∅, {n }, {0} by (RED NIL) - → ∅, {n }, ∅
by (RED NIL)

B. 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. [START_REF] Arapinis | Stateful applied pi calculus[END_REF] 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 ν ñ.

( | Q) with fv(Q) = ∅ and barriers(Q) = ∅. When C = B, E, P and C[ ] = ν ñ.( | Q) is an adversarial context, we define C[C] = B, E ∪ {ñ}, P ∪ {Q}, after renaming the names in E, P so that E ∩ fn(Q) = ∅. A configuration C = B, E, P can output on a channel N , denoted, C ↓ N , if
there exists N M .P ∈ P with fn(N ) ∩ E = ∅, 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:

1) if C ↓ N , then C - → * ↓ N , for all N ; 2) if C → C 1 , then C → * C 1 and C 1 R C 1 , for some C 1 . 3) C[C] R C[C ] for all adversarial contexts C[ ].
Closed processes P and P are observationally equivalent,

denoted P ≈ P , if C init (P ) ≈ 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.

C. 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 ∈ P} and snd(P) = {snd(P ) | P ∈ 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. Observational equivalence can be formalised as a property of biprocesses: Definition 2. A closed biprocess P satisfies observational equivalence if fst(P ) ≈ 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 -→ C , then fst(C) -→ fst(C ) and snd(C) -→ 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) -→ fst(C ), but there is no such reduction C -→ C , and symmetrically for snd(C). For example, given the configuration C = ∅, ∅, {diff[a, c] n .0, a(x).0}, we have fst(C) -→ ∅, ∅, {0, 0}, but there is no reduction C -→

B, E, P ∪ {N M .P, N (x).Q} →

B, E, P ∪ {P, Q{ M / x }} if fst(N ) = fst(N ) and snd(N ) = snd(N ) (RED I/O) B, E, P ∪ {let x = D in P else Q} → B, E, P ∪ {P { diff[M, M ] / x }} if fst(D) ⇓ M and snd(D) ⇓ M (RED DESTR 1) B, E, P ∪ {let x = D in P else Q} → B, E, P ∪ {Q} if there is no M such that fst(D) ⇓ M
and no M such that snd(D) ⇓ M (RED DESTR 2)

Figure 3. Generalised semantics for biprocesses

B, E, P ∪ {N M .P, N (x).Q} ↑ if (fst(N ) = fst(N )) ⇔ (snd(N ) = snd(N )) (DIV I/O) B, E, P ∪ {let x = D in P else Q} ↑ if (∃M.fst(D) ⇓ M ) ⇔ (∃M .snd(D) ⇓ M ) (DIV DESTR)

III. 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:

1) Function annotate annotates barriers with the data to be swapped and channels for sending and receiving such data. 2) 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 back data to a different barrier. We introduce annotated barriers (Section III-A) and define these two steps (Sections III-B and III-C) below. By combining these two steps we obtain our compiler (Section III-D), which we have implemented in ProVerif 1.94 (http://proverif.inria.fr/). The proof of soundness shows that these two steps preserve the observational behaviour of the biprocesses, so that if a compiled biprocess satisfies observational equivalence, then so does the initial biprocess.

A. 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 II, 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. Moreover, the ordered substitution ς = ( M 1/ x 1 , . . . , Mn / xn ) collects swappable data M 1 , . . . , M n and associates these terms with variables x 1 , . . . , x n ; the process P uses these variables instead of the terms M 1 , . . . , M n . The ordered substitution ς is similar to a substitution, except that the elements M 1/ x 1 , . . . , Mn / xn 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 , . . . , x n } and range(ς) = {M 1 , . . . , M n }. 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:

fn(t[a, c, ς]:: P ) = {a, c} ∪ fn(range(ς)) ∪ fn(P ) fv(t[a, c, ς]:: P ) = fv(range(ς)) ∪ (fv(P ) \ dom(ς))
We define the ordered domain of ς, ordom(ς) = (x 1 , . . . , 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, x]:: P , which is similar to an annotated barrier except that the ordered substitution ς is replaced with a tuple of variables x = (x 1 , . . . , 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:

barriers(t[a, c, ς]:: P ) = {t[a, c, ordom(ς)]:: P } ∪

barriers(P )

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, x]:: P ) = t[a, c, x]:: fst(P ) and fst(B, E, P) = fst(B), E, fst(P), and similarly for snd.

The operational semantics for processes with both standard and annotated barriers extends the semantics for processes with only standard barriers, with the following rule:

B, E, P ∪ {t:: P 1 , . . . , t:: P m , t[a m+1 , c m+1 , ς m+1 ]:: P m+1 , . . . , t[a n , c n , ς n ]:: We introduce the function channels(B) = {a | t[a, c, x]:: P ∈ B} ∪ {c | t[a, c, x]:: P ∈ B} to recover the multiset of names used by the domain-barriers in B. 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(ς)) ∪ 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 }.

P n } → B ,
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 III-B); 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, the elements of channels(barriers(P )) are pairwise distinct, channels(barriers(P )) ∩ fn-nobc(P ) = ∅, and for all annotated barriers in P such that

P = C[t[a, c, ς]:: Q],
we have fv(Q) ⊆ 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) ⊆ B, channels(B) ⊆ E, all processes in P are valid, the elements of channels(B) are pairwise distinct, and channels(B) ∩ fn-nobc(P) = ∅.

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 )) ∩ fn-nobc(P ) = ∅; channels(B) ∩ fn-nobc(P) = ∅), 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) ⊆ 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) ⊆ 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(ς).

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 and all other proofs are detailed in the long version of this paper [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF].

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

B. 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 , . . . , Mn / xn ) is an ordered substitution such that terms M 1 , . . . , M n are the largest subterms of Q that do not contain names or variables previously bound in Q, variables x 1 , . . . , 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 , . . . , 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 , . . . , 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 , . . . , M n are the largest possible subterms allows the checks in the definition of our compiler (see definition of function swapper in Section III-C) to succeed more often, and hence increases opportunities for swapping.

Example 5. We have

split(c diff[v, v ] ) = (x y , ( c / x , diff[v, v ] / y )) split(c diff[v , v] ) = (x y , ( c / x , diff[v , v] / y ))
The process c diff[v, v ] is separated into its skeleton Q = x y and the ordered substitution ς = ( c / x , diff[v, v ] / y ), which defines the values of the variables x and y such that c diff[v, v ] = Q ς. The process c diff[v , v] is separated similarly. Using these results, annotate(P ex ) is defined as

c A .1[a, b, ( c / x , diff[v, v ] / y )]:: x y | c B .1[a , b , ( c / x , diff[v , v] / y )]:: x y
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.) For soundness of the transformation (Proposition 4), it is sufficient that:

Lemma 3. If (Q , ς) = split(Q), then Q = Q ς, fv(Q ) = dom(ς), and fn(Q ) = ∅.
Intuitively, when reducing the annotated barrier by (RED BAR'), 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 ) = ∅ 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 4. If P 0 is a closed standard biprocess and P 0 = annotate(P 0 ), then P 0 is valid, fst(P 0 ) ≈ fst(P 0 ), and snd(P 0 ) ≈ 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 ς] ≈ C[t[a, c, ς]:: P ] (2)
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 Qς, so the same replacement also transform fst(P 0 ) into fst(P 0 ) and snd(P 0 ) into snd(P 0 ). By (2), this replacement preserves the observational behaviour of the processes.

C. 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, c, ς] is eliminated by replacing it with an output on channel a of swappable data, followed by an input on channel c that receives swapped data. A swapping process is added in parallel, which receives the swappable data on channels a for all barriers t, before sending swapped data on channels c. Therefore, all inputs on channels a must be received before the outputs on channels c are sent and the processes that follow the barriers can proceed, thus the synchronisation between the barriers is guaranteed. Moreover, the swapping process may permute data, sending on channel c data that comes from channel a with a = a, thus implementing swapping. This swapping is allowed only when the processes that follow the barriers are identical (up to renaming of some channel names and variables), so that swapping preserves the observational behaviour of the processes. We detail this construction below.

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 , . . . , Mn / zn )]::

Q into a (M 1 , . . . , M n ) .c(z). let z 1 = π 1,n (z) in • • • 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 , . . . , 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 ∈ {1, . . . , 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.

let x = π 1,2 (z) in let y = π 2,2 (z) in x y P comp c B .a (c, diff[v , v]) .b (z ). let x = π 1,2 (z ) in let y = π 2,2 (z ) in x y
for some fresh variables z and z .

2) Swapping: Next, we define swapping strategies.

Definition 7. The function swapper is defined as follows:

swapper(∅) = {0} swapper(B) = a 1 (x 1 ) . • • • . a n (x n ). c 1 diff[x 1 , x f (1) ] . • • • . c n diff[x n , x f (n) ] .R B = {t[a 1 , c 1 , z1 ]:: Q 1 , . . . , t[a n , c n , zn ]:: Q n } ∪ B
where, for all t [a, c, z]:: Q ∈ B , we have t > t; f is a permutation of {1, . . . , n} such that, for all 1 ≤ l ≤ n, we have Q l /z l = ch Q f (l) /z f (l) ; R ∈ swapper(B ); and x 1 , . . . , x n are fresh variables if B = ∅ where = ch is defined as follows:

• Q = ch Q means that Q equals Q modulo renaming
of channels of annotated barriers and

• Q/z = ch Q /z means that z = (z 1 , . . . , z k )
and z = (z 1 , . . . , z k ) for some integer k, and Q{ y 1/ z 1 , . . . , y k / z k } = ch Q { y 1/ z 1 , . . . , y k / z k } for some fresh variables y 1 , . . . , y k .

The function swapper builds a set of processes from a multiset of domain-barriers B as follows. We identify integer t ∈ N and domain-barriers t[a 1 , c 1 , z1 ]:: Q 1 , . . . , t[a n , c n , zn ]:: 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 , zi ]:: Q i and t[a j , c j , zj ]::

Q j such that Q i /z i = ch Q j /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 zi and zj 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 , . . . , a n , and sending it back on channels c 1 , . . . , 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 ), . . . , (a n , c n ), since any ordering is correct.

Example 7. We have barriers(annotate(P ex )) = {1[a, b, (x, y)]:: x y , 1[a , b , (x , y )]:: x y }. Moreover, we trivially have x y /(x, y) = ch x y /(x, y) and x y /(x , y ) = ch x y /(x , y ), because Q/z = ch Q/z for all Q and z. We also have x y /(x, y) = ch x y /(x , y ), because

x y { x / x , y / y } = x y = x y { x / x , y / y } It follows that swapper(barriers(annotate(P ex ))) = {P same , P swap }, where

P same a(z).a (z ).b diff[z, z] .b diff[z , z ] P swap a(z).a (z ).b diff[z, z ] .b diff[z , z]
for some fresh variables z and z . (Note that diff[z, z] could be simplified into z.) This set considers the two possible swapping strategies: the strategy that does not swap any data and the strategy that swaps data between the two processes at the barrier.

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. In the process P 1 , no data is swapped, so it behaves exactly like Proof sketch: This proof is performed by defining a relation R that satisfies the conditions of Definition 1. The proof is fairly long and delicate, and relies on preliminary lemmas that show that barrier elimination commutes with renaming and substitution, and that it preserves reduction when barriers are not reduced.

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 ]),

D. Our compiler

We combine the annotation (Section III-B) and removal of barrier (Section III-C) steps to define our compiler as compiler(P ) = elim-and-swap(annotate(P ))

We have implemented the compiler in ProVerif, which is available from: http://proverif.inria.fr/.

By combining Propositions 4 and 5, we immediately obtain: Proposition 6. Let P be a closed standard biprocess. If P ∈ compiler(P ), then fst(P ) ≈ fst(P ) and snd(P ) ≈ snd(P ).

This proposition shows that compilation preserves the observational behaviour of processes. The following theorem is an immediate consequence of this proposition: Theorem 7. Let P be a closed biprocess. If a biprocess in compiler(P ) satisfies observational equivalence, then 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 ∈ compiler(P ex ) of Example 8 satisfies observational equivalence, thus P ex satisfies observational equivalence too.

Our compiler could be implemented in other tools that prove diff-equivalence (e.g., Maude-NPA [START_REF] Santiago | A formal definition of protocol indistinguishability and its verification using Maude-NPA[END_REF] and Tamarin [START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF]), by adapting the input language. It could also be applied to other methods of proving equivalence. However, it may be less useful in these cases, since it might not permit the proof of more equivalences in such cases. Proposition 8 shows that, if our approach proves equivalence with unbounded replication, then it also proves equivalence with bounded replication. Proposition 9. 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 9 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 10. 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. Hence, we can apply our compiler to prove observational equivalence for biprocesses with bounded replication, for any value of the bound. In the case of election schemes, this result allows us to prove privacy for an unbounded number of voters, for instance in the protocol by Lee et al. (Section IV-B).

2) Local synchronisation: Our results could be extended to systems in which several groups of participants synchronise locally inside each group, but do not synchronise with other groups. In this case, we would need several swapping processes similar to those generated by swapper, one for each group.

3) 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) [START_REF] Blanchet | Automatic Verification of Correspondences for Security Protocols[END_REF]. 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.

IV. 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 receiptfreeness, are also possible.

• Ballot secrecy: a voter's vote is not revealed to anyone.

• Receipt-freeness: a voter cannot prove how she voted. We demonstrate the suitability of our approach for analysing privacy requirements of election schemes by Fujioka, Okamoto & Ohta, commonly referred to as FOO, and Lee et al., along with some of its variants. Our ProVerif scripts are included in ProVerif's documentation package (http: //proverif.inria.fr/). The runtime of these scripts (including compilation of barriers and proof of diff-equivalence by ProVerif) ranges from 0.14 seconds for FOO to 90 seconds for the most complex variant of the Lee et al. protocol, on an Intel Xeon 3.6 GHz under Linux.

A. Case study: FOO 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:

open(x k , commit(x k , x plain )) → x plain
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:

checksign(pk(x sk ), sign(x sk , x msg )) → x msg getmsg(sign(x sk , x msg )) → x msg unblind(x k , sign(x sk , blind(x k , x msg ))) → sign(x sk , x msg ) unblind(x k , blind(x k , x plain )) → x plain
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.

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.

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

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

3) 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 )). 4) The voter verifies the registrar's signature and unblinds the message to recover M = sign(sk R , M ), that is, her commitment signed by the registrar. After a deadline, the protocol enters the commitment phase.

5) The voter posts her ballot M to the bulletin board. Similarly, the tallying phase begins after a deadline.

6) The tallier checks validity of all signatures on the bulletin board and prepends an identifier to each valid entry. 7) The voter checks the bulletin board for her entry, the pair , M , and appends the commitment factor k. 8) Finally, using k, the tallier opens all of the ballots and announces the election outcome. The distinction between phases is essential to uphold the protocol's security properties. In particular, voters must synchronise before the commitment phase to ensure ballot secrecy (observe that without synchronisation, traffic analysis may allow the voter's signature to be linked with the commitment to her vote -this is trivially possible when a voter completes the commitment phase before any other voter starts the preparation phase, for instance -which can then be linked to her vote) and before the tallying phase to avoid publishing partial results, that is, to ensure fairness (see Cortier & Smyth [48] for further discussion on fairness).

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

ν k.ν k . % Step 2 let M = commit(k, x vote ) in let M = blind(k , M ) in 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 M = unblind(k , y) in 1:: c M . % Step 5 2:: c(z).let z 2 = π 2,2 (z) in % Step 7 if z 2 = M then c (z, k)
The process P foo (sk 1 , v 1 ) | • • • | P foo (sk n , v n ) models an election with n voters casting votes v 1 , . . . , v n and encodes the separation of phases using barriers.

4) Analysis: ballot secrecy: Based upon [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], [START_REF] Kremer | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus[END_REF] and as outlined in Section I, 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 7. 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

(pk(sk A ), sign(sk A , blind(k a , commit(k a , v)))) in fst(Q foo ) and (pk(sk A ), sign(sk A , blind(k a , commit(k a , v ))))
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 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 )
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

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 )
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 7. 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 [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], [START_REF] Kremer | Analysis of an Electronic Voting Protocol in the Applied Pi Calculus[END_REF] present a manual proof of ballot secrecy, Chothia et al. [START_REF] Chothia | A Framework for Automatically Checking Anonymity with µCRL[END_REF] provide an automated analysis in the presence of a passive adversary, and Delaune, Ryan & Smyth [START_REF] Delaune | Automatic verification of privacy properties in the applied pi-calculus[END_REF], Klus, Smyth & Ryan [START_REF] Klus | ProSwapper: Improved equivalence verifier for ProVerif[END_REF], and Chadha, Ciobâcȃ & Kremer [START_REF] Chadha | Automated Verification of Equivalence Properties of Cryptographic Protocols[END_REF], [START_REF] Ciobâca | Verification and Composition of Security Protocols with Applications to Electronic Voting[END_REF] provide automated analysis in the presence of an active adversary. Nevertheless, our analysis is useful to demonstrate our approach.

FOO does not satisfy receipt-freeness, because each voter knows the coins used to construct their ballot and these coins can be used as a witness to demonstrate how they voted. In an effort to achieve receipt-freeness, the protocol by Lee et al. [START_REF] Lee | Providing Receipt-Freeness in Mixnet-Based Voting Protocols[END_REF] uses a hardware device to introduce coins into the ballot that the voter does not know.

B. Case study: Lee et al.

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.

1) The tallier generates a key pair and publishes the public key. 2) Each voter is assumed to have a signing key pair and an offline tamper-resistant hardware device. The registrar is assumed to know the public keys of voters and devices. The registrar publishes those public keys.

The voting phase proceeds as follows.

3) The voter encrypts her vote and inputs the resulting ciphertext into her tamper-resistant hardware device. 4) The hardware device re-encrypts the voter's ciphertext, signs the re-encryption, computes a Designated Verifier Proof that the re-encryption was performed correctly, and outputs these values to the voter. 5) If the signature and proof are valid, then the voter outputs the re-encryption and signature, along with her signature of these elements.

The hardware device re-encrypts the voter's encrypted choice to ensure that the voter's coins cannot be used as a witness demonstrating how the voter voted. Moreover, the device is offline, thus communication between the voter and the device is assumed to be untappable, hence, the only meaningful relation between the ciphertexts input and output by the hardware device is due to the Designated Verifier Proof, which can only be verified by the voter. Finally, the tallying phase proceeds as follows.

6) Valid ballots (that is, ciphertexts associated with valid signatures) are input to a mixnet and the mixnet's output is published. We model the mixnet as a collection of parallel processes that each input a ballot, verify the signatures, synchronise with the other processes, and finally output the ciphertext on an anonymous channel. 7) The tallier decrypts each ciphertext and announces the election outcome.

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

C[V (A, v) | V (B, v )] ≈ C[V (A, v ) | V (B, v)] (3)
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 10 to model an unbounded number of voters by a replicated process. As far as we know, this is the first proof of this result.

With an additional dishonest voter, the proof of ballot secrecy fails. This failure does not come from a limitation of our approach, but from a ballot copying attack, already mentioned in the original paper [51, Section 6] and formalised in [START_REF] Dreier | Vote-independence: A powerful privacy notion for voting protocols[END_REF]: 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 tamperresistant 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.

3) Analysis: receipt-freeness: Following [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], receiptfreeness can be formalised as follows: there exists a process V such that

V \chc ≈ V (A, v) (4)
C[V (A, v ) chc | V (B, v)] ≈ C[V | V (B, v )] (5)
where the context

C[ ] appears in (3), 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 ( 4), but outputs messages on channel chc that aim to make the adversary think that it voted v . The equivalence [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF] 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 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 (4) holds by construction of V , because after removing outputs on chc, V is exactly the same as V (A, v). We prove (5) 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) Variant by Dreier, Lafourcade & Lakhnech: Dreier, Lafourcade & Lakhnech [START_REF] Dreier | Vote-independence: A powerful privacy notion for voting protocols[END_REF] 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.

5) Variant by Delaune, Kremer, & Ryan: Protocol description: Delaune, Kremer, & Ryan [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF] introduced a variant of this protocol in which the hardware devices are replaced with a single administrator, and the voting phase becomes:

3) The voter encrypts her vote, signs the ciphertext, and sends the ciphertext and signature to the administrator on a private channel. 4) The administrator verifies the signature, re-encrypts the voter's ciphertext, signs the re-encryption, computes a Designated Verifier Proof of re-encryption, and outputs these values to the voter. 5) If the signature and proof are valid, then the voter outputs her ballot, consisting of the signed re-encryption (via an anonymous channel). The mixnet is replaced with the anonymous channel, and the tallying phase becomes:

6) The collector checks that the ballots are pairwise distinct, checks the administrator's signature on each of the ballots, and, if valid, decrypts the ballots and announces the election outcome. Analysis: ballot secrecy: We have shown that this variant preserves ballot secrecy, with two honest voters, using our approach. In this proof, all keys are public and the collector is not trusted, so it is included in the adversary. Since the keys are public, any number of dishonest voters can also be included in the adversary, so the proof with two honest voters suffices to imply ballot secrecy for any number of possibly dishonest voters. Hence, this variant avoids the ballot copying attack and satisfies a stronger ballot secrecy property than the original protocol. Thus, we automate the proof made manually in [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF]. 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] ≈ C[Q | P ], much like for Example 1. Furthermore, an extension of ProVerif [START_REF] Cheval | Proving more observational equivalences with ProVerif[END_REF] takes advantage of this property to merge processes into biprocesses in order to prove observational equivalence. The approach outlined in that paper also succeeds in proving ballot secrecy for this variant. It takes 13 minutes 22 seconds, while our implementation with swapping takes 34 seconds. It spends most of the time computing the merged biprocesses; this is the reason why it is slower.

Analysis: receipt-freeness: We prove receipt-freeness for two honest voters. The administrator and voter keys do need to be secret, and all authorities need to be explicitly modelled. The process V is built similarly to the one for the original protocol by Lee et al. Equivalence (4) again holds by construction of V . To prove [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF], much like in [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], we model the collector as parallel processes that each input one ballot, check the signature, decrypt, synchronise together, and output the decrypted vote: There are as many such processes as there are voters, two in our case. However, such a collector does not check that the ballots are pairwise distinct: each of the two parallel processes has access to a single ballot, so each process individually cannot check that the two ballots are distinct. We implemented this necessary check by manually modifying the code generated by our compiler, by adding a check that the ballots are distinct in the process that swaps data. An excerpt of the obtained code follows:

c 1 diff[v 1 , v 2 ] ; c 2 diff[v 2 , v 1 ] )
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 collector should swap two ballots among the ones it has received (the two coming to the voters that swap their voters), but it has no means to detect which ones.

C. Other examples

The idea of swapping for proving equivalences has been applied by Dahl, Delaune & Steel [START_REF] Dahl | Formal Analysis of Privacy for Vehicular Mix-Zones[END_REF] to prove privacy in a vehicular ad-hoc network [START_REF] Freudiger | Mix-zones for location privacy in vehicular networks[END_REF]. They manually encode swapping based upon the informal idea of [START_REF] Delaune | Automatic verification of privacy properties in the applied pi-calculus[END_REF]. We have repeated their analysis using our approach. Thus, we automate the encoding of swapping in [START_REF] Dahl | Formal Analysis of Privacy for Vehicular Mix-Zones[END_REF], and obtain stronger confidence in the results thanks to our soundness proof.

Backes, Hrit ¸cu & Maffei [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus[END_REF] also applied the idea of swapping, together with other encoding tricks, to prove a privacy notion stronger than receipt-freeness, namely coercion resistance, of the protocol by Juels, Catalano & Jakobsson [START_REF] Juels | Coercion-resistant electronic elections[END_REF]. We did not try to repeat their analysis using our approach.

V. CONCLUSION

We extend the applied pi calculus to include barrier synchronisation and define a compiler to the calculus without barriers. Our compiler enables swapping data between processes at barriers, which simplifies proofs of observational equivalence. We have proven the soundness of our compiler and have implemented it in ProVerif, thereby extending the class of equivalences that can be automatically verified. The applicability of the results is demonstrated by analysing ballot secrecy and receipt-freeness in election schemes, as well as privacy in a vehicular ad-hoc network. The idea of swapping data at barriers was introduced in [START_REF] Delaune | Automatic verification of privacy properties in the applied pi-calculus[END_REF], without proving its soundness, and similar ideas have been used by several researchers [START_REF] Dahl | Formal Analysis of Privacy for Vehicular Mix-Zones[END_REF], [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus[END_REF], so we believe that it is important to provide a strong theoretical foundation to this technique.

Example 4 .

 4 Let us consider the parallel composition of processes P c k .1:: c(x), Q ν n.1:: c n , and R c(x), which yields the initial configuration C

Figure 4 .

 4 Figure 4. Semantics for divergence

Example 6 .

 6 Using the results of Example 5, eliminating barriers from annotate(P ex ) results in bar-elim(annotate(P ex )) = P comp | P comp , where P comp c A .a (c, diff[v, v ]) .b(z).

  elim-and-swap(P ) = ν ã.(bar-elim(P ) | R) where B = barriers(P ), {ã} = channels(B), and R ∈ swapper(B) Intuitively, function elim-and-swap encodes barrier synchronisation and swapping using private channel communication, thereby preserving the observational behaviour of processes. Example 8. Using the results of Examples 6 & 7, applying elim-and-swap to the process annotate(P ex ) generates two processes P 1 ν a, a , b, b .(P comp | P comp | P same ) P 2 ν a, a , b, b .(P comp | P comp | P swap )

E. Extensions 1 )

 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 | • • • | P with n copies of the process P . We have the following results: Proposition 8. 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.

  c(b); let ev = checksign(pk A , b) in let v = dec(sk C , ev) in 2:: c v

  (c(b); let ev = checksign(pk A , b) in let v = dec(sk C , ev) in a 1 (b, v) ; c 1 (v ); c v ) | (c(b); let ev = checksign(pk A , b) in let v = dec(sk C , ev) in a 2 (b, v) ; c 2 (v ); c v ) | (a 1 ((b 1 , v 1 )); a 2 ((b 2 , v 2 )); ( * ) if b 1 = b 2 then 0 else

  1/ x 1 , . . . , Mn / xn }

	M, N ::=	terms
	a, b, c, . . . , k, . . . , m, n, . . . , s name
	x, y, z	variable
	f (M 1 , . . . , M l )	constructor application
	D ::=	expressions
	M	term
	h(D 1 , . . . , D l )	function evaluation
	P, Q, R ::=	processes
	0	null process
	P | Q	parallel composition
	!P	replication
	ν a.P	name restriction
	M (x).P	message input
	M N .P	message output
	let x = D in P else Q	expression evaluation
	t:: P	barrier
	Figure 1. Syntax for terms and processes

  E, P ∪ {P 1 , . . . , P m , P m+1 ς m+1 , . . . , P n ς n } (RED BAR') where 0 ≤ m ≤ n, 1 ≤ n, B = {t m , t[a m+1 , c m+1 , ordom(ς m+1 )]:: P m+1 , . . . , t[a n , c n , ordom(ς

n )]:: P n } ∪ B , and for all t such that t ≤ t, t does not appear in B , i.e., t / ∈ B and t [ ]:: / ∈ B . When all barriers are standard, this rule reduces to (RED BAR).

  and after evaluating the projections, P comp reduces into c diff[v, v ] , which is the output present in the process P ex . Similarly, P comp reduces into 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 c v . Similarly, P comp reduces into c v . Hence P 2 behaves like c A .1:: c v | c B .1:: 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 this preservation of observable behaviour. Proposition 5. Let P be a valid, annotated biprocess. If P ∈ elim-and-swap(P ), then fst(P ) ≈ fst(P ) and snd(P ) ≈ snd(P ).

Acknowledgements: We are particularly grateful to Tom Chothia, Véronique Cortier, Andy Gordon, Mark Ryan, and the anonymous CSF reviewers, for their careful reading of preliminary drafts which led to this paper; their comments provided useful guidance. Birmingham's Formal Verification and Security Group provided excellent discussion and we are particularly grateful to: Myrto Arapinis, Sergiu Bursuc, Dan Ghica, and Eike Ritter, as well as, Mark and Tom, whom we have already mentioned. Part of the work was conducted while the authors were at École Normale Supérieure, Paris, France and while Smyth was at Inria, Paris, France and the University of Birmingham, Birmingham, UK.