Stéphanie Delaune
email: stephanie.delaune@irisa.fr

Joseph Lallemand
email: joseph.lallemand@irisa.fr

Arthur Outrey
email: arthur.outrey@ens-lyon.fr

One Vote is Enough for Analysing Privacy 1

Keywords: Electronic voting, Formal methods, Protocol verification, 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. We first consider the case where voters do not revote, and the ballot box is trusted before relaxing these two conditions. 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 votes -essentially, 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, in the case of a trusted ballot box [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF], with later extensions to handle an untrusted one [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[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 equivalence-based 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 diffequivalence. 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] 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 e-voting 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. In the computational setting, for instance, the casting of a ballot is handled by an oracle adding it to the ballot box. This means it is implicitly assumed that a ballot cast will necessarily reach the ballot box, and this is an important assumption when analysing weeding-based protocols (where duplicate ballots are eliminated before tallying).

Second, we identify some conditions under which BPRIV can be analysed considering only one honest voter and k dishonest ones, casting at most k ballots in total. The bound k depends on a property of the procedure used to count votes which we define. 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 restrict the equational theory, and our result applies for different counting functions. We first establish the reduction result in the setting where voters do not revote, and the ballot box is trusted. We then propose two extensions: we show the same result still holds when allowing revote, and when facing a dishonest ballot box. In the case of the untrusted ballot box, this requires us to propose an adaptation of the game-based definition of [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF] to the symbolic model.

Finally, we apply our result on several e-voting protocols from the literature relying on the tool Proverif. Even if our theoretical reductions result are generic, we are limited in practice by the features offered by the tools (e.g. homomorphic encryption is not supported by existing tools). Nevertheless, relying on Proverif, we successfully establish that BPRIV holds for an arbitrary number of voters in several cases. 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. This paper is an extended version of our work [START_REF] Delaune | One Vote Is Enough for Analysing Privacy[END_REF], published at the 27 th ESORICS conference (2022): in particular, the BPRIVD definition as well as the reduction result established in Section 6 to deal with the case of a dishonest ballot box is entirely new.

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 [START_REF] Abadi | Mobile values, new names, and secure communication[END_REF]. Participants are represented by processes, while messages exchanged between participants are represented by terms. 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 Σ = Σ c ∪ Σ d consisting of a finite set of function symbols together with their arity. We distinguish between constructors in Σ c and destructors in Σ d . We denote Σ + = Σ c Σ 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 where symbols in Σ Helios are constructors.

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 (Σ + ∪ Σ d , 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.

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 order to provide a meaning to constructor symbols, we equip (constructor) terms with an equational theory. We assume a set E of equations over T (Σ c , X ), and define = E as the smallest congruence containing E that is closed under substitutions.

In addition, the semantics of destructor symbols is given by a set R of ordered rewriting rules of the form g(M 1 , . . . , M n ) → M 0 with M 0 , M 1 , . . . , M n ∈ T (Σ c , X ). A ground expression D can be rewritten in D if there is a position p in D, a rewrite rule g(M 1 , . . . , M n ) → M 0 and a substitution θ from variables to ground terms such that D| p = E g(M 1 θ, . . . , M n θ), and D = E D[M 0 θ] p , i.e. D in which the subterm at position p has been replaced with M 0 θ. In case more than one rule may be applied at position p, only the first such rule can be effectively used. Moreover, we assume that the last rewriting rule defining a destructor g is of the form g(x 1 , . . . , x n ) → M 0 with x 1 , . . . , x n distinct variables, and thus always applies. Given a ground expression D, it may be possible to rewrite it (in an arbitrary number of steps) into a ground (constructor) term M : in that case, this term is noted D⇓, and we say that D evaluates to D⇓. Note that, in our setting, a computation never fails.

We extend the notation = E to terms that may contain destructor symbols (that never fail). We write u = E v when u⇓ = E v⇓.

Example 3. Consider Σ d = {ite} where ite is a destructor symbol of arity 4 that can be used to model conditional branching with the following ordered rewriting rules:

ite(x, x, y, z) → y ite(x, x , y, z) → z
The destructor defined in Example 3 may seem of little use, since it does not let an attacker compute any value he did not already know. It does indeed not bring extra power to the attacker. However, when dealing with the case of a dishonest ballot box, having such a construction will make it easier to write recipes used in our reduction result.

In the following, we consider an arbitrary signature Σ = Σ c ∪ Σ d , and we simply assume that the equational theory E (equations built over Σ c only), 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:

P, Q ::= 0 | P | Q | ! P | new n. P | new d. P | out(c, u). P | in(c, x). P | ! new d. out(c, d). P | let x = u in P | if u = v then P else Q | m := u. P | read m as x. P | append(c, u, m). P | phase i. P where n ∈ N , x ∈ X , m ∈ M, u ∈ T (Σ + , X ∪ N ), d ∈ Ch pri , c ∈ Ch, i ∈ N.
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 . Note that destructor symbols are not allowed in the syntax of processes. In case the recipe used by the attacker contains such a destructor, the hypothesis imposing that a computation never fails ensures that the resulting term is indeed a message. 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 4. 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, and is fully displayed in Figure 1.

For instance, considering an input on a public channel, i.e. the rule In, the attacker can inject any message Rφ 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 (rule Out-Err), or indirectly through the frame (rule Out). The rule Append corresponding to our new append action append(c, u, m) simply consists in appending a term u to the memory cell m. yes }, and the configuration K yes 0 = (2; {P }; φ yes ; {m bb → nil}). We have:

K yes 0 in(c,w 1 ).out(c,err invalid ) = ============= ⇒ (2; ∅; {w 0 → pk(sk), w 1 → b id H yes }; {m bb → nil}) K yes 0 in(c,R 0 ).out(c,w 2 ).append(c) = ================ ⇒ (2; ∅; {w 0 → pk(sk), w 1 → b id H yes , w 2 → b id D 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.

Par (i; {|P 1 | P 2 | } ∪ P; φ; M ) = ⇒ (i; {|P 1 , P 2 | } ∪ P; φ; M ) Zero (i; {|0| } ∪ P; φ; M ) = ⇒ (i; P; φ; M ) New-N (i; {|new n. P | } ∪ P; φ) = ⇒ (i; {|P {n → n }| } ∪ P; φ; M ) if n ∈ N ,
= ===== ⇒ (i; {|P | } ∪ P; φ; M ) if c ∈ Ch pub , c err ∈ Σ err Out (i; {|out(c, u). P | } ∪ P; φ; M ) out(c,w) = ==== ⇒ (i; {|P | } ∪ P; φ ∪ {w → u}; M ) if c ∈ Ch pub , u ground term not equal (modulo E) to a constant in Σ err , w ∈ W \ dom(φ)
In (i; {|in(c, x). P | } ∪ P; φ; M ) in(c,R) = === ⇒ (i; {|P {x → Rφ⇓}| } ∪ P; φ; M ) if c ∈ Ch pub , and R is a recipe such that var(R) ⊆ dom(φ) Priv (i; {|out(c, u). P, in(c, x). Q| } ∪ P; φ; M ) = ⇒ (i; {|P, Q{x → u}| } ∪ P; φ; M ) if c ∈ Ch pri , and u is a ground term Let (i; {|let x = u in P | } ∪ P; φ; M ) = ⇒ (i; {|P {x → u}| } ∪ P; φ; M ) if u is ground Then (i; {|if u = v then P else Q| } ∪ P; φ; M ) = ⇒ (i; {|P | } ∪ P; φ; M ) if u, v
; M ) = ⇒ (i; {|P {x → u}| } ∪ P; φ; M ) if M (m) is a message Append (i; {|append(c, u, m)| }. P ∪ P; φ; M ) append(c) = ===== ⇒ (i; {|P | } ∪ P; φ; M {m → u :: M (m)}) if m ∈ dom(M ) Phase (i; P; φ; M ) phase i+1
= ===== ⇒ (i + 1; P ; φ; M ) where P = {|P | phase i + 1. P ∈ P| } ∪ {|phase j. P | phase j. P ∈ P ∧ j > i + 1| } (keeping multiplicity)

R 1 φ = E R 2 φ ⇔ R 1 φ = E R 2 φ .
When establishing our reduction result, we will reason on the notion of static equivalence. In particular, we will assume an attack trace exists, and that this attack comes from publishing the result of the election, i.e. that the two processes are in trace equivalence until the result is output. In such cases, we will deduce that the results output by the tally on either side are different (modulo E). This result is formally stated and proved below and will be used in the proof of our main result. Lemma 1. Let t L and t R be two public terms, i.e. t L , t R ∈ T (Σ c , Σ 0 ). Let φ L , φ R be two frames such that φ L ∼ φ R , and w tall ∈ W dom(φ L ). We have:

φ 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 (Σ c , Σ 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 }. Then 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.

Trace equivalence is the active counterpart of static equivalence. Two configurations are in trace equivalence if, however the attacker behaves, the resulting sequences of messages observed by the attacker are in static equivalence. 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 6. 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, let us replace P with 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). The resulting trace 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.

In the following, we will consider action-deterministic configurations. Intuitively, for an actiondeterministic configuration K, once the trace tr is fixed, the configurations that are reachable following the trace tr are equal up to some α-renaming. Definition 5. 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 i 1 = i 2 , and φ 1 and φ 2 are equal modulo α-renaming of names generated during the execution.

Consider two ground processes P and Q whose associated configurations (0; {P }; ∅; ∅) and (0; {Q}; ∅; ∅) are action-deterministic. A witness of non-inclusion for P t Q is actually a trace tr for which there exists φ P such that (tr, φ P ) ∈ traces(P P ), and

• either there does not exist φ Q such that (tr, φ Q ) ∈ traces(P Q ); • or such a φ Q exists and φ P ∼ φ Q .
Indeed, once tr is fixed, the resulting configuration is unique up to α-renaming, thus there is no need to consider all the frames φ Q such that (tr, φ Q ) ∈ traces(Q) to establish that they are not in static equivalence with φ Q . It is sufficient to consider one representative.

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 6. 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 as a collection of processes that model the behaviour of voters, and a process representing the tallying authority. The election process is composed of several phases.

Phases 0 and 1: Setup. In the first two phases of the process, the election material is generated and published. More precisely, the election public key is published in the initial phase, and the public credentials of voters in phase 1.

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. This ballot box will be tallied at the end of the election. In fact, as we will see later on, when writing the BPRIV property, we will rather store the lists of ballots (bb 0 , bb obs ) in m bb , containing real and "observable" (sometimes fake) ballots. 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. While the attacker can modify messages on the public channel, he cannot directly access the memory cell, and thus he cannot impersonate the voter to submit a different ballot. 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. We will, in addition, use different channel names for the public channels used by each voter. This is more convenient when reasoning about traces, as it makes it easier to observe which voters have voted in a given trace.

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. The exact nature of this validity test depends on the construction of the ballot, and thus on the protocol considered. 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 7. 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] Delaune | Verifying Privacy-type Properties of Electronic Voting Protocols[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 8. We continue Example 7 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. The attacker has access to an oracle for each voter, and the oracle takes care of everything that happens when the voter votes. For honest voters, the attacker may submit two possible votes to the oracle, and the oracle constructs ballots accordingly, checks their validity, and records them in the ballot box. For dishonest voters, he may submit any ballot, and the oracle checks its validity and adds it to the box. 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 7. 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. In contrast, in our formalism, we allow executions where the process HVoter is not executed until its end: the attacker could send vote instructions, receive the ballot on the public channel, and leave the process at that point, without executing the end, so that the ballot is never added to the ballot box. 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 boxotherwise, some duplicates could be missed, if the original was blocked.

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 9. The Valid recipe and C tally computation from Examples 7 and 8 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 result

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 (see Section 4.3), and then we prove that the number of dishonest voters can be bounded as well (see Section 4.4). Before detailing these two parts, we first formally state our reduction result in Section 4.1, and we give in Section 4.2 a precise characterisation of an attack trace regrding the property BPRIV (when such a trace exists).

Main result

In order to reduce the number of dishonest voters needed to mount an attack against BPRIV, we need an additional assumption on the counting function used in the e-voting protocol. 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 8. 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 i 1 , . . . , v i k ]) = E count([v i 1 , . . . , v i k ]).
This assumption needed to establish our reduction results captures the most common counting functions such as multiset, sum, majority presented below.

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

for all n, count # ([v 1 , . . . , v n ]) = f ({|v 1 , . . . , v n | }) where f is a function such that f (M 1 ) = E f (M 2 ) (equality on terms) iff M 1 = # M 2 (
equality on multisets). For instance, if we just output the list of all votes, the order cannot matter

, i.e. count # ([a, b]) = E count # ([b, a]).
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:

count Σ ([v 1 , . . . , v n ]) = f ( n i=1 v i ) where v i = (p 1 , . . . , 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 ( #"

u 1 ) = E f ( #" u 2 ) (equality on terms) iff #" u 1 = #"
u 2 (equality on vectors of integers).

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

Lemma 2. 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 such that v i 0 = v i 0 . Hence, count([v i 0 ]) = count([v i 0 ]
), which concludes the proof for count # . A similar reasoning applies for count Σ , and count Maj .

We can now state our main reduction theorem establishing that to study BPRIV, it suffices to consider one honest voter, and at most k dishonest ones, as soon as the counting function is k-bounded. 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). Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box. This theorem is an easy consequence of Proposition 2 and Proposition 3 stated and proved in Section 4.3 and in Section 4.4.

Example 10. 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 6, 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.

Characterisation of an attack trace

In the proofs in the next two sections (i.e. Sections 4.3 and 4.4), we will start with an attack trace on the election process involving n voters, and show that an attack trace still exists considering less (honest) voters. To ease the proofs of these reduction results, we start by giving a precise characterisation of an attack trace (when such a trace exists). This characterisation is stated in Proposition 1. We first show that the election processes we study are action-deterministic.

Lemma 3. The two ground processes Election

L p,n-p ( #" v 1 , #" v 2 , . . . , #" v n ) and Election R p,n-p ( #" v 1 , #" v 2 , . . . , #"
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. 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.

We can now show that when considering an attack trace tr, i.e. a witness of non-inclusion between two election processes, the attack trace can be considered w.l.o.g. to be Σ err -free. That is, tr does not contain any occurrence of c err for any c err ∈ Σ err . We can also assume that the non-equivalence comes from static non-equivalence, and that inputs in phase 2 are messages representing valid voting options. Proposition 1. 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. Then 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 ).
As the processes under consideration are action-deterministic (Lemma 3), 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) 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 ); or (2) 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 ).
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 strong correctness, i.e.:

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: 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 the remaining 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 output. 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 Rφ L = E (v 0 , v 1 ) for any (v 0 , v 1 ) ∈ Votes 2 , and, again by minimality of the witness, 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 output 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.

Reduction to one honest voter

When designing symbolic definitions that formalise security properties, even when an arbitrary number of participants are involved, a common modelling choice is to particularise the definition on a small number of honest agents, on which the property should hold. For instance, a key agreement property is often formalised by requiring that two fixed (but arbitrary) honest agents agree on the key at the end of their session, even in presence of arbitrarily many dishonest agents. A more general definition would require that the same holds for any number of honest agents running the protocol in parallel, so that any two honest agent agree on a key once they finish a session together. The choice of fixing the honest agents when formalising the property produces a simpler property, with less honest sessions in parallel, which is usually easier on the automated tools. It is usually justified by arguing (more or less formally) that it implies the more general version: given an arbitrary number of honest agents, for any pair of agents, we can see from their point of view all other agents as potentially corrupted, and thus the simpler property applies and shows they agree.

A similar choice is implicitly made when considering the swapping definition for vote privacy. Indeed, the more general version would require that two scenarios, where the votes of any number of honest voters have been permuted, are always indistinguishable. This general formulation would in fact be closer to the one used in the computational setting. In contrast, the symbolic swapping definition consider two particular honest voters Alice and Bob, whose votes are exchanged. To justify this choice, it could be argued that, as any permutation can be decomposed in a finite sequence of swaps of two elements, by applying the seemingly weaker property as many times as needed, we can recover the general version. This argument is however not often formalised.

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 with dishonest ones is non trivial as the behaviour of an honest voter can not be mimicked by a dishonest one, or simply compensated by some steps performed by the attacker. 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 2. 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).

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 We fix 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}. For any i ∈ {0, . . . , p}, we define: use the fake one (their v 1 ). We consider intermediate processes P 0 , . . . , P p : as displayed in Figure 2, 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 i 0 +1 and P i 0 are not equivalent. These two processes differ only by the i 0 + 1 th HVoter, who is HVoter L in P i 0 , and HVoter R in P i 0 +1 . This voter will be our particular voter, who will remain honest, solving issue (i). All other HVoters behave the same in P i 0 and P i 0 +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.

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

Before proving the reduction result, let us first observe that since the Valid recipe and the C Tally computation process do not use any private names, and always return public values, their output cannot depend on the random values used in the ballots/credentials. More precisely, these random values can be renamed and/or replaced with public fresh names without changing the outcome of Valid or C Tally . This property, which we will refer to as randomness independence, is a direct consequence of the construction of terms and semantics of processes in our symbolic model. We will use it in the proof of the reduction theorem, and for this reason we state it formally below. Lemma 4. Consider a key sk ∈ N , with the associated pk = pk(sk), and n distinct voters id 1 , . . . , id p , id p+1 , . . . , id n ∈ Σ 0 , meant to represent p honest voters and n -p dishonest ones, each with their credential cr i ∈ N . Let φ 0 denote the frame of public keys and credentials

φ 0 = { w 0 → pk, w 1 → Pub(cr 1 , u 1 ), . . . , w p → Pub(cr p , u p )),
w p+1 → cr p+1 , Pub(cr p+1 , u p+1 ) , . . . , w n → cr p+1 , Pub(cr p+1 , u p+1 ) }.

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

φ 1 = {w 1 → Vote(pk, id i 1 , cr i 1 , v 1 ,
• Valid(R 1 φ, R 2 φ, R 3 φ, pk) = E true ⇔ Valid(R 1 φσ, R 2 φσ, R 3 φσ, pk) = E true; and • C tally (R 4 φ, sk) = E C tally (R 4 φσ, sk).
We can now recall and give a detailed proof of Proposition 2.

Proposition 2. 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 will show that under our assumptions we have P i ≈ t P i+1 for any i ∈ {0, . . . , p -1} where P i are the processes displayed in Figure 2. Since 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 process Q X with X ∈ {L, R} is as follows:

Q X = 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 X ( # " 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 X = ElectionX 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 have

Q L ≈ t Q R .
By contradiction, let us now assume that P i ≈ t P i+1 . Using Lemma 3, P i , P i+1 , Q L , Q R are action-determinate. Let tr be a witness of this non-equivalence of minimal length. Thanks to Proposition 1, 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 , and tr is Σ err -free.

Moreover, for any j ∈ {1, p}, if in(c j , R) occurs in tr in phase 2 (for some R), then there exist (v 0 , v 1 ) ∈ Votes × Votes such that Rφ L = Rφ R = E (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 nameswithout 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 i 1 , w i 1 ). . . . .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 ),

• 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 action-determinacy, 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 )σ (1)
R is constructed as follows:

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

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

Using property (1), we can now conclude the proof. Indeed, we know that Q L ≈ t Q R , 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 M φ L = N φ L and M φ R = N φ R , i.e.

M (Rφ

L )σ = N (Rφ L )σ and M (Rφ R )σ = N (Rφ R )σ .
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

M (Rφ L ) σ = N (Rφ L ) σ and M (Rφ R )σ = N (Rφ R )σ .
Since σ is a bijective renaming, this means

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

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.

Proposition 3. 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 0, then V does not satisfy BPRIV(1, k) Moreover, in that case there exists a witness of this attack where no more than k ballots reached the ballot box.

Roughly, 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 dishonest voters.

We now give a detailed proof of Proposition 3.

Proof. First, relying on Lemma 3, we know that the processes under study are action-deterministic, and therefore, thanks to Proposition 1, 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:

• Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v n ) tr = ⇒ (i L ; P L ; φ L ; M L ) for some (i L ; P L ; φ L ; M L ); • Election R 1,n ( #" v 0 , #" v 1 , . . . , #" 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.

We are going to show that this minimal witness tr is also a witness of the following 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 i 1 , w i 1 ). . . . .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, tr cannot 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 consider the case where some actions in phase 2 are performed by a dishonest voter id j , i.e. there is in(c j , R j ) ∈ tr and possibly out(c j , w j ) ∈ tr, and append(c j ) as well.

Then, 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 and R j is the recipe mentioned above 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, 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 know that φ L ∼ φ R implies that φ L ∼ φ R , and thus since φ 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. out(c i , w i ) occurs in phase 1, and 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. Then tr

passes in Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v n ) and also in Election R 1,n ( #" v 0 , #" v 1 , . . . , #" v n ).
Indeed, cr i and u i do not occur anymore in the remaining process to be executed since DVoter is not executed for id j . 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 , which proves this case. 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), the trace tr also passes starting from

Election L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ), or from Election R 1,k ( #" v 0 , #" v 1 , . . . , #" v k )
, and the resulting frames are the same as those obtained when starting the executions from

Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v n ), and Election R 1,k ( #" v 0 , #" v 1 , . . . , #" v n ). Therefore, tr is a witness of non- equivalence for Election L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t Election R 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) contradicting our main hypothesis.
Case 3: tr contains actions from phase 3 (actually only one). We distinguish three cases.

• If during phase 2, some action occurs 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.

• Otherwise, if 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 phase 1 during which only dishonest voters who cast their ballot (action append) participate to phase 1, then phase 2, and then phase 3 containing the output on channel c res . We also know that the last output (the one on c res ) is needed to get a witness of non-equivalence, and 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 output on c res ). Actually, relying on Lemma 1, we have w tall φ L = E w tall φ R . Moreover, we know that w tall φ L = count(extract(BB L )) and w tall φ R = 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, as we know that only the dishonest voters who cast a vote output their credential during the initialisation phase, we can deduce that this witness tr is also a witness of

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 cast 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 i 1 , . . . , id i k still leads to a difference in the result. In the trace tr, we know that there are actions append(c i 1 ), . . . , append(c i k ) corresponding to the append actions of these voters id i 1 , . . . , id i k . We consider tr obtained from tr by removing all these actions. It is easy to see that this smaller trace tr still passes in

Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v n ) and in Election R 1,n ( #" v 0 , #" v 1 , . . . , #" v n ).
The resulting bulletin board BB L (resp. BB R ) contain less ballots than before, and these ballots have been chosen such that:

count(extract(BB L )) = count(extract(BB R ))
Therefore, the resulting frames φ L and φ R are almost the same as φ L and φ R , except for the result output during the tallying phase, which we know are different public terms. As our processes are action-deterministic (Lemma 3), there is no other choice to obtain another frame, and thus tr is a smaller witness of

Election L 1,n ( #" v 0 , #" v 1 , . . . , #" v n ) ≈ t Election R 1,n ( #" v 0 , #" v 1 , . . . , #" v n ), leading again to a contradiction.
Hence the result.

Dealing with revoting

We now consider the case where re-voting is allowed. We first adapt the BPRIV definition to this setting (see Section 5.1) before stating and discussing our reduction result in Section 5.2 and Section 5.3.

Modelling BPRIV with re-voting

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

Reduction result with re-voting

We are now able to state our reduction result when considering re-voting.

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). 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 re-vote is not allowed, and is composed of two main reduction steps. Before performing these two reduction steps, we may note that our election processes are still action-deterministic. Actually, the construction new d.out(c, d).P is there for that, and Proposition 1 charaterizing the form of a minimal attack trace is still valid for these election processes where re-vote is allowed. Rather than redoing the proof completely, we highlight the differences with the "no revote" case for these two steps.

Step 1: Reducing the number of honest voters to 1. We show that if BPRIVR(1, n -1) holds, then so does BPRIV(p, n -p). The proof for this step has the same structure as the one for Proposition 2. 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. As in the "no revote" proof, we define intermediate processes P i for i ∈ {0, . . . , p}), and we assume by contradiction that there exists i 0 such that P i 0 ≈ t P i 0 +1 . 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.

Step 2: Reducing the number of dishonest voters to k. Again, the shape of the witness of non-equivalence that we consider is a bit different from the one used in Proposition 3 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, some actions (e.g. sess(c i , d), in(d, R), out(d, w)) occur on channel c i (with i > 0) but not the corresponding append(d) actions, 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 where the occurrences of w i are replaced with cr i , Pub(cr i , u i ) for fresh public constants cr i and u i . As before, we conclude that tr is a smaller witness. • We now consider the case of a trace tr 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 φ L ∼ φ R where φ L and φ R are the two resulting frames, and in fact, relying on Lemma 1, we have 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 cast their vote (action append), then we know that only these dishonest voters have output their credential during the initialisation phase, and thus this witness is also a witness of

ElectionRevote L 1,k ( #" v 0 , #" v 1 , . . . , #" v k ) ≈ t ElectionRevote R 1,k ( #" v 0 , #" v 1 , . . . , #" v k ).
Moreover, this witness satisfies our requirements, which concludes the proof for this case. Otherwise, we know that n votes with n > k have been cast (possibly by the same voter),

i.e. 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 ), 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 cast more than one ballot, then we know that only one has been taken into account due to the revote policy, and thus there is i 0 such that b L i 0 and b R i 0 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 n > k. Therefore the policy will consider all 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 count(extract([b L i 1 , . . . , b L i k ])) = count(extract([b R i 1 , . . . , b R i k ]))
Note that, since each voter only votes once, this implies that

count(policy(extract([b L i 1 , . . . , b L i k ]))) = count(policy(extract([b R i 1 , . . . , b R i k ]))).
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, except for their last element corresponding to the output of the result. We have ensured a difference is maintained between the two sides, and thus tr is still a witness of non-equivalence, which concludes the proof.

Discussion

Even after applying our reduction result, 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.

Extension to the case of a dishonest ballot box

We now consider the case where the ballot box is no longer trusted. As in the previous section, we first adapt the BPRIV definition to this setting before stating and proving our reduction result.

Symbolic BPRIV with a dishonest ballot box

The symbolic definition we propose in Section 3.2, based on the original game-based formulation of [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF], considers a setting where the ballot box is trusted. Indeed, it does not give the attacker complete control over the contents of the ballot box: the attacker cannot arbitrarily write to the ballot box, but rather can only see and block honest ballots, and cast ballots in the name of dishonest voters only.

In [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF], an extension of BPRIV that features a fully dishonest ballot box is introduced: the attacker can arbitrarily choose the content of the ballot box. This creates additional difficulties compared to the honest ballot box case. In BPRIV, on the left-hand side, the attacker is shown the "real" ballots, i.e. the ones that will be tallied. On the right-hand side, he sees a "fake" ballot for each voter, while using the corresponding "real" ballot when tallying. Adapting naïvely this behaviour to the dishonest ballot box setting produces an unsatisfiable definition. Indeed, if the attacker can modify arbitrarily the "fake" ballots he received before sending them to be tallied, simply using (on the right-hand side) the unmodified "real" ballots to compute the election result would let him trivially distinguish the two sides. Instead, [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF] proposes to observe how the attacker modified the "fake" ballots, and to apply the same modifications to the "real" ballots before tallying. This leads [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF] to an extension of BPRIV, in the form of a cryptographic game, that relies on a so-called recovery algorithm, which performs the operation of finding out what modifications the attacker did on the "fake" ballots.

We propose here an adaptation of our symbolic BPRIV definition, that incorporates this idea. To simplify the presentation, we restrict ourselves to the case where voters do not revote.

Voter processes. We update the HVoter L and HVoter R processes as follows.

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 append(c, id, ⊥, ⊥ 3 , m ref bb ). out(c, b 0 ) 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 append(c, id, b 0 , b 1 3 , m ref bb ). out(c, b 1 ) else out(c, err invalid ) else out(c, err vote )
They are very similar to the honest ballot box case, except that the m bb list, which was used to store the list of "real" ballots to be tallied, is replaced with a list m ref bb , that stores no information on the left-hand side, and the correspondence between "real" and "fake" ballots on the right-hand side. Note that ballots are added to m ref bb before being publicly output: indeed, we wish m ref bb to store the list of all generated ballots, even ones the attacker may block later by choosing not to add them to the ballot box he will compute.

Since we give the attacker complete control over the ballot box, there is no longer need for a DVoter process to cast ballots in the name of dishonest voters.

Validity check. The ballot box to be tallied will be input directly from the attacker. Since the attacker has direct write access to the ballot box, we first check he has not added invalid ballots to it, and that only one ballot has been submitted per voter (as we exclude revote here). To do so, we will use the Valid(id, pcr, pk) recipe. To make the processes more legible, we ask that the attacker provides for each ballot the identity of the voter allegedly casting it. This information is public, so asking that does not restrict the attacker. We thus consider a computation C Valid (bb, creds, pk), that takes as parameters a list bb of pairs (id, b) of an identity and a ballot, a list creds of pairs (id, pcr) of all identities and public credentials, and the public election key pk. The computation C Valid iterates through list bb, and for each element (id, b) of bb (an element not of that form causes it to fail), goes through creds to: i) check that id is indeed the identity of an actual voter, ii) retrieve the associated pcr, iii) check that Valid(id, pcr, b, pk) = true.

In addition, for each (id, b) in bb, it checks that no other (id, b ) (with the same id) is present in bb. We do not extensively write the process C Valid here -we have already shown earlier how all the operations it performs (iteration on lists, comparisons) can be implemented as computation processes.

Recovery. Before actually performing the tally, the recovery operation must be performed on the right-hand side. Depending on the way this recovery is done, the resulting definition expresses stronger or weaker guarantees. For this reason, the computational BPRIVD notion from [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF] is defined parametrically w.r.t. the recovery algorithm.

In order to keep our symbolic definition similarly generic, we simply assume a computation C Rec (bb, bb ref ). It takes as parameter a list bb of pairs id, b of identities and ballots (to be instantiated with the list produced by the attacker), and a list bb ref of tuples id, b 0 , b 1 3 (where b 0 , b 1 are ballots or ⊥), and computes the list bb tal to be tallied. The recovery and tallying will then be performed in the following process:

TallyRecover(c, sk) = in(c, bb). if C Valid (bb, pk(sk)) = true then read m ref bb as bb ref . let bb tal = C Rec (bb, bb ref ) in let res = C Tally (bb tal , sk) in out(c r , res) else out(c, err vote ).
Example 11. A typical recovery algorithm consists in going through the list submitted by the attacker, and, for each ballot, checking if it is equal to a "fake" ballot generated by an honest voter. If so, the ballot is replaced with the corresponding "real" ballot for that voter, otherwise it is left unchanged. That algorithm, as discussed in [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF], leads to a property expressing that the attacker cannot modify honest ballots, but only choose to include them or to remove them -essentially, the ballots must be non-malleable.

We can encode it as the following recovery computation C 0 Rec (bb, bb ref ) 2 .

C 0 Rec (bb, bb ref ) = new c. out(c, bb, nil ) | in(c, nil, bb tal ). out(c b , rev(bb tal )) | ! in(c, id, b 3 :: l, bb tal ). new c . out(c , bb ref ). | in(c , nil). out(c, l, b :: bb tal ) | ! in(c , id , b 0 , b 1 3 :: ll). if b 1 = b ∧ b 0 , b 1 = ⊥, ⊥ then out(c, l, b 0 :: bb tal )
else out(c , ll)

As another example, we could encode a variant of that algorithm, useful e.g. in the case of the original Helios protocol, where instead of comparing the entire ballot b to ballots in bb ref , only the ciphertext proj 2 (b) is compared. (Recall that in our model of Helios, ballots are (id, ciphertext)see Example 7). This would express a weaker property overall, as discussed in [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF]: the ciphertexts are non-malleable, but the identity included in the ballot is -which makes for a very weak notion of privacy, but accurately characterises the level of security provided by the unpatched Helios.

Assumptions on the recovery computation. Verification tools tend to reason more easily on processes with a similar structure: for this reason, we include the recovery computation on both sides of the equivalence. On the left-hand side, bb ref will only contain id, ⊥, ⊥ 3 elements, and the recovery should not change the provided ballot box. Hence, we require that ⊥ values are ignored: Moreover, we will need for our reduction result to assume that C Rec has the following property, which we call partial recovery. Consider a list bb of terms, and a list

C Rec (bb, bb ref
bb ref = [(id 1 , b 0 1 , b 1 1 ); . . . ; (id n , b 0 n , b 1 n )]
containing n honestly generated ballots for distinct voters id i (i.e., computed by the Vote recipe, with fresh randoms each time). Then we assume

• for any permutation bb ref of bb ref , C Rec (bb, bb ref ) = C Rec (bb, bb ref ); • for any partition bb ref = bb ref 1 @bb ref 2 , C Rec (bb, bb ref ) = C Rec (C Rec (bb, bb ref 1 ), bb ref 2 ).
Intuitively, that property means that the recovery operation does not depend on the order in which ballots are cast, and can be computed piecewise on a partition of the ballots.

In addition, we assume that C Rec is computable by recipes, in the sense that for any integers l 1 , l 2 , there exists a recipe R l 1 ,l 2 with only two variables x bb , x ref , such that for all bb of length l 1 and bb ref of length l 2 , the result returned by the computation

C Rec (bb, bb ref ) is equal to R l 1 ,l 2 [x bb → bb, x ref → bb ref ].
The recipe R l 1 ,l 2 may of course depend on the length of the lists -typically, if C Rec iterates through the list bb, it will likely use hd(tl n (x bb )) to access the n-th Finally, we add another, more restrictive assumption on the recovery computation. These assumptions, up to the last one, do not seem overly restrictive, and hold for all recovery algorithms considered in [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF]. The final assumption on the other hand is much more restrictive: it typically prevents the recovery computation from adding back to the ballot box some ballots that may have been removed by the attacker. [START_REF] Cortier | Fifty Shades of Ballot Privacy: Privacy against a Malicious Board[END_REF] makes use of such recovery when modelling variants of the property that express additional verifiability guarantees -basically, by having the recovery add all ballots from the voters who check their vote. We forbid such recovery computations here, meaning that our reduction result does not hold when considering verifiability guarantees. These typically require that a subset of honest voters perform verifications, and get additional assurance that their vote is counted. It is not particularly surprising that these guarantees cannot be captured by only one honest voter.

Example 12. The computation C 0

Rec (bb, bb ref ) given in Example 11 satisfies these assumptions. That is clear from its construction for most of them: the partial recovery, ignoring ⊥ values, length preservation and stability by sublists. The condition that it is computable by recipes is less obvious. In practical examples, such as this one, it is convenient, in order to establish that property, to use an equational theory that includes the term-level if-then-else ite equation introduced in section 2.1. Indeed, with that construction, it becomes quite clear how to construct a (very large) recipe that compares each element of bb with each element of bb ref (for fixed-size lists), and keeps the appropriate ballots. Note that, when the processes we consider do not rely on the term-level ite equation (but only the recipes), adding it does not actually give more distinguishing power to the attacker. Indeed, the attacker could only gain power by using it to produce a recipe that takes different branches on either side, but in that case, only considering the condition of the construction would already produce a boolean that distinguishes the two sides.

BPRIVD against a dishonest ballot box. Overall, the BPRIVD property against a dishonest ballot box is as follows. with ch ∈ Ch pub , X ∈ {L, R}.

Reduction result with dishonest ballot box

We are now able to state our reduction result when considering a dishonest ballot box. Theorem 3. 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 BPRIVD(p, n -p), then V does not satisfy BPRIVD (1, k). Moreover, in that case there exists a witness of this attack where no more than k ballots are present in the ballot box computed by the attacker (each from a different voter).

The proof of this result follows the same steps as the one for the honest ballot box, with the same two main reductions. Note first that the election processes we defined for the dishonest ballot box case are still action-deterministic. In fact, Proposition 1 still holds for these new election processes. Rather than re-doing the entire reduction proof, we detail here only the differences with the honest ballot box case.

Step 1: Reducing the number of honest voters to 1. We first show that, assuming BPRIVD(1, n -1) holds, then BPRIVD(p, n -p) also does. The main idea for this proof is similar to the one for Proposition 2: we define hybrid election processes P i , where the first i honest voters behave like HVoter R , while the other p -i behave like HVoter L , going gradually from ElectionD L p,n-p to ElectionD R p,n-p as i increases. Formally, fixing n distinct voters #" v 1 , . . . , #" v n , with #" v i = (c i , id i , cr i , pcr i ), pcr i = Pub(cr i , u i ) for all i, and p ∈ {1, . . . , n}, we define: We then show that for all i ∈ {0, . . . , p -1}, we have that P i ≈ t P i+1 . Since the two extreme processes P 0 , P p are in fact ElectionD L p,n-p and ElectionD R p,n-p , this will prove by transitivity that BPRIVD(p, n-p) holds. Let i ∈ {0, . . . , p-1}, and

P i =
Q X = ElectionD X 1,n-1 ( # " v i+1 , #" v 1 , . . . , #" v i , # " v i+2 , . . . , #" v n ) for X = L, R.
By assumption, BPRIVD(1, n-1) holds, and thus Q L ≈ t Q R . To prove that P i ≈ t P i+1 , we will show that from a (minimal) witness tr of non-equivalence of these two processes, we can construct a trace tr showing the non-equivalence of Q L and Q R . The construction of tr is quite similar to the one in the proof of Proposition 2, with some added difficulties. In the honest case, we had to show that the attacker can use dishonest voters to simulate the behaviour of the honest ones, and cast the appropriate ballots to obtain the same election result in Q X as in P i , P i+1 . In the case of the dishonest ballot box, this part of the proof is easier: the attacker can reconstruct the ballots from honest voters, except # " v i+1 , in the same way as in the honest case, and simply use these in the recipe that constructs the final ballot box bb. The difficulty comes next: in ElectionD X (1, n -1), for all these simulated honest voters, no binding will be added to m ref bb . Thus, the recovered ballot box bb tal , obtained after the recovery computation, will differ from the one obtained in P i . To avoid this issue, the attacker needs to apply part of the recovery computation himself before submitting the ballot box.

From Proposition 1, tr is Σ err -free, is executable in P i , P i+1 , and produces frames φ L , φ R such that φ L ∼ φ R . From the form of the processes, we may w.l.o.g. assume that tr is (a prefix of) out(ch, w 0 ).phase 1.out(c i 1 , w i 1 ). . . . .out(c ip , w ip ).phase 2.tr cast .phase 3.in(ch, R bb ). out(c res , w tall ) where tr cast only contains at most one input (recipe R i ) then one output (frame variable w i ) on each channel c i , and no operation on other channels.

We can define for each j ∈ {1, . . . , p} with j = i + 1 recipes B 0 j , B 1 j , that compute the ballots b 0 , and b 1 produced by the honest voter #" v j . We omit the details of that construction, as they are similar to the honest ballot box case. Note that Lemma 4, regarding randomness independence, extends to the C Rec computation, and allows us to rename all private names with fresh public names, as in the previous proof -we will omit the details of that renaming from now on, for better legibility.

Just as in the previous proof, we let tr be the trace containing the same actions as tr, except that in tr cast , all inputs on c j with j = i + 1 are removed, and the recipe R bb used by the attacker to compute the ballot box for the input in phase 3 is replaced with a new recipe R bb which we will define shortly. Note, first, that regardless of how R bb is defined, tr is executable in Q L , Q R up to the input in phase 3, and produces at that stage frames φ L , φ R .

We first let R bb = R bb {w j → B 1 j } 1 j i {w j → B 0 k } i+1 j p . Intuitively, R bb represents the same computation as R bb , except that all ballots produced by the honest voters #" v j , with j = i + 1, are replaced with the appropriate recipe (recall that these voters vote the same way in P i , P i+1 ). Just as in the honest case proof, it can be shown that the recipes B 0 j , B 1 j produce the expected ballots when applied to both φ L and φ R , and thus R bb , applied to these frames, produces the same ballot boxes bb L , bb R that R bb computes on φ L , φ R .

Our goal is to choose R bb in such a way that the ballot boxes bb L , bb R it produces on φ L , φ R will lead, when given to the TallyRecover process, to the same result being output in Q X as the one for bb L , bb R in P i , P i+1 . The TallyRecover part in these processes differs only in the C Rec computation. v i+1 . Note that by construction of P i , P i+1 , that list only contains ballots from voters that behave the same in both processes, and is thus the same starting from bb ref,L or bb ref,R . By the partial recovery assumption, the recovery computation can be performed first on bb ref,X , (for X = L, R) and then on bb ref :

C Rec (bb X , bb ref,X ) = C Rec (C Rec (bb X , bb ref ), bb ref,X ).
Thus, our goal is achieved if we find a R bb that produces the list C Rec (bb X , bb ref ) when applied to φ X . By assumption, C Rec is computable by recipes, and thus there exists a recipe R with two variables

x bb , x ref such that C Rec (bb X , bb ref ) = R[x bb → bb X , x ref → bb ref ] for X = L, R.
We have already constructed a recipe R bb producing bb X from φ X . Using the recipes B 0 j , B 1 j , and variable w i+1 , we can easily construct a recipe R 2 that produces bb

ref from φ X . Choosing R bb = R[x bb → R bb , x ref → R 2 ]
then achieves our goal. The trace tr obtained using R bb as input in phase 3 is executable in Q L , Q R , and produces frames φ L , φ R . Moreover it leads to the same result being output in φ L (resp. φ R ) as in φ L (resp. φ R ).

The end of the proof is then just as in the honest ballot box case: we show that φ L and φ R can be reconstructed from φ L , φ R using the same recipe, and thus deduce that since φ L ∼ φ R , we have φ L ∼ φ R , meaning that tr is indeed a witness of non-equivalence of Q L , Q R .

Step 2: Reducing the number of dishonest voters to k. The second step of the proof is to show that for a k-bounded counting function, if BPRIVD(1, n) does not hold, then neither does BPRIVD(1, k). We in fact show that there is then a witness of an attack against BPRIVD(1, k) where the ballot box submitted for tallying by the attacker contains at most k ballots.

The proof is very similar to the one for Proposition 3, in the case of an honest ballot box.

Consider a minimal-length attack trace tr on BPRIVD(1, n), i.e. one that distinguishes ElectionD L 1,n ( #" v 0 , . . . , #" v n ) and ElectionD R 1,n ( #" v 0 , . . . , #" v n ) for some distinct voters #" v 0 , . . . , #" v n . By Proposition 1, we know that the sequence of actions tr is Σ err -free, is executable (and reaches the same phase) in both elections processes, where it produces respectively frames φ L , φ R such that φ L ∼ φ R . Moreover, from the form of the processes, we may assume w.l.o.g. that tr is a prefix of out(ch, w 0 ).phase 1.out(c i 1 , w i 1 ). . . . .out(c ip , w ip ).phase 2.tr cast .phase 3.in(ch, R bb ). out(c res , w tall ) where tr cast only contains at most one input (recipe R 0 ), then one append, then one output (frame variable w 0 ) on channel c 0 , and no operation on other channels.

We will now show that tr is in fact also a witness that ElectionD

L 1,k ( #" v 0 , . . . , #" v k ) ≈ t ElectionD R 1,k ( #" v 0 , . . . , #" v k
), which will conclude the proof. As in the case of the honest ballot box, we can distinguish three cases, depending on which point of the execution tr reaches.

Case 1: tr only contains actions in phases 0 and 1. That is not possible: all messages output in these phases are the same on both sides, and thus tr could not be a witness of non-equivalence.

Case 2: tr contains actions in phases 0, 1, 2, and potentially the input in phase 3, but not the output in phase 3. In other words, it reaches the casting phase, and the attacker maybe submits a ballot box, but the execution stops before the result is received. We can immediately discard the case where the input in phase 3 is performed: if that were so, then stopping the execution just before that input would still be an attack witness, since the input itself does not gain the attacker any new information. Hence, tr would not be minimal. In addition, tr cast necessarily contains an output on c 0 : otherwise, simply removing it and stopping tr at the end of phase 1 would yield a shorter attack trace, as inputs and appends do not modify the frame. Thus, tr cast = in(c 0 , R 0 ). append(c 0 ). out(c 0 , w 0 ). We then conclude by the same argument as in the honest ballot box case. In summary, any dishonest voters outputting their credentials in phase 1 are not needed to construct the frame, as the attacker could obtain the same frame (up to renaming) by using a credential he generated himself. Removing them would produce a shorter attack trace, hence by minimality there are none in tr. Thus the attack only involves one honest voter, and tr is already an attack trace witnessing ElectionD Then, by assumption on C Rec , we get that keeping only the ballots pointed by s in the ballot box submitted by the attacker leads to a different result:

L 1,k ( #" v 0 , . . . , #" v k ) ≈ t ElectionD R 1,k ( #" v 0 , . . . , #" v k ).
count(extract(C Rec (bb L | s , bb ref,L )) = count(extract(C Rec (bb R | s , bb ref,R ))).
Let R bb denote the recipe that constructs the list of elements of R bb pointed by indices in s.

These indices point to k elements of bb L , bb R , each of the form (id, b), where the ids are distinct voter identities (in #" v 0 , . . . , #" v n ). Moreover, for each index i, the ith elements of bb L and bb R necessarily contain the same id -otherwise, again, as the identities are public values, the attacker could build a shorter attack witness by simply looking at that element. Consequently, the ballots in R bb φ L and R bb φ R are recorded for the same k distinct voter identities.

Consider the trace tr, obtained from tr by keeping in phase 1 only the actions related to those k voters, and replacing R bb with R bb -using public names instead of w i variables for removed voters, if they were used in that recipe.

Consider also the ElectionD L 1,k and ElectionD R 1,k processes featuring the k voters we kept, plus #" v 0 (if that voter was not already one of the k ), and k -k additional dishonest voters (that are unused in tr). tr can be executed in those processes. That is clear up to the input in phase 3. That input is instantiated with bb L | s on the left, and bb R | s on the right. The validity test is then performed on that ballot box, and succeeds -indeed, it succeeded on bb L and bb R in tr, and by construction the removal of some of the dishonest voters cannot make it fail. The final result election output when executed tr is count(extract(C Rec (bb L | s , bb ref,L )) on the left, and count(extract(C Rec (bb R | s , bb ref,R )) on the right -two different public values. tr is therefore an attack witness on BPRIVD(1, k), in which the submitted ballot box has length k k, which concludes the proof.

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 considering different counting functions. In this section, we first present the counting functions, as well as the e-voting protocols that we consider for our analysis. Then, we discuss the results we obtained relying on the Proverif tool. Note that the analysis performed using Proverif is only render possible thanks to our reduction results that allows one to obtain a bound on the number of voters and on the number of ballots that reach the ballot box.

Counting functions under study

We apply our results on several case studies considering different counting functions. We have already introduced some classical counting functions in Section 4.1, namely multiset, sum, and majority, and we have shown that they are 1-bounded. We now add an example of a more involved counting functions: Single Transferable Vote (STV), used e.g. in the Australian legislative elections, for which we establish that it is 5-bounded when considering 3 candidates for 1 seat.

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 ≺. Let Count

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 i 0 = (c i 0 ,1 ; c i 0 ,2 ; c i 0 ,3 ) and v i 0 = (c i 0 ,1 ; c i 0 ,2 ; c i 0 ,3 ) with c i 0 ,1 = c i 0 ,1 . In such a case, we keep this vote, and we have

c i 0 ,1 = Count 3 STV ([v i 0 ]) = Count 3 STV ([v i 0 ]) = c i 0 ,1
. Case 2: Otherwise, for 1 i n, we have c i,1 = c i,1 . 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.

Hence, c 0 occurs as the first choice in some votes. Let i 0 , . . . , i k denote the indices of all such votes. We have c i j ,1 = c i j ,1 = c 0 for any j ∈ {0, . . . , k}. If the second choice is the same in all these votes, i.e. for j ∈ {0, . . . , k}, we have c i j ,2 = c i j ,2 , then the eliminated candidate at the second round, and thus the winner, would be the same on both sides, which contradicts our hypothesis.

Therefore, there exists j ∈ {i 0 , . . . , i k } such that v j = (c 0 , c 1 , c 2 ), v j = (c 0 , c 2 , c 1 ) where {c 0 , c 1 , c 2 } = {a, b, c}. We keep v j , but we need more, as Count 3 STV ([v j ]) = Count 3 STV ([v j ]) = c 0 . Since c 0 is eliminated at the first round:

(1) Either c 0 = a and there exist j 1 , j 2 such that c j 1 ,1 = c j 1 ,1 = b, and c j 2 ,1 = c j 2 ,1 = c. Keeping these two votes in addition to v j /v j , we get

Count 3 STV ([v j , v j 1 , v j 2 ]) = Count 3 STV ([v j , v j 1 , v j 2 ]
). (2) Or c 0 = b and there exist j 1 , j 2 , j 3 (all distinct) such that c j 1 ,1 = c j 1 ,1 = a, c j 2 ,1 = c j 2 ,1 = a, and c j 3 ,1 = c j 3 ,1 = c. Keeping these three votes in addition to v j /v j , we have

Count 3 STV ([v j , v j 1 , v j 2 , v j 3 ]) = Count 3 STV ([v j , v j 1 , v j 2 , v j 3 ]
). (3) Or c 0 = c and there exist distinct j 1 , j 2 , j 3 , j 4 such that c j 1 ,1 = c j 1 ,1 = a, c j 2 ,1 = c j 2 ,1 = a, c j 3 ,1 = c j 3 ,1 = b, and c j 4 ,1 = c j 4 ,1 = b. Keeping these four votes in addition to v j /v j , we get Count 3 STV ([v j , v j 1 , v j 2 , v j 3 , v j 4 ]) = Count 3 STV ([v j , v j 1 , v j 2 , v j 3 , v j 4 ]). We conclude that at most 5 votes are needed to ensure the result will be different.

In the following, we consider majority, multiset, sum, and STV (restricted to 3 candidates).

E-voting protocols under study

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, in: Foundations of Security, Protocols, and Equational Reasoning -Essays Dedicated to Catherine A. Meadows[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 | Prêt à Voter with Re-encryption Mixes[END_REF]. Some of the protocols (notably Helios, Belenios) can make use of homomorphic encryption, so that all encrypted votes can be summed before decryption. In our case study however, we only consider the mixnet version of these protocols, where ballots are instead mixed in a random order before decryption. Indeed, even if our reduction results apply in presence of homomorphic encryption, Proverif does not support the equations needed to define such a primitive.

Several versions of Helios. We consider several versions of the Helios protocol depending on whether the identity of the voter is part of the zero-knowledge proof (ZKP) or not [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF]. The original version of Helios is the one without the identity of the voter in the ZKP, which we described in our running example. Note that this protocol is subject to a replay attack, described in [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF], where the attacker submits, in the name of a dishonest voter, a copy of a honest voter's ballot, which lets him break that voter's privacy. We do indeed find this attack, even with two voters.

This attack can be mitigated in two ways. The first one consists in adding the voter's identity to the ZKP, preventing the attacker to replay it in his name. The second one is weeding, i.e. adding a mechanism allowing the server to remove duplicate ballots. However, this operation is only effective if we assume that the ballots emitted by honest voters correctly reach the ballot box. Indeed, the attacker can otherwise simply block the original ballot, and still break the privacy property without the server being able to detect the copy. In our communication model, we decided not to make such a strong assumption, and the attacker is thus able to block messages. herefore, in our framework, weeding is not a solution to prevent the replay attack mentioned above. We do not study this version of Helios, as the validity test with weeding does not fall in our framework described in Section 3, since we require that the validity test does not depend on the current content of the ballot box.

Note that the framework proposed in [START_REF] Arapinis | When are three voters enough for privacy properties?[END_REF] makes the assumption that the ballots meant to be counted for each honest voter (typically the last one emitted), which are the ones swapped to express the privacy property, reach the ballot box. Against that weaker attacker, Helios with weeding is secure, as long as voters only vote once. It is not, though, if they revote: the replay could be performed using a previous ballot, which the attacker is allowed to block. Their security analysis correctly finds Helios with weeding secure when revote is disallowed. However, due to a misunderstanding of the reduction result, a replication operator is missing in the case of revote, which leads to the attack being missed in that case.

Several versions of Belenios. The Belenios system [START_REF] Cortier | Belenios: A Simple Private and Verifiable Electronic Voting System, in: Foundations of Security, Protocols, and Equational Reasoning -Essays Dedicated to Catherine A. Meadows[END_REF] builds on Helios and relies on an additional authority who is in charge of distributing to each voter a key pair. The signature key is given to each voter, and the list of associated public keys constitutes the list of eligible voters. Recently, a variant of Belenios, BeleniosRF, designed to ensure receipt-freeness has been proposed [START_REF] Chaidos | BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme[END_REF]. It is based on a cryptographic primitive called signatures on randomizable ciphertexts. We also propose an analysis of BeleniosVS that has been designed to achieve both privacy and verifiability against a dishonest voting server [START_REF] Cortier | BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device[END_REF]. Civitas [START_REF] Juels | Coercion-Resistant Electronic Elections[END_REF][START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF]. This system relies on anonymous credential to enforce privacy. They consist of random values encrypted with the public key of the election authority. Comparison between credentials (e.g. the one used to cast a ballot and those composing the list of legitimate voters) is done relying on plaintext equivalence tests.

Prêt-à-Voter [START_REF] Ryan | Prêt à Voter with Re-encryption Mixes[END_REF]. The ballot contains a detachable list of candidate names, given in a random order (usually the left part), and their corresponding encryption in the same order on the right. Once the voter marked the candidate of his choice, he posts the encrypted part of the ballot (the right part) on the bulleting board. Then, the design of Prêt-à-Voter is similar to other voting systems.

Results

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. The encoding for modelling STV (5-bounded for 3 candidates) is more complex, with 6 voters and 5 ballots. We only model this counting function when considering an honest ballot box (with or without revote). In presence of a dishonest ballot box, the recovery process for 6 voters and 5 ballots will require several nested conditionals, and we anticipate that Proverif (or rather, the recent prototype developed to go beyond diff-equivalence, which is required to conclude on this case) will not be able to obtain results in less than 1 hour (the timeout we consider here).

We modelled the protocols briefly presented in Section 7.2 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. 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 setting3 ). 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. We also performed case studies considering a dishonest ballot box. In that case, our Proverif models are more complex, and we rely on a recent extension of the tool that goes beyond the notion of diff-equivalence [START_REF] Cheval | Indistinguishability Beyond Diff-Equivalence in ProVerif[END_REF]. Note that this extension of Proverif is a prototype, which is currently unable to exhibit attack traces. Therefore, in case the equivalence does not hold, the result returned is always "cannot be proved".

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

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 1h: 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. As expected, we find the attack on Helios from [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF].

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. We have shown how to extend it to produce a symbolic vote privacy notion against an untrusted ballot box in the symbolic model, and proved that our reduction results still hold in that setting.

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.

Vote privacy is considered a fundamental security property for electronic voting schemes. It is of course not the only desirable one: in particular, receipt-freeness and coercion-resistance can be seen as stronger variants of privacy, that require that an attacker should be unable to ascertain

Definition 2 .Example 5 .

 25 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. Continuing Example 4 with φ yes = {w 0 → pk(sk), w 1 → b id H

Figure 1 .Definition 3 .

 13 Figure 1. Semantics of our calculus

Figure 2 .

 2 Figure 2. Proof of Proposition 2 -Intermediate processes P i

  ) and C Rec (bb, bb ref ) should return the same result if bb ref and bb ref are equal up to id, ⊥, ⊥ 3 elements, and C Rec (bb, nil) must return bb.

Case 3 :

 3 tr contains all actions from phase 3, i.e. reaches the final output of the election result. Let us call R bb the recipe provided by the attacker in phase 3, and bb L = R bb φ L , bb R = R bb φ R the ballot boxes submitted on the left and right side. Let also bb ref,L , bb ref,R be the lists recording the (only) honest ballot on the left and on the right. With these notations, the election results output on each side arew tall φ L = count(extract(C Rec (bb L , bb ref,L )) and w tall φ R = count(extract(C Rec (bb R , bb ref,R ))).By construction of the election process, both ballot boxes pass the validity checks of C Valid . Thus, bb L and bb R are two lists of pairs id, b , where id is one of the voters' identities, and b a valid ballot for the credential output for id in phase 1. Moreover, the C Valid computation ensures that all identities in each list are distinct.By the same reasoning as in the honest ballot box case, the static non-equivalence of φ L and φ R necessarily comes from the result of the election:count(extract(C Rec (bb L , bb ref,L )) = count(extract(C Rec (bb R , bb ref,R ))).The two lists bb L , bb R have the same length -otherwise, checking their length instead of submitting them as input would let the attacker obtain a smaller non-equivalence witness. Thus, by assumption on C Rec , so do C Rec (bb L , bb ref,L ) and C Rec (bb R , bb ref,R ). Thus, by the k-boundedness assumption on count, there exists a sequence s of k k indices, such that count(extract(C Rec (bb L , bb ref,L )| s ) = count(extract(C Rec (bb R , bb ref,R )| s )) (recall that "l| s " denotes the list obtained by keeping only the elements of indices in s of a list l).

3 Example 13 .

 313 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. Let v = (a; b; c) and v = (a; c; b). We have

  r 1 ), . . . , w m → Vote(pk, id im , cr im , v m , r

m )} with votes v 1 , . . . , v n ∈ Votes, using distinct random values r 1 , . . . , r m ∈ N \ {sk, u 1 , . . . , u n }. Let φ denote φ 0 ∪ φ 1 . Consider recipes R 1 , R 2 , R 3 , R 4 on dom(φ)

. 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 R 1 , R 2 , R 3 , R 4 , Valid, C Tally . Then we have:

  • C Rec preserves the length of the list of ballots it is given: for all bb, bb ref , C Rec (bb, bb ref ) has the same length as bb; • C Rec is stable by sub-list: for any bb, bb ref , any sequence s of distinct integers in {1, . . . , length(bb)}, if we denote "•| s " the operation of keeping in a list only the elements at the positions indicated by the indices in s, then C Rec (bb| s , bb ref ) = C Rec (bb, bb ref )| s .

  Definition 9. A voting scheme is BPRIVD for p honest voters and n -p dishonest voters, written BPRIVD(p, n -p), if ElectionD L , 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 1. out(c n , cr n , pcr n ) | phase 3. TallyRecover(ch, sk)

	p,n-p ( #" v 1 , . . . , #" v n ) ≈ t ElectionD R p,n-p ( #" v 1 , . . . , #" v n ) where
	ElectionD X p,n-p ( #" v 1 , . . . , #" v n ) = new sk. m ref bb := nil. out(ch, pk(sk)).
	phase 1. out(c 1

  new sk. m ref 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 1.out(c n , cr n , pcr n ) | phase 3. TallyRecover(ch, sk)

  Indeed, in P i , P i+1 , that computation operates on a list bb ref,L , bb ref,R (read from m ref bb ), containing all honest ballots from #" v 1 , . . . , #" v p . In Q L (resp. Q R ), the list bb ref,L (resp. bb ref,R ) only contains the honest ballot for voter # " v i+1 . Let bb ref be the list obtained from bb ref,L , bb ref,R by removing the ballot for # "

Table 1

 1 Summary of our results. : Proverif proves the property. : Proverif finds an attack trace. ? Proverif answers "cannot be proved". : timeout ( 1h). 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)
			Helios (id in ZKP)		1s	∼ 24 min
		without revote	Helios (ZKP without id) Belenios BeleniosRF BeleniosVS		1s 1s ∼ 3s ∼ 3s	∼ 27 min ∼ 27 min
			Civitas		1s	∼ 39 min
			Prêt-à-Voter		1s
		revote	Helios (id in ZKP) Helios (ZKP without id)		1s 1s	∼ 23 min ∼ 42 min
			Belenios		1s	∼ 23 min
	dishonest	ballot box	Helios (id in ZKP) Helios (ZKP without id) Belenios	?	2s 3s 9s	------

This work received funding from the France

program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.* Corresponding author.

To keep the order of the list unchanged, which is required later on, we write C 0 Rec using a rev computation that reverses a list, which is straightforward to construct.

While Civitas does support revote, it uses rather complex mechanisms in that case to determine which ballot replaces which, that we chose not to model in our case study.

the voters' choice, even when they are willing, or coerced, to reveal their vote. Computational game-based definitions [30] as well as symbolic ones [3] have been proposed for these properties. They are however written in the same spirit as SWAP. Proposing formalisations in the style of BPRIV, and establishing similar reduction results to ours for these properties are open questions for future work.