# Attacking and fixing Helios: An analysis of ballot secrecy , ## Abstract Helios 2.0 is an open-source web-based end-to-end verifiable electronic voting system, suitable for use in low-coercion environments. In this paper, we analyse ballot secrecy and discover a vulnerability which allows an adversary to compromise the privacy of voters. This vulnerability has been successfully exploited to break privacy in a mock election using the current Helios implementation. Moreover, the feasibility of an attack is considered in the context of French legislative elections and, based upon our findings, we believe it constitutes a real threat to ballot secrecy in such settings. Finally, we present a fix and show that our solution satisfies a formal definition of ballot secrecy using the applied pi calculus.
Applied Pi Calculus, Attack, Ballot Independence, Ballot Secrecy, Electronic Voting, Helios, Privacy.
# Introduction Paper-based elections derive privacy properties from physical characteristics of the real-world, for example, the indistinguishability of an individual’s ballot from an arbitrary ballot, and the inability of a coercer to collaborate with a voter inside a polling booth. Replicating these attributes in a digital setting has proven to be difficult and, hence, the provision of electronic voting systems which ensure the privacy of voters is an active research topic (Fujioka, Okamoto, and Ohta 1992; Okamoto 1998; Juels, Catalano, and Jakobsson 2002). Informally, privacy for electronic voting systems is characterised by the following properties (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2006; Backes, Hriţcu, and Maffei 2008): - *Ballot secrecy.* A voter’s vote is not revealed to anyone. - *Receipt freeness.* A voter cannot gain information which can be used to prove, to a coercer, how she voted. - *Coercion resistance.* A voter cannot collaborate, with a coercer, to gain information which can be used to prove how she voted. Other desirable properties of electronic voting systems include (Juels, Catalano, and Jakobsson 2002; Participants of the Dagstuhl Conference on Frontiers of E-Voting 2007; Kremer, Ryan, and Smyth 2010): - *Fairness:* All votes are independently cast. - *Individual verifiability:* A voter can check that her own ballot is published on the election’s bulletin board. - *Universal verifiability:* Anyone can check that all the votes in the election outcome correspond to ballots published on the election’s bulletin board. The fairness property prohibits the voting system from influencing a voter’s vote; more formally, this requires that observation of the voting system (that is, observing interaction between participants) does not leak information that may affect a voter’s decision. One aspect of fairness is *ballot independence*, which based upon (Gennaro 1995, sec. 1.1) can be informally stated as: observing another voter’s interaction with the election system does not allow a voter to cast a *related* vote. The individual and universal verifiability properties (also called *end-to-end verifiability* (Juels, Catalano, and Jakobsson 2002; Chaum, Ryan, and Schneider 2005; Adida 2006, 2008; Participants of the Dagstuhl Conference on Frontiers of E-Voting 2007)) allow voters and election observers to verify – independently of the hardware and software running the election – that votes have been recorded, tallied and declared correctly. In this paper, we analyse ballot secrecy in Helios 2.0 (Adida et al. 2009). Helios is an open-source web-based electronic voting system. The scheme is claimed to satisfy ballot secrecy (Adida et al. 2009), but the nature of remote voting makes the possibility of satisfying stronger privacy properties difficult, and Helios does not satisfy receipt freeness nor coercion resistance. In addition to ballot secrecy, the system provides end-to-end verifiability (cf. (Kremer, Ryan, and Smyth 2010; Smyth et al. 2010) and (Smyth 2011, chap. 3) for an analysis of end-to-end verifiability in Helios). Helios is particularly significant due to its real-world deployment: the International Association of Cryptologic Research used Helios to elect its board members (Benaloh, Vaudenay, and Quisquater 2010), following a successful trial in a non-binding poll (Haber, Benaloh, and Halevi 2010); the Catholic University of Louvain adopted the system to elect the university president (Adida et al. 2009); and Princeton University used Helios to elect the student vice president (Princeton University 2010). Formal definitions of ballot secrecy have been introduced in the context of the applied pi calculus by Delaune, Kremer & Ryan (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2006; Delaune, Kremer, and Ryan 2009, 2010) and Backes, Hriţcu & Maffei (Backes, Hriţcu, and Maffei 2008). These privacy definitions consider two voters $\mathcal{A}$, $\mathcal{B}$ and two candidates $t$, $t'$. Ballot secrecy is captured by the assertion that an adversary (controlling arbitrary many dishonest voters) cannot distinguish between a situation in which voter $\mathcal{A}$ votes for candidate $t$ and voter $\mathcal{B}$ votes for candidate $t'$, from another situation in which $\mathcal{A}$ votes $t'$ and $\mathcal{B}$ votes $t$. This can be expressed by the following equivalence. $$\mathcal{A}(t)\mid\mathcal{B}(t') \approx_l \mathcal{A}(t')\mid\mathcal{B}(t)$$ These formal definitions of ballot secrecy have been used by their respective authors to analyse the electronic voting protocols due to: Fujioka, Okamoto & Ohta (Fujioka, Okamoto, and Ohta 1992), Okamoto (Okamoto 1998), Lee *et al.* (Lee et al. 2004), and Juels, Catalano & Jakobsson (Juels, Catalano, and Jakobsson 2002, 2005, 2010). It therefore seems natural to check whether Helios satisfies ballot secrecy as well. #### Contribution Our analysis of Helios reveals an attack which violates ballot secrecy. The attack exploits the system’s lack of ballot independence, and works by replaying a voter’s ballot or a variant of it (without knowing the vote contained within that ballot). Replaying a voter’s ballot immediately violates ballot secrecy in an election with three voters. For example, consider the electorate Alice, Bob, and Mallory; if Mallory replays Alice’s ballot, then Mallory can reveal Alice’s vote by observing the election outcome and checking which candidate obtained at least two votes. The practicality of this attack has been demonstrated by violating privacy in a mock election using the current Helios implementation. Furthermore, the vulnerability can be exploited in more realistic settings and, as an illustrative example, we discuss the feasibility of the attack in French legislative elections. This case study suggests there is a plausible threat to ballot secrecy. We also propose a variant of the attack which abuses the malleability of ballots to ensure replayed ballots are distinct: this makes identification of replayed ballots non-trivial (that is, checking for exact duplicates is insufficient). Nonetheless, we fix the Helios protocol by identifying and discarding replayed ballots. We believe this solution is particular well-suited because it maintains Benaloh’s principle of ballot casting assurance (Benaloh 2006, 2007) and requires a minimal extension to the Helios code-base. Finally, we show that the revised scheme satisfies a formal definition of ballot secrecy using the applied pi calculus. #### Related work The concept of independence was introduced by Chor *et al.* (Chor et al. 1985) and the possibility of compromising security properties due to lack of independence has been considered, for example, by (Chor and Rabin 1987; Dolev, Dwork, and Naor 1991, 2000; Gennaro 2000). In the context of electronic voting, Gennaro (Gennaro 1995) demonstrates that the application of the Fiat-Shamir heuristic in the Sako-Kilian electronic voting protocol (Sako and Kilian 1994) violates ballot independence, and Wikström (Wikström 2006, 2008) studies non-malleability for mixnets to achieve ballot independence. By comparison, we focus on the violation of ballot secrecy rather than fairness, and exploit the absence of ballot independence to compromise privacy. Similar results have been shown against mixnets (Pfitzmann 1994). Estehghari & Desmedt (Estehghari and Desmedt 2010) claim to present an attack which undermines privacy and end-to-end verifiability in Helios. However, their attack is dependent on compromising a voter’s computer, a vulnerability which is explicitly acknowledged by the Helios specification (Adida et al. 2009): *“a specifically targeted virus could surreptitiously change a user’s vote and mask all of the verifications performed via the same computer to cover its tracks."* Accordingly, (Estehghari and Desmedt 2010) represents an exploration of known vulnerabilities rather than an attack. Langer *et al.* (Langer 2010; Langer, Schmidt, Buchmann, and Volkamer 2010) and Volkamer & Grimm (Volkamer and Grimm 2010) also study privacy in Helios. Langer *et al.* propose a taxonomy of informal privacy requirements (Langer 2010; Langer, Schmidt, Buchmann, and Volkamer 2010; Langer, Schmidt, Buchmann, Volkamer, and Stolfik 2010) to facilitate a more fine-grained comparison of electronic voting systems; this framework is used to analyse Helios and the authors claim ballot secrecy is satisfied if the adversary only has access to public data (Langer 2010; Langer, Schmidt, Buchmann, and Volkamer 2010). Volkamer & Grimm introduce the *$k$-resilience* metric (Volkamer and Grimm 2010; Volkamer 2009) to calculate the number of honest participants required for ballot secrecy in particular scenarios; this framework is used to analyse Helios and the authors claim ballot secrecy is satisfied if the software developers are honest and the key holders do not collude (Volkamer and Grimm 2010). Contrary to these results, we show an attack against privacy. Our work highlights the necessity for rigorous mathematical analysis techniques for security protocols; in particular, we believe the erroneous results reported by Langer *et al.* were due to the use of informal methods, and the approach by Volkamer & Grimm failed because only some particular scenarios were considered. #### Structure of this paper Section 2 presents the Helios electronic voting scheme. (We remark that this is the first cryptographic description of the Helios protocol in the literature and, hence, is an additional contribution of this paper.) Section 3 describes our attack and some variants, in addition to a study of its feasibility in the context of French legislative elections. We propose several solutions for recovering privacy in Section 4 and prove that our adopted solution formally satisfies ballot secrecy in Section 5. # Background: Helios 2.0 Helios exploits the additive homomorphic (Cramer, Damgård, and Schoenmakers 1994; Cramer, Gennaro, and Schoenmakers 1997; Schoenmakers 2009) and distributed decryption (Pedersen 1991; Chaum and Pedersen 1993) properties of ElGamal (ElGamal 1985). We will recall these cryptographic details before presenting the Helios protocol. ## Additive homomorphic ElGamal Given cryptographic parameters $(p,q,g)$ and a number $n\in\mathbb{N}$ of trustees, where $p$ and $q$ are large primes such that $q \mid p-1$ and $g$ is a generator of the multiplicative group $\mathbb{Z}^*_p$ of order $q$, the following operations are defined by ElGamal. #### Distributed key generation Each trustee $i \in n$ selects a private key share $x_i \in_R \mathbb{Z}_q^*$ and computes a public key share $h_i = g^{x_i} \bmod p$. The public key is $h = h_1 \cdot \ldots \cdot h_n \bmod p$. #### Encryption Given a message $m$ and a public key $h$, select a random nonce $r \in_R \mathbb{Z}_q^*$ and derive the ciphertext $(a,b) = (g^r \bmod p,\;g^m \cdot h^r \bmod p)$. #### Re-encryption Given a ciphertext $(a,b)$ and public key $h$, select a random nonce $r' \in_R \mathbb{Z}_q^*$ and derive the re-encrypted ciphertext $(a',b') = (a \cdot g^{r'} \bmod p,\; b \cdot h^{r'} \bmod p)$. #### Homomorphic addition Given two ciphertexts $(a,b)$ and $(a',b')$, the homomorphic addition of plaintexts is computed by multiplication $(a \cdot a' \bmod p,\; b \cdot b' \bmod p)$. #### Distributed decryption Given a ciphertext $(a,b)$, each trustee $i\in n$ computes the partial decryption $k_i = a^{x_i}$. The plaintext $m = \log_g M$ is recovered from $M = b/(k_1 \cdot \ldots \cdot k_n) \bmod p$. The computation of a discrete logarithm $\log_g M$ is hard in general. However, if $M$ is chosen from a restricted domain, then the complexity is reduced; for example, if $M$ is an integer such that $0 \leq M \leq n$, then the complexity is $O(n)$ by linear search or $O(\sqrt n)$ using the baby-step giant-step algorithm (Shanks 1971) (see also (Lenstra and Lenstra Jr. 1990, sec. 3.1)). For secrecy, each trustee $i\in n$ must demonstrate knowledge of a discrete logarithm $\log_g h_i$, that is, they proof that $h_i$ has been correctly constructed; this prevents, for example, a trustee constructing their public key share $h_i = h$. For integrity of decryption, each trustee $i\in n$ must demonstrate equality between discrete logarithms $\log_g h_i$ and $\log_a k_i$; this prevents, for example, a trustee constructing the public key share $h_i = g^{m+x_i}$ and providing the partial decryption $k_i = a^{x_i}$. In addition, the voter must demonstrate that a valid vote has been encrypted. These proofs can be achieved using signatures of knowledge (see Appendix 6.1 for details). ## Protocol description An election is created by naming an election officer, selecting a set of trustees, and generating a distributed public key pair. The election officer publishes, on the bulletin board, the public part of the trustees’ key (and proof of correct construction), the candidate list $\tilde{t} = (t_1,\dots,t_l) \cup \{\epsilon\}$ (where $\epsilon$ represents a vote of abstention), and the list of eligible voters $\widetilde{id} = (id_1,\dots,id_n)$; the officer also publishes the *election fingerprint*, that is, the hash of these parameters. Informally, the steps that participants take during a run of Helios are as follows. 1. The voter launches a browser script that downloads the election parameters and recomputes the election fingerprint. The voter should verify that the fingerprint corresponds to the value published on the bulletin board. (This ensures that the script is using the trustees’ public key; in particular, it helps prevent encrypting a vote with an adversary’s public key. Such attacks have been discussed in the context of Direct Anonymous Attestation by Rudolph (Rudolph 2007); although, the vulnerability was discounted, in the trusted computing setting, by Leung, Chen & Mitchell (Leung, Chen, and Mitchell 2008).) 2. The voter inputs her vote $v\in\tilde {t}$ to the browser script, which creates a ballot consisting of her vote encrypted by the trustees’ public key, and a proof that the ballot represents a permitted vote (this is needed because the ballots are never decrypted individually, in particular, it prevents multiple votes being encoded as a single ballot). The ballot is displayed to the voter. 3. The voter can audit the ballot to check if it really represents a vote for her chosen candidate; if she decides to do this, then the script provides her with the random data used in the ballot creation. She can then independently reconstruct her ballot and verify that it is indeed well-formed. The script provides some practical resistance against vote selling by refusing to cast audited ballots. See Benaloh (Benaloh 2006, 2007) for further details on ballot auditing. 4. When the voter has decided to cast her ballot, the script submits it to the election officer. The election officer authenticates the voter and checks that she is eligible to vote. The election officer also verifies the proof and publishes the ballot, appended with the voter’s identity $id$, on the bulletin board. (In practice, the election officer also publishes the hash of the ballot, we omit this detail for brevity.) 5. Individual voters can check that their ballots appear on the bulletin board and, by verifying the proof, observers are assured that ballots represent permitted votes. 6. After some predefined deadline, the election officer homomorphically combines the ballots and publishes the encrypted tally on the bulletin board. Anyone can check that tallying is performed correctly. 7. Each of the trustees publishes a partial decryption of the encrypted tally, together with a signature of knowledge proving the partial decryption’s correct construction. Anyone can verify these proofs. 8. The election officer decrypts the tally and publishes the result. Anyone can check this decryption. Formally, Step [step:ballot] is defined in Figure [fig:ballot]. (For simplicity the ballot construction algorithm in Figure [fig:ballot] considers a vote $v\in\tilde {t}$, this can be generalised (Adida et al. 2009) to consider a vote $\tilde v \subseteq \tilde t$.) Checking voter eligibility (Step [step:submit]) is beyond the scope of Helios and Adida *et al.* (Adida et al. 2009) propose the use of existing infrastructure. The remaining steps follow immediately from the application of cryptographic primitives (see Section 2.1 for details).

Input: Cryptographic parameters (p, q, g), public key h, candidate list t̃ = (t1, …, tl) ∪ {ϵ} and vote v.

Output: Encrypted vote (a1, b1), …, (al, bl), signatures of knowledge (ā1, b̄1, c̄1, s̄1, ā′1, b̄′1, c̄′1, s̄′1), …, (āl, b̄l, c̄l, s̄l, ā′l, b̄′l, c̄′l, s̄′l) and signature of knowledge (ā, b̄, c̄, s̄, ā′, b̄′, c̄′, s̄′).

  1. If v ∉ t̃ then the script terminates.

  2. Encode the vote v as a bitstring. For all 1 ≤ i ≤ l, let $$m_i = \left\{\begin{array}{lcl} 1 &\quad& \textrm{if $v = t_i$}\\ 0 & & \textrm{otherwise} \end{array}\right.$$

  3. The bitstring representing the vote is encrypted. For all 1 ≤ i ≤ l, let (ai, bi) = (gri mod  p, gmi ⋅ hri mod  p) where ri∈Rℤq*.

  4. For all 1 ≤ i ≤ l, let (āi, b̄i, c̄i, s̄i, ā′i, b̄′i, c̄′i, s̄′i) be a signature of knowledge demonstrating that the ciphertext (ai, bi) contains either 0 or 1, that is, each candidate can receive at most one vote.

  5. Let (ā, b̄, c̄, s̄, ā′, b̄′, c̄′, s̄′) be a signature of knowledge demonstrating that the ciphertext (a1 ⋅ … ⋅ al, b1 ⋅ … ⋅ bl) contains either 0 or 1, that is, at most one candidate receives one vote.

Ballot construction by the browser script
## Software implementation Helios 3.0 is an extension of Helios 2.0 which adds numerous practical features, including: integration of authentication with various web-services (for example, Facebook, GMail and Twitter), bulk voter registration using pre-existing electoral rolls, and simplification of administration with multiple trustees. Helios 3.0 has been implemented and is publicly available: . # Attacking ballot secrecy Ballot secrecy means a voter’s vote is not revealed to anyone. We show that the Helios protocol does not satisfy this definition of ballot secrecy, by presenting an attack which allows an adversary to reveal a voter’s vote. Moreover, we will show that formal definitions of ballot secrecy (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2009; Backes, Hriţcu, and Maffei 2008) are also violated. Intuitively, an adversary may identify a voter’s ballot on the bulletin board (using the voter’s $id$) and recast this ballot by corrupting dishonest voters. The multiple occurrences of the voter’s ballot will leak information in the tally and the adversary can exploit this knowledge to violate the voter’s privacy. An informal description of the attack will now be presented in the case of three eligible voters and Section 3.3 considers a more realistic setting. (A formal analysis appears in Section 4.) ## Attack description Let us consider an election with candidates $t_1,\dots,t_l$ and three eligible voters who have identities $id_1$, $id_2$ and $id_3$. Suppose that voters $id_1$, $id_2$ are honest and $id_3$ is a dishonest voter controlled by the adversary. Further assume that the honest voters have cast their ballots. The bulletin board entries are as follows: $$\begin{array}{c} id_1, ciph_1, spk_1, spk'_1 \\ id_2, ciph_2, spk_2, spk'_2 \end{array}$$ where for $i\in\{1,2\}$ we have $$\begin{array}{lcl} ciph_i &=& (a_{i,1},b_{i,1}),\dots,(a_{i,l},b_{i,l}) \\ spk_i &=& (\bar a_{i,1},\bar b_{i,1},\bar c_{i,1},\bar s_{i,1},\bar a'_{i,1},\bar b'_{i,1},\bar c'_{i,1},\bar s'_{i,1}),\\ && \qquad \dots, (\bar a_{i,l},\bar b_{i,l},\bar c_{i,l},\bar s_{i,l},\bar a'_{i,l},\bar b'_{i,l},\bar c'_{i,l},\bar s'_{i,l})\\ spk'_i &=& (\bar a_i,\bar b_i,\bar c_i,\bar s_i, \bar a'_i,\bar b'_i,\bar c'_i,\bar s'_i) \end{array}$$ The value $ciph_i$ is the $i$th voter’s encrypted vote, $spk_i$ demonstrates that ciphertexts $(a_{i,1},b_{i,1}),\dots,(a_{i,l},b_{i,l})$ contain either $0$ or $1$, and $spk'_i$ demonstrates that $(a_{i,1} \cdot\ldots\cdot a_{i,l}, \; b_{i,1} \cdot\ldots\cdot b_{i,l})$ contains either $0$ or $1$. #### Exploiting the absence of ballot independence The adversary observes the bulletin board and selects $ciph_k,\allowbreak spk_k,\allowbreak spk'_k$ such that $id_k$ is the voter whose privacy will be compromised, where $k\in\{1,2\}$. The adversary submits the ballot $ciph_k,\allowbreak spk_k,\allowbreak spk'_k$ and it immediately follows that the bulletin board is composed as follows: $$\begin{array}{c} id_1, ciph_1, spk_1, spk'_1 \\ id_2, ciph_2, spk_2, spk'_2 \\ id_3, ciph_k, spk_k, spk'_k \\ \end{array}$$ It is trivial to see that each bulletin board entry represents a permitted vote; that is, $spk_1, spk'_1, spk_2, spk'_2, spk_k, spk'_k$ all contain valid signatures of knowledge. We have informally shown that Helios does not satisfy ballot independence (observing another voter’s interaction with the election system allows a voter to cast the *same* vote), and this will now be exploited to violate privacy. #### Violating privacy The homomorphic addition of ballots reveals the encrypted tally $(a_{1,1} \cdot a_{2,1} \cdot a_{k,1},\;b_{1,1} \cdot b_{2,1} \cdot b_{k,1}),\dots,(a_{1,l} \cdot a_{2,l} \cdot a_{k,l},\;b_{1,l} \cdot b_{2,l} \cdot b_{k,l})$ and, given the partial decryptions, these ciphertexts can be decrypted to reveal the number of votes for each candidate. Since there will be at least two votes for the candidate voter $id_k$ voted for, the voter’s vote can be revealed and hence privacy is not preserved. Moreover, the vote of the remaining honest voter will also be revealed. A video demonstrating the attack against the Helios 3.0 implementation has been produced (Smyth and Cortier 2010b). ## Variants exploiting malleability and key reuse In the aforementioned attack description, the ballots cast by two voters are identical which may result in the detection of an attack. For a covert attack, the adversary may prefer to cast a distinct ballot. This can be achieved by exploiting the malleability of ballots. In particular, given a valid ballot $$\begin{gathered} \label{ballotOne} (a_1,b_1),\dots,(a_l,b_l),\\ (\bar a_1,\bar b_1,\bar c_1,\bar s_1,\bar a'_1,\bar b'_1,\bar c'_1,\bar s'_1),\dots,\\ (\bar a_l,\bar b_l,\bar c_l,\bar s_l,\bar a'_l,\bar b'_l,\bar c'_l,\bar s'_l), \\ (\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s') \end{gathered}$$ the following ballots are also valid $$\begin{gathered} \label{ballotTwo} (a_1,b_1),\dots,(a_l,b_l),\\ (\bar a_1,\bar b_1,\bar c_1,\bar s_1+ q,\bar a'_1,\bar b'_1,\bar c'_1,\bar s'_1+ q),\dots,\\ (\bar a_l,\bar b_l,\bar c_l,\bar s_l+ q,\bar a'_l,\bar b'_l,\bar c'_l,\bar s'_l+ q), \\ (\bar a,\bar b,\bar c,\bar s+ q,\bar a',\bar b',\bar c',\bar s'+ q) \end{gathered}$$ $$\begin{gathered} \label{ballotThree} (a_{\pi(1)},b_{\pi(1)}),\dots,(a_{\pi(l)},b_{\pi(l)}),\\ (\bar a_{\pi(1)},\bar b_{\pi(1)},\bar c_{\pi(1)},\bar s_{\pi(1)},\bar a'_{\pi(1)},\bar b'_{\pi(1)},\bar c'_{\pi(1)},\bar s'_{\pi(1)}),\dots,\\ (\bar a_{\pi(l)},\bar b_{\pi(l)},\bar c_{\pi(l)},\bar s_{\pi(l)},\bar a'_{\pi(l)},\bar b'_{\pi(l)},\bar c'_{\pi(l)},\bar s'_{\pi(l)}), \\ (\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s') \end{gathered}$$ where $\pi$ is an arbitrary permutation over $\{1,\dots,l\}$. Ballot [ballotTwo] adds $q$ to the response components of Ballot [ballotOne], this changes the ballot but not the vote. (It is also possible to modify a subset of the response components.) However, this might be considered an implementation bug in Helios 3.0, rather than a theoretical attack, because the ballots are identical if considered as group elements. Replaying Ballot [ballotThree] has the advantage of casting a theoretical distinct ballot, since Ballot [ballotThree] represents a vote for a different candidate (with the exception of an abstention vote), and it is possible to compromise ballot secrecy in elections with three voters without abstention votes; however, more than one (modified) ballot may be required in elections with abstention votes. This variant of our attack also demonstrates a further violation of ballot independence in Helios: observing another voter’s interaction with the election system allows a voter to cast a *different* vote (for example, a voter can cast a distinct vote from their boss). Both variants of the attack are particularly useful when the bulletin board includes the hash of the ballot (for example, in the Helios 3.0 implementation), rather than the complete ballot, because the hashes will be distinct. An adversary may replay ballots in different elections, when the trustees’ public key is reused and the candidate lists for each election are of equal length. This variant of the attack can be avoided if distinct keys are used for each election. The variants of our attack in this section have all been successfully launched against the Helios 3.0 implementation. ## Generalised attack and French election case study Our attack demonstrates that the ballot of an arbitrary voter can be replayed by any other voter. In general, this does not reveal the voter’s vote; but, some information is leaked, and colluding voters can replay sufficiently many ballots to leak the voter’s vote. We will now discuss the feasibility of compromising ballot secrecy in a real-world election, focusing on the cost of an attack in French legislative elections, where each district elects a representative for the French National Assembly. Districts have several polling stations and each polling station individually announces its tally (“Article L65 of the French Electoral Code,” n.d.); these tallies are published in local newspapers. The publication of tallies is typical of French elections at all levels; for example, from the election of mayor, to the presidential election. In this (standard) voting configuration, an adversary can violate the ballot secrecy of a given voter by corrupting voters registered at the same polling station (for example, a coalition of neighbours or a family). The corrupted voters replay the ballot of the voter under attack, as previously explained. The motivation for restricting the selection of corrupted voters to the same polling station is twofold. Firstly, fewer corrupt voters are required to significantly influence the tally of an individual polling station (in comparison to influencing the election outcome). Secondly, it is unlikely to change the district’s elected representative, because a candidate will receive only a few additional votes in the district; it follows that coercing voters to sacrifice their vote, for the purposes of the attack, should be easier. In the remainder of this section, we discuss how many corrupt voters are required to violate ballot secrecy – by making a significant change in the tally of a polling station – in an arbitrary district of Aulnay-sous-Bois and a rural district in Toul. ### Ballot secrecy in Aulnay-sous-Bois Using historic data and/or polls, it is possible to construct the expected distribution of votes. For simplicity, let us assume the distribution of votes per polling station is the average of the 2010 tally (Table 1), and that if the adversary can increase the number of votes for a particular candidate by more than $\sigma$ (by replaying a voter’s ballot), then this is sufficient to determine that the voter voted for that candidate. In addition, suppose that the adversary corrupts abstaining voters and therefore we do not consider the redistribution of votes. We remark that corrupting abstaining voters may be a fruitful strategy, since abstaining voters do not sacrifice their vote by participating in an attack.
| Party | Tally | |:---------------------|------:| | PS | 4120 | | UMP | 3463 | | FN | 1933 | | Europe Eco. | 1921 | | Front de gauche | 880 | | NPA | 697 | | MODEM | 456 | | Debout la République | 431 | | Alliance école | 193 | | LO | 156 | | Émergence | 113 | | Liste chrétienne | 113 | 2010 legislative election results in Aulnay-sous-Bois (“Résultat par bureau du premier tour des élections régionales” 2010)
Table [table:::] presents the expected distribution of votes, and includes the number of voters that an adversary must corrupt to determine if a voter voted for a particular candidate, for various values of $\sigma$. We shall further assume that participation in the region is consistent with 2010; that is, 291 of the 832 eligible voters are expected to participate. It follows that $50$ voters corresponds to approximately $6\%$ of the Aulnay-sous-Bois electorate, and $10$ voters corresponds to approximately $1\%$. Our results therefore demonstrate that the privacy of a voter can be compromised by corrupting a small number of voters. In particular, for medium-size parties (in terms of votes received) – including, for example, FN and Europe Ecologie – it is sufficient to corrupt 19 voters to see the number of votes increase by 50%. Furthermore, given the low turn-out (541 voters are expected to abstain), it seems feasible to corrupt abstaining voters, and therefore an attack can be launched without any voter sacrificing their vote.
| Party | Expected tally | $\sigma = 200\%$ | $\sigma = 150\%$ | $\sigma = 50\%$ | $\sigma = 20\%$ | |:---------------------|---------------:|-----------------:|-----------------:|----------------:|----------------:| | PS | 81 | 162 | 122 | 41 | 17 | | UMP | 68 | 136 | 102 | 34 | 14 | | FN | 38 | 76 | 57 | 19 | 8 | | Europe Eco. | 38 | 76 | 57 | 19 | 8 | | Front de gauche | 17 | 34 | 26 | 9 | 4 | | NPA | 14 | 28 | 21 | 7 | 3 | | MODEM | 9 | 18 | 14 | 5 | 2 | | Debout la République | 8 | 16 | 12 | 4 | 2 | | Alliance école | 4 | 8 | 6 | 2 | 1 | | LO | 3 | 6 | 5 | 2 | 1 | | Émergence | 2 | 4 | 3 | 1 | 1 | | Liste chrétienne | 2 | 4 | 3 | 1 | 1 |
#### Limitations For such an attack based on a statistical model, we acknowledge that this model is rather naïve, but believe it is sufficiently indicative to illustrate the real threat of an attack against privacy. A definitive mathematical analysis should be considered in the future. #### Cases of complete privacy breach The probabilistic nature of these attacks may introduce sufficient uncertainty to prevent privacy violations, and we will consider voting configurations where an adversary can definitively learn a voter’s vote. Observe that if an attacker can corrupt half of the voters at a polling station, then the vote of an arbitrary voter can be revealed. Moreover, the cost of this attack can be reduced. In particular, if $n$ dishonest voter’s replay voter $\mathcal{V}$’s ballot, then it is possible to deduce that $\mathcal{V}$ did not vote for any candidate that received strictly less than $n+1$ votes. This leaks information about voter $\mathcal{V}$’s chosen candidate and in cases where exactly one candidate received more than $n$ votes, the voter’s vote can be deduced. ### Ballot secrecy in small polling stations The difficulties of large scale corruption may prohibit our attack in the majority of polling stations; however, our attack is feasible in small polling stations found in rural districts. For example, let us consider the 2007 legislative elections in the district of Toul (“Est Républicain” 2007). This district has 75350 eligible voters registered at 193 polling stations. Accordingly, the average polling station has 390 registered voters, but the variance is large. Indeed, 33 polling stations have between 50 and 99 voters, 9 polling stations have less then 50 voters, and the smallest two polling stations have 8, respectively 16, voters. Moreover, the attack is simplified by non-participating voters. In these small polling stations it is thus sufficient to corrupt a very small number of voters to reveal a voter’s vote while the final outcome of the election would not change as it is based on 75350 eligible voters. # Solution: Weeding replayed ballots Our attack exploits the possibility of replaying a voter’s ballot without detection, and can be attributed to the lack of ballot independence in Helios. This section sketches some possible solutions to ensure ballot independence. ## Weeding replayed ballots The ballots replayed in our attacks can all be identified. First, ciphertexts and signatures of knowledge should have a unique representation as group elements, for example, by requiring that the response component of signatures of knowledge is in the interval $[0,q-1]$. Second, a ballot should not contain a ciphertext that already exists on the bulletin board. The election officer should reject ballots that do not satisfy these conditions. This solution is simple and can easily be implemented in a future version of Helios. ## Binding ballots to voters The previous approach requires a special mechanism to handle replayed ballots. We now propose a technique that makes such actions futile. In essence, based upon inspiration from (Gennaro 1995, sec. 4.2) and (Cramer, Gennaro, and Schoenmakers 1997), we ensure that proofs associated with replayed ballots are considered invalid; that is, we bind the link between a voter and her ballot. This is achieved by adding the identity of the voter in the construction of challenges used by signatures of knowledge. More precisely, for voter $id$, the sign algorithm (defined in Appendix 6.1) is modified as follows: on input $(a,b)$, such that $a\equiv g^r \bmod p$ and $b\equiv h^r \cdot g^m \bmod p$, let challenge $c_m = \mathcal{H}(a_{\sf min},b_{\sf min},\dots,a_{\sf max},b_{\sf max},id) - \sum_{i\in\{{\sf min},\dots,m-1,m+1,\dots,{\sf max}\}} c_i \pmod q$, where values $a_{\sf min},\allowbreak b_{\sf min},\dots,a_{\sf max},b_{\sf max}$ and $c_1,\dots,c_{m-1},c_{m+1},\dots,c_m$ are defined as before. For correctness, the verification algorithm must also be modified. In particular, for candidate signatures constructed by voter $id$, the verifier should check $\mathcal{H}(a_{\sf min},b_{\sf min},\dots,a_{\sf max},b_{\sf max},id) \equiv \sum_{{\sf min}\leq i \leq {\sf max}} c_i \pmod q$. In a similar direction, the electronic voting protocol proposed by Juels, Catalano & Jakobsson (Juels, Catalano, and Jakobsson 2005) – which has been implemented by Clarkson, Chong & Myers (Clarkson, Chong, and Myers 2008, 2007) as Civitas – requires ballots to be bound to private voter credentials. This provides *eligibility verifiability* (Kremer, Ryan, and Smyth 2010): anyone can check that each ballot published on the bulletin board was cast by a registered voter and at most one ballot is tallied per voter. It is likely that eligibility verifiability enforces ballot independence, but the provision of eligibility verifiability appears to be expensive, in particular, Juels, Catalano & Jakobsson and Clarkson, Chong & Myers assume the existence of an infrastructure for voter credentials. ## Discussion Our *weeding replayed ballots* solution is particular attractive because it adheres to Benaloh’s notion of *ballot casting assurance* (Benaloh 2006, 2007) which asserts that the ballot encryption device (the browser script in this instance) does not know the voter’s identity. (We remark that neither the original Helios scheme nor our proposed fix strictly satisfy Benaloh’s notion of ballot casting assurance if a voter decides to use her own computer.) The ballot casting assurance principle is important because knowledge of the voter’s identity could be used to infer the likelihood of auditing and this information can be used to influence the behaviour of the ballot encryption device; in particular, if a ballot is unlikely to be audited, then the device may act maliciously, for example, by encrypting a different vote. By comparison, the *binding ballots to voters* solution would necessarily require that the voter’s identity is revealed to the ballot encryption device. Moreover, for privacy purposes, the election officer may chose to allocate voters with pseudo-identities when casting ballots (rather than associate ballots with actual voter identities); since these pseudo-identities are unknown to voters in advance, an additional interaction with the election officer would be required. (Note that the use of pseudo-identities does not prevent the attack by breaking the link between ballots and voters, because the link is known by the election officer.) Finally, extending Helios to provide eligibility verifiability would require a considerable extension to the Helios code-base and, furthermore, finding a suitable solution is an open problem. Accordingly, we adopt the weeding replayed ballot solution and, in the next section, we show that this is sufficient to ensure ballot secrecy, in the formal setting. # Formal proof of ballot secrecy We formally prove that weeding duplicate ballots ensures ballot secrecy. We make use of the applied pi calculus (Abadi and Fournet 2001; M. D. Ryan and Smyth 2011), due to its proven suitability for evaluating security properties of electronic voting protocols (see, for example, (Delaune, Kremer, and Ryan 2009; Backes, Hriţcu, and Maffei 2008; Kremer, Ryan, and Smyth 2010)). ## Applied pi calculus We first recall the applied pi calculus setting (Abadi and Fournet 2001). We assume an infinite set of *names* $a,b,c,\ldots,\allowbreak k,\ldots,\allowbreak m,n,\ldots,\allowbreak s,\ldots$, an infinite set of *variables* $x,y,z,\ldots$, and a *signature* $\Sigma$ consisting of a finite set of *function symbols*, each with an associated arity. We use metavariables $u,w$ to range over both names and variables. *Terms* $L,M,N,T,U,V$ are built by applying function symbols to names, variables, and other terms. We write $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ for the *substitution* that replaces the variable $x$ with the term $M$. Arbitrarily large substitutions can be written as $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}},\ldots,\textnormal{\raisebox{2pt}{\footnotesize $M_l$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_l$}}\}$ and the letters $\sigma$ and $\tau$ range over substitutions. We write $N\sigma$ for the result of applying $\sigma$ to the free variables of term $N$. A term is *ground* when it does not contain variables. The signature $\Sigma$ is equipped with an *equational theory* $E$, that is, a set of equations of the form $M = N$, where the terms $M,N$ are defined over the signature $\Sigma$. We define equality modulo the equational theory, written $=_E$, as the smallest equivalence relation on terms that contains $E$ and is closed under application of function symbols, substitution of terms for variables and bijective renaming of names. We write $M =_EN$ when the equation $M = N$ is in the theory $E$, and keep the signature implicit. When $E$ is clear from its usage, we may abbreviate $M =_EN$ as $M = N$. The negation of $M =_EN$ is denoted $M \not=_EN$ (and similarly abbreviated $M \not= N$). *Processes* and *extended processes* are defined in the usual way (Figure 2). We write $\nu\,\tilde{u}$ for the (possibly empty) series of pairwise-distinct binders $\nu\,u_1.\cdots.\nu\,u_l$. The active substitution $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ can replace the variable $x$ for the term $M$ in every process it comes into contact with and this behaviour can be controlled by restriction, in particular, the process $\nu\,x.(\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \mid P)$ corresponds exactly to $\textnormal{let } x=M \textnormal{ in }P$. Arbitrarily large active substitutions can be obtained by parallel composition and we occasionally abbreviate $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}}\}\mid\ldots\mid\{\textnormal{\raisebox{2pt}{\footnotesize $M_l$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_l$}}\}$ as $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}},\ldots,\textnormal{\raisebox{2pt}{\footnotesize $M_l$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_l$}}\}$ or $\{\textnormal{\raisebox{2pt}{\footnotesize $\tilde{M}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $\tilde{x}$}}\}$. We also use $\sigma$ and $\tau$ to range over active substitutions, and write $N\sigma$ for the result of applying $\sigma$ to the free variables of $N$. Extended processes must have at most one active substitution for each variable and there is exactly one when the variable is under restriction. The only minor change compared to (Abadi and Fournet 2001) is that conditional branches now depend on formulae $\phi,\psi \mathrel{::=} M \mathrel= N \mid M \mathrel{\not=} N \mid \phi \mathrel\wedge \psi$. If $M$ and $N$ are ground, we define $[\! [ M=N ]\! ]$ to be $\mathsf{true}$ if $M=_E N$ and $\mathsf{false}$ otherwise. The semantics of $[\! [ \ ]\! ]$ is then extended to formulae in the standard way.

XXX̄XXXXXXXXXXXXXXXxxX̄X̄ P, Q, R : := (plain) processes
0 null process
P ∣ Q parallel composition
!P replication
ν n.P name restriction
$\textnormal{if } \phi \textnormal{ then } P \textnormal{ else }Q$ conditional
u(x).P message input
$\overline{u}\langle M\rangle.P$ message output

A, B, C : := extended processes
P plain process
A ∣ B parallel composition
ν n.A name restriction
ν x.A variable restriction
$\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ active substitution

Syntax for processes
The *scope* of names and variables are delimited by binders $u(x)$ and $\nu\,u$. The set of bound names is written $\textnormal{bn}(A)$ and the set of bound variables is written $\textnormal{bv}(A)$; similarly we define the set of free names $\textnormal{fn}(A)$ and free variables $\textnormal{fv}(A)$. Occasionally, we write $\textnormal{fn}(M)$ (and $\textnormal{fv}(M)$ respectively) for the set of names (and respectively variables) which appear in term $M$. An extended process is *closed* when every variable $x$ is either bound or defined by an active substitution. We define a *context* $C[\_]$ to be an extended process with a hole. We obtain $C[A]$ as the result of filling $C[\_]$’s hole with the extended process $A$. An *evaluation context* is a context whose hole is not in the scope of a replication, a conditional, an input, or an output. A context $C[\_]$ closes $A$ when $C[A]$ is closed. A *frame*, denoted $\varphi$ or $\psi$, is an extended process built from the null process $0$ and active substitutions $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$, which are composed by parallel composition and restriction. The *domain* $\textnormal{dom}(\varphi)$ of a frame $\varphi$ is the set of variables that $\varphi$ exports, that is, the set of variables $x$ for which $\varphi$ contains an active substitution $\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$ such that $x$ is not under restriction. Every extended process $A$ can be mapped to a frame $\varphi(A)$ by replacing every plain process in $A$ with $0$. ### Operational semantics The operational semantics are defined by three relations: *structural equivalence* ($\equiv$), *internal reduction* ($\xrightarrow{}$), and *labelled reduction* ($\xrightarrow{\alpha}$). These relations satisfy the rules in Figure 3 and are defined such that: structural equivalence is the smallest equivalence relation on extended processes that is closed by $\alpha$-conversion of both bound names and bound variables, and closed under application of evaluation contexts; internal reduction is the smallest relation on extended processes closed under structural equivalence and application of evaluation contexts; and for labelled reductions $\alpha$ is a *label* of the form $c(M),$ $\overline{c}\langle u\rangle,$ or $\nu\,u.\overline{c}\langle u\rangle$ such that $u$ is either a channel name or a variable of base type.

$$\begin{array}{lrcl} {\ensuremath{\mbox{\sc Par-0}}}& A & \equiv & A \mid 0\\ {\ensuremath{\mbox{\sc Par-A}}}& A\mid(B \mid C) & \equiv & (A \mid B) \mid C \\ {\ensuremath{\mbox{\sc Par-C}}}& A \mid B & \equiv & B \mid A \\ {\ensuremath{\mbox{\sc Repl}}}& !P & \equiv & P \mid {!P} \\ \\ {\ensuremath{\mbox{\sc New-0}}}& \nu\,n.0& \equiv & 0\\ {\ensuremath{\mbox{\sc New-C}}}& \nu\,u.\nu\,w.A & \equiv & \nu\,w.\nu\,u.A \\ {\ensuremath{\mbox{\sc New-Par}}}& A\mid\nu\,u.B & \equiv & \nu\,u.(A \mid B) \\ & & & \textrm{where } u\not\in \textnormal{fv}(A) \cup \textnormal{fn}(A)\\ \\ {\ensuremath{\mbox{\sc Alias}}}& \nu\,x.\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}& \equiv & 0\\ {\ensuremath{\mbox{\sc Subst}}}& \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \mid A & \equiv & \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \mid A\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \\ {\ensuremath{\mbox{\sc Rewrite}}}& \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} & \equiv & \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \\ & & & \textrm{where } M =_EN \\ \end{array}$$

XXXXXXx̄̄ ${\ensuremath{\mbox{\sc Comm}}}$ $\overline{c}\langle x\rangle.P\mid c(x).Q \xrightarrow{}P \mid Q$
${\ensuremath{\mbox{\sc Then}}}$ $\textnormal{if } \phi \textnormal{ then } P \textnormal{ else }Q \xrightarrow{}P$  if [ [ϕ] ] = true
${\ensuremath{\mbox{\sc Else}}}$ $\textnormal{if } \phi \textnormal{ then } P \textnormal{ else }Q \xrightarrow{}Q$  otherwise

$$\begin{array}{l} {\ensuremath{\mbox{\sc In}}}\quad c(x).P \xrightarrow{c(M)} P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \\[0.2cm] {\ensuremath{\mbox{\sc Out-Atom}}}\quad \overline{c}\langle u\rangle.P \xrightarrow{\overline{c}\langle u\rangle} P \\[0.2cm] {\ensuremath{\mbox{\sc Open-Atom}}}\quad \dfrac{A \xrightarrow{\overline{c}\langle u\rangle} A' \qquad u \not= c} {\nu\,u.A \xrightarrow{\nu\,u.\overline{c}\langle u\rangle} A'} \\[0.5cm] {\ensuremath{\mbox{\sc Scope}}}\quad \dfrac{A \xrightarrow{\alpha} A' \qquad \textrm{$u$ does not occur in $\alpha$}} {\nu\,u.A \xrightarrow{\alpha} \nu\,u.A'} \\[0.5cm] {\ensuremath{\mbox{\sc Par}}}\quad \dfrac{A \xrightarrow{\alpha} A' \qquad \textnormal{bv}(\alpha) \cap \textnormal{fv}(B) = \textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset} {A \mid B \xrightarrow{\alpha} A' \mid B} \\[0.5cm] {\ensuremath{\mbox{\sc Struct}}}\quad \dfrac{A \equiv B \qquad B \xrightarrow{\alpha} B' \qquad B' \equiv A'} {A \xrightarrow{\alpha} A'} \end{array}$$

Semantics for processes
### Equivalence The definition of observational equivalence (Abadi and Fournet 2001) quantifies over all contexts which makes proofs difficult, therefore we adopt labelled bisimilarity in this paper. Labelled bisimilarity relies on an equivalence relation between frames, called static equivalence.
**Definition 1** (Static equivalence). *Two closed frames $\varphi$ and $\psi$ are statically equivalent, denoted $\varphi \approx_s \psi$, if $\textnormal{dom}(\varphi) = \textnormal{dom}(\psi)$ and there exists a set of names $\tilde n$ and substitutions $\sigma,\tau$ such that $\varphi\equiv \nu\,\tilde{n}.\sigma$ and $\psi \equiv \nu\,\tilde{n}.\tau$ and for all terms $M,N$ such that $\tilde{n} \cap (\textnormal{fn}(M) \cup \textnormal{fn}(N)) = \emptyset$, we have $M\sigma =_EN\sigma$ holds if and only if $M\tau =_EN\tau$ holds. Two closed extended processes $A,B$ are statically equivalent, written $A \approx_s B$, if their frames are statically equivalent; that is, $\varphi(A) \approx_s \varphi(B)$.*
The relation $\approx_s$ is called *static* equivalence because it only examines the current state of the processes, and not the processes’ dynamic behaviour. The following definition of labelled bisimilarity captures the dynamic part.
**Definition 2** (Labelled bisimilarity). *Labelled bisimilarity ($\approx_l$) is the largest symmetric relation $\mathcal{R}$ on closed extended processes such that $A \mathrel{\mathcal{R}}B$ implies:* 1. *$A \approx_s B$;* 2. *if $A \xrightarrow{}A'$, then $B \xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$;* 3. *if $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then $B\xrightarrow{}^*\xrightarrow{\alpha}\xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$.*
## Modelling Helios in applied pi We start by constructing a suitable signature $\Sigma$ to capture the cryptographic primitives used by Helios and define an equational theory $E$ to capture the relationship between these primitives. ### Signature We adopt the following signature. $$\begin{gathered} \Sigma = \{\mathsf{ok},\mathsf{zero},\mathsf{one},\perp,\mathsf{fst},\mathsf{snd},\mathsf{pair},*,+,\circ,\\\mathsf{partial},\mathsf{checkspk},\mathsf{penc},\mathsf{spk},\} \end{gathered}$$ Functions $\mathsf{ok},\mathsf{zero},\mathsf{one},\perp$ are constants; $\mathsf{fst},\mathsf{snd}$ are unary functions; $\mathsf{dec},\mathsf{pair},\mathsf{partial},*,+,\circ$ are binary functions; $\mathsf{checkspk},\mathsf{penc}$ are ternary functions; and $\mathsf{spk}$ is a function of arity four. We adopt infix notation for $*,+$, and $\circ$. The term $\mathsf{penc}(T,N,M)$ denotes the encryption of plaintext $M$, using random nonce $N$ and key $T$. The term $U*U'$ denotes the homomorphic combination of ciphertexts $U$ and $U'$, the corresponding operation on plaintexts is written $M\mathrel+M'$ and $N\mathrel\circ N'$ on nonces. The partial decryption of ciphertext $U$ using key $L$ is denoted $\mathsf{partial}(L,U)$. The term $\mathsf{spk}(T,N,M,U)$ represents a signature of knowledge that proves $U$ is a ciphertext under public key $T$ on the plaintext $M$ using nonce $N$ and such that $M$ is either the constant $\mathsf{zero}$ or $\mathsf{one}$. We introduce tuples using pairings and, for convenience, $\mathsf{pair}(M_1, \mathsf{pair}(\dots, \mathsf{pair}(M_n, \perp)))$ is occasionally abbreviated as $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{M_1,\dots,M_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, and $\mathsf{fst}(\mathsf{snd}^{i-1}(M))$ is denoted $\pi_{i}(M)$, where $i\in\mathbb{N}$. We use the equational theory $E$ that asserts functions $+,*,\circ$ are commutative and associative, and includes the equations: $$\begin{aligned} &&\hspace{-11mm}\mathsf{fst}(\mathsf{pair}(x, y)) = x \label{eq:proj1}\\[0.3em] % &&\hspace{-11mm}\mathsf{snd}(\mathsf{pair}(x, y)) = y\label{eq:proj2}\\[0.3em] % %\>\sout{$\true \wedge \true = \true$}\\[1em] % &&\hspace{-11mm}\mathsf{zero}+ \mathsf{one}= \mathsf{one}\label{eq:addition}\\[0.3em] %%Needed to make signature proof of knowledge work. % &&\hspace{-11mm}\mathsf{dec}(x_{\mathsf{sk }},\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }})) = x_{\mathsf{plain }}\label{eq:dec}\\[0.3em] % &&\hspace{-11mm}\mathsf{dec}(\mathsf{partial}(x_{\mathsf{sk }},ciph),ciph) = x_{\mathsf{plain }}\label{eq:partial}\\ &&\hspace{-11mm}\text{ where } ciph=\mathsf{penc}(\mathsf{pk}(x_{\mathsf{sk }}),x_{\mathsf{rand }},x_{\mathsf{plain }}) \nonumber\\[0.3em] % &&\hspace{-11mm}\mathsf{penc}(x_{\mathsf{pk }},y_{\mathsf{rand }},y_{\mathsf{plain }})*\mathsf{penc}(x_{\mathsf{pk }},z_{\mathsf{rand }},z_{\mathsf{plain }}) \nonumber\\ &&\hspace{-11mm}\qquad=\mathsf{penc}(x_{\mathsf{pk }},y_{\mathsf{rand }}\circ z_{\mathsf{rand }},y_{\mathsf{plain }}+z_{\mathsf{plain }})\label{eq:combination}\\[0.3em] % &&\hspace{-11mm}\mathsf{checkspk}(x_{\mathsf{pk }},ball,\mathsf{spk}(x_{\mathsf{pk }},x_{\mathsf{rand }},\mathsf{zero},ball)\!) \!=\! \mathsf{ok}\label{eq:spk0}\\ &&\hspace{-11mm}\text{ where } ball=\mathsf{penc}(x_{\mathsf{pk }},x_{\mathsf{rand }},\mathsf{zero}) \nonumber\\[0.3em] % &&\hspace{-11mm}\mathsf{checkspk}(x_{\mathsf{pk }},ball,\mathsf{spk}(x_{\mathsf{pk }},x_{\mathsf{rand }},\mathsf{one},ball)\!) \!=\! \mathsf{ok}\label{eq:spk1}\\ &&\hspace{-11mm}\text{ where } ball=\mathsf{penc}(x_{\mathsf{pk }},x_{\mathsf{rand }},\mathsf{one}) \nonumber \end{aligned}$$ Equation [eq:partial] allows plaintext $M$ to be recovered from ciphertext $\mathsf{penc}(\mathsf{pk}(L),N,M)$ given partial decryption $\mathsf{partial}(L,\mathsf{penc}(\mathsf{pk}(L),N,M))$, when the partial decryption is constructed using the private key $L$. Equation [eq:combination] represents the homomorphic combination of ciphertexts. The Equations [eq:spk0] and [eq:spk1] allow the verification of signatures of knowledge $\mathsf{spk}(T,N,M,\mathsf{penc}(T,N,M))$, when $M\in\{\mathsf{zero},\mathsf{one}\}$. The remaining equations are standard.
**Example 1**. *Given randomness $N,N'$, plaintexts $(M,M')\in\{(\mathsf{zero},\mathsf{zero}),(\mathsf{zero},\mathsf{one}),(\mathsf{one},\mathsf{zero})\}$, and public key $T$, one can construct a signature of knowledge $L = \mathsf{spk}(T,N \circ N',M + M',\mathsf{penc}(T,N,M)*\mathsf{penc}(T,N',M'))$. Then $\mathsf{checkspk}$ applied to the public key $T$, the homomorphically combined ciphertexts $\mathsf{penc}(T,N,M)*\mathsf{penc}(T,N',M')$, and the signature $L$ is equal to $\mathsf{ok}$ using Equations [eq:addition], [eq:combination], [eq:spk0], and [eq:spk1]*
### Helios process specification In the applied pi calculus, it is sufficient to model the parts of the voting system which need to be trusted for ballot secrecy; all the remaining parts of the system are controlled by the adversarial environment. Accordingly, we assume the existence of at least two honest voters $\mathcal A$, $\mathcal B$; since this avoids the scenario where ballot secrecy of an individual voter is compromised by collusion amongst all the remaining voters. In addition, the following trust assumptions are required. - At least one trustee is honest - The election officer runs the bulletin board honestly: - Voters $\mathcal A$, $\mathcal B$ have authentic channels with the bulletin board - Signatures of knowledge are checked for dishonest voters\* - Replays of honest ballots (that is, those cast by $\mathcal A$ or $\mathcal B$) are rejected\* - The tally is correctly computed\* - The trustees have an authentic channel with the bulletin board - The browser script is trusted and has the correct public key of the election (Assumptions marked with \* could be performed by an honest trustee, rather than the bulletin board.) Although neither voters nor observers can verify that there exists an honest trustee, an assurance of trust is provided by distribution. The necessity to trust the election officer to run the bulletin board is less desirable and work-in-progress (Pereira, Adida, and Marneffe 2010) aims to weaken this assumption; moreover, to further distribute trust assumptions, the trustees could also check signatures and tallying. Finally, trust in the browser script can be obtained by using software written by a reputable source or writing your own code. In an election with two candidates, the trusted components are modelled by the administration process $A^{\phi}_n$ and voting process $V$ defined in Figure 4. For generality, the administration process $A^{\phi}_n$ is parametrised by the number of voters $n$ and a formula $\phi$; the latter corresponds to the checks performed by the bulletin board before accepting a ballot. We will consider several variants of Helios (including the original Helios 2.0 protocol and our fixed scheme) by considering suitable formula that we call *Helios process specifications*.

Given the number of voters n ≥ 2 and Helios process specification ϕ, the administration process Anϕ and voting process V are defined below $$\begin{array}{ll} V =& \nu\,r \mathrel.\\ & \textnormal{let } ciph=\mathsf{penc}(z_{\mathsf{pk }},r,x_{\mathsf{vote} }) \textnormal{ in }\\ & \textnormal{let } spk=\mathsf{spk}(z_{\mathsf{pk }},r,x_{\mathsf{vote} },ciph)) \textnormal{ in }\\ & \nu\,r' \mathrel.\\ & \textnormal{let } ciph'=\mathsf{penc}(z_{\mathsf{pk }},r',x_{\mathsf{vote} }') \textnormal{ in }\\ & \textnormal{let } spk'=\mathsf{spk}(z_{\mathsf{pk }},r',x_{\mathsf{vote} }',ciph')) \textnormal{ in }\\ &\textnormal{let } \widehat{spk}=\mathsf{spk}(z_{\mathsf{pk }},r\circ r',x_{\mathsf{vote} }+x_{\mathsf{vote} }',ciph * ciph') \textnormal{ in }\\ &\overline{x_{\mathsf{auth }}}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{ciph,ciph',spk,spk',\widehat{spk}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\ \\ A^{\phi}_n=& \nu\,sk_T,a_1,a_2,d\mathrel.(\_ \mid BB^{\phi}_n\mid T \mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\})\\ \end{array}$$ $$\begin{array}{lcl} BB^{\phi}_n& = & a_1(y_1)\mathrel.\overline{c}\langle y_1\rangle\mathrel.a_2(y_2)\mathrel.\overline{c}\langle y_2\rangle\mathrel.\\ && a_{3}(y_{3})\mathrel. \textnormal{if } \phi\{\textnormal{\raisebox{2pt}{\footnotesize $y_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\} \textnormal{ then } %\textrm{\sout{$\BBIfI{y_3}{y_1}{y_2}$}}} \\ && \cdots\ a_{n}(y_{n})\mathrel. \textnormal{if } \phi\{\textnormal{\raisebox{2pt}{\footnotesize $y_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\} \textnormal{ then } %\textrm{\sout{$\BBIfI{y_n}{y_1}{y_2}$}}} \\ && \textnormal{let } tally=\pi_{1}(y_1) *\allowbreak \dots *\allowbreak \pi_{1}(y_n) \textnormal{ in }\\ && \textnormal{let } tally'=\pi_{2}(y_1) *\allowbreak \dots *\allowbreak \pi_{2}(y_n) \textnormal{ in }\\ && \overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{tally,tally'}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\mathrel.\\ && d(y_{\mathsf{partial }})\mathrel.\\ && \overline{c}\langle y_{\mathsf{partial }}\rangle\mathrel.\\ && \overline{c}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{dec}(\pi_{1}(y_{\mathsf{partial }}),tally),\mathsf{dec}(\pi_{2}(y_{\mathsf{partial }}),tally')}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\ \\ T & = & d(y_{\mathsf{tally} })\mathrel.\\ &&\overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{partial}(sk_T,\pi_{1}(y_{\mathsf{tally} })),\mathsf{partial}(sk_T,\pi_{2}(y_{\mathsf{tally} }))}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle \end{array}$$

Helios process specification
**Definition 3** (Helios process specification). *A formula $\phi$ is a *Helios process specification*, if $\textnormal{fv}(\phi) \subseteq \{y_1,\allowbreak y_2,\allowbreak y_{\mathsf{ballot }},\allowbreak z_{\mathsf{pk }}\}$.*
The voting process $V$ contains free variables $x_{\mathsf{vote} },x_{\mathsf{vote} }'$ to represent the voter’s vote (which is expected to be encoded as constants $\mathsf{zero}$ and $\mathsf{one}$), and the free variable $x_{\mathsf{auth }}$ represents the channel shared by the voter and the bulletin board. The definition of the process $V$ corresponds to the description of the browser script (Figure 1). The administration process $A^{\phi}_n$ is parametrised by the number of voters $n$ and Helios process specification $\phi$. The restricted name $sk_T$ models the tallier’s secret key and the public part $\mathsf{pk}(sk_T)$ is included in the process’s frame. The restricted names $a_1,a_2$ model authentic channels between the two honest voters and the bulletin board, and the channel name $d$ captures the authentic channel with the honest trustee. To ensure the adversary has access to messages sent on private channels, communication is relayed on the public channel $c$. The sub-process $BB^{\phi}_n$ represents the bulletin board and $T$ represents the tallier. The bulletin board accepts ballots from each voter and checks they are valid using the Helios process specification $\phi$ (this predicate will be discussed in more detail below). Once all ballots have been submitted, the bulletin board homomorphically combines the ciphertexts and sends the encrypted tallies to the tallier for decryption. (The necessity for all voters to participate is included for simplicity, in particular, our bulletin board does not weed ballots containing invalid proofs.) The tallier receives the homomorphic combinations of ballots $y_{\mathsf{tally} }$ and derives a partial decryption for each candidate; these partial decryptions are sent to the bulletin board and the election result is published.
**Example 2**. *Given a Helios process specification $\phi$, an election with voters $\mathcal{A}$ and $\mathcal{B}$ who select votes $(m_1,m'_1),\allowbreak(m_2,m'_2)\in\{(\mathsf{zero},\mathsf{zero}),\allowbreak(\mathsf{zero},\mathsf{one}),\allowbreak(\mathsf{one},\mathsf{zero})\}$ and such that the other $n-2$ voters are controlled by the adversary, can be modelled by the process $A^\phi_n[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]$, where $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $m_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\textnormal{\raisebox{2pt}{\footnotesize $m'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $m_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $m'_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$.*
#### Ballot validity In Helios 2.0, the election officer considers a ballot to be valid if the signature proofs of knowledge hold. Accordingly, we can model the Helios administration by the process $A^{\phi_{\sf orig}}_n$ where the Helios process specification $\phi_{\sf orig}$ is defined as follows. $$\begin{gathered} \phi_{\sf orig}\triangleq \mathsf{checkspk}(z_{\mathsf{pk }},\pi_{1}(y_{\mathsf{ballot }}),\pi_{3}(y_{\mathsf{ballot }})) = \mathsf{ok}\\ \mathrel\wedge \mathsf{checkspk}(z_{\mathsf{pk }},\pi_{2}(y_{\mathsf{ballot }}),\pi_{4}(y_{\mathsf{ballot }})) = \mathsf{ok}\\ \mathrel\wedge \mathsf{checkspk}(z_{\mathsf{pk }},\pi_{1}(y_{\mathsf{ballot }}) * \pi_{2}(y_{\mathsf{ballot }}),\pi_{5}(y_{\mathsf{ballot }})) = \mathsf{ok} \end{gathered}$$ We have shown that these checks are insufficient to ensure ballot secrecy. Our weeding replayed ballots solution proposed in Section 4.1 additionally requires that the ciphertexts inside the ballot do not appear on the bulletin board. This revised scheme can be modelled using the Helios process specification $\phi_{\sf sol}$ is defined as follows. $$\begin{gathered} \phi_{\sf sol}\triangleq \phi_{\sf orig}\wedge \pi_{6}(y_{\mathsf{ballot }}) = \perp \mathrel\wedge \\ \bigwedge_{i,j\in\{1,2\}} \pi_{i}(y_j) \not= \pi_{1}(y_{\mathsf{ballot }}) \wedge \pi_{i}(y_j) \not= \pi_{2}(y_{\mathsf{ballot }}) \end{gathered}$$ We can also model a naïve solution that would consist in weeding only identical ballots by considering the Helios process specification $\phi_{\sf ident}$ defined below. $$\phi_{\sf ident}\triangleq \phi_{\sf orig}\mathrel\wedge \pi_{6}(y_{\mathsf{ballot }}) = \perp \mathrel\wedge y_{\mathsf{ballot }}\not= y_1 \mathrel\wedge y_{\mathsf{ballot }}\not= y_2$$ We have already shown that removing exact duplicates is insufficient because it would fail to detect variants of our attack whereby the contents of a ballot are permuted. In the next section, we formally show that Helios 2.0 (modelled using $\phi_{\sf orig}$) and the naïve solution (modelled using $\phi_{\sf ident}$) do not satisfy ballot secrecy, and that our proposed solution (modelled using $\phi_{\sf sol}$) does satisfy ballot secrecy. ## Formal analysis: Ballot secrecy Based upon Delaune, Kremer & Ryan (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2006; Delaune, Kremer, and Ryan 2009), and as previous discussed (see *related work* in Section 1), we formalise ballot secrecy for two voters $\mathcal{A}$, $\mathcal{B}$ and two candidates $t$, $t'$ with the assertion that an adversary cannot distinguish between a situation in which voter $\mathcal{A}$ votes for candidate $t$ and voter $\mathcal{B}$ votes for candidate $t'$, from another situation in which $\mathcal{A}$ votes $t'$ and $\mathcal{B}$ votes $t$. Formally, this is captured by Definition 4.
**Definition 4** (Ballot secrecy). *Given a Helios process specification $\phi$, we say *ballot secrecy is satisfied* if for all $(m_1,m'_1),\allowbreak(m_2,m'_2)\in\{(\mathsf{zero},\mathsf{zero}),\allowbreak(\mathsf{zero},\mathsf{one}),\allowbreak(\mathsf{one},\mathsf{zero})\}$ and integers $\allowbreak n \geq2$, we have $$\begin{gathered} A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]}\\ \approx_l A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]} \end{gathered}$$ where $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $m_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\textnormal{\raisebox{2pt}{\footnotesize $m'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $m_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $m'_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$.*
The ballot secrecy definition proposed by Delaune, Kremer & Ryan considered a vote to be an arbitrary name, whereas a vote in our setting must be a pair $(m,n)\in\{(\mathsf{zero},\mathsf{zero}),(\mathsf{zero},\mathsf{one}),(\mathsf{one},\mathsf{zero})\}$; it follows that Definition 4 is a straightforward variant of the original. The Helios 2.0 protocol does not satisfy our privacy definition (Lemma 1) and naïve ballot weeding solutions are also insufficient (Lemma 2).
**Lemma 1**. *The Helios process specification $\phi_{\sf orig}$ does not satisfy ballot secrecy.*
Intuitively, the proof of Lemma 1 is due to the environment’s ability to replay $\mathcal{A}$’s ballot, therefore introducing an observable difference: the result will include two instances of $\mathcal{A}$’s vote. Formally, this follows immediately from the proof Lemma 2.
**Lemma 2**. *The Helios process specification $\phi_{\sf ident}$ does not satisfy ballot secrecy.*
*Consider $n = 3$, $(m_1,m'_1) = (\mathsf{zero},\mathsf{one})$ and $(m_2,m'_2) = (\mathsf{one},\mathsf{zero})$. Let $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $m_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\textnormal{\raisebox{2pt}{\footnotesize $m'_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $m_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $m'_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }'$}}\}$. We consider a sequence of transitions where the two voters output their ballots and then the adversary chooses its ballots to be a permutation of the first voter’s ballot. Namely, if the first voter’s ballot is $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{ciph,ciph',spk,spk',\widehat{spk}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ then the adversary outputs $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{ciph',ciph,spk',spk,\widehat{spk}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$. Formally, this corresponds to the transitions.*
*xx̄ $A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]}\xrightarrow{}\xrightarrow{\nu\,x.\overline{c}\langle x\rangle}\xrightarrow{}\xrightarrow{\nu\,y.\overline{c}\langle y\rangle}$ $\xrightarrow{c(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(x),\pi_{1}(x),\pi_{4}(x),\pi_{3}(x),\pi_{5}(x)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}\xrightarrow{}^*\xrightarrow{\nu\,z.\overline{c}\langle z\rangle} \nu\,\tilde{n}.\tau_1$*
*for some names $\tilde{n}$ and substitution $\tau_1$ such that: $$\begin{array}{lcl} \mathsf{dec}(\pi_{1}(z),\pi_{1}(x)*\pi_{1}(y)*\pi_{2}(x))\tau_1 &=_E& \mathsf{one}+\mathsf{one} \end{array}$$ Then this labeled transition has to matched:*
*xx̄ $A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]}\xrightarrow{}\xrightarrow{\nu\,x.\overline{c}\langle x\rangle}\xrightarrow{}\xrightarrow{\nu\,y.\overline{c}\langle y\rangle}$ $\xrightarrow{c(\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{2}(x),\pi_{1}(x),\pi_{4}(x),\pi_{3}(x),\pi_{5}(x)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$})}\xrightarrow{}^*\xrightarrow{\nu\,z.\overline{c}\langle z\rangle} \nu\,\tilde{n}.\tau_2$*
*for some names $\tilde{n}$ and substitution $\tau_2$, such that: $$\begin{array}{lcl} %\Dec{\proj{1}{z}}{\proj{1}{x}*\proj{1}{y}*\proj{1}{x}}\tau_1 &=_\EE& \one\\ \mathsf{dec}(\pi_{1}(z),\pi_{1}(x)*\pi_{1}(y)*\pi_{2}(x))\tau_2 &=_E& \mathsf{one}%+ \one \end{array}$$ It follows immediately that $\nu\,\tilde{n}.\tau_1\not\approx_s\nu\,\tilde{n}.\tau_2$ and, hence, $\phi_{\sf ident}$ does not satisfy ballot secrecy.*
In contrast, removing duplicates up to permutation ensures ballot secrecy.
**Theorem 1**. *The Helios process specification $\phi_{\sf sol}$ satisfies ballot secrecy.*
ProVerif is an automatic tool that can check equivalence in the applied pi calculus (Blanchet, Abadi, and Fournet 2008). Although ProVerif has been successfully used to prove ballot secrecy (for example, in the Fujioka, Okamoto & Ohta protocol (Delaune, Ryan, and Smyth 2008)), it cannot prove Theorem 1 for two main reasons. First, ProVerif cannot prove equivalences under the homomorphic equation (Equation [eq:combination]). Second, our theorem states ballot secrecy for any number $n$ of participants and ProVerif cannot handle parametrised processes. We proceed by constructing a relation that relates ${A^{\phi}_n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]$ and ${A^{\phi}_n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau \mid\allowbreak V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]$, and all their successors, such that it satisfies the three properties of Definition 2. In particular, the two final frames (containing the result of the election) should be statically equivalent. A key step is to show that ballots accepted by the bulletin board must have a particular form due to the checks performed by $\phi_{\sf sol}$.
**Definition 5** (Valid ballot). *A term $N$ is said to be a *valid ballot* if $N=\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{N_1,N_2,N_3,N_4,N_5}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ for some $N_i$ such that $N_1 = \mathsf{penc}(z_{\mathsf{pk }},N_1^1,N_1^2)$ and $N_1 = \mathsf{penc}(z_{\mathsf{pk }},N_2^1,N_2^2)$ with $N_1^2,N_2^2\in\{\mathsf{zero},\mathsf{one}\}$.*
Having shown that the bulletin board accepts only valid ballots, we can deduce that the outcome of the election at the end of the execution of $A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]}$ is exactly the same as in $A^{\phi}_n{[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau\mid V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]}$. We can then conclude the proof of Theorem 1 by showing that the partial decryptions and the encrypted ballots of honest voters do not leak any extra information to the adversary. The full proof appears in the long version of this paper (Smyth and Cortier 2010a). ## Limitations The limitations of our model, which we introduced to simplify the presentation and proof, are detailed below; we believe a full security proof should follow using similar reasoning. We consider a model with only two candidates and, moreover, we make use of the (standard) definition of ballot secrecy which is limited to elections with two honest voters (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2006; Delaune, Kremer, and Ryan 2009). In addition, the definition of ballot secrecy does not consider parallel composition of protocol executions and we therefore recommend using distinct keys for each election (although we believe it should be sufficient to include an election identifier – for example, the election fingerprint – within the challenge hashes included within signatures of knowledge, similar to the methodology in Section 4.2). The administrative process $A^{\phi}_n$ enforces an ordering on voters (namely, the voter using private channel $a_1$ must vote first, followed by the voter using private channel $a_2$, and then any remaining voters – controlled by the adversarial environment – can vote) and $A^{\phi}_n$ does not permit revoting. The signature and equational theory do not capture low-level technical details surrounding the correct construction of public keys; in particular, we do not use signatures of knowledge to verify correct key construction. We also omit signatures of knowledge that demonstrate correct construction of partial decryptions. Finally, we offer the usual caveat to formal analysis and acknowledge that our result does not imply the absence of real-world attacks (see, for example, (P. Y. A. Ryan and Schneider 1998; Abadi and Rogaway 2000, 2002; Warinschi 2003, 2005)). It may, therefore, be possible to modify the ballot in a way that would not be captured by our analysis. (In particular, it is important to notice that the scheme used for signatures of knowledge is not provably non-malleable.) Accordingly, we encourage a thorough cryptographic analysis of our solution in the provable security model. # Conclusion and further discussion This paper identifies a vulnerability in Helios 2.0 which can be used to violate ballot secrecy. Critics may argue that an attack is unrealistic due its high cost; indeed, in some cases, the attack may change the outcome of an election (that is, the votes introduced for the purposes of violating privacy may swing the result), and large scale privacy invasions would be expensive in terms of the required number of dishonest voters. However, if the views of these critics are to be entertained, then we must revise the standard definitions of ballot secrecy in the literature (for example, (Kremer and Ryan 2005; Delaune, Kremer, and Ryan 2006; Backes, Hriţcu, and Maffei 2008)) because Helios cannot satisfy them. Furthermore, we believe all voters should be considered equally and, hence, the preservation of ballot secrecy should be universal. But, for elections using Helios, our case study demonstrates the contrary: in French legislative elections a coalition of voters can gain some information about a voter’s vote in an arbitrary polling station and, moreover, if the number of voters registered at a particular polling station is small (for example, in a rural setting), then a voter’s privacy can be violated by a few dishonest voters. It follows that privacy of individual voters can be compromised by a few dishonest voters and, accordingly, we believe our attack is significant. We also believe the absence of ballot independence can be similarly exploited in other electronic voting protocols to violate privacy (indeed, our preliminary results support this hypothesis). To address the problem, we have introduced a variant of the Helios protocol which has been shown to satisfy definitions of ballot secrecy in the applied pi calculus and work in progress aims to provide a full security proof in a cryptographic setting. Finally, Adida & Pereira have acknowledged the vulnerability (Adida 2010; Adida and Pereira 2010) and a fix has been proposed for future Helios releases. # Acknowledgements We are grateful to Ben Adida and Olivier Pereira for their constructive comments, and hope this research will enhance future Helios releases. Discussion with Mark D. Ryan helped clarify the presentation of this paper, and Ben Adida informed us that Douglas Wikström is the contemporaneous discoverer of this attack. David Bernhard gave useful feedback on our attack variants. The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement $n^{\circ}$ 258865, project ProSecure, and the ANR-07-SeSur-002 AVOTÉ project. ## Signatures of knowledge Helios is reliant on signatures of knowledge to ensure secrecy and integrity of the ElGamal scheme, and to ensure voters encrypt valid votes. This appendix presents suitable cryptographic primitives. Let $\mathcal{H}$ denote a hash function. In Helios, $\mathcal{H}$ is defined to be SHA-256. ### Knowledge of discrete logs Given the aforementioned cryptographic parameters $(p,q,g)$, a signature of knowledge demonstrating knowledge of a discrete logarithm $h = \log_g g^x$ can be derived, and verified, as defined by (Chaum et al. 1987; Chaum, Evertse, and Graaf 1988; Schnorr 1990). #### Sign Given $x$, select a random nonce $w \in_R \mathbb{Z}_q^*$. Compute witness $g' = g^w \bmod p$, challenge $c = \mathcal{H}(g') \bmod q$ and response $s = w + c \cdot x \bmod q$. #### Verify Given $h$ and signature $g',s$, check $g^s \equiv g'\cdot h^c \pmod p$, where $c = \mathcal{H}(g') \bmod q$. A valid proof asserts knowledge of $x$ such that $x = \log_g h$; that is, $h \equiv g^x \bmod p$. ### Equality between discrete logs Given the aforementioned cryptographic parameters $(p,q,g)$, a signature of knowledge demonstrating equality between discrete logarithms $\log_f f^x$ and $\log_g g^x$ can be derived, and verified, as defined by (Pedersen 1991; Chaum and Pedersen 1993). #### Sign Given $f,g,x$, select a random nonce $w \in_R \mathbb{Z}_q^*$. Compute witnesses $f' = f^w \bmod p$ and $g' = g^w \bmod p$, challenge $c = \mathcal{H}(f',g') \bmod q$ and response $s = w + c \cdot x \bmod q$. #### Verify Given $f,g,h,k$ and signature $f',g',s$, check $f^s \equiv f'\cdot h^c \pmod p$ and $g^s \equiv g'\cdot k^c \pmod p$, where $c = \mathcal{H}(f',g') \bmod q$. A valid proof asserts $\log_f h = \log_g k$; that is, there exists $x$, such that $h \equiv f^x \bmod p$ and $k \equiv g^x \bmod p$. This signature of knowledge scheme can be extended to a disjunctive proof of equality between discrete logs (see below). For our purposes, given a ciphertext $(a,b)$, each trustee would derive a signature on $g,a,x_i$, where $x_i$ is the trustee’s private key share. The $i$th trustee’s signature $g'_i,a'_i,c_i,s_i$ would be verified with respect to $g,a,h_i,k_i$, where $h_i$ is the trustee’s share of the public key and $k_i$ is the trustee’s partial decryption; that is, the proof asserts $\log_g h_i = \log_a k_i$, as required for integrity of decryption. ### Disjunctive proof of equality between discrete logs Given the aforementioned cryptographic parameters $(p,q,g)$, a signature of knowledge demonstrating that a ciphertext $(a,b)$ contains either $0$ or $1$ (without revealing which), can be constructed by proving that either $\log_g a = \log_h b$ or $\log_g a = \log_h b/g^{m}$; that is, a signature of knowledge demonstrating a disjunct proof of equality between discrete logarithms (Cramer, Damgård, and Schoenmakers 1994; Schoenmakers 2009). Observe for a valid ciphertext $(a,b)$ that $a\equiv g^r \bmod p$ and $b\equiv h^r \cdot g^m \bmod p$ for some nonce $r\in\mathbb{Z}_q^*$; hence the former disjunct $\log_g g^r = \log_h h^r \cdot g^m$ is satisfied when $m = 0$, and the latter $\log_g g^r = \log_h ( h^r \cdot g^m ) / g^{m}$ when $m = 1$. This technique is generalised by (Adida et al. 2009) to allow a signature of knowledge demonstrating that a ciphertext $(a,b)$ contains message $m$, where $m\in\{{\sf min},\dots,{\sf max}\}$ for some system parameters ${\sf min},{\sf max}\in\mathbb{N}$. Formally, a signature of knowledge demonstrating a disjunct proof of equality between discrete logarithms can be derived, and verified, as follows (Adida et al. 2009; Cramer, Damgård, and Schoenmakers 1994; Schoenmakers 2009). #### Sign Given ciphertext $(a,b)$ such that $a\equiv g^r \bmod p$ and $b\equiv h^r \cdot g^m \bmod p$ for some nonce $r\in\mathbb{Z}_q^*$, where plaintext $m\in\{{\sf min},\dots,{\sf max}\}$. For all $i \in \{{\sf min},\dots,m-1,m+1,\dots,{\sf max}\}$, compute challenge $c_i \in_R \mathbb{Z}_q^*$, response $s_i \in_R \mathbb{Z}_q^*$ and witnesses $a_i = g^{s_i} / a^{c_i} \bmod p$ and $b_{i} = h^{s_i} /(b / g^i)^{c_i} \bmod p$. Select a random nonce $w \in_R\mathbb{Z}_q^*$. Compute witnesses $a_m = g^w \bmod p$ and $b_m = h^w \bmod p$, challenge $c_m = \mathcal{H}(a_{\sf min},b_{\sf min},\dots,a_{\sf max},b_{\sf max}) - \sum_{i\in\{{\sf min},\dots,m-1,m+1,\dots,{\sf max}\}} c_i \pmod q$ and response $s_m = w + r\cdot c_m \bmod q$. #### Verify Given $(a,b)$ and $(a_{\sf min},\allowbreak b_{\sf min},\allowbreak c_{\sf min},\allowbreak s_{\sf min},\allowbreak \dots,\allowbreak a_{\sf max},\allowbreak b_{\sf max},\allowbreak c_{\sf max},\allowbreak s_{\sf max})$, for each ${\sf min}\leq i \leq {\sf max}$ check $g^{s_i} \equiv a_i \cdot a^{c_i} \pmod p$ and $h^{s_i} \equiv b_i \cdot (b/g^i)^{c_i} \pmod p$. Finally, check $\mathcal{H}(a_{\sf min},b_{\sf min},\dots,a_{\sf max},b_{\sf max}) \equiv \sum_{{\sf min}\leq i \leq {\sf max}} c_i \pmod q$. A valid proof asserts that $(a,b)$ is a ciphertext containing the message $m$ such that $m\in\{{\sf min},\dots,{\sf max}\}$. # References
Abadi, Martı́n, and Cédric Fournet. 2001. “Mobile Values, New Names, and Secure Communication.” In *POPL’01: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, 104–15. ACM Press.
Abadi, Martı́n, and Phillip Rogaway. 2000. “Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption).” In *IFIP TCS’00: 1st International Conference on Theoretical Computer Science*, 1872:3–22. LNCS. Springer.
———. 2002. “Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption).” *Journal of Cryptology* 15 (2): 103–27.
Adida, Ben. 2006. “Advances in Cryptographic Voting Systems.” PhD thesis, Department of Electrical Engineering; Computer Science, Massachusetts Institute of Technology.
———. 2008. “Helios: Web-based Open-Audit Voting.” In *USENIX Security’08: 17th USENIX Security Symposium*, 335–48. USENIX Association.
———. 2010. “Attacks and Defenses.” Helios documentation, .
Adida, Ben, Olivier de Marneffe, Olivier Pereira, and Jean-Jacques Quisquater. 2009. “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.
Adida, Ben, and Olivier Pereira. 2010. “Private Email Communication.”
“Article L65 of the French Electoral Code.” n.d. http://www.legifrance.gouv.fr/.
Backes, Michael, Cătălin Hriţcu, and Matteo Maffei. 2008. “Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus.” In *CSF’08: 21st Computer Security Foundations Symposium*, 195–209. IEEE Computer Society.
Benaloh, Josh. 2006. “Simple Verifiable Elections.” In *EVT’06: Electronic Voting Technology Workshop*. USENIX Association.
———. 2007. “Ballot Casting Assurance via Voter-Initiated Poll Station Auditing.” In *EVT’07: Electronic Voting Technology Workshop*. USENIX Association.
Benaloh, Josh, Serge Vaudenay, and Jean-Jacques Quisquater. 2010. “Final Report of IACR Electronic Voting Committee.” International Association for Cryptologic Research. .
Blanchet, Bruno, Martı́n Abadi, and Cédric Fournet. 2008. “Automated verification of selected equivalences for security protocols.” *Journal of Logic and Algebraic Programming* 75 (1): 3–51.
Chaum, David, Jan-Hendrik Evertse, and Jeroen van de Graaf. 1988. “An Improved Protocol for Demonstrating Possession of Discrete Logarithms and Some Generalizations.” In *EUROCRYPT’87: 4th International Conference on the Theory and Applications of Cryptographic Techniques*, 304:127–41. LNCS. Springer.
Chaum, David, Jan-Hendrik Evertse, Jeroen van de Graaf, and René Peralta. 1987. “Demonstrating Possession of a Discrete Logarithm Without Revealing It.” In *CRYPTO’86: 6th International Cryptology Conference*, 263:200–212. LNCS. Springer.
Chaum, David, and Torben P. Pedersen. 1993. “Wallet Databases with Observers.” In *CRYPTO’92: 12th International Cryptology Conference*, 740:89–105. LNCS. Springer.
Chaum, David, Peter Y. A. Ryan, and Steve Schneider. 2005. “A Practical Voter-Verifiable Election Scheme.” In *ESORICS’05: 10th European Symposium on Research in Computer Security*, 3679:118–39. LNCS. Springer.
Chor, Benny, Shafi Goldwasser, Silvio Micali, and Baruch Awerbuch. 1985. “Verifiable Secret Sharing and Achieving Simultaneity in the Presence of Faults.” In *FOCS’85: 26th Foundations of Computer Science Symposium*, 383–95. IEEE Computer Society.
Chor, Benny, and Michael O. Rabin. 1987. “Achieving Independence in Logarithmic Number of Rounds.” In *PODC’87: 6th Principles of Distributed Computing Symposium*, 260–68. ACM Press.
Clarkson, Michael R., Stephen Chong, and Andrew C. Myers. 2007. “Civitas: Toward a Secure Voting System.” 2007-2081. Cornell University; .
———. 2008. “Civitas: Toward a Secure Voting System.” In *S&p’08: 29th Security and Privacy Symposium*, 354–68. IEEE Computer Society.
Cramer, Ronald, Ivan Damgård, and Berry Schoenmakers. 1994. “Proofs of Partial Knowledge and Simplified Design of Witness Hiding Protocols.” In *CRYPTO’94: 14th International Cryptology Conference*, 839:174–87. LNCS. Springer.
Cramer, Ronald, Rosario Gennaro, and Berry Schoenmakers. 1997. “A Secure and Optimally Efficient Multi-Authority Election Scheme.” In *EUROCRYPT’97: 16th International Conference on the Theory and Applications of Cryptographic Techniques*, 1233:103–18. LNCS. Springer.
Delaune, Stéphanie, Steve Kremer, and Mark Ryan. 2006. “Coercion-Resistance and Receipt-Freeness in Electronic Voting.” In *CSFW’06: 19th Computer Security Foundations Workshop*, 28–42. IEEE Computer Society.
Delaune, Stéphanie, Steve Kremer, and Mark D. Ryan. 2009. “Verifying privacy-type properties of electronic voting protocols.” *Journal of Computer Security* 17 (4): 435–87.
———. 2010. “Verifying Privacy-Type Properties of Electronic Voting Protocols: A Taster.” In *Towards Trustworthy Elections: New Directions in Electronic Voting*, edited by David Chaum, Markus Jakobsson, Ronald L. Rivest, and Peter Y. A. Ryan, 6000:289–309. LNCS. Springer.
Delaune, Stéphanie, Mark D. Ryan, and Ben Smyth. 2008. “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*, 263:263–78. International Federation for Information Processing (IFIP). Springer.
Dolev, Danny, Cynthia Dwork, and Moni Naor. 1991. “Non-Malleable Cryptography.” In *STOC’91: 23rd Theory of Computing Symposium*, 542–52. ACM Press.
———. 2000. “Nonmalleable Cryptography.” *Journal on Computing* 30 (2): 391–437.
ElGamal, Taher. 1985. “A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms.” *IEEE Transactions on Information Theory* 31 (4): 469–72.
“Est Républicain.” 2007. Daily French Newspaper.
Estehghari, Saghar, and Yvo Desmedt. 2010. “Exploiting the Client Vulnerabilities in Internet E-voting Systems: Hacking Helios 2.0 as an Example.” In *EVT/WOTE’10: Electronic Voting Technology Workshop/Workshop on Trustworthy Elections*. USENIX Association.
Fujioka, Atsushi, Tatsuaki Okamoto, and Kazuo Ohta. 1992. “A Practical Secret Voting Scheme for Large Scale Elections.” In *AUSCRYPT’92: Workshop on the Theory and Application of Cryptographic Techniques*, 718:244–51. LNCS. Springer.
Gennaro, Rosario. 1995. “Achieving Independence Efficiently and Securely.” In *PODC’95: 14th Principles of Distributed Computing Symposium*, 130–36. ACM Press.
———. 2000. “A Protocol to Achieve Independence in Constant Rounds.” *IEEE Transactions on Parallel and Distributed Systems* 11 (7): 636–47.
Haber, Stuart, Josh Benaloh, and Shai Halevi. 2010. “The Helios e-Voting Demo for the IACR.” International Association for Cryptologic Research. .
Juels, Ari, Dario Catalano, and Markus Jakobsson. 2002. “Coercion-Resistant Electronic Elections.” Cryptology ePrint Archive, Report 2002/165.
———. 2005. “Coercion-Resistant Electronic Elections.” In *WPES’05: 4th Workshop on Privacy in the Electronic Society*, 61–70. ACM Press.
———. 2010. “Coercion-Resistant Electronic Elections.” In *Towards Trustworthy Elections: New Directions in Electronic Voting*, edited by David Chaum, Markus Jakobsson, Ronald L. Rivest, and Peter Y. A. Ryan, 6000:37–63. LNCS. Springer.
Kremer, Steve, and Mark D. Ryan. 2005. “Analysis of an Electronic Voting Protocol in the Applied Pi Calculus.” In *ESOP’05: 14th European Symposium on Programming*, 3444:186–200. LNCS. Springer.
Kremer, Steve, Mark D. Ryan, and Ben Smyth. 2010. “Election verifiability in electronic voting protocols.” In *ESORICS’10: 15th European Symposium on Research in Computer Security*, 6345:389–404. LNCS. Springer.
Langer, Lucie. 2010. “Privacy and Verifiability in Electronic Voting.” PhD thesis, Fachbereich Informatik, Technischen Universität Darmstadt.
Langer, Lucie, Axel Schmidt, Johannes Buchmann, and Melanie Volkamer. 2010. “A Taxonomy Refining the Security Requirements for Electronic Voting: Analyzing Helios as a Proof of Concept.” In *ARES’10: 5th International Conference on Availability, Reliability and Security*, 475–80. IEEE Computer Society.
Langer, Lucie, Axel Schmidt, Johannes Buchmann, Melanie Volkamer, and Alexander Stolfik. 2010. “Towards a Framework on the Security Requirements for Electronic Voting Protocols.” In *Re-Vote’09: First International Workshop on Requirements Engineering for e-Voting Systems*, 61–68. IEEE Computer Society.
Lee, Byoungcheon, Colin Boyd, Ed Dawson, Kwangjo Kim, Jeongmo Yang, and Seungjae Yoo. 2004. “Providing Receipt-Freeness in Mixnet-Based Voting Protocols.” In *ICISC’03: 6th International Conference on Information Security and Cryptology*, 2971:245–58. LNCS. Springer.
Lenstra, Arjen K., and Hendrik W. Lenstra Jr. 1990. “Algorithms in Number Theory.” In *Handbook of Theoretical Computer Science, Volume A: Algorithms and Complexity*, edited by Jan van Leeuwen, 673–716. MIT Press.
Leung, Adrian, Liqun Chen, and Chris J. Mitchell. 2008. “On a Possible Privacy Flaw in Direct Anonymous Attestation (DAA).” In *Trust’08: 1st International Conference on Trusted Computing and Trust in Information Technologies*, 179–90. LNCS 4968. Springer.
Okamoto, Tatsuaki. 1998. “Receipt-Free Electronic Voting Schemes for Large Scale Elections.” In *SP’97: 5th International Workshop on Security Protocols*, 1361:25–35. LNCS. Springer.
Participants of the Dagstuhl Conference on Frontiers of E-Voting. 2007. “Dagstuhl Accord.” .
Pedersen, Torben P. 1991. “A Threshold Cryptosystem without a Trusted Party.” In *EUROCRYPT’91: 10th International Conference on the Theory and Applications of Cryptographic Techniques*, 522–26. LNCS 547. Springer.
Pereira, Olivier, Ben Adida, and Olivier de Marneffe. 2010. “Bringing Open Audit Elections into Practice: Real World Uses of Helios.” Swiss e-voting workshop, . See also .
Pfitzmann, Birgit. 1994. “Breaking Efficient Anonymous Channel.” In *EUROCRYPT’94: 11th International Conference on the Theory and Applications of Cryptographic Techniques*, 950:332–40. LNCS. Springer.
Princeton University. 2010. “Princeton Election Server.” .
“Résultat par bureau du premier tour des élections régionales.” 2010. .
Rudolph, Carsten. 2007. “Covert Identity Information in Direct Anonymous Attestation (DAA).” In *SEC’07: 22nd International Information Security Conference*, 232:443–48. International Federation for Information Processing (IFIP). Springer.
Ryan, Mark D., and Ben Smyth. 2011. “Applied pi calculus.” In *Formal Models and Techniques for Analyzing Security Protocols*, edited by Véronique Cortier and Steve Kremer. IOS Press.
Ryan, Peter Y. A., and Steve A. Schneider. 1998. “An Attack on a Recursive Authentication Protocol. A Cautionary Tale.” *Information Processing Letters* 65 (1): 7–10.
Sako, Kazue, and Joe Kilian. 1994. “Secure Voting Using Partially Compatible Homomorphisms.” In *CRYPTO’94: 14th International Cryptology Conference*, 839:411–24. LNCS. Springer.
Schnorr, Claus-Peter. 1990. “Efficient Identification and Signatures for Smart Cards.” In *CRYPTO’89: 9th International Cryptology Conference*, 435:239–52. LNCS. Springer.
Schoenmakers, Berry. 2009. “Voting Schemes.” In *Algorithms and Theory of Computation Handbook, Second Edition, Volume 2: Special Topics and Techniques*, edited by Mikhail J. Atallah and Marina Blanton. CRC Press.
Shanks, Daniel. 1971. “Class number, a theory of factorization and genera.” In *Number Theory Institute*, 20:415–40. Symposia in Pure Mathematics. American Mathematical Society.
Smyth, Ben. 2011. “Formal verification of cryptographic protocols with automated reasoning.” PhD thesis, School of Computer Science, University of Birmingham.
Smyth, Ben, and Véronique Cortier. 2010a. “Attacking and Fixing Helios: An Analysis of Ballot Secrecy.” Cryptology ePrint Archive, Report 2010/625.
———. 2010b. “Attacking ballot secrecy in Helios.” YouTube video, linked from .
Smyth, Ben, Mark D. Ryan, Steve Kremer, and Mounira Kourjieh. 2010. “Towards automatic analysis of election verifiability properties.” In *ARSPA-WITS’10: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security*, 6186:165–82. LNCS. Springer.
Volkamer, Melanie. 2009. *Evaluation of Electronic Voting: Requirements and Evaluation Procedures to Support Responsible Election Authorities*. Vol. 30. Lecture Notes in Business Information Processing. Springer.
Volkamer, Melanie, and Rüdiger Grimm. 2010. “Determine the Resilience of Evaluated Internet Voting Systems.” In *Re-Vote’09: First International Workshop on Requirements Engineering for e-Voting Systems*, 47–54. IEEE Computer Society.
Warinschi, Bogdan. 2003. “A Computational Analysis of the Needham-Schröeder-(Lowe) Protocol.” In *CSFW’03: 16th Computer Security Foundations Workshop*, 248–62. IEEE Computer Society.
———. 2005. “A computational analysis of the Needham-Schroeder-(Lowe) protocol.” *Journal of Computer Security* 13 (3): 565–91.
Wikström, Douglas. 2006. “Simplified Submission of Inputs to Protocols.” Cryptology ePrint Archive, Report 2006/259.
———. 2008. “Simplified Submission of Inputs to Protocols.” In *SCN’08: 6th International Conference on Security and Cryptography for Networks*, 5229:293–308. LNCS. Springer.