# Attacking and fixing Helios: An analysis of ballot secrecy
Véronique Cortier, Ben Smyth
## 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 article, we analyse ballot secrecy in Helios and discover a vulnerability which allows an adversary to compromise the privacy of voters. The vulnerability exploits the absence of ballot independence in Helios and works by replaying a voter’s ballot or a variant of it, the replayed ballot magnifies the voter’s contribution to the election outcome and this magnification can be used to violated privacy. We demonstrate the practicality of the attack by violating a voter’s privacy in a mock election using the software implementation of Helios. 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. We present a fix and show that our solution satisfies a formal definition of ballot secrecy using the applied pi calculus. Furthermore, we present similar vulnerabilities in other electronic voting protocols – namely, the schemes by Lee *et al.*, Sako & Kilian, and Schoenmakers – which do not assure ballot independence. Finally, we argue that independence and privacy properties are unrelated, and non-malleability is stronger than independence.
#### Keywords.
Applied Pi Calculus, Attack, Ballot Independence, Ballot Secrecy, Electronic Voting, Helios, Malleability, Privacy.
# Introduction
Paper-based elections derive security properties from physical characteristics of the real-world. For example, marking a ballot in the isolation of a polling booth and depositing the completed ballot into a locked ballot box provides privacy; the polling booth also ensures that voters cannot be influenced by other votes and the locked ballot box prevents the announcement of early results, thereby ensuring fairness; and the transparency of the whole election process from ballot casting to tallying and the impossibility of altering the markings on a paper ballot sealed inside a locked ballot box gives an assurance of correctness and facilitates verifiability. Replicating these attributes in a digital setting has proven to be difficult and, hence, the provision of secure electronic voting systems is an active research topic.
Informally, *privacy* for electronic voting systems is characterised by the following requirements (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.
*Verifiability* includes three properties (Juels, Catalano, and Jakobsson 2005; *Dagstuhl Accord* 2007; Kremer, Ryan, and Smyth 2010):
- *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.
- *Eligibility verifiability.* 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.
Finally, *fairness* – summarised by the notion that *all voters are equal* – has not be thoroughly studied, but nonetheless we believe the following aspects are desirable:
- *Ballot independence.* Observing another voter’s interaction with the election system does not allow a voter to cast a meaningfully related vote.
- *No early results.* A voter cannot change her vote once partial results are available.
- *Pulling out.* Once partial results are available a voter cannot abort.
The privacy property helps ensure that voters can express their free-will without fear of retribution, in particular, receipt freeness and coercion resistance attempt to prevent intimidation of voters. In addition, receipt freeness helps prevent vote buying. The individual, universal and eligibility verifiability properties (also called *end-to-end verifiability* (Juels, Catalano, and Jakobsson 2002; Chaum, Ryan, and Schneider 2005; Adida 2006, 2008; *Dagstuhl Accord* 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. The fairness property prohibits the voting system from influencing a voter’s behaviour, that is, observation of the voting system does not leak information that may affect a voter’s vote, for example, ballot independence prevents Bob from casting the same vote as Alice (possibly without learning Alice’s vote). In this article, we analyse ballot secrecy in Helios 2.0 (Adida et al. 2009).
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 these formal definitions.
#### Helios 2.0.
Helios is an open-source web-based electronic voting system which uses homomorphic encryption. 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 (satisfying these stronger privacy properties typically increases the voting system’s complexity and, hence, a scheme satisfying ballot secrecy, rather than coercion resistance, may be preferred due its relative simplicity). In addition to ballot secrecy, the system provides individual and universal verifiability (cf. (Kremer, Ryan, and Smyth 2010; Smyth et al. 2010) and (Smyth 2011, chap. 3) for an analysis of verifiability in Helios). Helios is particularly significant due to its real-world deployment: the International Association of Cryptologic Research (IACR) 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 Election Server* 2010).
## 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 an attack in an election with three voters – namely, Alice, Bob, and Mallory – as follows: 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 our attack has been demonstrated by violating a voter’s privacy in a mock election using the software implementation of Helios. 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 voters’ privacy in elections using Helios. We also propose variants of the attack which abuse the malleability of ballots to ensure ballots cast by the adversary are distinct; this makes detecting the attack non-trivial (that is, checking for exact duplicates is insufficient to ensure ballot secrecy). Nonetheless, we fix the Helios protocol by identifying and discarding adversarial 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. The revised scheme is shown to satisfy a formal definition of ballot secrecy using the applied pi calculus. In addition, we demonstrate that the absence of ballot independence can be exploited in other electronic voting protocols to violate privacy; in particular, a similar attack is shown against the protocol by Lee *et al.* (Lee et al. 2004) whereby an adversary replays a voter’s ballot or a variant of it, and verbatim replay attacks are demonstrated against two schemes presented at CRYPTO (namely, the protocols due to Sako & Kilian (Sako and Kilian 1994) and Schoenmakers (Schoenmakers 1999)). Finally, we present some evidence to demonstrate that independence and privacy are unrelated properties, and non-malleability is stronger than independence.
#### Structure of this article.
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 article.) Section 3 describes our attack and some variants, in addition to a study of the attack’s 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. Section 6 demonstrates that the absence of ballot independence can be similarly exploited in other electronic voting protocols to violate privacy and Section 7 considers relationships between ballot independence and other security properties. Finally, Section 8 considers related work and our conclusion appears in Section 9.
# Background: Helios 2.0
We provide a full description of Helios 2.0. This scheme 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). In addition, signature proofs of knowledge are used to ensure secrecy and integrity of the ElGamal scheme, and to ensure voters encrypt valid votes. We will recall these cryptographic primitives 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 prove 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}$. These proofs can be achieved using signatures of knowledge (see Appendix 10 for details). In addition, the voter must demonstrate that a valid vote has been encrypted and we describe a suitable signature of knowledge scheme in the following section.
## 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, by application of a signature of knowledge demonstrating a disjunctive 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 disjunct $\log_g g^r = \log_h ( h^r \cdot g^m ) / g^{m}$ is satisfied when $m = 1$. This technique is generalised by Adida *et al.* (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,\allowbreak{\sf max}\}$ for some system parameters ${\sf min}\in\mathbb{N}$ and ${\sf max}\in\mathbb{N}^*$ such that ${\sf min}\leq {\sf max}$. Formally, a signature of knowledge demonstrating a disjunctive 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), where $\mathcal{H}$ is a SHA-256 hash function.
#### 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}\}$.
## 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_{\ell}) \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, …, tℓ) ∪ {ϵ} and vote v.
Output: Encrypted vote (a1, b1), …, (aℓ, bℓ), signatures of knowledge (ā1, b̄1, c̄1, s̄1, ā′1, b̄′1, c̄′1, s̄′1), …, (āℓ, b̄ℓ, c̄ℓ, s̄ℓ, ā′ℓ, b̄′ℓ, c̄′ℓ, s̄′ℓ) and signature of knowledge (ā, b̄, c̄, s̄, ā′, b̄′, c̄′, s̄′), where the signatures are constructed using the algorithm presented in Section 2.2.
If v ∉ t̃ then the script terminates.
Encode the vote v as a bitstring. For all 1 ≤ i ≤ ℓ, let $$m_i = \left\{\begin{array}{lcl}
1 &\quad& \textrm{if $v = t_i$}\\
0 & & \textrm{otherwise}
\end{array}\right.$$
The bitstring representing the vote is encrypted. For all 1 ≤ i ≤ ℓ, let (ai, bi) = (gri mod p, gmi ⋅ hri mod p) where ri∈Rℤq*.
For all 1 ≤ i ≤ ℓ, 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.
Let (ā, b̄, c̄, s̄, ā′, b̄′, c̄′, s̄′) be a signature of knowledge demonstrating that the ciphertext (a1 ⋅ … ⋅ aℓ, b1 ⋅ … ⋅ bℓ) 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" and this section shows that Helios does not satisfy this definition by presenting an attack which allows an adversary to reveal a voter’s vote (Section 5 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 identity $id$) and recast this ballot by corrupting dishonest voters. The multiple occurrences of the voter’s ballot will magnify the voter’s contribution to the election outcome, thereby leaking information that can be exploited to violate the voter’s privacy. The remainder of this section proceeds as follows: a description of the attack for three voters appears in Section 3.1 and variants are considered in Section 3.2, the attack is generalised to arbitrary many voters in Section 3.3 and the threat to real elections is also considered.
## Attack description
Let us consider an election with candidates $t_1,\dots,t_{\ell}$ and three eligible voters who have identities $id_1$, $id_2$ and $id_3$. Suppose that voters $id_1$ and $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,\ell},b_{i,\ell}) \\
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,\ell},\bar b_{i,\ell},\bar c_{i,\ell},\bar s_{i,\ell},\bar a'_{i,\ell},\bar b'_{i,\ell},\bar c'_{i,\ell},\bar s'_{i,\ell})\\
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,\ell},b_{i,\ell})$ contain either $0$ or $1$ (that is, the voter has assigned at most one vote to each candidate), and $spk'_i$ demonstrates that $(a_{i,1} \cdot\ldots\cdot a_{i,\ell}, \; b_{i,1} \cdot\ldots\cdot b_{i,\ell})$ contains either $0$ or $1$ (that is, the voter has voted for at most one candidate).
#### Replaying a ballot.
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 casts 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 observe 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. It follows that Helios does not satisfy ballot independence: observing another voter’s interaction with the election system allows a voter to cast the *same* vote. The absence of ballot independence 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,\ell} \cdot a_{2,\ell} \cdot a_{k,\ell},\;b_{1,\ell} \cdot b_{2,\ell} \cdot b_{k,\ell})$ 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 2010).
In the aforementioned attack description, the ballots cast by two voters are identical. This behaviour is not detected by Helios and, prior to our work, human detection – for example, by auditing – would have been improbable. Of course, further to our results, the aforementioned attack can be detected by searching for duplicated ballots. For a covert attack, the 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. However, this is not generally possible in Helios since fresh keys should be used for each election. The following section introduces further variants of our attack that exploit malleability to derive distinct ballots, thereby demonstrating that searching for duplicate ballots is insufficient to ensure ballot secrecy.
## Variants exploiting ballot malleability
Let us consider variants of our attack under the assumptions presented in the previous section: we have an election with candidates $t_1,\dots,t_{\ell}$ and three eligible voters such that the two honest voters have cast their votes using identities $id_1$ and $id_2$, and the remaining dishonest voter is controlled by the adversary, where the dishonest voter has the identity $id_3$. Given that we will consider ballot malleability, we refine our notation and consider the bulletin board entries of honest voters as follows: $$\begin{array}{c}
id_1, ciph_{1,1},\dots,ciph_{1,\ell}, spk_{1,1}, \dots, spk_{1,\ell}, spk'_1 \\
id_2, ciph_{2,1},\dots,ciph_{2,\ell}, spk_{2,1}, \dots, spk_{2,\ell}, spk'_2 \\
\end{array}$$ where for all $i\in\{1,2\}$ and $j\in\{1,\dots,\ell\}$ we have $$\begin{array}{lcl}
ciph_{i,j} &=& (a_{i,j},b_{i,j})\\
spk_{i,j} &=& (\bar a_{i,j},\bar b_{i,j},\bar c_{i,j},\bar s_{i,j},\bar a'_{i,j},\bar b'_{i,j},\bar c'_{i,j},\bar s'_{i,j})\\
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,j}$ is the $i$th voter’s encrypted vote for the candidate $t_j$ (that is, $ciph_{i,j}$ is a ciphertext containing the plaintext $1$ if the voter voted $t_j$, and $0$ otherwise), $spk_{i,j}$ demonstrates that the ciphertext $ciph_{i,j}$ contains either $0$ or $1$, and $spk'_i$ is defined as before, namely, it demonstrates that $(a_{i,1} \cdot\ldots\cdot a_{i,\ell}, \; b_{i,1} \cdot\ldots\cdot b_{i,\ell})$ contains either $0$ or $1$. In the remainder of this section we shall assume that the voter under attack casts the Ballot [ballotOne], namely, $$\label{ballotOne}
id_k,ciph_{k,1},\dots,ciph_{k,\ell},spk_{k,1},\dots,spk_{k,\ell},spk'_k$$ where $k\in\{1,2\}$.
### Integer representation attack
Given the Ballot [ballotOne], the adversary selects integers $r_1,r'_1,\dots,r_{\ell},r'_{\ell},r,r' \in\mathbb{N}$ and constructs the following related ballot, namely,
$$\label{ballotTwo}
ciph_{k,1},\dots,ciph_{k,\ell},\widebar{spk}_{k,1},\dots,\widebar{spk}_{k,\ell},\widebar{spk}'_k$$
where $\widebar{spk}'_k = (\bar a_k,\bar b_k,\bar c_k, \bar s_k+ r\cdot q, \bar a'_k,\bar b'_k,\bar c'_k, \bar s'_k+r'\cdot q)$ and for all $j\in\{1,\dots,\ell\}$ we have $\widebar{spk}_{k,j} = (\bar a_{k,j},\bar b_{k,j},\bar c_{k,j}, \bar s_{k,j}+r_j \cdot q,\bar a'_{k,j},\bar b'_{k,j},\bar c'_{k,j},\bar s'_{k,j}+r'_j \cdot q)$. Ballot [ballotTwo] adds multiples of $q$ to the response components of Ballot [ballotOne], this changes the ballot but not the vote, because the ciphertexts that encrypt the vote remain unchanged. It follows that Ballot [ballotTwo] can be cast by the adversary as a vote for the same candidate as the voter with identity $id_k$ selected and privacy can be violated as described in Section 3.1. This might be considered an oversight, rather than a theoretical issue, because the ballots are identical if considered as group elements.
### Permutation attacks
Given the Ballot [ballotOne], the adversary selects a permutation $\pi$ on $\{1,\dots,\ell\}$, where $\pi$ is not the identity, and proceeds as follows.
#### Constructing a related ballot.
The adversary constructs the Ballot [ballotThree]:
$$\label{ballotThree}
ciph_{k,\pi(1)},\dots,ciph_{k,\pi(\ell)},spk_{k,\pi(1)},\dots,spk_{k,\pi(\ell)},spk'_k$$
Ballot [ballotThree] permutes the ciphertexts included in Ballot [ballotOne], thereby deriving a ballot for a different candidate (with the exception of an abstention vote). The adversary can cast Ballot [ballotThree] and it is trivial to witness that this ballot will be accepted by the bulletin board, since $spk_{k,\pi(1)},\dots,spk_{k,\pi(\ell)},spk'_k$ are all valid signatures of knowledge. It follows that we have shown another technique to violate ballot independence in Helios: observing another voter’s interaction with the election system allows a voter to cast a *different* vote, with the exception of abstention votes which will be the *same*. (The ability to cast different votes may be of independent interest, for example, a voter can cast a distinct vote from their boss.) The absence of ballot independence can be exploited to violate privacy.
#### Violating privacy.
The decrypted tally reveals the number of votes for each candidate and this data can be used to discover how each voter voted. First, if the tally contains votes for three distinct candidates, then there exists integers $i,j\in\{1,\dots,\ell\}$ such that $\pi(i) = j$ and the voter with identity $id_k$ voted for candidate $t_i$. Secondly, if the tally contains two votes for a candidate and one vote for another candidate, then the voter with identity $id_k$ voted for the candidate with two votes. Finally, in the case where the outcome is unanimous, every vote is revealed[^1]
### Malformed ciphertext attack
Given the Ballot [ballotOne], the adversary can select an integer $v\in\{1,\dots,\ell\}$ and proceed as follows.
#### Constructing a related ballot.
The adversary constructs the Ballot [ballotMalformed], namely, $$\begin{gathered}
\label{ballotMalformed}
\underbrace{(1,1),\dots,(1,1)}_{\textrm{$v-1$ times}},
(a_{k,v}, b_{k,v}),
\underbrace{(1,1),\dots,(1,1)}_{\textrm{$\ell-v$ times}},\\
\widebar{spk}_1,\dots,\widebar{spk}_{v-1},spk_{k,v},\widebar{spk}_{v+1},\dots,\widebar{spk}_{\ell}, spk_{k,v}
\end{gathered}$$ such that for all $j \in\{1,\dots,v-1,v+1,\dots,\ell\}$ we have $\widebar{spk}_j = (\hat a_{j},\hat b_{j},\hat c_{j},\hat s_{j},\hat a'_{j},\hat b'_{j},\linebreak\hat c'_{j},\hat s'_{j})$ where $\hat c'_{j},\hat s'_{j}, \hat s_{j}\in_R \mathbb{Z}_q^*$ and $$\begin{array}{lcl}
\hat a_{j} &=& g^{\hat s_{j}} \bmod p \\
\hat a'_{j} &=& g^{\hat s'_{j}} \bmod p \\
\hat b_{j} &=& h^{\hat s_{j}} \bmod p \\
\hat b'_{j} &=& h^{\hat s'_{j}} \cdot g^{\hat c'_{j}} \bmod p \\
\hat c_{j} &=& \mathcal{H}(\hat a_{j},\hat b_{j},\hat a'_{j},\hat b'_{j}) - \hat c'_{j} \bmod q
\end{array}$$
By definition of Ballot [ballotOne], it is trivial to witness that $spk_{k,v}$ is a valid proof for $(a_{k,v}, b_{k,v})$ and, therefore, $spk_{k,v}$ is a valid proof for the homomorphic combination of ciphertexts encapsulated in Ballot [ballotMalformed]. Moreover, the following lemma demonstrates that for all $j \in\{1,\dots,v-1,v+1,\dots,\ell\}$ we have $\widebar{spk}_j$ is valid proof for $(1,1)$. We stress that Lemma 1 does not violate the soundness property of our signature of knowledge scheme for disjunctive proofs of equality between discrete logs (Section 2.2) because $\log_g a = \log_h b$ or $\log_g a = \log_h b/g^{m}$ holds for $(a,b) = (g^0,h^0)$.
**Lemma 1**. *The signature $(\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s')$ is valid for $(1,1)$, where $\bar c',\bar s', \bar s\allowbreak\in_R \mathbb{Z}_q^*$, $\bar a = g^{\bar s} \pmod p$, $\bar a' = g^{\bar s'} \pmod p$, $\bar b = h^{\bar s} \pmod p$, $\bar b' = h^{\bar s'} \cdot g^{\bar c'} \pmod p$, and $\bar c = \mathcal{H}(\bar a,\bar b,\bar a',\bar b') - \bar c' \pmod q$.*
**Proof.* Suppose the signature $(\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s')$ is defined above and let $(a,b)\allowbreak = (1,1)$. We must show that $(a,b)$ and $(\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s')$ satisfy the conditions of the verification algorithm described in Section 2.2. Since $a^{\bar c} = 1$ and $(b/g^0)^{\bar c} = 1$, we trivially derive $g^{\bar s} \equiv \bar a\cdot a^{\bar c} \pmod p$ and $h^{\bar s} \equiv \bar b\cdot (b/g^0)^{\bar c} \pmod p$. Moreover, since $a^{\bar c'} = 1$ and $(b/g^1)^{\bar c'} = g^{-\bar c'}$, it follows that $g^{\bar s'} \equiv \bar a'\cdot a^{\bar c'} \pmod p$ and $h^{\bar s'} \equiv \bar b' \cdot (b/g^1)^{\bar c'} \pmod p$. Finally, recall $\bar c = \mathcal{H}(\bar a,\bar b,\bar a',\bar b') - \bar c' \pmod q$ and therefore $\mathcal{H}(\bar a,\bar b,\bar a',\bar b') \equiv \bar c + \bar c' \pmod q$, concluding our proof. ◻*
It follows immediately that the adversary’s Ballot [ballotMalformed] will be accepted by the bulletin board, hence, we have shown another technique to violate ballot independence in Helios: observing another voter’s interaction with the election system allows a voter to cast a *meaningfully related* vote, in particular, if a voter votes for candidate $t_v$ or $\epsilon$, then the *same* vote can be cast, otherwise, a *different* vote (namely, $\epsilon$) can be cast. The absence of ballot independence can be exploited to violate privacy.
#### Violating privacy.
The homomorphic addition of ballots reveals the encrypted tally $(A_1,B_1),\dots,(A_\ell,B_\ell)$ defined as follows: $$\begin{gathered}
(a_{1,1} \cdot a_{2,1},\;b_{1,1} \cdot b_{2,1}),\dots,
(a_{1,v-1} \cdot a_{2,v-1},\;b_{1,v-1} \cdot b_{2,v-1}),\\
(a_{1,v} \cdot a_{2,v} \cdot a_{k,v},\;b_{1,v} \cdot b_{2,v} \cdot b_{k,v}),\\
(a_{1,v+1} \cdot a_{2,v+1},\;b_{1,v+1} \cdot b_{2,v+1}),\dots,
(a_{1,\ell} \cdot a_{2,\ell},\;b_{1,\ell} \cdot b_{2,\ell})
\end{gathered}$$ Given the partial decryptions, the tally can be decrypted to reveal the number of votes for each candidate. If the tally contains two votes for some candidate, one vote for some other candidate, and no votes for abstention, then the honest voter with identity $id_k$ must have cast a vote for the candidate with two votes and hence privacy is not preserved. A straightforward derivative of this attack allows privacy to be violated when candidate $t_v$ receives one vote, since the adversary learns that the voter with identity $id_k$ did not vote for this candidate and therefore must have voted for the candidate with the remaining vote.
### Homomorphic attack
Following from the methodology introduced by the malformed ciphertext attack (Section 3.2.3), we propose an attack that allows an adversary to construct a ballot related to an abstention vote cast by an honest voter. The attack proceeds as follows.
#### Constructing a related ballot.
The adversary constructs the Ballot [ballotHomomorphic], namely, $$\label{ballotHomomorphic}
(a_{k,1} \cdot\ldots\cdot a_{k,\ell}, \; b_{k,1} \cdot\ldots\cdot b_{k,\ell}),\underbrace{(1,1),\dots,(1,1)}_{\textrm{$\ell-1$ times}},
spk'_k, \widebar{spk}_2,\dots,\widebar{spk}_{\ell}, spk'_k$$ where for all $2 \leq i \leq \ell$ the signature $\widebar{spk}_i$ is constructed in accordance with the definition given in Lemma 1. It follows immediately for all $2 \leq i \leq \ell$ that $\widebar{spk}_i$ is a valid proof for $(1,1)$. Moreover, by definition of Ballot [ballotOne], it is trivial to witness that $spk'_k$ is a valid proof for $(a_{k,1} \cdot\ldots\cdot a_{k,\ell}, \; b_{k,1} \cdot\ldots\cdot b_{k,\ell})$ and, therefore, $spk'_k$ is a valid proof for the homomorphic combination of ciphertexts encapsulated in the Ballot [ballotHomomorphic]. It follows that the adversary’s Ballot [ballotHomomorphic] will be accepted by the bulletin board, hence, we have shown another technique to cast a *meaningfully related* vote, in particular, if a voter cast an abstention vote, then the *same* vote can be cast, otherwise, a *different* vote (namely, a vote for candidate $t_1$) can be cast. The absence of ballot independence can again 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} \cdot\ldots\cdot a_{k,\ell},\;b_{1,1} \cdot b_{2,1} \cdot b_{k,1} \cdot\ldots\cdot b_{k,\ell}),
(a_{1,2} \cdot a_{2,2},\;b_{1,2} \cdot b_{2,2})
\dots,
(a_{1,\ell} \cdot a_{2,\ell},\;b_{1,\ell} \cdot b_{2,\ell})$. If the decrypted tally contains two votes for abstention and one vote for some candidate, then the voter with identity $id_k$ cast a vote for abstention and hence privacy is not preserved.
### Further malleability attacks
A further variant that exploits malleability has been introduced by Bernhard (Bernhard 2012) and, concurrently, Desmedt & Chaidos (Desmedt and Chaidos 2012a, 2012b). We recall the details here for completion. Given the Ballot [ballotOne], the adversary selects $r_1,\dots,r_{\ell} \in\mathbb{N}$ and constructs the Ballot [ballotBernhard], namely, $$\label{ballotBernhard}
\widebar{ciph}_{k,1},\dots,\widebar{ciph}_{k,\ell},\widebar{spk}_{k,1},\dots,\widebar{spk}_{k,\ell},\widebar{spk}'_k$$ such that for all $j\in\{1,\dots,\ell\}$ we have $$\begin{array}{lcl}
\widebar{ciph}_{k,j} &=& (a_{k,j}\cdot g^{r_j},\; b_{k,j}\cdot h^{r_j})\\
\widebar{spk}_{k,j} &=& (\bar a_{k,j},\bar b_{k,j},\bar c_{k,j},\bar s_{k,j} + r_j \cdot c_{k,j},\bar a'_{k,j},\bar b'_{k,j},\bar c'_{k,j},\bar s'_{k,j} + r_j \cdot \bar c_{k,j})\\
\widebar{spk}'_k &=& (\bar a_k,\bar b_k,\bar c_k,\bar s_k + r \cdot \bar c_{k}, \bar a'_k,\bar b'_k,\bar c'_k,\bar s'_k + r \cdot \bar c'_{k})
\end{array}$$ where $r = r_1+\ldots+ r_\ell$. As shown by Bernhard (Bernhard 2012), the signatures of knowledge $\widebar{spk}_{k,1},\dots,\widebar{spk}_{k,\ell},\widebar{spk}'_{k}$ are valid (Lemma 2).
**Lemma 2**. *If $(\bar a,\bar b,\bar c,\bar s,\bar a',\bar b',\bar c',\bar s')$ is a signature for $(a,b)$, then $(\bar a,\bar b,\bar c,\bar s + r \cdot \bar c, \bar a',\bar b',\bar c',\bar s' + r \cdot \bar c')$ is a signature for $(a\cdot g^r,\; b\cdot h^r)$, where $r\in\mathbb{N}$.*
It follows that the adversary’s ballot ([ballotBernhard]) will be accepted by the bulletin board and privacy can be violated as described in Section 3.1.
### Attacks against the software implementation of Helios
The variants described in Sections 3.2.1 – 3.2.5 have been successfully launched against the Helios 3.0 implementation. Moreover, given Ballot [ballotOne] as input, a PHP script has been written to construct each of the related Ballots [ballotTwo] – [ballotBernhard].
## Generalised attack and French election case study
Our attack (Section 3.1) demonstrates that the ballot of an arbitrary voter can be replayed by any other voter and we have shown how privacy can be violated in elections with three voters. However, in general, the attack does not apply to elections with more than three voters, nonetheless, some information is leaked, and colluding voters can replay sufficiently many ballots to violate a voter’s privacy. 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. (We limit discussion to the replay attack described in Section 3.1 for simplicity and stress that the variants of our attack presented in Section 3.2 can be similarly used in elections with more than three voters.) 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.
#### Limitations.
For such an attack based upon a statistical model, we acknowledge that this model is rather naïve. For example, the attacker can never be certain that the distribution of votes follows from a previous election or a poll, in particular, differences may arise from changes in voter behaviour. Nevertheless, we believe our model is sufficiently indicative to illustrate the real threat of an attack against privacy. A definitive mathematical analysis could 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 (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 small number of voters to reveal a voter’s vote, furthermore, the final outcome of the election would not change as it is based on 75350 eligible voters.
# Solution: Ballot independence
Our attacks exploit the possibility of replaying a voter’s ballot, or a variant of the 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.
## Ballot weeding
The ballots cast by the adversary in our attacks can all be identified. Accordingly, we propose a solution which identifies and rejects such ballots. First, we assume that the signature of knowledge scheme (Section 2.2) is revised to ensure non-malleability, in particular, this will ensure that the response components of signatures cannot be changed. Secondly, we assume that the decryption algorithm will only decrypt ciphertexts $(a,b)$, where $a,b\in\mathbb{Z}_p^*$. Finally, the election officer should reject any ballot that contains a ciphertext that already exists on the bulletin board (this check can be performed in Step [step:submit] of the protocol execution, see Section 2.3). Witness that our first constraint eliminates the attacks described in Sections 3.2.1 & 3.2.5, the second eliminates the attacks described in Sections 3.2.3 & 3.2.4, and the final constraint eliminates those in Sections 3.1 & 3.2.2 (the attack described in Section 3.2.3 can also be eliminated by the final constraint). This solution is simple and can easily be implemented in a future version of Helios.
## Binding ballots to voters
Ballot weeding requires additional cryptographic assumptions and a special mechanism to reject ballots meaningfully related to those already present on the bulletin board. In this section, we propose techniques to prevent the construction of meaningfully related ballots that will be accepted by the bulletin board, namely, we bind the link between a voter and her ballot; it follows that any meaningfully related ballot constructed by the adversary will be rejected by the bulletin board because the ballot is not bound to the adversary.
#### Unique identifiers.
Based upon inspiration from Gennaro (Gennaro 1995, sec. 4.2), Cramer, Gennaro & Schoenmakers (Cramer, Gennaro, and Schoenmakers 1997), and Damgård, Jurik & Nielsen (Damgård and Jurik 2001; Damgård, Jurik, and Nielsen 2010), we use unique identifiers to ensure that signatures of knowledge are associated with distinct voters. This is achieved by including the voter’s identity in the challenges used by signatures of knowledge. More precisely, given a voter’s identity $id$, the sign algorithm (Section 2.2) 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},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 the voter with identity $id$, the verifier should check $\mathcal{H}(a_{\sf min},b_{\sf min},\dots,a_{\sf max},b_{\sf max},id) \equiv\linebreak \sum_{{\sf min}\leq i \leq {\sf max}} c_i \pmod q$.
#### Eligibility verifiability.
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.
## Critique of our solutions
Our *ballot weeding* solution is particularly 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. 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 *unique identifiers* solution would necessarily require that the voter’s identity be revealed to the ballot encryption device. Moreover, extending Helios to provide eligibility verifiability would require a considerable extension to the Helios code-base. Accordingly, we adopt the ballot weeding 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
In this section, we formally prove that our solution is sufficient for ballot secrecy using the applied pi calculus (Abadi and Fournet 2001; M. D. Ryan and Smyth 2011).
## Applied pi calculus
Let us recall the applied pi calculus. 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 article. 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'$.*
Definitions of observational equivalence and labelled bisimilarity have been shown to coincide (Liu 2011).
## 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. $$\Sigma = \{\mathsf{ok},\mathsf{zero},\mathsf{one},\perp,\mathsf{fst},\mathsf{snd},\mathsf{pair},*,+,\circ,\mathsf{partial},\mathsf{checkspk},\mathsf{penc},\mathsf{spk},\mathsf{dec}\}$$ 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 the 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, we occasionally abbreviated $\mathsf{pair}(M_1, \mathsf{pair}(\dots, \mathsf{pair}(M_n, \perp)))$ 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{zero}+ \mathsf{zero}= \mathsf{zero}\label{eq:addition2}\\[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 }}) \label{eq:combination} \\
&&\hspace{-11mm}\qquad=\mathsf{penc}(x_{\mathsf{pk }},y_{\mathsf{rand }}\circ z_{\mathsf{rand }},y_{\mathsf{plain }}+z_{\mathsf{plain }})\nonumber\\[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,\allowbreak 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},\allowbreak\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,\allowbreak 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\*
- Ballots which contain a ciphertext that already exists on the bulletin board 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.
The trusted components are modelled by the administration process $A^{\phi}_{\ell,n}$ and voting process $V_{\ell}$ defined in Figure 4. For generality, the voting process $V_{\ell}$ is parametrised by the number of candidates $\ell$. Similarly, the administration process $A^{\phi}_{\ell,n}$ is parametrised by the number of candidates $\ell$, the number of voters $n$, and a formula $\phi$; the formula $\phi$ defines 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*.
Let ℓ be some number of candidates, n ≥ 2 be some number of voters, and ϕ be a Helios process specification. The administration process Aℓ, nϕ and voting process Vℓ are defined below. $$\begin{array}{lcl}
V_{\ell}&=& \nu\,r_1 \mathrel.\\
&& \textnormal{let } ciph_1=\mathsf{penc}(z_{\mathsf{pk }},r_1,x^{\mathsf{vote}}_{1}) \textnormal{ in }\\
&& \textnormal{let } spk_1=\mathsf{spk}(z_{\mathsf{pk }},r_1,x^{\mathsf{vote}}_{1},ciph_1)) \textnormal{ in }\\
&& \vdots \\
&& \nu\,r_\ell \mathrel.\\
&& \textnormal{let } ciph_\ell=\mathsf{penc}(z_{\mathsf{pk }},r_\ell,x^{\mathsf{vote}}_{\ell}) \textnormal{ in }\\
&& \textnormal{let } spk_\ell=\mathsf{spk}(z_{\mathsf{pk }},r_\ell,x^{\mathsf{vote}}_{\ell},ciph_\ell)) \textnormal{ in }\\
&& \textnormal{let } \hat r=r_1\circ \dots \circ r_\ell \textnormal{ in } \\
&& \textnormal{let } \widehat{ciph}=ciph_1 * \dots * ciph_\ell \textnormal{ in } \\
&& \textnormal{let } \widehat{vote}=x^{\mathsf{vote}}_{1}+\dots+x^{\mathsf{vote}}_{\ell} \textnormal{ in } \\
&&\textnormal{let } \widehat{spk}=\mathsf{spk}(z_{\mathsf{pk }},\hat r,\widehat{vote},\widehat{ciph}) \textnormal{ in }\\
&&\overline{x_{\mathsf{auth }}}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{ciph_1,\dots,ciph_\ell,\,spk_1,\dots,spk_\ell,\,\widehat{spk}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\
\\
A^{\phi}_{\ell,n}&=& \nu\,sk_T,a_1,a_2,d\mathrel.(\_ \mid BB^{\phi}_{\ell,n}\mid T_\ell\mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\})\\
\\
BB^{\phi}_{\ell,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_{\ell,2}\{\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_{\ell,n-1}\{\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_1=\pi_{1}(y_1) *\allowbreak \dots *\allowbreak \pi_{1}(y_n) \textnormal{ in }\\
&& \cdots\textnormal{let } tally_\ell=\pi_{\ell}(y_1) *\allowbreak \dots *\allowbreak \pi_{\ell}(y_n) \textnormal{ in }\\
&& \overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{tally_1,\dots,tally_\ell}\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_1),\dots,\mathsf{dec}(\pi_{\ell}(y_{\mathsf{partial }}),tally_\ell)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\\
\\
T_\ell& = & 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} })),\dots,\mathsf{partial}(sk_T,\pi_{\ell}(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_{\ell,\bar n}$ is a *Helios process specification*, if $\textnormal{fv}(\phi_{\ell,\bar n}) \subseteq \{y_1,\dots,y_{\bar n},\allowbreak y_{\mathsf{ballot }},\allowbreak z_{\mathsf{pk }}\}$.*
The voting process $V_{\ell}$ contains free variables $x^{\mathsf{vote}}_{1},\dots,x^{\mathsf{vote}}_{\ell}$ to represent the voter’s vote (which is expected to be encoded using 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_{\ell}$ corresponds to the description of the browser script (Figure 1). The administration process $A^{\phi}_{\ell,n}$ is parametrised by the number of candidates $\ell$, the number of voters $n$, and a 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$ and $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}_{\ell,n}$ represents the bulletin board and $T_\ell$ 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.
The voting process $V_{\ell}$ is parametrised by a substitution $\sigma$, where variables $x^{\mathsf{vote}}_{1},\dots,x^{\mathsf{vote}}_{\ell}\in \textnormal{dom}(\sigma)$; these variables must be parametrised to encode a vote for at most one candidate, that is, there exists at most one integer $i\in\{1,\dots,\ell\}$ such that $\Sigma\vdash x^{\mathsf{vote}}_{i}\sigma = \mathsf{one}$. Formally, we define valid parametrisations using the notion of *candidate substitutions*.
**Definition 4** (Candidate substitution). *Given some number of candidates $\ell$ and a substitution $\sigma$, we say $\sigma$ is a *candidate substitution* if $$\Sigma \vdash (x^{\mathsf{vote}}_{1} + \dots + x^{\mathsf{vote}}_{\ell})\sigma = \mathsf{zero}\vee
\Sigma \vdash (x^{\mathsf{vote}}_{1} + \dots + x^{\mathsf{vote}}_{\ell})\sigma = \mathsf{one}$$*
It follows immediately that bitstrings $m_1,\dots,m_\ell$ generated during Step [step:ballot] of Figure [fig:ballot] can be modelled as candidate substitutions.
The application of our model is demonstrated in the following example.
**Example 2**. *Let $\ell$ be some number of candidates, $n \geq 2$ be some number of voters, and $\phi$ be a Helios process specification. An election with voters $\mathcal{A}$ and $\mathcal{B}$ who select candidate substitutions $\sigma$ and $\tau$, and such that the other $n-2$ voters are controlled by the adversary, can be modelled by the process $A^\phi_{\ell,n}[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]$.*
#### 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}}_{\ell,n}$ where the Helios process specification $\phi^{\sf orig}$, parametrised by the number of candidates $\ell$, is defined as follows. $$\begin{gathered}
\phi^{\sf orig}_\ell\triangleq
\mathsf{checkspk}(z_{\mathsf{pk }},\pi_{1}(y_{\mathsf{ballot }}) * \dots * \pi_{\ell}(y_{\mathsf{ballot }}),\pi_{2\cdot\ell+ 1}(y_{\mathsf{ballot }})) = \mathsf{ok}\mathrel\wedge \\
\mathsf{checkspk}(z_{\mathsf{pk }},\pi_{1}(y_{\mathsf{ballot }}),\pi_{\ell+ 1}(y_{\mathsf{ballot }})) = \mathsf{ok}\mathrel\wedge \dots \mathrel\wedge\\
\mathsf{checkspk}(z_{\mathsf{pk }},\pi_{\ell}(y_{\mathsf{ballot }}),\pi_{2\cdot\ell}(y_{\mathsf{ballot }})) = \mathsf{ok}
\end{gathered}$$ We have shown that these checks are insufficient to ensure ballot secrecy (Section 3). Our ballot weeding 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}$, parametrised by the number of candidates $\ell$ and number of ballots already on the bulletin board $\bar n$, defined as follows. $$\phi^{\sf sol}_{\ell,\bar n} \triangleq \phi^{\sf orig}_\ell\mathrel\wedge \pi_{2\cdot\ell+ 2}(y_{\mathsf{ballot }}) = {\perp} \mathrel{\wedge}
\bigwedge_{\substack{i,j\in\{1,\dots,\ell\},\\ k\in\{1,\dots,\bar n\}}} \pi_{i}(y_k) \not= \pi_{j}(y_{\mathsf{ballot }})$$ 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}$, parametrised by the number of candidates $\ell$ and number of ballots already on the bulletin board $\bar n$, defined below. $$\phi^{\sf ident}_{\ell,\bar n} \triangleq \phi^{\sf orig}_\ell\mathrel\wedge \pi_{6}(y_{\mathsf{ballot }}) = {\perp} \mathrel{\wedge} \bigwedge_{k\in\{1,\dots,\bar n\}} y_{\mathsf{ballot }}\not= y_k$$ 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 (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}$ and $\mathcal{B}$ 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 5.
**Definition 5** (Ballot secrecy). *Given a Helios process specification $\phi$, we say *ballot secrecy is satisfied* if for all integers $\ell\in \mathbb{N}^*$ and $n \geq2$, and for all candidates substitutions $\sigma$ and $\tau$, we have $$A^{\phi}_{\ell,n}{[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]}
\approx_l
A^{\phi}_{\ell,n}{[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau \mid V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]}$$*
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 series of the constant symbols $\mathsf{zero}$ and $\mathsf{one}$, such that their combination by application of the function $+$ is also a constant $\mathsf{zero}$ and $\mathsf{one}$; it follows that Definition 5 is a straightforward variant of the original.
The Helios 2.0 protocol does not satisfy our privacy definition (Lemma 3) and naïve weeding solutions are also insufficient (Lemma 4).
**Lemma 3**. *The Helios process specification $\phi^{\sf orig}$ does not satisfy ballot secrecy.*
Intuitively, the proof of Lemma 3 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 4.
**Lemma 4**. *The Helios process specification $\phi^{\sf ident}$ does not satisfy ballot secrecy.*
**Proof.* Consider $\ell= 2$, $n = 3$, $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{zero}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{one}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2}$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{one}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{zero}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2}$}}\}$. 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 following transitions*
*for some names $\tilde{n}$ and substitution $\tau_1$, such that: $$\mathsf{dec}(\pi_{1}(z),\pi_{1}(x)*\pi_{1}(y)*\pi_{2}(x))\tau_1 =_E\mathsf{one}+\mathsf{one}$$ This labelled transition has to matched by*
*for some names $\tilde{n}$ and substitution $\tau_2$, such that: $$%\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$$ 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.
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, at the time of writing, for two main reasons. Firstly, ProVerif cannot prove equivalences under the homomorphic equation (Equation [eq:combination]). Secondly, our theorem states ballot secrecy for any number $n$ of participants and ProVerif cannot handle parametrised processes (see Paiola & Blanchet (Paiola and Blanchet 2012, 2011; Paiola 2010) for some initial progress in this direction). We proceed by constructing a relation that relates ${A^{\phi}_{\ell,n}}[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]$ and ${A^{\phi}_{\ell,n}}[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau \mid\allowbreak V_{\ell}\{\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.
**Definition 6** (Valid ballot). *A term $T$ is said to be a *valid ballot* in an election with $\ell$ candidates if $[\! [ \phi^{\sf sol}_{\ell,0}\{\textnormal{\raisebox{2pt}{\footnotesize $T$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\} ]\! ] = \mathsf{true}$.*
By definition, the bulletin board accepts only valid ballots. A key step to proving static equivalence is to show that any valid ballot submitted to the bulletin board by the environment is “equivalent” to a term of the form $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}\mathsf{penc}(z_{\mathsf{pk }},N_1,M_1),\dots,\allowbreak\mathsf{penc}(z_{\mathsf{pk }},N_\ell,M_\ell),S_1,\dots,S_{\ell+1}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, where $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_\ell$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{\ell}$}}\}$ is a candidate substitution. This allows us to deduce that the election outcome produced by ${A^{\phi}_{\ell,n}}[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau]$ is exactly the same as in ${A^{\phi}_{\ell,n}}[V_{\ell}\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\tau\mid\allowbreak V_{\ell}\{\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 Appendix 11.
## 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 make use of a (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 – in the challenge hashes included within signatures of knowledge, similar to the methodology in Section 4.2). The administrative process $A^{\phi}_{\ell,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); this limitation could be overcome by parametrising $A^{\phi}_{\ell,n}$ with the channel names to restrict and by a minor unification of the bulletin process $BB^{\phi}_{\ell,n}$, however, this generalisation is of limited interest and would come at the cost of over-complicating the proof. In addition, the administrative process $A^{\phi}_{\ell,n}$ does not permit revoting. The signature and equational theory do not capture low-level technical details of public keys, in particular, we consider a single honest tallier and we do not model distributed keys nor signatures of knowledge to verify correct construction of both keys and partial decryptions (nonetheless, we include Equation [eq:partial] which models decryption of a ciphertext using a correctly constructed partial decryption). 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. We partly overcome these limitations in our further work (Bernhard et al. 2011) by presenting a variant of Helios that is provably secure in a cryptographic setting.
# Attacks against other schemes
This section demonstrates that the absence of ballot independence can be exploited in other electronic voting protocols to violate privacy. In particular, we demonstrate replay attacks against schemes by Sako & Kilian (Sako and Kilian 1994) and Schoenmakers (Schoenmakers 1999), and we show that the malleable cryptographic scheme adopted by Lee *et al.* (Lee et al. 2004) can be exploited to launch attacks.
## Exploiting replays in the protocol by Sako & Kilian
The Sako & Kilian (Sako and Kilian 1994) electronic voting scheme capitalises upon advances in cryptography to improve the Banaloh & Yung protocol (Benaloh and Yung 1986). The scheme is interesting because it was one of the first electronic voting protocols to adopt the Fiat-Shamir heuristic to derive non-interactive proofs (this evolution was key for the development of end-to-end verifiable electronic voting systems): a three-round zero-knowledge proof consisting of a commitment, challenge and response can be reduced to a non-interactive proof by replacing the challenge with a hash on the commitment. However, we show that the application of the Fiat-Shamir heuristic compromises ballot secrecy. In particular, the interactive nature of zero-knowledge proofs guarantees freshness, whereas, non-interactive proofs, derived using the Fiat-Shamir heuristic, do not assure freshness. This can be exploited by a replay attack to violate ballot secrecy.
### Protocol description
The scheme is based upon a pair of *partially compatible homomorphic encryption* functions, that is, a pair of functions $f_{1},f_{2}$ over $\mathbb{Z}_q$, where $q$ is prime, such that for all $i,j\in\{1,2\}$ the following properties are satisfied:
- $f_{i}(x+y) = f_{i}(x) \cdot f_{i}(y)$, where $x,y\in\mathbb{Z}_q$
- Distributions $(f_{i}(x),f_{j}(y))$ and $(f_{i}(x),f_{j}(x))$ are computationally indistinguishable, where $x$ and $y$ are chosen uniformly in $\mathbb{Z}_q$.
The voting protocol is defined for $m\in\mathbb{N}$ voters as follows.
#### Setup.
Talliers $\mathcal{T}$ and $\mathcal{T}'$ publish public keys $k$ and $k'$ for a public key encryption scheme $E$ (which need not be homomorphic).
#### Voting.
Given vote $v_i\in\{-1,1\}$, the voter generates nonces $x_i,x'_i\in\mathbb{Z}_q$ such that $v_i = x_i + x'_i$ and constructs her ballot as follows: $$\begin{array}{lcl}
Y_i &=& f_{1}(x_i)\\
Y'_i &=& f_{2}(x'_i)\\
Z_i &=& E(k,x_i)\\
Z'_i &=& E(k',x'_i)
\end{array}$$ In addition, the voter is required to prove $x_i + x'_i \in \{1,-1\}$ in zero-knowledge. However, to avoid an interactive proof, the Fiat-Shamir heuristic is applied to derive a signature of knowledge $\sigma_i$. (For brevity we omit the construction of $\sigma_i$, see (Sako and Kilian 1994, fig. 1) for details.)
#### Tallying.
Given ballots $Y_1,Y'_1,Z_1,Z'_1,\sigma_1,\dots,Y_n,Y'_n,Z_n,Z'_n,\sigma_n$, tallier $\mathcal{T}$ decrypts each $Z_i$ to recover $\hat x_i$ and checks $Y_i = f_{1}(\hat x_i)$, similarly, tallier $\mathcal{T}'$ decrypts $Z'_i$ to recover $\hat x'_i$ and checks $Y'_i = f_{1}(\hat x'_i)$; the talliers also check the signature of knowledge $\sigma_i$. The talliers publish $V = \sum_{i=1}^m \hat x_i$ and $V' = \sum_{i=1}^m \hat x'_i$, and the result is $T = V + V'$, which can be verified by checking $f_{1}(V) = \prod_{i=1}^m Y_i$ and $f_{2}(V') = \prod_{i=1}^m Y'_i$.
### Attacking ballot secrecy
We show that the voting protocol by Sako & Kilian does not satisfy ballot secrecy, by presenting a replay attack which allows an adversary to reveal a voter’s vote. Intuitively, an adversary may observe the ballot posted by a particular voter 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.
Let us consider an election with 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 adversary has observed the ballot $$Y_k,Y'_k,Z_k,Z'_k,\sigma_k$$ being cast by the voter whose privacy will be compromised.
#### Replaying a ballot.
As shown by Gennaro (Gennaro 1995), an adversary can replay the ballot $Y_k,Y'_k,Z_k,Z'_k,\sigma_k$, thereby violating ballot independence. (The violation of ballot independence is due to the adversary’s ability to cast the *same* vote as the honest voter.) Since the ballot was constructed by an honest voter, it is trivial to see that it will be considered valid by the talliers. We will now show how the lack of ballot independence can be exploited to violate privacy.
#### Violating privacy.
The bulletin board will be constructed as follows $$Y_1,Y'_1,Z_1,Z'_1,\sigma_1,Y_2,Y'_2,Z_2,Z'_2,\sigma_2,Y_k,Y'_k,Z_k,Z'_k,\sigma_k,V,V'$$ where $k\in\{1,2\}$, $V = x_1 + x_2 + x_k$ and $V' = x'_1 + x'_2 + x'_k$. It follows from the protocol description that $v_i = x_i + x'_i$, where $i\in\{1,2,k\}$, and the result $T = V + V' = v_1 + v_2 + v_k$. Since there will be at least two votes for the candidate voter $id_k$ voted for, the voter’s vote can be revealed: if $T \geq 2$, then $v_k = 1$; otherwise $v_k = -1$. It follows that the voter’s privacy has been compromised; moreover, the vote of the remaining honest voter is $T - 2 \cdot v_k$.
### Independence and the Fiat-Shamir heuristic
The interactive nature of zero-knowledge proofs guarantees freshness, because every proof contains a unique challenge, and this ensures independence. By comparison, non-interactive proofs, derived using the Fiat-Shamir heuristic, do not assure freshness, in particular, non-interactive proofs can be replayed. As a consequence, application of the Fiat-Shamir heuristic may compromise the security of cryptographic protocols and we have shown how application of the heuristic erodes privacy in the electronic voting scheme by Sako & Kilian. This demonstrates that the use of the Fiat-Shamir heuristic requires some care and highlights the necessity for thorough security analysis.
### Generalising replay attacks
The replay attack against Helios, and the voting protocol by Sako & Kilian, can be generalised to other schemes where an adversary can observe a ballot cast by a particular voter and replay this ballot verbatim. In particular, the voting protocol by Schoenmakers (Schoenmakers 1999) fits this description.
#### Exploiting replays in the protocol by Schoenmakers.
The electronic voting protocol by Schoenmakers (Schoenmakers 1999) is based upon (Cramer et al. 1996; Cramer, Gennaro, and Schoenmakers 1997). The scheme explicitly aims to provide efficient small-scale elections (for example, boardroom elections) and, given that our attack is particularly well suited to small-scale elections, we find it interesting to study the possibility of violating ballot secrecy in this setting. Ballot independence is not provided (Schoenmakers 1999, sec. 5) and we exploit privacy using a replay attack. The attack description is straightforward and follows immediately from our discussion; accordingly, we omit the details and refer the interested reader to our technical report (Smyth and Cortier 2011, sec. 3).
### Possible solutions: Weeding duplicate ballots
Our attacks against the voting protocols by Sako & Kilian and Schoenmakers exploit the possibility of replaying a voter’s ballot without detection. We believe it should be sufficient for the election officer to reject any duplicate ballots to ensure ballot secrecy, alternatively, the *unique identifiers* solution (Section 4.2) may also be suitable. Proving the security of these solutions remains an open problem.
## Exploiting malleability in the protocol by Lee *et al.*
The Lee *et al.* (Lee et al. 2004) electronic voting scheme adopts an offline tamper-resistant hardware device to ensure receipt freeness; more precisely, the hardware device takes an ElGamal encrypted vote as input and outputs a re-encrypted ciphertext, this prevents a voter proving how she voted by reconstruction as she does not know the nonce introduced for re-encryption. In addition, the hardware device provides a Designated Verifier Proof of re-encryption, thereby allowing the voter to verify that the device behaved correctly. The device is assumed to be offline and, hence, communication between the voter and the device is assumed to be untappable.
### Background: Multiplicative homomorphic ElGamal
The scheme uses multiplicative homomorphic ElGamal, rather than the additive variant presented in Section 2.1. The operations for key generation, homomorphic combination and re-encryption are standard; albeit, the result of homomorphic combination is the multiplication of plaintexts, rather than the addition of plaintexts. We recall the operations for encryption and decryption below.
#### 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,\;m \cdot h^r \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 = b/(k_1 \cdot \ldots \cdot k_n) \bmod p$.
The application of these primitives to derive the scheme by Lee *et al.* will be discussed in the next section.
### Protocol description
An election is created by naming an election officer, selecting a set of mixers, and choosing a set of trustees. The trustees generate a distributed public key pair and the election officer publishes the public key on the bulletin board. (For robustness, threshold ElGamal may be used; we omit these details for brevity.) The election officer also publishes the candidate list, the public keys of eligible voters, and the public keys of the tamper-resistant hardware devices. Informally, the steps that the participants take during an election are as follows.
1. The voter constructs an ElGamal ciphertext $(a,b)$ containing her vote $v$ and sends the ciphertext to her tamper-resistant hardware device.
2. The hardware device re-encrypts the voter’s ciphertext to produce $(a',b')$ and computes a Designated Verifier Proof of re-encryption $\tau$. The device also derives a signature $\sigma$ on the re-encryption. The hardware device returns $(a',b'),\sigma,\tau$ to the voter.
3. If the signature and proof are valid, then the voter generates a signature $\sigma'$ on the message $\sigma$ using her private key. The voter submits her ballot $(a',b'),\sigma,\sigma'$ to the bulletin board.
4. Individual voters can check that their ballots appear on the bulletin board and can be assured that the ciphertext $(a',b')$ contains their vote $v$ by verifying the Designated Verifier Proof $\tau$.
5. Voters and observers can check that ballots were cast by registered voters by verifying signatures $\sigma'$, and are assured that each voter cast at most one ballot by checking that no voter signed two values. In addition, voters and observers should verify signatures $\sigma$ for receipt freeness.
6. After some predefined deadline, valid ballots (that is, ballots associated with valid signatures $\sigma$ and $\sigma'$) are submitted to the mixers. Anyone can check that mixing is performed correctly.
7. Each of the trustees publishes a partial decryption for every ciphertext output by the mix. Anyone can verify these proofs.
8. The election officer decrypts each ciphertext and publishes the election result. Anyone can check these decryptions.
See Lee *et al.* (Lee et al. 2004) for further details.
### Attacking ballot secrecy
We show that the voting protocol by Lee *et al.* (Lee et al. 2004) does not satisfy ballot secrecy by recalling the attack by Dreier, Lafourcade & Lakhnech (Dreier, Lafourcade, and Lakhnech 2011) that exploits malleability to reveal a voter’s vote. Intuitively, an adversary may identify a voter’s encrypted vote on the bulletin board, since it is signed by the voter. This ciphertext can be submitted to a tamper-resistant hardware device (possibly after re-encryption) and the device will return $(\hat a, \hat b),\hat\sigma,\hat\tau$; the ballot $(\hat a, \hat b),\hat\sigma,\hat\sigma'$ can then be submitted by the adversary to the bulletin board, where $\hat\sigma'$ is a signature on $\hat\sigma$ constructed by a registered voter under the adversary’s control. As explained in Section 6.1.2, 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.
#### Variant exploiting homomorphic encryption.
The adversary can exploit the homomorphic properties of ElGamal to avoid casting the *same* vote as an honest voter. In this variant, suppose the adversary wants to recover the vote from ballot $(a'_k,b'_k),\sigma_k,\sigma'_k$, the adversary derives the ciphertext $(c,d) = (a'_k,b'_k) \cdot (c',d')$, where $(c',d')$ is an ElGamal ciphertext containing some message $m$. The adversary submits the ciphertext $(c,d)$ to a tamper-resistant hardware device and the device will return $(\hat c, \hat d),\hat\sigma,\hat\tau$; the ballot $(\hat c, \hat d),\hat\sigma,\hat\sigma'$ can be submitted by the adversary to the bulletin board, where $\hat\sigma'$ is a signature on $\hat\sigma$ constructed by a registered voter. The output of the mix will include the adversaries re-encrypted ciphertext and the election officer will publish $m \cdot v$ on the bulletin board, where ciphertext $(a'_k,b'_k)$ includes the vote $v$. This variant of the attack is interesting because the adversary’s ballots are undetectable, in particular, weeding ballots would clearly not be sufficient to ensure privacy.
### Exploiting replays in protocols based upon mixnets
In homomorphic election schemes, voters encrypt their votes and ciphertexts are homomorphically combined before decryption. By comparison, in mixnet election schemes, voters encrypt their votes, ciphertexts are shuffled, and individual ciphertexts are decrypted. (The decryption of individual ciphertexts in mixnet elections can provide an advantage over homomorphic elections, since ballot construction can be simplified, for example, the number of ciphertexts used by Helios corresponds to the number of candidates, whereas, one ciphertext is sufficient in mixnet elections.) Privacy is ensured in homomorphic election schemes by never revealing the contents of individual ciphertexts, whereas, privacy is ensured in mixnet election schemes by breaking the link between the mix’s input and output. As highlighted by Pfitzmann & Pfitzmann (Pfitzmann and Pfitzmann 1989), independence is necessary in mixnets because the input ciphertexts are eventually decrypted, therefore, any meaningfully related ciphertexts input to the mixnet can be meaningfully related once the mix’s output is decrypted. In the context of electronic voting, it follows that a voter’s privacy can be violated if an adversary can construct a ciphertext meaningfully related to the voter’s ciphertext and the election result contains exactly two votes satisfying the adversary’s relation.
# Relationships between security properties
The variants of our attack (Section 3.2) abuse ballot malleability to violate privacy and our ballot weeding solution achieves privacy by ensuring ballots are independent. In this section, we study the relationships between independence and privacy, and independence and malleability.
## Independence and privacy are unrelated properties
In the context of Helios, we have shown that ballot independence is sufficient for ballot secrecy, however, we will now present examples that suggest independence and privacy are unrelated in a more general context.
#### A protocol with independence but no privacy.
Consider a variant of the fixed Helios voting scheme in which each of the trustees publish a partial decryption of individual ciphertexts (rather than a partial decryption of the homomorphically combined ciphertexts, that is, the encrypted tally). Intuitively, this variant preserves ballot independence but does not satisfy ballot secrecy, since the partial decryptions allow votes to be recovered from ballots and the link between a voter and her ballot is known. Formally, this variant is captured by modelling the Helios administrator process as $\widebar A^{\phi^{\sf sol}}_n$, defined in Figure 5. The violation of ballot secrecy can be witnessed since $$\widebar A^{\phi^{\sf sol}}_2{[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]}
\not\approx_l
\widebar A^{\phi^{\sf sol}}_2{[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]}$$ where $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{zero}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{one}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2}$}}\}$ and $\tau = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{one}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{zero}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2}$}}\}$. Similarly, a further variant of the fixed Helios scheme in which each of the trustees publishes their private key at the end of the voting phase, rather than a partial decryption of the encrypted tally, also satisfies independence but not ballot secrecy.
Given the number of voters n ≥ 2 the administration process $\widebar A^{\phi^{\sf sol}}_n$ is defined below, where process T is presented in Figure 4. $$\begin{array}{lcl}
\widebar A^{\phi^{\sf sol}}_n &=& \nu\,sk_T,a_1,a_2,d\mathrel.(\_ \mid \widebar{BB}^{\phi^{\sf sol}}_n \mid {!T} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\})\\
\\
\widebar{BB}^{\phi^{\sf sol}}_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^{\sf sol}\{\textnormal{\raisebox{2pt}{\footnotesize $y_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\} \textnormal{ then }
\\
&& \cdots\ a_{n}(y_{n})\mathrel. \textnormal{if } \phi^{\sf sol}\{\textnormal{\raisebox{2pt}{\footnotesize $y_n$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\} \textnormal{ then }
\\
&& \overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(y_1),\pi_{2}(y_1)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\mathrel.d(z_1)\mathrel.\overline{c}\langle z_1\rangle\mathrel.\\
&& \cdots \mathrel . \overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\pi_{1}(y_n),\pi_{2}(y_n)}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\mathrel.d(z_n)\mathrel.\overline{c}\langle z_n\rangle
\end{array}$$
Helios administrator that preserves independence but not privacy
#### A protocol with privacy but no independence.
Consider a voting scheme in which each voter broadcasts their vote on an anonymous communication channel. Formally, the voter is modelled by the process $P = \overline{c}\langle x_{\mathsf{vote} }\rangle$, where variable $x_{\mathsf{vote} }$ is parametrised by the voter’s vote. For ballot secrecy it is sufficient to show $P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\} \mid P\{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\} \approx_l P\{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\} \mid P\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{vote} }$}}\}$ for all ground terms $M$ and $N$; this result trivially holds by structural equivalence and hence the scheme satisfies ballot secrecy. However, independence is intuitively violated in this setting, because an adversary may observe the voting system and replay a previously cast vote, that is, an adversary can cast the same vote as another voter (without knowing which voter). In addition, it follows that early results are available in this scheme.
We also expect some published electronic voting schemes based upon blind signatures to satisfy ballot secrecy but not independence; in particular, a more realistic example of a protocol that satisfies this property is the protocol by Fujioka, Okamoto & Ohta (Fujioka, Okamoto, and Ohta 1992) under the assumption that duplicates are not rejected. Indeed, independence can be violated by a verbatim replay of the signed committed vote.
Nonetheless, we believe a weaker property exists: *privacy and authenticated ballots implies independence*, where the term *authenticated ballot* means the link between an arbitrary ballot and associated voter is known (for example, our unique identifiers solution uses authenticated ballots). Informally, this can be witnessed as follows: suppose a system satisfies privacy and authenticated ballots but not independence, it follows that an adversary can identify a voter’s ballot and, since there is no independence, replay that ballot; privacy is then violated, as we have shown in this article, hence deriving a contradiction. In addition, Bernhard, Pereira & Warinschi (Bernhard, Pereira, and Warinschi 2012) propose a context where privacy implies independence.
## Non-malleability is stronger than independence
Non-malleability asserts that an adversary can only construct *meaningfully related* ballots if the related ballots are constructed by the adversary (Dolev, Dwork, and Naor 1991, 2000; Bellare et al. 1998). By comparison, given an election’s bulletin board, ballot independence asserts that an adversary can only construct a ballot which will be accepted by the bulletin board and be meaningfully related to an existing ballot on the board, if the adversary constructed both ballots. It intuitively follows that non-malleability implies ballot independence, since an adversary that is unable to construct a ballot meaningfully related to a non-adversarial ballot, is also unable to construct a ballot that will be accepted by an election’s bulletin board *and* be meaningfully related to a non-adversarial ballot from the bulletin board. By contrast, our ballot weeding solution (Section 4.1) suggests that non-malleability is not necessary for independence. Indeed, we have shown that an adversary can form several ballots that are meaningfully related to an initial one. All ballots are of the right format (in particular they contain a valid proof). In that sense, ballots are malleable. However, the additional checks of the ballot box (weeding duplicates) will reject them. Our unique identifier solution (Section 4.2) provides further evidence to support our claim that non-malleability is not necessary for independence. In this setting, a non-adversarial ballot from the bulletin board can be manipulated using all of the techniques defined in Section 3.2 to derive a meaningfully related ballot, nevertheless, if the adversary constructs such a ballot, then the ballot will be rejected by the bulletin board, because it is not bound to the adversary’s identity. Our examples therefore provide evidence to suggest that non-malleability is not necessary for independence.
## Discussion
In this article, we cannot make any definitive mathematical statements about the relationships between independence and privacy or independence and non-malleability, because independence has not been formally defined. Nonetheless, we hope this section provides some insight into the relationships we expect.
# Related work
Our attack against Helios relies upon the lack of ballot independence. The concept of independence was introduced by Chor *et al.* (Chor et al. 1985) and the possibility of compromising security properties due to the lack of independence has been considered, for example, in (Chor and Rabin 1987; Pfitzmann and Pfitzmann 1989; Pfitzmann 1994; 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. Sako & Kilian (Sako and Kilian 1995, sec. 2.4) and Michels & Horster (Michels and Horster 1996, sec. 3) discuss how the absence of ballot independence can be exploited to compromise privacy.
Our attack is also reliant on the voter’s ability to cast a ballot as a function of another voter’s ballot, for example, our basic attack (Section 3.1) applies the identity function and our variant in Section 3.2.2 performs a permutation on the ballot’s internal structure. In related work, Benaloh (Benaloh 1996) demonstrates that a simplified version of his voting scheme allows the administrator’s private key to be recovered by an adversary who constructs (and casts) a ballot as a function of other voters’ ballots.
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.
Other studies of Helios have also been conducted, in particular, Langer *et al.* (Langer 2010; Langer, Schmidt, Buchmann, and Volkamer 2010) and Volkamer & Grimm (Volkamer and Grimm 2010) 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). Our attacks invalidate these claims. We believe the erroneous results reported by Langer *et al.* are due to a lack of formally written proofs, and the approach by Volkamer & Grimm failed because only some particular scenarios were considered.
In our further work with Bernhard *et al.* (Bernhard et al. 2011), we present a computational security proof demonstrating that any variant of Helios using an IND-CCA2 secure encryption scheme provides ballot secrecy and, more concretely, propose a variant using the Naor-Yung paradigm (Naor and Yung 1990) to derive an IND-CCA2 secure encryption scheme from ElGamal. In this setting, independence is achieved using non-malleable ballots. Intuitively, the use of ElGamal and a suitable signature of knowledge scheme allows us to derive an IND-CCA2 secure encryption scheme; indeed, Tsiounis & Yung (Tsiounis and Yung 1998) and Schnorr & Jakobsson (Schnorr and Jakobsson 2000) provide some evidence to support this hypothesis, however, these results are presented in the generic group model and proving this result under weaker assumptions is an open problem (Shoup and Gennaro 1998, 2002). Nonetheless, it appears that a more efficient provably secure variant of Helios can be derived.
In principle, work by Bernhard, Pereira & Warinschi (Bernhard, Pereira, and Warinschi 2012) supports the aforementioned proposal that a more efficient variant of Helios exists: Bernhard, Pereira & Warinschi prove that an IND-CPA encryption scheme and a suitable signature of knowledge can be combined to derive NM-CPA security, and the *minivoting scheme* (Bernhard et al. 2011) is shown to satisfy ballot secrecy for any NM-CPA secure encryption scheme. Bernhard, Pereira & Warinschi argue that the minivoting scheme forms the basis of Helios and informally claim that Helios is therefore secure since the transformation from minivoting to Helios does not affect ballot secrecy. However, the minivoting scheme is restricted to ballots containing a single ciphertext, hence the security of Helios can only be guaranteed for ballots that contain a vote for a single candidate (for example, in referendums).
A further variant of Helios is proposed by Bulens, Giry & Pereira (Bulens, Giry, and Pereira 2011) using mixnets rather than homomorphic encryption. As highlighted by Pfitzmann & Pfitzmann (Pfitzmann and Pfitzmann 1989), independence is necessary in mixnets because the input ciphertexts are eventually decrypted and Bulens, Giry & Pereira use an IND-CCA2 secure encryption scheme to derive non-malleability and therefore independence.
Delaune, Kremer & Ryan (Delaune, Kremer, and Ryan 2006; Delaune, Kremer, and Ryan 2009) have shown that a variant of the Lee *et al.* protocol satisfies coercion resistance for two honest voters; but, based upon our preliminary results (Cortier and Smyth 2011), Dreier, Lafourcade & Lakhnech (Dreier, Lafourcade, and Lakhnech 2011) demonstrate an attack against privacy for three voters, when one voter is under the adversary’s control. Furthermore, using a stronger definition of coercion resistance, Küsters & Truderung (Küsters and Truderung 2009) have demonstrated a forced abstention attack; in addition, Küsters & Truderung propose a variant of the scheme by Lee *et al.* which is claimed to satisfy their stronger definition. In this article, we show a new attack against the original Lee *et al.* protocol and show that the revised scheme by Küsters & Truderung might not be secure under reasonable assumptions.
A preliminary version of this work (Cortier and Smyth 2011) appeared at the 24th Computer Security Foundations Symposium. By comparison, in this article, we provide further variants of our attack (a preliminary presentation of these variants appears on ePrint (Smyth 2012)), a more detailed description of our results, a generalisation of our ballot secrecy proof to a setting with arbitrary many candidates, and include complete proofs. In addition, we show that other electronic voting protocols are vulnerable to our attack and we discuss the relationships between independence and privacy, and independence and malleability.
# Conclusion
This article identifies a vulnerability in the Helios 2.0 electronic voting protocol 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. 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 in our further work (Bernhard et al. 2011) we present a security proof in the cryptographic setting (Section 8 summarises this result). We have also shown that the absence of ballot independence can be similarly exploited in other electronic voting protocols to violate privacy; in particular, we demonstrate verbatim replay attacks against the schemes by Sako & Kilian (Sako and Kilian 1994) and Schoenmakers (Schoenmakers 1999), and we show that the malleable cryptographic scheme adopted by Lee *et al.* (Lee et al. 2004) can be exploited to replay a voter’s ballot or a variant of it, thereby violating ballot secrecy. In addition, we argue that independence and privacy are unrelated in general, and non-malleability is strictly stronger than independence. Finally, with the exception of Schoenmakers, all of the vulnerabilities in this article have been acknowledged by the respective protocol authors, in particular, Adida & Pereira have acknowledged the vulnerability in Helios (Adida 2010; Adida and Pereira 2010), but since the vulnerability can only be exploited in elections where voters are willing to forfeit their vote to compromise another voter’s privacy, they believe an attack would be *“without serious practical impact."* Nonetheless, Adida & Pereira have scheduled a fix for future Helios releases (at the time of writing, the software implementation of Helios has been patched to prevent the replay attack described in Section 3.1, but the software is still vulnerable to the variants described in Section 3.2).
# Acknowledgements
We are grateful to Ben Adida, David Bernhard, Christian Cachin, Jeremy Clark, Olivier Pereira, Mark D. Ryan, and the anonymous reviewers of our work. Ben Adida and Olivier Pereira provided constructive comments; in addition, Ben informed us that Douglas Wikström is the contemporaneous discoverer of the attack described in Section 3.1. Discussion with Mark D. Ryan helped clarify the presentation of this article, David Bernhard and Jeremy Clark gave useful feedback on the variants of our attack described in Sections 3.2.3 & 3.2.4, and Christian Cachin highlighted Josh Benaloh’s related work.
# Signatures of knowledge
Helios is reliant on signatures of knowledge to ensure secrecy and integrity of the ElGamal scheme. This appendix presents suitable cryptographic primitives.
## Knowledge of discrete logs
Given the cryptographic parameters $(p,q,g)$ and hash function $\mathcal{H}$ (see Section 2 for details), 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$. These proofs are used in distributed ElGamal to ensure secrecy (see Section 2.1).
## Equality between discrete logs
Given the aforementioned cryptographic parameters $(p,q,g)$ and hash function $\mathcal{H}$, a signature of knowledge demonstrating equality between discrete logarithms $\log_f f^x$ and $\log_g\allowbreak 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$.
Signatures of knowledge demonstrating equality between discrete logarithms are used to ensure integrity of distributed decryption in ElGamal (see Section 2.1), moreover, the signature scheme forms the basis of disjunctive proofs of equality between discrete logs (Section 2.2). Formally, the signature scheme can be used to ensure integrity of distributed decryption in ElGamal as follows. 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. The signature $g'_i,a'_i,c_i,s_i$ asserts $\log_g h_i = \log_a k_i$, as required for integrity of decryption.
# Proof of Theorem 1
## Preliminaries
Before commencing our proof, let us first introduce some useful lemmas for the applied pi calculus.
**Lemma 5**. *Given frames $\varphi,\psi$, ground term $M$ and variable $x\not\in\textnormal{dom}(\varphi) \cup\textnormal{dom}(\psi)$, we have $\varphi \approx_s \psi$ iff $\varphi\mid\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\} \approx_s \psi\mid\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}$.*
**Lemma 6**. *Given frames $\varphi$, $\psi$, terms $M$, $N$, and a variable $x\not\in\textnormal{dom}(\varphi) \cup\textnormal{dom}(\psi)$, such that $\varphi = \nu\,\tilde m.\sigma$ and $\psi = \nu\,\tilde n.\tau$ for some names $\tilde m$, $\tilde n$ and substitutions $\sigma$, $\tau$, we have $\nu\,\tilde m.(\sigma \mid \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\}) \approx_s \nu\,\tilde n.(\tau \mid \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x$}}\})$ implies $\varphi \approx_s \psi$.*
The proofs of these lemmas are straightforward.
The following lemma shows when static equivalence implies the same branching behaviour for conditionals.
**Lemma 7**. *Given extended processes $A \equiv C[\textnormal{if } M=N \textnormal{ then } P \textnormal{ else }Q]$ and $B \equiv C'[\textnormal{if } M=N \textnormal{ then } P' \textnormal{ else }Q']$ such that $A \approx_s B$, $(\textnormal{bn}(C) \cup \textnormal{bn}(C')) \cap (\textnormal{fn}(M) \cup \textnormal{fn}(N)) = \emptyset$, $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C)$ and $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C')$, for some closing evaluation context $C,C'$, terms $M,N$ and processes $P,P',Q,Q'$, then $A \xrightarrow{}C[P]$ iff $B \xrightarrow{}C'[P']$ and $A \xrightarrow{}C[Q]$ iff $B \xrightarrow{}C'[Q']$.*
**Proof.* Suppose $A \equiv C[\textnormal{if } M=N \textnormal{ then } P \textnormal{ else }Q]$ and $B\equiv C'[
\textnormal{if } M=N \textnormal{ then }P'\allowbreak\textnormal{else } Q']$ such that $A \approx_s B$, $(\textnormal{bn}(C) \cup \textnormal{bn}(C')) \cap (\textnormal{fn}(M) \cup \textnormal{fn}(N)) = \emptyset$, $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C)$ and $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C')$, for some closing evaluation context $C,C'$, terms $M,N$ and processes $P,P',Q,Q'$. Further suppose $\varphi(C[\textnormal{if } M=N \textnormal{ then } P \textnormal{ else }Q]) = \nu\,\tilde{m}.\sigma$ and $\varphi(C'[\textnormal{if } M=N \textnormal{ then } P' \textnormal{ else }Q']) = \nu\,\tilde{n}.\tau$, for some names $\tilde m$ and $\tilde n$. By Lemma 8 we have $\nu\,\tilde{m}.\sigma \approx_s \nu\,\tilde{n}.\tau$, because static equivalence is closed under structural equivalence. Moreover, by the definition of static equivalence, for all terms $U,V$ such that $(\tilde m \cup \tilde{n}) \cap (\textnormal{fn}(U) \cup \textnormal{fn}(V)) = \emptyset$, we have $U\sigma =_EV\sigma$ iff $U\tau =_EV\tau$.*
*Let us first show $A \xrightarrow{}C[P]$ iff $B \xrightarrow{}C'[P']$. For the $\Rightarrow$ implication, suppose $A \xrightarrow{}C[P]$. Since $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C)$, it must be the case that $M\sigma =_EN\sigma$. We have $\tilde m \cup \tilde n \subseteq \textnormal{bn}(C) \cup \textnormal{bn}(C')$ by definition of the function $\varphi$, and we derive $(\tilde m \cup \tilde n) \cap (\textnormal{fn}(M)\cup\textnormal{fn}(N)) = \emptyset$ because $(\textnormal{bn}(C) \cup \textnormal{bn}(C')) \cap (\textnormal{fn}(M) \cup \textnormal{fn}(N)) = \emptyset$; it follows that $M\sigma =_EN\sigma$ is a special case of $U\sigma =_EV\sigma$. We derive $M\tau =_EN\tau$ from the implication $(U\sigma =_EV\sigma) \Rightarrow (U\tau =_EV\tau)$. It trivially follows that $B\equiv C'[\textnormal{if } M\tau=M\tau \textnormal{ then } P' \textnormal{ else }Q']$, and by closure of internal reduction under structural equivalence we derive $B\xrightarrow{}C'[P']$. The $\Leftarrow$ implications follows by symmetry.*
*We will now show $A \xrightarrow{}C[Q]$ iff $B \xrightarrow{}C'[Q']$. For the $\Rightarrow$ implication, suppose $A \xrightarrow{}C[Q]$. It must be the case that $M\sigma \not=_EN\sigma$ and, as before, we derive $M\tau \not=_EN\tau$. It trivially follows that $B\equiv C'[\textnormal{if } M\tau=N\tau \textnormal{ then } P' \textnormal{ else }Q']$, and since $\textnormal{fv}(M)\cup\textnormal{fv}(N) \subseteq \textnormal{dom}(C')$ we are assured that terms $M\tau, N\tau$ are ground; by closure of internal reduction under structural equivalence we derive $B\xrightarrow{}C'[Q']$. The $\Leftarrow$ implications follows by symmetry. ◻*
This result can naturally be extended to formula. Given $\phi$, let us denote the set of free names, respectively variables, in $\phi$ as $\textnormal{fn}(\phi)$, respectively $\textnormal{fv}(\phi)$.
**Corollary 1**. *Given extended processes $A \equiv C[\textnormal{if } \phi \textnormal{ then } P \textnormal{ else }Q]$ and $B \equiv C'[\textnormal{if } \phi \textnormal{ then } P' \textnormal{ else }Q']$ such that $A \approx_s B$, $(\textnormal{bn}(C) \cup \textnormal{bn}(C')) \cap \textnormal{fn}(\phi) = \emptyset$, $\textnormal{fv}(\phi) \subseteq \textnormal{dom}(C)$ and $\textnormal{fv}(\phi) \subseteq \textnormal{dom}(C')$, for some closing evaluation context $C,C'$, formulae $\phi$ and processes $P,P',\allowbreak Q,Q'$, then $A \xrightarrow{}C[P]$ iff $B \xrightarrow{}C'[P']$ and $A \xrightarrow{}C[Q]$ iff $B \xrightarrow{}C'[Q']$.*
We conclude this subsection with a useful result stated by Abadi & Fournet (Abadi and Fournet 2001).
**Lemma 8**. *Static equivalence is closed by structural equivalence.*
## Notations and Definitions
For the remainder of this article, let $\ell$ be some number of candidates, $n \geq 2$ be some number of voters, and $\sigma$ and $\sigma'$ be candidate substitutions.
### Notations
We introduce the following notations for all $1 \leq i \leq n$ and $1\leq j \leq \ell$: $$\begin{aligned}
\mathit{tally}_j & = & \pi_{j}(y_1) *\allowbreak \dots *\allowbreak \pi_{j}(y_n)\\
{\mathit{partial }}_j & = & \mathsf{partial}(sk_T,tally_j)\\
{\mathit{result }}_j & = & \mathsf{dec}({\mathit{partial }}_j,\mathit{tally}_j)\\
\mathit{ciph}_{i,j} &=& \mathsf{penc}(z_{\mathsf{pk }},r_{i,j},x^{\mathsf{vote}}_{i,j})\\
\mathit{spk}_{i,j} &=& \mathsf{spk}(z_{\mathsf{pk }},r_{i,j},x^{\mathsf{vote}}_{i,j},\mathit{ciph}_{i,j})\\
\widehat{\mathit{spk}}_i &=& \mathsf{spk}(z_{\mathsf{pk }},\,r_{i,1}\circ\dots\circ r_{i,\ell},\,x^{\mathsf{vote}}_{i,1}+\dots+x^{\mathsf{vote}}_{i,\ell},\,\mathit{ciph}_{i,1} * \dots * \mathit{ciph}_{i,\ell})\\
\mathit{ballot}_i & = & \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathit{ciph}_{i,1},\dots,\mathit{ciph}'_{i,\ell},\mathit{spk}_{i,1},\dots,\mathit{spk}'_{1,\ell},\widehat{\mathit{spk}}_i}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\\
%\sigma_L &=& \textcolor{blue}{\{\subst{m_1}{\xvotes{1}},\subst{m'_1}{\xvotess{1}'}\}}\\
%\sigma_R &=& \textcolor{blue}{\{\subst{m_2}{\xvotes{1}},\subst{m'_2}{\xvotess{1}'}\}}\\
\tau_L &=& \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1,i}$}}\mid \textrm{for all $1\leq i \leq\ell$ such that} \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{i}$}}\}\in\sigma\} \\
&& \mathrel\cup \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2,i}$}}\mid \textrm{for all $1\leq i \leq\ell$ such that } \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{i}$}}\}\in\sigma'\} \\
\tau_R &=& \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1,i}$}}\mid \textrm{for all $1\leq i \leq\ell$ such that} \{\textnormal{\raisebox{2pt}{\footnotesize $N$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{i}$}}\}\in\sigma'\}\\
&& \mathrel\cup \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{2,i}$}}\mid \textrm{for all $1\leq i \leq\ell$ such that } \{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{i}$}}\}\in\sigma\}
\end{aligned}$$
### Definitions
Given $N_3,\dots,N_k$ terms such that $\textnormal{fv}(N_j)\subseteq \{z_{\mathsf{pk }},y_1,\ldots,y_{j-1}\}$, we define $$\sigma_{\tilde{N_k}} = \{\textnormal{\raisebox{2pt}{\footnotesize $ballot_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\textnormal{\raisebox{2pt}{\footnotesize $ballot_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\textnormal{\raisebox{2pt}{\footnotesize $N_j$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}} \mid j \in \{3,\dots,k\}\}$$
Given an integer $k\in\mathbb{N}^+$ and a term $N$, we define $N^k$ (resp. $k.N$) to be $N\circ\cdots\circ N$ (resp. $N+\cdots+N$) where $N$ is replicated $k$ times.
We associate to the equational theory $E$ a rewriting system ${\cal R}_E$ by orienting the Equations [eq:proj1],[eq:proj2] and [eq:dec] to [eq:spk1] from left to right. We denote by $E'$ the equational theory that asserts functions $+,*,\circ$ are commutative and associative in addition to Equations [eq:addition] and [eq:addition2]. ${\cal R}_E$ modulo $E'$ forms a convergent rewriting system (modulo $E'$). We denote by $u\rightarrow_E v$ (or often simply $u\rightarrow v$) if $u$ modulo $E'$ can be rewritten to $v$ modulo $E'$, using ${\cal R}_E$. We denote by $u\downarrow$ a normal form of $u$ modulo $E'$.
We will say that a term $M$ is *free* w.r.t. a set of names $\tilde{n}$ if it does not contain any name of $\tilde{n}$. We simply say that a term is free when the set of names is clear from the context (typically free w.r.t. to the restricted names of a frame).
## Some useful lemmas
We prove some useful results about our definitions and notations. We first show that ballots accepted by the bulletin board must have a particular form due to the checks performed by $\phi^{\sf sol}_{\ell,\bar n}$.
**Lemma 9**. *Let $\ell$ be a number of candidates, $\bar n\geq 2$ be an integer, and $M$ be term free w.r.t. $r_{1,1},\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}$ and such that $\textnormal{fv}(M)\subseteq\{z_{\mathsf{pk }},y_1,y_2\}$. Let substitution $\tau\in\{\tau_L,\tau_R\}$ and substitution $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}}\}$. If $[\! [ \phi^{\sf sol}_{\ell,\bar n}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\}\sigma\tau ]\! ] = \mathsf{true}$, then there exists a term $$M'=\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathsf{penc}(z_{\mathsf{pk }},N_1,M_1),\dots,\mathsf{penc}(z_{\mathsf{pk }},N_\ell,M_\ell),S_1,\dots,S_{\ell+1}}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$$ for some terms $M_1,\dots,M_\ell,N_1,\dots,N_\ell,S_1,\dots,S_{\ell+1}$ such that $M \sigma\tau=_E M'\sigma\tau$, $M'$ is free w.r.t. $r_{1,1},\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}$, $\textnormal{fv}(M')\subseteq\{z_{\mathsf{pk }},y_1,y_2\}$, and $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}},\allowbreak \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_\ell$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{\ell}$}}\}$ is a candidate substitution.*
*Proof.* Let $M$, $\tau$ and $\sigma$ be defined as in the Lemma, and suppose $[\! [ \phi^{\sf sol}_{\ell,\bar n}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\}\linebreak\sigma\tau ]\! ] = \mathsf{true}$. We say that a term $N$ is a *minimal recipe* if it is minimal (in size) among the terms $N'$ such that $N \sigma\tau=_E N'\sigma\tau$. It is easy to check by induction on the size of $N$ that, whenever $N = f(N_1,\ldots,N_k)$ with $f\in\{\mathsf{dec},\pi_j\mid 1\leq j\leq \ell\}$ then either $N=\pi_j(x)$ for some $j$ and variable $x$ or ${(N \sigma\tau)\downarrow} \mathrel=
f({(N_1\sigma\tau)\downarrow} ,\ldots,{(N_k\sigma\tau)\downarrow} )$ (\*).
W.l.o.g. suppose $M'$ is a minimal recipe such that $M \sigma\tau=_E M'\sigma\tau$ and $M'$ is free w.r.t. $r_{1,1},\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}$. Further suppose w.l.o.g. that $M'$ is in normal form. We know $[\! [ \phi^{\sf sol}_{\ell,\bar n}\{\textnormal{\raisebox{2pt}{\footnotesize $M'$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\}\sigma\tau ]\! ] = \mathsf{true}$. Thus it must be the case that $M'\sigma\tau$ is of the form $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{U_1,\ldots,U_{\ell},V_1,\ldots,V_{\ell},W}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$, where for $1\leq j\leq \ell$ we have $U_j = \mathsf{penc}(\mathsf{pk}(sk_T),R_j,C_j)$, $C_j\in\{\mathsf{zero},\mathsf{one}\}$ and $\{\textnormal{\raisebox{2pt}{\footnotesize $C_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $C_\ell$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{\ell}$}}\}$ is a candidate substitution. Due to the disequality tests in $\phi^{\sf sol}_{\ell,\bar n}$, it must be the case that $M'$ is of the form $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{T_1,\ldots,T_{\ell},S_1,\ldots,S_{\ell},Z}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$ and $T_j \not\in\{ \pi_{k}(y_i) \mid 1\leq k\leq\ell\}$. We have $T_j\sigma\tau = \mathsf{penc}(A_j,B_j,C_j)$. Assume first that $T_j=\pi_{k}(T_j')$. Due to (\*), we must have $T_j'$ variable, which is excluded by the fact that $T_j \not\in\{ \pi_{k}(y_i) \mid 1\leq k\leq\ell\}$. Thus, due to the equational theory and (\*), it must be the case that $T_j = \mathsf{penc}(K_j,N_j,M_j)*\prod_{1\leq k\leq\ell}\pi_{k}(y_1)^{\alpha_k}*\pi_{k}(y_2)^{\beta_k}$ where each component is optional and $\alpha_i\in\mathbb{N}$. By convention $\alpha_i=0$ or $\beta_i=0$ means that the component is skipped. Assume that one of the $\alpha_i$ or $\beta_i$ is not null. Then $R_j = r\circ R_j'$ with $r\in\{r_{1,1},\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}\}$. Due to the tests in $\phi^{\sf sol}_{\ell,\bar n}$, we know $V_j=\mathsf{spk}(\mathsf{pk}(sk_T),R_j,C_j,V_j')$.
Let us show that $V_j$ cannot be a signature of knowledge that appears in either $ballot_1\tau_L$ or $ballot_2\tau_L$. Assume (by contradiction) that $V_j$ is a signature of knowledge that appears in either $ballot_1\tau_L$ or $ballot_2\tau_L$. Due to weeding, we cannot have $V_j = \mathsf{spk}_{i,k}$. Indeed, due to the equational theory, this would imply that $U_j$ is equal to a previsouly received cyphertext, which is excluded by weeding. Thus we must have $V_j=\widehat{spk}_i$ for some $i\in\{1,2\}$. Then $R_j=r_{i,1}\circ \cdots\circ r_{i,\ell}$. In that case, let us have a look at $W$. We know $W=\mathsf{spk}(\mathsf{pk}(sk_T),R_1\circ\cdots\circ R_{\ell},C_1+\cdots+C_{\ell},U_1*\cdots*U_{\ell})$. Thus $W$ cannot be one of the signatures of knowledge that appear in $ballot_1\tau_L$ or $ballot_2\tau_L$ (the depth of $R_1\circ \cdots\circ R_{\ell}$ is too big). Therefore (and due to the equational theory and minimality of $Z$), we must have $Z = \mathsf{spk}(Z^1,Z^2,Z^3,Z^4)$. Since $r_{i,1}\circ \cdots\circ r_{i,\ell}$ is not deducible, we cannot have $Z^2\sigma\tau =_E r_{i,1}\circ \cdots\circ r_{i,\ell}\circ R_1\circ R_{j-1}\circ R_{j+1}\circ R_{\ell}$, contradiction.
We must have $S_j = \mathsf{spk}(S_j^1,S_j^2,S_j^3,S_j^4)$, since $V_j$ cannot be one of the signatures of proof of knowledge that appear in $ballot_1\tau_L$ or $ballot_2\tau_L$, and due to the equational theory. Since $r$ is not deducible, we cannot have $S_j^2\sigma\tau =_E r\circ R_j'$, contradiction. We therefore deduce that $T_j = \mathsf{penc}(K_j,N_j,M_j)$. Moreover, $K_j\sigma\tau =_E \mathsf{pk}(sk_T)$ implies $K_j=z_{\mathsf{pk }}$ and $M_j\sigma\tau =_E \mathsf{zero}$ or $\mathsf{one}$ implies $M_j\in\{\mathsf{zero},\mathsf{one}\}$ due to the equational theory. Due to the validity check, we also deduce that $\{\textnormal{\raisebox{2pt}{\footnotesize $M_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{1}$}}, \dots, \textnormal{\raisebox{2pt}{\footnotesize $M_\ell$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x^{\mathsf{vote}}_{\ell}$}}\}$ is a candidate subsitution. ◻
*Proof.* First, we decompose $\phi_1$ and consider $\phi = \nu\,\tilde{n}.\theta$, where $\tilde{n} = \{sk_T,d, r_{1,1},\allowbreak\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}\}$ and $\theta =
\{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\}
\mid
\Big\{\{\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ciph}_{i,j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathit{ciph}_{i,j}}$}}\} \mid
\{\textnormal{\raisebox{2pt}{\footnotesize $\mathit{spk}_{i,j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathit{spk}_{i,j}}$}}\} \mid
\{\textnormal{\raisebox{2pt}{\footnotesize $\widehat{\mathit{spk}_i}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\widehat{\mathit{spk}_i}}$}}\} \mathrel\Big|
i\in\{1,2\} \wedge 1\leq j\leq \ell\Big\}$. It follows immediately that $\phi_1\tau_L\approx_s\phi_1\tau_R$ if and only if $\phi\tau_L\approx_s\phi\tau_R$.
Secondly, witness that the adversary can arbitrarily combine ciphertexts from the frame – namely, ciphertexts $\mathit{ciph}_{1,1},\mathit{ciph}_{2,1},\ldots,\mathit{ciph}_{1,\ell},\mathit{ciph}_{2,\ell}$ – with ciphertexts in the frame or freshly constructed ciphertexts, we enrich the frame $\phi$ with any such combination of ciphertexts. Formally, for any $\alpha_j,\beta_j\in\mathbb{N}$ and terms $P,R$ we define $C_{\alpha_1,\ldots,\alpha_{\ell},\beta_1,\ldots,\beta_{\ell},\alpha_4,P,R}$ as follows: $$\mathsf{penc}(\mathsf{pk}(sk_T),R\circ \bigcirc_{1\leq j\leq\ell}r_{1,j}^{\alpha_j}\circ r_{2,j}^{\beta_j},P+\sum_{1\leq j\leq\ell}\alpha_j.x^{\mathsf{vote}}_{1,j}+\beta_j.x^{\mathsf{vote}}_{2,j})$$ We define the extended frame $\phi_e$ below. $$\begin{gathered}
\phi_e = \nu\,\tilde{n}.(\theta \mid
\{
\textnormal{\raisebox{2pt}{\footnotesize $C_{\alpha_1,\alpha_2,\alpha_3,\alpha_4,P,R} $}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\alpha_1,\alpha_2,\alpha_3,\alpha_4,P,R} $}}\mid \alpha_1,\alpha_2,\alpha_3,\alpha_4\in\mathbb{N}\text{ and } \text{terms } \\
P,R %\text{ in normal form s.t. } \fv{M,N}\subseteq\dom{\phi} \text{ and }
\text{ s.t. }
(\textnormal{fn}(P)\cup\textnormal{fn}(R))\cap\tilde{n}=\emptyset, \textnormal{fv}(P,R)\subseteq\textnormal{dom}(\phi_e) \text{ with no cycle}
\})
\end{gathered}$$ Note that $\phi_e$ is infinite. By Lemma 6, it is sufficient to show $\phi_e\tau_L\approx_s\phi_e\tau_R$. We introduce the following two claims.
**Claim 1**. *Let $M$ be a term such that $\textnormal{fv}(M)\mathrel\cap(\textnormal{fv}(\phi_e)\mathrel\backslash\textnormal{dom}(\phi_e))=\emptyset$ and $\textnormal{fn}(M)\mathrel\cap\tilde{n}=\emptyset$. If $M\phi_e\tau\rightarrow U$ for some $\tau\in\{\tau_R,\tau_L\}$, then there exists $N$ such that $U=_{E'}N\phi_e\tau$ and $M\phi_e\tau'\rightarrow N\phi_e\tau'$ for any $\tau'\in\{\tau_R,\tau_L\}$.*
**Claim 2**. *Let $M,N$ be two terms such that $(\textnormal{fv}(M)\mathrel\cup\textnormal{fv}(N))\mathrel\cap(\textnormal{fv}(\phi_e)\mathrel\backslash\textnormal{dom}(\phi_e))=\emptyset$ and $\textnormal{fn}(M,N)\mathrel\cap\tilde{n}=\emptyset$. If $M\phi_e\tau =_{E'} N\phi_e\tau$ for some $\tau\in\{\tau_R,\tau_L\}$, then $M\phi_e =_{E'} N\phi_e$.*
The above claims allow the construction of our proof. Let $M,N$ be two terms such that $\textnormal{fn}(M,N)\cap\tilde{n}=\emptyset$ and $M\phi_e\sigma_{\tilde{N_k}}\tau_L =_{E} N\phi_e\sigma_{\tilde{N_k}}\tau_L$. We assume (possibly by renaming) that $(\textnormal{fv}(M)\cup\textnormal{fv}(N))\cap(\textnormal{fv}(\phi_e)\backslash\textnormal{dom}(\phi_e))=\emptyset$. We have $M\phi_e\tau_L =_{E} N\phi_e\tau_L$. Thus ${(M\phi_e\tau_L)\downarrow} =_{E'} {(N\phi_e\tau_L)\downarrow}$. Applying repeatedly Claim 1, we deduce that there exists $M'$ such that ${(M\phi_e\tau_L)\downarrow} = M'\phi_e\tau_L$ and $M\phi_e\tau_R\rightarrow^* M'\phi_e\tau_R$. Similarly, there exists $N'$ such that ${(N\phi_e\tau_L)\downarrow} = N'\phi_e\tau_L$ and $N\phi_e\tau_R\rightarrow^* N'\phi_e\tau_R$. From $M'\phi_e\tau_L=_{E'}N'\phi_e\tau_L$ and Claim 2, we deduce $M'\phi_e=_{E'}N'\phi_e$. Therefore $M'\phi_e\tau_R=_{E'}N'\phi_e\tau_R$ and thus $M\phi_e\tau_R =_{E} N\phi_e\tau_R$, that is $M\phi_e\sigma_{\tilde{N_k}}\tau_R =_{E} N\phi_e\sigma_{\tilde{N_k}}\tau_R$.
*Proof of Claim 1:* This result is proved by inspection of the rewrite rules, using the fact that the decryption key $sk_T$ is not deducible. More precisely, assume that $M\phi_e\tau\rightarrow U$ for some $\tau\in\{\tau_R,\tau_L\}$. It means that there exists a rewriting rule $l\rightarrow r\in{\cal R}_E$ and a position $p$ such that $M\phi_e\tau|_p=_{E'} l\theta$ for some $\theta$. $p$ cannot occur below $M$ since $\phi_e\tau$ is in normal form. If $M|_p=l\theta'$ for some $\theta'$ then we conclude that we can rewrite $M$ as expected. The only interesting case is thus when $M|_p$ is not an instance of $l$ but $M\phi_e\tau|_p$ is. By inspection of the rules, $l\rightarrow r$ can only correspond to one of the three equations [eq:dec], [eq:partial] or [eq:combination]. The case of Equations [eq:dec] or [eq:partial] is ruled out by the fact that $sk_T$ is not deducible from $\phi_e\tau$. The last case is when the rule corresponding to Equation [eq:combination] is applied. Then it must be the case that $M|_p=x*y$ with $x,y$ variables of $\textnormal{dom}(\phi_e)$. By construction of $\phi_e$, we have that $(x*y)\phi_e\rightarrow z\phi_e$ (applying the rule corresponding to Equation [eq:combination]), thus the result.
*Proof of Claim 2:* Assume by contradiction that there exist $M,N$ two terms such that $M\phi_e\tau =_{E'} N\phi_e\tau$ for some $\tau\in\{\tau_R,\tau_L\}$ and $M\phi_e \neq_{E'} N\phi_e$. Consider $M,N$ two minimal terms that satisfy this property. By case inspection, it must be the case that $M$ and $N$ are both variables. Thus we have $x\phi_e\tau =_{E'} y\phi_e\tau$ and $x\phi_e \neq_{E'} y\phi_e$ with $x,y\in\textnormal{dom}(\phi_e)$, $x\neq y$. The head symbol of $x\phi_e\tau$ must be $\mathsf{penc}$. Then by construction of $\phi_e$, $\tau$ does not change the randomness used in $\mathsf{penc}$ and the randomness uniquely determines the variable, which implies $x=y$, contradiction. ◻
We now demonstrate that tallying valid ballots yields the same result in both worlds.
**Lemma 11**. *Let $\ell$ be a number of candidates. Let $N_3,\dots,N_k$ be terms, free w.r.t. $sk_T,d, r_{1,1},\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}$. Let $\theta_{\tilde{N_k}} = \{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid k \in \{3,\dots,n\}\}$ such that $N_i\theta_{\tilde{N_k}}\sigma\tau$ is a valid ballot for any $\tau\in\{\tau_L,\tau_R\}$. Let $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}}\}$. Then $${\mathit{result }}_i\ \theta_{\tilde{N_k}}\sigma\tau_L =_E {\mathit{result }}_i\ \theta_{\tilde{N_k}}\sigma\tau_R$$ and both ${\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_L$ and ${\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_R$ are terms built from constants $\mathsf{one}$ and $\mathsf{zero}$ by application of the function symbol $+$.*
*Proof.* We first define $N_i' = N_i\theta_{\tilde{N_k}}$. By Lemma 9, we know that $\pi_j(N_i'\sigma\tau_L) =_E \mathsf{penc}(z_{\mathsf{pk }},U_j^i,V_j^i)\sigma\tau_L$ for some free terms $U_j^i,V_j^i$. By Lemma 10, we know that $\phi_1\tau_L\approx_s\phi_1\tau_R$ thus we can deduce $\pi_j(N_i'\sigma\tau_R) =_E \mathsf{penc}(z_{\mathsf{pk }},U_j^i,V_j^i)\sigma\tau_R$. The equational theory ensure that $\mathsf{penc}(K,U,V) =_E \mathsf{penc}(K',U',V')$ implies $K=_E K'$, $U=_E U'$, and $V=_E V'$. Thus we deduce $V_j^i\sigma\tau_L =_E V_j^i\sigma\tau_R$. Therefore, we get that ${\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_L =_E
x^{\mathsf{vote}}_{1,j}\tau_L+x^{\mathsf{vote}}_{2,j}\tau_L +
+(V_j^3+\cdots+V_j^k)\sigma\tau_L
=_E
x^{\mathsf{vote}}_{1,j}\tau_R+x^{\mathsf{vote}}_{2,j}\tau_R +
+(V_j^3+\cdots+V_j^k)\sigma\tau_R
=_E {\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_R$.
Moreover, ${V_j^i}\sigma\tau \in \{\mathsf{one}, \mathsf{zero}\}$ is ensured by the fact that $N_i\theta_{\tilde{N_k}}\sigma\tau$ is a valid ballot. Therefore we deduce that both ${\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_L$ and ${\mathit{result }}_j\ \theta_{\tilde{N_k}}\sigma\tau_R$ are terms built from constants $\mathsf{one}$ and $\mathsf{zero}$ by application of the function symbol $+$. ◻
We finally show that the encrypted ballots of honest voters and the partial decryptions do not leak any information to the adversary.
The proof is very similar to the proof of Lemma 10
*Proof.* First, we decompose $\phi_6$ and consider $\phi = \nu\,\tilde{n}.\theta$ where $\tilde{n} = \{sk_T,d, r_{1,1},\allowbreak\dots,r_{1,\ell},r_{2,1},\dots,r_{2,\ell}\}$ and $\theta =
\{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\}
\mid
\Big\{\{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{partial}_{j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{partial}_{j}}$}}\} \mid
\{\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ciph}_{i,j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathit{ciph}_{i,j}}$}}\} \allowbreak\mid
\{\textnormal{\raisebox{2pt}{\footnotesize $\mathit{spk}_{i,j}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathit{spk}_{i,j}}$}}\} \mid
\{\textnormal{\raisebox{2pt}{\footnotesize $\widehat{\mathit{spk}_i}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\widehat{\mathit{spk}_i}}$}}\} \mathrel{\Big|}
i\in\{1,2\} \wedge 1\leq j\leq \ell\Big\}$. It follows immediately that $\phi_6\tau_L\approx_s\phi_6\tau_R$ if and only if $\phi\tau_L\approx_s\phi\tau_R$.
Secondly, witness that the adversary can arbitrarily combine ciphertexts from the frame – namely, ciphertexts $\mathit{ciph}_{1,1},\mathit{ciph}_{2,1},\ldots,\mathit{ciph}_{1,\ell},\mathit{ciph}_{2,\ell}$ – with ciphertexts in the frame or freshly constructed ciphertexts, we enrich the frame $\phi$ with any such combination of ciphertexts. Formally, for any $\alpha_j,\beta_j\in\mathbb{N}$ and terms $P,R$ we define $C_{\alpha_1,\ldots,\alpha_{\ell},\beta_1,\ldots,\beta_{\ell},\alpha_4,P,R}$ as follows: $$\mathsf{penc}(\mathsf{pk}(sk_T),\;R\circ \bigcirc_{1\leq j\leq\ell}\,r_{1,j}^{\alpha_j}\circ r_{2,j}^{\beta_j},\;P+\sum_{1\leq j\leq\ell}\alpha_j.x^{\mathsf{vote}}_{1,j}+\beta_j.x^{\mathsf{vote}}_{2,j})$$ We define the extended frame $\phi_e$ below. $$\begin{gathered}
\phi_e = \nu\,\tilde{n}.(\theta \mid
\{
\textnormal{\raisebox{2pt}{\footnotesize $C_{\alpha_1,\alpha_2,\alpha_3,\alpha_4,P,R} $}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\alpha_1,\alpha_2,\alpha_3,\alpha_4,P,R} $}}\mid \alpha_1,\alpha_2,\alpha_3,\alpha_4\in\mathbb{N}\text{ and } \text{terms } \\
P,R %\text{ in normal form s.t. } \fv{M,N}\subseteq\dom{\phi} \text{ and }
\text{ s.t. }
(\textnormal{fn}(P)\cup\textnormal{fn}(R))\cap\tilde{n}=\emptyset, \textnormal{fv}(P,R)\subseteq\textnormal{dom}(\phi_e) \text{ with no cycle}
\})
\end{gathered}$$ Note that $\phi_e$ is infinite. By Lemma 6, it is sufficient to show $\phi_e\tau_L\approx_s\phi_e\tau_R$. Let $\phi_e' = \phi_e\sigma_{\tilde{N_k}}$. We introduce the following two claims.
**Claim 3**. *Let $M$ be a term such that $\textnormal{fv}(M)\mathrel\cap(\textnormal{fv}(\phi_e')\mathrel\backslash\textnormal{dom}(\phi_e'))=\emptyset$ and $\textnormal{fn}(M)\mathrel\cap\tilde{n}=\emptyset$. If $M\phi_e'\tau\rightarrow U$ for some $\tau\in\{\tau_R,\tau_L\}$ then there exists $N$ such that $U=_{E'}N\phi_e'\tau$ and $M\phi_e'\tau'\rightarrow N\phi_e'\tau'$ for any $\tau'\in\{\tau_R,\tau_L\}$.*
**Claim 4**. *Let $M,N$ be two terms such that $(\textnormal{fv}(M)\mathrel\cup\textnormal{fv}(N))\mathrel\cap(\textnormal{fv}(\phi_e')\mathrel\backslash\textnormal{dom}(\phi_e'))=\emptyset$ and $\textnormal{fn}(M,N)\mathrel\cap\tilde{n}=\emptyset$. If $M\phi_e'\tau =_{E'} N\phi_e'\tau$ for some $\tau\in\{\tau_R,\tau_L\}$ then $M\phi_e' =_{E'} N\phi_e'$.*
The above claims allow the construction of our proof. Let $M,N$ be two terms such that $\textnormal{fn}(M,N)\cap\tilde{n}=\emptyset$ and $M\phi_e'\sigma_{\tilde{N_k}}\tau_L =_{E} N\phi_e'\sigma_{\tilde{N_k}}\tau_L$. We assume (possibly by renaming) that $(\textnormal{fv}(M)\cup\textnormal{fv}(N))\cap(\textnormal{fv}(\phi_e')\backslash\textnormal{dom}(\phi_e'))=\emptyset$. We have $M\phi_e'\tau_L =_{E} N\phi_e'\tau_L$. Thus ${(M\phi_e'\tau_L)\downarrow} =_{E'} {(N\phi_e'\tau_L)\downarrow}$. Applying repeatedly Claim 3, we deduce that there exists $M'$ such that ${(M\phi_e'\tau_L)\downarrow} = M'\phi_e'\tau_L$ and $M\phi_e'\tau_R\rightarrow^* M'\phi_e'\tau_R$. Similarly, there exists $N'$ such that ${(N\phi_e'\tau_L)\downarrow} = N'\phi_e'\tau_L$ and $N\phi_e'\tau_R\rightarrow^* N'\phi_e'\tau_R$. From $M'\phi_e'\tau_L=_{E'}N'\phi_e'\tau_L$ and Claim 4, we deduce $M'\phi_e'=_{E'}N'\phi_e'$. Therefore $M'\phi_e'\tau_R=_{E'}N'\phi_e'\tau_R$ and thus $M\phi_e'\tau_R =_{E} N\phi_e'\tau_R$, that is $M\phi_e'\sigma_{\tilde{N_k}}\tau_R =_{E} N\phi_e'\sigma_{\tilde{N_k}}\tau_R$.
*Proof of Claim 3:* This result is proved by inspection of the rewrite rules, using the fact that the decryption key $sk_T$ is not deducible. More precisely, assume that $M\phi_e'\tau\rightarrow U$ for some $\tau\in\{\tau_R,\tau_L\}$. It means that there exists a rewriting rule $l\rightarrow r\in{\cal R}_E$ and a position $p$ such that $M\phi_e'\tau|_p=_{E'} l\theta$ for some $\theta$. $p$ cannot occur below $M$ since $\phi_e'\tau$ is in normal form. If $M|_p=l\theta'$ for some $\theta'$ then we conclude that we can rewrite $M$ as expected. The only interesting case is thus when $M|_p$ is not an instance of $l$ but $M\phi_e'\tau|_p$ is. By inspection of the rules, $l\rightarrow r$ can only correspond to one of the three equations [eq:dec], [eq:partial] or [eq:combination]. The case of Equations [eq:dec] is ruled out by the fact that $sk_T$ is not deducible from $\phi_e'\tau$. For Equation [eq:partial], it must be the case that $M\phi_e'|_p={\mathit{result }}_j\sigma_{\tilde{N_k}}$. Using Lemma 11, we deduce that $M\phi_e'|_p\tau\rightarrow R$ modulo $E'$ where $R$ is a sum of $\mathsf{one}$s and $\mathsf{zero}$. Therefore $M\phi_e'\tau\rightarrow M[R]_p\phi_e'\tau$. The last case is when the rule corresponding to Equation [eq:combination] is applied. Then it must be the case that $M|_p=x*y$ with $x,y$ variables of $\textnormal{dom}(\phi_e')$. By construction of $\phi_e'$, we have that $(x*y)\phi_e'\rightarrow z\phi_e'$ (applying the rule corresponding to Equation [eq:combination]), thus the result.
*Proof of Claim 4:* Assume by contradiction that there exist $M,N$ two terms such that $M\phi_e'\tau =_{E'} N\phi_e'\tau$ for some $\tau\in\{\tau_R,\tau_L\}$ and $M\phi_e' \neq_{E'} N\phi_e'$. Consider $M,N$ two minimal terms that satisfy this property. By case inspection, it must be the case that $M$ and $N$ are both variables. Thus we have $x\phi_e'\tau =_{E'} y\phi_e'\tau$ and $x\phi_e' \neq_{E'} y\phi_e'$ with $x,y\in\textnormal{dom}(\phi_e')$, $x\neq y$. The head symbol of $x\phi_e'\tau$ must be $\mathsf{penc}$ or $\mathsf{partial}$. Assume first that the head symbol of $x\phi_e'\tau$ is $\mathsf{penc}$. Then by construction of $\phi_e'$, $\tau$ does not change the randomness used in $\mathsf{penc}$ and the randomness uniquely determines the variable, which implies $x=y$, contradiction. Assume now that the head symbol of $x\phi_e'\tau$ is $\mathsf{partial}$. Then it must be the case that $\mathit{tally}_{j_1}\sigma_{\tilde{N_k}}\tau=_{E'}\mathit{tally}_{j_2}\sigma_{\tilde{N_k}}\tau$ while $\mathit{tally}_{j_1}\sigma_{\tilde{N_k}}\neq_{E'}\mathit{tally}_{j_2}\sigma_{\tilde{N_k}}$. This would require $x_{\mathit{ciph}_{i,j_1}}\tau = x_{\mathit{ciph}_{i',j_2}}'\tau$ for some $i,i'$, which is excluded due to the randomness. ◻
Consider the smallest relation ℛ which is closed under structural equivalence and includes the following pairs of extended processes, where for all 3 ≤ j ≤ n, terms M, terms N1, …, Nj, substitutions $\sigma = \{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid k \in \{3,\dots,n\}\}$ and distinct variables xpartial, xresult, x1, x2 such that NjστL and NjστR are valid ballot, $\textnormal{fv}(M) \cup \bigcup_{3\leq i \leq j} \textnormal{fv}(N_i) \subseteq \textnormal{dom}(A^4)$ and $(\textnormal{fn}(M) \cup \bigcup_{3\leq i \leq j}\textnormal{fn}(N_i)) \cap \textnormal{bn}(A^4) = \emptyset$. $$\label{ROne}
A^{\phi^{\sf sol}}_{\ell,n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'],\quad A^{\phi^{\sf sol}}_{\ell,n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]$$
Definition of the relation ℛ
We introduce some partial evolutions of the Helios process specification in Figure [fig:proofEvoThree] and define a relation $\mathrel{\mathcal{R}}$ between processes in Figure 6. We clearly have that $A^{\phi}_{\ell,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 }}$}}\}\sigma']}\mathrel{\mathcal{R}}A^{\phi}_{\ell,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 }}$}}\}\sigma]}$. We now wish to show that ${\mathrel{\mathcal{R}}} \mathrel\cup {\mathrel{\mathcal{R}}^{-1}}$ satisfies the three properties of Definition 2. By symmetry we focus on $\mathrel{\mathcal{R}}$. Overwriting the definition, we may say that a term $N$ is a valid ballot if both $N\sigma\tau_L$ and $N\sigma\tau_R$ are valid ballots, where $\sigma$ is defined Figure 6.
#### Static equivalence.
We must show for all extended processes $A$ and $B$, where $A \mathrel{\mathcal{R}}B$, that $A \approx_s B$. By Lemma 6, it is sufficient to show $A^7\tau\tau_L \approx_sA^7\tau\tau_R$ for any $N_3,\dots,N_n$ valid ballots. Let $\phi_7 = \nu\,sk_T,d,r_{1,1}, \dots, r_{1,\ell}, r_{2,1},\dots,r_{2,\ell}\mathrel.( \{\textnormal{\raisebox{2pt}{\footnotesize $ballot_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}}\} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $ballot_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_2$}}\} \mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\}
\mid \{\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\mathit{partial }}_1,\dots,{\mathit{partial }}_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{partial }}$}}\}
\mid\linebreak \{\textnormal{\raisebox{2pt}{\footnotesize $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{{\mathit{result }}_1,\dots,{\mathit{result }}_n}\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{result }}$}}\})$. We have to show $\phi_7\sigma_{N_3,\ldots,N_n}\tau_L\approx_s\phi_7\sigma_{N_3,\ldots,N_n}\tau_R$. By Lemma 11, we deduce that $\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathit{result }}_1,\dots,{\mathit{result }}_\ell\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma_{N_3,\ldots,N_n}\tau_L = \mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}{\mathit{result }}_1,\dots,\allowbreak{\mathit{result }}_\ell\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\sigma_{N_3,\ldots,N_n}\tau_R$ and is equal to a constant (always deducible) term. Thus by Lemma 5, it is sufficient to show that $\phi_6\sigma_{N_3,\ldots,N_n}\tau_L\approx_s\phi_6\sigma_{N_3,\ldots,N_n}\tau_R$, where $\phi_6$ as defined in Lemma 12. We conclude by Lemma 12.
#### Internal reductions.
We must show for all extended processes $A$ and $B$, where $A \mathrel{\mathcal{R}}B$, that if $A \xrightarrow{}A'$ for some $A'$, then $B \xrightarrow{}^* B'$ and $A' \mathrel{\mathcal{R}}B'$ for some $B'$. We observe that if $A \equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_L$ and $B\equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_R$ – that is, $A \mathrel{\mathcal{R}}B$ by ([RTwo]) – then there is no extended process $A'$ such that $A \xrightarrow{}A'$; similarly, for ([RFour]), ([RFive]), ([RSeven]), ([RTen]), ([REleven]) and ([RTwelve]). We proceed by case analysis on the remaining cases.
- We have $A \equiv A^{\phi^{\sf sol}}_{\ell,n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma']$ and $B \equiv A^{\phi^{\sf sol}}_{\ell,n}[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma]$. If $A \xrightarrow{}A'$, then it must be the case that $A \equiv C[\overline{a_1}\langle y_1\rangle.0 \mid a_1(y_1).BB^1_n]\tau_L$ and $A'\equiv C[0 \mid BB^1_n]\tau_L$, where $C[\_] = A^1[\nu\,a_1.(\_ \mid V\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma' \mid T_\ell)]$. It follows from $B \equiv C'[\overline{a_1}\langle y_1\rangle.0 \mid a_1(y_1).\allowbreak BB^1_n]\tau_R$, that $B \xrightarrow{}B'$, where $C'[\_] = A^1[\nu\,a_1.(\_ \mid V\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma \mid T_\ell)]$ and $B' = A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_R$. Since $A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_L\mathrel{\mathcal{R}}B'$ and $A' \equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_L$, we derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- This case is similar to ([ROne]). We have $A \equiv A^2[V\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^2_n\mid T_\ell]\tau_L$ and $B \equiv A^2[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak BB^2_n\mid T_\ell]\tau_R$. If $A \xrightarrow{}A'$, then it must be the case that $A \equiv C[\overline{a_2}\langle y_2\rangle.0 \mid a_2(y_2).BB^3_n]\tau_L$ and $A'\equiv C[0 \mid BB^3_n]\tau_L$, where $C[\_] = A^3[\nu\,a_2.(\_ \mid T_\ell)]$. It follows from $B \equiv C[\overline{a_2}\langle y_2\rangle.0 \mid a_2(y_2).BB^3_n]\tau_R$, that $B \xrightarrow{}B'$, where $B' = A^3[BB^3_n\allowbreak \mid\allowbreak T_\ell]\tau_R$. Since $A^3[BB^3_n\allowbreak \mid\allowbreak T_\ell]\tau_L\mathrel{\mathcal{R}}B'$ and $A' \equiv A^3[BB^3_n\allowbreak \mid\allowbreak T_\ell]\tau_L$, we derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- We have $A \equiv A^4[BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid k \in \{3,\dots,j-1\}\}\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\} \mid\allowbreak T_\ell]\tau_L$ and $B\equiv A^4[BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid k \in \{3,\dots,j-1\}\}\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\} \mid\allowbreak T_\ell]\tau_R$ for some integer $j\in\{3,\dots,n\}$, valid ballots $N_3,\dots,N_{j-1}$ and term $M$ such that $\textnormal{fv}(M) \cup \bigcup_{3\leq i \leq j-1} \textnormal{fv}(N_i) \subseteq \textnormal{dom}(A^4)$ and $(\textnormal{fn}(M) \cup \bigcup_{3\leq i \leq j-1} \textnormal{fn}(N_i)) \cap \textnormal{bn}(A^4) = \emptyset$.
If $A \xrightarrow{}A'$, then it must be the case that $A \equiv C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\allowbreak ballot_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\allowbreak ballot_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\} \textnormal{ then }
P \textnormal{ else }0]\tau_L$, where $C[\_] = A^4[\_ \mid\allowbreak T_\ell]$. Furthermore, if $j < n$, then $P = BB^{'}_{j+1,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid\allowbreak j > 3 \wedge k \in\allowbreak \{3,\dots,\allowbreak j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\}$; otherwise $P = BB^4_{n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge k \in\allowbreak \{3,\allowbreak\dots,\allowbreak j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\}$. We also have $B \equiv C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $ballot_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $ballot_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\} \textnormal{ then }
P\textnormal{ else }0]\tau_R$.
Let $\sigma_R = \{\textnormal{\raisebox{2pt}{\footnotesize $ballot_1\tau_R$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}}, \textnormal{\raisebox{2pt}{\footnotesize $ballot_2\tau_R$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_2$}}, \textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\}$, we have $ballot_1\tau_R$ is syntactically equal to $x_1\sigma_R$ and $ballot_2\tau_R$ is syntactically equal to $x_2\sigma_R$, it follows that $B \equiv C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1\sigma_R$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2\sigma_R$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\}\allowbreak \textnormal{then }
P \textnormal{ else }0]\tau_R$ and, moreover, since $\varphi(C[0]\tau_R) = \nu\,sk_T, \allowbreak d,\allowbreak r_{1,1}, \dots, r_{1,\ell},\allowbreak r_{2,1},\dots,r_{2,\ell}, y_1, y_2.\sigma_R$ we have $B \equiv C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\} \textnormal{ then }
P \textnormal{ else }0]\tau_R$. We proceed by case analysis on the structure of $A'$:
- If $A' \equiv C[P]\tau_L$, then by closure of internal reduction under structural equivalence we have $C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\} \textnormal{ then }
P \textnormal{ else }0]\tau_L\allowbreak \xrightarrow{}C[P]\tau_L$ because $ballot_1\tau_L$ is syntactically equal to $x_1\sigma_L$, $ballot_2\tau_L$ is syntactically equal to $x_2\sigma_L$ and $\varphi(C[0]\tau_L) %\BBIfParamBreak{M}{x_1}{x_2} P \Else 0]\tau_L)
= \nu\,sk_T, d, r_{1,1},\allowbreak \dots, r_{1,\ell}, r_{2,1},\dots,r_{2,\ell},\allowbreak y_1,\allowbreak y_2.\sigma_L$, where $\sigma_L = \{\textnormal{\raisebox{2pt}{\footnotesize $ballot_1\tau_L$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_1$}},\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $ballot_2\tau_L$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_2$}},\allowbreak \textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}}\}$.
Assume $A$ and $B$ satisfy the preconditions of Corollary 1, it follows that $B \xrightarrow{}B' = A^4[P \mid\allowbreak T_\ell]\tau_R$. We now prove our assumption. Since $A \mathrel{\mathcal{R}}B$, it follows by Condition 1 of Definition 2 that $A\approx_s B$. Let $\phi = \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\}$. By inspection of $\phi^{\sf sol}_{\ell,j-1}$, we have $\textnormal{fn}(\phi) = \textnormal{fn}(M)\cup\bigcup_{3\leq i \leq j-1} \textnormal{fn}(N_i)$ and since $\textnormal{bn}(C) = \textnormal{bn}(A^4)$ it follows that $\textnormal{bn}(C)\cap\textnormal{fn}(\phi) = \emptyset$; we also have $\textnormal{fv}(\phi) = \{ x_1,x_2,z_{\mathsf{pk }}\} \cup \textnormal{fv}(M) \cup \bigcup_{3\leq i \leq j-1} \textnormal{fv}(N_i)$ and since $\textnormal{dom}(C) = \{ x_1,x_2,z_{\mathsf{pk }}\}$ it follows that $\textnormal{fv}(\phi) \subset \textnormal{dom}(C)$. We have shown that the preconditions of Corollary 1 are satisfied, hence $B \xrightarrow{}B' = A^4[P \mid\allowbreak T_\ell]\tau_R$. It remains to show $A' \mathrel{\mathcal{R}}B'$.
We know $[\! [ \phi^{\sf sol}_{\ell,j-1}\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\}\sigma_L ]\! ] = \linebreak\mathsf{true}$ and $[\! [ \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\}\sigma_R ]\! ] \allowbreak=\linebreak \mathsf{true}$; it follows, for $\tau\in\{\tau_L,\tau_R\}$, that $[\! [ \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}}\}\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $\mathsf{pk}(sk_T)$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $z_{\mathsf{pk }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $\mathit{ballot}_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\dots,\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\}\tau ]\! ]\allowbreak = \mathsf{true}$ and we know that $M$ is a valid ballot. We continue by case analysis on the structure of $P$:
1. If $P = BB^{'}_{j+1,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\}$, then we have $j < n$. Let $j' = j+1$ and $N_j = M$, observe $P = BB^{'}_{j',n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j\}\}$ and $A^4[BB^{'}_{j',n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j\}\}\mid T_\ell]\tau_L\mathrel{\mathcal{R}}B'$. The result $A'\mathrel{\mathcal{R}}B'$ follows by closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
2. If $P = BB^4_{n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\}$, then it must be the case that $j=n$. Let $N_j = M$ and hence $P = BB^4_{n}\tau$. Since $A^4[BB^4_{n}\tau\allowbreak \mid\allowbreak T_\ell]\tau_L\mathrel{\mathcal{R}}B'$ and $A' \equiv A^4[BB^4_{n}\tau\allowbreak \mid\allowbreak T_\ell]\tau_L$, we derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- $A' \equiv C[0]\tau_L$, then similarly to above we have $C[\textnormal{if }\allowbreak \phi^{\sf sol}_{\ell,j-1}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{\mathsf{ballot }}$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_1$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_1$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $x_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_2$}},\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_3$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_3$}},\allowbreak\dots,\allowbreak\textnormal{\raisebox{2pt}{\footnotesize $N_{j-1}$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_{j-1}$}}\} \textnormal{ then }
P \textnormal{ else }0]\tau_L\allowbreak \xrightarrow{}C[0]\tau_L$ and it follows by Corollary 1 that $B \xrightarrow{}B' = C[0]\tau_R$. Since $A^4[0 \mid T_\ell] \mathrel{\mathcal{R}}B'$ and $A' \equiv A^4[0 \mid T_\ell]$, we derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- We have $A \equiv A^4[BB^4_{n}\tau\allowbreak \mid\allowbreak T_\ell]\tau_L$ and $B \equiv A^4[BB^4_{n}\allowbreak\tau\allowbreak \mid\allowbreak T_\ell]\tau_R$, where $BB^4_{n}= \overline{d}\langle\mbox{$(\mkern-2.8mu\rule[-.47ex]{.08ex}{2.10ex}\mkern 3mu$}tally_1,\allowbreak\dots,tally_\ell\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle\mathrel.BB^5_{n}$ and $T_\ell= 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} })),\allowbreak\dots,\mathsf{partial}(sk_T,\pi_{\ell}(y_{\mathsf{tally} }))\mbox{$\mkern 3mu\rule[-.47ex]{.08ex}{2.1ex}\mkern-2.5mu)$}\rangle$. If $A \xrightarrow{}A'$, then it must be the case that $A'\equiv A^4[BB^5_{n}\mid T^1_\ell]\tau\tau_L$. It follows immediately that $B \xrightarrow{}B'$, where $B' = A^4[BB^5_{n}\allowbreak\allowbreak \mid\allowbreak T^1_\ell]\tau\tau_R$. We derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- We have $A \equiv A^4[BB^5_{n}\allowbreak \mid\allowbreak T^1_\ell]\tau\tau_L$ and $B \equiv A^4[BB^5_{n}\allowbreak\allowbreak \mid\allowbreak T^1_\ell]\tau\tau_R$. If $A \xrightarrow{}A'$, then it must be the case that $A \equiv A^5[\overline{d}\langle y_{\mathsf{partial }}\rangle.0\mid\allowbreak d(y_{\mathsf{partial }}).BB^6_{n}\}]\tau\tau_L$ and $A'\equiv A^5[0\mid BB^6_{n}]\tau\tau_L$. It follows from $B \equiv A^5[d(y_{\mathsf{partial }}).BB^6_{n}\allowbreak \mid\allowbreak \overline{d}\langle y_{\mathsf{partial }}\rangle.0]\tau\tau_R$ that $B \xrightarrow{}B'$, where $B' = A^5[BB^6_{n}]\allowbreak\tau\tau_R$. We derive $A'\mathrel{\mathcal{R}}B'$ by the closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
#### Labelled reductions.
We must show for all extended processes $A$ and $B$, where $A \mathrel{\mathcal{R}}B$, that 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'$. We observe cases ([ROne]), ([RThree]), ([RSix]), ([RSeven]), ([REight]), ([RNine]) and ([RTwelve]) cannot be reduced by labelled reductions and proceed by case analysis on the remaining cases.
- We have $A \equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_L$ and $B \equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak BB^1_n\mid T_\ell]\tau_R$. If $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then it must be the case that $A \equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak \overline{c}\langle y_1\rangle.BB^2_n\mid T_\ell]\tau_L$ and $A' \equiv A^2[V\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^2_n\mid T_\ell]\tau_L$ for some variable $x_1$ where $\alpha = \nu\,x_1.\overline{c}\langle x_1\rangle$ and $x_1 \not=z_{\mathsf{pk }}$. It follows from $B\equiv A^1[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak \overline{c}\langle y_1\rangle.BB^2_n\mid T_\ell]\tau_R$, that $B \xrightarrow{\alpha} B'$ where $B' = A^2[V\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma\allowbreak\mid\allowbreak BB^2_n\mid T_\ell]\tau_R$. We have $A^2[V\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $a_2$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $x_{\mathsf{auth }}$}}\}\sigma'\allowbreak\mid\allowbreak BB^2_n\mid T_\ell]\tau_L\mathrel{\mathcal{R}}B'$ and by closure of $\mathrel{\mathcal{R}}$ under structural equivalence $A'\mathrel{\mathcal{R}}B'$.
- We have $A \equiv A^3[BB^3_n\allowbreak \mid\allowbreak T_\ell]\tau_L$ and $B \equiv A^3[BB^3_n\allowbreak \mid\allowbreak T_\ell]\tau_R$. If $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then it must be the case that $A \equiv A^3[\overline{c}\langle y_2\rangle.BB^{'}_{3,n}\allowbreak \mid\allowbreak T_\ell]\tau_L$ and $A' \equiv A^4[BB^{'}_{3,n} \mid\allowbreak T_\ell]\tau_L$ for some variable $x_2$, where $\alpha = \nu\,x_2.\overline{c}\langle x_2\rangle$ and $x_2 \not\in\{x_1,z_{\mathsf{pk }}\}$. It follows from $B\equiv A^3[\overline{c}\langle y_2\rangle.BB^{'}_{3,n}\allowbreak \mid\allowbreak T_\ell]\tau_R$, that $B \xrightarrow{\alpha} B'$, where $B' = A^4[BB^{'}_{3,n} \mid\allowbreak T_\ell]\tau_R$. Since $A^4[BB^{'}_{3,n} \mid\allowbreak T_\ell]\tau_L= A^4[BB^{'}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_L$ and $A^4[BB^{'}_{3,n} \mid\allowbreak T_\ell]\tau_R= A^4[BB^{'}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_R$ when $j=3$, we have $A^4[BB^{'}_{3,n} \mid\allowbreak T_\ell]\tau_L\mathrel{\mathcal{R}}B'$ and derive $A'\mathrel{\mathcal{R}}B'$ by closure of $\mathrel{\mathcal{R}}$ under structural equivalence $A'\mathrel{\mathcal{R}}B'$.
- We have $A \equiv A^4[BB^{'}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_L$ and $B \equiv A^4[BB^{'}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_R$ for some integer $j\in\{3,\dots,n\}$ and terms $N_3,\dots,N_{j-1}$, where $\bigcup_{3\leq i \leq j-1}\textnormal{fv}(N_i) \subseteq \textnormal{dom}(A^4)$ and $\textnormal{bn}(A^4) \cap \bigcup_{3\leq i \leq j-1}\textnormal{fn}(N_i) = \emptyset$. If $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then it must be the case that $A \equiv A^4[a_j(y_j).BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_L$ and $A' \equiv A^4[BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\} \mid\allowbreak T_\ell]\tau_L$, where $\alpha = c(M)$ for some term $M$. It follows from $B \equiv A^4[a_j(y_j).BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\} \mid\allowbreak T_\ell]\tau_R$, that $B \xrightarrow{\alpha} B'$, where $B' = A^4[BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid j > 3 \wedge\allowbreak k \in \{3,\dots,j-1\}\}\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\} \mid\allowbreak T_\ell]\tau_R$. We have $A^4[BB^{''}_{j,n}\{\textnormal{\raisebox{2pt}{\footnotesize $N_k$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_k$}} \mid k \in \{3,\dots,j-1\}\}\allowbreak\{\textnormal{\raisebox{2pt}{\footnotesize $M$}}/\textnormal{\raisebox{-1.5pt}{\footnotesize $y_j$}}\} \mid\allowbreak T_\ell]\tau_L\mathrel{\mathcal{R}}B'$, and derive $A'\mathrel{\mathcal{R}}B'$ by closure of $\mathrel{\mathcal{R}}$ under structural equivalence.
- We have $A \equiv A^5[BB^6_{n}]\tau\tau_L$ and $B \equiv A^5[BB^6_{n}]\allowbreak\tau\tau_R$. If $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then it must be the case that $A' \equiv A^6[BB^7_{n}]\tau\tau_L$ for some variable $x_{\mathsf{partial }}$, where $\alpha = \nu\,x_{\mathsf{partial }}.\overline{c}\langle x_{\mathsf{partial }}\rangle$ and $x_{\mathsf{partial }}\not\in\{x_1,x_2,z_{\mathsf{pk }}\}$. It follows immediately that $B \xrightarrow{\alpha} B'$, where $B' = A^6[BB^7_{n}]\tau\tau_R$. We have $A^6[BB^7_{n}]\tau\tau_L\mathrel{\mathcal{R}}B'$ and by closure of $\mathrel{\mathcal{R}}$ under structural equivalence $A'\mathrel{\mathcal{R}}B'$.
- This case is similar to ([RTen]). We have $A \equiv A^6[BB^7_{n}]\tau\tau_L$ and $B \equiv A^6[BB^7_{n}]\tau\tau_R$. If $A \xrightarrow{\alpha} A'$ such that $\textnormal{fv}(\alpha) \subseteq \textnormal{dom}(A)$ and $\textnormal{bn}(\alpha) \cap \textnormal{fn}(B) = \emptyset$, then it must be the case that $A' \equiv A^7\tau\tau_L$ for some variable $x_{\mathsf{result }}$, where $\alpha = \nu\,x_{\mathsf{result }}.\overline{c}\langle x_{\mathsf{result }}\rangle$ and $x_{\mathsf{result }}\not\in\{x_1,x_2,x_{\mathsf{partial }},z_{\mathsf{pk }}\}$. It follows immediately that $B \xrightarrow{\alpha} B'$, where $B' = A^7\tau\tau_R$. We have $A^7\tau\tau_L\mathrel{\mathcal{R}}B'$ and by closure of $\mathrel{\mathcal{R}}$ under structural equivalence $A'\mathrel{\mathcal{R}}B'$.
# References
2007\. Est Républicain.
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.
———. 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.
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.
Bellare, Mihir, Anand Desai, David Pointcheval, and Phillip Rogaway. 1998. “Relations Among Notions of Security for Public-Key Encryption Schemes.” In *CRYPTO’98: 18th International Cryptology Conference*, 1462:26–45. LNCS. Springer.
Benaloh, Josh. 1996. “Verifiable Secret-Ballot Elections.” PhD thesis, Department of Computer Science, Yale University.
———. 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. .
Benaloh, Josh, and Moti Yung. 1986. “Distributing the Power of a Government to Enhance the Privacy of Voters.” In *PODC’86: 5th Principles of Distributed Computing Symposium*, 52–62. ACM Press.
Bernhard, David, Véronique Cortier, Olivier Pereira, Ben Smyth, and Bogdan Warinschi. 2011. “Adapting Helios for provable ballot privacy.” In *ESORICS’11: 16th European Symposium on Research in Computer Security*, 6879:335–54. LNCS. Springer.
Bernhard, David, Olivier Pereira, and Bogdan Warinschi. 2012. “On Necessary and Sufficient Conditions for Private Ballot Submission.” Cryptology ePrint Archive, Report 2012/236.
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.
Bulens, Philippe, Damien Giry, and Olivier Pereira. 2011. “Running Mixnet-Based Elections with Helios.” In *EVT/WOTE’11: Electronic Voting Technology Workshop/Workshop on Trustworthy Elections*. USENIX Association.
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.
Cortier, Véronique, and Ben Smyth. 2011. “Attacking and fixing Helios: An analysis of ballot secrecy.” In *CSF’11: 24th Computer Security Foundations Symposium*, 297–311. 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, Matthew K. Franklin, Berry Schoenmakers, and Moti Yung. 1996. “Multi-Autority Secret-Ballot Elections with Linear Work.” In *EUROCRYPT’96: 15th International Conference on the Theory and Applications of Cryptographic Techniques*, 1070:72–83. 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.
*Dagstuhl Accord*. 2007. Participants of the Dagstuhl Conference on Frontiers of E-Voting.
Damgård, Ivan, and Mads Jurik. 2001. “A Generalisation, a Simplification and Some Applications of Paillier’s Probabilistic Public-Key System.” In *PKC’01: 4th International Workshop on Practice and Theory in Public Key Cryptography*, 1992:119–36. LNCS. Springer.
Damgård, Ivan, Mads Jurik, and Jesper Buus Nielsen. 2010. “A Generalization of Paillier’s Public-Key System with Applications to Electronic Voting.” *International Journal of Information Security* 9 (6): 371–85.
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.
Desmedt, Yvo, and Pyrros Chaidos. 2012a. “Applying Divertibility to Blind Ballot Copying in the Helios Internet Voting System.” In *ESORICS’12: 17th European Symposium on Research in Computer Security*, 7459:433–50. LNCS. Springer.
———. 2012b. “Private Communication.”
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.
Dreier, Jannik, Pascal Lafourcade, and Yassine Lakhnech. 2011. “Vote-Independence: A Powerful Privacy Notion for Voting Protocols.” In *FPS’11: 4th Workshop on Foundations & Practice of Security*, 6888:164–80. LNCS. Springer.
ElGamal, Taher. 1985. “A Public Key Cryptosystem and a Signature Scheme Based on Discrete Logarithms.” *IEEE Transactions on Information Theory* 31 (4): 469–72.
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.
Küsters, Ralf, and Tomasz Truderung. 2009. “An Epistemic Approach to Coercion-Resistance for Electronic Voting Protocols.” In *S&p’09: 30th IEEE Symposium on Security and Privacy*, 251–66. IEEE Computer Society.
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.
Liu, Jia. 2011. “A Proof of Coincidence of Labeled Bisimilarity and Observational Equivalence in Applied Pi Calculus.” .
Michels, Markus, and Patrick Horster. 1996. “Some Remarks on a Receipt-Free and Universally Verifiable Mix-Type Voting Scheme.” In *ASIACRYPT’96: International Conference on the Theory and Application of Cryptology and Information Security*, 1163:125–32. LNCS. Springer.
Naor, Moni, and Moti Yung. 1990. “Public-key Cryptosystems Provably Secure against Chosen Ciphertext Attacks.” In *STOC’90: 22nd Theory of Computing Symposium*, 427–37. ACM Press.
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.
Paiola, Miriam. 2010. “Extending ProVerif’s Resolution Algorithm for Verifying Group Protocols.” Master’s thesis, Faculty of Mathematical, Physical; Natural Science, University of Padova.
Paiola, Miriam, and Bruno Blanchet. 2011. “Automatic Verification of Group Protocols with Unbounded Numbers of Participants and Sessions.” Unpublished draft.
———. 2012. “Verification of Security Protocols with Lists: from Length One to Unbounded Length.” In *POST’12: First Conference on Principles of Security and Trust*, 7215:69–88. LNCS. Springer.
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.
Pfitzmann, Birgit, and Andreas Pfitzmann. 1989. “How to Break the Direct RSA-Implementation of Mixes.” In *EUROCRYPT’89: 6th International Conference on the Theory and Applications of Cryptographic Techniques*, 434:373–81. Lncs. sp.
*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.
———. 1995. “Receipt-Free Mix-Type Voting Scheme: A practical solution to the implementation of a voting booth.” In *EUROCRYPT’95: 12th International Conference on the Theory and Applications of Cryptographic Techniques*, 921:393–403. 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.
Schnorr, Claus-Peter, and Markus Jakobsson. 2000. “Security of Signed ElGamal Encryption.” In *ASIACRYPT’00: 6th International Conference on the Theory and Application of Cryptology and Information Security*, 1976:73–89. LNCS. Springer.
Schoenmakers, Berry. 1999. “A Simple Publicly Verifiable Secret Sharing Scheme and Its Application to Electronic Voting.” In *CRYPTO’99: 19th International Cryptology Conference*, 1666:148–64. LNCS. Springer.
———. 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.
Shoup, Victor, and Rosario Gennaro. 1998. “Securing Threshold Cryptosystems against Chosen Ciphertext Attack.” In *EUROCRYPT’97: 17th International Conference on the Theory and Applications of Cryptographic Techniques*, 1403:1–16. LNCS. Springer.
———. 2002. “Securing Threshold Cryptosystems against Chosen Ciphertext Attack.” *Journal of Cryptology* 15 (2): 75–96.
Smyth, Ben. 2011. “Formal verification of cryptographic protocols with automated reasoning.” PhD thesis, School of Computer Science, University of Birmingham.
———. 2012. “Replay Attacks That Violate Ballot Secrecy in Helios.” Cryptology ePrint Archive, Report 2012/185.
Smyth, Ben, and Véronique Cortier. 2010. “Attacking ballot secrecy in Helios.” YouTube video, linked from .
———. 2011. “A note on replay attacks that violate privacy in electronic voting schemes.” RR-7643. INRIA.
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.
Tsiounis, Yiannis, and Moti Yung. 1998. “On the Security of ElGamal Based Encryption.” In *PKC’98: First International Workshop on Practice and Theory in Public Key Cryptography*, 1431:117–34. 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.
[^1]: Unanimous election results highlight an inadequacy in our informal definition of privacy: as stated (Section 1), our definition is unsatisfiable. This issue is overcome in our formal privacy definition (Section 5.3).