Ballot secrecy: Security definition,sufficient conditions,and analysis of Helios

Abstract

We propose a definition of ballot secrecy as an indistinguishability game in the computational model of cryptography. Our definition improves upon earlier definitions to ensure ballot secrecy is preserved in the presence of an adversary that controls ballot collection. We also propose a definition of ballot independence as an adaptation of an indistinguishability game for asymmetric encryption. We prove relations between our definitions. In particular, we prove ballot independence is sufficient for ballot secrecy in voting systems with zero-knowledge tallying proofs. Moreover, we prove that building systems from non-malleable asymmetric encryption schemes suffices for ballot secrecy, thereby eliminating the expense of ballot-secrecy proofs for a class of encryption-based voting systems. We demonstrate applicability of our results by analysing the Helios voting system and its mixnet variant. Our analysis reveals that Helios does not satisfy ballot secrecy in the presence of an adversary that controls ballot collection. The vulnerability cannot be detected by earlier definitions of ballot secrecy, because they do not consider such adversaries. We adopt non-malleable ballots as a fix and prove that the fixed system satisfies ballot secrecy.

Keywords

Anonymity democracy elections Helios independence non-malleability privacy secrecy voting

1. Introduction

An election is a decision-making procedure to choose representatives [4,68,90,110]. Choices should be made by voters with equal influence, and this must be ensured by voting systems, as prescribed by the United Nations [138], the Organisation for Security & Cooperation in Europe [101], and the Organization of American States [102]. Historically, “Americans [voted] with their voices – viva voce – or with their hands or with their feet. Yea or nay. Raise your hand. All in favor of Jones, stand on this side of the town common; if you support Smith, line up over there” [89]. Thus, ensuring that only voters voted and did so with equal influence was straightforward. Indeed, the election outcome could be determined by anyone present, simply by considering at most one vote per voter and disregarding non-voters. Yet, voting systems must also ensure choices are made freely, as prescribed by the aforementioned organisations [101,102,138]. Mill eloquently argues that choices cannot be expressed freely in public: “The unfortunate voter is in the power of some opulent man; the opulent man informs him how he must vote. Conscience, virtue, moral obligation, religion, all cry to him, that he ought to consult his own judgement, and faithfully follow its dictates. The consequences of pleasing, or offending the opulent man, stare him in the face...the moral obligation is disregarded, a faithless, a prostitute, a pernicious vote is given” [95].

The need for free-choice started a movement towards voting as a private act, i.e., “when numerous social constraints in which citizens are routinely and universally enmeshed – community of religious allegiances, the patronage of big men, employers or notables, parties, ‘political machines’ – are kept at bay,” and “this idea has become the current doxa of democracy-builders worldwide” [23]. The most widely used embodiment of this idea is the Australian system, which demands that votes be marked on uniform ballots in polling booths and deposited into ballot boxes. Uniformity is intended to enable free-choice during distribution, collection and tallying of ballots, and the isolation of polling booths is intended to facilitate free-choice whilst marking.1

¹
Earlier systems merely required ballots to be marked in polling booths and deposited into ballot boxes, which permitted non-uniform ballots, including ballots of different colours and sizes, that could be easily identified as party tickets [29].

Moreover, the Australian system can assure that only voters vote and do so with equal influence. Indeed, observers can check that ballots are only distributed to voters and at most one ballot is deposited by each voter. Furthermore, observers can check that spoiled ballots are discarded and that votes expressed in the remaining ballots correspond to the election outcome. Albeit, assurance is limited by an observer’s ability to monitor [24,79,100] and the ability to transfer that assurance is limited to the observer’s “good word or sworn testimony” [98].

Since the paper-based Australian system’s introduction, electronic voting systems have emerged. Unfortunately, these electronic systems are routinely broken in ways that violate free-choice, e.g., [28,65,85,133,143,144], or permit undue influence, e.g., [28,31,75,85,137]. Breaks can be avoided by proving that systems satisfy formal notions of voters voting freely and of detecting undue influence. Universal verifiability formalises the latter notion, and we propose a definition of ballot secrecy that formalises the former. Our definition is presented in the computational, game-based model of cryptography, whereby a benign challenger, a malicious adversary and a voting system engage in a series of interactions which task the adversary to break security.

Ballot secrecy formalises a notion of free-choice,2

Ballot secrecy and privacy occasionally appear as synonyms in the literature. We favour ballot secrecy to avoid confusion with other privacy notions, such as receipt-freeness and coercion resistance, which we will briefly discuss in Section 8.

assuming voters’ ballots are constructed and tallied in the prescribed manner.

Ballot secrecy. A voter’s vote is not revealed to anyone.

We capture ballot secrecy as a game that proceeds as follows. First, the adversary picks a pair of votes

v_{0}

and

v_{1}

. Secondly, the challenger constructs a ballot for vote

v_{β}

(in the manner prescribed by the voting system), where β is a bit chosen uniformly at random. That ballot is given to the adversary. The adversary and challenger repeat the process to construct further ballots, using the same bit β. Thirdly, the adversary constructs a set of ballots, which may include ballots constructed by the adversary and ballots constructed by the challenger. Thus, the game captures a setting where the adversary casts ballots on behalf of some voters and controls the votes cast by the remaining voters. Fourthly, the challenger tallies the set of ballots (in the manner prescribed by the voting system) to determine the election outcome, which is given to the adversary. Finally, the adversary is tasked with determining if

β = 0

β = 1

. To avoid trivial distinctions, we require that the aforementioned votes (controlled by the adversary) remain constant regardless of whether

β = 0

β = 1

. If the adversary wins the game, then a voter’s vote can be revealed, otherwise, it cannot, i.e., the voting system provides ballot secrecy. Our game improves upon games by Bernhard et al. [16,18,20,125,126] to ensure ballot secrecy is preserved in the presence of an adversary that controls ballot collection (i.e., the bulletin board and the communication channel), whereas games by Bernhard et al. do not.

Beyond ballot secrecy, voting systems should satisfy properties including universal verifiability, which requires systems to produce evidence that can be checked to determine whether votes expressed in ballots correspond to the election outcome, thereby enabling the detection of undue influence. Smyth, Frink & Clarkson [128] capture universal verifiability as a game that tasks the adversary to falsify evidence that causes checks to succeed when the outcome does not correspond to the votes expressed in collected ballots, or that cause checks to fail when the outcome does correspond to the votes expressed. Thus, winning the game signifies the existence of a scenario in which a spurious outcome will be accepted or a legitimate outcome rejected. By comparison, when no winning adversary exists, anyone can determine whether the election outcome is correct. Universal verifiability and ballot secrecy are orthogonal properties of voting systems that can be studied, formulated and analysed independently. We shall largely avoid discussion of verifiability, except to introduce general concepts, to highlight features needed solely for verifiability, and to simplify proofs.

We introduce two voting systems to demonstrate how ballot secrecy and universal verifiability can be achieved. The first ( $Nonce$ ) instructs each voter to cast a ballot comprising of their vote paired with a nonce (which is collected and stored on a bulletin board) and instructs the tallier to publish the election outcome corresponding to votes (stored on that board). The second ( $Enc 2 Vote$ ) instructs voters to cast asymmetric encryptions of their votes and instructs the tallier to decrypt the encrypted votes and publish the outcome corresponding to those votes. Universal verifiability is ensured by the former system, because anyone can recompute the election outcome to check that it corresponds to votes expressed in collected ballots. But, ballot secrecy is not, because voters’ votes are revealed. By comparison, secrecy is ensured by the latter system, because asymmetric encryption can ensure that votes cannot be recovered from ballots and the tallying procedure ensures that individual votes are not revealed. But, universal verifiability is not ensured. Indeed, spurious election outcomes need not correspond to the encrypted votes. Thus, $Enc 2 Vote$ ensures secrecy not verifiability, and $Nonce$ achieves the reverse. More advanced voting systems must simultaneously satisfy both secrecy and verifiability, and we will consider the Helios voting system.

Helios is an open-source, web-based electronic voting system [2], which has been used in binding elections. In particular, the International Association of Cryptologic Research (IACR) has used Helios annually since 2010 to elect board members [12,69],3

https://www.iacr.org/elections/, accessed 29 Mar 2019.

the Association for Computing Machinery (ACM) used Helios for their 2014 general election [134], the Catholic University of Louvain used Helios to elect their university president in 2009 [2], and Princeton University has used Helios since 2009 to elect student governments.4

⁴

http://heliosvoting.wordpress.com/2009/10/13/helios-deployed-at-princeton/ and https://princeton.heliosvoting.org/, accessed 29 Mar 2019.

Helios is intended to satisfy universal verifiability whilst maintaining ballot secrecy. For ballot secrecy, each voter is instructed to encrypt their vote using an asymmetric homomorphic encryption scheme. Encrypted votes are homomorphically combined and the homomorphic combination is decrypted to reveal the outcome. Alternatively, a mixnet is applied to the encrypted votes and the mixed encrypted votes are decrypted to reveal the outcome [1,30]. We continue to refer to the former voting system as Helios and, henceforth, refer to the latter variant as Helios Mixnet. For universal verifiability, the encryption step is accompanied by a non-interactive zero-knowledge proof demonstrating correct computation. This ensures homomorphic combinations of encrypted votes and mixed encrypted votes can be decrypted, hence, the outcome can be recovered. Helios additionally requires proof that ciphertexts encrypt votes. This prevents an adversarial voter crafting a ciphertext that could be combined with others to derive an election outcome in the voter’s favour. (E.g., votes might be switched between candidates.) The decryption step is similarly accompanied by a non-interactive zero-knowledge proof to prevent spurious outcomes.

Contribution and structure. Contributions are summarised in the bullet points below and described in detail by the surrounding text:

A definition of ballot secrecy that overcomes limitations of previous works by considering an adversary that controls ballot collection.

Section 3 briefly explains the pitfalls of existing ballot secrecy definitions, introduces our game-based definition of ballot secrecy, adapts formalisations of non-malleability and indistinguishability for asymmetric encryption to derive two equivalent game-based definitions of ballot independence, and proves relations between definitions. In particular, ballot independence is shown to be sufficient for ballot secrecy in a class of voting systems with zero-knowledge tallying proofs, and it is shown to be necessary, but not sufficient, in general.

A Helios case study that identifies an attack, which cannot be detected by previous work, and a proof that secrecy is satisfied after applying a fix.

Section 4 shows that our definition of ballot secrecy can be used to identify a known vulnerability in Helios, explains why earlier definitions of ballot secrecy by Bernhard et al. cannot detect that vulnerability, discusses non-malleable ballots as a fix, and uses our sufficient condition to prove that secrecy is satisfied when the fix is applied.

A proof that voting systems built from non-malleable encryption satisfy ballot secrecy if tallying is additive, which trivialises secrecy proofs.

Section 5 proves that ballot independence cannot be harmed by tallying, if all ballots are tallied correctly; shows that universally-verifiable voting systems tally ballots correctly; proves

Enc 2 Vote

satisfies ballot independence, assuming the underlying asymmetric encryption scheme is non-malleable; and combines those results to show that proofs of ballot secrecy are trivial for a class of universally-verifiable, encryption-based voting systems.

A Helios Mixnet case study that demonstrates the triviality of ballot secrecy proofs for systems built from non-malleable encryption.

Section 6 presents an analysis of Helios Mixnet and demonstrates that our results do indeed make proofs of ballot secrecy trivial, by showing that the combination of universal verifiability and non-malleable encryption suffice for ballot secrecy in Helios Mixnet. The remaining sections present syntax (§2), discussion, limitations, and directions for further research (§7), related work (§8), and a brief conclusion (§9); Sidebar 1 introduces game-based security definitions and recalls notation; and the appendices define cryptographic primitives and relevant security definitions (Appendix A) and present further supplementary material. (Readers familiar with games might like to skip Sidebar 1, and some readers might like to study the related work before our definition of ballot secrecy.)

Sidebar 1

Preliminaries: Games and notation

2. Election scheme syntax

We recall syntax (Definition 1) for voting systems that consist of the following three steps. First, a tallier generates a key pair. Secondly, each voter constructs and casts a ballot for their vote. These ballots are collected and recorded on a bulletin board. Finally, the tallier tallies the collected ballots and announces the outcome as a frequency distribution of votes. The chosen representative is derived from this distribution, e.g., as the candidate with the most votes.5

⁵
Smyth, Frink & Clarkson use the syntax to model first-past-the-post voting systems [128] and Smyth shows ranked-choice voting systems can be modelled too [118].

Definition 1 (Election scheme [128]).

An election scheme is a tuple of probabilistic polynomial-time algorithms $(Setup, Vote, Tally)$ such that:

$Setup$ , denoted $(pk, sk, mb, mc) \leftarrow Setup (κ)$ , is run by the tallier. The algorithm takes a security parameter κ as input and outputs a key pair $pk, sk$ , a maximum number of ballots $mb$ , and a maximum number of candidates $mc$ .

$Vote$ , denoted $b \leftarrow Vote (pk, v, nc, κ)$ , is run by voters. The algorithm takes as input a public key $pk$ , a voter’s vote v, some number of candidates $nc$ , and a security parameter κ. Vote v should be selected from a sequence $1, \dots, nc$ of candidates. The algorithm outputs a ballot b or error symbol ⊥.

$Tally$ , denoted $(v, pf) \leftarrow Tally (sk, bb, nc, κ)$ , is run by the tallier. The algorithm takes as input a private key $sk$ , a bulletin board $bb$ , some number of candidates $nc$ , and a security parameter κ, where $bb$ is a set. The algorithm outputs an election outcome $v$ and a non-interactive tallying proof $pf$ , where $v$ is a vector of length $nc$ and each index v of that vector should indicate the number of votes for candidate v.

Election schemes must satisfy correctness, that is, there exists a negligible function $negl$ , such that for all security parameters κ, integers $nb$ and $nc$ , and votes $v_{1}, \dots, v_{nb} \in {1, \dots, nc}$ , it holds that, given a zero-filled vector $v$ of length $nc$ , we have:

The syntax provides a language to model voting systems and the correctness condition ensures that such systems function, i.e., election outcomes correspond to votes expressed in ballots, when ballots are constructed and tallied in the prescribed manner.

The syntax focuses on minimalism, rather than generality: Algorithm $Setup$ naturally inputs a security parameter and outputs a key pair. In addition, the algorithm outputs bounds on the number of ballots $mb$ , respectively candidates $mc$ . These bounds broaden the correctness definition’s scope. Indeed, $Enc 2 Vote$ requires $mc$ to be less than or equal to the size of the underlying encryption scheme’s message space (otherwise decryption might not reveal voters’ votes). Helios additionally requires the same constraint on $mb$ (otherwise decryption of the homomorphic combination might not reveal the outcome). Algorithm $Vote$ naturally inputs a public key, a vote, and a security parameter, and outputs a ballot. The vote is expressed as an integer, rather than alphanumeric strings, for brevity. Beyond those inputs, the algorithm inputs a number of candidates $nc$ , which is necessary in voting systems such as Helios, because ballot construction depends on the number of candidates. Tallying is similarly dependent on the number of candidates in Helios, hence the inputs and outputs to algorithm $Tally$ are all natural. Finally, the syntax restricts bulletin boards to sets, rather than multisets or lists. This is a limitation: Sets preclude the construction of schemes vulnerable to attacks that arise due to duplicate ballots [21, §2.1 & §4.3]. Systems vulnerable to such attacks cannot be modelled using the syntax: Analysts must not abstract away the details of lists or multisets and model them as sets, since any ensuing analysis will miss attacks. Analysts may abstractly model lists or multisets as sets with some additional effort.

Election schemes may also include an algorithm $Verify$ , which is used to audit an election. We omit that algorithm from Definition 1, because we focus on ballot secrecy, rather than verifiability: Ballot secrecy must be upheld independently of auditing, since voters’ votes should not be revealed regardless of whether an election outcome is correct (i.e., regardless of whether auditing succeeds). Hence, algorithm $Verify$ must not be used to achieve privacy and can be omitted. Nonetheless, algorithm $Tally$ must output the tallying proof (that would be input to algorithm $Verify$ ), since tallying proofs can harm privacy. (For instance, as an extreme example, a tallying proof may include the private key, which can used to violate every voter’s privacy.)

Voting systems must ensure that outcomes only include votes cast by voters, as opposed to non-voters, and that only one vote of each voter has influence [93]. The former can be achieved by authentication. Traditionally, the latter was achieved by permitting each voter to cast at most one ballot, whereas more recent systems permit multiple ballots and count only the last. Our syntax is compatible with voting systems, such as Helios, that rely on trusted external authentication services to ensure that collected ballots satisfy these properties (i.e., collected ballots were cast by voters and contain at most one ballot per voter), hence, election schemes need not achieve these properties directly. (An extension of the syntax is compatible with voting systems that introduce voter credentials and use cryptography to achieve these properties directly [107,117,128].) Here be dragons: The security of external authentication services must be verified.

We will use our syntax to express a privacy property of election schemes, moreover, we will model and analyse voting systems, including Helios (§4) and Helios Mixnet (§6). Beyond those systems, it also captures Helios-C [43] and the system by Juels, Catalano & Jakobsson [77] (once extended to include voter credentials), so Belenios and Civitas should be included as well. These schemes are rather dominant in the literature, so the class is interesting and rather general. Notable voting systems that are excluded include: systems relying on features implemented with paper (e.g., [34,37,97]); systems which require partially private ballots (e.g., [96]); and schemes relying on partially honest bulletin boards (e.g., [41]). We also exclude distributed tallying. These limitations are further discussed in Section 7.

3. Privacy

Some scenarios inevitably reveal voters’ votes: Unanimous outcomes reveal how everyone voted and, more generally, outcomes can be coupled with partial knowledge of voters’ votes to deduce voters’ votes. For example, suppose Alice, Bob and Mallory participate in a referendum and the outcome has frequency two for ‘yes’ and one for ‘no.’ Mallory and Alice can deduce Bob’s vote by pooling knowledge of their own votes. Similarly, Mallory and Bob can deduce Alice’s vote. Furthermore, Mallory can deduce that Alice and Bob both voted yes, if she voted no. For simplicity, our informal definition of ballot secrecy (§1) deliberately omitted side-conditions which exclude these inevitable revelations and which are necessary for satisfiability.6

⁶
Voting systems that announce chosen representatives (e.g., [13,56,73,74]), rather than frequency distributions of votes, could offer stronger notions of privacy.

We now refine that definition as follows:

A voter’s vote is not revealed to anyone, except when the vote can be deduced from the election outcome and any partial knowledge of voters’ votes.

This refinement ensures the aforementioned examples are not violations of ballot secrecy. By comparison, if Mallory votes yes and she can deduce the vote of Alice, without knowledge of Bob’s vote, then ballot secrecy is violated.

We could formulate ballot secrecy as the following game: First, the adversary picks a pair of votes $v_{0}$ and $v_{1}$ . Secondly, the challenger constructs a ballot $b_{1}$ for vote $v_{β}$ and a second ballot $b_{2}$ for $v_{1 - β}$ , where β is a bit chosen uniformly at random. Those ballots are given to the adversary. Thirdly, the adversary constructs ballots $b_{3}, \dots, b_{n}$ . Fourthly, the challenger tallies all the ballots (i.e., $b_{1}, \dots, b_{n}$ ) to the determine the election outcome, which the adversary is given. Finally, the adversary is tasked with determining bit β. This game challenges the adversary to determine if the first ballot is for $v_{0}$ and the second is for $v_{1}$ , or vice-versa. Intuitively, a losing adversary cannot distinguish ballots; seemingly suggesting that Alice voting ‘yes’ is indistinguishable from Bob voting ‘no.’

The first release of Helios is not secure with respect to the aforementioned game, due to a vulnerability identified by Cortier & Smyth [46,47]. Indeed, an adversary can observe a ballot constructed by the challenger, compute a meaningfully related ballot (from a malleable Helios ballot), and exploit the relation to win the game. This vulnerability can be attributed to tallying meaningfully related ballots; omitting such ballots from tallying, i.e., ballot weeding, is postulated as a defence [16,17,46,47,119,125,127]. Variants of Helios with ballot weeding seem secure with respect to this game. Unfortunately, ballot weeding mechanisms can be subverted by intercepting ballots or by re-ordering ballots. Given that current definitions cannot detect such vulnerabilities (§8), we should conclude that they are unsuitable. Indeed, the challenger tallying all ballots introduces an implicit trust assumption: ballots are recorded-as-cast, i.e., cast ballots are preserved with integrity through the ballot collection process.7

⁷

The recorded-as-cast notion was introduced by Adida & Neff [3, §2].

Thus, vulnerabilities that manipulate the ballot collection process cannot be detected, including vulnerabilities that can be exploited to distinguish Alice voting ‘yes’ from Bob voting ‘no.’ To overcome this shortcoming, we formulate a new definition of ballot secrecy in which the adversary controls the ballot collection process, i.e., the bulletin board and the communication channel.

3.1. Ballot secrecy

We formalise ballot secrecy (Definition 2) as a game that tasks the adversary to: select two lists of votes; construct a bulletin board from ballots for votes in one of those lists, which list is decided by a coin flip; and (non-trivially) determine the result of the coin flip from the resulting election outcome and tallying proof. That is, the game tasks the adversary to distinguish between an instance of the voting system for one list of votes, from another instance with the other list of votes, when the votes cast from each list are permutations of each other (hence, the distinction is non-trivial). The game proceeds as follows: The challenger generates a key pair (Line 1), the adversary chooses some number of candidates (Line 2), and the challenger flips a coin (Line 3) and initialises a set to record lists of votes (Line 4). The adversary computes a bulletin board from ballots for votes in one of two possible lists (Line 5), where the lists are chosen by the adversary, the choice between lists is determined by the coin flip, and the ballots (for votes in one of the lists) are constructed by an left-right oracle (further ballots may be constructed by the adversary).8

⁸
Bellare et al. introduced left-right oracles in the context of symmetric encryption [6] and Bellare & Rogaway provide a tutorial on their use [9].

The challenger tallies the bulletin board to derive the election outcome and tallying proof (Line 6), which are given to the adversary and the adversary is tasked with determining the result of the coin flip (Line 7 & 8). Definition 2 (

Ballot - Secrecy

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $A$ be an adversary, κ be a security parameter, and $Ballot - Secrecy$ be the following game.

Predicate $balanced$ and oracle $O$ are defined as follows:

$balanced (bb, nc, L)$ holds if for all votes $v \in {1, \dots, nc}$ we have $| {b ∣ b \in bb \land \exists v_{1} . (b, v, v_{1}) \in L} | = | {b ∣ b \in bb \land \exists v_{0} . (b, v_{0}, v) \in L} |$ ; and

$O (v_{0}, v_{1})$ computes $b \leftarrow Vote (pk, v_{β}, nc, κ); L \leftarrow L \cup {(b, v_{0}, v_{1})}$ and outputs b, where $v_{0}, v_{1} \in {1, ..., nc}$ .

We say Γ satisfies

Ballot - Secrecy

, if for all probabilistic polynomial-time adversaries

A

, there exists a negligible function

negl

, such that for all security parameters κ, we have

Succ (Ballot - Secrecy (Γ, A, κ)) ⩽ \frac{1}{2} + negl (κ)

An election scheme satisfies

Ballot - Secrecy

when algorithm

Vote

outputs ballots that do not reveal votes and algorithm

Tally

outputs election outcomes and proofs that do not reveal the relation between votes expressed in collected ballots and the outcome.

Game $Ballot - Secrecy$ tasks the adversary to compute a bulletin board, from ballots constructed by a left-right oracle for votes in one of two possible lists, and determine which list was used from the election outcome and proof generated from tallying that board. The choice between lists is determined by the result β of a coin flip, and the left-right oracle outputs a ballot for vote $v_{β}$ on input of a pair of votes $v_{0}, v_{1}$ . Hence, the left-right oracle constructs ballots for votes in one of two possible lists, where the lists are chosen by the adversary, and the bulletin board may contain those ballots in addition to ballots constructed by the adversary.

Election schemes reveal the number of votes for each candidate (i.e., the election outcome). Hence, to avoid trivial distinctions in game $Ballot - Secrecy$ , we require that runs of the game are balanced: “left” and “right” inputs to the left-right oracle are equivalent, when the corresponding outputs appear on the bulletin board. For example, suppose the inputs to the left-right oracle are $(v_{1, 0}, v_{1, 1}), \dots, (v_{n, 0}, v_{n, 1})$ and the corresponding outputs are $b_{1}, \dots, b_{n}$ , further suppose the bulletin board is ${b_{1}, \dots, b_{ℓ}}$ such that $ℓ ⩽ n$ . That game is balanced if the “left” inputs $v_{1, 0}, \dots, v_{ℓ, 0}$ are a permutation of the “right” inputs $v_{1, 1}, \dots, v_{ℓ, 1}$ . The balanced condition prevents trivial distinctions.9

⁹
A weaker balanced condition might be sufficient for alternative formalisations of election schemes. For instance, voting systems which only announce the winning candidate could be analysed using a balanced condition asserting that the winning candidate was input on both the “left” and “right.”

For instance, an adversary that computes a bulletin board containing only the ballot output by a left-right oracle query with input

(1, 2)

cannot win the game, because it is unbalanced. Albeit, that adversary could trivially determine whether

β = 0

β = 1

, given the tally of that board.

Intuitively, if the adversary wins game $Ballot - Secrecy$ , then there exists a strategy to distinguish ballots. Indeed, such an adversary can distinguish between an instance of the voting system in which voters cast some votes, from another instance in which voters cast a permutation of those votes, thus, voters’ votes are revealed. Otherwise, the adversary is unable to distinguish between a voter casting a ballot for vote $v_{0}$ and another voter casting a ballot for vote $v_{1}$ , hence, voters’ votes cannot be revealed.

Proving ballot secrecy is time consuming. Indeed, a proof for the simple $Enc 2 Vote$ scheme consumes around four and a half pages [108, Appendix C.6]. To reduce the expense of such proofs, we introduce ballot independence (§3.2) and prove that it suffices for $Ballot - Secrecy$ (§3.3). Using this sufficient condition, the four and a half page proof can be reduced to around one page [120, §4.3].

3.2. Ballot independence

Ballot independence [39,47,62] is seemingly related to ballot secrecy.

Ballot independence. Observing another voter’s interaction with the voting system does not allow a voter to cast a meaningfully related vote.

Our informal definition essentially states that an adversary is unable to construct a ballot meaningfully related to a non-adversarial ballot, i.e., ballots are non-malleable. Hence, we can formalise ballot independence as a straightforward adaptation of the non-malleability definition for asymmetric encryption by Bellare & Sahai [10].10

¹⁰
Non-malleability was first formalised by Dolev, Dwork & Naor in the context of asymmetric encryption [57,58]; the definition by Bellare & Sahai builds upon their results and results by Bellare et al. [7].

Such a formalisation captures an intuitive notion of ballot independence, but it is complex and proofs of non-malleability are relatively difficult. Bellare & Sahai observe similar complexities and show that their definition is equivalent to a simpler, indistinguishability notion. In a similar direction, we derive a definition of ballot independence, called indistinguishability under chosen vote attack (

IND - CVA

), as a straightforward adaptation of their indistinguishability notion for asymmetric encryption.

Definition 3 (

IND - CVA

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $A$ be an adversary, κ be the security parameter, and $IND - CVA$ be the following game.

We say Γ satisfies indistinguishability under chosen vote attack ( $IND - CVA$ ), if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (IND - CVA (Γ, A, κ)) ⩽ \frac{1}{2} + negl (κ)$ .

Game $IND - CVA$ is satisfied if the adversary cannot determine whether the challenge ballot b is for one of two possible votes $v_{0}$ and $v_{1}$ . In addition to the challenge ballot, the adversary is given the election outcome derived by tallying a bulletin board computed by the adversary. To avoid trivial distinctions, the adversary’s bulletin board should not contain the challenge ballot. Intuitively, the adversary wins if there exists a strategy to construct related ballots, since this strategy enables the adversary to construct a ballot $b^{'}$ , related to the challenge ballot b, and determine if b is for $v_{0}$ or $v_{1}$ from the outcome derived by tallying a bulletin board containing $b^{'}$ .

Comparing $IND - CVA$ and $IND - PA 0$ . The main distinction between indistinguishability for asymmetric encryption ( $IND - PA 0$ ) and indistinguishability for election schemes ( $IND - CVA$ ) is as follows: $IND - PA 0$ performs a parallel decryption, whereas $IND - CVA$ performs a single tally. Hence, indistinguishability for encryption reveals plaintexts corresponding to ciphertexts, whereas indistinguishability for elections reveals the number of votes for each candidate.

We present an alternative definition of ballot independence (Appendix B), based upon the definition of non-malleability for asymmetric encryption by Bellare & Sahai, and prove that the definition is equivalent to $IND - CVA$ .

3.3. Secrecy and independence coincide (for zero-knowledge tallying proofs)

The main distinctions between our ballot secrecy ( $Ballot - Secrecy$ ) and ballot independence ( $IND - CVA$ ) games are as follows.

The challenger produces one challenge ballot for the adversary in game $IND - CVA$ , whereas the left-right oracle produces arbitrarily many challenge ballots for the adversary in game $Ballot - Secrecy$ .

The adversary in game $Ballot - Secrecy$ has access to a tallying proof, but the adversary in game $IND - CVA$ does not.

The winning condition in game $Ballot - Secrecy$ requires the bulletin board to be balanced, whereas the bulletin board must not contain the challenge ballot in game $IND - CVA$ .

The second point distinguishes our games and shows

Ballot - Secrecy

is at least as strong as

IND - CVA

. Hence, non-malleable ballots are necessary in election schemes satisfying

Ballot - Secrecy

. (Non-malleable ballots are not generally necessary: Privacy definitions are sound but incomplete, Section 7.)

Theorem 1 ( $Ballot - Secrecy \Rightarrow IND - CVA$ ).

Given an election scheme Γ satisfying $Ballot - Secrecy$ , we have Γ satisfies $IND - CVA$ .

A proof of Theorem 1 and all further proofs, except where otherwise stated, appear in Appendix C.

Tallying proofs may reveal voters’ votes. For example, a variant of $Enc 2 Vote$ might define tallying proofs that map ballots to votes. Since proofs are available to the adversary in game $Ballot - Secrecy$ , but not in game $IND - CVA$ , it follows that $Ballot - Secrecy$ is strictly stronger than $IND - CVA$ .

Proposition 2 ( $IND - CVA ⇏ Ballot - Secrecy$ ).

An election scheme may satisfy $IND - CVA$ , but not $Ballot - Secrecy$ .

Proposition 2 follows from our informal reasoning and we omit a formal proof.

Game $Ballot - Secrecy$ is generally (strictly) stronger than game $IND - CVA$ . Nonetheless, we show that our games coincide for election schemes without tallying proofs (Definition 4), assuming tallying is additive (Definition 5), that is, the sum of election outcomes derived by tallying distinct subsets of a bulletin board is equivalent to the election outcome derived by tallying the union of those subsets.

Definition 4.
An election scheme $Γ = (Setup, Vote, Tally)$ is without tallying proofs, if there exists a constant symbol ϵ such that for all private keys $sk$ , sets $bb$ , integers $nc$ , security parameters κ, and computations $(v, pf) \leftarrow Tally (sk, bb, nc, κ)$ , we have $pf = ϵ$ .
Definition 5 ( $Additivity$ ).

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $A$ be an adversary, κ be a security parameter, and $Additivity$ be the following game.

We say Γ satisfies $Additivity$ , if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (Additivity (Γ, A, κ)) > 1 - negl (κ)$ .

Proposition 3 ( $Ballot - Secrecy = IND - CVA$ , without proofs).

Let Γ be an election scheme without tallying proofs. Suppose Γ satisfies $Additivity$ . We have Γ satisfies $Ballot - Secrecy$ iff Γ satisfies $IND - CVA$ .

Our equivalence result generalises to election schemes with zero-knowledge tallying proofs (Definition 19), i.e., schemes that compute proofs using non-interactive zero-knowledge proof systems.

Theorem 4 ( $Ballot - Secrecy = IND - CVA$ , with ZK proofs).

Let Γ be an election scheme with zero-knowledge tallying proofs. Suppose Γ satisfies $Additivity$ . We have Γ satisfies $Ballot - Secrecy$ iff Γ satisfies $IND - CVA$ .

Proof sketch.
Game $Ballot - Secrecy$ computes the election outcome from ballots constructed by the oracle and ballots constructed by the adversary. Intuitively, such an outcome can be equivalently computed as follows:

Yet, a poorly designed tallying algorithm might not ensure equivalence. In particular, ballots constructed by the adversary can cause the algorithm to behave unexpectedly. (Such algorithms are nonetheless compatible with our correctness requirement, because correctness does not consider an adversary.) Our $Additivity$ property ensures equivalence. Moreover, our $Additivity$ property ensures the above computation is equivalent to the following:

Furthermore, by correctness of the election scheme, the above for-loop can be equivalently computed as follows:

Indeed, for each $b \in bb \land (b, v_{0}, v_{1}) \in L$ , we have b is an output of $Vote (pk, v_{β}, nc, κ)$ , hence, $Tally (sk, {b}, nc, κ)$ outputs $(v, pf)$ such that $v$ is a zero-filled vector, except for index $v_{β}$ which contains one, and this suffices to ensure equivalence. In addition, for any adversary that wins game $Ballot - Secrecy$ , we are assured that $balanced (bb, nc, L)$ holds, hence, the above for-loop can be computed as

or

without weakening the game. Thus, perhaps surprisingly, tallying ballots constructed by the oracle does not provide the adversary with an advantage (in determining whether $β = 0$ or $β = 1$ ) and we can omit such ballots from tallying in game $Ballot - Secrecy$ . Thus, game $Ballot - Secrecy$ is equivalent to game $BS$ (Definition 20), which modifies the tallying procedure as described and simulates tallying proofs. Thereafter, we proceed with a hybrid argument (for which Shoup presents a brief tutorial [114]). □
Additivity is implied by universal verifiability (Lemmata 7 & 27). Thus, a special case of Theorem 4 requires the election scheme to satisfy universal verifiability, which is useful to simplify its application. Indeed, we exploit this result in the following section to prove $Ballot - Secrecy$ .
4. Case study I: Helios

Helios can be informally modelled as the following election scheme (further details appear in Sidebar 2):

$Setup$ generates a key pair for an asymmetric additively-homomorphic encryption scheme, proves correct key generation in zero-knowledge, and outputs the key pair and proof.

$Vote$ enciphers the vote’s bitstring encoding to a tuple of ciphertexts, proves in zero-knowledge that each ciphertext is correctly constructed and that the vote is selected from the sequence of candidates, and outputs the ciphertexts coupled with the proofs.

$Tally$ selects ballots from the bulletin board for which proofs hold, homomorphically combines the ciphertexts in those ballots, decrypts the homomorphic combination to reveal the election outcome, and announces the outcome, along with a zero-knowledge proof of correct decryption.

Helios was first released in 2009 as Helios 2.0,11

¹¹
https://github.com/benadida/helios/releases/tag/2.0, released 25 Jul 2009, accessed 29 Mar 2019.

and the current release is Helios 3.1.4.12

¹²

https://github.com/benadida/helios-server/releases/tag/v3.1.4, released 10 Mar 2011, last patched 27 Oct 2017, accessed 29 Mar 2019.

Sidebar 2

Helios: Ballot construction and tallying

4.1. Helios 2.0 & Helios 3.1.4

Cortier & Smyth show that Helios 2.0 does not satisfy ballot secrecy (§3) and neither does Helios 3.1.4.13

¹³
Helios 3.1.4 mitigates against a universal-verifiability vulnerability in Helios 2.0, by checking that tallied ballots are constructed from suitable cryptographic parameters [33, §4.1]. The vulnerabilities described herein use well-formed parameters, hence, the additional checks do not preclude vulnerabilities and we refer the reader to the original description for details.

Thus, we would not expect our definition of ballot secrecy to hold. Indeed, we adopt formal descriptions of Helios 2.0 and Helios 3.1.4 by Smyth, Frink & Clarkson [128] (Appendix D) and use those descriptions to prove that

Ballot - Secrecy

is not satisfied. Theorem 5.

Neither Helios 2.0 nor Helios 3.1.4 satisfy $Ballot - Secrecy$ .

Cortier & Smyth attribute the vulnerability to tallying meaningfully related ballots. Indeed, Helios uses malleable ballots: Given a ballot

c_{1}, \dots, c_{nc - 1}, σ_{1}, \dots, σ_{nc}

, we have

c_{χ (1)}, \dots, c_{χ (nc - 1)}, σ_{χ (1)}, \dots, σ_{χ (nc - 1)}, σ_{nc}

is a ballot for all permutations χ on

{1, \dots, nc - 1}

. Thus, ballots are malleable, which is incompatible with

Ballot - Secrecy

(§3.3). Proof sketch.

Suppose an adversary queries the left-right oracle with (distinct) inputs $v_{0}, v_{1} \in {1, \dots, nc - 1}$ to derive a ballot for $v_{β}$ , where integer $nc ⩾ 3$ is chosen by the adversary and bit β is chosen by the challenger. Further suppose the adversary picks a permutation χ on ${1, \dots, nc - 1}$ , abuses malleability to derive a related ballot b for $χ (v_{β})$ , and outputs bulletin board ${b}$ . The board is balanced, because it does not contain the ballot output by the oracle. Suppose the adversary performs the following computation on input of election outcome $v$ : if $v [χ (v_{0})] = 1$ , then output 0, otherwise, output 1. Since b is a ballot for $χ (v_{β})$ , it follows by correctness that $v [χ (v_{0})] = 1$ iff $β = 0$ , and $v [χ (v_{1})] = 1$ iff $β = 1$ , hence, the adversary wins the game. □

For simplicity, our proof sketch considers an adversary that omits ballots from the bulletin board. Voters might detect such an adversary, because Helios satisfies individual verifiability, hence, voters can discover if their ballot is omitted. Detection does not invalidate Theorem 5, since the ability to detect an attack after the fact does not eliminate the possibility of an attack. Our proof sketch can be extended to avoid such detection: Let

b_{1}

be the ballot output by the left-right oracle in the proof sketch and suppose

b_{2}

is the ballot output by a (second) left-right oracle query with inputs

v_{1}

and

v_{0}

. Further suppose the adversary outputs (the balanced) bulletin board

{b, b_{1}, b_{2}}

and performs the following computation on input of election outcome

v

: if

v

corresponds to votes

v_{0}, v_{1}, χ (v_{0})

, then output 0, otherwise, output 1, where χ is the permutation chosen by the adversary. Hence, the adversary wins the game.

Notions of ballot secrecy used by Bernhard, Pereira & Warinschi [19], Bernhard [15, §6.11] and Bernhard et al. [17, §D.3] cannot detect the known Helios 2.0 vulnerability (in the presence of an adversary that controls ballot collection), because interception is not possible when ballots are recorded-as-cast.14

¹⁴

This observation suggests that recorded-as-cast is unsatisfiable: An adversary that can intercept ballots can always prevent the collection of ballots. Nevertheless, the definition of recorded-as-cast is informal, thus ambiguity should be expected and some interpretation of the definition should be satisfiable.

Beyond ballot secrecy, Bernhard, Pereira & Warinschi show that Helios 3.1.4 does not satisfy universal verifiability [19].15

¹⁵

Beyond secrecy and verifiability, eligibility is not satisfied [93,131,132].

They attribute vulnerabilities to application of the Fiat-Shamir transformation without inclusion of statements in hashes (i.e., weak Fiat-Shamir), and propose including statements in hashes (i.e., applying the Fiat-Shamir transformation) as a defence.

4.2. Helios’16

We have seen that non-malleable ballots are necessary for $Ballot - Secrecy$ (§3.3); future Helios releases should adopt non-malleable ballots. The Fiat-Shamir transformation alone is insufficient to ensure non-malleability, because permutations can be applied to a ballot’s ciphertexts: An ordering over ciphertexts must be proved.16

¹⁶
I do not recall the exact origin of this idea: Email communication suggests both I (17 Dec 2010) and Olivier Pereira (27 Dec 2010) each independently conceived the need for a proven ordering over ciphertexts.

Smyth, Frink & Clarkson formalise this idea in Helios’16 [128], a variant of Helios 3.1.4 that uses the Fiat-Shamir transformation and includes a ciphertext’s position (relative to other ciphertexts) in hashes, which is intended, but not proven, to ensure non-malleable ballots. We recall their formal description in Appendix D, and using that formalisation we prove that Helios’16 delivers secrecy. Theorem 6.

Helios’16 satisfies $Ballot - Secrecy$ .

Proof sketch.

We prove that Helios’16 has zero-knowledge tallying proofs and, since universal verifiability is satisfied [128], we have $Additivity$ too (Lemmata 7 & 27). Hence, by Theorem 4, it suffices to show that Helios’16 satisfies $IND - CVA$ , which we prove by reduction to the security of the underlying encryption scheme, using an extractor that exists for the proof system used to construct ballots. □

A formal proof of Theorem 6 appears in Appendix D.1, assuming the random oracle model [8]. This proof, coupled with the proof of verifiability by Smyth, Frink & Clarkson [128], provides strong motivation for future Helios releases being based upon Helios’16, since it is the only variant of Helios which is proven to satisfy both ballot secrecy and verifiability.17

¹⁷

Earlier versions of Helios have been shown to satisfy definitions of ballot secrecy by Bernhard et al., but not notions of verifiability (the analysis by Küsters et al. [87] does not detect vulnerabilities identified by Bernhard et al. [19] and Chang-Fong & Essex [33], possibly because their analysis “does not formalize all the cryptographic primitives used by Helios” [128, §9]).

A new release of Helios, which we’ll call Helios 4.0, has been long-planned.18

¹⁸

https://web.archive.org/web/20171026064140/http://documentation.heliosvoting.org/verification-specs/helios-v4, published c. 2012, accessed 29 Mar 2019.

That version goes beyond the idea of merely proving an ordering over ciphertexts, to include far more information in hashes, which should be useful when sharing keys between elections (to prevent ballots from one election being cast in another, which could violate ballot secrecy). Security results are summarised in Table 1. Once Helios 4.0 is finalised, future work could consider whether our ballot secrecy proof and verifiability proofs by Smyth, Frink, & Clarkson can be adapted to that scheme.

Table 1

Summary of Helios security results

	Helios 2.0	Helios 3.1.4	Helios’16	Helios 4.0
Secrecy	✗	✗	✓	?
Verifiability	✗	✗	✓	?

Cortier & Smyth identify a secrecy vulnerability in Helios 2.0 and Helios 3.1.4 [47]. Bernhard, Pereira & Warinschi [19] and Bernhard et al. [17, §D.3] show that Helios 4.0 satisfies various notions of ballot secrecy in two candidate elections – a general result is unknown. We have proved that Helios’16 satisfies ballot secrecy (Theorem 6). Bernhard, Pereira & Warinschi identify universal-verifiability vulnerabilities in Helios 2.0 and Helios 3.1.4 [19] and Chang-Fong & Essex identify vulnerabilities in Helios 2.0 [33]. Smyth, Frink, & Clarkson prove that Helios’16 satisfies individual and universal verifiability.

5. Simplifying ballot-secrecy proofs

We have seen that our definitions of ballot secrecy and ballot independence coincide when tallying is additive and tallying proofs are zero-knowledge (Theorem 4). Building upon this result and Proposition 8, we show that tallying cannot harm secrecy when ballots are tallied correctly and tallying proofs are zero-knowledge. That is, $(Setup, Vote, Tally)$ satisfies $Ballot - Secrecy$ if and only if $(Setup, Vote, {Tally}^{'})$ does, assuming algorithms $Tally$ and ${Tally}^{'}$ both tally ballots correctly and tallying proofs are zero-knowledge.19

¹⁹
A more general result also holds: $(Setup, Vote, Tally)$ satisfies $Ballot - Secrecy$ iff $(Setup, Vote, {Tally}^{'})$ satisfies $Ballot - Secrecy$ , assuming algorithms $Tally$ and ${Tally}^{'}$ are indistinguishable, in particular, they tally ballots in the same way. However, election schemes that tally ballots incorrectly are not useful, so we forgo generality for practicality.

Smyth, Frink & Clarkson capture the notion of tallying ballots correctly using function $correct - outcome$ [128]. That function uses a counting quantifier: A predicate $(\exists^{= ℓ} x : P (x))$ that holds exactly when there are ℓ distinct values for x such that $P (x)$ is satisfied [113].20

²⁰

Variable x is bound by the quantifier and integer ℓ is free.

Using the counting quantifier, function

correct - outcome

is defined such that

correct - outcome (pk, nc, bb, κ) [v] = ℓ

iff

\exists^{= ℓ} b \in bb ∖ {⊥} : \exists r : b = Vote (pk, v, nc, κ; r)

, where

correct - outcome (pk, nc, bb, κ)

is a vector of length

nc

and

1 ⩽ v ⩽ nc

. Hence, component v of vector

correct - outcome (pk, nc, bb, κ)

equals ℓ iff there exist ℓ ballots for vote v on the bulletin board. The function requires ballots be interpreted for only one candidate, which can be ensured by injectivity.

Definition 6 (

HK - Injectivity

An election scheme $(Setup, Vote, Tally)$ satisfies honest-key injectivity ( $HK - Injectivity$ ), if for all probabilistic polynomial-time adversaries $A$ , security parameters κ and computations $(pk, sk, mb, mc) \leftarrow Setup (κ); (nc, v, v^{'}) \leftarrow A (pk, κ); b \leftarrow Vote (pk, nc, v, κ); b^{'} \leftarrow Vote (pk, nc, v^{'}, κ)$ such that $v \neq v^{'} \land b \neq ⊥ \land b^{'} \neq ⊥$ , we have $b \neq b^{'}$ .

Equipped with notions of injectivity and of tallying ballots correctly, we formalise a soundness condition asserting that an election scheme tallies ballots correctly (Definition 7), which allows us to formally state that tallying cannot harm ballot independence (Proposition 8).

Definition 7 ( $Tally - Soundness$ ).

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $A$ be an adversary, κ be a security parameter, and $Tally - Soundness$ be the following game.

We say Γ satisfies tally soundness ( $Tally - Soundness$ ), if Γ satisfies $HK - Injectivity$ and for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (Tally - Soundness (Γ, A, κ)) > 1 - negl (κ)$ .

Lemma 7.
$Tally - Soundness$ implies $Additivity$ .
Proposition 8.
Let $Γ = (Setup, Vote, Tally)$ and $Γ^{'} = (Setup, Vote, {Tally}^{'})$ be election schemes. Suppose Γ and $Γ^{'}$ satisfy $Tally - Soundness$ . We have Γ satisfies $IND - CVA$ iff $Γ^{'}$ satisfies $IND - CVA$ .
Proof.
Tally soundness assures us that algorithms $Tally$ and ${Tally}^{'}$ produce indistinguishable election outcomes, thus they are interchangeable in the context of game $IND - CVA$ . □

It follows from Proposition 8 that tally soundness suffices for ballot independence of scheme $(Setup, Vote, Tally)$ , if there exists an algorithm ${Tally}^{'}$ such that $(Setup, Vote, {Tally}^{'})$ is an election scheme satisfying tally soundness and ballot independence. We demonstrate the existence of such an algorithm with respect to election scheme $Enc 2 Vote$ ,21
²¹
Our presentation of $Enc 2 Vote$ extends the presentation by Quaglia & Smyth [108, Definition 7] to make the plaintext space explicit. We also embed the public key inside the private key. (Quaglia & Smyth’s formalisation of $Enc 2 Vote$ builds upon constructions by Bernhard et al. [18,20,125,126].)

thereby showcasing the applicability of Proposition 8 for a class of encryption-based election schemes. Definition 8 ( $Enc 2 Vote$ ).

Given an asymmetric encryption scheme $Π = (Gen, Enc, Dec)$ , we define $Enc 2 Vote (Π) = (Setup, Vote, Tally)$ such that:

$Setup (κ)$ computes $(pk, sk, m) \leftarrow Gen (κ); {pk}^{'} \leftarrow (pk, m); {sk}^{'} \leftarrow (pk, sk)$ , derives $mc$ as the largest integer such that ${0, \dots, mc} \subseteq {0} \cup m$ and for all $m_{0}, m_{1} \in {1, \dots, mc}$ we have $| m_{0} | = | m_{1} |$ , and outputs $({pk}^{'}, {sk}^{'}, p (κ), mc)$ , where p is a polynomial function.

$Vote ({pk}^{'}, v, nc, κ)$ parses ${pk}^{'}$ as pair $(pk, m)$ , outputting ⊥ if parsing fails or $v \notin {1, \dots, nc} \lor {1, \dots, nc} ⊈ m$ , computes $b \leftarrow Enc (pk, v)$ , and outputs b.

$Tally ({sk}^{'}, bb, nc, κ)$ initialises $v$ as a zero-filled vector of length $nc$ , parses ${sk}^{'}$ as pair $(pk, sk)$ , outputting $(v, ⊥)$ if parsing fails, computes for $b \in bb$ do $v \leftarrow Dec (sk, b);$ if $1 ⩽ v ⩽ nc$ then $v [v] \leftarrow v [v] + 1$ , and outputs $(v, ϵ)$ , where ϵ is a constant symbol.

To ensure

Enc 2 Vote (Π)

is an election scheme, we require asymmetric encryption scheme Π to produce distinct ciphertexts with overwhelming probability [120, Lemma 3]. Hence, we must restrict the class of asymmetric encryption schemes used to instantiate

Enc 2 Vote

. We consider a broad class of schemes that produce distinct ciphertexts with overwhelming probability.

Lemma 9.
Given an asymmetric encryption scheme Π satisfying $IND - CPA$ , we have $Enc 2 Vote (Π)$ is an election scheme. Moreover, if Π has perfect correctness, then $Enc 2 Vote (Π)$ satisfies $HK - Injectivity$ .
A proof of Lemma 9 follows from Smyth’s correctness proof [120, Lemma 4] and Quaglia & Smyth’s proof of a slightly stronger notion of $HK - Injectivity$ [108, Lemma 2].

Intuitively, given a non-malleable asymmetric encryption scheme Π, election scheme $Enc 2 Vote (Π)$ derives ballot secrecy from Π until tallying and tallying maintains ballot secrecy by returning only the number of votes for each candidate. Smyth presents a formal proof of ballot secrecy [120, Proposition 5], hence, ballot independence is satisfied too (Theorem 1). Corollary 10.
Given an asymmetric encryption scheme Π satisfying $IND - PA 0$ , we have $Enc 2 Vote (Π)$ satisfies $IND - CVA$ .
The reverse implication of Corollary 10 does not hold. Indeed, we have the following (stronger) result.
Proposition 11.
There exists an asymmetric encryption scheme Π such that $Enc 2 Vote (Π)$ satisfies $Ballot - Secrecy$ , but Π does not satisfy $IND - PA 0$ .

To capitalise on Proposition 8, we demonstrate that $Enc 2 Vote$ produces election schemes satisfying tallying soundness (Lemma 12), assuming “ill-formed” ciphertexts are distinguishable from “well-formed” ciphertexts, and combine our results to derive Theorem 13. Definition 9.
Given an asymmetric encryption scheme $Π = (Gen, Enc, Dec)$ , we say Π satisfies well-definedness, if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Pr [(pk, sk, m) \leftarrow Gen (κ); c \leftarrow A (pk, m, κ) : Dec (sk, c) \neq ⊥ \Rightarrow \exists m, r . m \in m \land c = Enc (pk, m; r) \land c \neq ⊥] > 1 - negl (κ)$ .
$Tally - Soundness$ demands that every counted ballot be output by algorithm $Vote$ , i.e., only “well-formed” ballots are counted, “ill-formed” ballots are not. Election scheme $Enc 2 Vote (Π)$ defines ballots as ciphertexts, hence, when Π satisfies well-definedness, we are assured that only “well-formed” ballots are counted, as $Tally - Soundness$ demands. Lemma 12.
Given a perfectly-correct asymmetric encryption scheme Π satisfying well-definedness and $IND - CPA$ , we have $Enc 2 Vote (Π)$ satisfies $Tally - Soundness$ .
Theorem 13.
Let Π be an asymmetric encryption scheme, $Enc 2 Vote (Π) = (Setup, Vote, Tally)$ , and $Γ = (Setup, Vote, {Tally}^{'})$ for some algorithm ${Tally}^{'}$ such that Γ is an election scheme with zero-knowledge tallying proofs. Suppose Π is perfectly correct and satisfies $IND - PA 0$ and well-definedness. Further suppose Γ satisfies $Tally - Soundness$ . We have Γ satisfies $Ballot - Secrecy$ .
Proof.
Election scheme $Enc 2 Vote (Π)$ satisfies $Tally - Soundness$ (Lemma 12) and $IND - CVA$ (Corollary 10). Thus, Γ satisfies $IND - CVA$ (Proposition 8) and $Ballot - Secrecy$ (Theorem 4 & Lemma 7). □
We show that tally soundness is implied by universal verifiability in Appendix E. Thus, a special case of Theorem 13 requires universal verifiability rather than tally soundness. It follows that $Ballot - Secrecy$ is satisfied by verifiable election schemes that produce ballots by encrypting votes with asymmetric encryption schemes satisfying well-definedness and $IND - PA 0$ . Thereby making proofs of ballot secrecy trivial for a class of encryption-based election schemes. Indeed, we exploit this result in the following section to show that the combination of non-malleable encryption and universal verifiability achieve ballot secrecy.
6. Case study II: Helios Mixnet

Helios Mixnet can be informally modelled as the following election scheme:

$Setup$ generates a key pair for an asymmetric homomorphic encryption scheme, proves correct key generation in zero-knowledge, and outputs the key pair and proof.

$Vote$ enciphers the vote to a ciphertext, proves correct ciphertext construction in zero-knowledge, and outputs the ciphertext coupled with the proof.

$Tally$ selects ballots from the bulletin board for which proofs hold, mixes the ciphertexts in those ballots, decrypts the ciphertexts output by the mix to reveal the election outcome (i.e., the frequency distribution of votes), and announces that outcome, along with zero-knowledge proofs demonstrating correct decryption.

Neither Adida [1] nor Bulens, Giry & Pereira [30] have released an implementation of Helios Mixnet.22

²²
The planned implementation of Helios Mixnet (https://web.archive.org/web/20160912182802/https://documentation.heliosvoting.org/verification-specs/mixnet-support, published c. 2010, accessed 29 Mar 2019, & https://web.archive.org/web/20110119223848/http://documentation.heliosvoting.org/verification-specs/helios-v3-1, published Dec 2010, accessed 29 Mar 2019) has not been released.

Tsoukalas et al. [136] released Zeus as a fork of Helios spliced with mixnet code to derive an implementation,23

²³

https://github.com/grnet/zeus, accessed 29 Mar 2019.

and Yingtong Li released helios-server-mixnet as an extension of Zeus with threshold asymmetric encryption and some other minor changes.24

²⁴

https://github.com/RunasSudo/helios-server-mixnet, accessed 29 Mar 2019.

^,25

²⁵

The problem of malleable Helios ballots (§4) was discussed with the developers of Zeus and helios-server-mixnet, and they explained that their systems use non-malleable ballots (email communication, Oct & Dec 2017).

We can derive Helios Mixnet from $Enc 2 Vote (Π)$ by replacing its tallying algorithm, and by using an asymmetric encryption scheme $Π = (Gen, Enc, Dec)$ , where algorithm $Gen$ proves correct key generation, and algorithm $Enc$ verifies such proofs, enciphers plaintexts to ciphertexts using a second encryption scheme, proves correct ciphertext construction, and outputs the ciphertext coupled with the proof. However, a blight arises when $Enc 2 Vote$ is instantiated with encryption schemes that prove correct key generation.26

²⁶

Helios Mixnet defines public keys as triples comprising a public key and message space defined by the underlying asymmetric encryption scheme, along with a proof of correct key generation. By comparison, $Enc 2 Vote$ defines public keys as pairs comprising a public key and message space defined by the underlying asymmetric encryption scheme (wherein the public key defined by the encryption scheme incorporates some proof of correct key generation). Hence, $Enc 2 Vote$ cannot be instantiated to immediately derive Helios Mixnet – we have a slight mismatch of parameters, a minor blight.

To avoid this blight, we extend

Enc 2 Vote

with such proofs and show that results in Section 5 still hold (Appendix F). This leads us to treat Helios Mixnet as an election scheme built from asymmetric encryption schemes

Π = (Gen, Enc, Dec)

and

Π_{0} = (Gen, {Enc}^{'}, {Dec}^{'})

such that:

$Setup (κ)$ selects coins s uniformly at random, computes $(pk, sk, m) \leftarrow Gen (κ; s)$ and a proof ρ of correct key generation using $sk$ and s as the witness, derives $mc$ as the largest integer such that ${0, \dots, mc} \subseteq {0} \cup m$ , computes ${pk}^{'} \leftarrow (pk, m, ρ); {sk}^{'} \leftarrow (pk, sk)$ , and outputs $({pk}^{'}, {sk}^{'}, p (κ), mc)$ , where p is a polynomial function.

$Vote (pk, v, nc, κ)$ parses ${pk}^{'}$ as a vector $(pk, m, ρ)$ , outputting ⊥ if parsing fails, ρ does not verify, $v \notin {1, \dots, nc}$ , or ${0, \dots, nc} ⊈ m$ , computes $b \leftarrow Enc (pk, v)$ , and outputs b.

where

$Enc (pk, v)$ selects coins r uniformly at random, computes $c \leftarrow {Enc}^{'} (pk, v; r)$ and a proof σ of correct ciphertext construction using v and r as the witness, and outputs $(c, σ)$ .

$Dec (sk, b)$ parses b as a pair $(c, σ)$ , outputting ⊥ if parsing fails or σ does not verify, computes $v \leftarrow {Dec}^{'} (sk, c)$ , and outputs v.

It follows that our results (§5) can be applied to trivialise a ballot-secrecy proof: It is known that Π is a non-malleable encryption scheme [19, Theorem 2], assuming the proof system used by algorithm

Enc

satisfies simulation sound extractability and

Π_{0}

satisfies

IND - CPA

. Moreover, we have Π satisfies well-definedness, by the former assumption. Furthermore, Smyth has shown that universal verifiability is satisfied [116], hence,

Tally - Soundness

is satisfied too. Thus,

Ballot - Secrecy

is satisfied. Thereby providing evidence that our results do indeed make ballot-secrecy proofs trivial.

To formally state our ballot secrecy result, we adopt a set HeliosM’17 of election schemes that includes Helios Mixnet and prove ballot secrecy for every scheme in that set. Theorem 14.

Each election scheme in set HeliosM’17 satisfies $Ballot - Secrecy$ .

A proof of Theorem 14 along with a definition of HeliosM’17 appear in Appendix G.

7. Discussion, limitations, and directions for further research

This article advances our understanding of ballot secrecy, establishing a foundation for discussion, debate, and development, especially in terms of the following limitations.

Authentication, re-voting, and unforgeability. Voting systems have traditionally permitted voters to cast at most one ballot. More recent systems permit multiple ballots [2,64,77,91,93,106,117], with only the voter’s last having influence, enabling voters to change their vote, providing flexibility and aiding education (since voters can “ask the help of anyone for submitting a random ballot, and then re-voting privately afterwards” [2, §3.3]). Election schemes are reliant on external authentication services to ensure that only the last ballot of each voter has influence. (E.g., Helios supports authentication via Facebook, Google and Yahoo using OAuth [93].) Such services are assumed to be trusted, they are not intended to exclude attacks that arise when services are subverted (to authenticate non-voter ballots or to assert a ballot other than a voter’s last should have influence, for instance). Evaluating whether trust is merited (including determining whether external authentication services ensure that only the last choice of each voter has influence) is beyond the scope of our privacy definitions. Definitions could be extended with an ideal authentication service and external authentication services could be proven equivalent. Ultimately, a reliance on external authentication services introduces a trust assumption. That assumption is eliminated by voting systems that use cryptography to implement their own authentication mechanisms, rendering authorised ballots unforgeable. (E.g., the voting system by Juels, Catalano & Jakobsson uses a combination of encrypted nonces and plaintext equality tests for authentication [77].) Extending definitions to include voting systems with their own cryptography-based authentication mechanisms and considering the interplay between privacy and re-voting, without trusting an authentication service, would be an interesting direction for further research. The aforementioned extensions necessitate changes to our balanced condition such that only the last choice of each voter is considered. This could be achieved by keeping track of the number of ballots cast by each voter, for example, $O (i d, v_{0}, v_{1})$ could compute $L \leftarrow L \cup {(i d, b, n, v_{0}, v_{1})}$ , where $i d$ is a voter identifier, b is the constructed ballot, and $n = | {b^{'} ∣ (i d, b^{'}, i, v_{0}^{'}, v_{1}^{'}) \in L} |$ , i.e., the number n of ballots previously cast with identifier $i d$ . And by applying predicate $balanced$ to a set containing only voters’ last votes, for instance, using $balanced (bb, nc, {b ∣ (i d, b, i, v_{0}, v_{1}) \in L \land \forall (i d, b^{'}, i^{'}, v_{0}^{'}, v_{1}^{'}) \in L \land i ⩾ i^{'}})$ on the final line of game $Ballot - Secrecy$ . Further investigation of the details would be prudent.

Ballot secrecy notions and interplay with individual verifiability. We know some scenarios inevitably reveal voters’ votes, which is why an exception is included in our informal definition of ballot secrecy (a voter’s vote is not revealed to anyone, except when the vote can be deduced from the election outcome and any partial knowledge of voters’ votes).27

²⁷
Some revelations are an artefact of announcing the outcome as a frequency distribution of votes (a functional requirement of many nations, which comes at a privacy cost), rather than revealing less information, e.g., just the winning candidate [13,56,74].

That exception tolerates revelations in the following example, namely, Alice, Bob and Mallory participate in a referendum, Mallory (who controls ballot collection) discards Bob’s ballot, and the outcome has frequency one for each of ‘yes’ and ‘no,’ allowing Mallory to deduce Alice’s vote. Such revelations are undesirable, but are tolerated by many voting systems and our definition of ballot secrecy. It is open to debate as to whether such voting systems should be branded secret and whether my definition is sound. (I believe so: My definition should only tolerate revelations deducible from outcomes and partial knowledge of votes. As I’ve asserted, it is open to debate as to whether such tolerance is too broad.) Individual verifiability allows voters to check whether their ballots are collected, allowing detection of some troublesome scenarios. Checks cannot, in themselves, preclude revelations. (Indeed, Bob discovering their ballot is absent, does not preclude revelation of Alice’s vote.) Additional properties are necessary. The ability to attribute malice to a particular party (cf. accountability [86]) and to recover from such malice may suffice. (Demanding inclusion of Bob’s ballot can avoid revelation of Alice’s vote.) However, even with additional properties, there is a reliance on voters performing checks, which few voters do [22, §2.1.6]. Regardless, ballot secrecy should be delivered without regard for privilege, without dependence on actions few are willing and able to perform. Future research may consider such possibilities. Demanding delegatable individual-verifiability checks may provide a fruitful advancement: Envisage voters leaving polling stations and handing over material for checks to voting advocates, for instance.

Distributed tallying. Ballot secrecy does not provide assurances when deviations from the prescribed tallying procedure are possible. Indeed, ballots can be tallied individually to reveal votes. Hence, the tallier must be trusted. Consequently, an election scheme that leaks the ballot-vote relation during tallying can satisfy ballot secrecy, because a trusted tallier will not disclose mappings. E.g., construction $Enc 2 Vote$ produces election schemes satisfying ballot secrecy, despite revealing such a map during tallying. Additionally, the tallier cannot collude with the adversary, in particularly, they cannot post to the bulletin board. We can design election schemes that distribute the tallier’s role amongst several talliers and ensure free-choice assuming at least one tallier tallies ballots in the prescribed manner, other talliers can collude with the adversary. Extending our results in this direction is an opportunity for further research; as it stands, the definition is limited. This is a design decision: Distributed tallying adds complexity, increasing the possibility of error; getting the “right” ballot-secrecy definition for a single tallier seems the safer, preferable first step. Ultimately, we would prefer not to trust talliers. Unfortunately, this is only known to be possible for decentralised voting systems, e.g., [66,71,80–82,112], which are designed such that ballots cannot be tallied individually, but are unsuitable for large-scale elections.

Privacy definitions are incomplete: Controlled malleability is tolerable. We have seen that tallying meaningfully related ballots introduces a vulnerability that can be exploited to violate secrecy. Non-malleable ballots serve as a solution and are necessary in election schemes satisfying our definition. More generally, non-malleable ballots are not necessary. Indeed, given an election scheme Γ with non-malleable ballots, let $Γ^{'}$ be derived from Γ by prepending a bit to Γ-ballots and disregarding any ballot that is identical to another except for the first bit before tallying. Intuitively, election scheme $Γ^{'}$ satisfies ballot secrecy, if Γ does. Malleability cannot be exploited in a manner that causes meaningfully related ballots to be tallied; related ballots can be tolerated, as long as they are not counted. Albeit, scheme $Γ^{'}$ cannot satisfy universal verifiability, because voters’ votes may be discarded when related ballots are present. This makes a case for adopting non-malleable ballots. Nonetheless, further research could consider a weakening of our ballot secrecy definition that is compatible with such malleability. Without such a weakening, our definition is too strong: it will incorrectly brand some election schemes (with malleable ballots) as insecure, as $Γ^{'}$ demonstrates.

8. Related work

Discussion of ballot secrecy originates from Chaum [38] and the earliest definitions of ballot secrecy are due to Benaloh et al. [11,13,14].28

²⁸
Quaglia & Smyth present a tutorial-style introduction to modelling ballot secrecy [109], and Bernhard et al. survey ballot secrecy definitions [16,17].

More recently, Bernhard et al. propose a series of ballot secrecy definitions: They consider election schemes without tallying proofs [18,20] and, subsequently, schemes with tallying proofs [16,19,125,126]. The definition by Bernhard, Pereira & Warinschi computes tallying proofs using algorithm

Tally

or a simulator [19], but that definition is too weak and some strengthening is required [16, §3.4 & §4]. (Cortier et al. [42,44] propose a variant of the ballot secrecy definition by Bernhard, Pereira & Warinschi, which is also too weak [16].) By comparison, the definition by Smyth & Bernhard computes tallying proofs using only algorithm

Tally

[125], but their definition is too strong [16, §3.5] and a weakening is required [126]. We prove that our ballot secrecy definition is strictly stronger than the weakened definition by Smyth & Bernhard (Appendix H). The relative merits of definitions by Smyth & Bernhard [126, Definition 5] and by Bernhard et al. [16, Definition 7] are unknown, in particular, it is unknown whether one definition is stronger than the other.

Discussion of ballot independence originates from Gennaro [62] and the apparent relationship between ballot secrecy and ballot independence has been considered. In particular, Benaloh shows that a simplified version of his voting system allows the administrator’s private key to be recovered by an adversary who casts a ballot as a function of other voters’ ballots [11, §2.9]. More generally, Sako & Kilian [111, §2.4], Michels & Horster [94, §3], Wikström [140–142] and Cortier & Smyth [46,47] discuss how malleable ballots can be abused to compromise ballot secrecy. The first definition of ballot independence seems to be due to Smyth & Bernhard [125,126]. Moreover, Smyth & Bernhard formally prove relations between their definitions of ballot secrecy and ballot independence. Independence has also been studied beyond elections, e.g., [39], and the possibility of compromising security in the absence of independence has been considered, e.g., [40,57,58,63,104,105].

All of the ballot secrecy definitions by Bernhard et al. [16,18–20,125,126] and the ballot independence definition by Smyth & Bernhard [125,126] focus on detecting vulnerabilities exploitable by adversaries that control some voters. Vulnerabilities that require control of the bulletin board or the communication channel are not detected, i.e., the bulletin board is implicitly assumed to operate in accordance with the election scheme’s rules and the communication channel is implicitly assumed to be secure. This introduces a trust assumption. Under this assumption, Smyth & Bernhard prove that non-malleable ballots are not necessary for ballot secrecy [125, §4.3]. By comparison, we prove that non-malleable ballots are necessary for ballot secrecy without this trust assumption. Thus, our definition of ballot secrecy improves upon definitions by Bernhard et al. by detecting more vulnerabilities.

Confidence in our ballot secrecy definition might be improved by proving equivalence with a simulation-based definition of ballot secrecy. However, it is unclear how to formulate a suitable simulation-based definition. Bernhard et al. propose an ideal functionality that “collects all votes from the voters, then computes and announces the [election outcome]” [16, §1],29

²⁹

In the context of voting systems that announce the chosen representative (rather than the frequency distribution of votes), a stronger ideal functionality might announce the chosen representative.

but a voting system satisfying ballot secrecy need not be equivalent, because ballot secrecy does not guarantee correct computation of the election outcome. Equivalence can perhaps be shown between their ideal functionality and voting systems satisfying ballot secrecy and some soundness condition (e.g.,

Tally - Soundness

). Albeit, voting systems that bound the number of ballots or candidates, e.g., Helios, may not be equivalent, because soundness conditions (such as

Tally - Soundness

) need only provide guarantees when operating within the aforementioned bounds. Thus, bounds need to be taken into consideration. Moreover, no voting system is equivalent to the ideal functionality by Bernhard et al. in the presence of an adversary that controls the bulletin board, because such an adversary can discard ballots, which creates a trivial distinction.30

³⁰

The real functionality by Bernhard et al. does not capture adversaries that control ballot collection. Thus, the relation they prove between their game-based and simulation-based definitions of ballot secrecy does not preclude vulnerabilities exploitable by such adversaries. Indeed, proving such relations does not guarantee the absence of vulnerabilities.

Nonetheless, equivalence can perhaps be shown for verifiable voting systems in cases where the number of ballots and candidates are bounded, and all voters successfully verify the presence of their ballot, but such a result has no practical relevance, because it is well-known that many voters do not perform checks necessary for verifiability [22, §2.1.6]. Alternatively, the ideal functionality could be weakened such that a discarded ballot in the real functionality corresponds to a discarded vote in the ideal functionality. We leave further exploration of simulation-based definitions of ballot secrecy as a possible extension for future work.

Bulens, Giry & Pereira pose the investigation of voting systems which allow casting of meaningfully related ballots as a means for voters to delegate candidate selection, whilst preserving ballot secrecy, as an interesting research question [30, §3.2]. Desmedt & Chaidos claim to provide such a system [55]. Smyth & Bernhard critique their work and argue that the security results do not support their claims [125, §5.1]. We have shown that non-malleable ballots are necessary to satisfy $Ballot - Secrecy$ (§3.3), providing a negative result for the question posed by Bulens, Giry & Pereira.

Some of the ideas presented in this article previously appeared in my technical report [121] and an extended version of that technical report by Bernhard & Smyth [21]. In particular, the limitations of ballot secrecy definitions by Bernhard et al. were identified and Definition 2 is based upon my earlier definition [121]. The main distinction between Definition 2 and the earlier definition [121, Definition 3] is syntax: This article adopts syntax for election schemes from Smyth, Frink & Clarkson [128], whereas the earlier definition adopts syntax by Smyth & Bernhard [125,126]. The change in syntax is motivated by the superiority of syntax by Smyth, Frink & Clarkson. Moreover, we can capitalise upon results by Smyth, Frink & Clarkson [128] and Quaglia & Smyth [108].

Following the initial release of these results [122,123], Cortier et al. [45] presented a machine-checked proof that variants of Helios satisfy the notion of ballot secrecy by Bernhard et al. [16]. As discussed above, that notion is too weak: It cannot detect vulnerabilities that require control of ballot collection. Thus, our proof is more appropriate. Nonetheless, their proof builds upon similar ideas. In particular, their proof is dependent upon non-malleable ballots and zero-knowledge tallying proofs.

Further to their earlier work [130], Smyth & Hanatani show that Helios’16-ballots are essentially non-malleable ciphertexts and build upon this article to further simplify ballot-secrecy proofs [129], presenting a proof in just two pages, compared to the five pages used here.

Quaglia & Smyth [107] extend game $Ballot - Secrecy$ to syntax with voter credentials [128, Definition 6]. Moreover, they define a transformation to that syntax from our syntax (Definition 1) and prove that their transformation preserves secrecy and verifiability. Furthermore, they apply their transformation to Helios. The resulting scheme is similar Helios-C [43], albeit Quaglia & Smyth observe that Helios-C does not satisfy ballot secrecy when the adversary controls ballot collection, whereas the scheme derived by applying their transformation does.

Beyond the computational model of security, Delaune, Kremer & Ryan formulate a definition of ballot secrecy in the applied pi calculus [51,52] and Smyth et al. show that this definition is amenable to automated reasoning [25,26,54,84,115]. An alternative definition is proposed by Cremers & Hirschi, along with sufficient conditions which are also amenable to automated reasoning [50]. Albeit, the scope of automated reasoning is limited by analysis tools (e.g., ProVerif [27]), because the function symbols and equational theory used to model cryptographic primitives might not be suitable for automated analysis (cf. [5,53,103]).

Ballot secrecy formalises a notion of free-choice assuming ballots are constructed and tallied in the prescribed manner. Moreover, our definition of ballot secrecy assumes the adversary’s capabilities are limited to casting ballots on behalf of some voters and controlling the votes cast by any remaining voters. We have seen that Helios’16 satisfies our definition, but ballot secrecy does not ensure free-choice when an adversary is able to communicate with voters, nor when voters deviate from the prescribed voting procedure to follow instructions provided by an adversary. Indeed, the coins used for encryption serve as proof of how a voter voted in Helios and the voter may communicate those coins to the adversary. Stronger notions of free-choice, such as receipt-freeness [32,51,60,83,96] and coercion resistance [61,70,76,88,139], are needed in the presence of such adversaries. Appendix I introduces these notions, proves that our syntax cannot be used to construct (interesting) schemes satisfying them, and discusses variants of our syntax that can.

McCarthy, Smyth & Quaglia [92] have shown that auction schemes can be constructed from election schemes, and Quaglia & Smyth [108] provide a generic construction for auction schemes from election schemes. Moreover, Quaglia & Smyth adapt our definition of ballot secrecy to a definition of bid secrecy, and prove that auction schemes produced by their construction satisfy bid secrecy. (Similarly, they adapt the definition of verifiability by Smyth, Frink & Clarkson [128] to a definition of verifiability for auctions, and prove that their construction produces schemes satisfying verifiability.) Thus, this research has applications beyond voting.

9. Conclusion

This work was initiated by a desire to eliminate the trust assumptions placed upon the bulletin board and the communication channel in definitions of ballot secrecy by Bernhard et al. and the definition of ballot independence by Smyth & Bernhard. This necessitated the introduction of new security definitions. The definition of ballot secrecy was largely constructed from intuition, with inspiration from indistinguishability games for asymmetric encryption and existing definitions of ballot secrecy. Moreover, the definition was guided by the desire to strengthen existing definitions of ballot secrecy. The definition of ballot independence was inspired by the realisation that independence requires non-malleable ballots, which enabled definitions to be constructed as straightforward adaptations of non-malleability and indistinguishability definitions for asymmetric encryption. The former adaptation being a more natural formulation of ballot independence and the latter being simpler.

Relationships between security definitions aid our understanding and offer insights that facilitate the construction of secure schemes. This prompted the study of relations between our definitions of ballot secrecy and ballot independence, resulting in a proof that non-malleable ballots are necessary for our definitions. We also proved non-malleable ballots suffice for our definition of ballot secrecy in election schemes with zero-knowledge tallying proofs. Moreover, we established a separation result demonstrating that our ballot secrecy definition is strictly stronger than our ballot independence definition.

We proved that Helios’16 uses non-malleable ballots and a proof that Helios’16 satisfies ballot secrecy follows from our results. This proof is particularly significant due to the use of Helios in binding elections, and we encourage developers to base future releases on this variant, since it is the only variant of Helios which is proven to satisfy both ballot secrecy and verifiability.

Proving ballot secrecy is expensive: It requires a significant devotion of time by experts. Indeed, Cortier et al. devoted one person-year to their machine-checked proof. Thus, sufficient conditions for ballot secrecy are highly desirable. We have established that non-malleable ballots are sufficient for our definition of ballot secrecy in election schemes with zero-knowledge tallying proofs and this simplified our ballot-secrecy proof for Helios’16. We have also established that building election schemes from non-malleable asymmetric encryption schemes suffices for our definition of ballot secrecy if tallying is additive (a condition implied by verifiability), and this trivialised our ballot-secrecy proof for Helios Mixnet. Thereby demonstrating the possibility of simple, inexpensive proofs.

This article delivers a definition of ballot secrecy that has been useful in detecting subtle vulnerabilities in voting systems, and has led to the development of election schemes that are proven secure. Thereby demonstrating the necessity of appropriate security definitions and accompanying analysis to ensure security of voting systems, especially those used in binding elections. I hope this article will simplify future proofs of ballot secrecy and, ultimately, aid democracy-builders in deploying their systems securely. There is still work to be done, especially in seeking definitions that consider distributed tallying.

Acknowledgements

I am grateful to David Bernhard and to Elizabeth Quaglia for extensive discussions, feedback, and, more generally, their help in extending my knowledge of cryptography. In addition, I am grateful to Constantin Cătălin Drăgan for explaining subtleties of his work and to Maxime Meyer for his careful proofreading. I am also grateful to JCS reviewers and editors: it’s clear from reviews that this article has been thoroughly studied. I appreciate the detail that reviewers have gone to. I also appreciate the actionable points listed by my associate editor, which expedited time required for revision. All efforts have helped improve this article and any remaining issues are my own. This work received financial support from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC project CRYSP (259639) and from the Luxembourg National Research Fund (FNR) under the FNR-INTER-VoteVerif project (10415467). Work was partly performed at INRIA and the University of Luxembourg.

A. Cryptographic primitives

A.1. Asymmetric encryption

Definition 10 (Asymmetric encryption scheme [78]).

An asymmetric encryption scheme is a tuple of probabilistic polynomial-time algorithms $(Gen, Enc, Dec)$ , such that:31

³¹
Our definition differs from Katz and Lindell’s original definition [78, Definition 10.1] in that we formally state the plaintext space.

Gen , denoted $(pk, sk, m) \leftarrow Gen (κ)$ , inputs a security parameter κ and outputs a key pair $(pk, sk)$ and message space $m$ .

Enc , denoted $c \leftarrow Enc (pk, m)$ , inputs a public key $pk$ and message $m \in m$ , and outputs a ciphertext c.

Dec , denoted $m \leftarrow Dec (sk, c)$ , inputs a private key $sk$ and ciphertext c, and outputs a message m or an error symbol. We assume $Dec$ is deterministic.

Moreover, the scheme must be correct: there exists a negligible function

negl

, such that for all security parameters κ and messages m, we have

Pr [(pk, sk, m) \leftarrow Gen (κ); c \leftarrow Enc (pk, m) : m \in m \Rightarrow Dec (sk, c) = m] > 1 - negl (κ)

. A scheme has perfect correctness if the probability is 1.

Definition 11 (Homomorphic encryption [128]).

An asymmetric encryption scheme $Π = (Gen, Enc, Dec)$ is homomorphic, with respect to ternary operators ⊙, ⊕, and ⊗,32

³²
For brevity, we write Π is a homomorphic asymmetric encryption scheme as opposed to the more verbose Π is a homomorphic asymmetric encryption scheme, with respect to ternary operators ⊙, ⊕, and ⊗.

if there exists a negligible function

negl

, such that for all security parameters κ, we have the following.33

³³

We write $X \circ_{pk} Y$ for the application of ternary operator ∘ to inputs X, Y, and $pk$ . We occasionally abbreviate $X \circ_{pk} Y$ as $X \circ Y$ , when $pk$ is clear from the context.

First, for all messages

m_{1}

and

m_{2}

we have

Pr [(pk, sk, m) \leftarrow Gen (κ); c_{1} \leftarrow Enc (pk, m_{1}); c_{2} \leftarrow Enc (pk, m_{2}) : m_{1}, m_{2} \in m \Rightarrow Dec (sk, c_{1} \otimes_{pk} c_{2}) = Dec (sk, c_{1}) ⊙_{pk} Dec (sk, c_{2})] > 1 - negl (κ)

. Secondly, for all messages

m_{1}

and

m_{2}

, and all coins

r_{1}

and

r_{2}

, we have

Pr [(pk, sk, m) \leftarrow Gen (κ) : m_{1}, m_{2} \in m \Rightarrow Enc (pk, m_{1}; r_{1}) \otimes_{pk} Enc (pk, m_{2}; r_{2}) = Enc (pk, m_{1} ⊙_{pk} m_{2}; r_{1} \oplus_{pk} r_{2})] > 1 - negl (κ)

. We say Π is additively homomorphic, if for all security parameters κ, key pairs

pk, sk

, and message spaces

m

, such that there exists coins r and

(pk, sk, m) = Gen (κ; r)

, we have

⊙_{pk}

is the addition operator in group

(m, ⊙_{pk})

Definition 12 (

IND - CPA

[7]).

Let $Π = (Gen, Enc, Dec)$ be an asymmetric encryption scheme, $A$ be an adversary, κ be the security parameter, and $IND - CPA$ be the following game. 34

³⁴
Our definition of an asymmetric encryption scheme explicitly defines the plaintext space, whereas Bellare et al. [7] leave the plaintext space implicit; this change is reflected in our definition of $IND - CPA$ . Moreover, we provide the adversary with the message space and security parameter. We adapt $IND - PA 0$ similarly.

In the above game, we require $m_{0}, m_{1} \in m$ and $| m_{0} | = | m_{1} |$ . We say Π satisfies $IND - CPA$ , if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (IND - CPA (Π, A, κ)) ⩽ \frac{1}{2} + negl (κ)$ .

Definition 13 (

IND - PA 0

[10]).

Let $Π = (Gen, Enc, Dec)$ be an asymmetric encryption scheme, $A$ be an adversary, κ be the security parameter, and $IND - PA 0$ be the following game.

In the above game, we require $m_{0}, m_{1} \in m$ and $| m_{0} | = | m_{1} |$ . We say Π satisfies $IND - PA 0$ , if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (IND - PA 0 (Π, A, κ)) ⩽ \frac{1}{2} + negl (κ)$ .

A.2. Proof systems

Definition 14 (Non-interactive proof system [128]).

A non-interactive proof system for a relation R is a tuple of algorithms $(Prove, Verify)$ , such that:

Prove , denoted $σ \leftarrow Prove (s, w, κ)$ , is executed by a prover to prove $(s, w) \in R$ .

Verify , denoted $v \leftarrow Verify (s, σ, κ)$ , is executed by anyone to check the validity of a proof. We assume $Verify$ is deterministic.

Moreover, the system must be complete: there exists a negligible function

negl

, such that for all statement and witnesses

(s, w) \in R

and security parameters κ, we have

Pr [σ \leftarrow Prove (s, w, κ) : Verify (s, σ, κ) = 1] > 1 - negl (κ)

. A system has perfect completeness if the probability is 1.

Definition 15 (Fiat-Shamir transformation [59]).

Given a sigma protocol $Σ = (Comm, Chal, Resp, {Verify}_{Σ})$ for relation R and a hash function $H$ , the Fiat-Shamir transformation, denoted $FS (Σ, H)$ , is the non-interactive proof system $(Prove, Verify)$ , defined as follows:

A string m can be included in the hashes computed by algorithms $Prove$ and $Verify$ . That is, the hashes are computed in both algorithms as $chal \leftarrow H (comm, s, m)$ . We write $Prove (s, w, m, κ)$ and $Verify (s, (comm, resp), m, k)$ for invocations of $Prove$ and $Verify$ which include string m.

Definition 16 (Zero-knowledge [108]).

Let $Δ = (Prove, Verify)$ be a non-interactive proof system for a relation R, derived by application of the Fiat-Shamir transformation [ 59 ] to a random oracle $H$ and a sigma protocol. Moreover, let $S$ be an algorithm, $A$ be an adversary, κ be a security parameter, and $ZK$ be the following game.

Oracle $P$ is defined on inputs $(s, w) \in R$ as follows:

$P (s, w)$ computes if $β = 0$ then $σ \leftarrow Prove (s, w, κ)$ else $σ \leftarrow S (s, κ)$ and outputs σ.

And algorithm

S

can patch random oracle

H

.35

³⁵
Random oracles can be programmed or patched. We will not need the details of how patching works, so we omit them here; see Bernhard et al. [19] for a formalisation.

We say Δ satisfies zero-knowledge, if there exists a probabilistic polynomial-time algorithm

S

, such that for all probabilistic polynomial-time algorithm adversaries

A

, there exists a negligible function

negl

, and for all security parameters κ, we have

Succ (ZK (Δ, A, H, S, κ)) ⩽ \frac{1}{2} + negl (κ)

. An algorithm

S

for which zero-knowledge holds is called a simulator for

(Prove, Verify)

Definition 17 (Simulation sound extractability [19,67,128]).

Suppose Σ is a sigma protocol for relation R, $H$ is a random oracle, and $(Prove, Verify)$ is a non-interactive proof system, such that $FS (Σ, H) = (Prove, Verify)$ . Further suppose $S$ is a simulator for $(Prove, Verify)$ and $H$ can be patched by $S$ . Proof system $(Prove, Verify)$ satisfies simulation sound extractability if there exists a probabilistic polynomial-time algorithm $K$ , such that for all probabilistic polynomial-time adversaries $A$ and coins r, there exists a negligible function $negl$ , such that for all security parameters κ, we have:36

³⁶
We extend set membership notation to vectors: we write $x \in x$ if x is an element of the set ${x [i] : 1 ⩽ i ⩽ | x |}$ .

where $A (—; r)$ denotes running adversary $A$ with an empty input and coins r, where H is a transcript of the random oracle’s input and output, and where oracles $A^{'}$ and $P$ are defined below:

$A^{'} ()$ . Computes $Q^{'} \leftarrow A (—; r)$ , forwarding any of $A$ ’s oracle queries to $K$ , and outputs $Q^{'}$ . By running $A (—; r)$ , $K$ is rewinding the adversary.

$P (s)$ . Computes $σ \leftarrow S (s, κ); P \leftarrow (P [1], \dots, P [| P |], (s, σ))$ and outputs σ.

Algorithm

K

is an extractor for

(Prove, Verify)

Theorem 15 (from [19]).

Let Σ be a sigma protocol for relation R, and let $H$ be a random oracle. Suppose Σ satisfies special soundness and special honest verifier zero-knowledge. Non-interactive proof system $FS (Σ, H)$ satisfies zero-knowledge and simulation sound extractability.

The Fiat-Shamir transformation may include a string in the hashes computed by functions $Prove$ and $Verify$ . Simulators can be generalised to include such a string too. We write $S (s, m, κ)$ for invocations of simulator $S$ which include string m. And remark that Theorem 15 can be extended to this generalisation.

B. Ballot independence: Non-malleability game

We formalise an alternative definition of ballot independence as a non-malleability game, called comparison based non-malleability under chosen vote attack ( $CNM - CVA$ ), as a straightforward adaptation of the non-malleability definition for asymmetric encryption by Bellare & Sahai [10].

Definition 18 ( $CNM - CVA$ ).

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $A$ be an adversary, κ be a security parameter, and $cnm - cva$ and $cnm - cva - $$ be the following games.

In the above games, we require that relation R is computable in polynomial time. We say Γ satisfies comparison based non-malleability under chosen vote attack ( $CNM - CVA$ ), if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (cnm - cva (Γ, A, κ)) - Succ (cnm - cva - $ (Γ, A, κ)) ⩽ negl (κ)$ .

$CNM - CVA$ is satisfied if no adversary can distinguish between games $cnm - cva$ and $cnm - cva - $$ . That is, for all adversaries, the adversary wins $cnm - cva$ iff the adversary looses $cnm - cva - $$ , with negligible probability. The first three steps of games $cnm - cva$ and $cnm - cva - $$ are identical, thus, these steps cannot be distinguished. Then, game $cnm - cva - $$ performs an additional step: the challenger samples a second vote $v^{'}$ from vote space V. Thereafter, game $cnm - cva$ , respectively game $cnm - cva - $$ , proceeds as follows: the challenger constructs a challenge ballot b for v, respectively $v^{'}$ ; the adversary is given ballot b and computes a relation R and bulletin board $bb$ ; and the challenger tallies $bb$ to derive election outcome $v$ and evaluates whether $R (v, v)$ holds. Hence, $CNM - CVA$ is satisfied if there is no advantage of the relation computed by an adversary given a challenge ballot for v, over the relation computed by the adversary given a challenge ballot for $v^{'}$ . That is, for all adversaries, we have with negligible probability that the relation evaluated by the challenger in $cnm - cva$ holds iff the relation evaluated in $cnm - cva - $$ does not hold. It follows that no adversary can meaningfully relate ballots. On the other hand, if $CNM - CVA$ is not satisfied, then there exists a strategy to construct related ballots.

$CNM - CVA$ avoids crediting the adversary for trivial and unavoidable relations which hold if the challenge ballot appears on the bulletin board. For example, suppose the adversary is given a challenge ballot for v in $cnm - cva$ , respectively $v^{'}$ in $cnm - cva - $$ . This adversary could output a bulletin board containing only the challenge ballot and a relation R such that $R (v, v)$ holds if $v [v] = 1$ , hence, the relation evaluated in $cnm - cva$ holds, whereas the relation evaluated in $cnm - cva - $$ does not hold, but the adversary looses in both games because the challenge ballot appears on the bulletin board. By contrast, if the adversary can derive a ballot meaningfully related to the challenge ballot, then the adversary can win the game. For instance, Cortier & Smyth [46,47] identify a class of vulnerabilities against voting systems, which can be exploited as follows: an adversary observes a voter’s ballot, casts a meaningfully related ballot, and abuses the relation to recover the voter’s vote from the election outcome.

Comparing $CNM - CVA$ and $CNM - CPA$ . Unsurprisingly, the distinction between non-malleability for asymmetric encryption ( $CNM - CPA$ ) and non-malleability for election schemes ( $CNM - CVA$ ) is similar to the distinction between indistinguishability for asymmetric encryption and indistinguishability for election schemes (§3.2), namely, $CNM - CPA$ performs a parallel decryption, whereas $CNM - CVA$ performs a single tally.

Our ballot independence games are adaptations of standard security definitions for asymmetric encryption: $CNM - CVA$ is based on non-malleability for encryption and $IND - CVA$ is based on indistinguishability for encryption. Bellare & Sahai [10] have shown that non-malleability is equivalent to indistinguishability for encryption and their proof can be adapted to show that $CNM - CVA$ and $IND - CVA$ are equivalent.

Theorem 16 ( $CNM - CVA = IND - CVA$ ).

Given an election scheme Γ, we have Γ satisfies $CNM - CVA$ iff Γ satisfies $IND - CVA$ .

Proof.
For the if implication, suppose Γ does not satisfy $CNM - CVA$ , hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $Succ (cnm - cva (Γ, A, κ)) - Succ (cnm - cva - $ (Γ, A, κ)) > negl (κ)$ . We construct an adversary $B$ against game $IND - CVA$ from $A$ .

$B (pk, κ)$ computes $(V, nc) \leftarrow A (pk, κ); v, v^{'} \leftarrow_{R} V$ and outputs $(v, v^{'}, nc)$ .

$B (b)$ computes $(R, bb) \leftarrow A (b)$ and outputs $bb$ .

$B (v)$ outputs 0 if $R (v, v)$ holds and 1 otherwise.
If the challenger selects $β = 0$ in game $IND - CVA$ , then adversary $B$ simulates $A$ ’s challenger to $A$ in $cnm - cva$ and $B$ ’s success (which requires $R (v, v)$ to hold) is $Succ (cnm - cva (Γ, A, κ))$ . Otherwise ( $β = 1$ ), adversary $B$ simulates $A$ ’s challenger to $A$ in $cnm - cva - $$ and, since $B$ will evaluate $R (v, v)$ , $B$ ’s success (which requires $R (v, v)$ not to hold) is $1 - Succ (cnm - cva - $ (Γ, A, κ))$ . It follows that $Succ (IND - CVA (Γ, B, κ)) = \frac{1}{2} \cdot (Succ (cnm - cva (Γ, A, κ)) + 1 - Succ (cnm - cva - $ (Γ, A, κ)))$ , therefore, $2 \cdot Succ (IND - CVA (Γ, B, κ)) - 1 = Succ (cnm - cva (Γ, A, κ)) - Succ (cnm - cva - $ (Γ, A, κ))$ . Thus, $Succ (IND - CVA (Γ, B, κ)) > \frac{1}{2} + \frac{1}{2} \cdot negl (κ)$ , concluding our proof of the if implication.

For the only if implication, suppose Γ does not satisfy $IND - CVA$ , hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $Succ (IND - CVA (Γ, A, κ)) > \frac{1}{2} + negl (κ)$ . We construct an adversary $B$ against $CNM - CVA$ from $A$ .

$B (pk, κ)$ computes $(v_{0}, v_{1}, nc) \leftarrow A (pk, κ)$ and outputs $({v_{0}, v_{1}}, nc)$ .

$B (b)$ computes $bb \leftarrow A (b)$ , picks coins r uniformly at random, derives a relation R such that $R (v, v)$ holds if there exists a bit g such that $v = v_{g} \land g = A (v; r)$ and fails otherwise, and outputs $(R, bb)$ .
Adversary $B$ simulates $A$ ’s challenger to $A$ in game $IND - CVA$ . Indeed, the challenge ballot is equivalently computed. As is the election outcome. The computation $A (v; r)$ is not black-box, but this does not matter: it is still invoked exactly once in the game. Let us consider adversary $B$ ’s success against $cnm - cva$ and $cnm - cva - $$ .

Game $cnm - cva$ samples a single vote v from V. By inspection of $cnm - cva$ and $IND - CVA$ , we have $Succ (cnm - cva (Γ, B, κ)) = Succ (IND - CVA (Γ, A, κ))$ , hence, $Succ (cnm - cva (Γ, B, κ)) - \frac{1}{2} > negl (κ)$ .

Game $cnm - cva - $$ samples votes v and $v^{'}$ from V. Vote v is independent of $A$ ’s perspective, indeed, an equivalent formulation of $cnm - cva - $$ could sample v after $A$ has terminated and immediately before evaluating the adversary’s relation. By inspection of $cnm - cva - $$ and $IND - CVA$ , we have $Succ (cnm - cva - $ (Γ, B, κ)) = \frac{1}{2} \cdot Succ (IND - CVA (Γ, A, κ)) + \frac{1}{2} \cdot (1 - Succ (IND - CVA (Γ, A, κ))) = \frac{1}{2}$ .
It follows that $Succ (cnm - cva (Γ, B, κ)) - Succ (cnm - cva - $ (Γ, B, κ)) > negl (κ)$ . □

C. Proofs

C.1. Proof of Theorem 1

Suppose Γ does not satisfy ballot independence, hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $Succ (IND - CVA) > \frac{1}{2} + negl (κ)$ . We construct an adversary $B$ against $Ballot - Secrecy$ from $A$ .

$B (pk, κ)$ computes $(v_{0}, v_{1}, nc) \leftarrow A (pk, κ)$ and outputs $nc$ .

$B ()$ computes $b \leftarrow O (v_{0}, v_{1}); bb \leftarrow A (b)$ and outputs $bb$ .

$B (v, pf)$ computes $g \leftarrow A (v)$ and outputs g.

Adversary

B

simulates

A

’s challenger to

A

. Indeed, the challenge ballot and election outcome are equivalently computed. Moreover, the challenge ballot does not appear on the bulletin board, hence, the bulletin board is balanced. It follows that

Succ (IND - CVA (Γ, A, κ)) = Succ (Ballot - Secrecy (Γ, B, κ))

, hence,

Succ (Ballot - Secrecy (Γ, B, κ)) > \frac{1}{2} + negl (κ)

, concluding our proof. □

C.2. Proof of Proposition 3

In essence, the proof follows from Theorem 4. Albeit, formally, a few extra steps are required. In particular, the definition of an election scheme with zero-knowledge proofs demands that tallying proofs must be computed by a zero-knowledge non-interactive proof system, but an election scheme without tallying proofs need not compute proofs with such a system. Thus, we must introduce an election scheme with zero-knowledge proofs and prove that it is equivalent to the election scheme without proofs. This is trivial, so we do not pursue the details. □

C.3. Proof of Theorem 4

Definition 19 (Zero-knowledge tallying proofs).

An election scheme $Γ = (Setup, Vote, Tally)$ has zero-knowledge tallying proofs, if there exists a non-interactive zero-knowledge proof system $(Prove, Verify)$ , such that for all security parameters κ, integers $nc$ , bulletin boards $bb$ , outputs $(pk, sk, mb, mc)$ of $Setup (κ)$ , and outputs $(v, pf)$ of $Tally (sk, bb, nc, κ)$ , we have $pf$ is an output of algorithm $Prove$ parameterised with statement $(pk, bb, nc, v)$ and coins chosen uniformly at random.

(Beyond the statement and coins, algorithm $Prove$ additionally inputs some witness and security parameter.)

Definition 20.
Let $Γ = (Setup, Vote, Tally)$ be an election scheme with zero-knowledge tallying proofs, $A$ be an adversary, and κ be a security parameter. Moreover, let $S$ be the simulator for the non-interactive zero-knowledge proof system used by algorithm $Tally$ to compute tallying proofs. We define game $BS$ as follows.

Predicate $balanced$ and oracle $O$ are defined as per game $Ballot - Secrecy$ .
Lemma 17.
Let $Γ = (Setup, Vote, Tally)$ be an election scheme with zero-knowledge tally proofs, $S$ be the simulator for that proof system, $A$ be an adversary, and κ be a security parameter. If Γ satisfies $Additivity$ , then $| Succ (BS (Γ, A, S, κ)) - Succ (Ballot - Secrecy (Γ, A, κ)) | ⩽ negl (κ)$ , for all negligible functions $negl$ and some security parameter κ.
Proof.
The challengers in games $BS$ and $Ballot - Secrecy$ both compute public keys using the same algorithm and provide those keys, along with the security parameter, as input to the first adversary call, thus, these inputs and corresponding outputs are equivalent. Moreover, the left-right oracle is the same in both $BS$ and $Ballot - Secrecy$ , hence, the bulletin board output by the second adversary call is equivalent in both games. Furthermore, predicate $balanced$ is satisfied in $BS$ iff it is satisfied in $Ballot - Secrecy$ , hence, if predicate $balanced$ is not satisfied, then $Succ (BS (Γ, A, S, κ)) = Succ (Ballot - Secrecy (Γ, A, κ))$ , concluding our proof. Otherwise, it suffices to show that the outcome and tallying proof are equivalently computed in $BS$ and $Ballot - Secrecy$ , since this ensures the inputs to the third adversary call are equivalent, thus the corresponding outputs are equivalent too, which suffices to conclude.

In $Ballot - Secrecy$ , the outcome is computed by tallying the bulletin board. By comparison, in $BS$ , the outcome is computed by tallying the ballots on the bulletin board that were constructed by the adversary (i.e., ballots in $bb ∖ {b ∣ (b, v_{0}, v_{1}) \in L}$ , where $bb$ is the bulletin board and L is the set constructed by the oracle) and by simulating the tallying of any remaining ballots (i.e., ballots constructed by the oracle, namely, ballots in $bb \cap {b ∣ (b, v_{0}, v_{1}) \in L}$ ). Suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ and $nc$ is an integer. Since Γ satisfies $Additivity$ , computing $v$ as

is equivalent to computing $v$ as

and as

Moreover, by correctness of Γ, we have $Tally (sk, \emptyset, nc, κ)$ outputs $(v^{'}, {pf}^{'})$ such that $v^{'}$ is a zero-filled vector. Hence, the above computation is equivalent to

Thus, to prove the outcome is computed equivalently in $Ballot - Secrecy$ and $BS$ , it suffices to prove that the simulations are valid, i.e., computing the above for-loop is equivalent to computing for $b \in bb \land (b, v_{0}, v_{1}) \in L$ do $v [v_{0}] \leftarrow v [v_{0}] + 1$ .

In $BS$ , we have for all $(b, v_{0}, v_{1}) \in L$ that b is an output of $Vote (pk, v_{β}, nc, κ)$ such that $v_{0}, v_{1} \in {1, ..., nc}$ , where β is the bit chosen by the challenger. Moreover, by correctness of Γ, we have $Tally (sk, {b}, nc, κ)$ outputs $(v^{'}, {pf}^{'})$ such that $v^{'}$ is a zero-filled vector, except for index $v_{β}$ , which contains one, hence, computing $v \leftarrow v + v^{'}$ inside the for-loop is equivalent to computing $v [v_{β}] \leftarrow v [v_{β}] + 1$ inside the loop. Furthermore, since predicate $balanced$ holds in $BS$ , we have for all $v \in {1, \dots, nc}$ that $| {b ∣ b \in bb \land \exists v_{1} . (b, v, v_{1}) \in L} | = | {b ∣ b \in bb \land \exists v_{0} . (b, v_{0}, v) \in L} |$ . Hence, in $BS$ , computing

is equivalent to computing

Thus, the simulation is valid in $BS$ .

In $Ballot - Secrecy$ , the tallying proof is computed by tallying the bulletin board. By comparison, in $BS$ , the tallying proof is computed by simulator $S$ . Since Γ has zero-knowledge tallying proofs, there exists a non-interactive proof system $(Prove, Verify)$ such that for all $(v, pf)$ output by $Tally (sk, bb, nc, κ)$ , we have $pf$ is an output of algorithm $Prove$ parameterised with statement $(pk, bb, nc, v)$ and coins chosen uniformly at random. Moreover, since $S$ is a simulator for $(Prove, Verify)$ , proofs output by algorithm $Prove$ are indistinguishable from outputs of simulator $S$ . Thus, tallying proofs are equivalently computed in $Ballot - Secrecy$ and $BS$ , thereby concluding our proof. □

Let $BS - 0$ , respectively $BS - 1$ , be the game derived from $BS$ by replacing $β \leftarrow_{R} {0, 1}$ with $β \leftarrow 0$ , respectively $β \leftarrow 1$ . These games are trivially related to $BS$ , namely, $Succ (BS (Γ, A, S, κ)) = \frac{1}{2} \cdot Succ (BS - 0 (Γ, A, S, κ)) + \frac{1}{2} \cdot Succ (BS - 1 (Γ, A, S, κ))$ . Moreover, let $BS - 1 : 0$ be the game derived from $BS - 1$ by replacing $g = β$ with $g = 0$ and let $G_{j}$ be the game derived from $BS - 1 : 0$ by removing $β \leftarrow 1$ and redefining oracle $O$ such that $O (v_{0}, v_{1})$ computes, on inputs $v_{0}, v_{1} \in {1, ..., nc}$ , the following:

Games $G_{0}, G_{1}, \dots$ are distinguished from games $BS - 0$ and $BS - 1 : 0$ by their left-right oracles. In particular, the first j left-right oracle queries in $G_{j}$ construct ballots for the oracle’s “right” input and any remaining queries construct ballots for the oracle’s “left” input, whereas the left-right oracle in $BS - 0$ , respectively $BS - 1 : 0$ , always constructs ballots for the oracle’s “left,” respectively “right,” input. We relate game $BS - 1 : 0$ to $BS - 1$ , games $BS - 0$ and $BS - 1 : 0$ to the hybrid games $G_{0}, G_{1}, \dots$ , and we prove Theorem 4 using these relations. Lemma 18.
Let Γ be an election scheme with zero-knowledge tally proofs, $S$ be the simulator for that proof system, $A$ be an adversary, and κ be a security parameter. If adversary $A$ wins game $Ballot - Secrecy$ against election scheme Γ, then $Succ (BS - 1 (Γ, A, S, κ)) = 1 - Succ (BS - 1 : 0 (Γ, A, S, κ))$ .
Lemma 19.
Let Γ be an election scheme with zero-knowledge tally proofs, $S$ be the simulator for that proof system, $A$ be an adversary, and κ be a security parameter. If Γ satisfies $Additivity$ , then $Succ (BS - 0 (Γ, A, S, κ)) = Succ (G_{0} (Γ, A, S, κ))$ and $Succ (BS - 1 : 0 (Γ, A, S, κ)) = Succ (G_{q} (Γ, A, S, κ))$ , where q is an upper-bound on $A$ ’s left-right oracle queries.
Proof.
Games $BS - 0$ and $G_{0}$ , respectively $BS - 1 : 0$ and $G_{q}$ , are identical up to the oracle, except $BS - 0$ computes $β \leftarrow 0$ and checks $g = β$ , which is equivalent to $G_{0}$ checking $g = 0$ , respectively $BS - 1 : 0$ computes $β \leftarrow 1$ and checks $g = 0$ , which is equivalent to $G_{q}$ checking $g = 0$ . Thus, it suffices to show that oracle outputs in $BS - 0$ are equivalent to oracle outputs in $G_{0}$ , and similarly for $BS - 1 : 0$ and $G_{q}$ . Left-right oracles queries $O (v_{0}, v_{1})$ in games $BS - 0$ and $G_{0}$ output ballots for vote $v_{0}$ , hence, outputs are equivalent in both games. Oracle outputs in $BS - 1 : 0$ and $G_{q}$ are similarly equivalent, in particular, left-right oracles queries $O (v_{0}, v_{1})$ in both games output ballots for vote $v_{1}$ , because q is an upper-bound on the left-right oracle queries, therefore, $| L | < q$ in $G_{q}$ , concluding our proof. □
Proof of Theorem 4.
By Theorem 1, it suffices to prove that ballot independence implies ballot secrecy. Suppose Γ does not satisfy ballot secrecy, hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $\begin{array}{l} \frac{1}{2} + negl (κ) < Succ (Ballot - Secrecy (Γ, A, κ)) \end{array}$ Let $Γ = (Setup, Vote, Tally)$ . Since Γ has zero-knowledge tallying proofs, tallying proofs output by $Tally$ are computed by a non-interactive zero-knowledge proof system. Let algorithm $S$ be the simulator for that proof system. By Lemma 17, we have $\begin{array}{l} \approx Succ (BS (Γ, A, S, κ)) \end{array}$ By definition of $BS - 0$ and $BS - 1$ , we have $\begin{array}{l} = \frac{1}{2} \cdot (Succ (BS - 0 (Γ, A, S, κ)) + Succ (BS - 1 (Γ, A, S, κ))) \end{array}$ And, by Lemma 18, we have $\begin{array}{l} = \frac{1}{2} \cdot (Succ (BS - 0 (Γ, A, S, κ)) + 1 - Succ (BS - 1 : 0 (Γ, A, S, κ))) \\ = \frac{1}{2} + \frac{1}{2} \cdot (Succ (BS - 0 (Γ, A, S, κ)) - Succ (BS - 1 : 0 (Γ, A, S, κ))) \end{array}$ Let q be an upper-bound on $A$ ’s left-right oracle queries. Hence, by Lemma 19, we have $\begin{array}{l} = \frac{1}{2} + \frac{1}{2} \cdot (Succ (G_{0} (Γ, A, S, κ)) - Succ (G_{q} (Γ, A, S, κ))) \end{array}$ which can be rewritten as the telescoping series $\begin{array}{l} = \frac{1}{2} + \frac{1}{2} \cdot \sum_{1 ⩽ j ⩽ q} Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ)) \end{array}$ Let $j \in {1, \dots, q}$ be such that $Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ))$ is the largest term in that series. Hence, $\begin{array}{l} ⩽ \frac{1}{2} + \frac{1}{2} \cdot q \cdot (Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ))) \end{array}$ Thus, $\begin{matrix} \frac{1}{2} + \frac{1}{q} \cdot negl (κ) ⩽ \frac{1}{2} + \frac{1}{2} \cdot (Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ))) \end{matrix}$ From $A$ , we construct the following adversary $B$ against $IND - CVA$ :

$B (pk, κ)$ computes $nc \leftarrow A (pk, κ); L \leftarrow \emptyset$ and runs $A^{O} ()$ , handling $A$ ’s oracle queries $O (v_{0}, v_{1})$ as follows: if $| L | < j$ , then compute $b \leftarrow Vote (pk, v_{1}, nc, κ); L \leftarrow L \cup {b, v_{0}, v_{1}}$ and return b to $A$ , otherwise, assign $v_{0}^{c} \leftarrow v_{0}; v_{1}^{c} \leftarrow v_{1}$ , and output $(v_{0}, v_{1}, nc)$ .

$B (b)$ assigns $L \leftarrow L \cup {(b, v_{0}^{c}, v_{1}^{c})}$ ; returns b to $A$ and handles any further oracle queries $O (v_{0}, v_{1})$ as follows, namely, compute $b \leftarrow Vote (pk, v_{0}, nc, κ); L \leftarrow L \cup {(b, v_{0}, v_{1})}$ and return b to $A$ ; assigns $A$ ’s output to $bb$ ; and outputs $bb ∖ {b ∣ (b, v_{0}, v_{1}) \in L}$ .

$B (v)$ computes

and outputs g.
We prove that $B$ wins $IND - CVA$ with success of at least $\frac{1}{2} + \frac{1}{2} \cdot (Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ)))$ .

Suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ . Further suppose we run $B (pk, κ)$ . It is straightforward to see that $B$ simulates the challenger and oracle in both $G_{j - 1}$ and $G_{j}$ to $A$ . In particular, $B$ simulates query $O (v_{0}, v_{1})$ by computing $b \leftarrow Vote (pk, v_{1}, nc, κ)$ for the first $j - 1$ queries. Since $G_{j - 1}$ and $G_{j}$ are equivalent to adversaries that make fewer than j left-right oracle queries, adversary $A$ must make at least j queries to ensure $Succ (G_{j - 1} (Γ, A, S, κ)) - Succ (G_{j} (Γ, A, S, κ))$ is non-negligible. Hence, $B (pk, κ)$ terminates with non-negligible probability. Suppose adversary $B$ terminates by outputting $(v_{0}, v_{1}, nc)$ , where $v_{0}, v_{1}$ correspond to the inputs of the jth oracle query by $A$ . Further suppose b is an output of $Vote (pk, v_{β}, nc, κ)$ , where β is a bit. If $β = 0$ , then $B (b)$ simulates the oracle in $G_{j - 1}$ to $A$ , otherwise, $B (b)$ simulates the oracle in $G_{j}$ to $A$ . In particular, $B (b)$ responds to the jth oracle query with ballot b for $v_{β}$ , thus, simulating the challenger in $G_{j - 1}$ when $β = 0$ , respectively $G_{j}$ when $β = 1$ . And $B (b)$ responds to any further oracle queries $O (v_{0}, v_{1})$ with ballots for $v_{0}$ . Suppose $bb$ is an output of $A$ , thus $B (b)$ outputs $bb ∖ {b ∣ (b, v_{0}, v_{1}) \in L}$ . Further suppose $(v, pf)$ is an output of $Tally (sk, bb ∖ {b ∣ (b, v_{0}, v_{1}) \in L}, nc, κ)$ and g is an output of $B (v)$ . It is trivial to see that $B (v)$ simulates $A$ ’s challenger. Thus, either
$β = 0$ and $B$ simulates $G_{j - 1}$ to $A$ , thus, $g = β$ with at least the probability that $A$ wins $G_{j - 1}$ ; or

$β = 1$ and $B$ simulates $G_{j}$ to $A$ , thus, $g \neq 0$ with at least the probability that $B$ looses $G_{j}$ and, since $A$ wins game $Ballot - Secrecy$ , we have g is a bit, hence, $g = β$ .
It follows that the success of adversary $B$ is at least $\frac{1}{2} \cdot Succ (G_{j - 1} (Γ, A, S, κ)) + \frac{1}{2} \cdot (1 - Succ (G_{j} (Γ, A, S, κ)))$ , thus we conclude our proof. □

C.4. Proof of Lemma 7

Suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ and $(nc, bb, {bb}^{'})$ is an output of $A (pk, κ)$ such that $nc ⩽ mc$ and $| bb | ⩽ mb$ . Further suppose $(v, pf)$ is an output $Tally (sk, bb, nc, κ)$ , $(v_{0}, {pf}_{0})$ is an output of $Tally (sk, bb ∖ {bb}^{'}, nc, κ)$ , and $(v_{1}, {pf}_{1})$ is an output of $Tally (sk, bb \cap {bb}^{'}, nc, κ)$ . Let $v^{+} = v_{0} + v_{1}$ . Moreover, let $v^{*} = correct - outcome (pk, nc, bb, κ)$ , $v_{0}^{*} = correct - outcome (pk, nc, bb ∖ {bb}^{'}, κ)$ , and $v_{1}^{*} = correct - outcome (pk, nc, bb \cap {bb}^{'}, κ)$ . By definition of function $correct - outcome$ , we have $v^{*} = v_{0}^{*} + v_{1}^{*}$ . Moreover, by $Tally - Soundness$ , we have $v = v^{*}$ , $v_{0} = v_{0}^{*}$ , and $v_{1} = v_{1}^{*}$ , with overwhelming probability. It follows by transitivity that $v = v^{+}$ , with overwhelming probability.

C.5. Proof of Proposition 11

We present a construction (Definition 21) for encryption schemes (Lemma 20) which are clearly not secure (Lemma 21). Nevertheless, the construction produces encryption schemes that are sufficient for ballot secrecy (Lemma 22). The proof of Proposition 11 follows from Lemmata 20–22.

Definition 21.
Given an asymmetric encryption scheme $Π = ({Gen}_{Π}, {Enc}_{Π}, {Dec}_{Π})$ and a constant symbol ω, let $Leak (Π, ω) = ({Gen}_{Π}, {Enc}_{Π}, Dec)$ such that $Dec (sk, c)$ proceeds as follows: if $c = ω$ , then output $sk$ , otherwise, compute $m \leftarrow {Dec}_{Π} (sk, c)$ and output m.
Lemma 20.
Given an asymmetric encryption scheme Π and a constant symbol ω such that Π’s ciphertext space does not contain ω, we have $Leak (Π, ω)$ is an asymmetric encryption scheme.
Proof sketch.
The proof follows immediately from correctness of the underlying encryption scheme, because constant symbol ω does not appear in the scheme’s ciphertext space. □
Lemma 21.
Given an asymmetric encryption scheme Π and a constant symbol ω such that Π’s ciphertext space does not contain ω and Π’s message space is larger than one for some security parameter, we have $Leak (Π, ω)$ does not satisfy $IND - PA 0$ .
Proof sketch.
The proof is trivial: an adversary can output two distinct messages and a vector containing constant symbol ω during the first two adversary calls, learn the private key from the parallel decryption, and use the key to recover the plaintext from the challenge ciphertext, which allows the adversary to win the game. □
Lemma 22.
Let $Π = (Gen, Enc, Dec)$ be an asymmetric encryption scheme and ω be a constant symbol. Suppose Π’s ciphertext space does not contain ω and Π’s message space is smaller than the private key. Further suppose $Enc 2 Vote (Π)$ satisfies $Ballot - Secrecy$ . We have $Enc 2 Vote (Leak (Π, ω))$ satisfies $Ballot - Secrecy$ .
Proof.
Let $Enc 2 Vote (Π) = (Setup, Vote, Tally)$ and let $Enc 2 Vote (Leak (Π, ω)) = ({Setup}^{'}, {Vote}^{'}, {Tally}^{'})$ . By definition of $Enc 2 Vote (Π)$ and $Leak$ , we have $Setup = {Setup}^{'}$ and $Vote = {Vote}^{'}$ . Suppose $m$ is Π’s message space. By definition of $Leak$ , we have $m$ is $Leak (Π, ω)$ ’s message space too. Moreover, since $| m |$ is smaller than the private key, we have for all security parameters κ, bulletin boards $bb$ , and number of candidates $nc$ , that $nc ⩽ | m |$ implies $\begin{matrix} Pr [(pk, sk, m) \leftarrow Gen (κ); (v, pf) \leftarrow Tally (sk, bb, nc, κ); \\ (v^{'}, {pf}^{'}) \leftarrow {Tally}^{'} (sk, bb, nc, κ) : v = v^{'} \land pf = {pf}^{'}] = 1, \end{matrix}$

because $Enc 2 Vote (Π)$ ensures that $v^{'}$ is not influenced by decrypting ω (witness that decrypting ω outputs $sk$ such that $sk > | m | ⩾ nc$ ) and $pf$ is a constant symbol. It follows for all adversaries $A$ and security parameters κ that games $Ballot - Secrecy (Enc 2 Vote (Π), A, κ)$ and $Ballot - Secrecy (Enc 2 Vote (Leak (Π, ω)), A, κ)$ are equivalent, hence, we have $Succ (Ballot - Secrecy (Enc 2 Vote (Π), A, κ)) = Succ (Ballot - Secrecy (Enc 2 Vote (Leak (Π, ω), A, κ))$ . Moreover, since $Enc 2 Vote (Π)$ satisfies $Ballot - Secrecy$ , it follows that $Enc 2 Vote (Leak (Π, ω))$ satisfies $Ballot - Secrecy$ too. □
Proof of Proposition 11.
Let Π be an asymmetric encryption scheme and ω be a constant symbol. Suppose Π’s ciphertext space does not contain ω. Further suppose Π’s message space is larger than one for some security parameter, but smaller than the private key. We have $Enc 2 Vote (Leak (Π, ω))$ is an asymmetric encryption scheme (Lemma 20) such that $Enc 2 Vote (Leak (Π, ω))$ satisfies $Ballot - Secrecy$ (Lemma 22), but $Leak (Π, ω)$ does not satisfy $IND - PA 0$ (Lemma 21), concluding our proof. □

C.6. Proof of Lemma 12

Let $Π = (Gen, Enc, Dec)$ and $Enc 2 Vote (Π) = (Setup, Vote, Tally)$ . Election scheme $Enc 2 Vote (Π)$ satisfies $HK - Injectivity$ (Lemma 9). Suppose $Enc 2 Vote (Π)$ does not satisfy $Tally - Soundness$ , hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $Succ (Tally - Soundness (Enc 2 Vote (Π), A, κ)) ⩽ 1 - negl (κ)$ . Further suppose $({pk}^{'}, sk, mb, mc)$ is an output of $Setup (κ)$ , $(nc, bb)$ is an output of $A (pk, κ)$ , and $(v, pf)$ is an output of $Tally (sk, bb, nc, κ)$ . By definition of algorithm $Setup$ , we have ${pk}^{'}$ is a pair $(pk, m)$ such that $(pk, sk, m)$ is an output of $Gen (κ)$ , and $mc$ is the largest integer such that ${0, \dots, mc} \subseteq {0} \cup m$ . Moreover, since $A$ is a winning adversary, we have $nc ⩽ mc$ . By definition of algorithm $Tally$ , we have $v$ is initialised as a zero-filled vector of length $nc$ and updated by computing for $b \in bb$ do $v \leftarrow Dec (sk, b);$ if $1 ⩽ v ⩽ nc$ then $v [v] \leftarrow v [v] + 1$ . Since Π satisfies well-definedness and error symbol ⊥ is not an integer, that computation is equivalent to

with overwhelming probability. Although each ciphertext $Enc (pk, m; r) \in bb$ may not have been computed using coins r chosen uniformly at random, we nonetheless have $Dec (sk, Enc (pk, m; r)) = m$ , because Π is perfectly correct. Hence, the above computation is equivalent to

Thus, for all $v \in {1, \dots, nc}$ , we have $v [v] = ℓ$ if and only if $\exists^{= ℓ} b \in bb ∖ {⊥} : \exists r : b = Enc (pk, v; r)$ , with overwhelming probability. It follows by definition of $Vote$ that for all $v \in {1, \dots, nc}$ we have $\begin{matrix} v [v] = ℓ iff \exists^{= ℓ} b \in bb ∖ {⊥} : \exists r : b = Vote (pk, v, nc, κ; r) \end{matrix}$ with overwhelming probability. Thereby contradicting our assumption that $A$ is a winning adversary, since $v = correct - outcome (pk, nc, bb, κ)$ , with overwhelming probability, which concludes our proof. □

D. Helios

Smyth, Frink & Clarkson [128] formalise a generic construction for Helios-like election schemes (Definition 23), which is parameterised on the choice of homomorphic encryption scheme and sigma protocols for the relations introduced in the following definition.

Definition 22 (from [128]).

Let $(Gen, Enc, Dec)$ be a homomorphic asymmetric encryption scheme and Σ be a sigma protocol for a binary relation R.37

³⁷
Given a binary relation R, we write $((s_{1}, \dots, s_{l}), (w_{1}, \dots, w_{k})) \in R \Leftrightarrow P (s_{1}, \dots, s_{l}, w_{1}, \dots, w_{k})$ for $(s, w) \in R \Leftrightarrow P (s_{1}, \dots, s_{l}, w_{1}, \dots, w_{k}) \land s = (s_{1}, \dots, s_{l}) \land w = (w_{1}, \dots, w_{k})$ , hence, R is only defined over pairs of vectors of lengths l and k.

Σ proves correct key generation if a $((κ, pk, m), (sk, s)) \in R \Leftrightarrow (pk, sk, m) = Gen (κ; s)$ .

Further, suppose that

(pk, sk, m)

is the output of

Gen (κ; s)

, for some security parameter κ and coins s.

Σ proves plaintext knowledge in a subspace if $((pk, c, m^{'}), (m, r)) \in R \Leftrightarrow c = Enc (pk, m; r) \land m \in m^{'} \land m^{'} \subseteq m$ .

Σ proves correct decryption if $((pk, c, m), sk) \in R \Leftrightarrow m = Dec (sk, c) .$

Definition 23 (Generalised Helios [128]).

Suppose $Π = (Gen, Enc, Dec)$ is an additively homomorphic asymmetric encryption scheme, $Σ_{1}$ is a sigma protocol that proves correct key generation, $Σ_{2}$ is a sigma protocol that proves plaintext knowledge in a subspace, $Σ_{3}$ is a sigma protocol that proves correct decryption, and $H$ is a hash function. Let $FS (Σ_{1}, H) = (ProveKey, VerKey)$ , $FS (Σ_{2}, H) = (ProveCiph, VerCiph)$ , and $FS (Σ_{3}, H) = (ProveDec, VerDec)$ . We define election scheme generalised Helios, denoted $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H) = (Setup, Vote, Tally)$ , as follows.38

³⁸
We omit algorithm $Verify$ for brevity.

$Setup (κ)$ . Select coins s uniformly at random, compute $(pk, sk, m) \leftarrow Gen (κ; s); ρ \leftarrow ProveKey ((κ, pk, m), (sk, s), κ); {pk}^{'} \leftarrow (pk, m, ρ); {sk}^{'} \leftarrow (pk, sk)$ , let m be the largest integer such that ${0, \dots, m} \subseteq {0} \cup m$ , and output $({pk}^{'}, {sk}^{'}, m, m)$ .

. Parse ${pk}^{'}$ as a vector $(pk, m, ρ)$ . Output ⊥ if parsing fails or $VerKey ((κ, pk, m), ρ, κ) \neq 1 \lor v \notin {1, \dots, nc}$ . Select coins $r_{1}, \dots, r_{nc - 1}$ uniformly at random and compute:

Output ballot $(c_{1}, \dots, c_{nc - 1}, σ_{1}, \dots, σ_{nc})$ .

$Tally ({sk}^{'}, bb, nc, κ)$ . Initialise vectors $v$ of length $nc$ and $pf$ of length $nc - 1$ . Compute for $1 ⩽ j ⩽ nc$ do $v [j] \leftarrow 0$ . Parse ${sk}^{'}$ as a pair $(pk, sk)$ . Output $(v, pf)$ if parsing fails. Let ${b_{1}, \dots, b_{ℓ}}$ be the largest subset of $bb$ such that $b_{1} < \dots < b_{ℓ}$ and for all $1 ⩽ i ⩽ ℓ$ we have $b_{i}$ is a vector of length $2 \cdot nc - 1$ and $⋀_{j = 1}^{nc - 1} VerCiph ((pk, b_{i} [j], {0, 1}), b_{i} [j + nc - 1], j, κ) = 1 \land VerCiph ((pk, b_{i} [1] \otimes \dots \otimes b_{i} [nc - 1], {0, 1}), b_{i} [2 \cdot nc - 1], nc, κ) = 1$ . If ${b_{1}, \dots, b_{ℓ}} = \emptyset$ , then output $(v, pf)$ , otherwise, compute:

Output $(v, pf)$ .

The above algorithms assume

nc > 1

. Smyth, Frink & Clarkson define special cases of

Vote

and

Tally

when

nc = 1

. We omit those cases for brevity and, henceforth, assume

nc

is always greater than one.

The generic construction can be instantiated to derive Helios 2.0 and Helios’16. Definition 24 (Weak Fiat-Shamir transformation [19]).

The weak Fiat-Shamir transformation is a function $wFS$ that is identical to $FS$ , except that it excludes statement s in the hashes computed by $Prove$ and $Verify$ , as follows: $chal \leftarrow H (comm)$ .

Definition 25 (Helios 2.0 [128]).

Let $\hat{Helios}$ be $Helios$ after replacing all instances of the Fiat-Shamir transformation with the weak Fiat-Shamir transformation and excluding the (optional) messages input to $ProveCiph$ , i.e., $ProveCiph$ should be used as a ternary function. Helios 2.0 is $\hat{Helios} (Π, Σ_{1}, Σ_{2}, Σ_{3}, H)$ , where Π is additively homomorphic El Gamal [ 49 , §2], $Σ_{1}$ is the sigma protocol for proving knowledge of discrete logarithms by Chaum et al. [ 35 , Protocol 2], $Σ_{2}$ is the sigma protocol for proving knowledge of disjunctive equality between discrete logarithms by Cramer et al. [ 48 , Figure 1], $Σ_{3}$ is the sigma protocol for proving knowledge of equality between discrete logarithms by Chaum and Pedersen [ 36 , §3.2], and $H$ is SHA-256 [ 99 ].

Definition 26 (Helios 3.1.4 [128]).

Election scheme Helios 3.1.4 is Helios 2.0 after modifying the sigma protocols to perform the checks proposed by Chang-Fong & Essex [ 33 , §4].

Definition 27 (Helios’16 [128]).

Election scheme Helios’16 is $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H)$ , where Π is additively homomorphic El Gamal [ 49 , §2], $Σ_{1}$ is the sigma protocol for proving knowledge of discrete logarithms by Chaum et al. [ 35 , Protocol 2], $Σ_{2}$ is the sigma protocol for proving knowledge of disjunctive equality between discrete logarithms by Cramer et al. [ 48 , Figure 1], $Σ_{3}$ is the sigma protocol for proving knowledge of equality between discrete logarithms by Chaum & Pedersen [ 36 , §3.2], $H$ is a random oracle, and the sigma protocols are modified to perform the checks proposed by Chang-Fong & Essex [ 33 , §4].

Although Helios actually uses SHA-256 [99], we assume that

H

is a random oracle to prove Theorem 6. Moreover, we assume the sigma protocols used by Helios’16 satisfy the preconditions of generalised Helios, that is, [35, Protocol 2] is a sigma protocol for proving correct key generation, [48, Figure 1] is a sigma protocol for proving plaintext knowledge in a subspace, and [36, §3.2] is a sigma protocol for proving decryption. We leave formally proving this assumption as future work.

D.1. Proof of Theorem 6

The construction for Helios-like schemes produces election schemes with zero-knowledge tallying proofs (Lemma 23) that satisfy universal verifiability [128] and, thus, $Additivity$ (Lemma 27). They also satisfy ballot independence (Proposition 24). Hence, they satisfy ballot secrecy too (Theorem 4). We show that Helios’16 satisfies ballot secrecy.

Henceforth, we assume Π, $Σ_{1}$ , $Σ_{2}$ and $Σ_{3}$ satisfy the preconditions of Definition 23, and $H$ is a random oracle. Let $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H) = (Setup, Vote, Tally)$ and $Π = (Gen, Enc, Dec)$ . Moreover, let $FS (Σ_{1}, H) = (ProveKey, VerKey)$ , $FS (Σ_{2}, H) = (ProveCiph, VerCiph)$ , and $FS (Σ_{3}, H) = (ProveDec, VerDec)$ .

Lemma 23.
If $(ProveDec, VerDec)$ is zero-knowledge, then $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H)$ has zero-knowledge tallying proofs.
Proof sketch.
Suppose $A$ is an adversary and κ is a security parameter. Further suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ , $(nc, bb)$ is an output of $A (pk, κ)$ , and $(v, pf)$ is an output of $Tally (sk, bb, nc, κ)$ , such that $| bb | ⩽ mb \land nc ⩽ mc$ . By inspection of algorithm $Tally$ , tallying proof $pf$ is a vector of proofs produced by $ProveDec$ . Thus, there trivially exists a non-interactive proof system that could compute $pf$ , moreover, that proof system is zero-knowledge because $(ProveDec, VerDec)$ is zero-knowledge, which concludes our proof. □
Proposition 24.
Suppose Π is perfectly correct and satisfies $IND - CPA$ . Further suppose $(ProveKey, VerKey)$ and $(ProveCiph, VerCiph)$ satisfy special soundness and special honest verifier zero-knowledge. We have $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H)$ satisfies $IND - CVA$ .
Proof.
By Theorem 15, the proof systems have extractors and simulators. Let $Sim ProveKey$ , respectively $Sim ProveCiph$ , be the simulator for $(ProveKey, VerKey)$ , respectively $(ProveCiph, VerCiph)$ . And let $ExtProveCiph$ be the extractor for $(ProveCiph, VerCiph)$ .

Let $IND - {CPA}^{}$ be a variant of $IND - CPA$ in which: 1) the adversary outputs two vectors of messages $m_{0}$ and $m_{1}$ such that $| m_{0} | = | m_{1} |$ and for all $1 ⩽ i ⩽ | m_{0} |$ we have $| m_{0} [i] | = | m_{1} [i] |$ and $m_{0} [i]$ and $m_{1} [i]$ are from the encryption scheme’s message space, and 2) the challenger computes $c_{1} \leftarrow Enc (pk, m_{β} [1]); \dots; c_{| m_{β} |} \leftarrow Enc (pk, m_{β} [| m_{β} |])$ and inputs $c_{1}, \dots, c_{| m_{β} |}$ to the adversary. We have Π satisfies $IND - {CPA}^{}$ [78, §10.2.2].

Suppose $Helios (Π, Σ_{1}, Σ_{2}, Σ_{3}, H)$ does not satisfy $IND - CVA$ . Hence, there exists a probabilistic polynomial-time adversary $A$ , such that for all negligible functions $negl$ , there exists a security parameter κ and $\frac{1}{2} + negl (κ) < IND - CVA (Γ, A, κ)$ . Since $A$ is a winning adversary, we have $A ({pk}^{'}, κ)$ outputs $(v_{0}, v_{1}, nc)$ such that $v_{0} \neq v_{1}$ with non-negligible probability, hence, either $v_{0} < v_{1}$ or $v_{1} < v_{0}$ . For brevity, we suppose $v_{0} < v_{1}$ . (Our proof can be adapted to consider cases such that $v_{1} < v_{0}$ , but these details provide little value, so we do not pursue them.) We construct the following adversary $B$ against $IND - {CPA}^{}$ from $A$ :

$B (pk, m, κ)$ outputs $((1, 0), (0, 1))$ .

$B (c)$ proceeds as follows. First, compute:

Secondly, select coins $r_{1}, \dots, r_{nc - 1}$ uniformly at random and compute:

Thirdly, compute ${b_{1}, \dots, b_{ℓ}}$ as the largest subset of $bb$ satisfying the conditions of algorithm $Tally$ . Fourthly, initialise H as a transcript of the random oracle’s input and output, P as a transcript of simulated proofs, Q as a vector of length $nc - 1$ , and $v$ as a zero-filled vector of length $nc$ . Fifthly, compute:

Finally, output g.
We prove that $B$ wins $IND - {CPA}^{}$ .

Suppose $(pk, sk, m)$ is an output of $Gen (κ)$ and $(m_{0}, m_{1})$ is an output of $B (pk, m, κ)$ . Let $β \in {0, 1}$ . Further suppose $c_{1}$ is an output of $Enc (pk, m_{β} [1])$ and $c_{2}$ is an output of $Enc (pk, m_{β} [2])$ . Let $c = (c_{1}, c_{2})$ . Moreover, suppose ρ is an output of $Sim ProveKey ((κ, pk, m), κ)$ . Let ${pk}^{'} = (pk, m, ρ)$ . Suppose $(v_{0}, v_{1}, nc)$ is an output of $A ({pk}^{'}, κ)$ . Since $Sim ProveKey$ is a simulator for $(ProveKey, VerKey)$ , we have $B$ simulates the challenger in $IND - CVA$ to $A ({pk}^{'}, κ)$ . In particular, ${pk}^{'}$ is a triple containing a public key and corresponding message space generated $Gen$ , and a (simulated) proof of correct key generation. Suppose $B$ computes b and $bb$ is an output of $A (b)$ . Further suppose $B$ computes $v$ , and g is an output of $A (v)$ . The following claims prove that $B$ simulates the challenger in $IND - CVA$ to $A (b)$ and $A (v)$ , hence, $g = β$ , with at least the probability that $A$ wins $IND - CVA$ , concluding our proof. Claim 25.
Adversary $B$ ’s computation of b is equivalent to computing b as $b \leftarrow Vote ({pk}^{'}, v_{β}, nc, κ)$ .
Proof of Claim 25.
We have ${pk}^{'}$ parses as a vector $(pk, m, ρ)$ . Moreover, since $(pk, sk, m)$ is an output of $Gen (κ)$ , there exist coins r such that $(pk, sk, m) = Gen (κ; r)$ . Hence, $(sk, r)$ is a witness for statement $(κ, pk, m)$ . Furthermore, since $Sim ProveKey$ is a simulator for $(ProveKey, VerKey)$ and proofs output by $ProveKey$ are indistinguishable from outputs of $Sim ProveKey$ , we have $VerKey ((κ, pk, m), ρ, κ) κ, pk, m ρ = 1$ , with non-negligible probability. In addition, since $B$ is a winning adversary, we have $v_{0}, v_{1} \in {1, \dots, nc}$ , with non-negligible probability. It follows that $Vote ({pk}^{'}, v_{β}, nc, κ)$ does not output ⊥, with non-negligible probability. Indeed, computation $b \leftarrow Vote ({pk}^{'}, v_{β}, nc, κ)$ is equivalent to the following. Select coins $r_{1}, \dots, r_{nc - 1}$ uniformly at random and compute:

Since $v_{β} \in {v_{0}, v_{1}}$ , ciphertexts computed by the above for-loop all contain plaintext 0, except (possibly) ciphertext $c_{v_{0}}$ and, if defined, ciphertext $c_{v_{1}}$ . (Ciphertext $c_{v_{1}}$ only exists if $v_{1} < nc$ .) Given that $v_{0} < v_{1} ⩽ nc$ , ciphertext $c_{v_{0}}$ contains $1 - β$ , i.e., if $β = 0$ , then $c_{v_{0}}$ contains 1, otherwise ( $β = 1$ ), $c_{v_{0}}$ contains 0. If $v_{1} < nc$ , then ciphertext $c_{v_{1}}$ contains β. Moreover, since ⊙ is the addition operator in group $(m, ⊙)$ and 0 is the identity element in that group, if $v_{1} = nc$ , then plaintext m computed by the above algorithm is $1 - β$ , otherwise, $m = 1 - β ⊙ β = 1$ . Hence, the above algorithm is equivalent to selecting coins $r_{1}, \dots, r_{nc - 1}$ uniformly at random and computing:

Computation $c_{v_{0}} \leftarrow Enc (pk, 1 - β; r_{v_{0}})$ is equivalent to $c_{v_{0}} \leftarrow c [1]$ , because if $β = 0$ , then $c [1]$ contains plaintext 1, otherwise ( $β = 1$ ), $c [1]$ contains plaintext 0. Similarly, if $v_{1} \neq nc$ , then computation $c_{v_{1}} \leftarrow Enc (pk, β; r_{v_{1}})$ is equivalent to $c_{v_{1}} \leftarrow c [1]$ . Moreover, proof $ProveCiph ((pk, c_{v_{0}}, {0, 1}), (1 - β, r_{v_{0}}), v_{0}, κ)$ , respectively $ProveCiph ((pk, c_{v_{1}}, {0, 1}), (β, r_{v_{1}}), v_{1}, κ)$ , can be simulated by $Sim ProveCiph ((pk, c_{v_{0}}, {0, 1}), v_{0}, κ)$ , respectively $Sim ProveCiph ((pk, c_{v_{1}}, {0, 1}), v_{1}, κ)$ . Furthermore,

can be simulated by

Hence, we conclude the proof of this claim. □
Claim 26.
Adversary $B$ ’s computation of $v$ is equivalent to computing $v$ as $(v, pf) \leftarrow Tally ({sk}^{'}, bb, nc, κ)$ , where ${sk}^{'} = (pk, sk)$ .
Proof of Claim 26.
Let ${b_{1}, \dots, b_{ℓ}}$ be the largest subset of $bb$ satisfying the conditions of algorithm $Tally$ . It is trivial to see that the claim holds when ${b_{1}, \dots, b_{ℓ}} = \emptyset$ , because $v$ is computed as a zero-filled vector of length $nc$ in both cases. We prove the claim also holds when ${b_{1}, \dots, b_{ℓ}} \neq \emptyset$ .

By simulation sound extractability, for all $1 ⩽ i ⩽ ℓ$ and $1 ⩽ j ⩽ nc - 1$ , there exists a message $m_{i, j} \in {0, 1}$ and coins $r_{i, j}$ and $r_{i, j + nc - 1}$ such that $b_{i} [j] = Enc (pk, m_{i, j}; r_{i, j})$ and $b_{i} [j + nc - 1] = ProveCiph ((pk, b_{i} [j], {0, 1}), (m_{i, j}, r_{i, j}), j, κ; r_{i, j + nc - 1})$ , with overwhelming probability. Suppose Q and W are computed by $B$ . We have for all $1 ⩽ i ⩽ ℓ$ and $1 ⩽ j ⩽ nc - 1$ that $Q [ℓ \cdot (j - 1) + i] = ((pk, b_{i} [j], {0, 1}), b_{i} [j + nc - 1])$ and $W [ℓ \cdot (j - 1) + i]$ is a witness for $(pk, b_{i} [j], {0, 1})$ , i.e., $(m_{i, j}, r_{i, j})$ , and $W [ℓ \cdot (j - 1) + i] [1] = m_{i, j}$ . Hence, adversary $B$ ’s computation of $v$ is equivalent to computing $v$ as: $\begin{matrix} v \leftarrow (Σ_{i = 1}^{ℓ} m_{i, 1}, \dots, Σ_{i = 1}^{ℓ} m_{i, nc - 1}, ℓ - Σ_{j = 1}^{nc - 1} v [j]) \end{matrix}$ Moreover, computing $v$ as $(v, pf) \leftarrow Tally ({sk}^{'}, bb, nc, κ)$ is equivalent to initialising $v$ as a zero-filled vector of length $nc$ and computing

Since Π is a homomorphic encryption scheme, we have for all $1 ⩽ j ⩽ nc - 1$ that $b_{1} [j] \otimes \dots \otimes b_{ℓ} [j]$ is a ciphertext with overwhelming probability. And although ciphertext $b_{1} [j] \otimes \dots \otimes b_{ℓ} [j]$ may not have been computed using coins chosen uniformly at random, we nevertheless have $Dec (sk, b_{1} [j] \otimes \dots \otimes b_{ℓ} [j]) = m_{1, j} ⊙ \dots ⊙ m_{ℓ, j}$ with overwhelming probability, because Π is perfectly correct. It follows that $v = (m_{1, 1} ⊙ \dots ⊙ m_{ℓ, 1}, \dots, m_{1, nc - 1} ⊙ \dots ⊙ m_{ℓ, nc - 1}, ℓ - \sum_{j = 1}^{nc - 1} v [j])$ , with overwhelming probability. Let $mb$ be the largest integer such that ${0, \dots, mb} \subseteq m$ . Since $A$ is a winning adversary, we have $ℓ ⩽ mb$ . Moreover, since $m_{1, j}, \dots, m_{ℓ, j} \in {0, 1}$ for all $1 ⩽ j ⩽ nc - 1$ and ⊙ is the addition operator in group $(m, ⊙)$ , we have $m_{1, j} ⊙ \dots ⊙ m_{ℓ, j} = \sum_{i = 1}^{ℓ} m_{i, j}$ , which suffices to conclude the proof of this claim. □

For Helios’16, encryption scheme Π is additively homomorphic El Gamal [49, §2]. Moreover, $(ProveKey, VerKey)$ , respectively $(ProveCiph, VerCiph)$ and $(ProveDec, VerDec)$ , is the non-interactive proof system derived by application of the Fiat-Shamir transformation [59] to a random oracle $H$ and the sigma protocol for proving knowledge of discrete logarithms by Chaum et al. [35, Protocol 2], respectively the sigma protocol for proving knowledge of disjunctive equality between discrete logarithms by Cramer et al. [48, Figure 1] and the sigma protocol for proving knowledge of equality between discrete logarithms by Chaum & Pedersen [36, §3.2].

Bernhard, Pereira & Warinschi [19, §4] remark that the sigma protocols underlying non-interactive proof systems $(ProveKey, VerKey)$ and $(ProveCiph, VerCiph)$ both satisfy special soundness and special honest verifier zero-knowledge, hence, Theorem 15 is applicable. Bernhard, Pereira & Warinschi also remark that the sigma protocol underlying $(ProveDec, VerDec)$ satisfies special soundness and “almost special honest verifier zero-knowledge” and argue that “we could fix this[, but] it is easy to see that ... all relevant theorems [including Theorem 15] still hold.” We adopt the same position and assume that Theorem 15 is applicable. Proof of Theorem 6.
Helios’16 has zero-knowledge tallying proofs (Lemma 23), subject to the applicability of Theorem 15 to the sigma protocol underlying $(ProveDec, VerDec)$ . Moreover, since Helios’16 satisfies $UV$ [128], we have Helios’16 satisfies $Additivity (Γ, A, κ)$ (Lemma 27). Furthermore, since El Gamal satisfies $IND - CPA$ [78,135] and is perfectly correct, and since non-interactive proof systems $(ProveKey, VerKey)$ and $(ProveCiph, VerCiph)$ satisfy special soundness and special honest verifier zero-knowledge, we have Helios’16 satisfies $IND - CVA$ (Proposition 24). Hence, Helios’16 satisfies $Ballot - Secrecy$ too (Theorem 4). □

E. Universal verifiability implies tally soundness

We recall the definition of universal verifiability by Smyth, Frink & Clarkson [128] and show that verifiable election schemes satisfy $Tally - Soundness$ (Lemma 27). This is useful to simplify applications of Theorems 4, 13, & 29. Indeed, our ballot-secrecy proofs for Helios and Helios Mixnet make use of this result.

We extend our syntax for election schemes (Definition 1) to include a probabilistic polynomial-time algorithm $Verify$ :

$Verify$ , denoted $s \leftarrow Verify (pk, bb, nc, v, pf, κ)$ , is run to audit an election. It takes as input a public key $pk$ , a bulletin board $bb$ , some number of candidates $nc$ , an election outcome $v$ , a tallying proof $pf$ , and a security parameter κ. It outputs a bit s, where 1 signifies success and 0 failure.

We previously omitted algorithm

Verify

, because we did not focus on verifiability in the main body.

For universal verifiability, anyone must be able to check whether the election outcome represents the votes used to construct ballots on the bulletin board. The formal definition of universal verifiability by Smyth, Frink & Clarkson requires algorithm $Verify$ to accept if and only if the election outcome is correct. The if requirement is captured by completeness (Definition 28), which stipulates that election outcomes produced by algorithm $Tally$ will actually be accepted by algorithm $Verify$ . And the only if requirement is captured by soundness (Definition 30), which challenges an adversary to concoct a scenario in which algorithm $Verify$ accepts, but the election outcome is not correct.

Definition 28 (Completeness [128]).

An election scheme $(Setup, Vote, Tally, Verify)$ satisfies completeness, if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Pr [(pk, sk, mb, mc) \leftarrow Setup (κ); (bb, nc) \leftarrow A (pk, κ); (v, pf) \leftarrow Tally (sk, bb, nc, κ) : | bb | ⩽ mb \land nc ⩽ mc \Rightarrow Verify (pk, bb, nc, v, pf, κ) = 1] > 1 - negl (κ)$ .

Definition 29 (Injectivity [116,128]).

An election scheme $(Setup, Vote, Tally, Verify)$ satisfies injectivity, if for all probabilistic polynomial-time adversaries $A$ , security parameters κ and computations $(pk, nc, v, v^{'}) \leftarrow A (κ); b \leftarrow Vote (pk, v, nc, κ); b^{'} \leftarrow Vote (pk, v^{'}, nc, κ)$ such that $v \neq v^{'} \land b \neq ⊥ \land b^{'} \neq ⊥$ , we have $b \neq b^{'}$ .

Definition 30 (Soundness [128]).

An election scheme $Γ = (Setup, Vote, Tally, Verify)$ satisfies soundness, if Γ satisfies injectivity and for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Pr [(pk, nc, bb, v, pf) \leftarrow A (κ) : v \neq correct - outcome (pk, nc, bb, κ) \land Verify (pk, bb, nc, v, pf, κ) = 1] ⩽ negl (κ)$ .

Definition 31 ( $UV$ [116,128]).

An election scheme Γ satisfies universal verifiability $(UV)$ , if completeness, injectivity and soundness are satisfied.

Lemma 27.
If election scheme Γ satisfies completeness and soundness, then Γ satisfies $Tally - Soundness$ .
Proof.
Let $Γ = (Setup, Vote, Tally, Verify)$ . Suppose there exists a probabilistic polynomial-time adversary $A$ that wins $Tally - Soundness$ against Γ. We construct an adversary $B$ against $Exp - UV - Ext$ from $A$ . We define $B$ such that $B (κ) = (pk, sk, mb, mc) \leftarrow Setup (κ); (nc, bb) \leftarrow A (pk, κ); (v, pf) \leftarrow Tally (sk, bb, nc, κ); return (pk, nc, bb, v, pf)$ . Suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ , $(nc, bb)$ is an output of $A (pk, κ)$ , and $(v, pf)$ is an output of $Tally (sk, bb, nc, κ)$ . Since $A$ is a winning adversary, we have $v \neq correct - outcome (pk, nc, bb, κ) \land | bb | ⩽ mb \land nc ⩽ mc$ , with non-negligible probability. And, by completeness, we have $Verify (pk, bb, nc, v, pf, κ) = 1$ , with overwhelming probability. Thereby concluding our proof. □
The reverse implication of Lemma 27 does not hold: Observe that $Tally - Soundness$ only ensures algorithm $Tally$ tallies ballots correctly, whereas $UV$ additionally ensures that anyone can check whether ballots are tallied correctly.
F. Encryption-based voting systems

We have seen that election scheme $Enc 2 Vote (Π)$ satisfies $HK - Injectivity$ , if Π is perfectly correct (Lemma 9). But, $HK - Injectivity$ assumes public keys are computed using the key generation algorithm. Thus, perfect correctness is insufficient to ensure injectivity when public keys are controlled by an adversary. Nonetheless, this can be ensured using proofs of correct key generation. A sub-class of schemes generated by $Enc 2 Vote$ prove correct key generation. Indeed, we can consider schemes $Enc 2 Vote (Π)$ such that $Gen$ proves correct key generation and $Enc$ verifies such proofs, where $Π = (Gen, Enc, Dec)$ . Alternatively, we can couple $Enc 2 Vote$ with proofs of correct key generation:

Definition 32 ( ${Enc 2 Vote}^{+}$ [116]).

Suppose $Π = (Gen, Enc, Dec)$ is an asymmetric encryption scheme, Σ is a sigma protocol that proves correct key generation, and $H$ is a hash function. Let $FS (Σ, H) = (ProveKey, VerKey)$ . We define ${Enc 2 Vote}^{+} (Π, Σ, H) = (Setup, Vote, Tally)$ such that:

$Setup (κ)$ selects coins s uniformly at random, computes $(pk, sk, m) \leftarrow Gen (κ; s); ρ \leftarrow ProveKey ((κ, pk, m), (sk, s), κ); {pk}^{'} \leftarrow (pk, m, ρ); {sk}^{'} \leftarrow (pk, sk)$ , derives $mc$ as the largest integer such that ${0, \dots, mc} \subseteq {0} \cup m$ and for all $m_{0}, m_{1} \in {1, \dots, mc}$ we have $| m_{0} | = | m_{1} |$ , and outputs $({pk}^{'}, {sk}^{'}, p (κ), mc)$ , where p is a polynomial function.

$Vote ({pk}^{'}, v, nc, κ)$ parses ${pk}^{'}$ as vector $(pk, m, ρ)$ , outputting ⊥ if parsing fails or $VerKey ((κ, pk, m), ρ, κ) \neq 1 \lor v \notin {1, \dots, nc} \lor {1, \dots, nc} ⊈ m$ , computes $b \leftarrow Enc (pk, v)$ , and outputs b.

Lemma 28.
Given an asymmetric encryption scheme Π satisfying $IND - CPA$ , a sigma protocol Σ that proves correct key generation, and a hash function $H$ , we have ${Enc 2 Vote}^{+} (Π, Σ, H)$ is an election scheme.
A proof of Lemma 28 follows from [116].39
³⁹
Smyth considers instantiating ${Enc 2 Vote}^{+}$ with a broad class of asymmetric encryption schemes that produce distinct ciphertexts with overwhelming probability [116], whereas we consider a strictly narrower class of schemes satisfying $IND - CPA$ . This avoids having to recall Smyth’s notion of distinct ciphertexts.

Although the set of election schemes produced by ${Enc 2 Vote}^{+}$ is not a subset of the schemes produced by $Enc 2 Vote$ , there is nonetheless a straightforward mapping from the former to the latter. Thus, the results in Section 5 also hold for ${Enc 2 Vote}^{+}$ : Theorem 29.
Let ${Enc 2 Vote}^{+} (Π, Σ, H) = (Setup, Vote, Tally)$ , where Π is an asymmetric encryption scheme, Σ is a sigma protocol that proves correct key generation, and $H$ is a random oracle. Moreover, let $Γ = (Setup, Vote, {Tally}^{'})$ for some algorithm ${Tally}^{'}$ such that Γ is an election scheme with zero-knowledge tallying proofs. Suppose Π is perfectly correct and satisfies $IND - PA 0$ and well-definedness. Moreover, suppose Σ is perfectly complete and $FS (Σ, H)$ satisfies zero-knowledge. Further suppose Γ satisfies $Tally - Soundness$ . We have Γ satisfies $Ballot - Secrecy$ .
Proof.
Let $FS (Σ, H) = (ProveKey, VerKey)$ and $Π = (Gen, Enc, Dec)$ . Moreover, let asymmetric encryption scheme $Π^{'} = ({Gen}^{'}, {Enc}^{'}, Dec)$ such that

${Gen}^{'} (κ)$ selects coins s uniformly at random, computes $(pk, sk, m) \leftarrow Gen (κ; s); ρ \leftarrow ProveKey ((κ, pk, m), (sk, s), κ); {pk}^{'} \leftarrow (pk, m, ρ)$ , and outputs $({pk}^{'}, sk, m)$ .

${Enc}^{'} (pk, v)$ parses ${pk}^{'}$ as a vector $(pk, m, ρ)$ , outputting ⊥ if parsing fails or $VerKey ((κ, pk, m), ρ, κ) \neq 1$ , computes ciphertext $c \leftarrow Enc (pk, v)$ , and outputs c.
Since Π is perfectly correct and Σ is perfectly complete, we have $Π^{'}$ is perfectly correct. Moreover, since Π satisfies well-definedness, we have $Π^{'}$ does too. Furthermore, since $FS (Σ, H)$ satisfies zero-knowledge and Π satisfies $IND - PA 0$ , we have $Π^{'}$ satisfies $IND - PA 0$ . It follows that $Enc 2 Vote (Π^{'})$ satisfies $Tally - Soundness$ and $IND - CVA$ (Corollary 10 & Lemma 12).

We have $Enc 2 Vote (Π^{'}) = ({Setup}^{'}, {Vote}^{'}, Tally)$ such that ${Setup}^{'}$ is $Setup$ except $Setup$ outputs public key ${pk}^{'}$ as a vector $(pk, m, ρ)$ , whereas ${Setup}^{'}$ outputs public key $(pk, m)$ . Moreover, ${Vote}^{'}$ is $Vote$ except $Vote$ inputs public key $(pk, m)$ whereas ${Vote}^{'}$ inputs public key $(pk, m, ρ)$ . (This blight motivated the inclusion of this appendix.) Hence, it is straightforward to see that ${Enc 2 Vote}^{+} (Π, Σ, H)$ satisfies $Tally - Soundness$ and $IND - CVA$ , because $Enc 2 Vote (Π^{'})$ does. Thus, Γ satisfies $IND - CVA$ (Proposition 8) and $Ballot - Secrecy$ (Theorem 4 & Lemma 7). □

G. Helios Mixnet

We recall a generic construction for election schemes similar to Helios Mixnet (Definition 34). The construction is parameterised on the choice of homomorphic encryption scheme and sigma protocols for the relations introduced in Definition 22 and the following definition.

Definition 33 (from [128]).

Let $(Gen, Enc, Dec)$ be a homomorphic asymmetric encryption scheme and Σ be a sigma protocol for a binary relation R. Suppose that $(pk, sk) = Gen (κ; s)$ , for some security parameter κ and coins s, and $m$ is the encryption scheme’s plaintext space.

Σ proves plaintext knowledge if $((pk, c), (m, r)) \in R \Leftrightarrow c = Enc (pk, m; r) \land m \in m .$

Σ proves mixing if $((pk, c, c^{'}), (r, χ)) \in R \Leftrightarrow ⋀_{1 ⩽ i ⩽ | c |} c^{'} [i] = c [χ (i)] \otimes Enc (pk, e; r [i]) \land | c | = | c^{'} | = | r |$ , where c and $c^{'}$ are both vectors of ciphertexts encrypted under $pk$ , r is a vector of coins, χ is a permutation on ${1, \dots, | c |}$ , and $e$ is an identity element of the encryption scheme’s message space with respect to ⊙.

Definition 34 ( $HeliosM$ [108,124]).

Suppose $Π_{0} = (Gen, Enc, Dec)$ is a homomorphic asymmetric encryption algorithm, $Σ_{1}$ is a sigma protocol that proves correct key construction, $Σ_{2}$ is a sigma protocol that proves plaintext knowledge, and $H$ is a hash function. Let $FS (Σ_{1}, H) = (ProveKey, VerKey)$ and $FS (Σ_{2}, H) = (ProveCiph, VerCiph)$ . Moreover, let $π (Π, Σ_{2}, H) = (Gen, {Enc}^{'}, {Dec}^{'})$ be an asymmetric encryption scheme such that:

${Enc}^{'} (pk, v)$ selects coins r uniformly at random, computes $c \leftarrow Enc (pk, v; r); σ \leftarrow ProveCiph ((pk, c), (v, r), κ)$ , and outputs $(c, σ)$ .

${Dec}^{'} (sk, c^{'})$ parses $c^{'}$ as $(c, σ)$ , outputting ⊥ if parsing fails or $VerCiph ((pk, c), σ, κ) \neq 1$ , computes $v \leftarrow Dec (sk, c)$ , and outputs v.

Let

{Enc 2 Vote}^{+} (π (Π, Σ_{2}, H), Σ_{1}, H) = (Setup, Vote, {Tally}^{'})

. Suppose

Σ_{3}

is a sigma protocol that proves correct decryption and

Σ_{4}

is a sigma protocol that proves mixing. Let

FS (Σ_{3}, H) = (ProveDec, VerDec)

and

FS (Σ_{4}, H) = (ProveMix, VerMix)

. We define

HeliosM (Π, Σ_{1}, Σ_{2}, Σ_{3}, Σ_{4}, H) = (Setup, Vote, Tally)

, where algorithm

Tally

is defined below. 40

⁴⁰
We omit algorithm $Verify$ for brevity.

$Tally ({sk}^{'}, nc, bb, κ)$ initialises $v$ as a zero-filled vector of length $nc$ ; parses ${sk}^{'}$ as a pair $(pk, sk)$ , outputting $(v, ⊥)$ if parsing fails; and proceeds as follows:

Remove invalid ballots. Let ${b_{1}, \dots, b_{ℓ}}$ be the largest subset of $bb$ such that for all $1 ⩽ i ⩽ ℓ$ we have $b_{i}$ is a pair and $VerCiph ((pk, b_{i} [1]), b_{i} [2], κ) = 1$ . If ${b_{1}, \dots, b_{ℓ}} = \emptyset$ , then output $(v, ⊥)$ .

Mix. Select a permutation χ on ${1, \dots, ℓ}$ uniformly at random, initialise $bb$ and r as a vector of length ℓ, fill r with coins chosen uniformly at random, and compute

where $e$ is an identity element of Π’s message space with respect to ⊙.

Decrypt. Initialise W and ${pf}_{2}$ as vectors of length ℓ and compute:

Output

(v, (bb, {pf}_{1}, W, {pf}_{2}))

Definition 35 (HeliosM’17).

HeliosM’17 is the set of election schemes that includes every $HeliosM (Π_{0}, Σ_{1}, Σ_{2}, Σ_{3}, Σ_{4}, H)$ such that $Π_{0}$ , $Σ_{1}$ , $Σ_{2}$ , $Σ_{3}$ , $Σ_{4}$ and $H$ satisfy the preconditions of Definition 34 , moreover, $Π_{0}$ is perfectly correct and $Σ_{1}$ and $Σ_{2}$ are perfectly complete, furthermore, $Π_{0}$ satisfies $IND - CPA$ , $Σ_{1}$ , $Σ_{2}$ , $Σ_{3}$ and $Σ_{4}$ satisfy special soundness and special honest verifier zero-knowledge, $H$ is a random oracle, and $HeliosM (Π_{0}, Σ_{1}, Σ_{2}, Σ_{3}, Σ_{4}, H)$ satisfies $UV$ .

Smyth has shown that there exists an election scheme in HeliosM’17 that satisfies

UV

[124]. Hence, set HeliosM’17 is not empty.

G.1. Proof of Theorem 14

Let election scheme $Γ = HeliosM (Π_{0}, Σ_{1}, Σ_{2}, Σ_{3}, Σ_{4}, H) = (Setup, Vote, Tally)$ and asymmetric encryption scheme $Π = π (Π_{0}, Σ_{2}, H)$ . It follows that election scheme ${Enc 2 Vote}^{+} (Π, Σ_{1}, H) = (Setup, Vote, {Tally}^{'})$ . Moreover, since $Σ_{1}$ satisfies special soundness and special honest verifier zero-knowledge, we have $FS (Σ_{1}, H)$ satisfies zero-knowledge (Theorem 15). We use Theorem 29 to prove that $Γ \in Helios M^{'} 17$ satisfies $Ballot - Secrecy$ .

Since $Π_{0}$ is perfectly correct and $Σ_{2}$ is perfectly complete, we have Π is a perfectly correct. Moreover, since $Σ_{2}$ satisfies special soundness and special honest verifier zero-knowledge, we have $FS (Σ_{2}, H)$ satisfies simulation sound extractability (Theorem 15), hence, Π satisfies $CNM - CPA$ [19, Theorem 2] and, equivalently, $IND - PA 0$ [10].

To prove $Π = (Gen, Enc, Dec)$ satisfies well-definedness, suppose $A$ is a probabilistic polynomial-time adversary, κ is a security parameter, $(pk, sk, m)$ is an output of $Gen (κ)$ , and c is an output of $A (pk, m, κ)$ such that $Dec (sk, c) \neq ⊥$ . By definition of $Dec$ , we have c is a pair (hence, $c \neq ⊥$ ) such that $FS (Σ_{2}, H)$ can verify $c [2]$ with respect to $pk$ and $c [1]$ . Since $FS (Σ_{2}, H)$ satisfies simulation sound extractability, we have $c [2]$ is a proof computed using $FS (Σ_{2}, H)$ and there exists plaintext $m \in m$ and coins r such that $c [1] = Enc (pk, m; r)$ , with overwhelming probability. Thus, Π satisfies well-definedness.

Since $Σ_{3}$ and $Σ_{4}$ satisfy special soundness and special honest verifier zero-knowledge, we have $FS (Σ_{3}, H)$ and $FS (Σ_{4}, H)$ satisfy zero-knowledge (Theorem 15), therefore, Γ has zero-knowledge tallying proofs by reasoning similar to that given in the proof sketch of Lemma 23. Moreover, since Γ satisfies universal verifiability, we have Γ satisfies $Tally - Soundness$ (Lemma 27).

We conclude by Theorem 29. □

H. $Ballot - Secrecy$ is strictly stronger than $IND - SEC$

Smyth & Bernhard propose definitions of ballot secrecy that consider an adversary that cannot control the bulletin board nor the communication channel [125,126]. As discussed in Section 8, their original definition [125] is too strong [16, §3.5] and they propose a revision [126]. We recall their syntax (Definition 36) and revised definition (Definition 37), define a transformation from their syntax to ours (Definition 38), and prove $Ballot - Secrecy$ is strictly stronger than their definition (Theorem 31).

Definition 36 (Election scheme with a trusted bulletin board).

An election scheme with a trusted bulletin board is a tuple of efficient algorithms $(Setup, Vote, BB, Tally)$ such that:

$Setup$ , denoted $(pk, sk, m, bb) \leftarrow Setup (κ)$ , takes a security parameter κ as input and outputs a key pair $pk, sk$ , a vote space $m$ , and a bulletin board $bb$ , where $m$ and $bb$ are both sets.

$Vote$ , denoted $b \leftarrow Vote (pk, v)$ , takes a public key $pk$ and vote v as input and outputs a ballot b. Vote v should be selected from the vote space $m$ .

$BB$ , denoted ${bb}^{'} \leftarrow BB (bb, b)$ , takes a bulletin board $bb$ and ballot b as input and outputs an updated bulletin board ${bb}^{'}$ .

$Tally$ , denoted $(o, pf) \leftarrow Tally (sk, bb)$ , takes a private key $sk$ and bulletin board $bb$ as input and outputs an election outcome $o$ and a tallying proof $pf$ , where $o$ is a multiset of votes.

Election schemes with a trusted bulletin board must satisfy correctness, that is, for all security parameters κ, votes v and multisets

bb

, we have:

Pr [(pk, sk, m, {bb}_{0}) \leftarrow Setup (κ); b \leftarrow Vote (pk, v); {bb}^{'} \leftarrow BB (bb, b); (o, pf) \leftarrow Tally (sk, bb); (o^{'}, {pf}^{'}) \leftarrow Tally (sk, {bb}^{'}) : {bb}^{'} = bb \cup {b} \land (o \neq \emptyset \Rightarrow o^{'} = o \cup {v} \land | v | = | bb |) \land (o = \emptyset \Rightarrow o^{'} = \emptyset)] > 1 - negl (κ)

Definition 37.
Let $Γ = (Setup, Vote, BB, Tally)$ be an election scheme with a trusted bulletin board, $A$ be an adversary, κ be a security parameter, and $IND - SEC$ be the following game.

In the above game, $L_{0}$ and $L_{1}$ are multisets and oracle $O$ is defined as follows:

$O (v_{0}, v_{1})$ computes $L_{0} \leftarrow L_{0} \cup {v_{0}}; L_{1} \leftarrow L_{1} \cup {v_{1}}; b_{0} \leftarrow Vote (pk, v_{0}); {bb}_{0} \leftarrow BB ({bb}_{0}, b_{0}); b_{1} \leftarrow Vote (pk, v_{1}); {bb}_{1} \leftarrow BB ({bb}_{1}, b_{1})$ , where $v_{0}, v_{1} \in m$ .

$O (b)$ computes ${bb}^{'} \leftarrow {bb}_{β}; {bb}_{β} \leftarrow BB ({bb}_{β}, b);$ if ${bb}_{β} \neq {bb}^{'}$ then ${bb}_{1 - β} \leftarrow BB ({bb}_{1 - β}, b)$ .

$O ()$ outputs ${bb}_{β}$ .
We say Γ satisfies $IND - SEC$ , if for all probabilistic polynomial-time adversaries $A$ , there exists a negligible function $negl$ , such that for all security parameters κ, we have $Succ (IND - SEC (Γ, A, κ)) ⩽ \frac{1}{2} + negl (κ)$ .
Observe that game $IND - SEC$ uses bulletin boards ${bb}_{β}$ and ${bb}_{0}$ , hence, ${bb}_{1}$ is unused when $β = 0$ . It follows that game $IND - SEC$ is equivalent to a variant that redefines the following oracle calls:

$O (v_{0}, v_{1})$ computes $L_{0} \leftarrow L_{0} \cup {v_{0}}; L_{1} \leftarrow L_{1} \cup {v_{1}}; b_{β} \leftarrow Vote (pk, v_{β}); {bb}_{β} \leftarrow BB ({bb}_{β}, b_{β});$ if $β = 1$ then $b_{0} \leftarrow Vote (pk, v_{0}); {bb}_{0} \leftarrow BB ({bb}_{0}, b_{0})$ , where $v_{0}, v_{1} \in m$ .

$O (b)$ computes ${bb}^{'} \leftarrow {bb}_{β}; {bb}_{β} \leftarrow BB ({bb}_{β}, b);$ if ${bb}_{β} \neq {bb}^{'} \land β = 1$ then ${bb}_{0} \leftarrow BB ({bb}_{0}, b)$ .
Let that variant be $IND - {SEC}^{}$ . Lemma 30.
An election scheme with a trusted bulletin board* Γ satisfies $IND - SEC$ iff Γ satisfies $IND - {SEC}^{}$ .
Lemma 30 follows from our informal reasoning and we omit a formal proof. Definition 38.
Given an election scheme with a trusted bulletin board* $Γ = (Setup, Vote, BB, Tally)$ such that for all security parameters κ and computations $(pk, sk, m, bb) \leftarrow Setup (κ)$ we have $m = {1, \dots, mc}$ for some integer $mc$ , we define $γ (Γ) = ({Setup}^{'}, {Vote}^{'}, {Tally}^{'})$ such that

${Setup}^{'} (κ)$ computes $(pk, sk, m, bb) \leftarrow Setup (κ); mc \leftarrow | m |; {pk}^{'} \leftarrow (pk, mc)$ and outputs $({pk}^{'}, sk, mc, p (κ))$ , where p is a polynomial function.

${Vote}^{'} ({pk}^{'}, v, nc, κ)$ parses ${pk}^{'}$ as $(pk, mc)$ , aborting if parsing fails; computes $b \leftarrow Vote (pk, v)$ ; and outputs b.

${Tally}^{'} (sk, bb, nc, κ)$ computes $(o, pf) \leftarrow Tally (sk, bb)$ , outputting an empty vector if $o$ is empty; assigns the largest integer in $o$ to $nc$ ; initialises $v$ as a zero-filled vector of length $nc$ ; computes while $v \in o$ do $v [v] \leftarrow v [v] + 1; o \leftarrow o ∖ {v}$ ; and outputs $(v, pf)$ .

Theorem 31.
Let Γ be an election scheme with a trusted bulletin board. If $γ (Γ)$ is an election scheme satisfying $Ballot - Secrecy$ , then Γ satisfies $IND - SEC$ .
Proof sketch.
Let $Γ = (Setup, Vote, BB, Tally)$ and $γ (Γ) = ({Setup}^{'}, {Vote}^{'}, {Tally}^{'})$ . Suppose $γ (Γ)$ is an election scheme satisfying $Ballot - Secrecy$ . Moreover, suppose Γ does not satisfy $IND - SEC$ . Hence, there exists a probabilistic polynomial-time adversary $A$ , such that for negligible functions $negl$ , there exists a security parameter κ and $Succ (IND - SEC (Γ, A, κ)) > \frac{1}{2} + negl (κ)$ . We construct the following adversary $B$ against $Ballot - Secrecy$ from $A$ , where $O_{A}$ denotes $A$ ’s oracle and $O_{B}$ denotes $B$ ’s oracle:

$B ({pk}^{'}, κ)$ parses ${pk}^{'}$ as $(pk, mc)$ , aborting if parsing fails, and outputs $mc$ .

$B ()$ initialises $bb$ and ${bb}_{0}$ as empty sets and $L_{0}$ and $L_{1}$ as empty multisets; computes $m \leftarrow {1, \dots, mc}; x \leftarrow A (pk, m)$ , handling $A$ ’s oracle calls as follows, namely,

$O_{A} (v_{0}, v_{1})$ computes $L_{0} \leftarrow L_{0} \cup {v_{0}}; L_{1} \leftarrow L_{1} \cup {v_{1}}; b \leftarrow O_{B} (v_{0}, v_{1}); bb \leftarrow BB (bb, b); b_{0} \leftarrow Vote (pk, v_{0}); {bb}_{0} \leftarrow BB (bb, b_{0})$ ,

$O_{A} (b)$ computes ${bb}^{'} \leftarrow bb; bb \leftarrow BB (bb, b);$ if $bb \neq {bb}^{'}$ then $b b_{0} \leftarrow BB ({bb}_{0}, b)$ , and

$O_{A} ()$ outputs $bb$ ,
and outputs $bb$ if $L_{0} = L_{1}$ and ${bb}_{0}$ otherwise.

$B (v, pf)$ computes $o \leftarrow {v^{v [v]} ∣ 1 ⩽ v ⩽ mc};$ if $L_{0} \neq L_{1}$ then $pf \leftarrow ⊥$ ; $g \leftarrow A (o, pf)$ and outputs g.
We prove that $B$ wins $Ballot - Secrecy$ .

Suppose $({pk}^{'}, sk, mb, mc)$ is an output of ${Setup}^{'} (κ)$ . By definition of algorithm ${Setup}^{'}$ , we have ${pk}^{'}$ is a pair $(pk, mc)$ , where $(pk, sk, m, bb)$ is an output of $Setup (κ)$ and $mc = | m |$ . Hence, $B ({pk}^{'}, κ)$ outputs $mc$ . Let β be a bit and suppose $bb$ is an output of $B ()$ . It is trivial to see that $B ()$ simulates $A$ ’s challenger to $A$ . Moreover, by Lemma 30 it is straightforward to see that $B$ simulates $A$ ’s oracle too. Indeed, adversary $B$ maintains bulletin board $bb$ such that $O_{A} (v_{0}, v_{1})$ constructs a ballot b for $v_{β}$ using $B$ ’s oracle, hence, the ballot is constructed by algorithm $Vote$ by way of algorithm ${Vote}^{'}$ , and adds that ballot to the bulletin board using algorithm $BB$ . Suppose $(v, pf)$ is an output of $Tally (sk, bb, nc, κ)$ and g is an output of $B (v, pf)$ . It is straightforward to see that $B (v, pf)$ simulates $A$ ’s challenger to $A$ , thus, $g = β$ , with at least the probability that $A$ wins $IND - SEC$ , concluding our proof. □

I. Stronger privacy notions

Ballot secrecy does not ensure free-choice when an adversary is able to communicate with voters nor when voters deviate from the prescribed voting procedure to follow instructions provided by an adversary. Stronger notions of free-choice, such as receipt-freeness [32,51,60,83,96] and coercion resistance [61,70,76,88,139], are needed in the presence of such adversaries. This appendix introduces these notions, proves that our syntax cannot be used to construct (interesting) schemes satisfying them, and discusses variants of our syntax that can.

Receipt-freeness formalises a notion of free-choice in the presence of an adversary that can communicate with voters.

Receipt-freeness. A voter cannot collaborate with a conspirator to produce information which can be used to prove how they voted.

Free-choice may be compromised in receipt-free voting systems if voters deviate from the prescribed voting procedure.41

⁴¹
For receipt-freeness to be an effective notion of free-choice it might be necessary for the voting system to prevent voters deviating from the prescribed voting procedure. This might be achieved by physically securing devices that can be used to cast ballots.

Coercion-resistance formalises a stronger notion of free-choice assuming that not only can voters deviate, but the adversary can instruct voters how to deviate.

Coercion resistance. A voter can deviate from a coercer’s instructions, to cast their vote, without detection.

The distinction between receipt-freeness and coercion resistance is subtle: “receipt-freeness deals with a coercer who is only concerned with deducing information about how someone voted from receipts and public information, but who does not give detailed instructions on how to cast the vote. Coercion resistance, on the other hand, includes dealing with a coercer who gives details not just on which candidate to vote for but also on how to cast the vote” [72, §1.1]. Both receipt-freeness and coercion resistance retain the assumption that voters’ ballots are tallied in the prescribed manner, and receipt-freeness additionally assumes voters’ ballots are constructed in the prescribed manner. Moreover, both require side conditions to exclude inevitable revelations (§3).

I.1. Receipt-freeness

We cast the definition of receipt-freeness by Delaune, Kremer & Ryan [51,52] from the symbolic model to the computational model of cryptography, in the context of our election scheme syntax. Moreover, we extend their work to consider arbitrarily many voters, rather than just the two considered by the original definition. The resulting formalisation (Definition 39) is a pair of games.

The first game ( $Receipt - Freeness - A$ ) is an extension of $Ballot - Secrecy$ that tasks the adversary to: select a list of their preferred votes and a list of voter preferred votes (although it is somewhat unnatural for the adversary to specify voter preferred votes, this is useful to quantify over all possible voter preferences); construct a bulletin board from either (i) ballots for their preferred votes and coins used to construct those ballots, or (ii) ballots for voter preferred votes and simulated coins; and non-trivially determine whether their preferred or voter preferred votes were used, from the resulting election outcome and tallying proof. The game proceeds as per game $Ballot - Secrecy$ , except a new oracle is used (Line 5). That oracle constructs ballots for either the adversary’s preferred votes (using algorithm $Vote$ ) or for voter preferred votes (using algorithm $V$ ). Those ballots are output along with either the coins used by algorithm $Vote$ or coins simulated by algorithm $V$ . Intuitively, algorithm $V$ provides a strategy for voters to cast voter preferred votes whilst convincing the adversary that its preferred votes were cast, hence, information cannot be produced to prove how voters voted.

The second game ( $Receipt - Freeness - B$ ) tasks the adversary to compute inputs (including a public key) to algorithms $Vote$ and $V$ that cause the algorithms to output ballots that can be distinguished, thereby over-approximating the requirement that algorithm $V$ must produce a ballot for voter preferred votes. (Indeed, the adversary can use algorithm $Tally$ to determine whether a ballot is for the expected vote.) The game proceeds as follows: The adversary computes inputs to algorithms $Vote$ and $V$ (Line 1); the challenger flips a coin (Line 2) and computes a ballot using one of the algorithms (Lines 3–6), where the choice between algorithms is determined by the coin flip; and the adversary is tasked with determining the result of the coin flip from the ballot (Lines 7 & 8).

Definition 39 ( $Receipt - Freeness$ ).

Let $Γ = (Setup, Vote, Tally)$ be an election scheme, $V$ be an algorithm, $A$ be an adversary, κ be a security parameter, and $Receipt - Freeness - A$ be the following game.

Oracle $O$ is defined as follows:

$O (v_{0}, v_{1})$ chooses coins r uniformly at random from the coin space of algorithm $Vote$ , computes if $β = 0$ then $b \leftarrow Vote (pk, v_{0}, nc, κ; r)$ else $(b, r) \leftarrow V (pk, v 1, v 0, nc, κ)$ and $L \leftarrow L \cup {(b, v_{0}, v_{1})}$ , and outputs $(b, r)$ , where $v_{0}, v_{1} \in {1, ..., nc}$ .

Moreover, let

B

be an adversary and

Receipt - Freeness - B

be the following game.

We say Γ satisfies $Receipt - Freeness$ , if there exists a probabilistic polynomial-time algorithm $V$ such that for all probabilistic polynomial-time adversaries $A$ and $B$ , there exists a negligible function $negl$ and for all security parameters κ, we have $Succ (Receipt - Freeness - A (Γ, V, A, κ)) ⩽ \frac{1}{2} + negl (κ)$ and $Succ (Receipt - Freeness - B (Γ, V, B, κ)) ⩽ \frac{1}{2} + negl (κ)$ .

An election scheme satisfies receipt-freeness when ballot secrecy is preserved even when coins used to construct ballots are revealed.

Similarly to ballot secrecy (§3), receipt-freeness tolerates inevitable revelations, e.g., unanimous election outcomes. It follows that an election scheme for one candidate satisfies our definition of receipt-freeness, because that scheme will always produce unanimous election outcomes.

Proposition 32.
Given an election scheme Γ for one candidate (i.e., for all security parameters the maximum number of candidates is one), we have Γ satisfies $Ballot - Secrecy$ and $Receipt - Freeness$ .
Proof.
Let $Γ = (Setup, Vote, Tally)$ . Suppose $(pk, sk, mb, mc)$ is an output of $Setup (κ)$ and $nc$ is an output of $A (pk, κ)$ such that $1 ⩽ nc ⩽ mc$ , for some security parameter κ and some adversary $A$ against game $Ballot - Secrecy$ or game $Receipt - Freeness - A$ . Since $mc = 1$ by hypothesis, we have $nc = 1$ too. For game $Receipt - Freeness - A$ , let algorithm $V$ be such that $V (pk, v_{0}, v_{1}, nc, κ)$ chooses coins r uniformly at random from the coin space of algorithm $Vote$ , computes $b \leftarrow Vote (pk, v_{0}, nc, κ)$ , and outputs $(b, r)$ . Suppose β is a bit chosen uniformly at random and $bb$ is an output of $A ()$ . By inspection of the oracle definition in each game, we have for every oracle call $O (v_{0}, v_{1})$ that $v_{0} = v_{1}$ , moreover, the ballot output by the oracle is independent of bit β. It follows that the adversary looses each game, hence Γ satisfies $Ballot - Secrecy$ . To show that $Receipt - Freeness$ is satisfied too, we must consider game $Receipt - Freeness - B$ .

Suppose $(pk, v_{0}, v_{1}, nc)$ is an output of $B (κ)$ such that $1 ⩽ v_{0}, v_{1} ⩽ nc$ , for some adversary $B$ against game $Receipt - Freeness - B$ . Let β be a bit chosen uniformly at random. If $β = 0$ , then suppose b is an output of $Vote (pk, v_{0}, nc, κ)$ , otherwise ( $β = 1$ ), suppose $(b, r)$ is an output of $V (pk, v_{0}, v_{1}, nc, κ)$ , hence, b is an output of $Vote (pk, v_{0}, nc, κ)$ by definition of $V$ . Thus, the ballot computed by the challenger is independent of bit β. It follows that the adversary looses game $Receipt - Freeness - B$ , hence, Γ satisfies $Receipt - Freeness$ , thereby concluding our proof. □
Beyond the uninteresting case (Proposition 32), we prove that $Receipt - Freeness$ cannot be satisfied by election schemes for more than one candidate (Proposition 33), assuming the election scheme is perfectly correct or satisfies tally soundness. Proposition 33.
Let Γ be an election scheme for more than one candidate (i.e., there exists a security parameter such that the maximum number of candidates is greater than one). Suppose Γ is perfectly correct or Γ satisfies $Tally - Soundness$ . We have Γ does not satisfy $Receipt - Freeness$ .
Proof.
Let $Γ = (Setup, Vote, Tally)$ . Suppose to the contrary that Γ satisfies $Receipt - Freeness$ , hence, there exists a probabilistic polynomial-time algorithm $V$ such that for all probabilistic polynomial-time adversaries $A$ and $B$ , there exists a negligible function $negl$ and for all security parameters κ, we have $Succ (Receipt - Freeness - A (Γ, V, A, κ)) + Succ (Receipt - Freeness - B (Γ, V, B, κ)) ⩽ \frac{1}{2} + negl (κ)$ . Further suppose κ is such that the maximum number of candidates output by algorithm $Setup (κ)$ is greater than one. Moreover, suppose $A$ is the following adversary.
$A (pk, κ)$ computes $nc \leftarrow 2$ and outputs $nc$ .

$A ()$ computes $v_{0} \leftarrow 1; v_{1} \leftarrow 2; (b, r) \leftarrow O (v_{0}, v_{1})$ and outputs ∅.

$A (v, pf)$ outputs 0 if $v = Vote (pk, v_{0}, nc, κ; r)$ and 1 otherwise.
Since Γ satisfies $Receipt - Freeness$ , it follows that $V (pk, v 1, v 0, nc, κ)$ outputs $(b, r)$ such that $b = Vote (pk, v_{0}, nc, κ; r)$ , with overwhelming probability. Suppose $B$ is the following adversary.
$B (κ)$ computes $(pk, sk, mb, mc) \leftarrow Setup (κ); v_{0} \leftarrow 1; v_{1} \leftarrow 2; nc \leftarrow 2$ and outputs $(pk, v_{0}, v_{1}, nc)$ .

$B (b)$ computes $(v, pf) \leftarrow Tally (sk, {b}, nc, κ)$ and outputs 0 if $v = (1, 0)$ and 1 otherwise.
We prove that $B$ wins $Receipt - Freeness - B (Γ, V, B, κ)$ .

Suppose $(pk, v_{0}, v_{1}, nc)$ is an output of $B (κ)$ and β is a bit chosen uniformly at random. If $β = 0$ , then further suppose b is an output of $Vote (pk, v_{0}, nc, κ)$ , and g is an output of $B (b)$ . Outputs $(v, pf)$ of $Tally (sk, {b}, nc, κ)$ are such that $v = (1, 0)$ by correctness, which ensures $g = β$ by definition of $B$ . Otherwise ( $β = 1$ ), suppose $(b, r)$ is an output of $V (pk, v_{0}, v_{1}, nc, κ)$ , hence, $b = Vote (pk, v_{1}, nc, κ; r)$ , and g is an output of $B (b)$ . Outputs $(v, pf)$ of $Tally (sk, {b}, nc, κ)$ are such that $v = (0, 1)$ by perfect correctness and $v = correct - outcome (pk, nc, {b}, κ) = (0, 1)$ by $Tally - Soundness$ , which ensures $g = β$ by definition of $B$ . (Correctness, rather than perfect correctness, is insufficient, because algorithm $V$ may not have chosen coins r uniformly at random.) Thus, $Succ (Receipt - Freeness - A (Γ, V, A, κ)) + Succ (Receipt - Freeness - B (Γ, V, B, κ)) ≰ \frac{1}{2} + negl (κ)$ , concluding our proof. □
A special case of our proposition holds for universal verifiability, rather than tally soundness, because universal verifiability is strictly stronger (Appendix E).

It follows from Proposition 33 that our syntax cannot be used to construct (interesting) election schemes satisfying stronger notions of privacy such as $Receipt - Freeness$ . Nonetheless, algorithm $Vote$ could be distributed between the voter and some other (possibly untrusted) parties to enable stronger privacy notions. Indeed, a variant of Helios that delegates ballot construction to a trusted party would satisfy receipt-freeness, since voters cannot access coins used by the trusted party to construct ballots, hence, cannot communicate such coins to the adversary. More generally, an election scheme satisfying ballot secrecy can delegate ballot construction to achieve receipt-freeness.

We have seen that election schemes for more than one candidate cannot satisfy $Receipt - Freeness$ (Proposition 33), assuming the election scheme is perfectly correct or satisfies tally soundness. Intuitively, it follows that coercion resistance cannot be satisfied by such election schemes either, because coercion resistance strengthens receipt-freeness. Nevertheless, receipt-freeness can be satisfied by election schemes with interactive voting algorithms and we now consider whether coercion resistance can hold too.
I.2. Coercion resistance

Coercion resistance requires a mechanism to deviate from a coercer’s instructions. Intuitively, no such mechanism exists for election schemes with interactive voting algorithms, because there exists instructions for which deviations are impossible. Indeed, the coercer can instruct the voter to run the algorithms themselves (i.e., without the aid of another party) and furnish the coercer with the coins used, thereby enabling the coercer to check whether voters followed their instructions. It follows that election schemes with interactive voting algorithms cannot satisfy coercion resistance.

Interactive voting algorithms can be extended with private inputs which cannot be simulated by voters, thereby enabling voters to deviate from the coercer’s instructions. Alternatively, the variant of our syntax with voter credentials [128, Definition 6] can be used; that variant extends algorithm $Vote$ to input a private credential (essentially resulting in interactive ballot construction). The latter has been used by Smyth, Frink & Clarkson [128, §6] to model the coercion-resistant voting system by Juels, Catalano & Jakobsson [76,77] and by Smyth as a foundation for his coercion-resistant voting system [117], thus, the syntax with voter credentials is compatible with stronger privacy notions.

References

Adida, Helios: Web-based open-audit voting, in: USENIX Security’08: 17th USENIX Security Symposium, USENIX Association, 2008, pp. 335–348.

Adida,

Marneffe,

Pereira and

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

Adida and

C.A.

Neff, Ballot casting assurance, in: EVT’06: Electronic Voting Technology Workshop, USENIX Association, 2006.

R.M.

Alvarez and

T.E.

Hall, Electronic Elections: The Perils and Promises of Digital Democracy, Princeton University Press, 2010. doi:10.1515/9781400834082.

Arapinis,

Bursuc and

Ryan, Reduction of equational theories for verification of trace equivalence: Re-encryption, associativity and commutativity, in: POST’12: First Conference on Principles of Security and Trust, LNCS, Vol. 7215, Springer, 2012, pp. 169–188. doi:10.1007/978-3-642-28641-4_10.

Bellare,

Desai,

Jokipii and

Rogaway, A concrete security treatment of symmetric encryption, in: FOCS’97: 38th Annual Symposium on Foundations of Computer Science, IEEE Computer Society, 1997, pp. 394–403.

Bellare,

Desai,

Pointcheval and

Rogaway, Relations among notions of security for public-key encryption schemes, in: CRYPTO’98: 18th International Cryptology Conference, LNCS, Vol. 1462, Springer, 1998, pp. 26–45. doi:10.1007/BFb0055718.

Bellare and

Rogaway, Random oracles are practical: A paradigm for designing efficient protocols, in: CCS’93: 1st ACM Conference on Computer and Communications Security, ACM, 1993, pp. 62–73. ISBN 0-89791-629-8. doi:10.1145/168588.168596.

Bellare and

Rogaway, Symmetric encryption, in: Introduction to Modern Cryptography, 2005, Chapter 4. http://cseweb.ucsd.edu/~mihir/cse207/w-se.pdf.

10.

Bellare and

Sahai, Non-malleable encryption: Equivalence between two notions, and an indistinguishability-based characterization, in: CRYPTO’99: 19th International Cryptology Conference, LNCS, Vol. 1666, Springer, 1999, pp. 519–536. doi:10.1007/3-540-48405-1_33.

11.

Benaloh, Verifiable Secret-Ballot Elections, PhD thesis, Department of Computer Science, Yale University, 1996.

12.

Benaloh,

Vaudenay and

Quisquater, Final Report of IACR Electronic Voting Committee, 2010, International Association for Cryptologic Research. http://www.iacr.org/elections/eVoting/finalReportHelios_2010-09-27.html.

13.

Benaloh and

Yung, Distributing the power of a government to enhance the privacy of voters, in: PODC’86: 5th Principles of Distributed Computing Symposium, ACM Press, 1986, pp. 52–62. doi:10.1145/10590.10595.

14.

J.C.

Benaloh and

Tuinstra, Receipt-free secret-ballot elections, in: STOC’94: 26th Theory of Computing Symposium, ACM Press, 1994, pp. 544–553. doi:10.1145/195058.195407.

15.

Bernhard, Zero-Knowledge Proofs in Theory and Practice, PhD thesis, Department of Computer Science, University of Bristol, 2014.

16.

Bernhard,

Cortier,

Galindo,

Pereira and

Warinschi, SoK: A comprehensive analysis of game-based ballot privacy definitions, in: S&P’15: 36th Security and Privacy Symposium, IEEE Computer Society, 2015, pp. 499–516.

17.

Bernhard,

Cortier,

Galindo,

Pereira and

Warinschi, A comprehensive analysis of game-based ballot privacy definitions, 2015, Cryptology ePrint Archive, Report 2015/255 (version 20150319:100626).

18.

Bernhard,

Cortier,

Pereira,

Smyth and

Warinschi, Adapting Helios for provable ballot privacy, in: ESORICS’11: 16th European Symposium on Research in Computer Security, LNCS, Vol. 6879, Springer, 2011, pp. 335–354.

19.

Bernhard,

Pereira and

Warinschi, How not to prove yourself: Pitfalls of the Fiat-Shamir heuristic and applications to Helios, in: ASIACRYPT’12: 18th International Conference on the Theory and Application of Cryptology and Information Security, LNCS, Vol. 7658, Springer, 2012, pp. 626–643.

20.

Bernhard,

Pereira and

Warinschi, On Necessary and Sufficient Conditions for Private Ballot Submission, 2012, Cryptology ePrint Archive, Report 2012/236 (version 20120430:154117b).

21.

Bernhard and

Smyth, Ballot secrecy with malicious bulletin boards, 2015, Cryptology ePrint Archive, Report 2014/822 (version 20150413:170300).

22.

Bernhard,

Benaloh,

J.A.

Halderman,

R.L.

Rivest,

P.Y.A.

Ryan,

P.B.

Stark,

Teague,

P.L.

Vora and

D.S.

Wallach, Public evidence from secret ballots, in: E-Vote-ID’17: 10th International Conference for Electronic Voting, LNCS, Springer, 2017, pp. 84–109.

23.

Bertrand,

J.-L.

Briquet and

Pels, Introduction: Towards a historical ethnography of voting, in: The Hidden History of the Secret Ballot, Indiana University Press, 2007.

24.

E.C.

Bjornlund, Beyond Free and Fair: Monitoring Elections and Building Democracy, Woodrow Wilson Center Press / Johns Hopkins University Press, 2004.

25.

Blanchet and

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

26.

Blanchet and

Smyth, Automated reasoning for equivalences in the applied pi calculus with barriers, Journal of Computer Security 26(3) (2018), 367–422. doi:10.3233/JCS-171013.

27.

Blanchet,

Smyth,

Cheval and

Sylvestre, ProVerif 1.96: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial, 2016.

28.

Bowen, Secretary of State Debra Bowen Moves to Strengthen Voter Confidence in Election Security Following Top-to-Bottom Review of Voting Systems, 2007, California Secretary of State, press release DB07:042.

29.

Brent, The Australian ballot: Not the secret ballot, Australian Journal of Political Science 41(1) (2006), 39–50. doi:10.1080/10361140500507278.

30.

Bulens,

Giry and

Pereira, Running Mixnet-based elections with Helios, in: EVT/WOTE’11: Electronic Voting Technology Workshop/Workshop on Trustworthy Elections, USENIX Association, 2011.

31.

Bundesverfassungsgericht (Germany’s Federal Constitutional Court), Use of Voting Computers in 2005 Bundestag Election Unconstitutional, 2009, Press release 19/2009.

32.

Chaidos,

Cortier,

Fuschbauer and

Galindo, BeleniosRF: A non-interactive receipt-free electronic voting scheme, in: CCS’16: 23rd ACM Conference on Computer and Communications Security, ACM Press, 2016, pp. 1614–1625. doi:10.1145/2976749.2978337.

33.

Chang-Fong and

Essex, The cloudier side of cryptographic end-to-end verifiable voting: A security analysis of Helios, in: ACSAC’16: 32nd Annual Conference on Computer Security Applications, ACM Press, 2016, pp. 324–335. doi:10.1145/2991079.2991106.

34.

Chaum,

Carback,

Clark,

Essex,

Popoveniuc,

R.L.

Rivest,

P.Y.A.

Ryan,

Shen and

A.T.

Sherman, Scantegrity II: End-to-end verifiability for optical scan election systems using invisible ink confirmation codes, in: EVT’08: Electronic Voting Technology Workshop, USENIX Association, 2008.

35.

Chaum,

Evertse,

van de Graaf and

Peralta, Demonstrating possession of a discrete logarithm without revealing it, in: CRYPTO’86: 6th International Cryptology Conference, LNCS, Vol. 263, Springer, 1987, pp. 200–212. doi:10.1007/3-540-47721-7_14.

36.

Chaum and

T.P.

Pedersen, Wallet databases with observers, in: CRYPTO’92: 12th International Cryptology Conference, LNCS, Vol. 740, Springer, 1993, pp. 89–105. doi:10.1007/3-540-48071-4_7.

37.

Chaum,

P.Y.

Ryan and

Schneider, A practical voter-verifiable election scheme, in: ESORICS’05: 10th European Symposium on Research in Computer Security, LNCS, Vol. 3679, Springer, 2005, pp. 118–139.

38.

D.L.

Chaum, Untraceable electronic mail, return addresses, and digital pseudonyms, Communications of the ACM 24 (1981), 84–90. doi:10.1145/358549.358563.

39.

Chor,

Goldwasser,

Micali and

Awerbuch, Verifiable secret sharing and achieving simultaneity in the presence of faults, in: FOCS’85: 26th Foundations of Computer Science Symposium, IEEE Computer Society, 1985, pp. 383–395.

40.

Chor and

M.O.

Rabin, Achieving independence in logarithmic number of rounds, in: PODC’87: 6th Principles of Distributed Computing Symposium, ACM Press, 1987, pp. 260–268. doi:10.1145/41840.41862.

41.

Clarkson,

Hay,

Inge, abhi shelat ,

Wagner and

Yasinsac, Software Review and Security Analysis of Scytl Remote Voting Software, http://election.dos.state.fl.us/voting-systems/pdf/FinalReportSept19.pdf.

42.

Cortier,

Galindo,

Glondu and

Izabachene, Distributed ElGamal à la Pedersen: Application to Helios, in: WPES’13: Workshop on Privacy in the Electronic Society, ACM Press, 2013, pp. 131–142. doi:10.1145/2517840.2517852.

43.

Cortier,

Galindo,

Glondu and

Izabachène, Election verifiability for Helios under weaker trust assumptions, in: ESORICS’14: 19th European Symposium on Research in Computer Security, LNCS, Vol. 8713, Springer, 2014, pp. 327–344.

44.

Cortier,

Galindo,

Glondu and

Izabachene, A generic construction for voting correctness at minimum cost - Application to Helios, 2013, Cryptology ePrint Archive, Report 2013/177 (version 20130521:145727).

45.

Cortier,

Schmidt,

C.C.

Drăgan,

P.-Y.

Strub,

Dupressoir and

Warinschi, Machine-checked proofs of privacy for electronic voting protocols, in: S&P’17: 37th IEEE Symposium on Security and Privacy, IEEE Computer Society, 2017.

46.

Cortier and

Smyth, Attacking and fixing Helios: An analysis of ballot secrecy, in: CSF’11: 24th Computer Security Foundations Symposium, IEEE Computer Society, 2011, pp. 297–311.

47.

Cortier and

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

48.

Cramer,

M.K.

Franklin,

Schoenmakers and

Yung, Multi-authority secret-ballot elections with linear work, in: EUROCRYPT’96: 15th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 1070, Springer, 1996, pp. 72–83.

49.

Cramer,

Gennaro and

Schoenmakers, A secure and optimally efficient multi-authority election scheme, in: EUROCRYPT’97: 16th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 1233, Springer, 1997, pp. 103–118.

50.

Cremers and

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

51.

Delaune,

Kremer and

Ryan, Coercion-resistance and receipt-freeness in electronic voting, in: CSFW’06: 19th Computer Security Foundations Workshop, IEEE Computer Society, 2006, pp. 28–42.

52.

Delaune,

Kremer and

M.D.

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

53.

Delaune,

Kremer,

M.D.

Ryan and

Steel, Formal analysis of protocols based on TPM state registers, in: CSF’11: 24th Computer Security Foundations Symposium, IEEE Computer Society, 2011, pp. 66–80.

54.

Delaune,

M.D.

Ryan and

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

55.

Desmedt and

Chaidos, Applying divertibility to blind ballot copying in the Helios Internet voting system, in: ESORICS’12: 17th European Symposium on Research in Computer Security, LNCS, Vol. 7459, Springer, 2012, pp. 433–450.

56.

Desmedt and

Kurosawa, Electronic voting: Starting over?, in: ISC’05: International Conference on Information Security, LNCS, Vol. 3650, Springer, 2005, pp. 329–343. doi:10.1007/11556992_24.

57.

Dolev,

Dwork and

Naor, Non-malleable cryptography, in: STOC’91: 23rd Theory of Computing Symposium, ACM Press, 1991, pp. 542–552. doi:10.1145/103418.103474.

58.

Dolev,

Dwork and

Naor, Nonmalleable cryptography, Journal on Computing 30(2) (2000), 391–437.

59.

Fiat and

Shamir, How to prove yourself: Practical solutions to identification and signature problems, in: CRYPTO’86: 6th International Cryptology Conference, LNCS, Vol. 263, Springer, 1987, pp. 186–194. doi:10.1007/3-540-47721-7_12.

60.

Fraser,

E.A.

Quaglia and

Smyth, A critique of game-based definitions of receipt-freeness for voting, in: ProveSec’19: 13th International Conference on Provable and Practical Security, LNCS, Springer, 2019.

61.

R.W.

Gardner,

Garera and

A.D.

Rubin, Coercion resistant end-to-end voting, in: FC’09: 13th International Conference on Financial Cryptography and Data Security, LNCS, Vol. 5628, Springer, 2009, pp. 344–361. doi:10.1007/978-3-642-03549-4_21.

62.

Gennaro, Achieving independence efficiently and securely, in: PODC’95: 14th Principles of Distributed Computing Symposium, ACM Press, 1995, pp. 130–136. doi:10.1145/224964.224979.

63.

Gennaro, A protocol to achieve independence in constant rounds, IEEE Transactions on Parallel and Distributed Systems 11(7) (2000), 636–647. doi:10.1109/71.877748.

64.

Gjøsteen, The Norwegian Internet voting protocol, in: VoteID’11: 3rd International Conference on e-Voting and Identity, Springer, 2012, pp. 1–18.

65.

Gonggrijp and

W.-J.

Hengeveld, Studying the Nedap/Groenendaal ES3B Voting Computer: A computer security perspective, in: EVT’07: Electronic Voting Technology Workshop, USENIX Association, 2007.

66.

Groth, Efficient maximal privacy in boardroom voting and anonymous broadcast, in: FC’04: 8th International Conference on Financial Cryptography, LNCS, Vol. 3110, Springer, 2004, pp. 90–104. doi:10.1007/978-3-540-27809-2_10.

67.

Groth, Simulation-sound NIZK proofs for a practical language and constant size group signatures, in: ASIACRYPT’02: 12th International Conference on the Theory and Application of Cryptology and Information Security, LNCS, Vol. 4284, Springer, 2006, pp. 444–459.

68.

Gumbel, Steal This Vote: Dirty Elections and the Rotten History of Democracy in America, Nation Books, 2005.

69.

Haber,

Benaloh and

Halevi, The Helios e-Voting Demo for the IACR, 2010, International Association for Cryptologic Research. http://www.iacr.org/elections/eVoting/heliosDemo.pdf.

70.

Haines and

Smyth, Surveying definitions of coercion resistance, 2020.

71.

Hao,

P.Y.A.

Ryan and

Zieliński, Anonymous voting by two-round public discussion, Journal of Information Security 4(2) (2010), 62–67.

72.

Heather and

Schneider, A formal framework for modelling coercion resistanc and receipt freeness, in: FM’12: 18th International Symposium on Formal Methods, LNCS, Springer, 2012, pp. 217–231.

73.

Hevia and

M.A.

Kiwi, Electronic jury voting protocols, in: LATIN’02: Theoretical Informatics, LNCS, Vol. 2286, Springer, 2002, pp. 415–429.

74.

Hevia and

M.A.

Kiwi, Electronic jury voting protocols, Theoretical Computer Science 321(1) (2004), 73–94. doi:10.1016/j.tcs.2003.06.003.

75.

D.W.

Jones and

Simons, Broken Ballots: Will Your Vote Count?, CSLI Lecture Notes, Vol. 204, Center for the Study of Language and Information, Stanford University, 2012.

76.

Juels,

Catalano and

Jakobsson, Coercion-resistant electronic elections, in: WPES’05: 4th Workshop on Privacy in the Electronic Society, ACM Press, 2005, pp. 61–70. doi:10.1145/1102199.1102213.

77.

Juels,

Catalano and

Jakobsson, Coercion-resistant electronic elections, in: Towards Trustworthy Elections: New Directions in Electronic Voting,

Chaum,

Jakobsson,

R.L.

Rivest and

P.Y.

Ryan, eds, LNCS, Vol. 6000, Springer, 2010, pp. 37–63. doi:10.1007/978-3-642-12980-3_2.

78.

Katz and

Lindell, Introduction to Modern Cryptography, Chapman & Hall/CRC, 2007. doi:10.1201/9781420010756.

79.

J.G.

Kelley, Monitoring Democracy: When International Election Observation Works, and Why It Often Fails, Princeton University Press, 2012.

80.

Khader,

Smyth,

P.Y.A.

Ryan and

Hao, A fair and robust voting system by broadcast, in: EVOTE’12: 5th International Conference on Electronic Voting, Lecture Notes in Informatics, Vol. 205, Gesellschaft für Informatik, 2012, pp. 285–299.

81.

Khazaei and

Rezaei-Aliabadi, A rigorous security analysis of a decentralized electronic voting protocol in the universal composability framework, Journal of Information Security and Applications 43 (2018), 99–109. doi:10.1016/j.jisa.2018.10.010.

82.

Kiayias and

Yung, Self-tallying elections and perfect ballot secrecy, in: PKC’01: 3rd International Workshop on Practice and Theory in Public Key Cryptography, LNCS, Vol. 2274, Springer, 2002, pp. 141–158.

83.

Kiayias,

Zacharias and

Zhang, End-to-end verifiable elections in the standard model, in: EUROCRYPT’15: 34th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 9057, Springer, 2015, pp. 468–498.

84.

Klus,

Smyth and

M.D.

Ryan, ProSwapper: Improved equivalence verifier for ProVerif, 2010, http://www.bensmyth.com/proswapper.php.

85.

Kohno,

Stubblefield,

A.D.

Rubin and

D.S.

Wallach, Analysis of an electronic voting system, in: S&P’04: 25th Security and Privacy Symposium, IEEE Computer Society, 2004, pp. 27–40.

86.

Küsters,

Truderung and

Vogt, Accountability: Definition and relationship to verifiability, in: CCS’10: 17th ACM Conference on Computer and Communications Security, ACM Press, 2010, pp. 526–535. doi:10.1145/1866307.1866366.

87.

Küsters,

Truderung and

Vogt, Clash attacks on the verifiability of E-voting systems, in: S&P’12: 33rd IEEE Symposium on Security and Privacy, IEEE Computer Society, 2012, pp. 395–409.

88.

Küsters,

Truderung and

Vogt, A game-based definition of coercion-resistance and its applications, Journal of Computer Security 20(6) (2012), 709–764. doi:10.3233/JCS-2012-0444.

89.

Lepore, Rock, Paper, Scissors: How we used to vote, Annals of Democracy, The New Yorker (2008).

90.

Lijphart and

Grofman, Choosing an Electoral System: Issues and Alternatives, Praeger, 1984.

91.

Maaten, Towards remote e-voting: Estonian case, Electronic Voting in Europe-Technology, Law, Politics and Society 47 (2004), 83–100.

92.

McCarthy,

Smyth and

E.A.

Quaglia, Hawk and aucitas: E-auction schemes from the Helios and Civitas e-voting schemes, in: FC’14: 18th International Conference on Financial Cryptography and Data Security, LNCS, Vol. 8437, Springer, 2014, pp. 51–63.

93.

Meyer and

Smyth, Exploiting re-voting in the Helios election system, Information Processing Letters (2019), 14–19.

94.

Michels and

Horster, Some remarks on a receipt-free and universally verifiable mix-type voting scheme, in: ASIACRYPT’96: International Conference on the Theory and Application of Cryptology and Information Security, LNCS, Vol. 1163, Springer, 1996, pp. 125–132. doi:10.1007/BFb0034841.

95.

Mill, The Ballot, in: The Westminster Review, Vol. 13, Robert Heward, 1830.

96.

Moran and

Naor, Receipt-free universally-verifiable voting with everlasting privacy, in: CRYPTO’06: 26th International Cryptology Conference, LNCS, Vol. 4117, Springer, 2006, pp. 373–392.

97.

C.A.

Neff, Practical High Certainty Intent Verification for Encrypted Votes, Technical Report, VoteHere, 2004.

98.

C.A.

Neff and

Adler, Verifiable e-Voting: Indisputable electronic elections at polling places, Technical Report, VoteHere, 2003.

99.

NIST , Secure Hash Standard (SHS), FIPS PUB, 180-4, Information Technology Laboratory, National Institute of Standards and Technology, 2012.

100.

Norris, Why Elections Fail, Cambridge University Press, 2015. doi:10.1017/CBO9781107280908.

101.

Organization for Security and Co-operation in Europe, Document of the Copenhagen Meeting of the Conference on the Human Dimension of the CSCE, 1990.

102.

Organization of American States, American Convention on Human Rights, “Pact of San Jose, Costa Rica”, 1969.

103.

Paiola and

Blanchet, Verification of security protocols with lists: From length one to unbounded length, in: POST’12: First Conference on Principles of Security and Trust, LNCS, Vol. 7215, Springer, 2012, pp. 69–88. doi:10.1007/978-3-642-28641-4_5.

104.

Pfitzmann, Breaking efficient anonymous channel, in: EUROCRYPT’94: 11th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 950, Springer, 1994, pp. 332–340. doi:10.1007/BFb0053448.

105.

Pfitzmann and

Pfitzmann, How to break the direct RSA-implementation of mixes, in: EUROCRYPT’89: 6th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 434, Springer, 1989, pp. 373–381.

106.

G.V.

Post, Using re-voting to reduce the threat of coercion in elections, Electronic Government, an International Journal 7(2) (2010), 168–182. doi:10.1504/EG.2010.030926.

107.

E.A.

Quaglia and

Smyth, Authentication with weaker trust assumptions for voting systems, in: AFRICACRYPT’18: 10th International Conference on Cryptology in Africa, LNCS, Springer, 2018.

108.

E.A.

Quaglia and

Smyth, Secret, verifiable auctions from elections, Theoretical Computer Science 730 (2018), 44–92. doi:10.1016/j.tcs.2018.03.022.

109.

E.A.

Quaglia and

Smyth, A short introduction to secrecy and verifiability for elections, 2018, arXiv, Report 1702.03168.

110.

Saalfeld, On dogs and whips: Recorded votes, in: Parliaments and Majority Rule in Western Europe,

Döring, ed., St. Martin’s Press, 1995, Chapter 16.

111.

Sako and

Kilian, Receipt-free mix-type voting scheme: A practical solution to the implementation of a voting booth, in: EUROCRYPT’95: 12th International Conference on the Theory and Applications of Cryptographic Techniques, LNCS, Vol. 921, Springer, 1995, pp. 393–403.

112.

Schoenmakers, A simple publicly verifiable secret sharing scheme and its application to electronic voting, in: CRYPTO’99: 19th International Cryptology Conference, LNCS, Vol. 1666, Springer, 1999, pp. 148–164. doi:10.1007/3-540-48405-1_10.

113.

Schweikardt, Arithmetic, first-order logic, and counting quantifiers, ACM Transactions on Computational Logic 6(3) (2005), 634–671. doi:10.1145/1071596.1071602.

114.

Shoup, Sequences of games: A tool for taming complexity in security proofs, 2004.

115.

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

116.

Smyth, Verifiability of Helios Mixnet, in: Voting’18: 3rd Workshop on Advances in Secure Electronic Voting, LNCS, Springer, 2018.

117.

Smyth, Athena: A verifiable, coercion-resistant voting system with linear complexity, 2019.

118.

Smyth, First-past-the-post suffices for ranked voting, 2017, https://bensmyth.com/publications/2017-FPTP-suffices-for-ranked-voting/.

119.

Smyth, Replay attacks that violate ballot secrecy in Helios, 2012, Cryptology ePrint Archive, Report 2012/185.

120.

Smyth, A foundation for secret, verifiable elections, 2018, Cryptology ePrint Archive, Report 2018/225 (version 20180301:164045).

121.

Smyth, Ballot secrecy with malicious bulletin boards, 2014, Cryptology ePrint Archive, Report 2014/822 (version 20141012:004943).

122.

Smyth, Secrecy and independence for election schemes, 2015, Cryptology ePrint Archive, Report 2015/942 (version 20150928:195428).

123.

Smyth, Secrecy and independence for election schemes, 2016, Cryptology ePrint Archive, Report 2015/942 (version 20160713:142934).

124.

Smyth, Verifiability of Helios Mixnet, 2018, Cryptology ePrint Archive, Report 2018/017.

125.

Smyth and

Bernhard, Ballot secrecy and ballot independence coincide, in: ESORICS’13: 18th European Symposium on Research in Computer Security, LNCS, Vol. 8134, Springer, 2013, pp. 463–480.

126.

Smyth and

Bernhard, Ballot secrecy and ballot independence: Definitions and relations, 2014, Cryptology ePrint Archive, Report 2013/235 (version 20141010:082554).

127.

Smyth and

Cortier, A note on replay attacks that violate privacy in electronic voting schemes, Technical Report, RR-7643, INRIA, 2011.

128.

Smyth,

Frink and

M.R.

Clarkson, Election Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJ, 2017, Cryptology ePrint Archive, Report 2015/233 (version 20170213:132559).

129.

Smyth and

Hanatani, Non-malleable encryption with proofs of plaintext knowledge and applications to voting, International Journal of Security and Networks 14(4) (2019), 191–204. doi:10.1504/IJSN.2019.103150.

130.

Smyth,

Hanatani and

Muratani, NM-CPA secure encryption with proofs of plaintext knowledge, in: IWSEC’15: 10th International Workshop on Security, LNCS, Vol. 9241, Springer, 2015, pp. 115–134.

131.

Smyth and

Pironti, Truncating TLS connections to violate beliefs in web applications, in: WOOT’13: 7th USENIX Workshop on Offensive Technologies, USENIX Association, 2013 (First appeared at Black Hat USA 2013).

132.

Smyth and

Pironti, Truncating TLS Connections to Violate Beliefs in Web Applications, Technical Report, hal-01102013, INRIA, 2015.

133.

Springall,

Finkenauer,

Durumeric,

Kitcat,

Hursti,

MacAlpine and

J.A.

Halderman, Security analysis of the Estonian Internet Voting System, in: CCS’14: 21st ACM Conference on Computer and Communications Security, ACM Press, 2014, pp. 703–715. doi:10.1145/2660267.2660315.

134.

Staff, ACM’s 2014 General Election: Please take this opportunity to vote, Communications of the ACM 57(5) (2014), 9–17. doi:10.1145/2597769.

135.

Tsiounis and

Yung, On the security of ElGamal based encryption, in: PKC’98: First International Workshop on Practice and Theory in Public Key Cryptography, LNCS, Vol. 1431, Springer, 1998, pp. 117–134.

136.

Tsoukalas,

Papadimitriou,

Louridas and

Tsanakas, From Helios to Zeus, Journal of Election Technology and Systems 1(1) (2013).

137.

UK Electoral Commission, Key Issues and Conclusions: May 2007 Electoral Pilot Schemes, 2007.

138.

United Nations, Universal Declaration of Human Rights, 1948.

139.

Unruh and

Müller-Quade, Universally composable incoercibility, in: CRYPTO’10: 30th International Cryptology Conference, LNCS, Vol. 6223, Springer, 2010, pp. 411–428.

140.

Wikström, Simplified submission of inputs to protocols, in: SCN’08: 6th International Conference on Security and Cryptography for Networks, LNCS, Vol. 5229, Springer, 2008, pp. 293–308. doi:10.1007/978-3-540-85855-3_20.

141.

Wikström, Verificatum: How to Implement a Stand-Alone Verifier for the Verificatum Mix-Net (VMN Version 3.0.2), 2016, http://www.verificatum.com/files/vmnum-3.0.2.pdf .

142.

Wikström, Simplified Submission of Inputs to Protocols, 2006, Cryptology ePrint Archive, Report 2006/259.

143.

Wolchok,

Wustrow,

J.A.

Halderman,

H.K.

Prasad,

Kankipati,

S.K.

Sakhamuri,

Yagati and

Gonggrijp, Security analysis of India’s electronic voting machines, in: CCS’10: 17th ACM Conference on Computer and Communications Security, ACM Press, 2010, pp. 1–14.

144.

Wolchok,

Wustrow,

Isabel and

J.A.

Halderman, Attacking the Washington, D.C. Internet voting system, in: FC’12: 16th International Conference on Financial Cryptography and Data Security, LNCS, Vol. 7397, Springer, 2012, pp. 114–128. doi:10.1007/978-3-642-32946-3_10.

Ballot secrecy: Security definition,sufficient conditions,and analysis of Helios

Abstract

Keywords

1. Introduction

1 Earlier systems merely required ballots to be marked in polling booths and deposited into ballot boxes, which permitted non-uniform ballots, including ballots of different colours and sizes, that could be easily identified as party tickets [29].

5 Smyth, Frink & Clarkson use the syntax to model first-past-the-post voting systems [128] and Smyth shows ranked-choice voting systems can be modelled too [118].

3. Privacy

6 Voting systems that announce chosen representatives (e.g., [13,56,73,74]), rather than frequency distributions of votes, could offer stronger notions of privacy.

8 Bellare et al. introduced left-right oracles in the context of symmetric encryption [6] and Bellare & Rogaway provide a tutorial on their use [9].

10 Non-malleability was first formalised by Dolev, Dwork & Naor in the context of asymmetric encryption [57,58]; the definition by Bellare & Sahai builds upon their results and results by Bellare et al. [7].

3.3. Secrecy and independence coincide (for zero-knowledge tallying proofs)

Theorem 1 ( Ballot - Secrecy ⇒ IND - CVA ).

Proposition 2 ( IND - CVA ⇏ Ballot - Secrecy ).

Proposition 3 ( Ballot - Secrecy = IND - CVA , without proofs).

Theorem 4 ( Ballot - Secrecy = IND - CVA , with ZK proofs).

11 https://github.com/benadida/helios/releases/tag/2.0, released 25 Jul 2009, accessed 29 Mar 2019.

16 I do not recall the exact origin of this idea: Email communication suggests both I (17 Dec 2010) and Olivier Pereira (27 Dec 2010) each independently conceived the need for a proven ordering over ciphertexts.

Definition 7 ( Tally - Soundness ).

27 Some revelations are an artefact of announcing the outcome as a frequency distribution of votes (a functional requirement of many nations, which comes at a privacy cost), rather than revealing less information, e.g., just the winning candidate [13,56,74].

28 Quaglia & Smyth present a tutorial-style introduction to modelling ballot secrecy [109], and Bernhard et al. survey ballot secrecy definitions [16,17].

Acknowledgements

A. Cryptographic primitives

A.1. Asymmetric encryption

Definition 10 (Asymmetric encryption scheme [78]).

31 Our definition differs from Katz and Lindell’s original definition [78, Definition 10.1] in that we formally state the plaintext space.

32 For brevity, we write Π is a homomorphic asymmetric encryption scheme as opposed to the more verbose Π is a homomorphic asymmetric encryption scheme, with respect to ternary operators ⊙, ⊕, and ⊗.

A.2. Proof systems

Definition 14 (Non-interactive proof system [128]).

Definition 15 (Fiat-Shamir transformation [59]).

Definition 16 (Zero-knowledge [108]).

35 Random oracles can be programmed or patched. We will not need the details of how patching works, so we omit them here; see Bernhard et al. [19] for a formalisation.

36 We extend set membership notation to vectors: we write x ∈ x if x is an element of the set { x [ i ] : 1 ⩽ i ⩽ | x | } .

B. Ballot independence: Non-malleability game

Definition 18 ( CNM - CVA ).

Theorem 16 ( CNM - CVA = IND - CVA ).

C.1. Proof of Theorem 1

C.2. Proof of Proposition 3

C.3. Proof of Theorem 4

Definition 19 (Zero-knowledge tallying proofs).

C.5. Proof of Proposition 11

D. Helios

Definition 22 (from [128]).

38 We omit algorithm Verify for brevity.

Definition 25 (Helios 2.0 [128]).

Definition 26 (Helios 3.1.4 [128]).

Definition 27 (Helios’16 [128]).

D.1. Proof of Theorem 6

Definition 28 (Completeness [128]).

Definition 29 (Injectivity [116,128]).

Definition 30 (Soundness [128]).

Definition 31 ( UV [116,128]).

Definition 32 ( Enc 2 Vote + [116]).

Definition 33 (from [128]).

Definition 34 ( HeliosM [108,124]).

40 We omit algorithm Verify for brevity.

G.1. Proof of Theorem 14

H. Ballot - Secrecy is strictly stronger than IND - SEC

Definition 36 (Election scheme with a trusted bulletin board).

41 For receipt-freeness to be an effective notion of free-choice it might be necessary for the voting system to prevent voters deviating from the prescribed voting procedure. This might be achieved by physically securing devices that can be used to cast ballots.

Definition 39 ( Receipt - Freeness ).

References

¹
Earlier systems merely required ballots to be marked in polling booths and deposited into ballot boxes, which permitted non-uniform ballots, including ballots of different colours and sizes, that could be easily identified as party tickets [29].

⁵
Smyth, Frink & Clarkson use the syntax to model first-past-the-post voting systems [128] and Smyth shows ranked-choice voting systems can be modelled too [118].

⁶
Voting systems that announce chosen representatives (e.g., [13,56,73,74]), rather than frequency distributions of votes, could offer stronger notions of privacy.

⁸
Bellare et al. introduced left-right oracles in the context of symmetric encryption [6] and Bellare & Rogaway provide a tutorial on their use [9].

¹⁰
Non-malleability was first formalised by Dolev, Dwork & Naor in the context of asymmetric encryption [57,58]; the definition by Bellare & Sahai builds upon their results and results by Bellare et al. [7].

Theorem 1 ( $Ballot - Secrecy \Rightarrow IND - CVA$ ).

Proposition 2 ( $IND - CVA ⇏ Ballot - Secrecy$ ).

Proposition 3 ( $Ballot - Secrecy = IND - CVA$ , without proofs).

Theorem 4 ( $Ballot - Secrecy = IND - CVA$ , with ZK proofs).

¹¹
https://github.com/benadida/helios/releases/tag/2.0, released 25 Jul 2009, accessed 29 Mar 2019.

¹⁶
I do not recall the exact origin of this idea: Email communication suggests both I (17 Dec 2010) and Olivier Pereira (27 Dec 2010) each independently conceived the need for a proven ordering over ciphertexts.

Definition 7 ( $Tally - Soundness$ ).

²⁷
Some revelations are an artefact of announcing the outcome as a frequency distribution of votes (a functional requirement of many nations, which comes at a privacy cost), rather than revealing less information, e.g., just the winning candidate [13,56,74].

²⁸
Quaglia & Smyth present a tutorial-style introduction to modelling ballot secrecy [109], and Bernhard et al. survey ballot secrecy definitions [16,17].

³¹
Our definition differs from Katz and Lindell’s original definition [78, Definition 10.1] in that we formally state the plaintext space.

³²
For brevity, we write Π is a homomorphic asymmetric encryption scheme as opposed to the more verbose Π is a homomorphic asymmetric encryption scheme, with respect to ternary operators ⊙, ⊕, and ⊗.

³⁵
Random oracles can be programmed or patched. We will not need the details of how patching works, so we omit them here; see Bernhard et al. [19] for a formalisation.

³⁶
We extend set membership notation to vectors: we write $x \in x$ if x is an element of the set ${x [i] : 1 ⩽ i ⩽ | x |}$ .

Definition 18 ( $CNM - CVA$ ).

Theorem 16 ( $CNM - CVA = IND - CVA$ ).

³⁸
We omit algorithm $Verify$ for brevity.

Definition 31 ( $UV$ [116,128]).

Definition 32 ( ${Enc 2 Vote}^{+}$ [116]).

Definition 34 ( $HeliosM$ [108,124]).

⁴⁰
We omit algorithm $Verify$ for brevity.

H. $Ballot - Secrecy$ is strictly stronger than $IND - SEC$

⁴¹
For receipt-freeness to be an effective notion of free-choice it might be necessary for the voting system to prevent voters deviating from the prescribed voting procedure. This might be achieved by physically securing devices that can be used to cast ballots.

Definition 39 ( $Receipt - Freeness$ ).