Véronique Cortier
email: veronique.cortier@loria.fr

Joseph Lallemand
email: joseph.lallemand@loria.fr

Voting: You Can't Have Privacy without Individual Verifiability (Technical Report)

Electronic voting typically aims at two main security goals: vote privacy and verifiability. These two goals are often seen as antagonistic and some national agencies even impose a hierarchy between them: first privacy, and then verifiability as an additional feature. Verifiability typically includes individual verifiability (a voter can check that her ballot is counted); universal verifiability (anyone can check that the result corresponds to the published ballots); and eligibility verifiability (only legitimate voters may vote).

We show that actually, privacy implies individual verifiability. In other words, systems without individual verifiability cannot achieve privacy (under the same trust assumptions). To demonstrate the generality of our result, we show this implication in two different settings, namely cryptographic and symbolic models, for standard notions of privacy and individual verifiability. Our findings also highlight limitations in existing privacy definitions in cryptographic settings.

INTRODUCTION

Electronic voting is often seen as a convenient way for running elections as it allows voters to vote from any place. Moreover, it eases the tally and it can therefore often be used for non trivial counting procedures such as Single Transferable Vote or Condorcet. Numerous voting systems have been proposed so far, like Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF], Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF], Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF], Prêt-à-voter [START_REF] Ryan | Prêt à Voter with Paillier encryption[END_REF], or the protocols deployed in Estonia [START_REF] Heiberg | Improving the Verifiability of the Estonian Internet Voting Scheme[END_REF] or in Australia [START_REF] Brightwell | An overview of the iVote 2015 voting system[END_REF] to cite a few. On the other hand, many weaknesses or even attacks have been unveiled [START_REF] Springall | Security Analysis of the Estonian Internet Voting System[END_REF][START_REF] Wolchok | Security Analysis of India's Electronic Voting Machines[END_REF], from voting machines [START_REF] Gonggrijp | Studying the Nedap/Groenendaal ES3B Voting Computer: A Computer Security Perspective[END_REF] to Internet voting [START_REF] Wolchok | Attacking the Washington, D.C. Internet Voting System[END_REF].

In order to carefully analyse voting systems, security requirements have been defined. The two main security properties are:

• privacy: no one should know how I voted; • verifiability is typically described through the three following sub-properties.

individual verifiability: a voter can check that her ballot is counted; -universal verifiability: anyone can check that the results corresponds to the published ballots; -eligibility verifiability: only legitimate voters may vote. These two main properties seem antagonistic and an impossibility result has even been established between verifiability and unconditional privacy [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], that is, a notion of privacy that is independent of the power of the attacker.

The main contribution of this paper is to establish that, in fact, (computational) privacy implies individual verifiability, that is, guarantees that all the honest votes will be counted. This result holds for arbitrary primitives and voting protocols without anonymous channels. To show that this implication is not due to a choice of a very particular definition, we prove this implication in two very distinct contexts, namely symbolic and cryptographic models. In symbolic models, messages are represented by terms and the attacker's behaviour is typically axiomatised through a set of logical formulas or rewrite rules. Cryptographic models are more precise. They represent messages as bitstrings and consider attackers that can be any probabilistic polynomial time Turing machines. Proofs of security are made by reduction to well accepted security assumptions such as hardness of factorisation or discrete logarithm. In both models, we consider a standard notion of privacy, already used to analyse several protocols. In both cases, we establish that privacy implies individual verifiability for a (standard) basic notion of individual verifiability, namely that the result of the election must contain the votes of all honest voters.

We now describe the main idea of the result. Actually, we show the contrapositive implication: if there is an attack against individual verifiability, then there is an attack against privacy. To explain the idea, let's consider a very simple protocol, not at all verifiable. In this simple protocol, voters simply encrypt their votes with the public key of the election. The ballot box stores the ballots and, at the end of the election, it provides the list of recorded ballots to the talliers, who detain the private key, possibly split in shares. The talliers compute and publish the result of the election. The ballot box is not public and no proof of correct decryption is provided so voters have no control over the correctness of the result. Such a system is of course not satisfactory but it is often viewed as a "basic" system that can be used in contexts where only privacy is a concern. Indeed, it is typically believed that such a system guarantees privacy provided that the attacker does not have access to the private key of the election. In particular, the ballot box (that is, the voting server) seems powerless. This is actually not the case. If the ballot box aims at knowing how a particular voter, say Alice, voted, he may simply keep Alice's ballot in the list of recorded ballots and then replace all the other ballots by encryptions of valid votes of his choice, possibly following a plausible distribution, to make the attack undetected. When the result of the election is published, the ballot box will know all the votes but Alice's vote, and will therefore be able to deduce how Alice voted.

One may argue that such an attack is not realistic: the ballot box needs to be able to change all ballots but one. Note however that elections are often split in many small voting stations (sometimes as small as 20 voters in total [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF]). Therefore changing a few ballots can be sufficient to learn how Alice voted. Maybe more importantly, this attack highlights the fact that it is not possible to require privacy without verifiability as sometimes specified by national agencies. For example, in France, only privacy is required [START_REF]octobre 2010 portant adoption d'une recommandation relative à la sécurité des systèmes de vote électronique[END_REF]. In Switzerland, privacy is a pre-requisite and the level of verifiability depend on the percentage of voters that can vote electronically [START_REF]Ordonnance de la ChF sur le vote électronique (OVotE) du 13 décembre 2013[END_REF]. Our findings point out that if voters cannot trust some authorities w.r.t. the fact that their vote will be counted they cannot trust the same authorities w.r.t. their privacy, even for entities that do not have access to the secret keys. Beyond the attack explained on a simple (and naive) protocol, our proof that privacy implies individual verifiability shows that as soon as a protocol is not verifiable, then the adversary can take advantage of the fact that he may modify a vote without being detected in order to break privacy. Individual verifiability is only one part of verifiability. It does not account for universal nor eligibility verifiability. So our result cannot be used to conclude that a private voting scheme ensures all desirable verifiability properties. Instead, it demonstrates that there is no hope to design a private voting system if it does not include some degree of verifiability, namely individual verifiability at least.

Our results also emphasise issues in existing privacy definitions. Indeed, if privacy implies individual verifiability, how is it possible to prove Helios [START_REF] Bernhard | How Not to Prove Yourself: Pitfalls of the Fiat-Shamir Heuristic and Applications to Helios[END_REF] or Civitas [START_REF] Backes | Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-Calculus[END_REF] without even modelling the verification aspects? How can a system that is not fully verifiable like the Neuchâtel protocol be proved private [START_REF] Galindo | 2015 Neuchâtel's Castas-Intended Verification Mechanism[END_REF]? As already pointed out in [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF], existing cryptographic definitions of privacy (see [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] for a survey) implicitly assume an honest voting ballot box: honest ballots are assumed to be properly stored and then tallied. Actually, we notice that the same situation occurs in symbolic models. Although the well adopted definition of privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] does not specify how the ballot box should be modelled, most symbolic proofs of privacy (see 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] Cortier | A formal analysis of the Norwegian E-voting protocol[END_REF][START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF]) actually assume that the votes of honest voters always reach the ballot box without being modified and that they are properly tallied. The reason is that the authors were aware of the fact that if the adversary may block all ballots but Alice's ballot, he can obviously break privacy. However, to avoid this apparently systematic attack, they make a very strong assumption: the ballot box needs to be honest. This means that previous cryptographic and symbolic privacy analyses only hold assuming an honest ballot box while the corresponding voting systems aim at privacy without trusting the ballot box. This seriously weakens the security analysis and attacks may be missed, like the attack of P. Roenne [START_REF] Roenne | [END_REF] on Helios, for which there is no easy fix.

Why is it so hard to define vote privacy w.r.t. a dishonest ballot box? Intuitively, vote privacy tries to capture the idea that, no matter how voters vote, the attacker should not be able to see any difference. The key issue is that the result of the election does leak some information (typically the sum of the votes) and the adversary may notice a difference based on this. This particularity makes vote privacy differ from privacy in other contexts, where the adversary really should learn no information. Therefore, most definitions of vote privacy (roughly) say that, no matter how honest voters voted, provided that the aggregation of the corresponding votes remains the same, then the attacker should not see any difference. However, as soon as the ballot box is dishonest, it may discard some honest ballots and break privacy, as already discussed. The first definition of privacy w.r.t. a dishonest ballot box [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] weakens privacy by requiring that among the ballots that are ready to be tallied, the (sub-)tally of the honest ones does not change. This preliminary definition has two limitations. First, it assumes that the tallied ballots are exactly the same as the cast ones, which is not the case of all protocols (e.g. in ThreeBallots [START_REF] Rivest | Three Voting Protocols: ThreeBallot, VAV and Twin[END_REF], only a part of the ballot is published; in BeleniosRF [START_REF] Chaidos | BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme[END_REF], ballots are re-randomised). Second, it does not model re-voting: the tally process cannot discard ballots due to some revote policy.

We propose here another approach. Instead of changing the privacy definition, we now include a model of the verification process: the ballots should be tallied only if the honest voters have successfully performed the tests specified by the protocol. We compare our definition with [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] and an original definition of privacy [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF] on a selection of well-studied protocols, that have different levels of verifiability (Helios, Civitas, Belenios, Neuchâtel, and our simplenon verifiable -protocol). We show again that our notion of privacy, w.r.t. a dishonest ballot box, implies individual verifiability. We do not consider our new definition of privacy as final but it opens the way to a better understanding of privacy in the context of fully dishonest authorities.

Threat model. We show that privacy implies individual verifiability, under the same trust assumptions, that is, trusting the same group of authorities, channels, etc. In symbolic models, the privacy definition does not make prior assumptions on the threat model. Instead, the encoding of the protocol defines which parties are trusted. In particular, as already discussed, existing proofs of privacy [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] Cortier | A formal analysis of the Norwegian E-voting protocol[END_REF][START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] often implicitly assume that honest ballots reach the ballot box without any modification. We show that whenever privacy holds then individual verifiability holds, for the same encoding, hence the same assumptions. In contrast, most cryptographic definitions of privacy implicitly assume an honest ballot box. Therefore, we first show that privacy implies individual verifiability, assuming an honest ballot box, considering the standard definition of privacy by Benaloh [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]. Then we show that privacy still implies individual verifiability, assuming a dishonest ballot box, considering our novel definition of privacy, that explicitly models the verification steps.

Related work. As already mentioned, [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] shows an impossibility result between universal verifiability and unconditional privacy. We show in contrast that the commonly used (computational) definitions of privacy actually imply verifiability. The discrepancy between the two results comes from the fact that [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] considers unconditional privacy while most protocols achieve only computational privacy, that is against a polynomially bounded adversary. Interestingly, the impossibility result still holds between unconditional privacy and our notion of individual verifiability. [START_REF] Delaune | Coercion-Resistance and Receipt-Freeness in Electronic Voting[END_REF] establishes a hierarchy between privacy, receipt-freeness, and coercion resistance, while in a quantitative setting, [START_REF] Küsters | Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study[END_REF] shows that this hierarchy does not hold anymore. [START_REF] Cortier | SoK: Verifiability Notions for E-Voting Protocols[END_REF] recasts several definition of verifiability in a common setting, providing a framework to compare them. Besides [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], none of these approaches relates privacy with verifiability. Many privacy definitions have been proposed as surveyed in [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. However, they all assume an honest ballot box. To our knowledge, [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is the only exception, as already discussed in details. [START_REF] Cortier | Attacking and fixing Helios: An analysis of ballot secrecy[END_REF] shows how to break privacy by replaying a ballot. If an attacker may replay Alice's ballot and cast it in his own name (or cast a related ballot), then he introduces a bias in the result, that leaks some information on Alice's vote. Note that this replay attack does not break individual verifiability: honest votes are correctly counted. We show here another breach for privacy: if an attacker may remove some honest votes, then he breaks privacy as well.

Roadmap. We first prove that privacy implies individual verifiability in symbolic models, in Section 3, and then in cryptographic models, in Section 4. These two parts are rather independent. In Section 6, we examine a selection of well-studied voting protocols and compare the effect of different (cryptographic) notions of privacy when the ballot box is dishonest.

PRELIMINARIES

Notations: The multiset of elements a, a, b, c is denoted {|a, a, b, c | }. The union of two multisets S 1 and S 2 is denoted S 1 ⊎ S 2 .

In both cryptographic and symbolic models, we assume a set V of votes and a set R of possible results, equipped with an associative and commutative operator * (e.g. addition of vectors). A counting function is a function ρ that associates a result r ∈ R to a multiset of votes. We assume that counting functions have a partial tally property: it is always possible to count the votes in two distinct multisets and then combine the results.

∀V , V ′ ρ(V ⊎ V ′ ) = ρ(V ) * ρ(V ′ ) A vote v is said to be neutral if ρ(v) is neutral w.r.t. * . Example 2.1. Consider a finite set of candidates C = {a 1 , . . . , a k }.
In case voters should select between k 1 and k 2 candidates or vote blank, we can represent valid votes by vectors representing the selection of candidates

V k 1 ,k 2 = v ∈ {0, 1} k | k 1 ≤ k i=0 v i ≤ k 2 ∪ {v blank }
where v blank is the null vector (0, . . . , 0), representing a blank vote. In a mixnet-based tally, all the individual votes are revealed. Thus R is the set of multisets of votes in V k 1 ,k 2 and * is the union of multisets. The corresponding counting function is

ρ mix (V ) = V , where V is a multiset of elements of V k 1 ,k 2 .
In an homomorphic-based tally, the votes are added together. Thus R = N k , the set of vectors of k elements, and * is the addition of vectors. The corresponding counting function is

ρ hom (V ) = v ∈V v.
Both ρ mix and ρ hom have the partial tally property. The vote v blank is a neutral vote w.r.t. ρ hom but not ρ mix .

The result of the election r may have several representations. For example, a multiset may be represented by several lists (where the order changes). In symbolic models, the result will be represented by abstract terms and we wish our result to be independent of a particular choice of representation. Therefore, we will simply say that a representation R is a function that associates to a result r ∈ R a set of possible representations with an injectivity property:

∀r r ′ . R(r ) ∩ R(r ′ ) = ∅
Intuitively, a result can be associated to several representations but a given representation can correspond to at most one result.

For our proofs in a cryptographic setting, we will also assume that given an election result r and a set of votes V , one can decide efficiently (in polynomial time) whether r includes all the votes of V , that is, whether there exists V ′ such that r = ρ(V ⊎ V ′ ). This condition is satisfied by ρ mix and ρ hom and all standard counting functions.

SYMBOLIC MODEL 3.1 Model

In symbolic models, security protocols are often modelled through a process algebra, in the spirit of the applied pi-calculus [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF], that offers a small, abstract language for specifying communications, where messages are represented as terms. We present here a calculus inspired from the calculus underlying the ProVerif tool [START_REF] Blanchet | Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif[END_REF].

3.1.1 Terms. We consider an infinite set of names N that model fresh values such as nonces and keys. We distinguish the set FN of free nonces (generated by the attacker) and the set BN of bound nonces (generated by the protocol agents). We also assume an infinite set of variables V = X ⊎ AX where X contains variables used in processes (agent's memory) while AX contains variables used to store messages (adversary's memory). Cryptographic primitives are represented through a set of function symbols, called signature F . Each function symbol has an arity, that is, the number of its arguments. We assume an infinite set C ⊆ F of public constants, which are functions of arity 0.

Example 3.1. The standard primitives, public keys, symmetric and asymmetric encryption, concatenation, as well as addition, can be modelled by the following signature.

F c = {pk/1, enc/2, aenc/2, ⟨•, •⟩/2, +/2}
The companion primitives (symmetric and asymmetric decryption, projections) are then represented by the following signature:

F d = {dec/2, adec/2, π 1 /1, π 2 /1}
Given a signature F , a set of names N , a set of variables V, the set of terms T (F , V, N ) is the set inductively defined by applying functions to variables in V and names in N . The set of names resp. variables) occurring in t is denoted names(t) (resp. vars(t)). A term is ground if it does not contain any variable. The set of terms T (F , AX, FN ) represents the attacker terms, that is, terms built from the messages sent on the network and stored thanks to the variables in AX.

A

substitution σ = {M 1 /x 1 , . . . , M k /x k } maps variables x 1 , . . . , x k ∈ V to messages M 1 , . . . , M k . Its domain is denoted dom(σ ) = {x 1 , . . . , x k }.
The application of σ to a term t is denoted tσ and is defined as usual. A substitution σ is ground if its messages M 1 , . . . , M k are ground.

The properties of the cryptographic primitives are modelled through an equational theory E, which is a finite set of equations of the form M = N where M, N ∈ T (F , X, ∅) are messages without names. Equality modulo E, denoted by = E , is defined as the smallest equivalence relation on terms that is closed under context and substitution. We denote disequalities modulo E by M E N .

Example 3.2. Considering the signature F c ∪ F d ∪ C from Example 3.1, the following equational theory describes the ability to decrypt symmetrically, asymmetrically, and to project pairs. It also Processes:

P, Q ::= 0 | ν n.P for n ∈ BN (n bound in P) | out(c, M).P | in(c, x).P for x ∈ X (x bound in P) | event(M 1 , . . . , M n ).P for event ∈ Ev of arity n | P | Q | let x = M in P for x ∈ X (x bound in P) | if M = N then P else Q | !P
where M, N , M 1 , . . . , M n are messages and c ∈ Ch is a channel. characterises + as an associative and commutative operator.

dec(enc(x, y), y) = x adec(aenc(x, pk(y)), y) = x π 1 (⟨x, y⟩) = x π 2 (⟨x, y⟩) = y x + (y + z) = (x + y) + z x + y = y + x 3.1.2
Processes. The behaviour of protocol parties is described through processes. Let Ch be an infinite set of channel names, representing the channels on which the messages are exchanged. All channels will be public. We consider different channels nevertheless to model the fact that an attacker can identify the provenance of a message. We also consider a finite set Ev of event symbols, given together with their arity. Events are used to record that participants have reached a certain step, with some associated knowledge. Protocols are modelled through a process algebra, whose syntax is displayed in Figure 1.

As usual, we identify processes up to α-renaming, to avoid capture of bound names and variables.

A configuration of the system is a triple (E; P; ϕ) where:

• P is a multiset of processes that represents the current active processes; • E is a set of names, which represents the private names of the processes; • ϕ is a substitution with dom(ϕ) ⊆ AX that represents the messages sent on the network. We assume ϕ to be ground, that is for any x ∈ dom(ϕ), ϕ(x) is a ground term.

The semantics of processes is given through a transition relation α --→ provided in Figure 2, where α is the action associated to the transition. τ denotes a silent action. Events are recorded but will be invisible to the attacker. Intuitively, process ν n.P creates a fresh nonce, stored in E, and behaves like P. Process out(c, M).P emits M on c and behaves like P. Process in(c, x).P inputs a term computed by the attacker (that is a term built from ϕ using an attacker term) on channel c and then behaves like P. Process event(M 1 , . . . , M n ).P triggers the event event(M 1 , . . . , M n ), and then behaves like P. Process P | Q corresponds to the parallel composition of P and Q.

Process let x = M in P behaves like P in which x is replaced with M. Process if M = N then P else Q behaves like P if M and N are equal modulo E, and behaves like Q otherwise. The replicated process !P behaves as an unbounded number of copies of P.

We denote by w ---→ * the reflexive transitive closure of α --→, where w is the concatenation of all actions. We also write equality up to silent actions and events = τ .

A trace of a process P is any possible sequence of transitions starting from P. Traces correspond to all possible executions in the presence of an attacker that may read, forge, and send messages. Formally, the set of traces trace(P) is defined as follows.

trace(P) = {(w, new E.ϕ)|(∅; {P }; ∅) w ---→ * (E; P; ϕ)}
A sequence of actions t is blocking in a process P if it cannot be executed. Example 3.3. Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] is a simple voting protocol used in several elections, like the election of the recteur of the university of Louvainla-Neuve. A voter simply encrypts her vote with the public key of the election. This encrypted vote forms the ballot, which is sent to the ballot box. The voter may check that her ballot is on the ballot box since the ballot box is public. There are two ways for tallying, either homomorphic tally or mixnet-based tally. We model here the two options in an abstract way: given the ballots, the talliers output the aggregation of the decryption of the ballot. This aggregation could be the addition or just the votes in a random order. For simplicity, we describe here a simple version with only two honest voters A and B, a dishonest voter C, and a voting server S. This protocol can be modelled by the following process.

blocking(t, P)

P Helios (v a , v b ) = ν k as , k bs , k cs , k e . (out(c, k cs ).out(c, pk(k e )) | Voter(A, v a , c a , c ′ a , k as , k e ) | Voter(B, v b , c b , c ′ b , k bs , k e ) | Tally Helios (c a , c b , c c , c s , k as , k bs , k cs , k e ))
where Voter(a, v, c, c ′ , k, k e ) represents voter a willing to vote for v using the channels c and c ′ , the election key k e and the credential k to authenticate to the server, while Tally Helios represents the voting server.

Voter(a, v, c, c ′ , k, k e ) simply sends an encrypted vote. To model the fact that voters communicate with the ballot box through an authenticated channel, we assume that a voter first sends her ballot privately to the server (using the encryption with k) and then sends the ballot on a public channel. Note that the key k is just a modelling artefact to abstract away the underlying password-based authenticated channel.

Voter(a, v, c, c ′ , k, k e ) = ν r . out(c, enc(aenc(⟨v, r ⟩, pk(k e )), k)). Voted(a, v). out(c ′ , aenc(⟨v, r ⟩, pk(k e )))

The voting server receives ballots from voters A, B, and C and then outputs the decrypted ballots, after some mixing, modelled -------→ (E; {P[Rϕ/x]} ∪ P; ϕ) In if R is an attacker term such that vars(R) ⊆ dom(ϕ)

(E; {P 1 | P 2 } ∪ P; ϕ) τ --→ (E;
(E; {event(M 1 , . . . , M n ).P } ∪ P; ϕ) event(M 1 , ..., M n ) ----------------→ (E; {P } ∪ P; ϕ) Event if ∀i. M i is a ground message (E; {let x = M in P } ∪ P; ϕ) τ --→ (E; {P[M/x]} ∪ P; ϕ) Let-In if M is ground (E; {if M = N then P else Q } ∪ P; ϕ) τ --→ (E; {P } ∪ P; ϕ) If-Then if M, N are ground messages such that M = E N (E; {if M = N then P else Q } ∪ P; ϕ) τ --→ (E; {Q } ∪ P; ϕ) If-Else if M, N are ground messages such that M E N (E; {!P } ∪ P; ϕ) τ --→ (E; {P, !P } ∪ P; ϕ) Repl
Tally Helios (c a , c b , c c , c s , k as , k bs , k cs , k e ) = in(c a , x 1 ).in(c b , x 2 ).in(c c , x 3 ). let y 1 = dec(x 1 , k as ) in let y 2 = dec(x 2 , k bs ) in let y 3 = dec(x 3 , k cs ) in if x 1 x 2 ∧ x 1 x 3 ∧ x 2 x 3 then out(c s , π 1 (adec(y 1 , k e )) + π 1 (adec(y 2 , k e )) + π 1 (adec(y 3 , k e )))
where we omit the null else-branches. ∧ is syntactic sugar for a succession of tests and if M N then P is syntactic sugar for if M = N then 0 else P.

3.1.3 Equivalence. Sent messages are stored in a substitution ϕ while private names are stored in E. A frame is simply an expression of the form new E.ϕ where dom(ϕ) ⊆ AX. It represents the knowledge of an attacker. We define dom(new E.ϕ) as dom(ϕ).

Intuitively, two sequences of messages are indistinguishable to an attacker if he cannot perform any test that could distinguish them. This is typically modelled as static equivalence [START_REF] Abadi | Mobile Values, New Names, and Secure Communication[END_REF]. Definition 3.4 (Static Equivalence). Two ground frames new E.ϕ and new E ′ .ϕ ′ are statically equivalent if and only if they have the same domain, and for all attacker terms R, S with variables in dom(ϕ) = dom(ϕ ′ ), we have

(Rϕ = E Sϕ) ⇐⇒ (Rϕ ′ = E Sϕ ′ )
Two processes P and Q are in equivalence if no matter how the adversary interacts with P, a similar interaction may happen with Q, with equivalent resulting frames. Definition 3.5 (Trace Equivalence). Let P, Q be two processes. We write P ⊑ t Q if for all (s,ψ ) ∈ trace(P), there exists (s ′ ,ψ ′ ) ∈ trace(Q) such that s = τ s ′ and ψ and ψ ′ are statically equivalent. We say that P and Q are trace equivalent, and we write

P ≈ t Q, if P ⊑ t Q and Q ⊑ t P.
Note that this definition already includes the attacker's behaviour, since processes may input any message forged by the attacker.

Example 3.6. Ballot privacy is typically modelled as an equivalence property [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] that requires that an attacker cannot distinguish when Alice is voting 0 and Bob is voting 1 from the scenario where the two votes are swapped.

Continuing Example 3.3, ballot privacy of Helios can be expressed as follows: P Helios (0, 1) ≈ t P Helios (1, 0)

Voting protocols

We consider two disjoint, infinite subsets of C: a set A of agent names or identities, and a set V of votes. We assume given a representation R of the result.

A voting protocol is modelled as a process. It is composed of:

• processes that represent honest voters;

• a process modelling the tally;

• possibly other processes, modelling other authorities. Formally, we define a voting process as follows.

Definition 3.7. A voting process is a process of the form

P = ν # " cred.ν cred 1 . . . ν cred p . ( Voter(a 1 , v a 1 , #" c 1 , # " cred, cred 1 ) | • • • | Voter(a n , v a n , #" c n , # " cred, cred n ) | Tally p ( #" c , # " cred, cred 1 , . . . , cred p ) | Others p ( #" c ′ , # " cred, cred 1 , . . . , cred p ))
where

a i ∈ A, v a i ∈ V, #" c i , #" c , #" c ′ are (distinct) channels, # "
cred and cred i are (distinct) names.

A voting process may be instantiated by various voters and vote selections. Given A = {b 1 , . . . , b n } ⊆ A a finite set of voters, and α : A → V that associates a vote to each voter, we define P α by replacing a i by b i and v i by α(b i ) in P.

Moreover, P must satisfy the following properties.

• Process Voter(a, v a , #" c , # " cred, cred) models an honest voter a willing to vote for v a , using the channels #" c , credentials cred (e.g. a signing key) and election credentials # " cred. It is assumed to contain an event Voted(a, v) that models that a has voted for v. This event is typically placed at the end of process Voter(a, v a , #" c , # " cred, cred). This event cannot appear in process Tally p nor Others p .

• Process Tally p ( #" c , # " cred, cred 1 , . . . , cred p ) models the tally. It is parametrised by the total number of voters p (honest and dishonest), with p ≥ n. It is assumed to contain exactly one output action on a reserved channel c r . The term output on this channel is assumed to represent the final result of the election.

∀α . ∀(tr , ϕ) ∈ trace(P α ). out(c r , r ) ∈ tr ⇒ ∃V . ϕ(r ) ∈ R(ρ(V ))
Tally p may of course contain input/output actions on other channels.

• Process Others p ( #" c ′ , # " cred, cred 1 , . . . , cred p ) is an arbitrary process, also parametrised by p. It models the remaining of the voting protocol, for example the behaviour of other authorities. It also models the initial knowledge of the attacker by sending appropriate data (e.g. the public key of the election or dishonest credentials). We simply assume that it uses a set of channels disjoint from the channels used in Voter and Tally p .

The channel c r used in Tally p to publish the result is called the result channel of P.

Example 3.8. The process modelling the Helios protocol, as defined in Example 3.3 is a voting process, where process Others p consists in the output of the keys: out(c, k cs ).out(c, pk(k e )).

We can read which voters voted from a trace. Formally, given a sequence tr of actions, the set of voters Voters(tr ) who did vote in tr is defined as follows.

Voters(tr ) = {a ∈ A | ∃v ∈ V. Voted(a, v) ∈ tr }.
The result of the election is emitted on a special channel c r . It should correspond to the tally of a multiset of votes. Formally, given a trace (t, ϕ) and a multiset of votes V , the predicate result(t, ϕ, V )

holds if the election result in (t, ϕ) corresponds to V . result(t, ϕ, V ) def = ∃x, t ′ . t = t ′ .out(c r , x) ∧ ϕ(x) ∈ R(ρ(V )).

Security properties

Several definitions of verifiability have been proposed. In the lines of [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF][START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF], we consider a very basic notion, that says that the result should at least contain the votes from honest voters. Definition 3.9 (symbolic individual verifiability). Let P be a voting process with result channel c r . P satisfies symbolic individual verifiability if, for any trace (t, ϕ) ∈ trace(P α ) of the form t ′ .out(c r , x)), there exists V c such that the result in t corresponds to

V a ⊎ V c , that is result(t, ϕ, V a ⊎ V c ), where V a = {|v | ∃a. Voted(a, v) ∈ t | }
Individual verifiability typically guarantees that voters can check that their ballot will be counted. Our notion of individual verifiability goes one step further, ensuring that the corresponding votes will appear in the result, even if the tally is dishonest. One of the first definitions of verifiability was given in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF], distinguishing between individual, universal, and eligibility verifiability. Intuitively, our own notion of individual verifiability sits somewhere between individual verifiability and individual plus universal verifiability as defined in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF]. A precise comparison is difficult as individual and universal verifiability are strongly tight together in [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF]. Moreover, [START_REF] Kremer | Election verifiability in electronic voting protocols[END_REF] only considers the case where all voters are honest and they all vote.

We consider the privacy definition proposed in [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF] and widely adopted in symbolic models: an attacker cannot distinguish when Alice is voting v 1 and Bob is voting v 1 from the scenario where the two votes are swapped. Definition 3.10 (Privacy [START_REF] Delaune | Verifying Privacytype Properties of Electronic Voting Protocols[END_REF]). Let P be a voting process. P satisfies privacy if, for any subtitution α from voters to votes, for any two voters a, b ∈ A\dom(α) and any two votes v 1 , v 2 ∈ V, we have

P α ∪{a →v 1 ,b →v 2 } ≈ P α ∪{a →v 2 ,b →v 1 }

Privacy implies verifiability

We show that privacy implies verifiability under a couple of assumptions, typically satisfied in practice.

First, we assume a light form of determinacy: two traces with the same observable actions yield the same election result. This excludes for example cases for voters chose non deterministically how they vote. Formally, we say that a voting process P with election channel c r is election determinate if, for any substitution α from voters to votes, for any two traces t, t ′ such that t = τ t ′ , (t .out(c r , x), ϕ) ∈ trace(P α ), and (t ′ .out(c r , x), ϕ ′ ) ∈ trace(P α ), then

ϕ(x) ∈ R(ρ(V ))) ⇒ ϕ ′ (x) ∈ R(ρ(V ))
This assumption still supports some form of non determinism but may not hold for example in the case where voters use anonymous channels that even hide who participated in the election.

Second, we assume that it is always possible for a new voter to vote (before the tally started) without modifying the behaviour of the protocol.

Formally, a voting proces P is voting friendly if for all voter a ∈ A, there exists t ′′ (the honest voting trace) such that for all α satisfying a dom(α),

• for all (t, ϕ) ∈ trace(P α ), such that t = t ′ .out(c r , x) for some t ′ , x, for all v, there exists tr , ψ such that tr

= τ t ′′ , Voted(a, v) ∈ tr , (t ′ .tr .out(c r , x),ψ ) ∈ trace(P α ∪{a →v } ), and
∀V . ϕ(x) ∈ R(ρ(V )) ⇒ ψ (x) ∈ R(ρ(V ∪{v})).
Intuitively, if a votes normally, her vote will be counted as expected, no matter how the adversary interfered with the other voters. • for all t ′ , x such that blocking(t ′ .out(c r , x), P α ), for all v, tr , ψ such that tr = τ t ′′ , we have blocking(t ′ .tr .out(c r , x), P α ∪{a →v } ). Intuitively, the fact that a voted does not suddenly unlock the tally. In practice, most voting systems are voting friendly since voters vote independently. In particular, process P Helios modelling Helios, as defined in Example 3.3, is voting friendly (assuming an honest tally). The voting friendly property prevents a fully dishonest tally since the first item requires that unmodified honest ballots are correctly counted. However, we can still consider a partially dishonest tally that, for example, discards or modifies ballots that have been flagged by the attacker.

Moreover, we assume that there exists a neutral vote, which is often the case in practice. Actually, this is a simplified (sufficient) condition. Our result also holds as soon as there is a vote that can be counted separately from the other votes (as formally defined in appendix). Theorem 3.11 (Privacy implies individual verifiability). Let P be a voting friendly, election determinate voting process.

If P satisfies privacy then P satisfies individual verifiability.

The proof of this result intuitively relies on the fact that in order to satisfy privacy w.r.t. two voters Alice and Bob, a voting process has to guarantee that the vote of Alice is, if not correctly counted, at least taken into account to some extent. Indeed, if an attacker, trying to distinguish whether Alice voted for 0 and Bob for 1, or Alice voted for 1 and Bob for 0, is able to make the tally ignore completely the vote of Alice, the result of the election is then Bob's choice. Hence the attacker learns how Bob voted, which breaks privacy.

Therefore, we first we prove that if a protocol satisfies privacy, then if we compare an execution (i.e. a trace) where Alice votes 0 with the corresponding execution where Alice votes 1, the resulting election results must differ by exactly a vote for 0 and a vote for 1. Formally, we show the following property. Lemma 3.12. If a voting friendly, election determinate voting process P satisfies privacy, then it satisfies

[ t = τ t ′ ∧ (t, ϕ) ∈ trace(P α ∪{a →v 1 } ) ∧ (t ′ , ϕ ′ ) ∈ trace(P α ∪{a →v 2 } ) ∧ result(t, ϕ, V ) ∧ result(t ′ , ϕ ′ , V ′ ) ] =⇒ ρ(V ′ ⊎ {|v 1 | }) = ρ(V ⊎ {|v 2 | }).
This lemma is used as a central property to prove the theorem. Intuitively, we apply this lemma repeatedly, changing one by one all the votes from honest voters into neutral votes. Let r denote the result before this operation, and r ′ the result after. Let V a denote the multiset of honest votes, and V b the multiset containing the same number of neutral votes. Thanks to Lemma 3.12, we can show that r * ρ(V b ) = r ′ * ρ(V a ). Since V b only contains neutral votes, we have r = r ′ * ρ(V a ). This means that r contains all honest votes, hence the voting process satisfies individual verifiability.

The detailed proof of this theorem can be found in appendix.

COMPUTATIONAL MODEL

Computational models define protocols and adversaries as probabilistic polynomial-time algorithms. Notation: We may write (id, * ) ∈ L as a shorthand, meaning that there exists an element of the form

(id, x) in L. If V is a multiset of elements of the form (id, v), we define ρ(V ) = ρ({|v | (id, v) ∈ V | }).

Voting system

We assume that the ballot box displays a board BB, that is a list of ballots. The nature of the ballots depend on the protocol we consider. • Setup(1 λ ), given a security parameter λ, returns a pair of election keys (pk, sk). • Credential(1 λ , id) creates a credential cred for voter id, for example a signing key. The credential may be empty as well.

Registered voters are stored in a list U. • Vote(id, cred, pk, v) constructs a ballot containing the vote v for voter id with credential cred, using the election public key pk. • VerifVoter(id, cred, L, BB) checks whether the local knowledge L of voter id is consistent with the board BB. For example, a voter may check that her (last) ballot appears on the bulletin board. • Tally(BB, sk, U) computes the tally of the ballots on the board BB, using the election secret key sk, assuming a list of registered voter identities and credentials U. The Tally algorithm first runs some test ValidTally(BB, sk, U) that typically checks that the ballots of BB are valid. Tally may return ⊥ if the tally procedure fails (invalid board or decryption failure for example). If Tally(BB, sk, U) ⊥ then it must correspond to a valid result, that is, there exists V such that Tally(BB, sk, U) = ρ(V ). • Valid(id, b, BB, pk) checks that a ballot b cast by a voter id is valid with respect to the board BB using the election public key pk. For example, the ballot b should have a valid signature or valid proofs of knowledge. The ballot b will be added to BB only if Valid(id, b, BB, pk) succeeds.

We will always assume a correct voting scheme, that is, tallying honestly generated ballots yields the expected result. Formally, for all distinct identities U = id 1 , . . . , id n , and credentials cred 1 , . . . , cred n , for all votes v 1 , . . . , v n , for all election keys (pk, sk),

if BB = [Vote(id i , cred i , pk, v i )|i ∈ 1, n ], then Tally(BB, sk, U) = ρ({|v 1 , . . . , v n | })
The tally algorithm typically applies a revote policy. Indeed, if voters may vote several times, the revote policy states which vote should be counted. The two main standard revote policies are 1. the last vote counts or 2. the first vote counts (typically when revote is forbidden). In what follows, our definitions are written assuming the last ballot revote policy. However, they can easily be adapted to the first ballot revote policy and all our results hold in both cases (as shown in appendix).

The revote policy is either based on the identities or the credentials. We say that a voting system is id-based if there exists a a function open id which, given a ballot b, retrieves the associated identity. Formally, for any id, cred, pk, v,

open id (Vote(id, cred, pk, v)) = id
Similarly, we say that a voting system is cred-based if there exists a function open cred which, given a ballot b, the election secret key sk, and a list U of registered voters and credentials, retrieves the credential cred used by the voter to create the ballot. Formally, for any id, cred, sk, pk, v,

open cred (Vote(id, cred, pk, v), sk, U ) = cred O reg (id) if (id, * ) ∈ U then stop else cred id ← Credential(1 λ , id) U ← U ∥(id, cred id ) O corr (id) if (id, * ) U ∨ (id, * ) ∈ CU then stop else CU ← CU ∥(id, cred id ) return cred id
where (id, cred id ) ∈ U Note that some schemes are neither id-based nor cred-based, in particular when the ballots contain no identifier. Such schemes typically assume that voters do not revote since there is no means to identify whether two ballots originate from the same voter.

Security properties

As usual, an adversary is any probabilistic polynomial time Turing machine (PPTM). We define verifiability and privacy through gamebased properties.

Verifiability.

For verifiability, we propose a simple definition, inspired from [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF][START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF]. Intuitively, we require that the election result contains at least the votes of all honest voters. This notion was called weak verifiability in [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] but we will call it individual verifiability to match the terminology used in symbolic settings. More sophisticated and demanding definitions have been proposed, for example controlling how many dishonest votes can be inserted [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] or tolerating some variations in the result [START_REF] Küsters | Accountabiliy: Definition and Relationship to Verifiability[END_REF]. The main missing part (in terms of security) is that our definition does not control ballot stuffing: arbitrarily many dishonest votes may be added to the result. The reason is that ballot stuffing seems unrelated to privacy. Moreover, our definition assumes an honest tally, and thus does not capture universal verifiability aspects. The main reason is that existing privacy definitions in computational settings assume an honest tally and we compare the two notions under the same trust assumptions. We leave as future work to determine how to extend these two definitions to a dishonest tally, and whether the implication still holds.

Verifiability is defined through the game Exp verif A (λ) displayed on Figure 4. In a first step, the adversary may use oracles O reg (id) and O corr (id) (defined on Figure 3) to respectively register a voter and get her credential (in this case, the voter is said to be corrupted). Then the adversary may ask an honest voter id to vote for a given vote v through oracle O v vote (id, v). In this case, the adversary sees the corresponding ballot and the fact that id voted for v is registered in the list Voted. The adversary may also cast an arbitrary ballot b in the name of a dishonest voter id through oracle O cast (id, b). Finally, the adversary wins if the election result does not contain all the honest votes registered in Voted (where only the last vote is counted).

Definition 4.2 (Individual verifiability). A voting system is individually verifiable if for any adversary A,

P Exp verif A (λ) = 1 is negligible.
As mentioned in introduction, [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] shows an impossibility result between (unconditional) privacy and verifiability. [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF] considers another aspect of verifiability, namely universal verifiability, that is, the guarantee that the result corresponds to the content of the ballot, even in presence of a dishonest tally. Interestingly, the same incompatibility result holds between individual verifiability and unconditional privacy, for the same reasons. Exactly like in [START_REF] Chevallier-Mames | On Some Incompatible Properties of Voting Schemes[END_REF], a powerful adversary (i.e. not polynomial) could tally BB and BB ′ where BB ′ is the ballot box from which Alice's ballot has been removed and infer Alice's vote by difference. More generally, unconditional privacy is lost as soon as there exists a tally function that is meaningfully related to the result, which is implied by individual verifiability.

Privacy.

For privacy, we consider the old, well established definition of Josh Benaloh [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]. More sophisticated definitions are been proposed later (see [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] for a survey and a unifying definition). They aim in particular at getting rid of the partial tally assumption (needed in [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]). Note however that they all assume an honest ballot box. Since we also assume partial tally, the original Benaloh definition is sufficient for our needs. In particular, we do not know if privacy implies verifiability for counting functions that do not have the partial tally property. This is left as future work.

Intuitively, a voting system is private if, no matter how honest voters vote, the adversary cannot see any difference. However, the adversary always sees the election result, that leaks how the group of honest voters voted (altogether). Therefore, the election result w.r.t. the honest voters has to remain the same. More formally, in a first step, the adversary uses oracles O reg (id) and O corr (id) to respectively register a voter and get her credential. Then the adversary may request an honest voter id to vote either for v 0 or v 1 through oracle O p vote (id, v 0 , v 1 ). Voter id will vote v β depending on the bit β. The adversary may also cast an arbitrary ballot b in the name of a dishonest voter id through oracle O cast (id, b). The election will be tallied, only if the set V 0 of votes v 0 yields the same result than the set V 1 of votes v 1 (where only the last vote is counted). Finally, the adversary wins if he correctly guesses β. Formally, privacy is defined through the game Exp priv, β A (λ) displayed on Figure 5. [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF]). A voting system is private if for any adversary A,

Definition 4.3 (Privacy

P Exp priv,0 A (λ) = 1 -P Exp priv,1 A (λ) = 1 is negligible.

Privacy implies individual verifiability

We show that privacy implies individual verifiability and we first list here our assumptions. As for the symbolic case, we assume the existence of a neutral vote. We also require that the tally can be performed piecewise, that is, informally, as soon as two boards BB 1 , BB 2 are independant then Tally(BB 1 ⊎ BB 2 ) = Tally(BB 1 ) * Tally(BB 2 ). This property is satisfied by most voting schemes. Formally, we characterize this notion of "independence" depending on whether a scheme is id-based or cred-based.

An id-based voting scheme has the piecewise tally property if for any two boards BB 1 and BB 2 that contain ballots registered for

Exp verif A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) BB, Voted ← [] A O v vote , O cast 2 (state, pk) r ← Tally(BB, sk, U) if r ⊥ ∧ ∀V c (finite) . r ρ({v i } 1≤i ≤k ⊎ V c ) then return 1 where Voted = {(id 1 , v 1 ), . . . , (id k , v k )} O v vote (id, v) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v) BB ← BB ∥b Voted ← Voted ′ ∥(id, cred id , v)
return b where (id, cred id ) ∈ U and Voted ′ is obtained from Voted by removing all previous instances of (id, * )

O cast (id, b) if (id, * ) ∈ CU ∧ Valid(id, b, BB, pk) then BB ← BB ∥(id, b) Figure 4: Verifiability Exp priv, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) BB, V 0 , V 1 ← [] state 2 ← A O p vote , O cast 2 (state 1 , pk) if ρ(V 0 ) = ρ(V 1 ) then r ← Tally(BB, sk, U) β ′ ← A 3 (state 2 , pk, r ) return β ′ O p vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) BB ← BB ∥b V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) return b where (id, cred id ) ∈ U and V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 ) by removing all instances of (id, * ) O cast (id, b) if (id, * ) ∈ CU ∧ Valid(id, b, BB, pk) then BB ← BB ∥(id, b)
ValidTally(BB 1 ⊎ BB 2 , sk, U) ∧ ∀b ∈ BB 1 . ∀b ′ ∈ BB 2 . open id (b) open id (b ′ ),
then their tally can be computed separately:

Tally(BB 1 ⊎ BB 2 , sk, U) = Tally(BB 1 , sk, U) * Tally(BB 2 , sk, U). (*)
We also assume that the tally only counts ballots cast with registered ids, i. Similarly, a cred-based voting scheme has the piecewise tally property if for any two boards BB 1 and BB 2 that contain ballots associated to different credentials, that is

∀b ∈ BB 1 . ∀b ′ ∈ BB 2 . open cred (b, sk, U) open cred (b ′ , sk, U)
then their tally can be computed separately (Property (*)).

We also assume that registering more voters does not change the tally: if U, U ′ share no credentials and ∀b ∈ BB. ( * , open cred (b, sk, U∪ U ′ )) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∪ U ′ ).

We say that a (id-based) voting scheme is strongly correct if whatever valid board the adversary may produce, adding a honestly generated ballot still yields a valid board. This property is formally defined through the game Exp ValidTally A (λ) displayed in Figure 6. A

Exp ValidTally A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) (BB, id, v) ← A O v t vote 2 (state, pk) b ← Vote(id, cred id , pk, v) where (id, cred id ) ∈ U if (id, * ) ∈ U\CU ∧ (∀b ′ ∈ BB. open id (b ′ ) id) ∧ ValidTally(BB, sk, U) ∧ ¬ValidTally(BB| |b, sk, U) then return 1 O vt vote (id, v)
if ∃cred id .(id, cred id ) ∈ U\CU then return Vote(id, cred id , pk, v) A voter credential typically includes a private part used to generate a signing key for example. It should not be possible for an adversary to forge a ballot with an honest credential. Formally, we say that a voting scheme has non-malleable credentials, if for any

Exp NM A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state ← A Oreg, Ocorr 1 (pk) L ← [] b ← A Oc 2 (state, pk) if b L ∧ ∃(id, cred id ) ∈ U\CU. open cred (b, sk, U ) = cred id then return 1 O c (id, v) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v) L ← L ∥b return b
where (id, cred id ) ∈ U where Exp NM A (λ) is defined on Figure 7. For example, Belenios and Civitas have non-malleable credentials. Theorem 4.4 (Privacy implies individual verifiability). Let V be an id-based, strongly correct, voting scheme that has the piecewise tally property. If V is private, then V is individually verifiable.

Similarly, let V be a cred-based voting scheme that has the piecewise tally property and non-malleable credentials. If V is private, then V is individually verifiable.

The proof of this theorem is inspired by the same intuition as in the symbolic case: if an attacker manages to break verifiability, that is, to obtain that not all votes from the honest voters are counted correctly, then there also exists an attack against privacy. Indeed, consider a scenario with additional, new voters, whose votes should compensate those cast by the initial voters. By performing the attack on verifiability for the initial voters, the attacker reaches a state where, in the result of the election, they are no longer compensated by the new votes. This allows the attacker to break privacy.

More precisely, the general idea of the proof is as follows. Consider an attacker A that breaks individual verifiability, i.e. wins the game Exp verif with non negligible probability. We construct an attacker B that breaks privacy, i.e. wins Exp priv, β . B starts by registering, and corrupting, the same voters as

(id ′ i , v blank , v i )
, where v i is the (last) vote cast by id i . The vote of each id ′ i compensates the vote of id i , so that the condition ρ(V 0 ) = ρ(V 1 ) from Exp priv holds. B then obtains the result r of the election, which is equal to r 1 * r 2 , where r 1 is the tally of the ballots cast by A, and r 2 the tally of the additional ballots cast by B. Then:

Exp dis, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) V 0 , V 1 ← [] state 2 , BB ← A O d vote 2 (state 1 , pk) if ρ(V 0 ) = ρ(V 1 ) then r ← Tally(BB, sk, U) β ′ ← A 3 (state 2 , pk, r ) return β ′ O d vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) return b
where (id, cred id ) ∈ U and

V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 )
by removing all instances of (id, * ) • if β = 0: then all the votes cast by the id ′ i were v blank , and the result is thus r = r 1 . Since A breaks individual verifiability, r 1 does not contain the honest votes, i.e., for all multiset V c of votes, r ρ(v 1 , . . . , v n ) * ρ(V c ).

• if β = 1 however, the votes cast by the id ′ i were the v i , and the partial tally r 2 is therefore r 2 = ρ(v 1 , . . . , v n ). Hence, the result r does contain the honest votes.

Therefore, by observing whether the final result of the election contains the honest votes, B is able to guess β, and wins Exp priv .

PRIVACY WITH A DISHONEST BOARD

Our main theorem states that privacy implies individual verifiability. However, the privacy definition introduced by Benaloh assumes an honest ballot box, as most existing privacy definitions of the literature [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF]. Therefore, our main theorem shows that whenever a voting scheme is private w.r.t. an honest ballot box, then it is also individually verifiable w.r.t. an honest ballot box, which is of course a rather weak property. However, intuitively, our proof technique does not rely on the trust assumptions.

As pointed out in introduction, extending cryptographic privacy definitions to a dishonest ballot box is difficult. Consider the natural extension of privacy as displayed in Figure 8: the game is the same than Exp priv, β A (λ) except that the adversary arbitrarily controls the ballot box. Unfortunately, an adversary can always win this new game. Indeed, he may simply query O d vote (id 1 , 0, 1) and O d vote (id 2 , 1, 0), yielding respectively ballots b id 1 and b id 2 . Then the adversary choses BB = b id 1 . The tally will return β, hence the adversary wins. This corresponds to the fact that an adversary may always isolate a voter and break her privacy.

Privacy with careful voters

To solve this issue, we choose another approach, which consists in explicitly modelling the verification steps made by voters: the tally will be performed only if honest voters have successfully run their checks (e.g. checking that their ballot belongs to the bulletin board). Therefore, we extend the privacy game as follows. The adversary arbitrarily controls the ballot box and may request honest voters to vote through O p,c vote (id, v 0 , v 1 ) as before. Note that there is no need for the O cast oracle since the adversary may add directly his own

Exp priv-careful, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) V 0 , V 1 , L id (for all id in U) ← [] state 2 , BB ← A O p,c vote 2 (state 1 , pk) H ← [] state 3 ← A O happy BB 3 (state 2 ) if ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H and ρ(V 0 ) = ρ(V 1 ) then r ← Tally(BB, sk, U) else r ← ⊥ β ′ ← A 4 (state 3 , pk, r ) return β ′ O p,c vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) V 0 ← V ′ 0 ∥(id, v 0 ) V 1 ← V ′ 1 ∥(id, v 1 ) L id ← L id ∥(b, v β ) return b
where (id, cred id ) ∈ U and To run her verification test (using algorithm VerifVoter), the voter has access to the ballot box BB forged by the adversary as well as her local state L id that contains in particular her previously generated ballots. The tally is performed only if all honest voters have successfully performed their test and if, as previously, the set V 0 of left votes v 0 yields the same result than the set V 1 of right votes v 1 . Formally, privacy with careful voters is defined through the game Exp priv-careful displayed on Figure 9. Definition 5.1 (Privacy with careful voters). A voting system is private against a dishonest board with careful voters if for any adversary A,

V ′ 0 (resp. V ′ 1 ) is obtained from V 0 (resp. V 1 ) by removing all instances of (id, * ) O happy BB (id) if (id, cred id ) ∈ U\CU then if VerifVoter(id, cred id , L id , BB) then H ← H ∥id
P Exp priv-careful,0 A (λ) = 1 -P Exp priv-careful,1 A (λ) = 1 is negligible.
While this definition models a dishonest ballot box, it implicitly assumes that all voters see the same (possibly dishonest) ballot box. This is a very common assumption in voting, that needs to be achieved by external means.

Similarly, we extend individual verifiability to individual verifiability against a dishonest board as expected, assuming that the tally is performed only if all honest voters have successfully performed their test. The formal definition of individual verifiability against a dishonest board can be found in appendix.

Privacy implies individual verifiability against a dishonest box too

We need to assume that the verification test run by honest voters (VerifVoter) is consistent with how the voter voted. Namely, if the

Exp BS, β A (λ) (pk, sk) ← Setup(1 λ ) U, CU ← [] state 1 ← A Oreg, Ocorr 1 (pk) L ← [] state 2 , BB ← A O bs vote 2 (state 1 , pk) if ∀v . | {b |b ∈ BB ∧ ∃v ′ . (b, v, v ′ ) ∈ L} | = | {b |b ∈ BB ∧ ∃v ′ . (b, v ′ , v) ∈ L} | then r ← Tally(BB, sk, U) β ′ ← A 3 (state 2 , pk, r ) return β ′ O bs vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU then b ← Vote(id, cred id , pk, v β ) L ← L ∥(b, v 0 , v 1 )
return b where (id, cred id ) ∈ U voter's intended ballot is the one that is selected from the board by the revote policy (e.g. appears last w.r.t. this voter), then this voter must be satisfied with the board (that is, VerifVoter passes). Conversely, if the test VerifVoter fails for voter id then adding ballots unrelated to id (or her credential) will not change this fact (VerifVoter will still fail). These assumptions are formally stated in appendix.

Theorem 5.2 (Privacy implies individual verifiability against a dishonest board). Let V be an id-based, strongly correct voting scheme that has the piecewise tally property. If V is private against a dishonest board with careful voters, then V is individually verifiable against a dishonest board with careful voters.

Similarly, let V be a cred-based voting scheme that has the piecewise tally property and non-malleable credentials. If V is private against a dishonest board with careful voters, then V is individually verifiable against a dishonest board with careful voters.

COMPARING PRIVACY

We compare different notions of privacy, with and without an honest ballot box, on four standard protocols (Helios, Belenios, Civitas, and Neuchâtel) as well as on our simple protocol, sketched in introduction.

To our knowledge, the only other definition of privacy with a dishonest ballot box is the privacy notion introduced by Bernhard and Smyth [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF]. We first start by discussing this definition.

PrivacyBS

The privacy notion introduced by Bernhard and Smyth [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is recalled in Figure 10 (PrivacyBS). The adversary may request a voter id to vote for v 0 or v 1 (depending on the bit β) through the oracle O bs vote (id, v 0 , v 1 ). He produces an arbitrary ballot box BB and the tally will be performed provided that, looking at honest ballots that appear in BB, counting the corresponding left and right votes yields the same result.

The main interest of [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] is to highlight the fact that previous definitions implicitly assume an honest ballot box. The first attempt at defining privacy w.r.t. a dishonest ballot box (PrivacyBS) has several limitations. First, it strongly assumes that the ballots that appear in the ballot box are exactly the same than the cast ballots. This is not the case for example of the ThreeBallots protocol [START_REF] Rivest | Three Voting Protocols: ThreeBallot, VAV and Twin[END_REF] where the ballot box only contains two shares (out of three) of the original ballot. It is not applicable either to a protocol like BeleniosRF [START_REF] Chaidos | BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme[END_REF] where ballots are re-randomised before their publication. Second, it requires ballots to be non-malleable [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF]. This means that, as soon as a ballot includes a malleable part (for example the voter's id like in Helios, or a timestamp), privacy cannot be satisfied. This severely restricts the class of protocols that can be considered. Third, Pri-vacyBS does not account for a revote policy. As soon as revote is allowed (for example in Helios), then PrivacyBS is broken since some ballots may not be counted. Indeed, an attacker may call O bs vote (id 1 , 1, 0), followed by O bs vote (id 1 , 0, 1), obtaining ballots b 1 , b ′ 1 , and return the board

BB = [b 1 , b ′ 1 ]
. The equality condition on the number of ballots in BB produced by O bs vote holds, since for v = 0, 1:

|{b ∈ BB|∃v ′ . (b, v, v ′ ) ∈ L}| = |{b ∈ BB|∃v ′ . (b, v ′ , v) ∈ L}| = 1 where L = [(b 1 , 1, 0), (b ′ 1 , 0, 1)].
Hence the tally is computed. According to the revote policy, only b ′ 1 is counted, and the result is β, which lets the attacker win Exp BS .

Protocols

We consider four standard protocols (Helios, Belenios, Civitas, and Neuchâtel) as well as our simple protocol, presented in introduction. We briefly explain each of them in this section. In what follows E = (gen, enc, dec) denotes an encryption algorithm.

Simple. We detail the simple protocol sketched in introduction. Recall that voters simply send their encrypted votes to the ballot box, and, at the end of the voting phase, the tally computes and publishes the result of the election. No revote is allowed, and the voters do not have any means of verifying that their vote is taken into account. Identities and credentials are not used in this protocol. The corresponding algorithms of this protocol are:

• Vote(id, cred, pk, v) = enc(pk, v) • VerifVoter(id, cred, L, BB) = true (voters do not make any checks) • Tally(BB, sk, U) checks that all the ballots in BB are distinct, and returns ⊥ if not. The tally performs a random permutation of the ballots, decrypts all of them and returns the multiset of the votes they contain. • Valid(id, b, BB, pk) checks that b does not already occur in BB.

Helios [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF] is similar to Simple, except that revote is allowed, and the last vote cast by each id is counted. To make this revote policy possible, the ballots contain the id of the voter: Vote(id, cred, pk, v) = (id, enc(pk, v)). enc(pk, v) here also includes a proof that v is a valid vote. Credentials are unused. The tally computes the result of the election similarly to Simple except that it also features an homomorphic mode, where the tally homomorphically computes the sum of the ballots in BB, decrypts the resulting ciphertext and returns the result. Moreover, the tally returns a proof of correct decryption. In addition, the board which will be tallied is made public, allowing the voters to check that their last ballot is indeed the last ballot with their id on the board: VerifVoter(id, cred, L id , BB) = the last element in L id is the last ballot registered for id in BB.

Similarly to Simple, the Valid function checks that there is no duplicated ciphertext and also checks that the ballot is submitted under the right id.

Valid(id, (id ′ , c), BB, pk) = (id = id ′ ) ∧ c does not occur in BB

This models an authenticated channel between the ballot box and each voter: a voter id may not cast a vote in the name of id ′ .

Belenios [START_REF] Cortier | Election Verifiability for Helios under Weaker Trust Assumptions[END_REF] is similar to Helios, except that voters sign their encrypted vote thanks to their credential:

Vote(id, k, pk, v) = (id, signElGamal(v, pk, k))
where signElGamal(•, •, •) denotes the combination of the (ElGamal) encryption and the signature. As for Helios, it also includes a proof that v is a valid vote. Tally checks that there exists a bijection between the ids and the credentials in the final board, i.e. that the same id is always associated with the same signature, and vice versa. The revote policy counts the last ballot corresponding to a given credential. Voters can verify that their last ballot is indeed the last one signed by their key on the board.

Civitas [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF]. In Civitas, voters privately receive a credential, that is published encrypted on the bulletin board. To cast a vote, a voter encrypts her vote, also encrypts her credential, and produces a proof π of well-formedness that links the two ciphertexts together. The corresponding ballot is of the form Vote(id, cred, pk, v) = (enc(pk, cred), enc(pk, v), π ).

The voters can verify that their vote will be taken into account by checking that it is present on the board that will be tallied.

VerifVoter(id, cred, L id , BB) = b ∈ BB where b is the ballot in L id . In theory, revote is allowed. However, we unveil a small discrepancy in how revote should be performed. Assume for example that the last ballot should be counted. Since an adversary may recast old ballots generated by an honest voter, a voter should memorise all the ballots he generated and check that they appear in the right order on the ballot box. Such a check seems highly cumbersome for an average voter and we could not find its description in [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF]. Therefore, we simply assume here that honest voters do not revote.

Neuchâtel [START_REF] Galindo | 2015 Neuchâtel's Castas-Intended Verification Mechanism[END_REF]. Voters privately receive a code sheet, where each candidate is associated to a (short) code. To cast a vote, voters send their encrypted votes to the ballot box, similarly to Simple or Helios. The ballot box then provides a return code allowing the voter to check that the ballot has been received and that it encrypts their candidate, as intended. This offers a protection against a dishonest voting client (e.g. if the voter's computer is corrupted). No revote is allowed. Since the bulletin board is not published, voters cannot check that their ballots really belong to the final board (used for tally), which we model by VerifVoter(id, cred, L, BB) = true . Voters have to trust the voting server (or other internal components) on this aspect.

Protocol

Honest board [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF] PrivDis-Naive PrivacyBS [START_REF] Bernhard | Ballot secrecy with malicious bulletin boards[END_REF] Priv-careful Simple (no revote)

✓ ✗ ✓ ✗ Helios ✓ ✗ ✗ ✗ Belenios ✓ ✗ ✗ ✓ Civitas (no revote) ✓ ✗ ✓ ✓ Neuchâtel (no revote) ✓ ✗ ✓ ✗
Figure 11: Comparison of several privacy definitions (✓: the protocol is private, ✗: there exists an attack on privacy)

Attacks

Simple. As described in introduction, a dishonest ballot box may break ballot privacy of any voter by simply replacing the other votes by votes of its choice. In other words, even if the ballot box does not detain any decryption key, it can learn how Alice's voted.

Neuchâtel. Exactly like the Simple protocol, a dishonest ballot box may break ballot privacy of any voter by simply replacing the other votes. This is due to the fact that voters have no control over the ballots that are actually tallied. Note that the Neuchâtel protocol actually includes internal mechanisms that render such an attack difficult. However, from the point of view of a voter, if the ballot box is compromised, her privacy is no longer guaranteed.

Helios. Helios is also vulnerable to an attack when the ballot box is compromised. This attack is due to P. Roenne [START_REF] Roenne | [END_REF]. It involves two honest voters id 1 , id 2 , and a dishonest voter id 3 . The attacker may call O Belenios and Civitas remain private against a dishonest board as long as voters perform their verification checks. We formally prove privacy according to our definition Priv-careful.

Comparison

We summarise our findings in Figure 11. As explained in Section 5, the naive extension of the privacy definition to a dishonest board (PrivDis-Naive) is immediately false for any protocol.

All of our five protocols satisfy privacy against an honest ballot box. We rely here on previous results of the literature, except for Civitas (and of course the Simple protocol). Indeed, Civitas has been proved to be coercion-resistant [START_REF] Clarkson | Civitas: Toward a Secure Voting System[END_REF] in a rather different setting. Therefore we show here that it satisfies the Benaloh definition.

PrivacyBS fails to detect the attack on the Neuchâtel protocol and the Simple protocol since it requires that the tally of the honest ballots present on the final board does not leak information. Conversely, it cannot prove Belenios private as it does not properly handle revoting as explained in Section 6.1.

CONCLUSION

We show a subtle relation between privacy and verifiability, namely that privacy implies individual verifiability, which is rather counterintuitive. Our result holds in a cryptographic as well as a symbolic setting, for various trust assumptions. In contrast, privacy does not seem to imply universal verifiability nor eligibility verifiability. To show that there is indeed no implication, we plan to exhibit counter-examples, as simple as possible.

Our result assumes counting functions that have the partial tally property. Our proof technique does not extend immediately to more complex counting functions such as STV or Condorcet. We plan to study how privacy and individual verifiability are related in this context. Also, our results implicitly discard anonymous channels: computational models do not account for anonymous channels while our election determinism assumption discards at least some use of anonymous channels. Intuitively, in presence of anonymous channels, an attacker may be able to modify a ballot without being able to tell which one, hence breaking verifiability without breaking privacy. It would be interesting to identify which kind of anonymous channels and more generally, which form of non determinism, can still be tolerated.

Our findings also highlight a crucial need for a ballot privacy definition in the context of a dishonest ballot box, in a cryptographic setting. So far, privacy has only been proved assuming an honest ballot box, which forms a very strong trust assumption that was probably never made clear to voters nor election authorities.

We propose a first attempt at modelling privacy against a dishonest board, assuming that honest voters checks their ballots as expected by the voting protocol. We do not see our definition as final. In particular, assuming that all voters check their vote is highly unrealistic. In a realistic setting, it is more likely that a (small) fraction of honest voters perform the required tests while the others stop after casting their vote. We plan to explore how to adapt our definition to a quantitative setting, in the lines of [START_REF] Küsters | Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study[END_REF].

Appendix A SYMBOLIC PROOF A.1 Assumptions summary

We simply recall here the assumptions described in the core of the paper (Sections 2 and 3.4). The numbers will be useful to refer to the assumptions in the proofs. We also formally define alternative assumptions only sketched in the core of the paper, like the possibility to assume a special "independent" vote instead of a neutral vote.

Notations: if k ∈ N and v ∈ V, k • v denotes the multiset containing k instances of v. If V is a multiset of votes, and v a vote, we denote V (v) the number of instances of v in V .

(1) The tallying process is assumed to output terms representing the result of the election on a channel c r , i.e. ∀α . ∀(tr , ϕ) ∈ trace(P α ). out(c r , r ) ∈ tr ⇒ ∃V . ϕ(r ) ∈ R(ρ(V )).

(2) The representation function is assumed to be injective: ∀r r ′ . R(r ) ∩ R(r ′ ) = ∅.

(3) The counting function is assumed to have the partial tally property: ∀V , V ′ . ρ(V ⊎V ′ ) = ρ(V ) * ρ(V ′ ). * is an associative, commutative operation. (4) The voting processes must be election determinate, i.e. satisfy ∀α, t, t ′ , ϕ, ϕ ′ , x, V .

(t = τ t ′ ∧ (t .out(c r , x), ϕ) ∈ trace(P α ) ∧ (t ′ .out(c r , x), ϕ ′ ) ∈ trace(P α ) ∧ ϕ(x) ∈ R(ρ(V ))) ⇒ ϕ ′ (x) ∈ R(ρ(V ))
(5) The voting processes are assumed to be voting friendly, i.e. we assume that for all voter a ∈ A, there exists t ′′ such that for all α satisfying a dom(α),

• for all (t, ϕ) ∈ trace(P α ), such that t = t ′ .out(c r , x) for some t ′ , x, for all v, there exists tr , ψ such that tr = τ t ′′ , Voted(a, v) ∈ tr , (t ′ .tr .out(c r , x),ψ ) ∈ trace(P α ∪{a →v } ), and

∀V . ϕ(x) ∈ R(ρ(V )) ⇒ ψ (x) ∈ R(ρ(V ⊎ {|v | })).
• and for all t ′ , x such that blocking(t ′ .out(c r , x), P α ), for all v, tr , ψ such that tr = τ t ′′ , blocking(t ′ .tr .out(c r , x), P α ∪{a →v } ).

Our result holds provided one of the two following assumptions is true: [START_REF] Benaloh | Verifiable secret-ballot elections[END_REF] There exists a neutral vote v neutral ∈ V, such that ρ({|v neutral | }) is neutral for * . [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] There exists a special vote v special ∈ V, which is counted separately in the result, as briefly sketched in the core of the paper. Formally, v special must enjoy the following properties.

• the result associated with a multiset determines the number of instances of v special in it

∀V , V ′ . ρ(V ) = ρ(V ′ ) =⇒ V (v special ) = V ′ (v special ).
• the count of v special can be simplified

∀V , V ′ , k. ρ(V ⊎ k • v special ) = ρ(V ′ ⊎ k • v special ) =⇒ ρ(V ) = ρ(V ′ ).
For example, for ρ hom , all the votes are special, therefore this property always holds. For ρ mix , it depends on the set of valid votes. In the standard case where a vote is a selection of candidates (for example between k 1 and k 2 candidates), then a special vote is, for instance, a vote that includes the selection of an extra candidate, not used before.

A.1.1 Properties. We recall here the definitions of the individual verifiability and privacy properties (presented in 3.3), and we define two properties used as pivots in the proof.

• Individual verifiability:

V 1 (t, ϕ) def = ∀t ′ , x . (t = t ′ .out(c r , x)) ⇒ ∃V c . ϕ(x) ∈ R(ρ({|v | ∃a. Voted(a, v) ∈ t | } ⊎ V c )) V def = ∀α . ∀(t, ϕ) ∈ trace(P α ). V 1 (t, ϕ).
• Privacy:

P = ∀α . ∀a, b ∈ A\dom(α). ∀v 1 , v 2 . P α ∪{a →v 1 ,b →v 2 } ≈ t P α ∪{a →v 2 ,b →v 1 }
• First pivot property:

F def = ∀α . ∀a ∈ A\dom(α). ∀v 1 , v 2 ∈ V. ∀t, t ′ , ϕ, ϕ ′ , V , V ′ . [ t = τ t ′ ∧ (t, ϕ) ∈ trace(P α ∪{a →v 1 } ) ∧ (t ′ , ϕ ′ ) ∈ trace(P α ∪{a →v 2 } ) ∧ result(t, ϕ, V ) ∧ result(t ′ , ϕ ′ , V ′ ) ] =⇒ ρ(V ′ ⊎ {|v 1 | }) = ρ(V ⊎ {|v 2 | }).
• Second pivot property:

F F def = ∀α . ∀(t, ϕ) ∈ trace(P α ). ∀V , V change . ∀V wanted ⊆ {|v | ∃a. Voted(a, v) ∈ t | }. result(t, ϕ, V ) ⇒ |V change | = |V wanted | ⇒ ∃V c . ρ(V ) * ρ(V change ) = ρ(V wanted ) * ρ(V c )

A.2 Theorem

Lemma A.1 (Privacy implies F ). Under assumptions 1, 2, 3, 4, and 5,

P ⇒ F
Proof. We prove this by contradiction: assuming F does not hold, we construct an attack on privacy. Assume F is false. Hence there exists a scenario where changing the vote of one agent does not change the result by one. That is to say, there exist an affectation of votes α, an agent a dom(α), votes v 1 , v 2 ∈ V, traces (t, ϕ) ∈ trace(P α ∪{a →v 1 } ) and (t ′ , ϕ ′ ) ∈ trace(P α ∪{a →v 2 } ), such that t = τ t ′ ,and two multisets V , V ′ , such that result(t, ϕ, V ), result(t ′ , ϕ ′ , V ′ ), and ρ(

V ′ ⊎ {|v 1 | }) ρ(V ⊎ {|v 2 | }).
Since result(t, ϕ, V ), there exist x, t 1 such that t = t 1 .out(c r , x) and ϕ(x) ∈ R(ρ(V )). Similarly, there exist y, t ′ 1 such that t

′ = t ′ 1 .out(c r , y) and ϕ ′ (y) ∈ R(ρ(V ′ )). Since t = τ t ′ , x = y.
Note that we necessarily have v 1 v 2 : indeed, if v 1 = v 2 then (t, ϕ) and (t, ϕ ′ ) are traces of the same process. Since ϕ(x) ∈ R(ρ(V )), by assumption 4, this implies that ϕ ′ (x) ∈ R(ρ(V )). Since we already know that ϕ ′ (x) ∈ R(ρ(V ′ )), by assumption 2, we have ρ(V ) = ρ(V ′ ). Thus, as

v 1 = v 2 , we have ρ(V ) * ρ({|v 2 | }) = ρ(V ′ ) * ρ({|v 1 | }), which is contradictory. Hence v 1 v 2 .
The attack on privacy consists in the fact that, since changing a's vote does not produce a change of exactly one in the result, even in presence of another agent b whose vote is the opposite of a's, the result will be different depending on the vote of a.

Formally, let b dom(α) ∪ {a}. By assumption 5, there exist sequences of actions t b , t ′ b , and frames ψ , ψ ′ , such that

(t 1 .t b .out(c r , x),ψ ) ∈ trace(P α ∪{a →v 1 ,b →v 2 } ), (t ′ 1 .t ′ b .out(c r , x),ψ ′ ) ∈ trace(P α ∪{a →v 2 ,b →v 1 } ), Voted(b, v 2 ) ∈ t b , Voted(b, v 1 ) ∈ t ′ b , t b = τ t ′ b , ψ (x) ∈ R(ρ(V ⊎ {|v 2 | })), and ψ ′ (x) ∈ R(ρ(V ′ ⊎ {|v 1 | })). Since ρ(V ′ ⊎ {|v 1 | }) ρ(V ⊎ {|v 2 | })
, by assumption 2, we have ψ (x) ψ ′ (x).

We have constructed two frames, obtained by the same actions in P α ∪{a →v 1 ,b →v 2 } and P α ∪{a →v 2 ,b →v 1 } , which yield different results for the election. Using assumption 4, this lets us prove that these two processes are not ≈ t -equivalent.

Indeed, let us denote t

2 def = t 1 .t b .out(c r , x) and t ′ 2 def = t ′ 1 .t ′ b .out(c r , x).
We have (t 2 ,ψ ) ∈ trace(P α ∪{a →v 1 ,b →v 2 } ). For any trace (t ′′ 2 ,ψ ′′ ) ∈ trace(P α ∪{a →v 2 ,b →v 1 } ), if t ′′ 2 = τ t 2 = τ t ′ 2 , then by assumption 4 we have

ψ ′′ (x) ∈ R(ρ(V ′ ⊎ {|v 1 | })). Hence, by assumption 2 as ρ(V ⊎ {|v 2 | }) ρ(V ′ ⊎ {|v 1 | }), we have ψ ′′ (x) R(ρ(V ⊎ {|v 2 | }))
, which implies that ψ , ψ ′′ are not statically equivalent.

Thus, P α ∪{a →v 1 ,b →v 2 } ̸ ≈ t P α ∪{a →v 2 ,b →v 1 } . This violates P, which concludes the proof. □ Lemma A.2 (Privacy and F imply F F ). Under assumptions 1, 2, 3, 4, and 5,

(P ∧ F ) ⇒ F F
Proof. Assume that both P and F hold. Let α be an affectation of votes, let (t, ϕ) ∈ trace(P α ), let V be such that result(t, ϕ, V ), i.e. there exist t ′ , x such that t = t ′ .out(c r , x) and ϕ(x

) ∈ R(ρ(V )). Let V wanted ⊆ {|v | ∃a. Voted(a, v) ∈ t | }, and V change such that |V change | = |V wanted |.
To prove F F , we need to show that the result in this trace augmented with V change contains at least the subset V wanted of the (intended) votes of the honest voters. That is to say, we must show that there exists

V c such that ρ(V ) * ρ(V change ) = ρ(V wanted ) * ρ(V c ).
The idea of the proof is to compare ρ(V ) to the result ρ(V ′ ) obtained by turning, one by one, all votes from V wanted into the votes from V change , and performing the same sequence of actions. As we will see, this is possible, otherwise P would break; and V ⊎ V change contains more instances of the honest votes than V ′ ⊎ V wanted , since F holds.

Let us denote the Voted events appearing in t by Voted(a 1 , v 1 ), . . . , Voted(a l , v l ) for some pairwise distinct agents a 1 , . . . , a l ∈ Voters(t), and some l ∈ N.

By definition, each element of V wanted is associated with one of these Voted events. Let m def = |V wanted |. Without loss of generality, we may assume that V wanted = {|v 1 , . . . , v m | }.

Note that |V change | is also equal to m by assumption. Let us then denote

V change def = {|v ′ 1 , . . . , v ′ m | }.
Since, by assumption on the form of the processes, the Voted(a, v) event can only be emitted by the process Voter(a, v, c) for some credential c, we have α(a i ) = v i for all i ∈ 1, m .

For i ∈ 0, m , let α i denote the affectation of votes obtained from α by turning the first i votes from V wanted to V change , i.e.

• α i (a j ) = v ′ j if j ∈ 1, i ; • α i (a j ) = v j if j ∈ i + 1, m ; • α i (a) = α(a) if a ∈ dom(α) is not one of the a j , j ∈ 1, m . Let β def = α m .
Note that α 0 = α, and that all the α i have the same domain. Let us show that for all i, the same actions as t can be performed in P α i with the same agents emitting Voted events, i.e. that ∀i ∈ 0, k 1 . ∃t i . t i = τ t ∧ ¬blocking(t i , P α i ).

By contradiction, assume this property does not hold, and let i be the smallest index that falsifies it. Hence,

∀t i . t i = τ t ⇒ blocking(t i , P α i ). (1)
In addition, note that since the property is clearly satisfied at the 0th step, i ≥ 1. Hence, it holds for i -1, i.e. there exists t i-1 such that t i-1 = τ t, and ¬blocking(t i-1 , P α i -1 ). Since t = t ′ .out(c r , x), we also have

t i-1 = t ′ i-1 .out(c r , x) for some t ′ i-1 such that t ′ i-1 = τ t ′ . Then, for all t ′ i = τ t ′ i-1 (= τ t ′ ), by (1)
, blocking(t ′ i .out(c r , x), P α i ) holds. The same sequence of actions t i-1 is blocking at step i and not at step i -1, which differs only by the vote of of a i . This lets us construct an attack on privacy, which constitutes a contradiction. Indeed, by assumption 5, we may add a voter b dom(α), who votes for v ′ i at step i -1, and for v i at step i, and there exists tr such that • there exists tr ′ = τ tr and ψ such that

(t ′ i-1 .tr ′ .out(c r , x),ψ ) ∈ trace(P α i -1 ∪{b →v ′ i } ). • for all t ′ i = τ t ′ i-1 (= τ t ′ )
, we have shown that blocking(t ′ i .out(c r , x), P α i ), and thus for all tr ′′ = τ tr and all ψ ′ , (t ′ i .tr ′′ .out(c r , x),ψ ′ ) trace(P α i ∪{b →v i } ). Therefore, the processes P α i ∪{b →v i } and P α i -1 ∪{b →v ′ i } are not trace equivalent. Since they only differ by the votes of a i and b, who respectively vote for v i , v ′ i on the left and v ′ i , v i on the right, this breaks privacy, which contradicts the hypotheses. Thus, for all i, there exists t i such that t i = τ t, of the form t ′ i .out(c r , x), such that ¬blocking(t i , P α i ). In other words, there exists ϕ i such that (t i , ϕ i ) ∈ trace(P α i ). By assumption 1, there exists

V i such that ϕ i (x) ∈ R(ρ(V i )), i.e. result(t i , ϕ i , V i ). Let V ′ def = V m . Note that V 0 = V . For all i ∈ 0, m -1 , α i and α i+1 only differ by the vote of a i+1 , which is v ′ i+1 in α i+1 and v i+1 in α i . Hence, by F , we have ρ(V i ⊎ {|v ′ i+1 | }) = ρ(V i+1 ⊎ {|v i+1 | }).
That is to say, by assumption 3, that ρ(

V i ) * ρ({|v ′ i+1 | }) = ρ(V i+1 ) * ρ({|v i+1 | }).
Therefore, by rewriting these m equalities successively, we have

ρ(V 0 ) * ρ({|v ′ 1 | }) * . . . * ρ({|v ′ m | }) = ρ(V m ) * ρ({|v 1 | }) * . . . * ρ({|v m | }),
i.e., by assumption 3,

ρ(V ) * ρ({|v ′ i | i ∈ 1, m | }) = ρ({|v i | i ∈ 1, m | }) * ρ(V ′ ). By definition, this means ρ(V ) * ρ(V change ) = ρ(V wanted ) * ρ(V ′ )
which concludes the proof. □ Lemma A.3 (F F implies V with a neutral vote). Under assumptions 1, 2, 3, 4, 5, and assuming the existence of a neutral vote (assumption 6),

F F ⇒ V Proof.
Under assumption 6, there exists a neutral vote v neutral . Assume F F holds.

Let α be an affectation of votes, and let (t ′ .out(c r , x), ϕ) ∈ trace(P α ). Let t def = t ′ .out(c r , x). To prove individual verifiability, we need to show that the result in this trace contains at least the (intended) votes of the honest voters. That is to say, we must show that there exists

V c such that ϕ(x) ∈ R(ρ({|v | ∃a. Voted(a, v) ∈ t | } ⊎ V c )).
By assumption 1, there exists V such that ϕ(x) ∈ R(ρ(V )). We have result(t, ϕ, V ).

Let V wanted def = {|v | ∃a. Voted(a, v) ∈ t | } be the multiset of all intended honest votes in t. Let k def = |V wanted |, and V change def = k • v neutral . By F F , there exists a multiset V c such that ρ(V ) * ρ(V change ) = ρ(V wanted ) * ρ(V c ). By assumption 3, ρ(V change ) = ρ({|v neutral | }) k . As, by assumption 6, ρ({|v neutral | }) is neutral for * , so is ρ(V change ). Therefore, ρ(V ) = ρ(V wanted ) * ρ(V c ) = ρ(V wanted ⊎ V c
), which proves the claim. □ Lemma A.4 (F F implies V with a special vote). Under assumptions 1, 2, 3, 4, 5, and assuming the existence of a vote that is counted separately (assumption 7), F F ⇒ V Proof. Under assumption 7, there exists a special vote v special which is counted separately in the result. Assume F F holds. Let α be an affectation of votes, and let (t ′ .out(c r , x), ϕ) ∈ trace(P α ). Let t def = t ′ .out(c r , x). To prove individual verifiability, we need to show that the result in this trace contains at least the (intended) votes of the honest voters. That is to say, we must show that there exists

V c such that ϕ(x) ∈ R(ρ({|v | ∃a. Voted(a, v) ∈ t | } ⊎ V c )).
By assumption 1, there exists V such that ϕ(x) ∈ R(ρ(V )). We have result(t, ϕ, V ).

Let V wanted def = {|v | ∃a. Voted(a, v) ∈ t ∧ v v special |
} be the multiset of all intended honest votes in t that are not v special .

Let

k def = |V wanted |, and V change def = k • v special . By F F , there exists a multiset V c such that ρ(V ) * ρ(V change ) = ρ(V wanted ) * ρ(V c ).
We may rewrite this equality as ρ(V ⊎ k • v special ) = ρ(V wanted ⊎ V c ) by assumption 3. Assumption 7 then lets us deduce that

(V ⊎ k • v special )(v special ) = (V wanted ⊎ V c )(v special ).
Yet, V wanted (v special ) = 0 by definition. Therefore, V c (v special ) ≥ k, and we may write

V c = V ′ c ⊎ k • v special for some V ′ c . We then have ρ(V ⊎ k • v special ) = ρ(V wanted ⊎ V ′ c ⊎ k • v special ),
which implies by assumption 7 that

ρ(V ) = ρ(V wanted ⊎ V ′ c ).
Since V wanted contains all the intended honest votes different from v special , it remains to be proved that V ′ c contains sufficiently many instances of v special .

Let k ′ def = |{|Voted(a, v special ) ∈ t | a ∈ A| }| the number of intended votes for v special in t; and V ′ wanted def = k ′ • v special . Let v ∈ V such that v v special . Let V ′ change def = k ′ • v. By F F , there exists V ′′ c such that ρ(V ) * ρ(V ′ change ) = ρ(V ′ wanted ) * ρ(V ′′ c ),
i.e., by assumption 3,

ρ(V ⊎ k ′ • v) = ρ(k ′ • v special ⊎ V ′′ c ).
By assumption 7, we then have

(V ⊎ k ′ • v)(v special ) = (k ′ • v special ⊎ V ′′ c )(v special ). As before, since v v special , this means that V (v special ) ≥ k ′ .
We already know that ρ(V ) = ρ(V wanted ⊎ V ′ c ). By applying assumption 7 again,

(V wanted ⊎ V ′ c )(v special ) = V (v special ) ≥ k ′ . Since v special V wanted , (V ′ c )(v special ) ≥ k ′ , i.e. V ′ c = V ′′′ c ⊎ k ′ • v special for some V ′′′ c .
Therefore we have

ρ(V ) = ρ(V wanted ⊎ k ′ • v special ⊎ V ′′′ c ) = ρ({|v | ∃a. Voted(a, v) ∈ t | } ⊎ V ′′′ c ), which concludes the proof. □
The next theorem corresponds to Theorem 3.11.

Theorem A.5 (Privacy implies individual verifiability when there is a neutral or a special vote). Under assumptions 1, 2, 3, 4, 5, and assuming the existence of either a neutral vote or a special vote counted separately (assumptions 6 or 7), P ⇒ V Proof. This follows directly from Lemmas A.1, A.2, A.3, and A. [START_REF] Adida | Helios: Web-based Open-Audit Voting[END_REF]. □

Appendix B COMPUTATIONAL PROOF B.1 Assumptions summary

We first recall some of the hypotheses used in the proofs, that were presented in Sections 2, 4.1 and 4.3. Some of these assumptions differ depending on whether the scheme is id-based or cred-based, or apply only to one of these two classes of schemes. In such cases, the differences will be clearly stated.

(1) The voting scheme has the piecewise tally property. In the case of id-based schemes, the assumption is that for all boards BB 1 , BB 2 , if sk is the election key and U is a list of registered users and credentials, and if

ValidTally(BB 1 ⊎ BB 2 , sk, U) ∧ ∀b ∈ BB 1 . ∀b ′ ∈ BB 2 . open id (b) open id (b ′ )
then the tally can be computed separately:

T ally(BB 1 ⊎ BB 2 , sk, U) = Tally(BB 1 , sk, U) * Tally(BB 2 , sk, U).

In the case of credential-based schemes, the assumption is that for all boards BB 1 , BB 2 , if sk is the election key and U is a list of registered users and credentials, and if

∀b ∈ BB 1 . ∀b ′ ∈ BB 2 . open cred (b, sk, U) open cred (b ′ , sk, U)
then the tally can be computed separately:

T ally(BB 1 ⊎ BB 2 , sk, U) = Tally(BB 1 , sk, U) * Tally(BB 2 , sk, U).

( In the case of credential-based schemes, the assumption is that if U, U ′ share no credentials and ∀b ∈ BB. ( * , open cred (b, sk, U∪U ′ )) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∪ U ′ ). (4) The voting scheme is correct,i.e. for all distinct identities U = id 1 , . . . , id n , and credentials cred 1 , . . . , cred n , for all votes v 1 , . . . , v n , for all election keys (pk, sk),

if BB = [Vote(id i , cred i , pk, v i )|i ∈ 1, n ], then
Tally(BB, sk, U) = ρ(v 1 , . . . , v n ).

(5) There exists a neutral vote v neutral ∈ V, such that ρ({v neutral }) is neutral for * .

(6) Given a multiset of valid votes V and a result r , it is possible to efficiently decide whether r can be decomposed into ρ(V ) * ρ(V ′ ) for some multiset V ′ of valid votes. That is to say there exists a PPTM D such that

∀r , V . D(r, V ) = 1 ⇐⇒ ∃V ′ . r = ρ(V ) * ρ(V ′ ).
In the proof that privacy implies individual verifiability against a dishonest board provided the voters are careful, we also use the following two hypotheses: [START_REF] Bernhard | A comprehensive analysis of game-based ballot privacy definitions[END_REF] If a voter's intended ballot is indeed the one which will be selected from the board by the revote policy, then this voter must be satisfied with the board. Formally, for all registered voter id with credential cred, for all ballot b, voter knowledge L, and board BB,

• For id-based schemes: if the revote policy is to count the last (resp. first) ballot cast for each id, the assumption is that if the last (resp. first) element of L is (b, * ), and the last (resp. first) ballot b ′ ∈ BB such that open id (b ′ ) = id is b, then VerifVoter(id, cred, L, BB) holds. • For credential-based schemes: if the revote policy is to count the last (resp. first) ballot cast for each credential, the assumption is that if the last (resp. first) element of L is (b, * ), and the last (resp. first) ballot b ′ ∈ BB such that open cred (b ′ , sk, U) = cred is b, then VerifVoter(id, cred, L, BB) holds. (8) If a voter id is satisfied with a board BB, then id remains satisfied with any board obtained from BB by adding new ballots that do not interfere with id's given the revote policy.

Formally, for all board BB, election key pk, registered voter id with credential cred and knowledge L, for all BB ′ , • For id-based schemes: the assumption is that if ∀b ∈ BB ′ . open id (b) id then VerifVoter(id, cred, L, BB) ⇐⇒ VerifVoter(id, cred, L, BB ⊎ BB ′ ).

• For credential-based schemes: the assumption is that if ∀b ∈ BB ′ . open cred (b, sk, U) cred then VerifVoter(id, cred, L, BB) ⇐⇒ VerifVoter(id, cred, L, BB ⊎ BB ′ ).

We will also assume, depending on whether the voting scheme is id or credential based, that no polynomial adversary wins Exp ValidTally with non-negligible probability, i.e.

∀A. P Exp

ValidTally A (λ) = 1 is negligible, or that no polynomial adversary wins Exp NM with non-negligible probability,i.e.

∀A. P Exp

NM A (λ) = 1 is negligible,
where Exp ValidTally is defined on Figure 6 and Exp NM is defined on Figure 7.

O v,f vote (id, v) if (id, * ) ∈ U\CU ∧ (id, * ) Voted then b ← Vote(id, cred id , pk, v) BB ← BB ∥b Voted ← Voted ∥(id, v) return b where (id, cred id ) ∈ U O p,f vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU ∧ (id, * ) V 0 ∪ V 1 then b ← Vote(id, cred id , pk, v β ) BB ← BB ∥b V 0 ← V 0 ∥(id, v 0 ) V 1 ← V 1 ∥(id, v 1 )
return b where (id, cred id ) ∈ U We consider the case of protocols where the revote policy is to count only the last ballot (for each id or credential) or the first ballot. In the case of the last ballot, the definitions of the individual verifiability and privacy games can be found on Figures 4 and5

(λ) = 1 -P Exp priv,1 A (λ) = 1 is negligible, then ∀A. P Exp verif A (λ) = 1 is negligible.
Proof. We first consider the case of id-based protocols.

Let A = A 1 , A 2 be an adversary that breaks individual verifiability, i.e. wins Exp verif . We consider an adversary B = B 1 , B 2 , B 3 that attacks privacy, i.e. plays Exp priv, β :

• B O reg , O corr 1 (pk) first simulates A O reg , O corr 1
(pk), i.e. B registers and corrupts the same identities as A, while keeping a list U 1 of the identities it registers by calling O reg . A returns some state. B 1 then calls O reg another |U 1 | times, on fresh identities that do not appear in U 1 . It keeps a list U 2 of these fresh identities. B 2 then returns a state 2 indicating whether A 2 has failed. Intuitively, A is accurately simulated only if β = 0, i.e. is shown a board where the votes it wanted to cast have indeed been cast. Hence whenever A wins Exp verif , the simulated A 2 failing can only mean that β = 1.

• Exp priv will then check that ρ(V 0 ) = ρ(V 1 ), where V 0 and V 1 are the lists it keeps, which contain the first (or last, depending on the revote policy) votes O p vote has been called on for each id. Considering the definition of B 2 , at this point we always have -

ρ(V 0 ) = ρ(V 1 ) = ρ(v 1 , . . . , v l , v neutral , . . . , v neutral l
if ∃V c . r = ρ(Voted) * ρ(V c ) then B returns β ′ = 1 -otherwise, B returns β ′ = 0.
We also construct an adversary C, who plays the game Exp ValidTally .

•

(id, v β ′′ ). If the kth call is O p vote (id, v 0 , v 1 ), C returns (BB, id, v β ′′ ).
We will now prove that if A breaks individual verifiability, then B breaks privacy provided C does not break Exp ValidTally .

The adversary C is polynomial, i.e. there exists a polynomial q(λ) bounding its number of operations. For any β, assume ValidTally(BB a , sk, U 1 ) holds and ValidTally(BB a ⊎ BB b , sk, U 1 ∪ U 2 ) does not. Thus, by assumption 3, ValidTally(BB a ⊎ BB b , sk, U 1 ∪ [(id 1 , cred id 1 ), . . . , (id l , cred id l )]) does not hold either. Hence, there exists a smallest k ∈ 1, l such that ValidTally(BB Since BB a only contains ballots cast for identities in U 1 and BB b for identities in U 2 , and

U 1 ∩ U 2 = ∅, if ValidTally(BB a ⊎ BB b , sk, U 1 ∪ U 2 ),
by assumption 1 we have (regardless of β) r = Tally(BB, sk, U) = Tally(BB a ⊎ BB b , sk, U) = Tally(BB a , sk, U) * Tally(BB b , sk, U)

In addition, by assumption 3, Tally(BB a , sk, U) = Tally(BB a , sk, U 1 ). Hence r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U).

• If β = 0: then Exp Let us first examine the case where A does not block and r ⊥. Since r ⊥, ValidTally(BB a , sk, U 1 ) holds. Hence, ValidTally(BB a ⊎ BB b , sk, U) also holds, and as explained previously we thus know that r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U). Since β = 0, BB b only contains ballots for v neutral . Hence, by assumption 4, Tally(BB b , sk, U) = ρ(v neutral ) l = ρ(v neutral ). Thus r = Tally(BB a , sk, U 1 ). The condition ∃V c . r = ρ(Voted) * ρ(V c ) is therefore equivalent to ∃V c . Tally(BB a , sk, U 1 ) = ρ(Voted) * ρ(V c ). Since, in this case, A has been accurately simulated without blocking, does not return ⊥, and BB a is the board after its execution, this is exactly the condition under which Exp verif A (λ) does not return 1.

O v,c,f vote (id, v) if (id, * ) ∈ U\CU ∧ (id, * ) Voted then b ← Vote(id, cred id , pk, v) Voted ← Voted ∥(id, v) L id ← L id ∥(b, v) return b where (id, cred id ) ∈ U O p,c,f vote (id, v 0 , v 1 ) if (id, * ) ∈ U\CU ∧ (id, * ) V 0 , V 1 then b ← Vote(id, cred id , pk, v β ) V 0 ← V 0 ∥(id, v 0 ) V 1 ← V 1 ∥(id, v 1 ) L id ← L id ∥(b, v β )
return b where (id, cred id ) ∈ U

(λ) = 1 -P Exp priv-careful,1 A (λ) = 1 is negligible, then ∀A. P Exp verif-careful A (λ) = 1 is negligible.
Proof. We first consider the case of id-based protocols.

Let A = A 1 , A 2 , A 3 be an adversary that breaks individual verifiability against a dishonest board with careful voters, i.e. wins Exp verif-careful . We consider an adversary B = B 1 , B 2 , B 3 , B 4 that attacks privacy against a dishonest board with careful voters, i.e. plays Exp priv-careful, β :

• B O reg , O corr 1 (pk) first simulates A O reg , O corr 1
(pk), i.e. B registers and corrupts the same identities as A, while keeping a list U 1 of the identities it registers by calling O reg . A returns some state. B 1 then calls O reg another |U 1 | times, on fresh identities that do not appear in U 1 . It keeps a list U 2 of these fresh identities. contains ballots for the id i ∈ U 2 . BB b , by construction, contain exactly one ballot for each id i , which is the ballot b i produced by the (only) call to O p vote (id i , * , * ). Since the revote policy is to count the first (or last) ballot for each id, by assumption 7, VerifVoter(id i , cred id i , L id i , BB) holds, and thus the call to O happy BB (id i ) adds id i to H. After that step, H thus necessarily contains at least id 1 , . . . , id l .

• Exp priv-careful will then check that all ids occurring in V 0 or V 1 are also in H, where V 0 and V 1 are the lists it keeps, which contain the first (or last, depending on the revote policy) votes O • Exp priv-careful will then check that ρ(V 0 ) = ρ(V 1 ). Considering the definition of B 2 , if this point is reached, we always have We will now prove that if A breaks Exp verif-careful , then B breaks Exp priv-careful provided C does not break Exp ValidTally .

ρ(V 0 ) = ρ(V 1 ) = ρ(
The adversary C is polynomial, i.e. there exists a polynomial q(λ) bounding its number of operations. In addition, by assumption 3, Tally(BB ′ a , sk, U) = Tally(BB ′ a , sk, U 1 ). Hence r = Tally(BB ′ a , sk, U 1 ) * Tally(BB b , sk, U). Moreover, since BB a \BB ′ a contains only ballots for identities not in U 1 , by assumption 2, Tally(BB ′ a , sk, U 1 ) = Tally(BB a , sk, U 1 ), and thus r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U).

• If β = 0: then Exp priv-careful,0 B (λ) = 1 if and only if B 4 (called on the result r ) returns 1 in this game, which happens either when A (simulated by B) blocks; -or when r = ⊥, i.e., as already mentioned, if the tally returns ⊥ or the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H fails in Exp Let us first examine the case where A does not block, the tally does not return ⊥, and the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds. Since r ⊥, ValidTally(BB a , sk, U 1 ) holds. Hence, ValidTally(BB a ⊎ BB b , sk, U) also holds, and as explained previously we thus know that r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U). Since β = 0, BB b only contains ballots for v neutral , and then by assumption 4, Tally(BB b , sk, U) = ρ(v neutral ) l = ρ(v neutral ). Thus r = Tally(BB a , sk, U 1 ). The condition ∃V c . r = ρ(Voted) * ρ(V c ) is therefore equivalent to ∃V c . Tally(BB a , sk, U 1 ) = ρ(Voted) * ρ(V c ). Since, in this case, -A has been accurately simulated without blocking, -BB a is the board it returns, -the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds in Exp verif-careful A , this is exactly the condition under which Exp verif-careful A (λ) does not return 1.

Hence, in that case, Exp Let us first examine the case where A does not block, the tally does not return ⊥, and the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds. As in the β = 0 case, we thus have r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U). Since β = 1, BB b contains ballots for v 1 , . . . , v l , i.e. for Voted. Hence, by assumption 4, Tally(BB b , sk, U) = ρ(Voted), and therefore r = Tally(BB a , sk, U 1 ) * ρ(Voted). By definition of Tally, there exists V such that Tally(BB a , sk, U 1 ) = ρ(V ). Hence the condition ∃V c . r = ρ(Voted) * ρ(V c ) necessarily holds. In addition we know that the test ∀id.

Figure 1 :

 1 Figure 1: Syntax for processes.

def=

  ∀ϕ. (t, ϕ) trace(P).

Figure 2 :

 2 Figure 2: Semantics

Definition 4 . 1 .

 41 A voting scheme consists in six algorithms (Setup, Credential, Vote, VerifVoter, Tally, Valid)

Figure 3 :

 3 Figure 3: Registration and corruption oracles

Figure 5 :

 5 Figure 5: Privacy

  e. ∀BB, sk, U. Tally(BB, sk, U) = Tally(BB ′ , sk, U) where BB ′ = [b ∈ BB | (open id (b), * ) ∈ U]; and that registering more voters does not change the tally: if U, U ′ have no id in common and ∀b ∈ BB. (open id (b), * ) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∪ U ′ ).

Figure 6 :

 6 Figure 6: ValidTally game

Figure 7 :

 7 Figure 7: Credential non-malleability

Figure 8 :

 8 Figure 8: Privacy against a dishonest board (PrivDis-Naive)

Figure 9 :

 9 Figure 9: Privacy game against a dishonest board with careful voters (Priv-careful)

Figure 10 :

 10 Figure 10: PrivacyBS [9]

  p,c vote (id 1 , 0, 1) twice and O p,c vote (id 2 , 1, 0) once, obtaining ballots (id 1 , b 1 ), (id 1 , b ′ 1 ), (id 2 , b 2 ). The adversary then returns the board [(id 1 , b ′ 1 ), (id 2 , b 2 ), (id 3 , b 1 )]. All ballots are different, hence no weeding is needed. The result of the tally is then ρ({|0, 1, 0| }) if β = 0 and ρ({|1, 0, 1| }) if β = 1. The attacker can therefore observe the difference in the result, which breaks privacy.

)

  In the case of id-based schemes only, the tally only counts ballots cast with registered ids, i.e. ∀BB, sk, U. Tally(BB, sk, U) = Tally(BB ′ , sk, U) whereBB ′ = [b ∈ BB | (open id (b), * ) ∈ U].(3) Registering more voters does not change the tally. In the case of id-based schemes, the assumption is that for all board BB, election key sk and list of voters U, if U, U ′ have no id in common and ∀b ∈ BB. (open id (b), * ) U ′ , then Tally(BB, sk, U) = Tally(BB, sk, U ∩ U ′ ).

Figure 12 :

 12 Figure 12: Oracles for the individual verifiability and privacy games (revote policy = first vote)

p

  vote (id, v, v neutral ) returns nothing); * or adds (id, v) to L and removes any previous couple (id, v ′ ) (for any v ′ ) from L. If O p vote (id, v, v neutral ) returns a ballot b, B then adds it to BB ′ , and passes it to A 2 . -for each call to O cast (id, b), provided id ∈ U 1 , B calls O cast (id, b), and, if Valid(id, b, BB ′ , pk), adds it to BB ′ . Let then Voted be the list of the votes in L: Voted = [v for (id, v) ∈ L]. Let also BB a be the value of the board BB ′ at that point. Note that BB a only contains identities from U 1 . If at any point during the simulation A 2 blocks or fails, B stops the simulation. In any case, B 2 calls O p vote (id 1 , v neutral , v 1 ), . . . , O p vote (id l , v neutral , v l ), where v 1 , . . . , v l are the elements of Voted, and id 1 , . . . , id l are pairwise distinct identities from U 2 . Note that since all identities in L are distinct and in U 1 , l is indeed smaller than |U 1 | = |U 2 |. Let BB b = [b 1 , . . . , b l ] be the set of new ballots added to the board by these l calls, i.e. ballots for v neutral if β = 0 and v 1 , . . . , v l if β = 1. At this point, we have BB = BB a ⊎ BB b .

times )

 times Hence this check necessarily succeeds, and Exp priv computes Tally(BB, sk, U).• B 3 obtains a result r . If r = ⊥, B 3 returns 1. If A 2 blocked previously, B returns β ′ = 1. Otherwise, B computes D(r, Voted) and:

  a ⊎ [b 1 , . . . , b k -1 ], sk, U 1 ∪U ′ 2 ) holds and ValidTally(BB a ⊎[b 1 , . . . , b k ], sk, U 1 ∪U ′ 2 ∪[(id k , cred id k )]) does not, where U ′ 2 = [(id 1 , cred id 1 ), . . . , (id k-1 , cred id k -1 )]. b k has been added to BB b by the kth call to O p vote by B: b k = Vote(id k , cred id k , pk, v β ) for some v β . Thus, provided C correctly guesses β ′′ = β and k, C returns (BB a ⊎ [b 1 , . . . , b k -1 ], id k , v β ) the conditions on BB in Exp ValidTally C holds, and thus Exp ValidTally C = 1. Therefore, ValidTally(BB a , sk, U 1 ) holds and ValidTally(BB a ⊎ BB b , sk, U 1 ∪ U 2 ) does not with probability at most 2l P Exp ValidTally C = 1 , which is smaller than 2q(λ) P Exp ValidTally C = 1 since l ≤ q(λ).

  = 1 if and only if B 3 returns 1 in this game, which happens either when A (simulated by B) blocks, or when it does not and ∃V c . r = ρ(Voted) * ρ(V c ) or r = ⊥. Assume ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB a ⊎ BB b , sk, U), which, as we have established, holds except with probability at most 2q(λ) P Exp ValidTally C = 1 .

Figure 14 :

 14 Figure 14: Oracles for the verifiability and privacy games with dishonest boards and careful voters (revote policy = first vote)

  v 1 , . . . , v l , v neutral , . . . , v neutral l times ) Hence this check necessarily succeeds, and Exp priv-careful computes Tally(BB, sk, U).• B 4 obtains a result r (or ⊥, if the previous tests by Exp priv failed or the tally returned ⊥). If -A 2 blocked previously; -or r = ⊥, which means, as we have established that ρ(V 0 ) = ρ(V 1 ) always holds, that the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H fails, or the tally returns ⊥; B returns β ′ = 1. Otherwise, B computes D(r, Voted) and: -if ∃V c . r = ρ(Voted) * ρ(V c ) then B returns β ′ = 1 -otherwise, B returns β ′ = 0.We also construct an adversary C, who plays the game Exp ValidTally .• C 1 is identical to B 1 . • C 2 firstdraws at random a bit β ′′ , and then simulates B 2 up to the point where B 2 has finished simulating A 2 . It simulates each call to O p,c vote (id, v 0 , v 1 ) B does by calling O vt vote (id, v β ′′ ). • Once C 2 has finished simulating B 2 up to the point B 2 has simulated A 2 and obtained a board BB ′ a , it draws at random a number k ∈ 1, l Recall that l is the number of different ids O p,c vote has been called on, and is also the number of additional calls to O p,c vote B will make. C then simulates the first k -1 calls to O p,c vote (id, v 0 , v 1 ), again by calling O vt vote (id, v β ′′ ). It obtains k -1 ballots, and stores them in a board BB b = [(id 1 , b 1 ), . . . , (id k -1 , b k -1 )]. If the kth call is O p,c vote (id, v 0 , v 1 ), C returns (BB ′ a ⊎ BB b , id, v β ′′ ).

= 1 .= 1 ,

 11 vote by B: b k = Vote(id k , cred id k , pk, v β ) for some v β . Thus, provided C correctly guessesβ ′′ = β and k, C returns (BB ′ a ⊎ [b 1 , . . . , b k -1 ], id k , v β )the conditions on BB in Exp ValidTally C holds, and thus Exp ValidTally C Therefore, ValidTally(BB a , sk, U 1 ) holds and ValidTally(BB a ⊎ BB b , sk, U 1 ∪ U 2 ) does not with probability at most 2l P Exp ValidTally C which is smaller than 2q(λ) P Exp ValidTally C= 1 since l ≤ q(λ).Since BB ′ a only contains ballots cast for identities in U 1 (by definition) and BB b for identities in U 2 , andU 1 ∩ U 2 = ∅, if ValidTally(BB ′ a ⊎ BB b , sk, U 1 ∪ U 2 ),by assumption 1 we have (regardless of β) r = Tally(BB, sk, U) = Tally(BB ′ a ⊎ BB b , sk, U) = Tally(BB ′ a , sk, U) * Tally(BB b , sk, U)

1 .

 1 priv-careful, β B ; -or when A does not block, the previous test succeeds, and∃V c . r = ρ(Voted) * ρ(V c ). Assume ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB ′ a ⊎ BB b , sk, U),which, as we have established, holds except with probability at most 2q(λ) P Exp ValidTally C = We have already established that the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds in Exp priv-careful, β B if and only if it succeeds in Exp verif-careful A .

= 1 - 1 . ( 4 )• 1 .

 1141 priv-careful,0 B (λ) = 1 if and only if either A (simulated by B) blocks; -or the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H fails in Exp verif-careful A ; -or the tally returns ⊥; -or A does not block, the previous test succeeds, the tally does not return ⊥, and Exp verif-careful A (λ) does not return 1. Since Exp verif-careful A (λ) also does not return 1 when A blocks, or when the test fails, or when the tally returns ⊥, this implies that, unless the implication ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB ′ a ⊎ BB b , sk, U) is false, P Exp verif-careful A (λ) 1 ≤ 2q(λ) P Exp ValidTally C = If β = 1: then Exp priv-careful,1 B (λ) = 1 if and only if B 4 (called on the result r ) returns 1 in this game, which happens either when A (simulated by B) blocks; -or when r = ⊥, i.e., as already mentioned, if the tally returns ⊥ or the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H fails in Exp priv-careful, β B ; -or when A does not block, the previous test succeeds, the tally returns r ⊥, and ∃V c . r = ρ(Voted) * ρ(V c ). Assume ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB ′ a ⊎ BB b , sk, U), which, as we have established, holds except with probability at most 2q(λ) P Exp ValidTally C = We have already established that the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds in Exp priv-careful, β B if and only if it succeeds in Exp verif-careful A .

  (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds in Exp verif-careful A . Therefore, unless the implication ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB ′ a ⊎ BB b , sk, U) is false, Exp priv,1 B (λ) = 1 if and only if either A (simulated by B) blocks; -or the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H fails in Exp verif-careful A ;or the tally returns ⊥;

  A, using oracles O reg and O corr . Let id 1 , . . . , id n be this first set of voters. B then registers another set of n voters id ′ 1 , . . . , id ′ n , where the id ′ i are fresh identities, that A does not use. B then simulates A, using the oracle O vote (id, v, v blank ), where v blank is a neutral vote. Once B is done simulating A, it triggers the new voters id ′ i to vote, by calling the oracle O

	p vote to simulate A's calls vote (id, v), B calls the oracle vote . Specifically, when A calls O v to O v O p

p vote

  . In the case of the first ballot, we adapt these definitions by replacing the oracles O v vote and Ovote , but keep only the first votes from each voter in the lists V 0 , V 1 , Voted, instead of the last. The following theorem corresponds to Theorem 4.4.• for id-based schemes, assuming that no polynomial adversary wins Exp ValidTally with non-negligible probability,• and for credential-based schemes, assuming that no polynomial adversary wins Exp NM with non-negligible probability,

	are analogous to O v vote and O	p vote with O v,f vote and O vote , described on Figure 12. These two oracles p,f
	Theorem B.1. Under assumptions 1, 2, 3, 4, 5, 6:
	if
	priv,0 ∀A. P Exp A

p

  (state 1 , pk) maintains a list L, initially empty, which will be used to record the calls to Ofor each call to O v vote (id, v), provided id ∈ U 1 , B calls O p vote (id, v, v neutral ), and, depending on the revote policy * either checks if id is already present in L, to add (id, v) to L only if it is not (note that, in case it is, O

	• B 2 O vote , O cast p current board BB ′ . B 2 first simulates A	O v vote , O cast 2	(state, pk):	p vote , and a representation of the

  C 1 is identical to B 1 . • C 2 first draws at random a bit β ′′ , and then simulates B 2 up to the point where B 2 has finished simulating A 2 . C 2 keeps a list BB, initially empty. It simulates each call to O p vote (id, v 0 , v 1 ) B does by calling O vt vote (id, v β ′′ ), and appending the obtained ballot to BB. It simulates each call to O cast (id, b) by appending b to BB, provided id is dishonest and Valid(id, b, BB, pk). • Once C 2 has finished simulating B 2 , it draws at random a number k ∈ 1, l Recall that l is the number of different ids O

	p vote (and thus
	O vt vote ) has been called on, and is also the number of additional calls to O

p vote B will make. Note that, at this point, BB in Exp ValidTally C is the same as BB a in Exp priv, β ′′ B . C then simulates the first k -1 calls to O p vote (id, v 0 , v 1 ), again by calling O vt vote

  , pk) maintains a list L, initially empty, which will be used to record the calls to O Depending on the revote policy, B 2 -either checks if id is already present in L, to add (id, v, b) to L only if it is not, if the revote policy is "first" (note that in this case, O or adds (id, v, b) to L and removes any previous entry (id, v ′ , b ′ ) (for any v ′ , b ′ ) from L, if the revote policy is "last" (note that in this case, O The simulated A 2 returns a board BB a and a state state ′ 2 . Let BB ′ a be the list of ballots in BB a that A 2 was allowed to cast, i.e. BB ′If at any point during the simulationA 2 blocks or fails, B stops the simulation, and lets BB a be the list of ballots in L, i.e. [b for (id, v, b) ∈ L]. vote (id l , v neutral , v l ), where v 1 , . . . , v l are the elements of Voted, and id 1 , . . . , id l are pairwise distinct identities from U 2 . Note that since all identities in L are distinct and in U 1 , l is indeed smaller than |U 1 | = |U 2 |. B 2 thus obtains l ballots b 1 , . . . , b l , for v neutral if β = 0 and v 1 , . . . , v l if β = 1. Let BB b be the list of these ballots. Let then BB = BB ′ a ⊎ BB b . B 2 then returns a state 2 indicating whether A 2 has failed, and the board BB. Intuitively, A is accurately simulated only if β = 0, i.e. is actually provided with ballots for the votes it wanted to cast. Hence whenever A wins Exp verif-careful , the simulated A 2 failing can only mean that β = 1. 3 then calls O happy BB (id i ) for each i ∈ 1, l . Since BB ′ a only contains ballots b such that open id (b) ∈ U 1 (by definition), only BB b

	• B 2 O vote p,c For each call to O v,c (state 1 p,c vote . B 2 first simulates A	O v,c vote 2	(state, pk).
	p,c vote indeed returns a ballot);
	In any case, B 2 calls O	p,c
	• B 3 O happy BB	(state 2 ) first simulates A	O happy BB 3	(state ′

vote (id, v), provided id ∈ U 1 , B calls O p,c vote (id, v, v neutral ) and (potentially) obtains a ballot b. p,c vote indeed returns a ballot). a = [b ∈ BB a |open id (b) ∈ U 1 ]. Let then Voted be the list of the votes in L: Voted = [v for (id, v, b) ∈ L]. vote (id 1 , v neutral , v 1 ), . . . , O p,c 2 ), unless A 2 has failed, in which case it simply calls O happy (open id (b)) for each b occurring in BB ′ a .

B

  vote has been called on for each id, and H is the list of identities O happy BB has successfully been called on. If H a and H b denote the value of the list H at this point respectively in Exp verif-careful , we have H b = H a ⊎ [id 1 , . . . , id l ]. Indeed: -we have established that H b contains id 1 , . . . , id l , -and for all (id, cred) ∈ U 1 , id ∈ H b if and only if O happy BB (id) has been called by B and VerifVoter(id, cred, L id , BB) succeeds, i.e. if and only if O happy BB a (id) was called by the simulated A and VerifVoter(id, cred, L id , BB) succeeds. Since BB = BB ′ a ⊎ BB b , and given the definition of BB b , by assumption 8, VerifVoter(id, cred, L id , BB) is equivalent to VerifVoter(id, cred, L id , BB ′ a ), which is itself equivalent to VerifVoter(id, cred, L id , BB a ). Thus id ∈ H b if and only if id ∈ H a . Therefore, the test ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H succeeds in Exp verif-careful A if and only if it succeeds in Exp priv-careful, β B .

	p,c
	A	priv-careful, β and Exp B

  For any β, assume ValidTally(BB a , sk, U 1 ) holds and ValidTally(BB ′ a ⊎ BB b , sk, U 1 ∪ U 2 ) does not. Thus, by assumptions 3 and 2,ValidTally(BB ′ a ⊎ BB b , sk, U 1 ∪ [(id 1 , cred id 1 ), . . . , (id l , cred id l )]) does not hold either, but ValidTally(BB ′ a , sk, U 1 ) does. Hence, there exists a smallest k ∈ 1, l such that ValidTally(BB ′ a ⊎[b 1 , . . . , b k -1 ], sk, U 1 ∪U ′ 2 ) holds and ValidTally(BB ′ a ⊎[b 1 , . . . , b k ], sk, U 1 ∪U ′ 2 ∪[(id k , cred id k )]) does not, where U ′ 2 = [(id 1 , cred id 1 ), . . . , (id k -1 , cred id k -1 )]. b k was produced by the kth call to O

ACKNOWLEDGMENTS

The authors would like to thank the anonymous reviewers as well as the shepherd, whose helpful comments and suggestions greatly contributed to clarify the notions presented in the paper. This work has been partially supported by the European Research Council (ERC) under the European Union's Horizon 2020 research (grant agreement No 645865-SPOOC).

Hence Exp priv,0 B (λ) = 1 if and only if either A (simulated by B) blocks, or constructs a board whose tally is ⊥, or it does not and

Exp verif

A (λ) 1. Since Exp verif A (λ) also does not return 1 when A blocks or when the tally is ⊥, this implies that, unless the implication ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB a ⊎ BB b , sk, U) is false, Exp

• If β = 1: then Exp priv,1 B

(λ) = 1 if and only if B 3 returns 1 in this game, which happens either when A (simulated by B) blocks, or when it does not and ∃V c . r = ρ(Voted) * ρ(V c ) or r = ⊥. Assume ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB a ⊎ BB b , sk, U), which, as we have established, holds except with probability at most 2q(λ) P Exp ValidTally C = 1 . Let us first examine the case where A does not block and r ⊥. As in the β = 0 case, we thus have r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U). Since β = 1, BB b contains ballots for v 1 , . . . , v l , i.e. for Voted. Hence, by assumption 4, Tally(BB b , sk, U) = ρ(Voted), and therefore r = Tally(BB a , sk, U 1 ) * ρ(Voted). By definition of Tally, there exists V such that Tally(BB a , sk, U 1 ) = ρ(V ). Hence the condition ∃V c . r = ρ(Voted) * ρ(V c ) necessarily holds.

Therefore, unless the implication ValidTally(BB a , sk, U 1 ) ⇒ ValidTally(BB a ⊎ BB b , sk, U) is false, Exp priv,1 B (λ) = 1 if and only if either A (simulated by B) blocks, or it does not and returns a board whose tally is ⊥, or it does not and returns a board whose tally is not ⊥.

We thus have, using 4 and 5: The proof for the case of credential-based protocols is very similar. In that case, instead of the Exp ValidTally assumption, we assume that

where Exp NM is defined on Figure 7.

Let A = A 1 , A 2 be an adversary that breaks individual verifiability, i.e. wins Exp verif . We construct the adversary B, that plays Exp priv , as in the id-based case. We also construct D, that plays Exp NM , and is similar to C in the id-based case, except that D simulates calls to O ). Since BB a is obtained by simulating A, which is polynomial, in all executions of D the length of BB a is bounded by some polynomial p(λ). D then draws at random a ballot in BB a , and returns it. Similarly to the proof for the id-based case, and keeping the same notations, it then follows that BB a contains a ballot with a credential in U 2 the same credential with probability at most 2p(λ) P Exp NM D = 1 . Indeed, if such a ballot exists, it cannot have been produced by a call to O c . Otherwise, it would necessarily have been produced by O c (id, v) for some id, v such that (id, cred) ∈ U 2 , and the only calls to this oracle simulate calls made by B to O p vote when simulating A. Since B only calls O p vote on ids in U 1 when simulating A, this is contradictory. Thus, a ballot in BB a with a credential in U 2 cannot have been produced by O c . Hence, provided D picked β ′′ = β, and picks the right ballot in BB a , which happens with probability at least 1 p(λ) , D wins Exp NM . Therefore, BB a contains no ballot with a credential in U 2 , except with probability at most 2p(λ) P Exp NM D (λ) = 1 .

(state, pk)

where

return b where (id, cred id ) ∈ U and Voted ′ is obtained from

Voted by removing all instances of (id, * )

Figure 13: Individual verifiability against a dishonest board with careful voters.

Note that by construction, all ballots in BB b have credentials in U 2 . Consequently, unless BB a contains a ballot with a credential in U 2 , by assumption 1, we have (regardless of β) r = Tally(BB, sk, U) = Tally(BB a ⊎ BB b , sk, U) = Tally(BB a , sk, U) * Tally(BB b , sk, U) which means, by assumption 3, that r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U).

The remainder of the proof is the same as before, and establishes that

Thus if A breaks verifiability, i.e. if P Exp verif A (λ) = 1 is not negligible, then B breaks privacy, or D breaks Exp NM , which proves the claim.

Note that, in these reductions, for each id in U We consider the case of protocols where the revote policy is to count only the last ballot (for each id or credential) or the first ballot. In the case of the last ballot, the definitions of the privacy game with a dishonest board and careful voters can be found on Figure 9. We adapt the verifiability game to the case of a dishonest board and careful voters as follows.

Definition B.2 (Individual verifiability against a dishonest board with careful voters). For an adversary A = A 1 , A 2 and a parameter λ, we consider the game Exp verif-careful A (λ) defined on Figure 13. The voting system is verifiable against a dishonest board with careful voters if

In the case of the first ballot, we adapt these definitions by replacing the oracles O

We thus have, using 4 and 5: The proof for the case of credential-based protocols is very similar. In that case, we assume that

A 3 be an adversary that breaks individual verifiability, i.e. wins Exp verif-careful . We construct the adversary B, that plays Exp priv-careful , as in the id-based case. However, contrary to the id-based case, B does not remove any ballots from BB a , and simply uses BB ′ a = BB a . We also construct ). Since BB a is obtained by simulating A, which is polynomial, in all executions of D the length of BB a is bounded by some polynomial p(λ). D then draws at random a ballot in BB a , and returns it. Similarly to the proof for the id-based case, and keeping the same notations, it then follows that BB a contains a ballot with a credential in U 2 the same credential with probability at most 2p(λ) P Exp NM D = 1 . Indeed, if such a ballot exists, it cannot have been produced by a call to O c . Otherwise, it would necessarily have been produced by O c (id, v) for some id, v such that (id, cred) ∈ U 2 , and the only calls to this oracle simulate calls made by B to O p,c vote when simulating A. Since B only calls O p,c vote on ids in U 1 when simulating A, this is contradictory. Thus, a ballot in BB a with a credential in U 2 cannot have been produced by O c . Hence, provided D picked β ′′ = β, and picks the right ballot in BB a , which happens with probability at least 1 p(λ) , D wins Exp NM . Therefore, BB a contains no ballot with a credential in U 2 , except with probability at most 2p(λ) P Exp NM D (λ) = 1 . Note that by construction, all ballots in BB b have credentials in U 2 . Consequently, unless BB a contains a ballot with a credential in U 2 , by assumption 1, we have (regardless of β) r = Tally(BB, sk, U) = Tally(BB a ⊎ BB b , sk, U) = Tally(BB a , sk, U) * Tally(BB b , sk, U) which means, by assumption 3, that r = Tally(BB a , sk, U 1 ) * Tally(BB b , sk, U).

The remainder of the proof is the same as before, and establishes that if A breaks verifiability with careful voters, i.e. if P Exp verif-careful

is not negligible, then B breaks privacy with careful voters, or D breaks Exp NM , which proves the claim.

Note that, in these reduction, for each id in U (pk) To prove that the protocols we study satisfy the different privacy properties, we will in some cases assume that no adversary wins Exp NM (presented on Figure 7) with non-negligible probability. We will also in some cases use the assumption that the ballot creation function has a property similar to the IND -CCA property i.e. that

where Exp ind is defined on Figure 15. This definition assumes a function open(b, sk, U) that returns the vote contained in the ballot b, i.e. for all election keys (pk, sk) and list of users and credentials U,

C.2 Proofs

C.2.1 Civitas is private for Exp priv .

Theorem C.1. Assuming no adversary wins Exp ind nor Exp NM with non-negligible probability, Civitas is private for Exp priv .

Proof. Let A = A 1 , A 2 , A 3 be an adversary that wins Exp priv . We consider an adversary B = B 1 , B 2 that plays Exp ind :

(pk), i.e. B registers and corrupts the same identities as A, while keeping lists U 1 , CU 1 of the identities it declares and corrupts by calling O reg and O corr . A returns some state ′ 1 . B 1 then corrupts each user A 1 has registered, i.e., B 1 calls O corr (id) for each id A 1 has declared, and stores each id's credential in a list CU 2 .

(state 1 , pk) maintains lists V 0 , V 1 , BB, initially empty, which will be used to simulate the lists with the same name in Exp priv . B 2 will also use lists hL, cL, initially empty.

for each call to O cast (id, b), provided id ∈ CU 1 and Valid(id, b, BB, pk), B appends b to BB, and to cL. We write cL\hL (resp. cL ∩ hL) the sublist of cL (in the same order) of ballots that do not occur (resp. do occur) in hL. Note that the lists BB, V 0 , V 1 in B are equal to the lists of the same name in Exp priv, β A

. Then, by construction, A 2 is always accurately simulated by B 2 , i.e. it is called on the same inputs, shown the same board, and provided with the same oracles as what would happen in Exp priv, β A . We also construct an adversary C, that plays the game Exp NM .

• C 1 simulates A 1 , similarly to B 1 . However, unlike B 1 , it stops there, and does not corrupt all identities.

• C 2 first draws at random a bit β ′′ , Similarly to B 2 , C 2 then simulates A 2 and uses lists BB, cL, hL, V:

- Note that the lists BB, cL, hL are the same for C in Exp NM at the point C 2 returns, and for B in Exp ind at the point B 2 returns. Similarly V in C is the same as V β ′′ in B. Let us also notice that hL in C is equal to the list L in the game Exp NM .

We will now prove that if A breaks privacy, then B wins Exp ind provided C does not win Exp NM .

The adversary C is polynomial, i.e. there exists a polynomial q(λ) bounding its number of operations. q(λ) necessarily also bounds the length of the list cL that C uses.

For any β, assume cL\hL contains a ballot b such that there exists a honest ( * , cred) , that is, when ρ(V 0 ) = ρ(V 1 ); and it is provided with the actually tally of the board BB (which A 2 interacted with).

Indeed, by construction of B 2 , BB = hL ⊎ cL is an interleaving of the ballots from hL and cL.

By assumption, cL\hL contains no ballot from honest credentials, while by construction hL (and thus cL ∩ hL) only contains ballots from honest credentials. Hence, the list BB d of ballots in BB associated with dishonest credentials is cL\hL (in that order). The list BB h of ballots in BB associated with honest credentials is an interleaving of the ballots from the lists hL and cL ∩ hL. However, by construction, hL contains at most one ballot for each credential. Thus, BB h also contains at most one distinct ballot (of which there can be several copies) for each credential. The list of distinct ballots in BB h (not necessarily in the same order) is thus hL.

The revote policy specified for Civitas is to count only the first ballot corresponding to each credential. Since BB can be separated into the lists BB h and BB d (whose ballots do not share any credential, by definition), and since the ballots of each of these two lists occur in the same order in BB, we have Tally(BB, sk, U 1 ) = Tally(BB h , sk, U 1 ) * Tally(BB d , sk, U 1 ) = Tally(hL, sk, U 1 ) * Tally(cL\hL, sk, U 1 ).

hL contains ballots for either the votes in V 0 or those in V 1 , depending on β. Since at that point ρ(V 0 ) = ρ(V 1 ), we have ρ(V 0 ) = Tally(hL, sk, U 1 ). In addition, the oracle O i d returns the list L of the credentials and votes of each ballot in cL\hL. Since L ′ is the list of the first vote for each credential in L, we thus have Tally(cL\hL, sk, U 1 ) = ρ(L ′ ). Therefore, ρ(V 0 ) * ρ(L ′ ), which is the result computed by B 2 , is indeed Tally(BB, sk, U 1 ), which concludes the proof that A 3 is accurately simulated by B 2 .

Hence, unless cL\hL contains a ballot associated with a honest credential, Exp

We thus have: 29

(state 1 , pk) maintains lists V 0 , V 1 , BB, initially empty, which will be used to simulate the lists with the same name in Exp priv-careful . B 2 will also use lists hL, H, and a list L id for each id ∈ U 1 , all of them initially empty. . For each call to O happy BB (id), provided id ∈ U 1 \CU 1 , following the specification of the voter verification for Civitas, B checks whether the first ballot b in L id is in BB (note that by definition of the oracles, L id actually only contains a single element). If so, B appends id to H. In any case, B then resumes the execution of A 3 .

• B 2 then computes ρ(V 0 ), ρ(V 1 ), and checks that they are equal, and that every id occurring in V 0 , V 1 is also an element of H. If so, B 2 computes r = ρ(V 0 ) * ρ(L ′ ). Otherwise, B 2 lets r = ⊥. • B 2 then calls A 4 on r , and obtains a bit β ′ . B 2 returns β ′ .

Note that the lists BB, V 0 , V 1 , H in B are equal to the lists of the same name in Exp priv-careful, β A . Then, by construction, A 2 is always accurately simulated by B 2 , i.e. it is called on the same inputs, and provided with the same oracles as what would happen in Exp priv, β A . Given the specification of VerifVoter for Civitas, A 3 is also accurately simulated by B 2 .

We also construct an adversary C, who plays the game Exp NM .

• C 1 simulates A 1 , similarly to B 1 . However, unlike B 1 , it stops there, and does not corrupt all identities.

• C 2 first draws at random a bit β ′′ , Similarly to B 2 , C 2 then simulates A 2 and uses lists hL, V. For each call to O p,c vote (id, v 0 , v 1 ), provided id ∈ U 1 \CU 1 does not already occur in V, C calls O c (id, v β ′′ ). C obtains a ballot b and appends (id, v β ′′ ) to V, and b to hL. Finally C returns b.

• A 2 eventually returns a board BB. C then draws at random a ballot of BB and returns it. Note that the lists BB, hL, are the same for C in Exp NM at the point C 2 returns, and for B in Exp ind at the point the simulated A 2 returns. Similarly V in C is the same as V β ′′ in B. Let us also notice that hL in C is equal to the list L in the game Exp NM .

We will now prove that if A wins Exp priv-careful , then B wins Exp ind provided C does not win Exp NM .

The adversary C is polynomial, i.e. there exists a polynomial q(λ) bounding its number of operations. q(λ) necessarily also bounds the length of the board BB that C computes. Let us then show that A 4 is accurately simulated by B 2 , i.e. it is provided by B 2 with the same input as when it is called in Exp priv, β A

, that is the actual tally of the board BB (which

It is clear from the definition of B that when either the equality condition ρ(V 0 ) = ρ(V 1 ) or the voter verification condition ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H do not hold, A 4 is indeed given ⊥ as an argument.

Let us now study the case where both these conditions are met. Among the ballots in BB, some are also in the list hL of ballots created by the oracle O i c . We will thus see BB as an interleaving (BB\hL) ⊎ (BB ∩ hL) of the ballots in BB\hL and BB ∩ hL (keeping the same order within each of these two lists).

By assumption, BB\hL contains no ballot for honest credentials, whereas by construction hL (and thus BB ∩ hL) only contains ballots for honest credentials. In addition, by construction, hL contains at most one ballot for each credential. Thus, BB ∩ hL also contains at most one distinct ballot (of which there can be several copies) for each credential. The list of distinct ballots with honest credentials in BB (not necessarily in the same order) is thus a subset of hL.

Moreover, we assumed the voter verifications succeeded, i.e. ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H holds. By construction, each b ∈ hL was added when simulating a call to O p vote (id, v 0 , v 1 ) for some honest id ∈ U 1 \CU 1 and some v 0 , v 1 . Therefore (id, v 0 ) ∈ V 0 , (id, v 1 ) ∈ V 1 , and

Hence, id ∈ H. By definition of B (which performs the voter verifications), this means that b is in BB.

Consequently, all ballots in hL are also in BB. Thus the list of distinct ballots with honest credentials in BB (not necessarily in the same order) is actually equal to hL.

The revote policy specified for Civitas is to count only the first ballot corresponding to each credential. Since BB can be separated into the lists BB\hL and BB ∩ hL (whose ballots do not share any credential, by assumption), and since the ballots of each of these two lists occur in the same order in BB, we have Tally(BB, sk, U 1 ) = Tally(BB ∩ hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ).

Then, by the previous observation that the list of distinct ballots in BB ∩ hL is hL (regardless of the order, which does not matter since all ballots in hL have distinct credentials by construction):

Tally(BB, sk, U 1 ) = Tally(hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ).

By construction, hL contains ballots for either the votes in V 0 or those in V 1 , depending on β. Since at that point ρ(V 0 ) = ρ(V 1 ), we have ρ(V 0 ) = Tally(hL, sk, U 1 ). In addition, the oracle O i d returns the list L of the credentials and votes of each ballot in BB\hL. Since L ′ is the list of the first vote for each credential in L, we thus have Tally(BB\hL, sk, U 1 ) = ρ(L ′ ). Therefore, ρ(V 0 ) * ρ(L ′ ), which is the result computed by B 2 , is indeed Tally(BB, sk, U 1 ), which concludes the proof that A 4 is accurately simulated by B 2 .

Hence, unless cL\hL contains a ballot associated with a honest credential, Exp

We thus have: (pk), i.e. B registers and corrupts the same identities as A, while keeping lists U 1 , CU 1 of the identities it declares and corrupts by calling O reg and O corr . A returns some state ′ 1 . B 1 then corrupts each user A 1 has registered, i.e., B 1 calls O corr (id) for each id A 1 has declared, and stores each id's credential in a list CU 2 .

(state 1 , pk) maintains lists V 0 , V 1 , BB, initially empty, which will be used to simulate the lists with the same name in Exp priv-careful . B 2 will also use lists hL, H, and a list L id for each id ∈ U 1 , all of them initially empty.

vote (id, v 0 , v 1 ), provided id ∈ U 1 \CU 1 , B retrieves id's credential id from CU 2 , and calls O i c (id, cred id , v 0 , v 1 ). B obtains a ballot b. B then removes from V 0 and V 1 all elements of the form (id, * ), and appends (id, v 0 ) to V 0 , (id, v 1 ) to V 1 , b to hL, and b to L id . Finally B returns b to A. A 2 eventually returns a board BB. We write BB\hL (resp. BB ∩ hL) the sublist of BB (in the same order) of ballots that do not occur (resp. do occur) in hL.

, and obtains a list L of pairs of credentials and votes. B 2 then computes the list L ′ of the last vote for each credential in L. We will see later that under the right assumptions, O i d accepts to open all (valid) ballots in BB\hL.

• B 2 then simulates A O happy BB 3

. For each call to O happy BB (id), provided id ∈ U 1 \CU 1 , following the specification of the voter verification for Belenios, B retrieves id's credential cred from CU 2 , and checks whether the last ballot b in L id is the last ballot associated to cred (i.e. signed by cred) in BB. If so, B appends id to H. In any case, B then resumes the execution of A 3 .

• B 2 then computes ρ(V 0 ), ρ(V 1 ), and checks that they are equal, and that every id We also construct an adversary C, who plays the game Exp NM .

• C 1 simulates A 1 , similarly to B 1 . However, unlike B 1 , it stops there, and does not corrupt all identities.

• C 2 first draws at random a bit β ′′ , Similarly to B 2 , C 2 then simulates A 2 and uses lists hL, V. For each call to

. C obtains a ballot b, removes all elements of the form (id, * ) from V, and appends (id, v β ′′ ) to V, and b to hL. Finally C returns b.

• A 2 eventually returns a board BB. C then draws at random a ballot of BB and returns it. Note that the lists BB, hL are the same for C in Exp NM at the point C 2 returns, and for B in Exp ind at the point the simulated A 2 returns. Similarly V in C is the same as V β ′′ in B. Let us also notice that hL in C is equal to the list L in the game Exp NM .

We will now prove that if A wins Exp priv-careful , then B wins Exp ind provided C does not win Exp NM .

The adversary C is polynomial, i.e. there exists a polynomial q(λ) bounding its number of operations. q(λ) necessarily also bounds the length of the board BB that C computes. For any β, Exp ind, β B (λ) = 1 if and only if B 2 returns 1 in this game. Assume BB\hL does not contain any ballot associated with a honest credential (i.e. a credential in U 1 \CU 1 ), which, as we have established, holds except with probability at most 2q(λ) P Exp NM C = 1 . 32

Note that this assumption notably implies that no ballot in BB\hL has the same ciphertext as a ballot generated by a call to O i c , that is, for all b ∈ BB\hL, extract(b) L. Indeed, the ciphertext part of the ballot, for Belenios, is signed with the credential. Hence any c ∈ L is (by definition of O i c ) signed with a honest credential, which, by the assumption, is not the case of any of the ballots in BB\hL. Therefore, as stated earlier, O i d accepts to open all (valid) ballots in BB\hL.

Let us then show that A 4 is accurately simulated by B 2 , i.e. it is provided by B 2 with the same input as when it is called in Exp priv, β A

, that is the actually tally of the board BB (which

It is clear from the definition of B that when either the equality condition ρ(V 0 ) = ρ(V 1 )) or the voter verification condition ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H do not hold, A 4 is indeed given ⊥ as an argument.

Let us now study the case where both these conditions are met. Among the ballots in BB, some are also in the list hL of ballots created by the oracle O i c . We will thus see BB as an interleaving of the ballots in BB\hL and BB ∩ hL (keeping the same order within each of these two lists).

By assumption, BB\hL contains no ballot for honest credentials, whereas by construction hL (and thus BB ∩ hL) only contains ballots for honest credentials.

Moreover, we assumed the voter verifications succeeded, i.e. ∀id. (id, * ) ∈ V 0 , V 1 ⇒ id ∈ H holds. According to the specification of VerifVoter for Belenios, this means that for all id occurring in V 0 , V 1 , the last ballot b in L id , i.e. the last ballot produced by O p,c vote (id, * , * ), is also the last ballot signed by cred id in BB. (cred id being the credential associated with id in CU 2 ). Since id (and thus cred id ) is honest by definition of V 0 , V 1 , b is actually the last ballot signed by cred id in BB ∩ hL.

Consider a credential cred such that BB ∩ hL contains at least one ballot signed by cred. This ballot can only have been added to hL by a call to O p,c vote , and therefore, by definition of this oracle, the associated id was at one point added to V 0 and V 1 . Since no identity is ever removed from these lists, at the time of tallying, id still occurs in

Hence, the list hL ′ of the last ballots signed by each credential in BB ∩ hL is exactly the list of the last ballots produced by O p,c vote for each id in V 0 , V 1 . By construction, this list contains ballots for either the votes in V 0 or those in V 1 , depending on β. Since at that point ρ(V 0 ) = ρ(V 1 ), we have ρ(V 0 ) = Tally(hL ′ , sk, U 1 ). In addition, the revote policy specified for Belenios is to count only the last ballot signed by each credential. Therefore, Tally(BB ∩ hL, sk, U 1 ) = Tally(hL ′ , sk, U 1 ) = ρ(V 0 ).

Besides, the oracle O i

d returns the list L of the credentials and votes of each ballot in BB\hL. Since L ′ is the list of the last votes associated with each credential in L, we thus have Tally(BB\hL, sk, U 1 ) = ρ(L ′ ).

Since BB can be separated into the lists BB\hL and BB ∩ hL (whose ballots do not share any credential, by assumption), and since the ballots of each of these two lists occur in the same order in BB, we have Tally(BB, sk, U 1 ) = Tally(BB ∩ hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ) = ρ(V 0 ) * ρ(L ′ ).

Therefore, ρ(V 0 ) * ρ(L ′ ), which is the result computed by B 2 , is indeed Tally(BB, sk, U 1 ), which concludes the proof that A 4 is accurately simulated by B 2 .

Hence, unless BB\hL contains a ballot associated with a honest credential, Exp

We thus have: (pk), i.e. B registers and corrupts the same identities as A, while keeping lists U 1 , CU 1 of the identities it declares and corrupts by calling O reg and O corr . A returns some state ′ 1 . B 1 then corrupts each user A 1 has registered, i.e., B 1 calls O corr (id) for each id A 1 has declared, and stores each id's credential in a list CU 2 .

(state 1 , pk) maintains lists V 0 , V 1 , BB, initially empty, which will be used to simulate the lists with the same name in Exp priv . B 2 will also use a list hL, initially empty.

1 , pk): -for each call to O p vote (id, v 0 , v 1 ), provided id ∈ U 1 \CU 1 , B retrieves id's credential cred id from CU 2 , and calls O i c (id, cred id , v 0 , v 1 ). B obtains a ballot b. B then removes from V 0 and V 1 all elements of the form (id, * ), and appends (id, v 0 ) to V 0 , (id, v 1 ) to V 1 , b to hL and to BB. Let us then show that A 3 is accurately simulated by B 2 , i.e. it is simulated by B 2 only when it is called in Exp priv, β A (that is, when ρ(V 0 ) = ρ(V 1 )); and it is provided with the actually tally of the board BB (which A 2 interacted with).

It is clear from the construction of B that if ρ(V 0 ) ρ(V 1 ), A By assumption, BB contains no duplicate ciphertexts. Hence, the lists BB h and BB d do not have any identity or ciphertexts in common, and according to the specification of Helios we have Tally(BB, sk, U 1 ) = Tally(BB h , sk, U 1 ) * Tally(BB d , sk, U 1 ) = Tally(hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ).

By construction of B 2 , the list of the last ballot associated with each honest id in hL contains ballots for either the votes in V 0 or those in V 1 , depending on β. Since at that point ρ(V 0 ) = ρ(V 1 ), we thus have ρ(V 0 ) = Tally(hL, sk, U 1 ).

In addition, the oracle O i d returns the list L of the votes of each ballot in BB\hL. Since L ′ is the list of the last vote in L associated in BB\hL to each id, we thus have Tally(BB\hL, sk, U 1 ) = ρ(L ′ ).

Therefore, we indeed have Tally(BB, sk, U 1 ) = Tally(hL, sk, U

We thus have:

Therefore (state 1 , pk) maintains lists V 0 , V 1 , BB, initially empty, which will be used to simulate the lists with the same name in Exp priv . B 2 will also use a list hL, initially empty. Let us then show that A 3 is accurately simulated by B 2 , i.e. it is simulated by B 2 only when it is called in Exp priv, β A (that is, when ρ(V 0 ) = ρ(V 1 )); and it is provided with the actually tally of the board BB (which A 2 interacted with).

It is clear from the construction of B that if ρ(V 0 ) ρ(V 1 ), A By assumption, BB contains no duplicate ballots. Hence, the lists hL and BB\hL do not have any ballot in common, and according to the specification of Simple we have Tally(BB, sk, U 1 ) = Tally(hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ). By construction of B 2 , the list hL contains ballots for either the votes in V 0 or those in V 1 , depending on β. Since at that point ρ(V 0 ) = ρ(V 1 ), we thus have ρ(V 0 ) = Tally(hL, sk, U 1 ).

In addition, the oracle O i d returns the list L of the votes of each ballot in BB\hL. We thus have Tally(BB\hL, sk, U 1 ) = ρ(L). Therefore, we indeed have Tally(BB, sk, U 1 ) = Tally(hL, sk, U 1 ) * Tally(BB\hL, sk, U 1 ) = ρ(V 0 ) * ρ(L), which is the result computed by B 2 . This concludes the proof that A