Stéphanie Delaune

Joseph Lallemand

One vote is enough for analysing privacy

Electronic voting promises the possibility of convenient and efficient systems for recording and tallying votes in an election. To be widely adopted, ensuring the security of the cryptographic protocols used in e-voting is of paramount importance. However, the security analysis of this type of protocols raises a number of challenges, and they are often out of reach of existing verification tools. In this paper, we study vote privacy, a central security property that should be satisfied by any e-voting system. More precisely, we propose the first formalisation of the recent BPRIV notion in the symbolic setting. To ease the formal security analysis of this notion, we propose a reduction result allowing one to bound the number of voters and ballots needed to mount an attack. Our result applies on a number of case studies including several versions of Helios, Belenios, JCJ/Civitas, and Prêt-à-Voter. For some of these protocols, thanks to our result, we are able to conduct the analysis relying on the automatic tool Proverif.

Introduction

Remote electronic voting systems aim at allowing the organisation of elections over the Internet, while providing the same guarantees as traditional paper voting. Although relying on e-voting for large-scale elections is controversial, it is already in use in many lower-stakes elections today (e.g. the Helios [START_REF] Adida | Helios: Web-based open-audit voting[END_REF] voting system has been used to elect the IACR board of directors since 2010), and is likely to be used even more in the future, for better or for worse. These elections may involve a large number of voters and may have an important impact on democracy when it comes to elect political leaders. It is therefore of paramount importance to ensure the security of these systems.

As for security protocols in general, formal methods provide powerful techniques to analyse e-voting systems, and prove their security. Identifying what makes a good, secure e-voting system is a complex problem that has not yet been completely solved, and is actively being researched. It is however rather universally acknowledged that a central security guarantee e-voting systems should provide is vote privacy. Intuitively, this property states that votes must remain secret, so that no one can learn who voted for which candidate.

One common way of formalising vote privacy, which we will call SWAP, is to require that an attacker is not able to distinguish between the situation where Alice is voting yes and Bob is voting no from the situation where the two voters swapped their vote. That formalisation was first proposed by Benaloh [START_REF] Benaloh | Distributing the power of a government to enhance the privacy of voters (extended abstract)[END_REF], originally in a computational model. It has since been adapted to the symbolic setting [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols[END_REF], and applied to many voting schemes, e.g. [START_REF] Backes | Automated verification of remote electronic voting protocols in the applied pi-calculus[END_REF][START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF][START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF][START_REF] Cortier | A formal analysis of the Norwegian e-voting protocol[END_REF][START_REF] Cortier | A formal analysis of the Neuchâtel e-voting protocol[END_REF][START_REF] Basin | Alethea: A provably secure random sample voting protocol[END_REF]. The SWAP notion was originally written considering the specific case of a referendum, where the result is the number of yes and no votes. It has then been generalised to cover other kinds of elections [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF], but remains limited w.r.t. the way of counting votesessentially, it only makes sense when the result of the election is the number of votes for each candidate, excluding more complex counting procedures such as Single Transferable Vote (STV).

More recently, a new definition, called BPRIV for "ballot privacy", has been proposed to overcome such limitations [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. Essentially, BPRIV lets the attacker interact with the system, and see either real ballots, or fake ones containing fake votes. Using oracles, he can choose the values of real and fake votes, and cast any ballot he can construct (in the name of corrupted voters). In the end, the tally of real ballots is published. To be BPRIV, the attacker should be unable to distinguish the two scenarios, i.e. no information is leaked on the ballots' content.

Privacy-type properties, and in particular vote privacy, are often expressed using a notion of behavioural equivalence [START_REF] Delaune | A survey of symbolic methods for establishing equivalencebased properties in cryptographic protocols[END_REF]. A notable exception is the definition of (α, β)-privacy [START_REF] Mödersheim | Alpha-beta privacy[END_REF] which nevertheless relies on some notion of static equivalence. Proving equivalences is cumbersome, and is difficult to do in details by hand, as witnessed by the manual analysis of the SWAP property done for e.g. the Helios protocol [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF] and the Norwegian one [START_REF] Cortier | A formal analysis of the Norwegian e-voting protocol[END_REF]. Regarding mechanisation, several mature tools are available for analysing trace properties such as secrecy or authentication in the symbolic setting: most notably, Proverif [START_REF] Blanchet | An Efficient Cryptographic Protocol Verifier Based on Prolog Rules[END_REF][START_REF] Blanchet | Modeling and verifying security protocols with the applied pi calculus and ProVerif[END_REF] and Tamarin [START_REF] Meier | The TAMARIN Prover for the Symbolic Analysis of Security Protocols[END_REF]. These tools support equivalence properties [START_REF] Blanchet | Automated Verification of Selected Equivalences for Security Protocols[END_REF][START_REF] Basin | Automated symbolic proofs of observational equivalence[END_REF], although they remain limited to a restricted form of equivalence, called diff-equivalence. Some e-voting schemes have been analysed with these automated tools in the symbolic model, e.g. the Neuchâtel [START_REF] Cortier | A formal analysis of the Neuchâtel e-voting protocol[END_REF] or BeleniosVS [START_REF] Cortier | BeleniosVS: Secrecy and verifiability against a corrupted voting device[END_REF] protocols. Proverif even has an extension called ProSwapper [START_REF] Blanchet | Automated reasoning for equivalences in the applied pi calculus with barriers[END_REF], that specifically handles swapped branches that typically occur in the SWAP definition. These tools have proved very helpful for the study of e-voting systems. However, they still suffer from limitations that restrict their applicability, as they e.g. cannot handle homomorphic encryption, or manipulate lists of arbitrary size to encode the bulletin board, and tend to quickly run into performance issues when the number of agents in parallel increases.

An interesting option to ease the security analysis is to rely on reduction results. This approach has been used to bound the number of agents involved in an attack for both reachability [START_REF] Comon-Lundh | Security properties: two agents are sufficient[END_REF], and equivalence properties [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF]. Reduction results bounding the number of sessions [START_REF] Fröschle | Leakiness is decidable for well-founded protocols?[END_REF][START_REF] D'osualdo | Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes[END_REF] have also been proposed in more restricted settings. All these results do not apply in the context of evoting protocols. Here, we would like to bound the number of voters (agents) participating in the election. However, since only one vote is counted for each voter, we can not replace a session played by A by one played by B, as was done e.g. in [START_REF] Cortier | Bounding the number of agents, for equivalence too[END_REF]. The only existing result in that context is the result proposed in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF], where the authors give bounds on the number of voters and ballotsrespectively 3 and 10 -needed for an attack on the SWAP notion This allows them to carry out several case studies using Proverif. No such results, however, exist for the newer and more general BPRIV definition.

Contributions. Our contributions are threefold. First, we propose a definition of BPRIV adapted for the symbolic model. BPRIV has been first introduced in the computational setting where some subtleties regarding the communication model have been overlooked. Second, we identify some conditions under which BPRIV can be analysed considering only one honest voter and k dishonest ones. Actually, in most usual cases, we have k = 1, and the number of ballots being tallied is reduced to 1. These reduction results are generic, in particular we do not assume anything regarding the equational theory,and our result applies for different counting functions. Revoting is also allowed. Finally, we apply our result on several e-voting protocols from the literature relying on the tool Proverif. Our bounds for BPRIV, better than those obtained in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF] when considering SWAP, allow us to analyse many protocols in a reasonable time (whereas several hours were needed in some cases in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF]). We also identify an issue in the security analysis performed in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF] where a protocol has been declared secure while it is not.

Modelling security protocols

In this section, we introduce background notions on protocol modelling. We model security protocols in the symbolic model with a process algebra inspired from the applied pi-calculus [2]. Our model is mostly standard, except that in order to model the stateful nature of e-voting protocols, we consider memory cells, that can store a persistent state across processes. We need to avoid concurrent accesses to memory cells while updating them: to that end, we use a specific instruction that atomically appends a message to the content of a memory cell.

Messages

We assume an infinite set N of names used to model keys, nonces, etc. We consider two infinite and disjoint sets of variables X and W. Variables in X are used to refer e.g. to input messages, and variables in W, called handles, are used as pointers to messages learned by the attacker. Lastly, we consider two disjoint sets of constant symbols, denoted Σ 0 and Σ err . Constants in Σ 0 represent public values, e.g. identities, nonces or keys drawn by the attacker. This set is assumed to be infinite. Constants in Σ err will typically refer to error messages. We fix a signature Σ consisting of a finite set of function symbols together with their arity. We denote Σ + = Σ Σ 0 Σ err . We note T (F, D) the set of terms built from elements in D by applying function symbols in the signature F. The set of names (resp. variables) occurring in a term t is denoted names(t) (resp. var(t)). A term t is ground if var(t) = ∅. We refer to elements of T (Σ + , N ) as messages.

Example 1. We consider the signature Σ err = {err vote , err invalid } to model error messages. The signature Σ list = {nil, hd, tl, ::} allows us to model lists of arbitrary size. We often write [t 1 , . . . , t n ] for t 1 :: • • • :: t n :: nil. The operators hd and tl are used to retrieve the head and the tail of a list. Lastly, we consider Σ ex = {aenc, adec, pk, zkp, check zkp , true, 3 , proj 3 1 , proj 3 2 , proj 3 3 , yes, no} to model asymmetric encryption, zero-knowledge proofs, and pairing operators. As a running example, we will consider a model of the Helios protocol (in its original version, as seen in [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]) and Σ Helios = Σ ex ∪ Σ list .

Let id H ∈ Σ 0 , r, sk ∈ N , and pk = pk(sk). Intuitively, id H represents the identity of a honest voter, and yes her vote (these data are known to the attacker), whereas r and sk are private names, modelling respectively the randomness used in the encryption and the private key of the authority. Let e yes = aenc(yes, pk, r), and b id H yes = id H , e yes , zkp(e yes , yes, r, pk) 3 . The first term encrypts the vote, and the second one is the ballot sent by the voter in the voting phase of Helios.

An element of T (Σ + , W) is called a recipe and models a computation performed by the attacker using his knowledge. A substitution σ is a mapping from variables to messages, and tσ is the application of σ to term t, which consists in replacing each variable x in t with σ(x). A frame φ is a substitution that maps variables from W to messages, and is used to store an attacker's knowledge.

In order to give a meaning to function symbols, we equip terms with an equational theory. We assume a set E of equations over T (Σ, X ), and define = E as the smallest congruence containing E that is closed under substitutions.

Example 2. Continuing Example 1, we consider the equational theory E ex given below and E list := {hd(x :: y) = x, tl(x :: y) = y}.

E ex =
adec(aenc(x, pk(y), z), y) = x proj 3 i ( x 1 , x 2 , x 3 3 ) = x i with i ∈ {1, 2, 3} check zkp (zkp(aenc(x, y, z), x, z, y), aenc(x, y, z), y) = true

We have adec(e yes , sk) = Eex v, and check zkp (proj 3 3 (b id H yes ), v, r, pk) = Eex true.

In the following, we consider an arbitrary signature Σ + = Σ Σ 0 ∪ Σ err together with its equational theory E (equations built over Σ only), and we assume it contains at least the formalisation of lists given in Example 1 and Example 2, i.e. Σ list ⊆ Σ and E list ⊆ E.

Processes

We model protocols using a process calculus. We consider an infinite set of channel names Ch = Ch pub Ch pri , partitioned into infinite sets of public and private channel names. We also assume an infinite set M of names to represent memory cells (used to store states). The syntax of processes is: This syntax is rather standard, except for the memory cell operations. Intuitively, read m as x stores the content of m in the variable x, whereas append(c, u, m) represents the agent with channel c appending u to memory m. In addition, we use a special construct ! new d. out(c, d). P , to generate as many times as needed a new public channel d and link it to channel c, in a single step. This could be encoded using the other instructions, but having a separate construction lets us mark it in the execution traces, which is convenient for the proofs. The constructs in(c, x).P , let x = u in; P , and read m as x. P bind x in P . Given a process P , fv(P ) denotes its free variables, and we say that it is ground when fv(P ) = ∅. Moreover, we usually omit the final 0 in processes.

Example 3. Continuing our running example, we consider the process P :

P = in(c, b). if check zkp (proj 3 3 (b), proj 3 2 (b), pk(sk)), proj 3 1 (b) = true, id D then out(c, b). append(c, b, m bb ) else out(b, err invalid ).
where b ∈ X , sk ∈ N , and id D ∈ Σ 0 . This represents an agent that receives a ballot b as input, and then checks the validity of the zero knowledge proof contained in b, as well as the identity of the voter. Depending on the outcome of this test, it either outputs the ballot and appends it in the cell m bb modelling the ballot box, or simply outputs an error message.

Definition 1.

A configuration is a tuple (i; P; φ; M ), composed of an integer i, a multiset P of ground processes, a frame φ, and a mapping M from a subset of memory names M to messages. We write P instead of (0; P; ∅; ∅).

The semantics of our calculus is defined as a transition relation a = ⇒ on configurations. Each transition step is labelled with an action a representing what the attacker can observe when performing it (it can be an input, an output, an append action, or a silent action ). This relation is defined in a standard manner. As a sample, depicted below are the rules for input, errors, and append.

(i; {|in(c, u). P | } ∪ P; φ; M ) in(c,R) ====⇒ (i; {|P σ| } ∪ P; φ; M ) if c ∈ Ch pub ,
and R is a recipe such that var(R) ⊆ domφ and Rφ = E uσ for some σ with dom(σ) = var(u)

(i; {|out(c, c err ). P | } ∪ P; φ; M ) out(c,cerr) = ===== ⇒ (i; {|P | } ∪ P; φ; M ) if c ∈ Ch pub , c err ∈ Σ err (i; {|append(c, u, m)| }. P ∪ P; φ; M ) append(c) = ===== ⇒ (i; {|P | } ∪ P; φ; M {m → u :: M (m)}) if m ∈ dom(M )
For instance, considering an input on a public channel, the attacker can inject any message he is able to build using his current knowledge. The outputs performed on a public channel are made available to the attacker either directly through the label (when it corresponds to an error message), or indirectly through the frame (this rule is not shown). Lastly, we present the rule corresponding to our new append action append(c, u, m) which simply consists in appending a term u to the memory cell m. The full formal semantics is given in Appendix A. yes }, and K yes 0 = (2; {P }; φ yes ; {m bb → nil}). We have that:

K yes 0 in(c,w1).out(c,errinvalid) = ============= ⇒ (2; ∅; {w 0 → pk(sk), w 1 → b idH yes }; {m bb → nil}) K yes 0 in(c,R0).out(c,w2).append(c) =================⇒ (2; ∅; {w 0 → pk(sk), w 1 → b idH yes , w 2 → b idD yes }; {m bb → b})
with R 0 = id D , proj 3 2 (w 1 ), proj 3 3 (w 1 ) 3 , and b id D yes = R 0 φ id H yes = Eex id D , e yes , zkp 3 . The term zkp here denotes the zero-knowledge proof from b id H yes . It does not contain the identity of the voter who computes it, and can therefore be reused by a dishonest voter to cast the ballot in her own name.

Equivalences

Our definition of the BPRIV property relies on two usual notions of equivalence in the symbolic model: static equivalence, for the indistinguishability of sequences of messages, and trace equivalence, for the indistinguishability of processes. Definition 3. Two frames φ and φ are statically equivalent, denoted by φ ∼ φ , if dom(φ) = dom(φ ) and for any recipes

R 1 , R 2 ∈ T (Σ + , dom(φ)), we have that R 1 φ = E R 2 φ ⇔ R 1 φ = E R 2 φ .
Definition 4. Two ground processes P , Q are in trace inclusion, denoted by P t Q, if for all (tr, φ) ∈ traces(P ), there exists φ such that (tr, φ ) ∈ traces(Q) and φ ∼ φ . We say that P and Q are trace equivalent, denoted by P ≈ t Q, if P t Q and Q t P . Example 5. We can consider a configuration K no 0 similar to K yes 0 but with no instead of yes in the initial frame. We can establish that K no 0 ≈ t K yes 0 . This is a non trivial equivalence. Now, we replace P by P + in both configurations, adding a simple process modelling the tally (for one vote), e.g. P + = P | phase 3. read m bb as bb. let res = adec(proj 3 2 (bb), sk) in out(c r , res). We have that the resulting equivalence does not hold. This is simply due to the fact that tr = in(c, R 0 ).out(c, w 2 ).append(c).phase 3.out(c r , w 3 ) can be executed starting from both configurations, and the resulting frames contains w 3 → no on the left, and w 3 → yes on the right. This breach of equivalence is not, strictly speaking, an attack, as the processes do not formalise the BPRIV property. However it follows the same idea as the ballot copy attack against Helios from [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]: a dishonest voter copies a honest voter's ballot, introducing an observable difference in the result. This attack can be prevented by patching Helios, either by weeding out duplicate ballots from the ballot box, or by adding the voter's id to the ZKP, which then becomes invalid for any other voter.

Modelling the general BPRIV notion

In this section, we present our formal model of e-voting protocols, and our BPRIV privacy notion. While BPRIV itself is not novel, our symbolic formalisation is.

Modelling e-voting protocols

When modelling voting systems, we often need to encode some computations (e.g. performed by the ballot box) that cannot be represented by recipes (e.g. iterating through an arbitrary-sized list). We encode these computations as processes, that do not share any names, channels, or memory cells with the rest of the process, except for a channel to return the result of the computation. Definition 5. A computation is a process C d ( #" p ) without free names, channels, or variables (not counting those in d, #" p ), without memory cell operations, and without phases. It is parametrised by a channel d, and terms #" p , meant to be the channel where the result is output, and the terms given as input parameters.

This process must be such that for all inputs #" p , there exists a ground term t 0 such that for all channel name d, we have

traces(C d ( #" p )) = {( , ∅)} ∪ {(out(d, w), {w → t 0 }) | w ∈ W}.
We then call t 0 the result of the computation. As it does not depend on the channel, we will often omit it and let C( #" p ) denote the result.

To use such a process to compute a term inside a process P , we will typically run it in parallel with an input waiting to retrieve the result on d, followed by the continuation process. We will write as a shortcut let x = C( #" p ) in P for new d. (C d ( #" p ) | in(d, x). P ), where d is a fresh private channel name (i.e. that does not appear anywhere else in the ambiant process).

We assume a set Votes ⊆ T (Σ, Σ 0 ) of public ground terms representing the possible values of the votes. A voting system is modelled by a collection of processes that model the behaviour of voters, and a process modelling the tallying authority. The election process is composed of several phases.

Phases 0 and 1: Setup. The election material is generated and published.

Phase 2: Casting. The voters send their ballots to the ballot box. In our model, a memory m bb will play the role of the ballot box, recording all ballots received by the voting server. The voters' processes will first publish their ballot on a dedicated public channel, and then append it to the memory cell m bb . This models the fact that voters are authenticated when they submit their ballot, and the ballot cannot be modified on its way to the ballot box. However, the attacker is able to block a ballot before it reaches the ballot box.

Each voter has a private credential cr ∈ N , with an associated public credential computed by a recipe Pub(cr, u), that may use a random value u. Some protocols, such as Civitas, use this value to randomise the public credential, while others, such as Belenios, do not use it -in such cases we can omit it. To model the construction of ballots, we assume a recipe Vote with 5 variables: the term Vote(pk, id, cr, v, r) represents a ballot generated for voter id with credential cr, public election key pk, randomness r, and containing a vote v.

When modelling vote privacy, the attacker chooses the vote v he wants the voter to use to construct the ballot. Hence, we will need to check that v is indeed a possible value for a vote, i.e. v ∈ Votes. If the set of candidates is finite, this can be tested exhaustively. In other cases, such as write-in votes, it can be done e.g. if legal votes have a specific format (start with a tag, etc.), or trivially if any value is legal. In a voting scheme, once a ballot is received by the voting server, another check is performed to ensure the ballot is valid, i.e. correctly constructed. Typically, it can consist in verifying signatures or zero-knowledge proofs included in the ballot. To keep our model generic, we simply assume a recipe Valid with four variables: Valid(id, pcr, b, pk) represents the validity test performed for the agent id, whose public credential is pcr, who submits a ballot b. The term it computes is meant to be equal to true if, and only if, ballot b cast by id is valid w.r.t. her public credential pcr and the election public key pk. We incorporate this validity check directly in the process modelling the voter, before publishing and adding the ballot to m bb . In reality, it is performed by the ballot box, but this modelling choice is both simpler (no need for an extra process) and closer to the cryptographic game (where the voting oracle performs the test).

The formal definition of the voter's process is given in Section 3.2 as it incorporates elements specific to the modelling of the property.

Example 6. Continuing Example 2, for Helios, we use the following recipes:

Vote Helios (pk, id, v, r) = id, aenc(v, pk, r), zkp(aenc(v, pk, r), v, r, pk) [START_REF] Adida | Helios: Web-based open-audit voting[END_REF] Valid Helios (id, b, pk) = check zkp (proj 3 3 (b), proj 3 2 (b), pk).

Phase 3: Tallying. In the final phase, the Tally(sk) process is in charge of reading the contents of the ballot box, and using the key sk to compute and publish the result on a dedicated channel c r . To leave it as generic as possible, we simply assume a computation C Tally (bb, sk), that takes as parameters a list bb of ballots, and sk, and computes the result as specified by the protocol. We then assume the following form for Tally:

Tally(sk) = read m bb as bb. let res = C Tally (bb, sk) in out(c r , res).
Example 7. We continue Example 6 and we consider for simplicity the case of a referendum with two possible votes yes and no. We assume function symbols zero/0 and incr/1, without any associated equations, that we use to count in unary. Slightly abusing notations with the use of pattern-matching in input, the tallying computation can be written as follows:

C Tally (bb, sk) = new c. out(c, zero, zero, bb 3 ) | in(c, x, y, nil 3 ). out(c r , x, y ) | ! in(c, x, y, id, b, p 3 :: l) 3 ). let v = adec(b, sk) in if v = yes then out(c, incr(x)
, y, l 3 ) else out(c, x, incr(y), l 3 ).

A symbolic definition of BPRIV

We model vote privacy by adapting the BPRIV notion, originally formulated as a cryptographic game [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF], to our symbolic setting. The idea remains the same as for the original notion: an attacker should not learn any information on the votes contained in the ballots, other than the final result of the election. This is modelled by letting the attacker suggest two possible values for the vote of each honest voter: a "real" one and a "fake" one. The attacker then sees the honest voters' ballots, containing either the real or fake votes, and then in the end the real result of the election, computed on the real votes. We model the behaviour of honest voter id, who uses channel c, private and public credentials cr, pcr, and election public key pk in these two scenarios by the two following processes.

HVoter L (c, id, cr, pcr, pk) = in(c, z). let (v 0 , v 1 ) = (proj 2 1 (z), proj 2 2 (z)) in if v 0 , v 1 ∈ Votes then new r 0 . new r 1 . let b 0 = Vote(pk, id, cr, v 0 , r 0 ) in let b 1 = Vote(pk, id, cr, v 1 , r 1 ) in if Valid(id, pcr, b 0 , pk) = true then out(c, b 0 ). append(c, b 0 , m bb ) else out(c, err invalid ) else out(c, err vote ) HVoter R (c, id, cr, pcr, pk) = in(c, z). let (v 0 , v 1 ) = (proj 2 1 (z), proj 2 2 (z)) in if v 0 , v 1 ∈ Votes then new r 0 . new r 1 . let b 0 = Vote(pk, id, cr, v 0 , r 0 ) in let b 1 = Vote(pk, id, cr, v 1 , r 1 ) in if Valid(id, pcr, b 1 , pk) = true then out(c, b 1 ). append(c, b 0 , m bb ) else out(c, err invalid ) else out(c, err vote )
In both cases, the process receives the two possible vote instructions (v 0 , v 1 ) from the attacker, and constructs two corresponding ballots b 0 , b 1 . It then tests for validity, and publishes, either the real b 0 (on the left), or the fake b 1 (on the right). However, since the result is always computed on the real votes, the ballot secretly added to the ballot box m bb is always b 0 . If any of the tests fail, we return error messages err invalid , err vote ∈ Σ err .

The attacker has complete control over the ballots submitted by dishonest voters. Hence, we model them by a process that receives an arbitrary ballot from the attacker, and adds it to the ballot box m bb after checking its validity:

DVoter(c, id, cr, pcr, pk) = in(c, b). if Valid(id, pcr, b, pk) = true then out(c, b). append(c, b, m bb ) else out(c, err invalid ).
To a reader used to symbolic modelling of protocols, it may seem strange that dishonest voters are modelled by a process, rather than being left completely under the control of the attacker. It may similarly be surprising that the voters' processes include the validity checks and write directly to the ballot box, while these operations are not actually performed by the voter but by an independent entity (typically the server storing the ballot box). While not essential for our results, we decided to adopt this style of modelling to follow more closely the original formulation as a cryptographic game. In that formalism, the protocol and the scenario considered are modelled as oracles. Our symbolic processes are written in the same spirit: they should be seen as models of what happens when a voter votes, rather than directly models of the voter's behaviour.

We then consider n voters: for each i ∈ 1, n , we let #" v i = (c i , id i , cr i , pcr i ), where c i ∈ Ch pub is a dedicated public channel, id i ∈ Σ 0 is the voter's identity, cr i ∈ N her private credential, and pcr i = Pub(cr i , u i ) her public credential randomised with u i ∈ N . We will say that for i = j, #" v i and #" v j are distinct voters, to signify that they have different identities, credentials, and channels, i.e.

c i = c j ∧ id i = id j ∧ cr i = cr j ∧ u i = u j ∧ u i = cr j ∧ cr i = u j .
We then define the BPRIV property as follows. Definition 6. A voting scheme is BPRIV for p honest voters and n -p dishonest voters, written BPRIV(p, n -p), if

Election L p,n-p ( #" v 1 , . . . , # " v n ) ≈ t Election R p,n-p ( #" v 1 , . . . , # " v n )
where

Election X p,n-p ( #" v 1 , . . . , # " v n ) = new sk. m bb := nil. out(ch, pk(sk)). phase 1. out(c 1 , pcr 1 ). phase 2. HVoter X ( #" v 1 , pk(sk)) | . . . | phase 1. out(c p , pcr p ). phase 2. HVoter X ( #" v p , pk(sk)) | phase 1. out(c p+1 , cr p+1 , pcr p+1 ). phase 2. DVoter( #" v p+1 , pk(sk)) | . . . | phase 1. out(c n , cr n , pcr n ). phase 2. DVoter( # " v n , pk(sk)) | phase 3. Tally(sk) with ch ∈ Ch pub , X ∈ {L, R}.
While we designed our symbolic definition to follow as closely as possible the original computational formulation of the property, there are two notable differences.

First, in the original notion, the oracle modelling honest voters was executed atomically: once the adversary submits his vote instructions, the generated ballot is immediately placed in the ballot box. That is not the case here. This difference is an important one, and is fully intentional: we wanted to model a scenario where the attacker can intercept and block ballots on their way to the ballot box. This gives him more power, and thus makes for a stronger privacy property. A consequence of that choice however, is that our definition is not suited to studying protocols that rely on weeding out duplicate ballots from the ballot box (e.g. some fixed versions of Helios). Indeed, the weeding operation only makes sense when assuming that all generated ballots have reached the ballot box.

Second, many voting schemes include mechanisms allowing everyone to check that the tallying authority computed the result correctly. Typically, the talliers publish, alongside the result itself, zero-knowledge proofs showing that they e.g. correctly decrypted the ballots in the ballot box. In BPRIV however, having them output this proof would immediately break the property. The proof only holds for the actual ballots being tallied, so the attacker could just check it against the ballots he saw, which would succeed on the left but fail on the right. The original formalisation handles this by using a simulator for the proof on the right. This sort of operation does not really have a counterpart in the symbolic model, and we decided (for now) to simply abstract this proof away and not model it.

Auxiliary properties

In [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF], the authors propose two companion properties to BPRIV, called strong correctness and strong consistency. Together with BPRIV, they imply a strong simulation-based notion of vote privacy. Although we do not prove such a simulation -these are not really used in the symbolic model -we still define symbolic counterparts to the original computational side-conditions. They are useful when establishing our reduction result, and we will from now on assume they hold.

Strong correctness.

Honest voters should always be able to cast their vote, i.e. their ballots are always valid. Formally, for any id, cr, r, u, sk ∈ Σ 0 ∪N , v ∈ Votes, we must have: Valid(id, Pub(cr, u), Vote(pk(sk), id, cr, v, r), pk(sk)) = E true.

Strong consistency. The tally itself should only compute the result of the election, and nothing else -it cannot accept hidden commands from the attacker coded as special ballots, etc. Formally we assume two functions extract and count:

extract(b, sk) is meant to extract the vote, and the voter's id and credential from b, using key sk, or return ⊥ if b is not readable (ill-formed, etc.). -count is the counting function, meant to compute the result from the list of votes. It is assumed to always return a public term in T (Σ, Σ 0 ).

We assume that: if Valid(id, Pub(cr, u), b, pk(sk)) = E true then extract(b, sk) = (id, cr, v) for some v ∈ Votes. In other words, extraction always succeeds on valid ballots. Moreover, extract must behave as expected on honestly generated ballots,

i.e. v = v 0 when b = Vote(pk(sk), cr, v 0 , r). We let extract([b 1 , . . . , b n ], sk) be the list of non-⊥ values in [extract(b 1 , sk), . . . , extract(b n , sk)].
Lastly, we assume that these functions characterise the behaviour of the C Tally computation, i.e. for all list bb of messages, for all sk ∈ N , we have:

C Tally (bb, sk) = count(lst(extract(bb, sk)))
where lst is a function that only keeps the vote in each tuple returned by extract. Later on, when considering the case of revote, lst will be replaced with a function applying a revoting policy to determine which vote to keep for each voter.

Example 8. The Valid recipe and C tally computation from Examples 6 and 7 satisfy these assumptions, where extract simply decrypts the ciphertext in the ballot, and count returns the pair of the numbers of votes for yes and no.

Reduction

We first establish our reduction in the case where voters vote only once. Some systems allow voters to vote again by submitting a new ballot that will e.g. replace their previous one, in the interest of coercion-resistance. We extend our result to that setting in Section 5. Our BPRIV definition stated in Section 3 is parametrized by the number n of voters among which p are assumed to be honest. We prove our reduction result in two main steps. We first establish that it is enough to consider the case where p = 1, i.e. one honest voter is enough, and then we establish the conditions under which the number of dishonest voters can be bounded as well.

Reduction to one honest voter

In order to remain faithful to the original computational BPRIV notion, and to define a strong privacy property, we decided to write our symbolic BPRIV property in a general way, i.e. considering an arbitrary number of honest voters. Each voter receives two vote instructions (v 0 , v 1 ) from the attacker, and shows him the ballot for one or the other. Reducing the number of honest voters by replacing them by dishonest ones is non trivial. This comes from the fact the behaviour of an honest voter is not exactly the same on both sides of the equivalence, as it is the case for a dishonest voter. Nevertheless, we establish the following result: one honest voter is enough.

Proposition 1. Consider a voting scheme V, and p, n such that 1 ≤ p ≤ n. If V does not satisfy BPRIV(p, n -p), then it does not satisfy BPRIV(1, n -1).

Proof (Sketch). The general idea of this proof is to show we can isolate one specific honest voter whose ballot is the one causing BPRIV(p, n -p) to break. We then leave that voter as the only honest one, and use dishonest voters to simulate the p -1 others, and obtain an attack against BPRIV(1, n -1).

The difficulties are (i) how to find this particular voter, and (ii) how to simulate the honest voters with dishonest ones. The simulation would be easy for a honest voter id voting for the same candidate v on both sides: simply use the dishonest voter to submit a ballot Vote(pk, id, cr, v, r) for some random r, and the correct credential cr. However, in the Election processes, id uses different values v 0 , v 1 on the left and on the right, so that we cannot easily construct a single dishonest ballot simulating id's on both sides at the same time.

To solve both issues, the main idea is to go gradually from the Election L process, where all HVoters are HVoter L and use the real vote (their v 0 ), to the Election R process, where they are HVoter R and use the fake one (their v 1 ). We consider intermediate processes P 0 , . . . , P p : in P i , the first i HVoters are HVoter R , and the others are HVoter L . Since BPRIV(p, n -p) does not hold, P 0 = Election L and P p = Election R are not equivalent. Hence, there must exist some i 0 such that P i0+1 and P i0 are not equivalent. These two processes differ only by the i 0 + 1 th HVoter, who is HVoter L in P i0 , and HVoter R in P i0+1 . This voter will be our particular voter, who will remain honest, solving issue (i). All other HVoters behave the same in P i0 and P i0+1 : they vote with their right vote for the first i 0 , and their left for the last p -i 0 -1. For them, issue (ii) is thus solved, and we can simulate them with dishonest voters. This way, we recover an attack with only one honest voter, and (n -p) + (p -1) = n -1 dishonest voters.

Note that, in the case of the earlier reduction result from [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF] for the SWAP definition, a simple version of vote privacy is used from the start. They consider only two honest voters who swap their votes, and not the general definition (as stated e.g. in [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF][START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]) involving an arbitrary permutation between an arbitrary number of honest voters. Due to this, in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF], this first step was trivial. The argument in our case is more involved, as we start from the general notion.

Bounding the number of dishonest voters

This second reduction result allows one to bound the number of dishonest voters when considering BPRIV. More precisely, we consider a unique honest voter, and we show that k dishonest voters are sufficient to mount an attack against vote privacy (if such an attack exists). Here, we reduce the number of voters from n to k + 1 (k dishonest voters plus one honest voter), and the resulting bound depends on the counting function. Roughly, as formally stated below, we have to ensure that when there is a difference in the result when considering n votes, then a difference still exists when considering at most k votes.

Definition 7. A counting function count is k-bounded if for all n, for all lists

l tally = [v 1 , . . . , v n ] and l tally = [v 1 , . . . , v n ] of size n > k of elements in Votes, such that count(l tally ) = E count(l tally ), there exist k ≤ k, and i 1 < . . . < i k , such that count([v i1 , . . . , v i k ]) = E count([v i1 , . . . , v i k ]).
This assumption needed to establish our reduction results captures the most common counting functions such as multiset, sum, majority (see Appendix D).

Lemma 1. The functions count # , count Σ , and count Maj are 1-bounded.

This can be easily established by noticing that, when considering count # (resp. count Σ or count Maj ), as soon as two lists [v 1 , . . . , v n ] and [v 1 , . . . , v n ] of votes give different results, it means that there exists at least an indice i 0 such that v i0 = v i0 . Hence, keeping this vote is enough to keep a difference. We can also consider more involved counting functions, such as Single Transferable Vote (STV), used e.g. in Australian legislative elections, for which we have established that it is 5-bounded when considering 3 candidates. Under this k-boundedness assumption, we are then able to bound the number of dishonest voters. Proposition 2. Let V be a voting scheme whose associated counting function is k-bounded for k ≥ 1. If V does not satisfy BPRIV(1, n) for some n ≥ 1, then V does not satisfy BPRIV(1, k ) for some k ≤ k. Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box. Proof (Sketch). If BPRIV(1, n -1) does not hold, the difference appears either (i) when the honest voter outputs her ballot, or (ii) when outputting the result. Indeed, the behaviour of a dishonest voter who simply outputs the message he received does not help to mount an attack. Moreover, the only test that a dishonest voter performs is a public test from which the attacker will not infer anything. In case (i), no dishonest voters are even needed, and the claim holds.

In case (ii), we know that that the public terms representing the final result are different on both sides. We apply our k-boundedness hypothesis, and we know that a difference is still there when considering k voters (or even less). Removing the corresponding actions performed by dishonest voters, the trace still corresponds to an execution assuming that the validity tests do not depend on the the other ballots on the bulletin board. Hence, we have a witness of non-equivalence with at most k ballots, and thus at most k -1 dishonest voters.

Main result

Combining Propositions 1 and 2, we get our main reduction theorem establishing that it suffices to consider one honest voter, and at most k dishonest ones. Theorem 1. Let V be a voting scheme whose associated counting function is k-bounded for some k ≥ 1, and p, n be two integers such that 1 ≤ p ≤ n. If V does not satisfy BPRIV(p, n -p), then V does not satisfies BPRIV(1, k ) for some k ≤ k. Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box.

Example 9. The ballot copy attack on Helios (with the 1-bounded multiset count) from [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF], mentioned in Example 5, can be performed against BPRIV(p, n -p): a honest voter is told to vote yes or no, her ballot is copied by a dishonest voter but remains valid, and the result is then {|yes, yes| } on the left (as the "yes" ballot was seen and copied), and {|yes, no| } on the right (as the "no" ballot was seen).

In accordance with Theorem 1, one honest voter, one dishonest, and one accepted ballot are actually sufficient: the attacker can simply block the honest ballot, so that only the copy is counted leading to {|yes| } on the left and {|no| } on the right, which suffices for the attack.

Dealing with revoting

We now consider the case where re-voting is allowed. We first adapt the BPRIV definition to this setting. The processes HVoter, DVoter, and Tally are left unchanged. Only the main Election processes, and the consistency assumption change. The tallying now takes into account a revote policy, indicating how to proceed when a voter casts multiple votes. A revote policy is a function: policy : (Σ 0 × N priv × Votes) list → Votes list. This policy function replaces lst in the strong consistency assumption (Section 3.3). We consider here the two most common revote policies. The last and first policies, that select resp. the last or the first vote from each voter.

We reuse the notations from Section 3.2, and we introduce in addition # " w i = (d i , id i , cr i , pcr i ) for each i ∈ {1, . . . , n} where d i are different private channel names. The privacy property BPRIVR(p, n -p) is written as follows:

ElectionRevote L p,n-p ( #" v 1 , . . . , # " v n ) ≈ t ElectionRevote R p,n-p ( #" v 1 , . . . , # " v n ) where ElectionRevote X p,n-p ( #" v 1 , . . . , # " v n ) =
with ch ∈ Ch pub , X ∈ {L, R}.
Note that a replication operator has been added in front of the voter processes to model the fact that revote is now possible. Theorem 2. Let V be a voting scheme whose associated counting function is k-bounded for some k ≥ 1, and p, n be two integers such that 1 ≤ p ≤ n. If V does not satisfy BPRIVR(p, n -p), then V does not satisfy BPRIVR(1, k ) for some k ≤ k. Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box (each from a different voter).

The proof of this Theorem follows the same lines as the one when revote is not allowed -see Appendix F. We may note that replication operators are still there, and thus establishing such an equivalence property (even when p = 1, and k = 1) is not trivial. Traces of unbounded length still must be considered. However, as we are able to establish that, in a minimal attack trace, at most k ballots reached the ballot box (each by a different voter), we can easily remove the replication operator in front of a dishonest voter. This reasoning does not apply for the honest voter, as the output she performed may be useful to mount an attack (contrary to the output of a dishonest voter who outputs a term known by the attacker). This has been overlooked in the reduction result presented in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF]. The security analysis of Helios with revote has been done without considering this replication operator, leading to erroneous security analysis.

Applications and case studies

To illustrate the generality of our result, and to showcase how useful it can be in practice, we apply it to several well-known voting protocols from the literature. For our case study, we chose the following protocols: two variants of Helios [START_REF] Adida | Helios: Web-based open-audit voting[END_REF], corresponding to its original version, subject to the attack discussed earlier, and a fixed version that includes identities in the ZKP; Belenios [START_REF] Cortier | Belenios: A simple private and verifiable electronic voting system[END_REF], and the related BeleniosRF [START_REF] Chaidos | BeleniosRF: A non-interactive receipt-free electronic voting scheme[END_REF] and BeleniosVS [START_REF] Cortier | BeleniosVS: Secrecy and verifiability against a corrupted voting device[END_REF]; Civitas [START_REF] Juels | Coercion-resistant electronic elections[END_REF]; and Prêt-à-Voter [START_REF] Chaum | A practical voter-verifiable election scheme[END_REF][START_REF] Ryan | ,2 = c ij ,2 , then the eliminated candidate at the second round, and thus the winner, would[END_REF].

We modelled these protocols as processes satisfying our assumptions, and analysed them using Proverif. We only prove BPRIV itself with Proverif. Strong correctness only involves terms, and can easily be proved by hand. Strong consistency requires to show that the tallying process rightly computes the tally, which Proverif is not well-suited to do, as it requires 1) modelling the tally in the general case, i.e. with no bounds on the lengths of lists, and 2) comparing it to the abstract definition of the counting function, which Proverif cannot really manipulate. The property clearly holds though, and could be proved by hand.

All model files for our case study are available at [START_REF] Delaune | One vote is enough for analysing privacy[END_REF]. The results are presented in Table 1. As expected, we find the attack on Helios from [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF].

We conduct the analysis for different counting functions, using our result to bound the number of agents and ballots. We considered majority, multiset, sum, and STV (restricted to 3 candidates). In fact, in the case of 1-bounded functions, since only one ballot needs to be accepted by the ballot box, the tallying is trivial, and ends up being the same for different functions (majority, multiset, etc.). Thus, a single Proverif file is enough to model several counting functions as once. We considered both the cases without and with revote, for protocols that support revoting (except Civitas, which in that case uses rather complex mechanisms that do not fit our setting). As mentioned earlier, when revote is allowed, our result does not get rid of the replication operator. Bounding the number of voters is still useful in that case, as it simplifies our models. More importantly, bounding the number of ballots means we can encode the ballot box as a fixed-length list, which is very helpful as Proverif does not support arbitrary length lists.

In some cases, we made slight adjustments to the protocols, so that they fit our framework. Detailed explanations on these modelling choices can be found in the files. Notably, many protocols use homomorphic encryption: talliers add all encrypted votes before decryption. While our result still applies in principle to such primitives, Proverif cannot handle the associated equations. Hence, we instead verify versions of the protocols that use a mixnet, i.e. mix ballots in a random order before decryption.

Overall, as can be seen in the table, our result allows for efficient verification of all protocols we considered. Thanks to the small bounds we establish, we get even better performance than previous work [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF] in scenarios where that result appliesi.e. the first column, for multiset counting. In that case, some analyses took several hours/days in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF], due to the higher bounds. Our result is more general and can handle e.g. STV counting. On most tested protocols, performance remains acceptable in that case. However Proverif did not terminate on three files after 24h: this is likely due to the combination of the complex equational theories used by these protocols, and the theory for STV, which is itself large.

Conclusion

We have proposed a symbolic version of the BPRIV vote privacy notion, and established reduction results that help us efficiently verify it on several voting protocols, with different counting functions, using automated tools.

As mentioned earlier, a limitation of our definition is the modelling of the correct tallying proofs, which we abstracted away. In the computational definition, they are handled using simulators. It remains to be seen whether such techniques can be adapted to the symbolic setting, and how.

Our attacker already controls the channel between voters and the ballot box. A natural further step is to consider an even stronger attacker, that can modify the content of the ballot box (altering already cast ballots, etc.). BPRIV has recently been extended to such a scenario in the computational model [START_REF] Cortier | Fifty shades of ballot privacy: Privacy against a malicious board[END_REF], at the cost of a much more complex definition -adapting that work to the symbolic setting constitutes exciting future work. Now, when reaching phase 3, the process Tally is a computation process that may involved private channels, and thus leads to non-determinism. However, by definition of a computation process, we know that this process will result on a unique output on the public channel c r , and the value of this output only depends on the parameters given to the computation process, here sk and the content of m bb . The content of m bb is entirely determined by tr and the content of the frame. When considering the same trace tr, we obtain frame which are equal up to α-renaming, and we will obtain the same public term for the tally.

A trace tr is Σ err -free if tr does not contain any occurrence of c err for any c err ∈ Σ err . Proposition 3. Let V be a voting scheme such that

Election L p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ) ≈ t Election R p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ).
Let tr be a witness of this non-equivalence of minimal length. We have that tr is such that:

-Election L p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ) tr = ⇒ (i L ; P L ; φ L ; M L ) for some (i L ; P L ; φ L ; M L ); -Election R p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ) tr = ⇒ (i R ; P R ; φ R ; M R ) for some (i R ; P R ; φ R ; M R ); -i L = i R , φ L ∼ φ R , and tr is Σ err -free.
Moreover, for any i ∈ {1, . . . , p}, if in(c i , R) occurrs in tr in phase 2 (for some R), then there exists

(v 0 , v 1 ) ∈ Votes × Votes such that Rφ L = E Rφ R = E (v 0 , v 1 ).
Proof. Assume first that the minimal witness of this non-equivalence is actually a witness for the following non-inclusion:

Election L p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ) t Election R p,n-p ( #" v 1 , #" v 2 , . . . , # " v n ).
This witness is a trace tr such that Election L p,n-p ( #" v 1 , . . . , # " v n ) tr = ⇒ (i L ; P L ; φ L ; M L ), and for which 1. either there does not exist (i

R ; P R ; φ R ; M R ) such that Election R p,n-p ( #" v 1 , . . . , # " v n ) tr = ⇒ (i R ; P R ; φ R ; M R ); 2. or such a trace exists, i.e. Election R p,n-p ( #" v 1 , . . . , # " v n ) tr = ⇒ (i R ; P R ; φ R ; M R ) but φ L ∼ φ R (note that we necessarily have that i L = i R ).
Let us first show the first three points.

We first assume that such a witness of minimal length satsifies the requirements stated in item 1, i.e. there does not exist (i

R ; P R ; φ R ; M R ) such that Election R 1,n ( #" v 0 , #" v 1 , . . . , # " v n ) tr = ⇒ (i R ; P R ; φ R ; M R ).
Note that, it means that, at some point, the outcome of a test is not the same on both sides, and this leads to an output that can not be mimicked on the other side. When the test under consideration is public (i.e corresponds to a computation that can be performed by the attacker), we get a contradiction since the trace tr without its last output will already lead to a witness of non-inclusion. The only remaining case is the validity test performed by the honest voter but here we know that such a test can not failed. Indeed, we have assumed that:

Valid(id, Pub(cr, u), Vote(pk(sk), id, cr, v, r), pk(sk)) = E true Therefore, we know that such a minimal witness is due to a problem regarding static equivalence, i.e. we know that there exists (i L ;

P L ; φ L ; M L ) such that Election R 1,n ( #" v 0 , #" v 1 , . . . , # " v n ) tr = ⇒ (i R ; P R ; φ R ; M R ) but φ L ∼ φ R .
It remains to establish that tr can be considered to be Σ err -free. Assume that tr contains an action of the form out(c i , c err ) for some c i and some c err ∈ Σ err . Then the trace tr without this action still passes on both sides, and leads to the exact same frames. Indeed, in the processes considered, the errors are always placed at the end of a branch, and hence not executing them does not change anything else in the trace. Therefore such an action can not occur in a minimal witness.

Finally, for any honest voter i, if in(c i , R) occurs in tr in phase 2, it must be that the test "if v 0 , v 1 ∈ Votes" succeeds on the left and eventually the corresponding output is performed, or the test fails on the left and eventually an error message is outputted. In the first case, there exist (v 0 , v 1 ) ∈ Votes 2 such that Rφ L = E (v 0 , v 1 ) and thus by minimality of the witness Rφ R = E (v 0 , v 1 ). In the second case, we have that Rφ L = E (v 0 , v 1 ) for any (v 0 , v 1 ) ∈ Votes 2 , and again by minimality of the witness, we have that Rφ R = E (v 0 , v 1 ) for any (v 0 , v 1 ). Since tr is Σ err -free, we know that the corresponding error message is not outputted in the trace, but in this case, by minimality of tr, we know that this input is not useful to get a witness of non-equivalence. Lemma 3. Let t L and t R be two public terms, i.e. t L , t R ∈ T (Σ, Σ 0 ). Let φ L , φ R be two frames such that φ L ∼ φ R , and w tall ∈ W \ dom(φ L ). We have that

φ L ∪ {w tall → t L } ∼ φ R ∪ {w tall → t R } if, and only if, t L = E t R .
Proof. First, assume that t L = E t R . In such a case, let M = w tall , and N = t L ∈ T (Σ, Σ 0 ). We have that the test M = N holds in φ L ∪ {w tall → t L }, and not in φ R ∪ {w tall → t R }. Indeed, we have that:

M φ L = w tall φ L = t L = N φ L ; and M φ R = w tall φ R = t R = E t L = N φ R . Therefore, we have that φ L ∪ {w tall → t L } ∼ φ R ∪ {w tall → t R }.
Now, we assume that φ L ∼ φ R , and

t L = E t R . Consider w.l.o.g. a test M = N that holds in φ L ∪ {w tall → t L }. Let M = M {w tall → t L }, and N = N {w tall → t L }.
We have that M = N is a test that holds in φ L , and thus in φ R (thanks to our hypothesis φ L ∼ φ R ). Since, t L = E t R , we easily conclude that M = N holds in φ R ∪ {w tall → t R }. This allows us to conclude.

Pub(cr i , u i ), and p ∈ {1, . . . , n}. For any i ∈ {0, . . . , p}, we define:

P i = new sk. m bb := nil. out(ch, pk(sk)). phase 1.out(c 1 , pcr 1 ). phase 2. HVoter R ( #" v 1 , pk(sk)) | . . . | phase 1.out(c i , pcr i ). phase 2. HVoter R ( #" v i , pk(sk)) | phase 1.out(c i+1 , pcr i+1 ). phase 2. HVoter L ( # " v i+1 , pk(sk)) | . . . | phase 1.out(c p , pcr p ). phase 2. HVoter L ( #" v p , pk(sk)) | phase 1.out(c p+1 , cr p+1 , pcr p+1 ). phase 2. DVoter( # " v p+1 , pk(sk)) | . . . | phase 1.out(c n , cr n , pcr n ). phase 2. DVoter( # " v n , pk(sk)) | phase 3. Tally(sk)
We will show that under our assumptions we have P i ≈ t P i+1 for any i ∈ {0, . . . , p -1}. Since we have that

P 0 = ElectionL p,n-p ( #" v 1 , . . . , # " v n ) and P p = ElectionR p,n-p ( #" v 1 , . . . , # " v n )
, by transitivity of ≈ t , this property suffices to prove the theorem.

Fix some index i ∈ {0, . . . , p -1}. Observe that P i and P i+1 differ only in the behaviour of the (i + 1) th voter id i+1 , which is modelled by the process HVoterL( # " v i+1 , pk(sk)) in process P i , and by the process HVoterR( # " v i+1 , pk(sk)) in P i+1 . All other honest voters are identical in P i and P i+1 : they always follow the attacker's instructions in the same way, either always voting for the right vote (for voters id j , j ≤ i) or the left vote (for voters id j , j ≥ i + 2). Therefore, the main idea of the proof is that all these other voters can be simulated by the attacker, since their behaviour is known and the same on both sides. The only remaining honest voter will be id i+1 , to which we will apply the assumption that BPRIV holds for one honest voter.

To prepare the terrain for applying this assumption later on, we define two additional processes Q L , Q R , where this "simulation" is performed, i.e. where all voters except id i+1 are controlled by the attacker. Formally, the processes for these voters are replaced by instances of process DVoter. The processes Q L , Q R are defined as follows:

Q L = new sk. m bb := nil. out(ch, pk(sk)). phase 1.out(c 1 , cr 1 , pcr 1 ). phase 2. DVoter( #" v 1 , pk(sk)) | . . . | phase 1.out(c i , cr i , pcr i ). phase 2. DVoter( #" v i , pk(sk)) | phase 1.out(c i+1 , pcr i+1 ). phase 2. HVoter L ( # " v i+1 , pk(sk)) | phase 1.out(c i+2 , cr i+2 , pcr i+2 ). phase 2. DVoter( # " v i+2 , pk(sk)) | . . . | phase 1.out(c n , cr n , pcr n ). phase 2. DVoter( # " v n , pk(sk)) | phase 3. Tally(sk) and Q R = new sk. m bb := nil. out(ch, pk(sk)). phase 1.out(c 1 , cr 1 , pcr 1 ). phase 2. DVoter( #" v 1 , pk(sk)) | . . . | phase 1.out(c i , cr i , pcr i ). phase 2. DVoter( #" v i , pk(sk)) | phase 1.out(c i+1 , pcr i+1 ). phase 2. HVoter R ( # " v i+1 , pk(sk)) | phase 1.out(c i+2 , cr i+2 , pcr i+2 ). phase 2. DVoter( # " v i+2 , pk(sk)) | . . . | phase 1.out(c n , cr n , pcr n ). phase 2. DVoter( # " v n , pk(sk)) | phase 3. Tally(sk)
In fact, up to permutation of the parallel branches, these two processes are instances of the generic election process, with one honest voter (id i+1 ) and n -1 dishonest voters (id j , j = i + 1):

Q L = ElectionL 1,n-1 ( # " v i+1 , #" v 1 , . . . , #" v i , # " v i+2 , . . . , # " v n ) and Q R = ElectionR 1,n-1 ( # " v i+1 , #" v 1 , . . . , #" v i , # " v i+2 , . . . , # " v n )
Thanks to the assumption that BPRIV holds for one honest voter, we thus have

Q L ≈ t Q R . (1)
By contradiction, let us now assume

P i ≈ t P i+1 . ( 2
)
Using the same arguments as for Lemma 2, P i , P i+1 , Q L , Q R are actiondeterminate. Let tr be a witness of this non-equivalence of minimal length. By the exact same argument used to prove Proposition 3, tr is such that:

-P i tr = ⇒ (i; P L ; φ L ; M L ) for some i, P L , φ L , M L ; -P i+1 tr = ⇒ (i; P R ; φ R ; M R ) for some P R , φ R , M R ; -φ L ∼ φ R ;
tr is Σ err -free; -for any j ∈ 1, p , if in(c j , R) occurs in tr in phase 2, then there exist (v 0 , v 1 ) ∈ Votes 2 such that Rφ L = Rφ R = (v 0 , v 1 ). When such an input exists, let instr(j) denote this pair of votes, which is the instruction given by the attacker to voter j in tr.

In addition, by action-determinacy, φ L and φ R are unique up to α-renaming of fresh names -without loss of generality, let us assume that the same symbols are used for matching private fresh names in both frames, i.e. the random values used for constructing a honest ballot on either side are given the same name, and similarly for the election key.

Our next step is to construct a sequence of actions tr, that describes how to simulate the execution tr of P i (resp. P i+1 ) in an execution of Q L (resp. Q R ).

Intuitively, the attacker interacting with Q L or Q R performs the same actions as the original one interacting with P i or P i+1 , except that all honest voters but id i+1 are simulated using dishonest voters. Hence, whenever the attacker (for P i , P i+1 ) provides two votes (v 0 , v 1 ) to an honest voter id j (with 1 ≤ j ≤ p and j = i + 1), we instead let the attacker (for Q L , Q R ) construct the corresponding ballot Vote(pk, id j , cr j , v 0 , r 0 ) and provide it to the process for id j , who is now dishonest. Note that, since the result computed in the end by the tally always counts the "left" vote v 0 , we must construct the ballot containing that vote, so that the result obtained in the end is the right one.

A subtle detail is that when constructing this ballot, the attacker will not be able to use the same private name r 0 originally used by the honest voter in tr. He must instead use a public name. To keep notations relatively light, we introduce, for each private name r generated by the process for an honest voter other than id i+1 in P i or P i+1 an associated public name, that the attacker may use instead, which we will call r. This name must be fresh, i.e. not appear in any of the processes or recipes considered until now (including those used in the inputs in tr). We also let σ denote the function mapping each such public r to the corresponding private r.

Due to the form of the processes, we can assume w.l.o.g. that tr is a prefix of: out(ch, w 0 ).phase 1.out(c i1 , w i1 ). . . . .out(c ip , w ip ).phase 2.tr cast .phase 3.out(c res , w tall ) where tr cast contains only inputs and outputs on the channels {c i } 1≤i≤n , with at most one input on each c i , and, when this input is present, at most one output on c i , placed after the input. Without loss of generality, call R i the recipe provided in the input on c i in tr cast , and w i the frame variable recording the output on c i (if they exist).

We now define recipes that we will use to let the attacker compute ballots for honest voters simulated by dishonest ones. For any j ∈ 1, p with j = i + 1 such that an input in(c j , R j ) occurs in tr cast , we let B 0 j = Vote(w 0 , id j , proj 2 1 (w j ), v 0 , r0 ) and B 1 j = Vote(w 0 , id j , proj 2 1 (w j ), v 1 , r1 ) where (v 0 , v 1 ) = instr(j) and r0 , r1 are fresh public names associated by σ to the private names r 0 , r 1 used to construct the ballots for voter j in P i and P i+1 .

Let tr be the trace containing the same actions as tr, except that in tr cast (if tr reaches tr cast at all), -any input in(c j , R j ) for 1 ≤ j ≤ p, j = i + 1, i.e. the input of the attacker's instructions for honest voter j, is replaced with in(c j , B 0 j ).

any input in(c j , R j ) for j > p, i.e. the attacker's instruction for dishonest voter j, os replaced with in(c j , S j ), where

S j = R j w k → B 1 k 1≤k≤i w k → B 0 k i+1<k≤p .
By construction of t, and from the shape of the processes Q L , Q R , it is clear that t is executable in Q L and Q R . All inputs and outputs in phases 0, 1, and 3 can be performed as expected. There are only two points where t might a priori be non-executable in phase 2, that are related to the validity checks:

-If the validity check in a DVoter process for a voter id j with j > p failed, preventing an output on c j that was possible in tr: by construction, the ballot b on which the validity check fails in tr and the ballot b output by this voter in tr, on which the test succeeds, are obtained by the same recipe applied to two frames of honest ballots that differ only on the random values used (the r or the r). By the randomness independence property (Lemma 4), this is not possible. -If the validity check in a DVoter process for a voter id j with j ≤ p failed, preventing an output on c j that was possible in tr: by the consistency assumption (Section 3.3), validity tests always succeed on honestly generated ballots, and this is not possible.

Executing tr in Q L and Q R respectively produces frames φ L , φ R . By actiondeterminacy, they are unique up to α-renaming fresh names -without loss of generality, let us assume that the same symbols are used for matching private fresh names in both frames, i.e. the random values used for constructing a honest ballot on either side are given the same name, and similarly for the election key. In addition, we will also assume these symbols are the same as for the corresponding names in φ L , φ R .

Note that, by construction, the recipes B 0 j , B 1 j from earlier, when applied to φ L and φ R , compute ballots b 0 , b 1 such that b 0 σ and b 1 σ are the two ballots computed by honest voter j in tr in P i and P i+1 respectively. Similarly, the recipe S j used in tr to compute dishonest ballots produces, when applied to φ L and φ R , a ballot b such that bσ is the ballot provided by the attacker to dishonest voter j in tr in P i and P i+1 respectively. The last step of our proof will be to describe the relation between φ L , φ R , and φ L , φ R . As we will see, this will bring out a contradiction, as the first two are assumed statically equivalent and the other two are not.

We construct a frame of recipes R, giving for each variable w ∈ dom(φ

L ) = dom(φ R ) a recipe R(w) with variables in dom(φ L ) = dom(φ R ), such that φ L = (Rφ L )σ and φ R = (Rφ R )σ, i.e. ∀w ∈ dom(φ L ). φ L (w) = (R(w)φ L )σ ∧ φ R (w) = (R(w)φ R )σ (3)
R is constructed as follows:

Majority.

such that v i0 = v i0 . Hence, count([v i0 ]) = count([v i0 ]
), which concludes the proof for count # . A similar reasoning applies for count Σ , and count Maj .

D.2 Single Transferable Vote

Single Transferable Vote (STV) is a system where each voter casts a single ballot containing a total ordering of all candidates. A vote goes to the voter's first choice. If that choice is later eliminated, instead of being thrown away, the vote is transferred to her second choice, and so on. In each round, the least popular candidate is eliminated. His votes are transferred based on voters' subsequent choices. The process is repeated until one candidate remains, who is declared the winner. We assume a total order ≺ on candidates is picked beforehand, and is used to break ties. The STV counting function outputs a term representing the winning candidate; it is parametrised by the set of candidates and the order ≺.

v = v , however Count 3 STV ([v]) = Count 3 STV ([v ]) = a.
Thus, the previous reasoning to establish 1-boundedness does not apply here.

Lemma 5. Count 3

STV is 5-bounded.

Proof. We assume that a ≺ b ≺ c. Let = [v 1 , . . . , v n ] and = [v 1 , . . . , v n ] be two lists of Votes such that Count 3 STV ( ) = Count 3 STV ( ). For each 1 ≤ i ≤ n, we denote (c i,1 ; c i,2 ; c i,3 ) the vote v i and (c i,1 ; c i,2 ; c i,3 ) the vote v i .

Case 1: There exists 1 ≤ i 0 ≤ n such that v i0 = (c i0,1 ; c i0,2 ; c i0,3 ) and v i0 = (c i0,1 ; c i0,2 ; c i0,3 ) with c i0,1 = c i0,1 . In such a case, we keep this vote, and we have [START_REF] Delaune | One vote is enough for analysing privacy[END_REF] . Thus, at the first round, the eliminated candidate is the same on both sides. Call it c 0 . If c 0 does not occur as the first choice on a vote, i.e. c 0 = c i,1 for all i (and thus c 0 = c i,1 , as c i,1 = c i,1 ), then the eliminated candidate at the second round will be the same on both sides, and the winner as well, contradicting our hypothesis.

c i0,1 = Count 3 STV ([v i0 ]) = Count 3 STV ([v i0 ]) = c i0,1 . Case 2: Otherwise, for 1 ≤ i ≤ n, we have c i,1 = c i,
Hence, c 0 occurs as the first choice in some votes. Let i 0 , . . . , i k the indices of all such votes. We have c ij ,1 = c ij ,1 = c 0 for any j ∈ {0, . . . , k}. If the second Now, we consider the case where n > k. We are going to show that this minimal witness tr is also a witness of the follwing non-equivalence

Election L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t Election R 1,k ( #" v 0 , #" v 1 , . . . , #" v k ).
In the following, we will distinguish cases depending on the form of tr. Due to the form of the processes, we can assume w.l.o.g. that tr is a prefix of: out(ch, w 0 ).phase 1.out(c i1 , w i1 ). . . . .out(c ip , w ip ).phase 2.tr cast .phase 3.out(c res , w tall ) Case 1: tr only contains actions from phase 0 and phase 1. In such a case, we have that tr can not be a witness of non-equivalence. Indeed, the frames on both sides are necessarily in static equivalence.

Case 2: tr contains actions from phases 0, 1, and 2 (but no action from phase 3). We distinguish two cases:

-We first assume that there are some actions performed by a dishonest voter id j in phase 2, i.e. there is in(c j , R j ) ∈ tr and possibly out(c j , w j ) ∈ tr, and append(c j ) as well. In such a case, we consider tr = tr{w j → R j } where tr is tr in which the input, output, and append actions performed during phase 2 on channel c j have been removed. The resulting trace tr is smaller than tr.

To conclude, it remains to show that tr is a witness of non equivalence, thus contradicting the minimality of the witness tr.

It is easy to see that this trace tr still passes in Election L 1,n ( #" v 0 , #" v 1 , . . . , # " v n ). Note that the action append(c j ) has no impact since the tallying phase has not been executed. The frame φ L resulting from this new execution tr is such that φ L = φ L ∪ {w j → b 0 L } where b 0 L = R j φ L for some recipe R j such that vars(R j ) ⊆ dom(φ L ). Similarly to the reasoning performed on the left side, this trace tr also passes in Election R 1,n ( #" v 0 , #" v 1 , . . . , # " v n ) (since tr passes too). Moreover, we have that the frame φ R resulting from this execution tr is such that φ R = φ R ∪ {w j → b 0 R } where b 0 R = R j φ R ↓ considering the exact same recipe R j as the one mentioned above. We have that φ L ∼ φ R implies that φ L ∼ φ R , and thus since we know that φ L ∼ φ R , we deduce that φ L ∼ φ R . This allows us to conclude that tr is a witness of non-inclusion, and this leads to a contradiction as tr is smaller than tr.

-We now assume that there is no input/output/append action performed by a dishonest voter during the casting phase (phase 2). In such a case, we have that either tr cast = in(c 0 , R 0 ).out(c 0 , w 0 ).append(c 0 ) or tr cast = in(c 0 , R 0 ).out(c 0 , w 0 ) or tr cast = in(c 0 , R 0 ). Note that actually the first and the last case are impossible since the input and the append actions do not modify the frame, and thus are not necessary to obtain a witness of non-equivalence (of the shape mentioned above) leading a contradiction regarding minimality.

In case phase 1 contains an output on c i with i > 0, i.e. we have that out(c i , w i ) occurs in phase 1, and we have that w i φ L = cr i , Pub(cr i , u i ) , we consider tr = tr{w i → cr i , Pub(cr i , u i ) }, where tr is tr in which this output has been removed, and cr i and u i are fresh public constants. We have that tr passes in during the initialization phase, and thus we have that this witness tr is also a witness regarding Election L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t Election R 1,k ( #" v 0 , #" v 1 , . . . , #" v k ). Otherwise, we know that n voters with n > k have casted their vote. Thanks to our k-bounded hypothesis, we know that there exists k ≤ k, and 0 ≤ i 1 < . . . < i k ≤ n such that counting the votes of id i1 , . . . , id i k still leads to a difference in the result. In the trace tr, we know that there are actions append(c i1 ), . . . , append(c i k ) corresponding to the append actions of these voters id i1 , . . . , id i k . We consider tr obtained from tr by removing all these actions. It is easy to see that this trace tr still passes in Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v k ) and in Election R 1,n ( #" v 0 , #" v 1 , . . . , #" v k ). The resulting bulletin board BB L (resp. BB R ) contain less ballots than before, and these ballots have been choosen to satisfy: count(extract(BB L )) = count(extract(BB R ))

Therefore, the resulting frames φ L and φ R are almost the same as φ L and φ R except the result outputted during the tallying phase, but we know that they are different public terms. As our processes are action-deterministic thanks to Lemma 2, there is no other choice to obtain another frame, and thus tr is a witness of Election L -constructs the public credential associated to the private credential in φ L , φ R , for voters j ∈ 1, p \ {i + 1}; -constructs the right ballot, using the ballot recipe from earlier, for the sessions of all voters j ≤ i, and the left ballot for the sessions of voters j ∈ i + 2, p ; -reads everything else, i.e. voter i + 1's credentials and ballots (from all her sessions), all dishonest ballots and credentials, and the election results, directly from φ L or φ R .

As before, it is clear that this accurately reconstructs all and credentials for all sessions of all voters. The subtle point is that the result is also accurately reconstructed: that is the case, since we used the ballot recipes to submit the correct ballots to dishonest voters simulating voters j ∈ 1, p \ {i + 1}.

Step 2. The shape of the witness of non-equivalence is a bit different from the one used in Proposition 2 as we now have sess(c j , d) actions that will occur. Nevertheless the reasoning remains the same. We only focus on the case where tr contains actions from phase 3 (actually only one), and we distinguish 3 cases:

-If during phase 2, there is some actions (e.g. sess(c i , d), in(d, R), out(d, w)) on channel c i (with i > 0) but not the corresponding append(d) action, then we can consider tr = tr{w → R} where tr is equal to tr without these actions, and we can show that tr is a witness of non-equivalence obtaining a contradiction regarding the minimality of tr. -Now, in case phase 1 contains an action of the form out(c i , w i ) with i > 0, whereas there is no sess(c i , d) in phase 2, then we can consider the trace tr which is equal to tr without this output out(c i , w i ), and we also replace the occurrences of w i in tr by cr i , Pub(cr i , u i ) where cr i and u i are fresh public constants. As before, we conclude that tr is a smaller witness. -We now consider the case of a trace tr that is composed of a phase 1 (only voters who outputs a ballot participate to this phase 1), then a phase 2, and then the output of the result during phase 3. We have that φ L ∼ φ R where φ L and φ R are the two resulting frames, and actually relying on Lemma 3, we have that w tall φ L == E w tall φ R . Moreover, we know that:

w tall φ L = count(policy(extract(BB L ))) and w tall φ R = count(policy(extract(BB R )))

where BB L (resp. BB R ) is the bulletin board (i.e. the content of the memory cell m bb ) resulting from the trace tr on the left (resp. on the right).

If at most k distinct voters casted their vote (action append), then we know that only these dishonest voters outputted their credential during the initialization phase, and thus we have that this witness is also a witness regarding

ElectionRevote L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t ElectionRevote R 1,k ( #" v 0 , #" v 1 , . . . , #" v k ).
This relies on the fact that our processes are action-deterministic (Lemma 2), and thus there is no other possibility to get another frame. Moreover, this witness satisfies our requirements. Therfore, we are done. Otherwise, we know that n votes with n > k have been casted (possibly by the same voter), i.e. we have that:

BB L = [b L 1 , . . . , b L n ] and BB R = [b R 1 , . . . , b R n ]
. Moreover, we know that for each pair of ballots (b L j , b R j ), we have that there exists id, cr, v L , and v R such that: extract(b L j ) = (id, cr, v L ) and extract(b R j ) = (id, cr, v R ) In case a voter casted more than one ballot, then we know that only one has been taken into account due to the revote and thus there is i 0 such that b L i0 and b R i0 do not influence the result (since it has been removed by the revote policy). Therefore, we can remove the corresponding append(d) action, and we obtain a smaller trace tr leading to the exact same frames, and same result. Otherwise, each voter has voted only once but we have n > k. Therefore the policy will consider all the ballots to compute the result. Thanks to our k-bounded hypothesis, we know that there exists k ≤ k, and 0 ≤ i 1 < . . . < i k ≤ n such that We now consider tr which is tr without the actions append(d) corresponding to all the ballots that have been removed. Note that, if we want to remove the i th 0 ballot from the bulletin board, this corresponds to removing the i th 0

append actions from the trace tr. The resulting trace tr is smaller than tr, and leads to the exact same frames but its last element corresponding to the output of the result. We have pay attention to maintain a difference on both sides, and thus tr is still a witness of non-equivalence. Hence, this allows us to conclude the proof.

Definition 2 .

 2 The set of traces of a configuration K is defined as traces(K) = {(tr, φ) | ∃i, P, M such that K tr = ⇒ (i; P; φ; M )} where • = ⇒ is the reflexive transitive closure of • = ⇒, concatenating all (non-silent) actions into the sequence tr.

Example 4 .

 4 Continuing Example 3 with φ yes = {w 0 → pk(sk), w 1 → b id H

Let Count 3

 3 STV the STV function for candidates {a, b, c} with a ≺ b ≺ c. Votes are 3-tuples: (c 1 ; c 2 ; c 3 ) where {c 1 , c 2 , c 3 } = {a, b, c} and c i denotes the i th choice. Example 10. Let v = (a; b; c) and v = (a; c; b). We have

  count(extract([b L i1 , . . . , b L i k ])) = count(extract([b R i1 , . . . , b R i k ]))Note that, since each voter only votes once, this implies thatcount(policy(extract([b L i1 , . . . , b L i k ]))) = count(policy(extract([b R i1 , . . . , b R i k ]))).

  | phase 1. out(c p , pcr p ). phase 2. ! new d p . out(c p , d p ). HVoter X ( # " w p , pk(sk)) | phase 1. out(c p+1 , pcr p+1 ). phase 2. ! new d p+1 . out(c p+1 , d p+1 ).DVoter( # " w p+1 , pk(sk)) | . . . | phase 1. out(c n , pcr n ). phase 2. ! new d n . out(c n , d n ).

	DVoter( # " w n , pk(sk))
	| phase 3. Tally(sk)

new sk. m bb := nil. out(ch, pk(sk)).

phase

1. out(c 1 , pcr 1 ). phase 2. ! new d 1 . out(c 1 , d 1 ). HVoter X ( #" v 1 , pk(sk)) | . . .

Table 1 .

 1 Summary of our results. : Proverif proves the property. : Proverif finds an attack trace. : timeout (≥ 24h). Execution times are on an Intel i7-1068NG7 CPU.

		Counting	Multiset/Maj/Sum	Single Transferable Vote
		Protocols	(2 voters/1 ballot)	(6 voters/5 ballots)
	without revote	Helios (id in ZKP) Helios (ZKP without id) Belenios BeleniosRF BeleniosVS Civitas	≤ 1s ≤ 1s ≤ 1s ∼ 3s ∼ 3s ≤ 1s	∼ 24 min ∼ 27 min ∼ 27 min ∼ 39 min
		Prêt-à-Voter	≤ 1s
	revote	Helios (id in ZKP) Helios (ZKP without id) Belenios	≤ 1s ≤ 1s ≤ 1s	∼ 23 min ∼ 42 min ∼ 23 min

  The majority function between two choices yes and no simply outputs yes if #yes > n/2 where n is the number of votes, and no otherwise. For all n,count Maj ([v 1 , . . . , v n ]) = yes if #{i | v i = yes} > n/2; and count Maj ([v 1 , . . . , v n ]) = no otherwise.Here, yes and no are two public constants (yes = E no). The functions count # , count Σ , and count Maj are 1-bounded.Proof. Let [v 1 , . . . , v n ] and [v 1 , . . . , v n ] be two lists of votes with n > 1, such that count # ([v 1 , . . . , v n ]) = count # ([v 1 , . . . v n ]). Since count # is a function, we have {|v 1 , . . . , v n | } = {|v 1 , . . . , v n | }, and thus there exists i 0

	Lemma 1.

1,n ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t Election R 1,n ( #" v 0 , #" v 1 , . . . , #" v k ). Hence the result.

Acknowledgements This work has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation program (grant agreement n°714955-POPSTAR), as well as from the French National Research Agency (ANR), under project TECAP, and under the France 2030 programme with reference ANR-22-PECY-0006.

Appendix A Semantics of our calculus

Appendix B Characterisation of an attack trace

In this section, we establish a property characterising the form of all potential attack traces on our election processes. Definition 8. A configuration K is action-deterministic if for any tr, any configurations K 1 = (i 1 ; P 1 ; φ 1 ; M 1 ) and K 2 = (i 2 ; P 2 ; φ 2 ; M 2 ) such that K tr = ⇒ K 1 and K tr = ⇒ K 2 , we have that i 1 = i 2 and φ 1 and φ 2 are equal modulo α-renaming of names generated during the execution.

Given two action-deterministic ground processes P L and P R such that P L t P R , a witness of non-inclusion is a trace tr for which there exists φ L such that (tr, φ L ) ∈ traces(P L ), and either there does not exist φ R such that (tr, φ R ) ∈ traces(P R ); -or such a φ R exists and φ L ∼ φ R .

Lemma 2. The two ground election processes Election

. . , # " v n ) are action-deterministic for any n, and any p ≤ n.

Proof. For these two processes, until phase 3, each process in parallel has its own public dedicated channel. Thus, the action mentioned on the trace tr indicates which action will be triggered, there is no ambiguity, and it is therefore clear that the resulting frames are equal up to α-renaming.

In if c ∈ Ch pub , and R is an attacker term such that var(R) ⊆ domφ and Rφ = E uσ for some σ with dom(σ) = var(u)

Consider a frame φ 1 of m ballots, honestly generated by honest voters id i1 , . . . , id im (two ballots can potentially be generated by the same voter):

Also consider an arbitrary injective renaming σ : {r 1 , . . . , r m , u 1 , . . . , u m } → Σ 0 ∪ N \ {sk}, such that for any r in its domain, σ(r) does not appear in any

We can now recall and prove Proposition 1.

Proposition 1. Consider a voting scheme V, and p, n such that 1 ≤ p ≤ n. If V does not satisfy BPRIV(p, n -p), then it does not satisfy BPRIV(1, n -1).

Proof. We first define intermediate processes we will use to prove the equivalence. We fix n distinct voters #" v 1 , . . . , # " v n , with for all i #"

-For w 0 , storing the election key output in phase 0: this output is also performed in tr, and R(w 0 ) = w 0 is adequate.

-For all w j present in dom(φ L ), storing credentials output in phase 1:

• if j = i + 1, φ L and φ R as well as φ L , φ R contain the public credential pcr j in w j , and thus R(w j ) = w j works;

• if 1 ≤ j ≤ p and j = i + 1, φ L and φ R contain the public credential pcr j in w j , while φ L and φ R contain cr j , pcr j ; thus R(w j ) = proj 2 2 (w j ) works;

• if j > p, φ L and φ R as well as φ L , φ R contain the credentials cr j , pcr j in w j , and thus R(w j ) = w j works.

-For all w j present in dom(φ L ), storing all ballots output during phase 2:

• if j < i + 1, according to the processes, φ L and φ R contain in w j the ballot Vote(pk, id j , cr j , v 1 , r 1 ), where (v 0 , v 1 ) = instr(j), and r 1 is the nonce generated by the voter. Thus R(w j ) = B 1 j is adequate.

• if j = i + 1, according to the processes, φ L as well as φ L contain in w j the ballot Vote(pk, id j , cr j , v 0 , r 0 ), while φ R and φ R contain the ballot Vote(pk, id j , cr j , v 1 , r 1 ), where (v 0 , v 1 ) = instr(j), and r 0 , r 1 the random values used. Thus R(w j ) = w j is appropriate.

• if i + 1 < j ≤ p, according to the processes, φ L and φ R contain Vote(pk, id j , cr j , v 0 , r 0 ) in w j , where (v 0 , v 1 ) = instr(j) and r 0 is the nonce generated by the voter. Thus R(w j ) = B 0 j is adequate.

• if j > p, according to the processes, φ L , φ R , φ L , φ R each contain in w j the ballot received as an input from the attacker earlier by voter j's process. As explained earlier, the recipe used in tr to construct that input is such that this ballot verifies φ L (w j )σ = φ L (w j ) and φ R (w j )σ = φ R (w j ). Hence, picking R(w j ) = w j satisfies 3.

-Finally, the only remaining variable is w tall , storing the result output in phase 3. Our argument is that the tally actually outputs the same result in the execution of tr in P i and tr in Q L , and similarly for P i+1 and Q R . Indeed, consider the inputs received by Tally on the private channel containing the internal state. In P i and tr, these are the "left" ballots computed by all honest voters, and the dishonest ballots. In Q L and tr, they are • the left ballot of voter i + 1

• the ballots given as input to dishonest voters j ∈ 1, p computed using B 0 j , which, as explained earlier, are the left ballots of the original honest voters where r 0 is replaced with r 0

• the ballots given as input to dishonest voters j > p, computed using RR j , which, as explained earlier, are computed in the same way as the ballots of the original dishonest voters, from the list of honest ballots where all random values r are replaced with the corresponding r. Hence, the randomness-independence property (Lemma 4) applies, and guarantees that tallying the ballots in P i with tr, and in Q L with tr produces the same result. The same argument applies to P i+1 and Q R . Thus, R(w tall ) = w tall satisfies 3.

Using property 3, we can now conclude the proof. Indeed, by 1, Q L and Q R are trace equivalent, which, applied to tr, implies that that φ L ∼ φ R . Since R is a frame of recipes, it follows immediately from the definition of static equivalence that Rφ L ∼ Rφ R .

On the other hand, tr was obtained as a non-equivalence witness for P i and P i+1 , meaning that φ L ∼ φ R . Thus there exist recipes M , N such that

Since none of the public names r appear in φ L or φ R , we may always w.l.o.g. choose M and N that do not contain these names either. We then have

Since σ is a bijective renaming, this means

i.e. M R ? = N R is a test distinguishing φ L and φ R . This contradicts 1. Therefore, assumption 2 was false, i.e. P i ≈ t P i+1 , which concludes the proof.

Appendix D Some counting functions

D.1 Some 1-bounded counting functions

Multiset. The result is the multiset of all votes. Formally, in our setting, a term representing that multiset is computed:

equality on multisets). For instance, if we just output the list of all votes, the order cannot matter

Sum. A total of points total is given to each voter who decides to distribute them among the candidates of his choice. The result is a vector of integers representing the total of points obtained by each candidate. Assuming c candidates, for all n, we have: ,p c ) with 1 ≤ i ≤ n, and p 1 , . . . , p c ∈ N with p 1 + . . . + p c ≤ total, and f is a function from vectors of c integers to terms such that f ( # "

equality on vectors of integers)

.

Appendix E Proof of the reduction to k dishonest voters

In this section, we recall and prove Proposition 2.

Proposition 2. Let V be a voting scheme whose associated counting function is k-bounded for k ≥ 1. If V does not satisfy BPRIV(1, n) for some n ≥ 1, then V does not satisfy BPRIV(1, k ) for some k ≤ k. Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box.

Proof. First, relying on Lemma 2, we know that the processes under study are action-deterministic, and therefore, thanks to Proposition 3, we can assume that a witness of an attack of minimal length has some specific shape. Following the notation introduced in Section 3, we consider n + 1 distinct voters #" v 0 , . . . , # " v n , and we consider a witness tr of non-equivalence of minimal length. We know that:

and tr is Σ err -free.

In case n ≤ k, then the result is straightforward. Indeed, thanks to actiondeterminism, such a witness is also a witness of non-equivalence regarding:

. Indeed, we have that cr i and u i do not occur anymore in the remaining process to be executed since DVoter is not executed for id j . We have that this trace tr leads to the frames φ L (on the left) and φ R (on the right) such that φ X = φ X {cr i → cr i }{u i → u i } ∪ {w i → cr i , Pub(cr i , u i ) } for X ∈ {L, R}. Since, we know that φ L ∼ φ R , we conclude that φ L ∼ φ R , and thus we are done. Note that, in case the distinguishing test relies on w i , we can easily reconstruct the corresponding term cr i , Pub(cr i , u i ) to obtain a witness of φ L ∼ φ R . Otherwise (no output on c i with i > 0 during phase 1), we have that the trace tr passes also starting from

, and the resulting frames are the same than those obtained when starting the executions from

. Therefore, we have that tr is a witness of nonequivalence for

Case 3: tr contains actions from phase 3 (actually only one). We distinguish three cases:

-If during phase 2, there is some action on channel c i with i > 0in(c i , R), and out(c i , w) but not the append(c i ) one -then we can consider tr = tr{w → R} where tr is equal to tr without these actions (input and output) on channel c i , and we can show that this trace tr is a witness of non-equivalence obtaining a contradiction regarding the minimality of tr. -Now, in case phase 1 contains an action of the form out(c i , w i ) corresponding to the output of a credential of a dishonest voter id i (i.e. i > 0), whereas there is no in(c i , R i ) during phase 2 for this particular (dishonest) voter, then we consider the trace tr which is equal to tr without this output out(c i , w i ), and we also replace the occurrences of w i in tr by cr i , Pub(cr i , u i ) where cr i and u i are fresh public constants. As before, we conclude that tr is a smaller witness. -We now consider the case of a trace tr that is composed of a phase 1 during which only dishonest voters who cast their ballot (action append) participate to phase 1, then a phase 2, and then tr contains the output on channel c res done in phase 3. We also know that the last output (the one on c res ) is needed to get a witness of non-equivalence, and we have that φ L ∼ φ R where φ L and φ R are the two resulting frames. Thus, the test distinguishing these two frames relies on w tall (the message outputted on c res ). Actually, relying on Lemma 3, we have that that w tall φ L = E w tall φ R . Moreover, we know that w tall φ L = count(extract(BB L )) and w tall φ L = count(extract(BB R )) where BB L (resp. BB R ) is the bulletin board (i.e. the content of the memory cell m bb ) resulting from trace tr on the left (resp. on the right).

If at most k voters voted (i.e. cast their vote -action append), then we know that only the dishonest voters who casted a vote outputted their credential

Appendix F Handling the case of revote

In this section, we recall and prove Theorem 2.

Theorem 2. Let V be a voting scheme whose associated counting function is k-bounded for some k ≥ 1, and p, n be two integers such that 1 ≤ p ≤ n. If V does not satisfy BPRIVR(p, n -p), then V does not satisfy BPRIVR(1, k ) for some k ≤ k. Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box (each from a different voter).

Proof. The proof follows the same lines as the proof of Theorem 1 and is composed of two main steps:

1. reducing the number of honest voters to 1; 2. reducing the number of dishonest voters to k.

For each step, rather than redoing the proof completely, we highlight the differences with the "no revote" case.

Step 1. We show that if BPRIVR(1, n -1) holds, then so does BPRIV(p, n -p).

The proof for step 1 has the same structure as the one for Proposition 1. The only difference, essentially, is that instead of each honest voter only submitting one ballot, which we have to simulate for a dishonest voter, they may submit any number of ballots. Thanks to the actions sess(c j , d) added to the trace, we know however which voter each ballot belongs to. Using this information, we can simulate the honest ballots, just as in the previous proof.

We start with n distinct voters #" v 1 , . . . , # " v n , with for all i #" v i = (c i , id i , cr i , pcr i ), pcr i = Pub(cr i , u i ), and p ∈ 1, n .

We define intermediate processes P i (for i ∈ 0, p ) similarly to the previous proof. P i is like ElectionRevote X p,n-p ( #" v 1 , . . . , # " v n ), except that the first i honest voters use process HVoter R , and the other p -i use process HVoter L .

As in the "no revote" proof, we show by contradiction that ∀i ∈ 0, p -1 . P i ≈ t P i+1 which suffices to prove the claim.

Assuming some i such that P i ≈ t P i+1 , as before, we define two processes Q L , Q , where all voters except voter i + 1 are modelled by process DVoter, and voter i + 1 uses

We consider a minimal trace tr witnessing P i ≈ t P i+1 , with associated frames φ L , φ R . Its shape is slightly different from the one in the previous proof, because of the sess(c j , d) actions added whenever voter j is replicated for a new session. However the ideas are the same.

We obtain a contradiction, as before, by constructing a trace for processes Q L and Q R that simulates tr, and is therefore a non-equivalence witness, contradicting

Ignoring the nonce renaming issues (which are handled just as in Proposition 1), this trace is constructed as before. For each j ∈ 1, p , we can read in tr (and the frames) the voting instructions submitted by the attacker for each session of voter j. We can read in the trace which instruction is addressed to which voter, thanks to the action sess(c j , d) that binds the channel d used in a given session to the voter running that session (or rather, her channel c j ).

For each session of each honest voter j = i + 1, we can thus construct recipes computing two ballots, containing the attacker's instruction for that session.

We then consider the sequence tr of actions obtained from tr by replacing any input on a honest session's channel d with an input of the recipe for the appropriate ballot: the left ballot if that session belongs to voter j > i + 1, the right one otherwise. Just as in the previous proof, we also replace any dishonest ballot input of a recipe R with a recipe S, which is R where all frame variables for honest ballots (except id i+1 's) are replaced with the appropriate ballot recipe.

These actions effectively simulate the behaviour of all honest voters in P i , P i+1 , except i + 1, with dishonest voters in Q L , Q R . The same arguments as before show that tr is executable in Q L , Q R , and produces some frames φ L , φ R . We then only need to show that φ L , φ R can be reconstructed from φ L , φ R using the same recipe. As in the "no revote" case, this shows φ L ∼ φ R , which constitutes the contradiction that concludes the proof.

We construct that recipe, as before, with a recipe that