# Verifiability of Helios Mixnet

Ben Smyth

2026-09-05

## Abstract

We study game-based definitions of individual and universal verifiability by Smyth, Frink & Clarkson. We prove that building voting systems from El Gamal coupled with proofs of correct key generation suffices for individual verifiability. We also prove that it suffices for an aspect of universal verifiability. Thereby eliminating the expense of individual-verifiability proofs and simplifying universal-verifiability proofs for a class of encryption-based voting systems. We use the definitions of individual and universal verifiability to analyse the mixnet variant of Helios. Our analysis reveals that universal verifiability is not satisfied by implementations using the weak Fiat-Shamir transformation. Moreover, we prove that individual and universal verifiability are satisfied when statements are included in hashes (i.e., when using the Fiat-Shamir transformation, rather than the weak Fiat-Shamir transformation).

# Introduction

An election is a decision-making procedure to choose representatives (**Lijphart84?**; **Saalfeld95?**; **Gumbel05:StealThisVote?**; **Alvarez10:ElectronicElections?**). Choices should be made by voters with equal influence, and this must be ensured by voting systems (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**). Many electronic voting systems build upon creativity and skill, rather than scientific foundations, and are routinely broken in ways that permit adversaries to unduly influence the selection of representatives, e.g., (**Wallach04:Diebold?**; **ElectoralCommision07?**; **DebraBowenCalifornia07?**; **GermanyCourt09?**; **JonesSimons12:VotingBook?**). Breaks can be avoided by carefully formulating rigorous and precise security definitions that capture notions of voters voting with equal influence, and proving that systems satisfy these definitions. Applicable definitions include (**JCJ10?**; **Kusters10?**; **Smyth10:ElectionVerifiability?**; **Smyth10:ElectionVerifiabilityA?**; **Cortier14:verifiability?**; **Kiayias15?**; **Cortier16:VerifiabilitySoK?**; **Smyth15:ElectionVerifiability?**) and we build upon work by Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**). (The relative merits of definitions are considered in Section <a href="#sec:syntax" data-reference-type="ref" data-reference="sec:syntax">[sec:syntax]</a>.) They present game-based security definitions in the computational model of cryptography (**Katz07?**), whereby a benign challenger, a malicious adversary and a voting system engage in a series of interactions which task the adversary to complete a challenge. Successful completion of the task corresponds to an execution of the voting system in which security is broken. Thus, the task captures what the adversary should not be able to achieve.

Universal verifiability formalises a notion of checking whether voters voted with equal influence.

- Universal verifiability. Anyone can check whether an outcome corresponds to votes expressed in recorded ballots.

Smyth, Frink & Clarkson formalise a game-based definition of universal verifiability (**Smyth15:ElectionVerifiability?**). That game tasks the adversary to compute inputs to the tallying procedure, including an election outcome and some ballots, that cause checks to succeed when the outcome does not correspond to the votes expressed by those ballots, or that cause checks to fail when the outcome does correspond to the votes expressed.

Merely casting a ballot is insufficient to ensure it is recorded, because an adversary may discard ballots. Individual verifiability formalises the notion of voters convincing themselves that their ballot is amongst those recorded.

- Individual verifiability. A voter can check whether their ballot is recorded.

Smyth, Frink & Clarkson formalise individual verifiability as a game that tasks the adversary to cause a collision between ballots (**Smyth15:ElectionVerifiability?**). That game proceeds as follows: First, the adversary provides any inputs necessary to construct a ballot, including a vote $v_0$. Secondly, the challenger constructs a ballot using those inputs. Finally, the adversary and the challenger repeat the process to construct a second ballot for vote $v_1$. The adversary wins if the two independently constructed ballots are equal. Hence, winning signifies the existence of a scenario in which two voters cannot uniquely identify their ballot, thus a voter cannot be convinced that their ballot is recorded.

Equipped with definitions of individual and universal verifiability, we can analyse existing voting systems to determine whether they are secure. As is exemplified by the following two voting systems. The first ($\mathsf{Enc2Vote}$) instructs each voter to encrypt their vote using an asymmetric encryption scheme and instructs the tallier to decrypt the encrypted votes and publish the number of votes for each candidate. The second ($\mathsf{Enc2Vote}^*$) extends the former to include proofs of correct computation, in particular, the tallier computes proofs of correct key generation and decryption. The former system achieves neither individual nor universal verifiability. Indeed, a public key can be maliciously constructed such that ciphertexts collide and spurious outcomes need not correspond to the encrypted votes. By comparison, the latter system achieves both individual and universal verifiability, because well-formed ciphertexts are unique (individual verifiability) and anyone can check proofs to determine whether the election outcome corresponds to votes expressed in recorded ballots (universal verifiability). Voting systems $\mathsf{Enc2Vote}$ and $\mathsf{Enc2Vote}^*$ leak the ballot-vote relation during tallying; more advanced voting systems, such as Helios, do not.

Helios is intended to satisfy verifiability and ballot secrecy. For ballot secrecy, each voter encrypts their vote using a homomorphic encryption scheme. Those encrypted votes are homomorphically combined and the homomorphic combination is decrypted to reveal the outcome (**AdidaPereiraMarneffeQuisquater?**). Alternatively, a mixnet is applied to the encrypted votes and the mixed encrypted votes are decrypted to reveal the outcome (**Adida08?**; **Pereira11:HeliosMixnet?**). We refer to the former voting system as *Helios* and the latter as *Helios Mixnet*. For universal verifiability, the encryption and decryption steps are accompanied by non-interactive proofs demonstrating correct computation.

#### Contribution and structure.

Section <a href="#sec:nm-suffices" data-reference-type="ref" data-reference="sec:nm-suffices">[sec:nm-suffices]</a> proves that individual verifiability and an aspect of universal verifiability are satisfied by voting systems built from El Gamal coupled with proofs of correct key generation, thereby eliminating the expense of individual-verifiability proofs and simplifying universal-verifiability proofs for a class of encryption-based voting systems. Section <a href="#sec:heliosMixnet" data-reference-type="ref" data-reference="sec:heliosMixnet">[sec:heliosMixnet]</a> presents an analysis of Helios Mixnet that uncovers a vulnerability in implementations, discusses a fix, and proves that individual and universal verifiability are satisfied when the fix is applied. The remaining sections present syntax and definitions of individual and universal verifiability (§<a href="#sec:syntax" data-reference-type="ref" data-reference="sec:syntax">[sec:syntax]</a>) and a brief conclusion (§<a href="#sec:conclusion" data-reference-type="ref" data-reference="sec:conclusion">[sec:conclusion]</a>).

Definitions of cryptographic primitives, security definitions and proofs are deferred to an accompanying technical report (**Smyth18:heliosMixnetLong?**).

# Election scheme syntax and verifiability definitions

**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 403, column 17): expecting \end{document} \end{definition} ^`

``` latex
\section{Election scheme syntax and verifiability definitions}\label{sec:syntax}

We recall syntax for \emph{election schemes} (Definition~\ref{def:election})
from Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}.
Election schemes capture a class of voting systems
that consist of the following four steps.	
First, a tallier generates a key pair. 
Secondly, each voter constructs and casts a ballot for their vote. 
These ballots are recorded on a bulletin board.
Thirdly, the tallier 
tallies the recorded ballots and
announces an outcome, i.e., a frequency distribution of votes.
Finally, voters and other interested parties check that 
the outcome corresponds to votes expressed in recorded ballots.\footnote{%
	Smyth, Frink \& Clarkson use the syntax to model first-past-the-post voting
	systems and Smyth shows the syntax is sufficiently versatile to capture ranked-choice voting systems~\cite{2017-FPTP-suffices-for-ranked-voting}. Moreover, Smyth, Frink \& Clarkson
  extend the syntax to voting systems with eligibility 
  verifiability, which enables 
  anyone to check whether counted votes were cast by voters.
  (Quaglia \& Smyth~\cite{Smyth18:HeliosC} define a transformation from election schemes to 
  the extended syntax which ensures secrecy and verifiability.)
  Eligibility verifiability seems to require expensive infrastructures 
  for voter credentials and some systems 
  -- including Helios and  Helios Mixnet -- forgo eligibility verifiability 
  in favour of cheaper, non-verifiable ballot authentication mechanisms.
  Hence, we do not pursue eligibility verifiability further.
}

\begin{definition}[Election scheme~\cite{Smyth15:ElectionVerifiability}] \label{def:election}
An \emph{election scheme} is a tuple of probabilistic polynomial-time algorithms 
$(\SetupSymb,%\RegisterSymb,
	\VoteSymb,\TallySymb\VerifySymb)$ such that:

\begin{description}
\item $\SetupSymb$, denoted $(\pk,\sk,\mB,\mC) \leftarrow \Setup$,\footnote{%
	Let $A(x_1,\dots,x_n; r)$ denote the output of probabilistic algorithm $A$ on
	inputs $x_1,\dots,x_n$ and random coins $r$. Let $A(x_1,\dots,x_n)$ denote 
	$A(x_1,\dots,x_n;r)$, where $r$ is chosen uniformly at random. And let 
	$\leftarrow$ denote assignment.}
%
is run by the tallier.
It takes a security parameter $\kappa$ as input and outputs a key pair 
$\pk,\sk$, a maximum number of ballots $\mB$, 
and a maximum number of candidates $\mC$.

\item  $\VoteSymb$, denoted $b\leftarrow\Vote$, is run by voters. It
takes as input a public key $\pk$, a voter's vote $v$, some number of candidates 
$\nC$, and a security parameter $\kappa$. The vote should be selected from a
sequence  $1,\dots,\nC$ of candidates.
The algorithm outputs a ballot $b$ or error symbol $\perp$. 

\item  $\TallySymb$, denoted $(\outcome, \tpf)\leftarrow\Tally$, is run by the 
tallier. It takes as input a private key $\sk$, a bulletin board $\bb$, 
some number of candidates $\nC$, and a security parameter $\kappa$, where $\bb$ 
is a set. And outputs an election outcome $\outcome$ and a non-interactive tallying
proof $\tpf$ demonstrating that the outcome corresponds to votes expressed in
ballots on the bulletin board. The election outcome $\outcome$ should be a vector 
of length $\nC$ such that $\outcome[v]$ indicates the number of votes
for candidate $v$.\iflong\footnote{Let $\outcome[v]$ denote component $v$ of vector $\outcome$.}\fi

\item $\VerifySymb$, denoted $s \leftarrow \Verify$, is run to audit an election.
It takes as input a public key $\pk$, a bulletin board $\bb$,
some number of candidates $\nC$, an election outcome $\outcome$, a tallying proof 
$\tpf$, and a security parameter $\kappa$. And outputs a bit $s$, where $1$ 
signifies success and $0$ signifies failure.
\end{description}

\noindent
Election schemes must satisfy \emph{correctness}: there exists a negligible
function $\negl$, such that for all security parameters $\kappa$, integers 
$\nB$ and $\nC$, and votes $v_1,\dots,v_{\nB}\in\{1,\dots,\nC\}$, it holds that, 
given a zero-filled vector $\outcome$ of length $\nC$, we have:\\

{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup$;\\
\begin{algorithm}[H]
	\For{$1 \leq i \leq \nB$}{
		$b_i \leftarrow \Vote[\pk,v_i,\nC,\kk]$;\\
		$\outcome[v_i] \leftarrow \outcome[v_i] + 1$;
	}
	$(\outcome',\tpf) \leftarrow \Tally[\sk,\{b_1,\dots,b_{\nB}\},\nC, \kk]:$
	$\nB \leq \mB \wedge \nC\leq \mC \Rightarrow \outcome = \outcome'] > 1 - \neglK$.
\end{algorithm} 
}

\end{definition}

For individual verifiability, voters must be able to check whether their ballot is recorded.
Smyth, Frink \& Clarkson capture this notion using a game that challenges the adversary to 
provide inputs to algorithm $\VoteSymb$ that cause ballots to collide.

\begin{definition}[Individual verifiability~\cite{Smyth15:ElectionVerifiability}]\label{def:iv}
An election scheme $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ 
satisfies \emph{individual verifiability}, if for all probabilistic poly\-no\-mi\-al-time 
adversaries $\adv$, there exists a negligible function $\negl$, such that for all security 
parameters $\kk$, we have
$\Pr[(\pk, \nC,v,v') \leftarrow \adv(\kk);
	b\leftarrow\Vote[\pk,\nC,v,\kk];\allowbreak 
	b'\leftarrow\Vote[\pk,\nC,v',\kk]
	\mathrel : b = b' \wedge b \not= {\perp} \wedge b' \not= {\perp}] \leq \neglK$.
\end{definition}

For universal verifiability, anyone must be able to check whether 
the election outcome represents the votes used to construct 
ballots on the bulletin board. The formal definition of 
universal verifiability by Smyth, Frink \& Clarkson
requires algorithm $\VerSymb$ to accept if and only if 
the election outcome is correct.\footnote{%
  Quaglia \& Smyth~\cite{Smyth17:voting-tutorial} provide a tutorial-style introduction to 
  the individual and universal verifiability definitions by Smyth, Frink \& Clarkson, 
  and Smyth~\cite{Smyth18:voting-tutorial} provides a detailed technical introduction.}
%
The \emph{if} requirement is captured by completeness (Definition~\ref{def:UVComplete}), which 
stipulates that election outcomes produced by algorithm $\TallySymb$
will actually be accepted by algorithm $\VerSymb$. And the \emph{only if} requirement 
is captured by soundness (Definition~\ref{def:UVSoundness}), which challenges an adversary to concoct 
a scenario in which algorithm $\VerSymb$ accepts, but the election outcome is not correct.

\begin{definition}[Completeness~\cite{Smyth15:ElectionVerifiability}]\label{def:UVComplete}
An election scheme $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies \emph{completeness}, 
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\negl$, such that 
for all security parameters $\kk$, we have
%
$
\Pr [(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC) \leftarrow\allowbreak \Setup;\allowbreak
		 (\bb,\nC)\leftarrow\adv(\pk,\kk);
     (\outcome,\allowbreak\tpf) \leftarrow\allowbreak \Tally
%	
:\allowbreak |\bb| \leq \mB \wedge\allowbreak \nC\leq \mC\allowbreak\Rightarrow\VerSymb(\pk,\allowbreak\bb,\allowbreak\nC,\allowbreak\outcome,\allowbreak\tpf,\allowbreak\kk) =\allowbreak 1] >\allowbreak 1 - \neglK
$.
\end{definition}

Smyth, Frink \& Clarkson capture correct election
outcomes using function $\correcttally$, which is defined such that 
$
\correcttally(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak\kk)[v] =\allowbreak \ell$ 
iff $\exists^{=\ell} b\in \bb \setminus \{\bot\} : 
\exists r : b=\Vote[\pk,\allowbreak v,\allowbreak\nC,\allowbreak\kk;\allowbreak r]
$,\footnote{%
		Function $\correcttally$ uses a 
		\emph{counting quantifier}~\cite{Schweikardt05} denoted $\exists^{=}$.
		Predicate $(\exists^{=\ell} x : P(x))$ holds exactly when there are
		$\ell$ distinct values for $x$ such that $P(x)$ is satisfied.
		Variable $x$ is bound by the quantifier, whereas $\ell$ is free.}
where $\correcttally(\pk,\nC,\allowbreak\bb,\allowbreak\kk)$ is a vector of length $\nC$
and $1 \leq v \leq \nC$.
Hence, component $v$ of vector 
$\correcttally(\allowbreak\pk,\allowbreak \nC,\bb,\allowbreak\kk)$ 
equals $\ell$ iff there exist $\ell$ ballots on the bulletin board that are votes 
for candidate $v$. The function requires ballots to be interpreted for only
one candidate, which can be ensured by injectivity.\iflong\footnote{Injectivity resembles 
  individual verifiability, except individual verifiability allows votes to be equal.}\fi

\begin{definition}[Injectivity]
An election scheme $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies \emph{injectivity},\footnote{%
	Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability} consider a definition of 
	injectivity which quantifies over all public keys, rather than public keys constructed by an 
	adversary. That definition is stronger than necessary.}
\begin{comment}
if for all probabilistic polynomial-time adversaries $\adv$ and security parameters $\kk$,
we have 
%
$
\Pr [(\pk,\nC,v,v') \leftarrow \adv(\kk);
	b\leftarrow \Vote[\pk,v,\nC,\kk];\allowbreak
	b'\leftarrow \Vote[\pk,v',\nC,\kk]
%
	: v\neq v' \wedge b\neq \bot \wedge b'\neq \bot \Rightarrow b\neq b'] = 1
$.
\end{comment}
if for all probabilistic polynomial-time adversaries $\adv$, security parameters $\kk$
and computations 
$
  (\pk,\nC,v,v') \leftarrow \adv(\kk);
  b\leftarrow \Vote[\pk,v,\nC,\kk];\allowbreak
	b'\leftarrow \Vote[\pk,v',\nC,\kk]
$
such that $v\neq v' \wedge b\neq \bot \wedge b'\neq \bot$, we have
$b\neq b'$.
\end{definition}

\begin{definition}[Soundness~\cite{Smyth15:ElectionVerifiability}]\label{def:UVSoundness}
An election scheme $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$
satisfies \emph{soundness}, if $\Gamma$ satisfies injectivity and 
for all probabilistic 
poly\-no\-mi\-al-time adversaries $\adv$, 
there exists a negligible function $\negl$, such that
for all security parameters $\kk$, we have
$\Pr[(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak\outcome,\allowbreak\tpf) \leftarrow\allowbreak \adv(\kk)\allowbreak
	\mathrel : \outcome \not=\allowbreak \correcttally(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak \kk) \mathrel\wedge\allowbreak \VerSymb(\pk,\allowbreak\bb,\allowbreak\nC,\allowbreak \outcome,\allowbreak\tpf,\allowbreak\kk) =\allowbreak 1] \leq \neglK$.
\end{definition}

\begin{definition}[Universal verifiability]\label{def:UV}
An election scheme $\Gamma$ satisfies \emph{universal verifiability}, if 
completeness, injectivity and soundness are satisfied.
\end{definition}

\paragraph{Comparison with other verifiability definitions.}

Other definitions of verifiability exist. In particular, definitions have been 
proposed by 
Juels, Catalano \& Jakobsson~\cite{JCJ10}, 
Cortier \emph{et al.}~\cite{Cortier14:verifiability} and 
Kiayias, Zacharias \& Zhang~\cite{Kiayias15}. 
Smyth, Frink \& Clarkson~\cite[\S7]{Smyth15:ElectionVerifiability} show that definitions 
by Juels, Catalano \& Jakobsson and Cortier \emph{et al.} do not detect attacks that 
arise  when tallying and verification procedures are corrupt nor when verification procedures 
reject legitimate outcomes. Moreover, they show that the definition by 
Kiayias, Zacharias \& Zhang does not detect the latter class of attacks.
By comparison, Definition~\ref{def:UV} detects these attacks, thereby motivating
its adoption.

K\"usters \emph{et al.}~\cite{Kusters10,Kusters11:UniversalVerifiability,Kusters12:ClashAttacks}
propose an alternative, holistic notion of verifiability called 
\emph{global verifiability}, which must be instantiated with a goal. 
Smyth, Frink \& Clarkson~\cite[\S8]{Smyth15:ElectionVerifiability} show that 
goals proposed by K\"usters \emph{et al.}~\cite[\S5.2]{Kusters10b} and 
by Cortier et al.~\cite[\S10.2]{Cortier16:VerifiabilitySoK} are too strong
(in the sense that they cannot be satisfied by some verifiable voting systems, 
including Helios).
Moreover, Smyth, Frink \& Clarkson propose a slight weakening of the goal by 
K\"usters \emph{et al.} and proved that their notion of verifiability is strictly 
stronger than global verifiability with that goal (the ``gap" is due to 
an uninteresting technical detail), which further motivates the 
adoption of Definition~\ref{def:UV}.\footnote{%
  Cortier \emph{et al.}~\cite[\S8.5 \& \S10.1]{Cortier16:VerifiabilitySoK} claim that 
  definitions by Smyth, Frink \& Clarkson are flawed. 
  Those claims were discussed with Cortier \emph{et al.} (email communication, April'16) 
  and are believed to be false~\cite[\S9]{Smyth15:ElectionVerifiability}.
  %
  Moreover, Smyth, Frink \& Clarkson prove that any flaw in their
  definitions implies flaws in the context of global verifiability, 
  which should increase confidence in their definitions.
}



\begin{comment}
Voting systems rely on authentication mechanisms to ensure that only voters' 
votes are counted. Some such mechanisms are verifiable, enabling
anyone to check whether counted votes were cast by voters. This is known as 
eligibility verifiability~\cite{Smyth10:ElectionVerifiability,Smyth15:ElectionVerifiability}. 
Satisfying eligibility verifiability appears to be expensive. Indeed, known
solutions require infrastructures for voter credentials. And some voting 
systems forgo eligibility verifiability in favour of cheaper, non-verifiable 
authentication mechanisms. For instance, Helios relies on authentication 
via Facebook, Google or Yahoo using OAuth.\footnote{
  Meyer \& Smyth describe the application of OAuth in Helios~\cite{Smyth16:helios-eligibility}.
}
Although such third parties might convince themselves that only voters' 
votes are counted, their ability to convince other parties is limited
to their ``good word or sworn testimony"~\cite{Neff03}. Hence, voting 
systems satisfying eligibility verifiability are preferable, but systems
without eligibility verifiability are nonetheless interesting and the 
focus of this paper.
\end{comment}


```

# Encryption ensures individual verifiability \\ injectivity

**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 376, column 17): expecting \end{document} \end{definition} ^`

``` latex
\section{Encryption ensures individual verifiability \& injectivity}\label{sec:nm-suffices}

Definitions of individual verifiability and injectivity only focus on 
properties of algorithm $\VoteSymb$, hence, to prove these properties
for election scheme $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$,
it suffices to prove the existence of an election scheme 
$(\SetupPrimeSymb,\allowbreak\VoteSymb,\allowbreak\TallyPrimeSymb,\allowbreak\VerifyPrimeSymb)$
satisfying both properties. We demonstrate the existence of
such schemes by coupling election scheme $\encToVoteSymb$
with proofs of correct key generation.%, and using an encryption scheme that proves correct ciphertext construction. 
\footnote{%
  Election scheme $\encToVoteStarSymb$ (\S\ref{sec:intro}) couples 
  $\encToVoteSymb$ with proofs of correct key generation \emph{and} proofs
  of correct decryption, hence, it is distinguished from schemes produced
  by $\encToVotePlusSymb$. This distinction enables $\encToVoteStarSymb$ 
  to satisfy individual and universal verifiability, whereas 
  $\encToVotePlusSymb$ cannot produce schemes satisfying universal 
  verifiability.% It is nonetheless useful for proofs of individual verifiability and injectivity.
}\textsuperscript{,}\footnote{%
  Election scheme $\encToVotePlus$ adopts the setup algorithm formalised
  by Smyth, Frink \& Clarkson for Helios~\cite[Appendix~C]{Smyth15:ElectionVerifiability}.
}

\begin{definition}[$\encToVotePlusSymb$]
Suppose $\Pi = (\GenSymb,\allowbreak\EncSymb,\DecSymb)$ is an asymmetric encryption scheme,
$\Sigma$ is a sigma protocol that proves correct key generation, and $\mathcal H$ is a hash function. 
Let $\sFS{\Sigma}{\allowbreak\mathcal H} = (\ProveKeySymb,\allowbreak \VerKeySymb)$.\footnote{%
	Let $\sFS{\Sigma}{\mathcal H}$ denote the non-interactive proof system derived 
	by application of the Fiat-Shamir transformation to sigma protocol $\Sigma$ 
	and hash function $\mathcal H$.}
We define $\encToVotePlus = (\SetupSymb,\VoteSymb,\TallySymb,\VerifySymb)$ 
such that:

\begin{itemize}
\item $\Setup$ selects coins $s$ uniformly at random, computes 
		$(\pk,\sk,\votespace) \leftarrow \Gen[\kk;\allowbreak s];\allowbreak
	   \rho \leftarrow \ProveKey[(\kk,\allowbreak\pk,\allowbreak\mathfrak m),(\allowbreak\sk,\allowbreak s),\kk];
     \pk'\leftarrow(\pk,\votespace,\rho);
     \sk'\leftarrow(\pk,\allowbreak\sk)$,
		derives $\mC$ as the largest integer such that $\{0,\dots,\mC\}\subseteq\{0\} \cup\mathfrak m$
    and for all $m_0,m_1\in\{1,\dots,\mC\}$ we have $|m_0|=|m_1|$, and 
		outputs $(\pk',\sk',p(\kappa),\mC)$, where $p$ is a polynomial function.

\item $\Vote[\pk',v,\nC,\kk]$ parses $\pk'$ as vector $(\pk,\votespace,\rho)$, outputting $\perp$ if parsing fails or
	$\VerKey \not= 1 \vee v\not\in\{1,\dots,\nC\} \vee \{1,\dots,\nC\}\not\subseteq \votespace$, computes $b\leftarrow\Enc{v}$, and outputs $b$.

\item $\Tally[\sk',\bb,\nC,\kk]$ initialises vector $\outcome$ of length $\nC$, parses $\sk'$ as vector $(\pk,\sk)$, outputting $(\outcome,\perp)$ if parsing fails,  
computes 
{ \DontPrintSemicolon
\llFor{$b\in\bb$}{%
$v\leftarrow\Dec{b};$
\llIf{$1\leq v\leq \nC$}{${\bf v}[v] \leftarrow {\bf v}[v]+1$}%
}%
}, and outputs 
$(\outcome,\epsilon)$, where $\epsilon$ is a constant symbol.
	
\item $\Verify$ outputs 1. 
\end{itemize}
\end{definition}

\noindent
To ensure $\encToVotePlus$ is an election scheme, we require asymmetric
encryption scheme $\Pi$ to produce distinct ciphertexts with overwhelming
probability. Hence, we restrict the class of asymmetric encryption schemes 
used to instantiate $\encToVotePlusSymb$.

\begin{lemma}\label{lem:Enc2Vote:correctness}
%Given an asymmetric encryption scheme $\Pi$,
%a sigma protocol $\Sigma$ that proves correct key generation, and a hash function
%$\mathcal H$, we have $\encToVotePlus$ is an election
%scheme.
Let $\Pi= (\GenSymb,\allowbreak\EncSymb,\DecSymb)$ be an asymmetric encryption scheme, $\Sigma$ be a sigma protocol 
that proves correct key generation, and $\mathcal H$ be a hash function.
We have $\encToVotePlus[\Pi,\allowbreak\Sigma,\allowbreak\mathcal H]$ is an election scheme if for all security parameters 
$\kk$ and messages $m$ and $m'$, we have 
$\Pr [
	(\pk,\sk,\mathfrak m) \leftarrow\Gen; 
	c\leftarrow \Enc{m};
  c'\leftarrow \Enc{\allowbreak m'}:
	m,m'\in\mathfrak m \Rightarrow
	c \not=c'] > 1-\neglK$.
\end{lemma}

\noindent
Our correctness proof (Lemma~\ref{lem:Enc2Vote:correctness}) and all further proofs 
appear in\iflong\ Appendix~\ref{app:proofs}\else~\cite[Appendix~B]{Smyth18:heliosMixnetLong}\fi.

Security properties of asymmetric encryption schemes ensure ciphertexts do not 
collide. Indeed, IND-CPA demands that no adversary can construct a ciphertext
that collides with the challenge ciphertext.\footnote{%
  Correctness of asymmetric encryption schemes only ensures ciphertexts do not 
  collide for distinct plaintexts.}
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 election scheme 
$\encToVotePlus[\Pi,\Sigma,\mathcal H]$ satisfies individual verifiability
and injectivity. Nonetheless, given that the scheme's $\VoteSymb$ algorithm 
checks correct key generation, it suffices that ciphertexts do not collide for 
correctly generated keys.

\begin{proposition}\label{prop:iv-injForFree}
Let $\Pi= (\GenSymb,\allowbreak\EncSymb,\DecSymb)$ be an asymmetric encryption scheme, 
$\Sigma$ be a sigma protocol that proves correct key generated, and
$\mathcal H$ be a hash function. 
We have $\encToVotePlus[\Pi,\Sigma,\mathcal H]$ satisfies individual verifiability 
if for all probabilistic polynomial-time adversaries $\adv$ and security parameters $\kk$ we have
\begin{multline*}
	\Pr[(\pk,\mathfrak{m},\rho,m,m')\leftarrow \adv(\kk); c\leftarrow\Enc{m};
		c'\leftarrow\Enc{m'} \\\mathrel: \VerKey =\allowbreak 1 \wedge m,m'\in\mathfrak{m}
		\Rightarrow c \not=c'] > 1 -\neglK,
\end{multline*}
where $\sFS{\Sigma}{\allowbreak\mathcal H} = (\ProveKeySymb,\allowbreak \VerKeySymb)$.
Moreover, the election scheme satisfies injectivity if the probability is $1$ when 
plaintexts $m$ and $m'$ are distinct.
\end{proposition}

\noindent
Our proof of Proposition~\ref{prop:iv-injForFree}\iflong\ (Appendix~\ref{app:prop:iv-injForFree}) \else~\cite[Appendix~B.2]{Smyth18:heliosMixnetLong} \fi 
follows immediately from our preconditions. It is nevertheless useful, because the 
preconditions are defined over encryption scheme $\Pi$ and proof system 
$\sFS{\Sigma}{\allowbreak\mathcal H}$, rather than election scheme 
$\encToVotePlus[\Pi,\Sigma,\mathcal H]$, which makes the preconditions
easier to reason with.
%
For El~Gamal~\cite{ElGamal85}, the preconditions are ensured if the proof system 
checks parameters:

\begin{definition}\label{def:checkElGamalParams}
Let $(\ProveKeySymb,\allowbreak \VerKeySymb)$ be a non-interactive proof
system that proves correct key generation. The proof system \emph{checks
El Gamal parameters}, if for all security parameters $\kappa$, public keys
$\pk$, messages spaces $\mathfrak m$, and proofs $\rho$, we have 
$\VerKey =\allowbreak 1$ implies 
$\pk$ is a vector $(p,q,g,h)$ such that $p = 2 \cdot q + 1$, $|q| = \kk$, $g$ is a generator 
of $\mathbb Z_p^*$ of order $q$, $h\in\mathbb Z_p^*$, and $\votespace = \{1,\dots,p-1\}$.
\end{definition}

\begin{theorem}\label{thm:iv-injForFree}
Let $\Pi$ be El Gamal, $\Sigma$ be a sigma protocol that proves correct key generation, and
$\mathcal H$ be a hash function. 
Suppose proof system $\sFS{\Sigma}{\allowbreak\mathcal H}$ checks El~Gamal parameters.
We have $\encToVotePlus[\Pi,\Sigma,\mathcal H]$ satisfies individual verifiability and injectivity.
\end{theorem}

\begin{comment}
\begin{proof}[Proof sketch]
An El Gamal ciphertext on a plaintext $m$ is a pair $g^r \pmod p,\allowbreak {h^r \cdot m \pmod p}$ for some 
coins $r$ chosen uniformly at random from $\mathbb Z_q^*$. It follows from Definition~\ref{def:checkElGamalParams}
that El Gamal ciphertexts are distinct with overwhelming probability for a particular plaintext due 
to the overwhelming probability of choosing distinct coins and are always distinct for different plaintexts. 
Thus, we conclude by Proposition~\ref{prop:iv-injForFree}, since the proposition's preconditions are satisfied.
\end{proof}
\end{comment}

\noindent
We exploit Theorem~\ref{thm:iv-injForFree} in the following section to derive a 
proof of individual verifiability for free and to simplify 
a proof of universal verifiability.



```

# Case study: Helios Mixnet

**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 562, column 17): expecting \end{document} \end{enumerate} ^`

``` latex
\section{Case study: Helios Mixnet}\label{sec:heliosMixnet}

Helios Mixnet can be informally modelled as an election scheme such that:

\begin{description}

\item $\SetupSymb$ generates a key pair for an asymmetric homomorphic encryption scheme, proves correct key generation in zero-knowledge, and outputs the public key coupled with the proof.

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

\item $\TallySymb$ 
\begin{comment}
	discards any ballots on the bulletin board for which proofs do not hold, mixes the ciphertexts in the remaining ballots, decrypts the ciphertexts output by the mix to reveal the distribution of candidate preferences, and announces that distribution, along with proofs demonstrating correct decryption.
\end{comment}
	selects the ballots on the bulletin board for which proofs hold, mixes the ciphertexts in those ballots, decrypts the ciphertexts output by the mix to reveal the frequency distribution of candidate preferences, and announces that distribution, along with zero-knowledge proofs demonstrating correct decryption and mixing.

\item $\VerifySymb$ checks the proofs and accepts the frequency distribution if these checks succeed.

\end{description}

\noindent
Neither Adida~\cite{Adida08} nor Bulens, Giry \& Pereira~\cite{Pereira11:HeliosMixnet}
have released an implementation of Helios Mixnet.\footnote{%
	The planned implementation of Helios Mixnet (\url{http://documentation.heliosvoting.org/verification-specs/mixnet-support}, published c. 2010, accessed 19 Dec 2017,
  and \url{https://web.archive.org/web/20110119223848/http://documentation.heliosvoting.org/verification-specs/helios-v3-1}, 
	published Dec 2010, accessed 15 Sep 2017) has not been released.}
Tsoukalas \emph{et al.}~\cite{Tsoukalas13:HeliosToZeus} released \emph{Zeus} as a fork of Helios~3.1.4 
spliced with mixnet code to derive an implementation,\iflong\footnote{%
	\url{https://github.com/grnet/zeus}, accessed 15 Sep 2017.}\fi\
and Yingtong Li released \emph{helios-server-mixnet} as an extension of Zeus
with threshold asymmetric encryption.% and some other minor changes.
\iflong\footnote{\url{https://github.com/RunasSudo/helios-server-mixnet}, accessed 15 Sep 2017.}\fi\
Both implementations use multiplicatively-homomorphic asymmetric encryption, rather than additively-homomorphic encryption. 
\begin{comment}
moreover, they both prove correct ciphertext construction, rather than proving correct ciphertext construction for a vote
selected from a sequence of candidates.
\end{comment}

Chang-Fong \& Essex~\cite{Essex16:HeliosVerifiability} show that Helios 2.0 does 
not satisfy completeness (because cryptographic parameters were not checked for
suitability), hence, implementations of Helios Mixnet
did not satisfy completeness until Helios was patched (because the 
implementations fork Helios and do not add code to check parameters).\footnote{%
	\url{https://github.com/benadida/helios-server/pull/133}, published 31 May 2016, accessed 21 Sep 2017.}
Moreover, Bernhard, Pereira \& Warinschi~\cite{Bernhard12:Helios} show that Helios~3.1.4 does not satisfy soundness.%
%because tallying proofs can be falsified,
\footnote{%
  Bernhard, Pereira \& Warinschi show that a malicious tallier can add votes 
  for their preferred candidate and remove votes for other candidates.
  Smyth, Frink \& Clarkson formalise that attack 
  and prove that soundness is not satisfied~\cite{Smyth15:ElectionVerifiability}.
}\textsuperscript{,}%
\footnote{%
  A further soundness vulnerability is known~\cite{Smyth15:ElectionVerifiability},
  as are secrecy~\cite{Smyth12:Helios} and eligibility~\cite{Smyth16:helios-eligibility}
  vulnerabilities.
}
They also demonstrate a denial of service attack.
We exploit their denial of service attack to show that implementations of 
Helios Mixnet do not satisfy soundness:
 A malicious tallier can decrypt the ciphertexts output by the mix 
to reveal the distribution of candidate preferences, select the ciphertexts that decrypt to
the tallier's preferred subdistribution, prove correct decryption of those ciphertexts, and exploit the 
attack by Bernhard, Pereira \& Warinschi to falsify proofs that the remaining ciphertexts decrypt to 
arbitrary elements of the message space, thereby enabling the malicious tallier to exclude votes from 
the election outcome. 

\begin{remark}\label{rem:heliosM}
Zeus does not satisfy soundness.
%Implementations of Helios Mixnet do not satisfy soundness.
%Neither Zeus nor helios-server-mixnet satisfy soundness.
\end{remark}

\noindent
%It follows that the Helios Election System with mixnet support does not satisfy
%soundness either. An informal proof of these claims follows from our discussion 
%and a formal proof is omitted. 
%An informal proof of Remark~\ref{rem:heliosM} follows from our discussion 
%and we do not pursue a formal proof.
Similarly, helios-server-mixnet does not satisfy soundness when a $(n,n)$-threshold
is used. An informal proof of these claims follows from our discussion 
and a formal proof is omitted. 


Helios~3.1.4 uses additively-homomorphic El Gamal, hence, 
an adversary can 	falsify that ciphertexts decrypt to arbitrary elements of the group, but cannot 
recover the corresponding messages, because solving discrete logarithms for arbitrary group elements 
is hard. Thus, the attack by Bernhard, Pereira \& Warinschi leads to a denial of service attack 
against Helios 3.1.4, whereby the election outcome is not recovered, rather than an attack that violates
soundness. %(another attack by Bernhard, Pereira \& Warinschi does violate soundness). 
By comparison, our attack against implementations of Helios Mixnet violates soundness, 
because a malicious tallier can exclude votes from the election outcome.

Bernhard, Pereira \& Warinschi attribute vulnerabilities of Helios 3.1.4 to use of
the Fiat-Shamir transformation without including statements in hashes (i.e., the weak 
Fiat-Shamir transformation), and recommend including statements in hashes (i.e., using
the Fiat-Shamir transformation) as a defence. Implementations of Helios Mixnet can be 
extended to use the Fiat-Shamir transformation and we derive a formalisation of that 
extension from $\encToVotePlus$ by replacing its tallying and verification algorithms,\footnote{%
	The tallying and verification algorithms in Definition~\ref{def:mixnetHelios}
	adapt (unpublished) algorithms prepared by Quaglia \& Smyth in 
	the context of ~\cite{Smyth15:Hawk}. Quaglia \& Smyth have since 
	incorporated these adaptations into their work to take advantage 
	of the results presented in this manuscript.}
and by using a suitable asymmetric encryption algorithm. Using the Fiat-Shamir transformation
(rather than the weak Fiat-Shamir transformation) ensures that proofs of correct decryption
cannot be falsified, hence, the formalisation is not vulnerable to the aforementioned attack.


\begin{definition}\label{def:mixnetHelios}
Suppose $\Pi = (\GenSymb,\allowbreak\EncSymb,\DecSymb)$ is a homomorphic asymmetric encryption algorithm, 
$\Sigma_1$ is a sigma protocol that proves correct key construction, 
$\Sigma_2$ is a sigma protocol that proves plaintext knowledge, 
and $\mathcal H$ is a hash function. 
Let $\sFS{\Sigma_1}{\allowbreak\mathcal H} = (\ProveKeySymb,\allowbreak \VerKeySymb)$ and 
$\sFS{\Sigma_2}{\allowbreak\mathcal H} = (\SignCiphSymb,\allowbreak \VerCiphSymb)$.
Moreover, let $\pi(\Pi,\Sigma_2,\mathcal H) = (\GenSymb,\allowbreak\EncPrimeSymb,\DecPrimeSymb)$
be an asymmetric encryption scheme such that:

\begin{itemize}
\item $\EncPrime{v}$ selects coins $r$ uniformly at random, computes 
$
	c \leftarrow \Enc{v;r};\allowbreak\sigma \leftarrow \SignCiphh{\pk, c}{v, r}
$,
and outputs $(c,\sigma)$.
\end{itemize}

\begin{comment}
\begin{proof}[$\Pi'$ is an asymmetric encryption]
Let $\DecPrimeSymb$ be defined such that

\begin{itemize}
\item $\DecPrimeSymb{c'}$ parses $c'$ as $(c,\sigma)$, outputting $\perp$ if parsing fails or 
$\VerCiphSymb((\pk,\allowbreak c),\sigma,\kappa)\not=1$, computes $v \leftarrow\Dec{c}$,
and outputs $v$.
\end{itemize}

\noindent
We have $\Pi'$ is asymmetric encryption scheme. Indeed, suppose $\kk$ is a security parameter 
and $m$ is a message. Further suppose $(\pk,\sk,\mathfrak m)$ is an output 
of $\Gen$ such that $m\in\mathfrak m$ and $c$ is an output of $\EncPrime{m}$. 
By definition of algorithm $\EncPrimeSymb$, there exist coins $r$ such that 
$c[1]= \Enc{v;r}$ and $\sigma$ is an output of $\SignCiphh{\pk, c}{v, r}$. 
By completeness $(\SignCiphSymb,\allowbreak \VerCiphSymb)$, we have 
$\VerCiphSymb((\pk,\allowbreak c[1]),\sigma,\kappa)=1$, with overwhelming 
probability. It follows by correctness of $\Pi$ 
that $\DecPrime{c} = v$, with overwhelming probability.
Thus, $\Pi'$ an is asymmetric encryption scheme.
\end{proof}
\end{comment}

\noindent
Suppose $\Sigma_3$ is a sigma protocol that proves correct decryption and $\Sigma_4$ is a sigma protocol that 
proves mixing. 
Let $\sFS{\Sigma_3}{\allowbreak\mathcal H} = (\ProveDecSymb,\allowbreak \VerDecSymb)$ and
$\sFS{\Sigma_4}{\allowbreak\mathcal H} = (\ProveMixSymb,\allowbreak \VerMixSymb)$.
We define 
$\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H) = (\SetupSymb,\VoteSymb,\allowbreak\TallySymb,\VerifySymb)$, where 
$\encToVotePlus[\pi(\Pi,\Sigma_2,\mathcal H),\Sigma_1,\mathcal H] = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallyPrimeSymb,\allowbreak\VerifyPrimeSymb)$ and algorithms $\TallySymb$ and $\VerifySymb$
are defined below.\\

\noindent
$\Tally[\sk',\nC,\bb,\kk]$ initialises $\outcome$ as a zero-filled vector of length $\nC$, parses $\sk'$ as a vector $(\pk,\sk)$, outputting $(\outcome,\perp)$ if parsing fails, and proceeds as follows:
%
\begin{enumerate}
\item\label{heliosM:tally:invalidBallots} \emph{Remove invalid ballots.}
Let $\{b_1, \dots, b_\ell\}$ be the largest 
subset of $\bb$ such that for all $1 \leq i \leq \ell$ we have $b_i$
is a pair and 
$\VerCiphSymb((\pk,\allowbreak b_i[1]),b_i[2],\kappa) =1$.
If $\{b_1, \dots, b_\ell\} = \emptyset$, then output $(\outcome,\perp)$.

\item\label{heliosM:tally:mix} \emph{Mix.} Select a permutation $\chi$ on $\{1,\dots,\ell\}$ uniformly at random, 
	initialise ${\bf bb}$ and ${\bf r}$ as vectors of length $\ell$, fill
	${\bf r}$ with coins chosen uniformly at random, and compute

{\upshape
\begin{algorithm}[H]
	\For{$1 \leq i \leq \ell$}
	{
		${\bf bb}[i] \leftarrow b_{\chi(i)}[1] \otimes \Enc{\mathfrak e; {\bf r}[i]}$;
	}
	$\tpf_1 \leftarrow \ProveMixSymb((\pk,(b_1[1],\dots,b_\ell[1]),{\bf bb}),({\bf r},\chi),\kappa)$;
\end{algorithm}
}

	where $\mathfrak e$ is an identity element of $\Pi$'s message space with respect to $\odot$.

\item\label{heliosM:tally:dec} \emph{Decrypt.} Initialise ${\bf W}$ and $\tpf_2$ as vectors of length $\ell$ and compute:

{\upshape
\begin{algorithm}[H]
	\For{$1 \leq i \leq \ell$}
	{
		${\bf W}[i] \leftarrow\Dec{{\bf bb}[i]}$\;
		$\tpf_2[i] \leftarrow \ProveDec{\pk, {\bf bb}[i],{\bf W}[i]}{\sk}$\;
		\If{$1\leq {\bf W}[i]\leq \nC$}{
			$\outcome[{\bf W}[i]]\leftarrow\outcome[{\bf W}[i]]+1$\;
		}
	}%
\end{algorithm}%
}%
\end{enumerate}%
%
\noindent
Output $(\outcome,({\bf bb},\tpf_1,{\bf W},\tpf_2))$.\\



\noindent
$\VerSymb(\pk',\nC, \bb,  \outcome, \tpf, \kappa)$ derives the largest integer $\mC$ such that 
$\{0,\dots,\mC\}\subseteq\{0\} \cup \mathfrak m$; parses $\pk'$ as a vector $(\pk,\mathfrak m,\rho)$
and $\outcome$ parses as a vector of length $\nC$, 
	outputting $0$ if parsing fails, $\VerKey\allowbreak \not=\allowbreak 1$, $|\bb| \not\leq p(\kappa)$, or $\nC\not\leq\mC$, 
	where $p$ is the polynomial function used by algorithm $\SetupSymb$ to bound the maximum number of ballots;
and proceeds as follows:

\begin{enumerate}
\item\label{heliosM:verify:invalidBallots} \emph{Remove invalid ballots.} Compute $\{b_1,\dots,b_\ell\}$ as per Step~\ref{heliosM:tally:invalidBallots} of algorithm $\TallySymb$. If $\{b_1, \dots, b_\ell\} = \emptyset$ and
$\outcome$ is a zero-filled vector, then output $1$. Otherwise, perform the following checks.

\item\label{heliosM:verify:mix}\emph{Check mixing.} Parse $\tpf$ as a vector $({\bf bb},\tpf_1,{\bf W},\tpf_2)$, outputting $0$ if parsing fails, and check 
$\VerMixSymb((\pk,(b_1[1],\dots,b_\ell[1]),{\bf bb}),\tpf_1,\kappa) = 1$.

\item\label{heliosM:verify:dec} \emph{Check decryption.}
\begin{comment}
Initialise $\outcome'$ as a zero-filled vector of length $\nC$ and compute

{\upshape
\begin{algorithm}[H]
	\For{$1 \leq i \leq \ell$}
	{
		\If{$1\leq {\bf W}[i] \leq \nC$}{
			$\outcome'[{\bf W}[i]]\leftarrow\outcome'[{\bf W}[i]]+1$\;
		}
	}
\end{algorithm}
}

\noindent
Check $\outcome=\outcome'$, 
\end{comment}
Check ${\bf W}$ and $\tpf_2$ are vectors of length $\ell$, $\bigwedge_{i=1}^{\ell}\VerDec{\pk,\allowbreak {\bf bb}[i],\allowbreak{\bf W}[i]}{\allowbreak\tpf_2[i]} = 1$, and $\bigwedge_{v=1}^{\nC}\exists^{=\outcome[v]} i\in\{1,\dots,\ell\} : v = {\bf W}[i]$.
\end{enumerate}
If the above checks hold, then output $1$, otherwise, output $0$.
\end{definition}

\begin{lemma}\label{lem:heliosMCorrectness}
Suppose $\Pi$, $\Sigma_1$, $\Sigma_2$, $\Sigma_3$, $\Sigma_4$ and $\mathcal H$
satisfy the preconditions of Definition~\ref{def:mixnetHelios} and $\Pi$ satisfies
the condition in Lemma~\ref{lem:Enc2Vote:correctness}. We have 
$\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ is an election scheme.
\end{lemma}


Our formalisation of Helios Mixnet is similar to the formalisation of Helios
by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}. The main 
distinctions are as follows: First, given a vote $v$ from a sequence of candidates 
$1,\dots,\nC$, a Helios-Mixnet ballot contains an encryption of $v$, whereas
a Helios ballot contains ciphertexts $c_1,\allowbreak\dots,\allowbreak c_{\nC-1}$ such that if 
$v< \nC$, then $c_v$ encrypts plaintext one and the remaining ciphertexts
all encrypt zero, otherwise, all ciphertexts encrypt zero. (Both Helios Mixnet and
Helios ballots prove correct ciphertext construction, only Helios ballots prove 
the vote is selected from the sequence of candidates.) Secondly, Helios Mixnet
decrypts individual ciphertexts after mixing, whereas Helios homomorphically combines 
ciphertexts and decrypts the resulting homomorphic combination. (Both
Helios Mixnet and Helios prove correct decryption. For Helios Mixnet, decryption of 
individual votes is proved correct. Whereas Helios proves correct decryption of the 
election outcome.) Finally, the aforementioned distinctions lead to slight 
differences in the verification algorithms.


Since election schemes $\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ and $\encToVotePlus[\pi(\Pi,\allowbreak\Sigma_2,\allowbreak\mathcal H),\allowbreak\Sigma_1,\allowbreak\mathcal H]$ share the same voting algorithm, both schemes satisfy individual verifiability and injectivity by Proposition~\ref{prop:iv-injForFree}, assuming the proposition's preconditions are satisfied. Moreover, since the preconditions hold for El Gamal when parameters are checked
(Corollary~\ref{prop:iv-injForFree}), we have:

\begin{corollary}\label{cor:heliosM}
Suppose $\Pi$, $\Sigma_1$, $\Sigma_2$, $\Sigma_3$, $\Sigma_4$ and $\mathcal H$
satisfy the preconditions of Definition~\ref{def:mixnetHelios}. Further suppose 
$\Pi$ is El Gamal and $\Sigma_1$ checks El Gamal parameters.
Election scheme $\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies individual verifiability and injectivity.
\end{corollary}

\noindent
To evaluate whether universal verifiability is satisfied, it remains to consider completeness 
and soundness.\footnote{Our proof of Theorem~\ref{thm:heliosM} uses a result by Bernhard 
  \emph{et al.}~\cite{Bernhard12:Helios} that shows non-interactive proof systems derived by
  application of the Fiat-Shamir transformation satisfy zero-knowledge, assuming the underlying 
  sigma protocols satisfy \emph{special soundness} and \emph{special honest-verifier zero-knowledge}.
  We will not need the details of those properties, so we omit formal definitions; 
  see Bernhard \emph{et al.} for formalisations.}

\begin{theorem}\label{thm:heliosM}
Suppose $\Pi$, $\Sigma_1$, $\Sigma_2$, $\Sigma_3$, $\Sigma_4$ and $\mathcal H$
satisfy the preconditions of Definition~\ref{def:mixnetHelios}.
Moreover, suppose $\Sigma_2$ satisfies special soundness and special honest verifier 
zero-knowledge and $\mathcal H$ is a random oracle.
Election scheme $\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies completeness. Further suppose, 
$\Pi$ is perfectly correct and perfectly homomorphic,
$\Sigma_1$, $\Sigma_3$ and $\Sigma_4$ satisfy special soundness and 
special honest verifier zero-knowledge, and 
$\mathsf{HeliosM}(\Pi,\allowbreak\Sigma_1,\allowbreak \Sigma_2,\allowbreak \Sigma_3,\allowbreak \Sigma_4,\allowbreak \mathcal H)$ satisfies injectivity.
The election scheme satisfies soundness.
\end{theorem}

\noindent
Theorem~\ref{thm:heliosM} requires perfect correctness,
rather than computational correctness,\footnote{%
  Properties such as correctness are typically required to hold with 
  overwhelming probability. A property is perfect if the probability 
  is $1$.}
because soundness quantifies over public keys constructed by an adversary
and such an adversary might not construct the public key using coins chosen uniformly
at random. (We can, nonetheless, verify whether public keys are constructed 
using the correct algorithm.) Thus, perfect correctness is required, because
it quantifies over all coins. Moreover, perfect homomorphisms are similarly 
required.

%By Corollary~\ref{cor:heliosM} \& Theorem~\ref{thm:heliosM}, individual and
%universal verifiability are satisfied. Thereby supporting our claim that
%the expense of individual-verifiability proofs can be eliminated and
%proofs of universal verifiability are simplified.

These findings were reported to the Zeus developers,
who conducted an investigation of their code and 
confirmed Zeus does not satisfy soundness.\iflong\footnote{Email communication, Oct \& Dec 2017.}\fi\
They promptly adopted and deployed the proposed fix,\footnote{%
  See commitments \texttt{d2653d4} (9 Oct 2017), \texttt{4fddcd3} (11 Oct 2017), 
  and \texttt{aab1b6f} (9 Oct 2017), accessed 20 Dec 2017.
}
this was straightforward, because they had already written code for the Fiat-Shamir 
transformation.
These findings were also reported to the developer of helios-server-mixnet,\iflong\footnote{Email communication, 22 Dec 2017.}\fi\
who confirmed soundness is not satisfied with a $(n,n)$-threshold,
but is for other thresholds because code from the PloneVote\iflong\footnote{\url{https://github.com/HRodriguez/svelib}, accessed 4 Jan 2017.}\fi\ cryptographic 
library is used rather than code from Helios,\iflong\footnote{Email communication, 25 Dec 2017.}\fi\
and has since adopted and deployed the proposed fix.\footnote{See commitment 
\texttt{9af7674} (25 Dec 2017).}

Beyond verifiability, Smyth has shown that $\mathsf{HeliosM}$ produces election 
schemes that satisfy ballot secrecy~\cite{Smyth17:ballotSecrecy}.





%\input{related}
```

# Conclusion

We have introduced a construction that serves as a foundation for verifiable voting systems, and we have shown that it produces systems satisfying individual verifiability and the injectivity aspect of universal verifiability, when instantiated with El Gamal. Moreover, we have analysed verifiability of two implementations of Helios Mixnet and shown that the soundness aspect of universal verifiability is not satisfied, due to vulnerabilities in Helios. Finally, we propose a fix and exploit our construction to prove that the fix suffices for individual and universal verifiability.

#### Acknowledgements.

I am grateful to Steve Kremer and the anonymous reviewers for useful feedback that helped improve this paper. I am also grateful to Yingtong Li (developer of helios-server-mixnet) and to Georgios Tsoukalas & Panos Louridas (developers of Zeus) for discussions about their voting systems.