# Athena: A verifiable, coercion-resistant voting system with linear complexity Ben Smyth ## Abstract Seminal work by Juels, Catalano & Jakobsson delivered a verifiable, coercion-resistant voting system with quadratic complexity. This article attempts to advance the state-of-the-art by delivering a voting system with equivalent security and linear complexity. # Introduction Voting systems must ensure free-choice (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**). A notion of which is formalised by *ballot secrecy* (i.e., a voter’s vote is not revealed to anyone) (**Chaum:1981?**; **Benaloh86?**; **Benaloh96:Thesis?**; **BCGPW15?**; **Smyth15:BallotSecrecyFull?**). This notion can be satisfied by voting systems that simply instruct voters to encrypt their vote. But, free-choice may be compromised by an adversary that is able to communicate with voters, since the coins used for encryption serve as proof of how voters voted and voters may communicate those coins to the adversary. Hence, formulations of free-choice must be accompanied by operational assumptions and limitations on the adversary’s capabilities. Indeed, ballot secrecy assumes that voters’ ballots are constructed and tallied in the prescribed manner, and that the adversary’s capabilities are limited to controlling ballot collection. *Receipt-freeness* (i.e., a voter cannot collaborate with a conspirator to gain information which can be used to prove how they voted) formalises a notion of free-choice in the presence of an adversary that can communicate with voters (**BT94:ReceiptFreeVoting?**; **DKR06?**; **Moran06?**; **Kiayias15?**; **Cortier16:BeleniosRF?**; **Smyth19:receipt-freeness?**). Yet free-choice may be compromised if voters deviate from the prescribed voting procedure. *Coercion-resistance* (i.e., a voter can deviate from a coercer’s instructions, to cast their own vote, without detection) formalises a stronger notion of free-choice assuming that not only can voters deviate, but the adversary can instruct voters how to deviate (**JCJ05?**; **Unruh10?**; **Kusters12:CoercionResistance?**; **2019-surveying-coercion-resistance?**). The distinction between receipt-freeness and coercion-resistance is subtle: “receipt-freeness deals with a \[conspirator\] who is only concerned with deducing information about how someone voted from receipts and public information, but who does not give detailed instructions on how to cast the vote. Coercion resistance, on the other hand, includes dealing with a coercer who gives details not just on which candidate to vote for but also on how to cast the vote" (**Heather11:CoercionResistance?**). Both receipt-freeness and coercion-resistance retain the assumption that voters’ ballots are tallied in the prescribed manner, and receipt-freeness additionally assumes voters’ ballots are constructed in the prescribed manner. Beyond free-choice, voting systems must ensure that only voters vote (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**), which can be achieved by issuing credentials to voters and using cryptography to ensure that authorised ballots are *unforgeability* (i.e., only voters can construct authorised ballots) (**Smyth18:voting-tutorial?**; **Smyth15:ElectionVerifiability?**).[^1]  (Unforgeability is sometimes known as *eligibility verifiability*.) Moreover, voting systems must ensure that voters have equal influence in the decision (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**), which can be achieved by *universal verifiability* (i.e., anyone can check whether an outcome corresponds to votes expressed in collected ballots that are authorised, except for votes expressed in ballots from the same voter, which are all discarded, except for the voter’s last vote) and *individual verifiability* (i.e., a voter can check whether their ballot is collected) (**Benaloh85?**; **Smyth10:ElectionVerifiability?**; **Kusters11:UniversalVerifiability?**; **Smyth15:ElectionVerifiability?**; **Kiayias15?**). Seminal work by Juels, Catalano & Jakobsson (**JCJ02?**; **JCJ05?**; **JCJ10?**) made significant progress towards a voting system satisfying the aforementioned properties, moreover, Clarkson, Chong & Myers (**CCM08?**; **CCM08b?**) implemented their results as Civitas – complexity of those systems is $\mathcal O(|\mathfrak{bb}|^2)$, i.e., quadratic in the length of the bulletin board ($\mathfrak{bb}$). Quadratic complexity arises from the use of pairwise plaintext equality tests on the bulletin board’s ballots to discard all but the last vote cast using a private credential.[^2] Pairwise plaintext equality tests are also used on mixed ballots and mixed public credentials to discard mixed ballots that are unauthorised, with complexity $\mathcal O(|L| \cdot |\mathfrak{bb}|)$, where $L$ is the electoral roll. ## Contribution We advance the state-of-the-art with Athena: A verifiable, coercion-resistance voting system with linear complexity $\mathcal O(|\mathfrak{bb}|)$. Our system reveals anonymised credentials to discard ballots cast using the same private credential (with linear complexity) and uses plaintext equality tests on each individual mixed ballot – which includes a mixed public credential – to discard any mixed ballot that is unauthorised (with linear complexity). Athena works as follows. *Voting.* Voters are issued with credential pairs, wherein the private credential is a nonce and the public credential is an encryption of that nonce. Each voter encrypts the negation of their private credential and their vote, and publishes the two resulting ciphertexts prepended with their public credential and appended with a counter (to the bulletin board). A voter computes ballots for any re-votes similarly, using an incremented counter. It follows that the bulletin board will contain voters’ ballots, plus any adversarial ballots. *Tallying.* Any ballots not containing a public credential are discarded, the second ciphertext of each remaining ballot is homomorphically combined with itself $n$-times (for some nonce $n$), and the resulting combination is decrypted to reveal an anonymised credential. Entries that share an anonymised credential are discarded, except for the one with the highest counter, thus, only the last vote associated with each anonymised credential is retained. The first two ciphertexts of each retained ballot are homomorphically combined, deriving either: 1) the combination of a private credential and the negation of that credential, or 2) the combination of a private credential and some other message (excluding the credential’s negation). The resulting homomorphic combinations and corresponding encrypted votes are mixed (using the same permutation), plaintext equality tests are used to determine whether the mixed homomorphic combinations where constructed using private credentials, and the corresponding mixed encrypted votes are decrypted if they were. Intuitively, Athena achieves coercion-resistance, because a well-formed ballot that encrypts the negation of a voter’s private credential is indistinguishable from an ill-formed ballot that encrypts some other message, hence, a voter cannot prove whether they cast a well-formed ballot (that will be counted, as opposed to an ill-formed ballot that will not), during the voting phase. Moreover, mixing ensures that ballots cannot be mapped to votes during tallying. Thus, coercion-resistance is achieved. (Unlike the voting system by Juels, Catalano & Jakobsson, Athena reveals the number of ballots cast using a voter’s public credential, which requires voters to deny casting ballots when instructed by the coercer to abstain. This is a reasonable strategy, since no voter can prove whether they even cast a well-formed ballot.) Moreover, verifiability is achieved too, because only voters have access to private credentials, hence, only voters can construct authorised ballots (unforgeability), tallying produces evidence (specified in Definition [def:scheme]) demonstrating that election outcomes correspond to the votes expressed in collected ballots that are authorised (universal verifiability), and ballots are recorded on a bulletin board, hence, voters can check whether their ballot is collected (individual verifiability). ## Structure The remaining sections present related work (§[sec:related]) and a brief conclusion (§[sec:conclusion]), Sidebar [sidebar:notation] introduces game-based security definitions and recalls notation, and the appendices define cryptographic primitives, along with relevant security definitions, and present proofs.
A game formulates a series of interactions between a benign challenger, a malicious adversary, and a cryptographic scheme. The adversary wins by completing a task that captures an execution of the scheme in which security is broken, i.e., winning captures what should be unachievable. Tasks can generally be expressed as *indistinguishability* or *reachability* requirements. For example, universal verifiability can be expressed as the inability to reach a state that causes a voting system’s checks to succeed for invalid election outcomes, or fail for valid outcomes. Moreover, ballot secrecy can be expressed as the inability to distinguish between an instance of a voting system in which voters cast some votes, from another instance in which the voters cast a permutation of those votes. Formally, games are probabilistic algorithms that output booleans. We introduce some notation before formalising games. We let $A(x_1,\dots,x_n; r)$ denote the output of probabilistic algorithm $A$ on inputs $x_1,\dots,x_n$ and coins $r$, and we let $A(x_1,\dots,x_n)$ denote $A(x_1,\dots,x_n;r)$, where coins $r$ are chosen uniformly at random from the coin space of algorithm $A$. Moreover, we let $x \leftarrow T$ denote assignment of $T$ to $x$; $x \xleftarrow{r} A(x_1,\dots,x_n)$ denote assignment of $A(x_1,\dots,x_n;r)$ to $x$, where coins $r$ are chosen uniformly at random from the coin space of algorithm $A$; and $x\leftarrow_R S$ denote assignment to $x$ of an element chosen uniformly at random from set $S$ (we use the same notation when $S$ is a distribution). Furthermore, we let $x[i]$ denote component $i$ of vector $x$ and let $|x|$ denote the length of vector $x$. Finally, we write $(x_1,\allowbreak\dots,\allowbreak x_{|T|}) \leftarrow T$ for $x \leftarrow T;\allowbreak x_1\leftarrow x[1];\allowbreak \dots;\allowbreak x_{|T|}\leftarrow x[|T|]$, when $T$ is a vector, and $x,x'\leftarrow_R S$ for $x\leftarrow_R S;\allowbreak x'\leftarrow_R S$. Using our notation, we can formulate the following game $\mathsf{Exp}$ such that $\mathsf{Exp}(H,S,\mathcal A)$ tasks an adversary $\mathcal A$ to distinguish between a function $H$ and a simulator $S$: $m \leftarrow \mathcal A(); \beta \leftarrow_R \{0,1\};$ $g \leftarrow \mathcal A(x); \Return\ g = \beta$. Adversaries are *stateful*, i.e., information persists across invocations of an adversary in a game. In particular, adversaries can access earlier assignments. For instance, the adversary’s second instantiation in game $\mathsf{Exp}$ has access to any assignments made during its first instantiation. An adversary *wins* a game by causing it to output true ($\top$) and the adversary’s *success* in a game $\mathsf{Exp}(\cdot)$, denoted $\mathsf{Succ}(\mathsf{Exp}(\cdot))$, is the probability that the adversary wins, that is, $\mathsf{Succ}(\mathsf{Exp}(\cdot)) =\allowbreak \mathrm{Pr}[\mathsf{Exp}(\cdot) = \top]$. We focus on computational security, rather than information-theoretic security, and tolerate breaks by adversaries in non-polynomial time and breaks with negligible success, since such breaks are infeasible in practice. Game $\mathsf{Exp}$ captures a single interaction between the challenger and the adversary. We can extend games with oracles to capture arbitrarily many interactions. For instance, we can formulate a strengthening of $\mathsf{Exp}$ as follows: $\beta \leftarrow_R \{0,1\}; g \leftarrow \mathcal A^\mathcal O(x);\allowbreak \Return\ g = \beta$, where $\mathcal A^\mathcal O$ denotes $\mathcal A$’s access to oracle $\mathcal O$ and $\mathcal O(m)$ computes $x$. Oracles may access game parameters such as bit $\beta$.
# Our voting system: \scheme **\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 810, column 17): expecting \end{document} ^` ``` latex \section{Our voting system: \scheme}\label{sec:scheme} Our voting system $(\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$ is used as follows: The tallier initiates an election using algorithm $\SetupSymb$ to compute a key pair, which includes a public key $\pk$ for an underlying multiplicative-homomorphic asymmetric encryption scheme $(\GenSymb,\allowbreak\EncSymb,\allowbreak\DecSymb)$, for which there exists a generator $\g$ of the scheme's message space. Next, the registrar uses algorithm $\RegisterSymb$ to compute a credential pair, wherein the private credential is a nonce $\sd$ and the public credential is an encryption $\Enc{\gsd;\pdc}$ of that nonce, for some coins~$\pdc$. The registrar repeats the process to create further credential pairs and these pairs are issued to voters. Each voter uses algorithm $\VoteSymb$ to compute their ballot, which includes: their public credential, an encryption $\Enc{\igsd;\bcc}$ of their negated private credential, an encryption $\Enc{v;\bvc}$ of their vote $v$, and a counter~$\cnt$, for some coins $\bcc$ and $\bvc$. A voter similarly computes ballots for re-votes, using an incremented counter. It follows that the bulletin board will contain a ballot for a voter's first vote % \begin{alignat*}{4} &\Enc{\gsd;r} &\quad&\Enc{\igsd;\bcc_1} &\quad&\Enc{v_1;\bvc_1} &\quad&\cnt_1, % \intertext{ballots for any of the voter's re-votes} % &\Enc{\gsd;r} &&\Enc{\igsd;\bcc_2} &&\Enc{v_2;\bvc_2} &&\cnt_2\ifcompress, \; \ldots,\fi \\ \ifcompress\else&&\vdots\\\fi &\Enc{\gsd;r} &&\Enc{\igsd;\bcc_k} &&\Enc{v_k;\bvc_k} &&\cnt_k, \\ % \intertext{such that $\cnt_1 < \dots < \cnt_k$, and any other ballots cast using the voter's public credential, without the private credential (including those cast by the adversary or even the voter themselves), namely,} % &\Enc{\gsd;r} &&\Enc{\gD{1};\overline\bcc_1} &&\Enc{\overline v_1;\overline\bvc_1} &&\overline{\cnt}_1\ifcompress, \; \ldots,\fi \\ \ifcompress\else&&\vdots\\\fi &\Enc{\gsd;r} &&\Enc{\gD{l};\overline\bcc_l} &&\Enc{\overline v_l;\overline\bvc_l} &&\overline{\cnt}_l. \end{alignat*} % (Ballots also prove correct ciphertext construction, moreover, they prove that the second ciphertext of each ballot encrypts a message of the form $g^m$. Hence, we restrict ourselves to well-defined ballots above.) Beyond the above ballots, the bulletin board will of course contain ballots cast using other public credentials. The tallier uses algorithm $\TallySymb$ to compute the election outcome as follows: The tallier generates a nonce $n$, homomorphically combines the second ciphertext of each entry on the bulletin board with itself $n$-times, decrypts the resulting homomorphic combinations to reveal anonymised credentials,\ifcompress\else\footnote{% The second ciphertext could simply be decrypted (without harming unforgeability, since knowledge of the exponent must be demonstrated), but this permits some linkability between elections, which is undesirable}\fi\ and prepends entries with anonymised credentials, thereby producing output including %%% %%% Anonymising credentials might not be necessary in all situations, since %%% revealing $\igsd$ may not harm security, but it really depends on the %%% setting. Indeed, revealing $\igsd$ allows it to be tracked across elections %%% % \begin{alignat*}{5} &\igsd[\cdot n] &\ifieee\,\,\else\quad\fi&\Enc{\gsd;r} &\ifieee\,\,\else\quad\fi&\Enc{\igsd;\bcc_1} &\ifieee\,\,\else\quad\fi&\Enc{v_1;\bvc_1} &\ifieee\,\,\else\quad\fi&\cnt_1\ifcompress, \; \ldots,\fi\\ \ifcompress\else&&\vdots\\\fi &\igsd[\cdot n] &&\Enc{\gsd;r} &&\Enc{\igsd;\bcc_k} &&\Enc{v_k;\bvc_k} &&\cnt_k\ifcompress,\fi\\ &\gD[\cdot n]{1} &&\Enc{\gsd;r} &&\Enc{\gD{1};\overline\bcc_1} &&\Enc{\overline v_1;\overline\bvc_1} &&\overline{\cnt}_1\ifcompress, \; \ldots,\fi\\ \ifcompress\else&&\vdots\\\fi &\gD[\cdot n]{l} &&\Enc{\gsd;r} &&\Enc{\gD{l};\overline\bcc_l} &&\Enc{\overline v_l;\overline\bvc_l} &&\overline{\cnt}_l. \end{alignat*} % Entries with the same public credential that are prepended with the same value are discarded, except for the one with the highest counter. Hence, the first $k-1$ entries (above) are discarded, whilst the $k$th entry is preserved. The remaining entries are similarly processed, therefore, the last will be kept if any entries sharing the prepended value ($\gD[\cdot n]{l}$) have counter values lower than counter $\overline{\cnt}_l$. (For example, suppose only the penultimate entry shares prepended value $\gD[\cdot n]{l}$, i.e., $D_l = D_{l-1}$, and further suppose $\overline{\cnt}_l > \overline{\cnt}_{l-1}$. Hence, the last entry will be preserved and the penultimate entry will be discarded. By comparison, the penultimate entry will be kept if $\overline{\cnt}_l < \overline{\cnt}_{l-1}$.) The first two ciphertexts of preserved entries are homomorphically combined and paired with encrypted votes, producing \[ \Enc{\gsd\odot\igsd;r\oplus\bcc_k} \qquad \Enc{v_k;\bvc_k}, \] for the $k$th entry (above), and \[ \Enc{\gsd\odot{}\gD{l};r\oplus\overline\bcc_l} \qquad\Enc{\overline v_l;\overline\bvc_l}, \] for the last (assuming it is preserved). The homomorphic combinations and encrypted votes are mixed (using the same permutation). The tallier performs (optimised) plaintext equality tests on each of the mixed homomorphic combinations to determine whether they contain plaintext one,\ifcompress\else\footnote{Mixed homomorphic combinations could simply be decrypted (without harming unforgeability), but this permits some linkability between elections. }\fi\ and decrypts the corresponding mixed encrypted votes when the test holds. Thus, the voter's vote $v_k$ (above) is revealed, because mixed ciphertext $\Enc{\gsd\odot\igsd;r\oplus\bcc_k\oplus \tmc}$ encrypts $1$, whereas vote $\overline v_l$ is not revealed, because mixed ciphertext $\Enc{\gsd\odot{}\gD{l};r\oplus\overline\bcc_l\oplus \overline \tmc}$ does not (recall $\gD{l}$ was constructed without private credential $d$), where $\tmc$ and $\overline\tmc$ are coins introduced during mixing. The election outcome is the tally of revealed votes. \scheme\ is formally specified by Definition~\ref{def:scheme}, using cryptographic primitives introduced in Appendix~\ref{sec:crypto}. Those primitives include sigma protocols for proving correct key generation, ciphertext construction, and decryption, which behave as one might expect. They also include a sigma protocol for proving iterative homomorphic combination, that is, proving that a ciphertext $c$ is computed from another ciphertext $c'$ such that $c = \bigotimes_1^n c'$, for some nonce $n$. We apply the Fiat-Shamir transformation to sigma protocols to derive non-interactive proof systems, which we use to achieve verifiability. \begin{definition}[\scheme]\label{def:scheme}% \iflncs\else\begin{sloppypar}\fi Suppose $\Pi = (\GenSymb,\allowbreak\EncSymb,\allowbreak\DecSymb)$ is a multiplicative-homomorphic asymmetric encryption scheme with a message space that is super-polynomial in the security parameter and for which a generator exists; $\mathcal M$ is a verifiable pairwise mixnet; $\Sigma_1$, $\Sigma_2$, $\Sigma_3$ and $\Sigma_4$ are sigma protocols that prove key generation, ciphertext construction, decryption and iterative homomorphic combination, respectively; and $\mathcal H$ is a hash function. Let $\sFS{\Sigma_1}{\mathcal H} = (\ProveKeySymb,\allowbreak \VerKeySymb)$, $\sFS{\Sigma_2}{\mathcal H} = (\SignCiphSymb,\allowbreak \VerCiphSymb)$, $\sFS{\Sigma_3}{\mathcal H} = (\ProveDecSymb,\allowbreak \VerDecSymb)$, and $\sFS{\Sigma_4}{\mathcal H} = (\ProveCombSymb,\allowbreak \VerCombSymb)$. \emph{\scheme}, denoted $\mathsf{\scheme}(\allowbreak\Pi,\allowbreak\mathcal M,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak\Sigma_4,\allowbreak\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$, is defined by the following algorithms. \iflncs\else\end{sloppypar}\fi % \begin{itemize} \item $\Setup$. Compute \begingroup \removelatexerror {\upshape \begin{algorithm}[H] $(\pk,\sk,\mathfrak m) \xleftarrow{r} \Gen[\kk]$\; $\rho \leftarrow \ProveKey[(\kk,\pk,\mathfrak m),(\sk, r),\kk]$\; $\mathbf{\pkSymb}\leftarrow(\pk,\mathfrak m,\rho)$\; $\mathbf{\skSymb}\leftarrow(\pk,\sk)$, \end{algorithm} } \endgroup \noindent let $\mB$ be the largest integer upper-bound by a polynomial in the security parameter, let $\mC$ be the largest integer such that $\{0,\dots,\mC\}\subseteq\{0\} \cup \mathfrak m$ and $\mC$ is upper-bound by a polynomial in the security parameter, and output $(\mathbf{\pkSymb},\mathbf{\skSymb},\mB,\mC)$. \item $\Register[\PKT,k]$. Parse $\PKT$ as $(\pk,\mathfrak{m},\rho)$, outputting $(\perp,\perp)$ if parsing fails or $\VerKey=\allowbreak {\perp}$, generate nonce $\sd$, compute \begingroup \removelatexerror {\upshape \begin{algorithm}[H] $\pd\leftarrow\Enc{\gsd}$\; $\mathbf{\sdSymb}\leftarrow(\pd,\sd)$, \end{algorithm} } \endgroup \noindent and output $(\pd,\mathbf{\sdSymb})$, where $\g$ is a generator of message space $\mathfrak m$. \item $\ReVote[\SD,\PKT, v,\cnt,\nC,\kk]$. Parse $\SD$ as a vector $(\pd,\sd)$ and $\PKT$ as a vector $(\pk,\allowbreak\mathfrak m,\allowbreak\rho)$, outputting $\perp$ if parsing fails or $\VerKey = {\perp} \allowbreak\vee\allowbreak v\not\in\{1,\allowbreak\dots,\allowbreak \nC\}\allowbreak\vee\allowbreak \{1,\allowbreak\dots,\allowbreak \nC\}\not\subseteq\mathfrak m$, compute \begingroup \removelatexerror {\upshape \begin{algorithm}[H] $c_1\xleftarrow{\bcc}\Enc{\igsd}$\; $c_2\xleftarrow{\bvc}\Enc{v}$\; $\sigma_1 \leftarrow \SignCiph{\pk, \g, c_1,\mathfrak m}{-\sd, \bcc}{m}$\; $\sigma_2 \leftarrow \SignCiph{\pk, c_2,\{1,\dots,\nC\}}{v, \bvc}{m}$, \end{algorithm} } \endgroup \begin{comment} \marginpar{We probably need to prove that $c_1$ isn't an encryption of $0$ (to avoid forced abstention on decryption of $0$).} \marginpar{If $0$ is in the message space, then it needs to be encoded, otherwise, the scheme won't be homomorphic.} \end{comment} \noindent and output $(\pd,c_1,c_2,\sigma_1,\sigma_2,\cnt)$, where message $m = (\pd,c_1,c_2,\cnt)$ and $\g$ is the aforementioned generator of message space $\mathfrak m$. \item $\Tally[\SKT,\bb,\nC,\electoralroll,\kk]$. Parse $\SKT$ as vector $(\pk,\sk)$, initialise $\outcome$ as a zero-filled vector of length $\nC$, and proceed as follows. % \begin{enumerate} \item\label{scheme:tally:removeInvalidBallots} Remove invalid ballots: Let $\{b_1,\dots,b_\ell\}$ be the largest subset of senary vectors in $\bb$ such that $b_1[1] \leq \dots \leq b_\ell[1]$ and for each $(\pd,\allowbreak c_1,\allowbreak c_2,\allowbreak\sigma_1,\allowbreak\sigma_2,\cnt)$ in the subset we have $ \pd \in \electoralroll\wedge\allowbreak \VerCiph{\pk,\allowbreak\g,\allowbreak c_1,\allowbreak\mathfrak m}{\sigma_1}{m} \wedge\allowbreak \VerCiph{\pk,\allowbreak c_2,\allowbreak\{1,\dots,\nC\}}{\sigma_2}{m} $, where $g$ is again the aforementioned generator of message space $\mathfrak m$ and message $m = (\pd,\allowbreak c_1,\allowbreak c_2,\cnt)$. If the subset is empty, then output $(\outcome,\perp)$. \item\label{scheme:tally:revotes} Mix final votes: Initialise $\tpfRevotes$ as an empty vector and $\mixPairInA$ as an empty map from pairs (comprising a ciphertext and a group element) to triples (comprising a counter and two ciphertexts), generate nonce $n$, compute \begingroup \removelatexerror {\upshape \begin{algorithm}[H] % \SetAlgoLined %Use vertical line | below blocks % \SetKwFor{For}{for}{do}{} %For-block without "end" after vertical line \For{$1 \leq i \leq \ell$}{ \SetAlgoVlined %Restore |_ line below blocks $c'_{i} \leftarrow \bigotimes_1^n b_i[2]$\; $N \leftarrow \Dec{c'_1}$\; ${\bf t}\leftarrow \mixPairInA[(b_i[1],N)]$\; %%Start manual split % } %\end{algorithm} %\begin{algorithm}[H] % \SetKwBlock{Begin}{}{} %Block without keyword % \Begin{ %%End manual split \uIf{${\bf t} = \Null \vee {\bf t}[1] < b_i[6]$}{ \tcp{Update the map if $\mixPairInA[(b_i[1],N)]$ is empty or contains a lower counter} $\mixPairInA[(b_i[1],N)] \leftarrow (b_i[6],b_i[1] \otimes b_i[2],b_i[3])$\; } \ElseIf{${\bf t}[1] = b_i[6]$}{ \tcp{Disregard duplicate counters} $\mixPairInA[(b_i[1],N)] \leftarrow (b_i[6],\perp,\perp)$\; } $\varsigma \leftarrow \ProveDecSymb((\pk,c'_{i}, N),\sk, \kk)$\; \eIf{$|\tpfRevotes| > 0$}{ %% Computing proofs as follows ensures that each anonymised credential %% $c'_i$ is anonymised using the same nonce $n$. %% Optimisation: It is perhaps more efficient to compute just one proof %% outside of the for-loop \tcp{Prove $c'_{i-1}$ and $c'_{i}$ are derived %from $b_{i-1}[2]$ and $b_{i}[2]$ by iterative homomorphic combination wrt nonce $n$} $\omega \leftarrow \ProveComb{\pk,(c'_{i-1},c'_{i}),(b_{i-1}[2],b_i[2])}{n}$\; $\tpfRevotes \leftarrow \tpfRevotes \parallel (c'_{i}, N,\varsigma,\omega)$\; }{ $\tpfRevotes \leftarrow \tpfRevotes \parallel (c'_{i}, N,\varsigma)$, } } \end{algorithm} } \endgroup \noindent and apply (pairwise) mixnet $\mathcal M$ to the pairs of ciphertexts in map $\mixPairInA$ to derive vector~$\mixPairOutA$. \item\label{scheme:tally:decrypt} Reveal eligible votes: Initialise $\tpfDec$ as an empty vector, generate nonces $n_1,\dots,n_{|\mixPairOutA|}$, and compute \begingroup \removelatexerror {\upshape \begin{algorithm}[H] \For{$(c_1,c_2)\in \mixPairOutA$}{ $c' \leftarrow \bigotimes_1^{n_{|\tpfDec|+1}} c_1$\; $m\leftarrow\Dec{c'}$\; $\omega \leftarrow \ProveComb{\pk,c',c_1}{n_{|\tpfDec|+1}}$\; $\varsigma_1 \leftarrow \ProveDecSymb((\pk,c', m),\sk, \kk)$\; \eIf{$m=1$}{ \tcp{$c_1$ encrypts $g^0$, hence, is derived from homo comb of pub cred and enc of neg priv cred} $v \leftarrow \Dec{c_2}$\; $\outcome[v] \leftarrow \outcome[v]+1$\; $\varsigma_2 \leftarrow \ProveDecSymb((\pk,c_2, v),\sk, \kk)$\; $\tpfDec \leftarrow \tpfDec \parallel (c',v,\omega,\varsigma_1,\varsigma_2)$\; }{ $\tpfDec \leftarrow \tpfDec \parallel (c',m,\omega,\varsigma_1)$, } } \end{algorithm} } \endgroup \noindent and output $(\outcome,(\tpfRevotes,\mixPairOutA,\tpfDec))$, where $\g$ is the aforementioned generator of message space $\mathfrak m$. \end{enumerate} \item $\Verify[\PKT,\allowbreak\bb,\allowbreak\nC,\allowbreak\electoralroll,\allowbreak\outcome,\allowbreak\tpf,\allowbreak\kk]$. Parse $\PKT$ as vector $(\pk,\mathfrak{m},\rho)$ and $\outcome$ as a vector of length $\nC$, outputting $0$ if parsing fails, $\VerKey = {\perp}$, or $\nC \not\leq \mC$, where $\mC$ is computed as per algorithm $\SetupSymb$. Perform the following checks. \begin{enumerate} \item\label{scheme:verify:removeInvalidBallots} Check ballot removal. Compute $\{b_1,\dots,b_\ell\}$ as per Step~\ref{scheme:tally:removeInvalidBallots} of algorithm $\TallySymb$ and check $\{b_1,\dots,b_\ell\} = \emptyset$ implies $\outcome$ is a zero-filled vector. \item\label{scheme:verify:revotes} \begin{sloppypar} Check mix. Check $\tpf$ parses as a vector $(\tpfRevotes,\mixPairOutA,\tpfDec)$ and $\tpfRevotes$ parses as a vector $((c'_1,\allowbreak N_1,\allowbreak\varsigma_1),\allowbreak(c'_2,\allowbreak N_2,\allowbreak\varsigma_2,\allowbreak\omega_2),\allowbreak\dots,\allowbreak(c'_\ell,\allowbreak N_\ell,\allowbreak\varsigma_\ell,\allowbreak\omega_\ell))$ such that $ \bigwedge_{1\leq i \leq \ell} \VerDec{\pk,\allowbreak c'_i,\allowbreak N_i}{\varsigma_i} $ and $ \bigwedge_{1< i \leq \ell} \VerComb{\pk,\allowbreak(c'_{i-1},\allowbreak c'_i),(b_{i-1}[2],\allowbreak b_i[2])}{\allowbreak\omega_i} $, initialise $\mixPairInA$ as an empty map from pairs to triples, compute \end{sloppypar} \begingroup \removelatexerror {\upshape \begin{algorithm}[H] \For{$1 \leq i \leq \ell$}{ ${\bf t}\leftarrow \mixPairInA[(b_i[1],N_i)]$\; \uIf{${\bf t} = \Null \vee {\bf t}[1] < b_i[6]$}{ $\mixPairInA[(b_i[1],N)] \leftarrow (b_i[6],b_i[1] \otimes b_i[2],b_i[3])$, } \ElseIf{${\bf t}[1] = b_i[6]$}{ $\mixPairInA[(b_i[1],N)] \leftarrow (b_i[6],\perp,\perp)$\; } } \end{algorithm} } \endgroup \noindent and check $\mixPairOutA$ was output by the mix applied in Step~\ref{scheme:tally:revotes} of algorithm $\TallySymb$ on input of the pairs of ciphertexts in $\mixPairInA$. \item \label{scheme:verify:decrypt} Check revelation. Checks $\tpfDec$ parses as a vector of length $|\mixPairOutA|$ such that for each $v\in\{1,\dots,\nC\}$ we have % %\begin{multline*} $ \exists^{=\outcome[v]} i\in\{1,\dots,|\mixPairOutA|\} : \exists c_1,c_2,c',\omega,\varsigma_1,\varsigma_2 : (c_1,c_2) = \mixPairOutA[i] \mathrel \wedge (c',v,\omega,\varsigma_1,\varsigma_2) = \tpfDec[i] \mathrel \wedge \VerComb{\pk, c', c_1}{\omega} \mathrel \wedge \VerDec{\pk,c', 1}{\varsigma_1} \allowbreak\wedge \VerDec{\pk,c_2, v}{\varsigma_2}, $ %\end{multline*} % and for each remaining integer $i \in \{1,\dots,|\mixPairOutA|\}$ we have $\mixPairOutA[i]$ parses as $(c_1,c_2)$, $\tpfDec[i]$ parses as $(c',m,\omega,\varsigma_1)$, and $\VerComb{\pk,\allowbreak c', c_1}{\allowbreak\omega} \wedge \VerDec{\pk,c', m}{\varsigma_1} \wedge m \not=1$. \end{enumerate} \noindent Output $1$ if all the above checks hold. \end{itemize} \end{definition} \scheme\ is specified in terms of \emph{election scheme} syntax by Smyth, Frink~\& Clarkson~\cite{Smyth15:ElectionVerifiability}, which we extend to include re-voting (Appendix~\ref{app:syntax}). %(Definition~\ref{def:election}). Election schemes must satisfy a %That definition incorporates a correctness condition that ensures such schemes function, i.e., election outcomes %output by algorithm $\TallySymb$ correspond to votes expressed in %the ballots input to that %algorithm, when the ballots are output by algorithm $\VoteSymb$ %and the key pair is output by algorithm $\SetupSymb$. ballots (except for votes expressed in ballots from the same voter, which are all discarded, except for the voter's last vote), when ballots are constructed and tallied in the prescribed manner, and we prove \scheme\ satisfies the condition. \begin{lemma}\label{lem:correctness} $\mathsf{\scheme}(\Pi,\mathcal M,\Sigma_1, \Sigma_2, \Sigma_3, \Sigma_4, \mathcal H)$ is an election scheme when cryptographic primitives satisfy the preconditions of Definition~\ref{def:scheme} and asymmetric encryption scheme $\Pi$ is perfectly correct. \end{lemma} \iffalse \marginpar{Push Section~2 to the appendix in the conference version and write, \emph{A proof of Lemma~\ref{lem:correctness} appears in Appendix~\ref{app:proof:correctness}, along with our definition of an election scheme} (or similar), here} \fi \noindent A proof of Lemma~\ref{lem:correctness} appears in Appendix~\ref{app:proof:correctness}. Beyond correctness, verifiable election schemes should satisfy \emph{completeness}, i.e., auditing should succeed for evidence produced by tallying, hence, algorithm $\VerifySymb$ should accept outputs of algorithm $\TallySymb$. We prove \scheme\ satisfies completeness in \ifinformal Appendix~\ref{app:proof:completeness}\else Section~\ref{sec:uv}\fi. $\mathsf{\scheme}$ should be instantiated with an asymmetric encryption scheme satisfying IND-CPA and sigma protocols satisfying special soundness and special honest verifier zero-knowledge. This ensures the non-interactive proof systems derived by application of the Fiat-Shamir transformation satisfy zero-knowledge and simulation sound extractability~\cite{Bernhard12:Helios}, which help achieve both privacy and verifiability. Moreover, this ensures that ballots are non-malleable~\cite{Bernhard12:Helios}, which is necessary for privacy~\cite{Smyth15:BallotSecrecyFull}. Furthermore, for linear complexity, we require computation $\bigotimes_1^n c$ to be linear in the length of $c$, which is possible for El Gamal, for instance. (Indeed, we have $\bigotimes_1^n (g^r,(g^x)^r \cdot M) \equiv (g^r,(g^x)^r \cdot M)^n \equiv (g^{r\cdot n},(g^x)^{r\cdot n} \cdot M^n)$.) \ifieee\else\paragraph{Implementation.} \fi \scheme\ is formally stated independently of the underlying cryptographic primitives (for generality, algorithm agility, and ease of proofs). In practice, $\mathsf{\scheme}(\Pi,\mathcal M,\Sigma_1, \Sigma_2, \Sigma_3, \Sigma_4, \mathcal H)$ can be instantiated with established cryptographic primitives. For instance, we might instantiate asymmetric encryption scheme $\Pi$ as El Gamal~\cite{ElGamal85} and we might instantiate sigma protocols as follows: % $\Sigma_1$ as the protocol for proving knowledge of discrete logarithms by Chaum \emph{et al.}~\cite[Protocol 2]{Chaum86}, $\Sigma_2$ as the protocol for proving knowledge of disjunctive equality between discrete logarithms by Cramer \emph{et al.}~\cite[Figure~1]{CramerFranklinSchoenmakersYung96}, $\Sigma_3$ as the protocol for proving knowledge of equality between discrete logarithms by Chaum \& Pedersen~\cite[\S3.2]{Pedersen92}, and $\Sigma_4$ as a slight variant of the protocol by Chaum \& Pedersen.\footnote{% To prove iterative homomorphic combination using equality between discrete logarithms, witness that $ \bigwedge_{1 \leq i \leq n} (\alpha_i,\beta_i) = (\alpha'_i,\beta'_i)^n $ iff $ \bigwedge_{1 \leq i \leq n} \log_{\alpha'_i} \alpha_i \equiv \log_{\beta'_i} \beta_i \wedge\allowbreak \bigwedge_{1 < i \leq n} \log_{\alpha_{i-1}} \alpha_{i-1} \equiv \log_{\alpha_{i}} \alpha_{i} $, where $(\alpha_1,\allowbreak\beta_1),\allowbreak(\alpha'_1,\allowbreak\beta'_1),\allowbreak\dots,\allowbreak(\alpha_n,\allowbreak\beta_n),\allowbreak(\alpha'_n,\allowbreak\beta'_n)$ are El Gamal ciphertexts.% } \ifinformal ``` # Informal security analysis ## Coercion-resistance # Privacy results An Athena ballot contains a public credential, i.e., an encryption of the corresponding private credential, and an encryption of the negated private credential. Yet, no voter can prove that any ballot contains their private credential. Indeed, a well-formed Athena ballot that encrypts the negation of a voter’s private credential is indistinguishable from an ill-formed ballot that encrypts some other value, rather than such a negation. Hence, during the voting phase, a voter cannot prove whether they cast a well-formed ballot (that will be counted, as opposed to an ill-formed ballot that will not), let alone prove how they voted, thereby assuring coercion-resistance during the voting phase. Associating each public credential with anonymised credentials (to discard early votes prior to mixing) reveals the number of ballots whose second ciphertext contains the same plaintext (be that a private credential or some other value). For instance, a voter that casts a specific number of ballots containing such a plaintext can check to see whether an anonymised credential appears the specified number of times (in association with the voter’s public credential). But, no voter can prove that those ballots are well-formed. Indeed, the voter may cast the expected number of ballots using a nonce in place of their private credential’s negation, which will result in the expected relation, yet the ballots are ill-formed and will not be counted. Hence, coercion-resistance is preserved before mixing. Finally, homomorphically combining ciphertexts, mixing those combinations and encrypted votes, and using plaintext equality tests to determine voters’ votes (as opposed to adversarial votes) preserves coercion-resistance, as does decrypting mixed (voters’) votes. (Ballots prove that votes are selected from the sequence of candidates, which provides protection against randomisation attacks (**JCJ10?**).) It follows that tallying preserves coercion-resistance. Thus, Athena is a coercion-resistant voting system. The desire to formally prove that Athena satisfies coercion resistance #### Distributed tallying. Coercion-resistance does not provide assurances when deviations from the prescribed tallying procedure are possible. Indeed, such deviations include revealing the tallier’s private key, which undermines privacy. Hence, the tallier must be trusted. Alternatively, we can design voting systems that distribute the tallier’s role amongst several talliers and ensure free-choice assuming at least one tallier behaves. Extending Athena in this direction is straightforward, since distributed variants of the underlying primitives are well-known. Ultimately, we would prefer not to trust talliers; unfortunately, this is only known to be possible for decentralised voting systems, e.g., (**Schoenmakers99:PVSS?**; **KY02?**; **G04?**; **HRZ09?**; **Smyth12:decentralised-voting-system?**; **Khazaei18:DecentralisedVotingAnalysis?**), which do not scale. ## Verifiability # Verifiability results Athena records ballots on a (public) bulletin board, hence, voters can check whether their ballot is collected (individual verifiability). Moreover, tallying produces evidence demonstrating that the announced election outcome corresponds to the votes expressed in collected ballots that are authorised (universal verifiability). Furthermore, only voters can construct authorised ballots (unforgeability). It follows that Athena is a verifiable election scheme, as we shall prove using formal definitions from Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) that we extend to include re-voting (Appendix [app:verifiability]). ## Universal verifiability Universal verifiability asserts that anyone must be able to check whether an election outcome corresponds to votes expressed in collected ballots that are authorised. Since checks can be performed by algorithm $\mathsf{Verify}$, it suffices that the algorithm accept if and only if the outcome corresponds to votes expressed in collected ballots that are authorised. The *only if* requirement is formalised by $\mathsf{Soundness}$ (Definition [def:UVSoundness]), which requires algorithm $\mathsf{Verify}$ to only accept correct outcomes, and the *if* requirement is captured by $\mathsf{Completeness}$ (Definition [def:UVComplete]), which requires election outcomes produced by algorithm $\mathsf{Tally}$ to be accepted by algorithm $\mathsf{Verify}$.
**Proposition 1** ($\mathsf{Soundness}$). *Election scheme $\mathsf{Athena}(\Pi,\allowbreak\mathcal M,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies $\mathsf{Soundness}$, when asymmetric encryption scheme $\Pi$ is perfectly correct, mixnet $\mathcal M$ is verifiable, sigma protocols $\Sigma_1$, $\Sigma_2$, $\Sigma_3$ and $\Sigma_4$ satisfy special soundness and special honest verifier zero-knowledge, and $\mathcal H$ is a random oracle, assuming $\mathsf{Injectivity}$ is satisfied.*
We defer consideration of $\mathsf{Injectivity}$ (Definition [def:injectivity]) to Section 1.3.
*Proof.* We must establish that outcomes accepted by algorithm $\mathsf{Verify}$ correspond to votes expressed in collected ballots that are authorised. Step [scheme:verify:removeInvalidBallots] of the algorithm ensures accepted outcomes are only influenced by bulletin board entries constructed by algorithm $\mathsf{Vote}$, i.e., only (valid) ballots have influence (invalid ballots do not), and only when they contain a public credential. Step [scheme:verify:revotes] ensures no influence from any mixed ballots that share a public credential (and a anonymised credential) with another mixed ballot, whilst being associated with a (strictly) lower counter value. Moreover, pairs of mixed ballots that share a public credential (and a anonymised credential) and a counter are ensured to have no influence either. It follows that only mixed ballots expressing the last vote associated with a public and an anonymised credential may have influence. Finally, Step [scheme:verify:decrypt] restricts influence to mixed ballots associated with a voter’s public and private credential, i.e., only voters’ last votes have influence, hence, accepted outcomes correspond to votes expressed in authorised collected ballots. ◻
A detailed proof of Proposition 1 and all other verifiability proofs appear in Appendix [app:proofs].
**Proposition 2** ($\mathsf{Completeness}$).
*Proof.* We must establish that outcomes produced by algorithm $\mathsf{Tally}$ are accepted by algorithm $\mathsf{Verify}$. It is trivial to see that an outcome output by the first step of algorithm $\mathsf{Tally}$ will be accepted by the first step of algorithm $\mathsf{Verify}$, and it remains to consider outcomes output by the last step of algorithm $\mathsf{Tally}$. Simulation sound extractability (of sigma protocol $\Sigma_2$) assures us that such outcomes are derived from ballots containing well-formed ciphertexts. It is straightforward to see that computations performed by the second step of algorithm $\mathsf{Tally}$ can be successfully checked in the second step of algorithm $\mathsf{Verify}$, in particular, proofs can be verified, because proof systems are complete. Moreover, since map $\mixPairInA$ is equivalently computed (from well-formed ciphertexts) by both algorithms and since the mixnet is verifiable, it follows that checks performed on the mixnet’s output succeed. Finally, the checks performed by the third step of algorithm $\mathsf{Verify}$ succeed, because proof systems are complete, thus, outcomes produced by algorithm $\mathsf{Tally}$ are accepted. ◻
## Unforgeability Unforgeability asserts that only voters can construct authorised ballots. Since ballots are authenticated by private credentials, it suffices to ensure that knowledge of a private credential is necessary to construct an authentic ballot, which is formalised by $\mathsf{Unforgeability}$ (Definition [def:unforgeability]).
**Proposition 3** ($\mathsf{Unforgeability}$). *Election scheme $\mathsf{Athena}(\Pi,\allowbreak\mathcal M,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies $\mathsf{Unforgeability}$, when sigma protocol $\Sigma_2$ satisfies special soundness and special honest verifier zero-knowledge and $\mathcal H$ is a random oracle, assuming hardness of discrete logs.*
*Proof sketch.* Suppose an adversary can construct an authorised ballot. It follows that the adversary can prove knowledge of a voter’s private credential, which suffices to solve the discrete logarithm problem, thereby deriving a contradiction. ◻
## Individual verifiability Individual verifiability asserts that voters must be able to check whether their ballot is amongst those collected. Since ballots should be collected and recorded on a bulletin board, and since the board must be available to everyone, it suffices for voters to check that their ballot (i.e., the ballot they constructed) is on the bulletin board. Hence, it is necessary for voters to check that their ballot has not been omitted from the bulletin board. Yet, this is insufficient, because the presence of a ballot identical to a voter’s ballot, does not imply the presence of the ballot constructed by the voter. Indeed, such a ballot might have been constructed by another voter. Thus, individual verifiability requires that voters must be able to uniquely identify their ballot, i.e., ballots do not collide, which is formalised by $\mathsf{Individual}\textrm{-}\allowbreak\mathsf{Verifiability}$ (Definition [def:iv]). To ensure Athena satisfies individual verifiability, it suffices to require that the underlying encryption scheme produces distinct ciphertexts with overwhelming probability. Smyth explains that “\[s\]ecurity properties of asymmetric encryption schemes ensure \[distinct\] ciphertexts...But, such security properties assume public keys are generated (by key generation algorithms) using coins chosen uniformly at random. By comparison, individual verifiability and injectivity assume public keys are constructed by the adversary. Thus, security properties are insufficient to ensure...individual verifiability and injectivity" (**Smyth18:HeliosMixnetVerifiability?**). Nonetheless, given that Athena checks correct key generation, it suffices that ciphertexts are distinct for correctly generated keys.
**Proposition 4** ($\mathsf{Individual}\textrm{-}\allowbreak\mathsf{Verifiability}$). *Election scheme $\mathsf{Athena}(\Pi,\allowbreak\mathcal M,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies $\mathsf{Individual}\textrm{-}\allowbreak\mathsf{Verifiability}$ if for all probabilistic polynomial-time adversaries $\mathcal A$ and security parameters $\kappa$ we have $\Pr[(\mathit{pk},\mathfrak{m},\rho,m,m')\leftarrow \mathcal A(\kappa);\allowbreak c\leftarrow\mathsf{Enc}(\mathit{pk},m); c'\leftarrow\mathsf{Enc}(\mathit{pk},m') %\\ \mathrel: \mathsf{VerKey}((\kappa,\allowbreak\mathit{pk},\allowbreak\mathfrak m),\allowbreak\rho,\allowbreak\kappa)=\allowbreak 1 \wedge m,m'\in\mathfrak{m} \Rightarrow c \not=c'] > 1 -\mathsf{negl}(\kappa)%,$, where $\Pi = (\mathsf{Gen},\allowbreak\mathsf{Enc},\allowbreak\mathsf{Dec})$ and $\mathsf{FS}(\Sigma,\allowbreak\mathcal H) = (\mathsf{ProveKey},\allowbreak \mathsf{VerKey})$. Moreover, $\mathsf{Injectivity}$ is satisfied if the probability is $1$ when plaintexts $m$ and $m'$ are distinct.*
The preconditions used by Proposition 4 are due to Smyth (**Smyth18:HeliosMixnetVerifiability?**), and our proof is structurally similar to his proof of individual verifiability and injectivity for a class of encryption-based voting systems. # Complexity analysis Analysing the complexity of algorithms $\mathsf{Setup}$, $\mathsf{Register}$, and $\mathsf{Vote}$ is straightforward (given the simplicity of those algorithm): $\mathsf{Setup}$ generates a key pair and proof of correct generation, $\mathsf{Register}$ computes a ciphertext, and $\mathsf{Vote}$ computes two ciphertexts along with proofs of correct construction. Hence, complexity of the registration phase is linear in the number of voters and complexity of the voting phase is linear in the number of ballots cast. Algorithms $\mathsf{Tally}$ and $\mathsf{Verify}$ are more elaborate and analysis is more involved. We proceed by a detailed inspection of each algorithm and find that complexity remains linear. We consider each step of algorithm $\mathsf{Tally}$: It is trivial to see that complexity is upper-bound by the bulletin board’s length in Step [scheme:tally:removeInvalidBallots]. For Step [scheme:tally:revotes], we have assumed computation $\bigotimes_1^n c$ is linear in the length of $c$ (§[sec:scheme]), hence, it is straightforward to see that complexity is upper-bound by the number of for-loop iterations, which is constrained by the number of valid ballots on the bulletin board, therefore, complexity is again upper-bound by the bulletin board’s length, because the number of valid ballots is at most the number of ballots on the bulletin board. Complexity of Step [scheme:verify:decrypt] is similarly upper-bound by the number of for-loop iterations, which is constrained by the number of pairs output by the mix and at most the number of ballots on the bulletin board, therefore, complexity is upper-bound by the bulletin board’s length. We consider the steps of algorithm $\mathsf{Verify}$: Complexity of Step [scheme:verify:removeInvalidBallots] is trivially linear in the bulletin board’s length; Step [scheme:verify:revotes] is straightforwardly linear in the number of for-loop iterations, which is linear in the bulletin board’s length; and Step [scheme:verify:decrypt] is straightforwardly linear in the number pairs output by the mix, which is again linear in the bulletin board’s length. Thus, Athena has linear complexity $\mathcal O(|\mathfrak{bb}|)$ in the length of the bulletin board ($\mathfrak{bb}$), assuming linear complexity of iterative homomorphic combinations (§[sec:scheme]), which is possible for El Gamal, for instance. Complexity of the voting system by Juels, Catalano & Jakobsson is quadratic, due to pairwise plaintext equality tests performed on ballots to ensure that only the last choice of each voter has influence, which is needed for universal verifiability. By comparison, Athena uses anonymised credentials in a manner that achieves the same property, whilst reducing complexity. (The voting system by Juels, Catalano & Jakobsson also performs pairwise plaintext equality tests on mixed ballots and mixed credentials, to identify authorised ballots. The complexity of those tests is upper-bound by $\mathcal O(|L| \cdot |\mathfrak{bb}|)$, where $L$ is the electoral roll and $|\mathfrak{bb}|$ is the bulletin board’s length. By comparison, the plaintext equality tests performed by Athena are upper-bound by $\mathcal O(|\mathfrak{bb}|)$.) # General design principles General design principles were identified and embraced during the development of Athena. This section shares these principles to aid the development of future voting systems, especially those with linear complexity. Our first design principle is guided by definitions of correctness and universal verifiability: 1. Algorithm $\mathsf{Tally}$ must map votes expressed in authorised ballots to the outcome corresponding to those votes, except for any early votes. It follows that: 1. Algorithm $\mathsf{Vote}$ must authenticate ballots. The next two design principles follow from our informal definitions of ballot secrecy and coercion resistance, respectively: 1. Algorithm $\mathsf{Vote}$ must ensure votes cannot be revealed from ballots; and 2. Algorithm $\mathsf{Tally}$ must not reveal any (meaningful) mapping between ballots and the outcome. Forgoing coercion resistance (in favour of ballot secrecy), the previous design principle can be generalised: Algorithm $\mathsf{Tally}$ must not reveal any (meaningful) mapping between *authorised* ballots and the outcome. But this permits revealing authorised ballots, which allows *simulation attacks* (**JCJ10?**), whereby a coercer instructs a voter to reveal their private credential, uses that private credential to cast a ballot, and determines whether the voter followed instruction by checking whether the cast ballot is authorised. By comparison, ([design:Tally:NoLeak]) gives way to the following design principle: 1. Algorithm $\mathsf{Tally}$ must not reveal authorised ballots. Similarly, authorised ballots must not be revealed during casting and collection: 1. Algorithm $\mathsf{Vote}$ must not reveal authorised ballots. Since ballots must be authenticated ([design:Tally:Map]) without revealing authorised ballots ([design:Tally:NoLeakAuthorised] & [design:Vote:NoLeakAuthorised]), the following principle emerges: 1. Algorithm $\mathsf{Tally}$ should anonymise ballots prior to authentication. Given that ballots should be anonymised ([design:Tally:Anonymise]) and that bulletin boards may contain more than just ballots, it is proposed that: 1. Algorithm $\mathsf{Vote}$ should prove correct ballot construction; and 2. Algorithm $\mathsf{Tally}$ should discard garbage, i.e., non-ballots. Revealing re-votes after anonymisation can be problematic, for instance, a voter that casts a specific number of ballots can deanonymise their anonymised ballots. Thus, our final design principle is suggested: 1. Algorithm $\mathsf{Tally}$ should discard ballots representing early votes prior to anonymisation. For compatibility between ([design:Tally:Anonymise] & [design:Tally:ReVotes]) and ([design:Tally:NoLeak]), our notion of *meaningful* should exclude garbage and early votes, i.e., algorithm $\mathsf{Tally}$ is permitted to reveal mappings between the outcome and garbage, ballots representing early votes, or both. By combining our design principles, we observe that algorithm $\mathsf{Tally}$ should filter the bulletin board to remove garbage ([design:Tally:Garbage]) and ballots representing early votes ([design:Tally:ReVotes]). Moreover, after anonymising any remaining ballots, the algorithm should authenticate anonymised ballots and remove any unauthorised anonymous ballots ([design:Tally:Anonymise]). Finally, votes expressed in any authenticated anonymous ballots should be mapped to the outcome corresponding to those votes ([design:Tally:Map]). This procedure is illustrated in Figure [fig:design] and underpins the design of Athena.
*\[tikzpicture diagram omitted\]*
# Related work Acquisti (**Acquisti04:JCJLinear?**), Smith (**Smith05:JCJLinear?**), and Weber, Araújo & Buchmann (**Weber07:JCJLinear?**) reduce complexity to linear in variants of the voting system by Juels, Catalano & Jakobsson, but those reductions led to the lose of coercion-resistance (**Araujo08b:JCJLinear?**; **Araujo08:JCJLinear?**; **CCM08?**; **Araujo10:JCJLinear?**; **Araujo13:JCJLinear?**). Araújo *et al.* (**Araujo08b:JCJLinear?**; **Araujo08:JCJLinear?**; **Araujo10:JCJLinear?**) make better progress, albeit, without supporting audits for statistically determining whether non-voters are issued with credentials (**Spycher11:JCJLinear?**; **Schlapfer11:JCJLinear?**; **Araujo13:JCJLinear?**) and without supporting reuse of credentials between elections (**Araujo13:JCJLinear?**; **Araujo16:JCJLinear?**). Haghighat, Dousti & Jalili do not permit reuse either (**Haghighat13:JCJLinear?**), whereas Araújo *et al.* do (**Araujo13:JCJLinear?**; **Araujo16:JCJLinear?**), albeit, Araújo *et al.* do not achieve *strong non-reusability* (i.e., only the last choice of each voter has influence (**Smyth16:helios-eligibility?**)) nor universal verifiability, in the presence of an adversary that can re-order ballots (e.g., a network adversary), because they are reliant on ballot order to discard early votes.[^3],[^4] (The voting system by Juels, Catalano & Jakobsson does not satisfy strong non-reusability nor universal verifiability against such an adversary either, whereas Civitas does (**Smyth15:ElectionVerifiability?**).) Schläpfer *et al.* and Spycher *et al.* also make progress, albeit, Schläpfer *et al.* only achieve linear complexity for a trade in the degree of coercion-resistance and they leak the number of ballots each voter casts (**Schlapfer11:JCJLinear?**) and Spycher *et al.* make an additional trust assumption, namely, they assume the tallier introduces a secret number of dummy votes for each voter (without any means for voters to confirm they did) (**Spycher11:JCJLinear?**). Beyond variants of the voting system by Juels, Catalano & Jakobsson, distinct voting systems have also been introduced: The system by Schweisgut (**Schweisgut06:JCJLinear?**) achieves linear-complexity, but fails to achieve coercion-resistance (**Araujo10:JCJLinear?**). Clark & Hengartner propose the *Selections* voting system, which makes better progress, albeit, some degree of coercion-resistance is traded to achieve linear complexity and the number of ballots each voter casts is leaked (**Clark11:Selections?**; **Clark11:thesis?**). (Athena leaks the number of ballots cast in association with each public credential, but not the number of ballots each voter casts.) Finally, Essex, Clark & Hengartner propose the *Cobra* voting system, which achieves remarkably fast tallying, albeit, registration has quadratic complexity in the number of voters (**Essex12:Cobra?**). With the exception of Juels, Catalano & Jakobsson, Haghighat, Dousti & Jalili, and Clark & Hengartner, none of these prior works present security proofs and proving their security remains an open problem. (Araújo *et al.* (**Araujo10:JCJLinear?**; **Araujo16:JCJLinear?**) formally state theorems, but defer proofs to full versions of their papers, which do not appear to be public.) # Conclusion For one and a half decades, researchers have strived to improve upon seminal work by Juels, Catalano & Jakobsson. This work attempts to deliver such an improvement: A verifiable, coercion-resistant voting system with linear complexity. We have seen how several of the ideas can help improve security of existing voting systems. Moreover, they generalise beyond voting to other systems that require strong forms of privacy, authentication, and verifiability, thereby advancing not just voting technology, but the science of security. [^1]: Auditing can statistically determine whether non-voters are issued with credentials. [^2]: A *plaintext equality test* (PET) is a cryptographic primitive for determining whether two ciphertexts encrypt the same plaintext (**Jakobsson00?**). [^3]: Araújo *et al.* can probably achieve strong non-reusability and universal verifiability using counters, as per Athena. [^4]: Araújo *et al.* do not specify sufficient details to ensure non-malleable ballots, without which unforgeability is not satisfied, because authentication material can be replayed. Similarly, encrypted votes can be replayed to violate coercion-resistance (cf. (**Benaloh96:Thesis?**; **Sako95:ImpactOfNoIndependence?**; **Michels96:ImpactOfNoIndependence?**; **Wikstrom08:Independence?**; **Smyth12:Helios?**)). Nonetheless, including the entire ballot (except proofs) in the hashes used by proofs should suffice to ensure non-malleability.