# Ballot secrecy: Security definition, sufficient conditions, and analysis of Helios
, Ben Smyth
2026-09-05
## Abstract
Let’s formalise ballot secrecy as a game between a benign challenger, malicious adversary, and voting system, the adversary tasked to break security, make distinction between observed world and some parallel one, only the challenger knowing which world is under observation: Our formalisation improves earlier work to ensure detection of attacks when ballot collection is adversary controlled. We also formalise ballot independence (from asymmetric encryption’s security game), and prove independence suffices for secrecy in voting systems with zero-knowledge tallying proofs. Using that proof simplification, we present blueprints for construction of non-malleable encryption based voting systems with certified ballot secrecy. Additionally, we analyse the Helios voting system and its mixnet variant, finding secrecy isn’t satisfied by Helios, earlier techniques missing the attack because tallying algorithm inputs are assumed uncompromised, implicitly requiring all ballot processing be trusted, which we like to avoid, rather than assuming risk. Our blueprint guides construction of a variant proven to ensure secrecy.
# 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. (Cf. the United Nations, the Organisation for Security & Cooperation in Europe, and the Organization of American States (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**).) Historically, “Americans \[voted\] with their voices – *viva voce* – or with their hands or with their feet. Yea or nay. Raise your hand. All in favor of Jones, stand on this side of the town common; if you support Smith, line up over there” (**Lepore08?**). Physical actions ensured only voters voted and did so with equal influence; elections being tallable by anyone counting votes. (At most one each, ignore non-voters.) Yet, voting systems must also ensure choices are freely made (cf. aforementioned organisations (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**)), Mill arguing there’s no public freedom: “The unfortunate voter is in the power of some opulent man; the opulent man informs him how he must vote. Conscience, virtue, moral obligation, religion, all cry to him, that he ought to consult his own judgement, and faithfully follow its dictates. The consequences of pleasing, or offending the opulent man, stare him in the face...the moral obligation is disregarded, a faithless, a prostitute, a pernicious vote is given” (**Mill1830?**).
The need for free-choice started a movement towards voting as a private act, “when numerous social constraints in which citizens are routinely and universally enmeshed – community of religious allegiances, the patronage of big men, employers or notables, parties, ‘political machines’ – are kept at bay,” and “this idea has become the current *doxa* of democracy-builders worldwide” (**Bertrand07:Opening:HiddenHistorySecrectBallot?**). The most widely used embodiment of this idea is the Australian system, demanding votes be marked on uniform ballots in polling booths and deposited into ballot boxes. Uniformity enabling free-choice during distribution, collection and tallying of ballots,[^1] and the isolation of polling booths facilitating free-choice whilst marking. The Australian system assures only voters vote and do so with equal influence. Observers check ballots are only distributed to voters, and at most one ballot is deposited by each voter, spoiled ballots discarded, votes expressed in remaining ballots tally to the election outcome. Assurance is limited by an observer’s ability to monitor (**Bjornlund04:ElectionMonitoring?**; **Kelley12:ElectionMonitoring?**; **Norris15:ElectionMonitoring?**) and the ability to transfer that assurance is limited to the observer’s “good word or sworn testimony” (**Neff03?**).
Since the paper-based Australian system’s introduction, electronic voting systems have emerged. Unfortunately, these electronic systems are routinely broken in ways that violate free-choice, e.g., (**Wallach04:Diebold?**; **Rop07:NetherlandsVoting?**; **DebraBowenCalifornia07?**; **Halderman10:IndiaVoting?**; **Halderman12:DCVoting?**; **Halderman14:EstoniaVoting?**), or permit undue influence, e.g., (**Wallach04:Diebold?**; **ElectoralCommision07?**; **DebraBowenCalifornia07?**; **GermanyCourt09?**; **JonesSimons12:VotingBook?**). Breaks can be avoided by proving systems satisfy formalisations of voters voting freely and of detecting undue influence. Universal verifiability formalises the latter. Herein, we formalise the former, capturing ballot secrecy as a notion of free-choice assuming voters’ construct ballots as prescribed and keyholders don’t abuse their privilege. (Keyholders can tally individual ballots, secrecy requires some trust.)
- Ballot secrecy. A voter’s vote is not revealed to anyone.
We’ll work in the computational model of cryptography, formalise a game between a benign challenger, a malicious adversary and a voting system, engaging in a series of interactions, tasking the adversary to break security, make a distinction between observed world and some parallel one, only the challenger knowing which world is under observation. Our game proceeds as follows.
1. Adversary picks vote pair $v_0$ and $v_1$.
2. Challenger constructs ballot for vote $v_\beta$, using voting system prescribed algorithm $\mathsf{Vote}$, and gives that ballot to the adversary, bit $\beta$ being chosen uniformly at random.
Adversary and challenger optionally repeat for further ballots, using the same bit $\beta$.
3. Adversary constructs set of ballots $\mathfrak{bb}$ (at least one being adversary- or challenger-constructed).
Game’s adversary effectively casts ballots on behalf of some voters, and controls votes cast by others.
4. Challenger tallies, applying algorithm $\mathsf{Tally}$ to ballots $\mathfrak{bb}$, giving resulting outcome to adversary.
Adversary wins determining if $\beta = 0$ or $\beta = 1$. To avoid trivial distinctions, we require the aforementioned votes (controlled by the adversary) remain constant regardless of whether $\beta =\allowbreak 0$ or $\beta = 1$. If the adversary wins the game, then there’s an attack strategy to reveal voters’ votes, otherwise, no voter’s vote can ever be revealed to anyone, ensuring privacy. Our game improves upon games by Bernhard *et al.* (**Smyth11:HeliosProvableSecure?**; **Bernhard11:Helios?**; **2013:BallotIndependenceESORICS?**; **2014:BallotIndependenceEprint?**; **BCGPW15?**) to ensure detection of attacks when tallying algorithm inputs may be compromised.
Beyond ballot secrecy, voting systems should satisfy universal verifiability, requiring systems to produce evidence that can be checked to determine whether votes expressed in ballots correspond to the election outcome, enabling detection of undue influence. Smyth *et al.* capture universal verifiability as a game tasking the adversary to falsify evidence causing checks to succeed when they shouldn’t (for unsound systems announcing invalid outcomes, in disregard for votes expressed in collected ballots), or causing checks to fail when they shouldn’t (for incomplete systems that refuse to operate for unfavourable results) (**2022-surveying-election-verifiability?**; **Smyth15:ElectionVerifiability?**). Winning their game signifies existence of adversary strategy for spurious outcome that’ll be inadvertently accepted, or for legitimate outcome rejection. When no such adversary exists, anyone can verify election outcome legitimacy. Universal verifiability and ballot secrecy are orthogonal properties of voting systems that can be studied, formulated and analysed independently. We’ll avoid discussion of verifiability, except to introduce general concepts, to highlight features needed solely for verifiability, and to simplify proofs.
Let’s introduce two voting systems to demonstrate how ballot secrecy and universal verifiability can be achieved. The first ($\mathsf{Nonce}$) instructs each voter to cast a ballot comprising their vote paired with a nonce (that ballot being collected and stored on a bulletin board) and instructs the tallier to publish the election outcome corresponding to votes (stored on that board). The second ($\mathsf{Enc2Vote}$) instructs voters to cast asymmetric encryptions of their votes and instructs the tallier to decrypt the encrypted votes and publish the outcome corresponding to those votes. Universal verifiability is ensured by the former system, because anyone can recompute the election outcome to check it corresponds to votes expressed in collected ballots. But, ballot secrecy is not, because voters’ votes are revealed. By comparison, secrecy is ensured by the latter system, because asymmetric encryption ensures votes cannot be recovered from ballots and the tallying procedure ensures no individual votes are revealed. But universal verifiability is not ensured because spurious election outcomes need not correspond to encrypted votes. $\mathsf{Enc2Vote}$ ensures secrecy not verifiability; $\mathsf{Nonce}$ achieves the reverse. More advanced voting systems must simultaneously satisfy both secrecy and verifiability, we’ll consider Helios.
Helios is an open-source, web-based electronic voting system (**AdidaPereiraMarneffeQuisquater?**), which has been used in binding elections, including the International Association of Cryptologic Research (IACR) using Helios annually since 2010 to elect board members (**IACRHelios10b?**; **IACRHelios10?**), the Association for Computing Machinery (ACM) using Helios for their 2014 general election (**ACM14:Helios?**), the Catholic University of Louvain using Helios to elect their university president in 2009 (**AdidaPereiraMarneffeQuisquater?**), and Princeton University using Helios since 2009 to elect student governments. Helios is intended to satisfy universal verifiability whilst maintaining ballot secrecy. For ballot secrecy, each voter is instructed to encrypt their vote using an asymmetric homomorphic encryption scheme. Encrypted votes are homomorphically combined and the homomorphic combination is decrypted to reveal the outcome. Alternatively, a mixnet is applied to the encrypted votes and the mixed encrypted votes are decrypted to reveal the outcome (**Adida08?**; **Pereira11:HeliosMixnet?**). We continue to refer to the former voting system as Helios and, henceforth, refer to the latter variant as *Helios Mixnet*. For universal verifiability, the encryption step is accompanied by a non-interactive zero-knowledge proof demonstrating correct computation. This ensures homomorphic combinations of encrypted votes and mixed encrypted votes can be decrypted, making the outcome recoverable. Helios additionally requires proof that ciphertexts encrypt votes. This prevents an adversarial voter crafting a ciphertext that could be combined with others to derive an election outcome in the voter’s favour. (E.g., votes might be switched between candidates.) The decryption step is similarly accompanied by a non-interactive zero-knowledge proof to prevent spurious outcomes.
*Contribution and structure:*
- Formalisation of ballot secrecy, detecting attacks compromising tallying algorithm input.
Section [sec:secrecy] briefly explains the pitfalls of existing ballot secrecy definitions, introduces our definition, adapts formalisations of non-malleability and indistinguishability for asymmetric encryption to derive two equivalent game-based definitions of ballot independence, and proves relations between definitions, ballot independence being proven sufficient for secrecy in systems with zero-knowledge tallying proofs, and independence being necessary, but not sufficient, in general.
- Helios study, identifying attack undetectable by earlier techniques, proof fix upholds secrecy.
Section [sec:helios] applies methodology to identify known Helios vulnerability, explains why earlier techniques cannot detect that vulnerability, discusses non-malleable ballots as a fix, and uses our sufficient condition to prove secrecy .
- Proof $\mathsf{Enc2Vote}$ is blueprint for securely constructing voting systems delivering on secrecy needs.
Section [sec:nm-suffices] proves that ballot independence cannot be harmed by tallying, when all ballots are tallied correctly; shows that universally-verifiable, encryption-based voting systems.
- Helios Mixnet study, demonstrating triviality of secrecy proofs when following $\mathsf{Enc2Vote}$ blueprint.
Section [sec:heliosMixnet] presents Helios Mixnet analysis, showcasing trivialisation of ballot-secrecy proofs with universal verifiability & non-malleable encryption combo.
The remaining sections present syntax (§[sec:syntax]), discussion, limitations, and directions for further research (§[sec:discussion]), related work (§[sec:related]), and a brief conclusion (§[sec:conclusion]); Sidebar [fig:notation] introduces game-based security definitions and recalls notation; the appendices define cryptographic primitives and relevant security definitions (Appendix [sec:crypto]) and present further supplementary material. (Readers familiar with games might skip Sidebar [fig:notation], and some might study related work prior to formalisation.)
# Election scheme syntax
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 598, column 1): unexpected } expecting \end{document} } ^`
``` latex
\section{Election scheme syntax}\label{sec:syntax}
We recall syntax (Definition~\ref{def:election}) for
voting systems that consist of the following \ifev four \else three \fi steps.
First, a tallier generates a key pair.
Secondly, each voter constructs and casts a ballot for their vote.
These ballots are collected and recorded on a bulletin board.
\ifev Thirdly, \else Finally, \fi the tallier
tallies the collected ballots and
announces the outcome as a frequency distribution of votes.
The chosen representative is derived from this distribution, e.g.,
as the candidate with the most votes.%
\ifev\footnote{
Beyond first-past-the-post voting systems,
Smyth shows the syntax can model ranked-choice voting systems
too~\cite{2017-FPTP-suffices-for-ranked-voting}.}
Finally, voters and other interested parties check that
the outcome corresponds to votes expressed in collected ballots.
\else\footnote{%
Smyth, Frink \& Clarkson use the syntax to model first-past-the-post voting
systems~\cite{Smyth15:ElectionVerifiability} and
% \ifoverview
% Smyth shows that ranked-choice voting systems can be captured by representing
% rankings as candidates~\cite{2017-FPTP-suffices-for-ranked-voting}.
% \else
Smyth shows ranked-choice voting systems can be modelled too~\cite{2017-FPTP-suffices-for-ranked-voting}.
% Both works consider a single tallier and we discuss distributing the tallier's
% role in Section~\ref{sec:discussion}.
% \fi
}
\fi
\begin{definition}[Election scheme~\cite{Smyth15:ElectionVerifiability}] \label{def:election}
An \emph{election scheme} is a tuple of probabilistic polynomial-time algorithms
$(\SetupSymb,\allowbreak%\RegisterSymb,
\VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$ such that:
\ifieee
\begin{itemize}
\else
\begin{description}
\fi
\ifacm\item[$\SetupSymb$,]\else\item $\SetupSymb$, \fi denoted $(\pk,\sk,\mB,\mC) \leftarrow \Setup$,
%
is run by the tallier.
The algorithm 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$.
\ifacm\item[$\VoteSymb$,]\else\item $\VoteSymb$, \fi denoted $b\leftarrow\Vote$, is run by voters. The algorithm
takes as input a public key $\pk$, a voter's vote $v$, some number of candidates
$\nC$, and a security parameter $\kappa$. Vote $v$ should be selected from a
sequence $1,\dots,\nC$ of candidates.
The algorithm outputs a ballot $b$ or error symbol~$\perp$.
\ifacm\item[$\TallySymb$,]\else\item $\TallySymb$, \fi denoted $(\outcome, \tpf)\leftarrow\Tally$, is run by the
tallier. The algorithm takes as input a private key $\sk$, a bulletin board $\bb$,
some number of candidates $\nC$, and a security parameter $\kappa$, where $\bb$
is a set. The algorithm outputs an election outcome $\outcome$ and a non-interactive tallying
proof $\tpf$, where $\outcome$ is a vector of length $\nC$
and each index $v$ of that vector should indicate the number of votes for candidate $v$.
\ifev
Moreover, the tallying proof should demonstrate that the outcome corresponds to votes
expressed in ballots on the bulletin board.
\fi
\ifev
\item $\VerifySymb$, denoted $s \leftarrow \Verify$, is run to audit an election.
The algorithm 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$. The algorithm outputs a bit $s$, which is $1$
if the %election verifies successfully or $0$ otherwise.
outcome should be accepted and $0$ otherwise. We require the algorithm to be
deterministic.
\fi
\ifieee
\end{itemize}
\else
\end{description}
\fi
\iftutorial
\marginpar{Does the need for correctness properties need motivating?}
\fi
\noindent
Election schemes must satisfy \emph{correctness}, that is, 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:\smallskip
\LinesNotNumbered%\LinesNumberedHidden
{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup$;\\
\begingroup\removelatexerror
\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}
\endgroup
}
\end{definition}
\ifnocompress
\noindent
The syntax provides a language to model voting systems and
the correctness condition ensures that such systems 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, when ballots are constructed and tallied in the
prescribed manner.
The syntax focuses on minimalism, rather than generality: Algorithm $\SetupSymb$
naturally inputs a security parameter and outputs a key pair, along with
bounds on the number of ballots $\mB$, respectively candidates $\mC$.\footnote{%
Bounds broaden the correctness definition's scope,
e.g., when $\encToVoteSymb$ requires $\mC$ to be less than or equal to
the size of the underlying encryption scheme's message space
(ensuring decryption operates within prescribed bounds).
Helios additionally requires the same constraint on $\mB$
(ensuring decryption of homomorphic combinations within prescribed bounds).
}
Algorithm $\VoteSymb$ naturally inputs a public key, a vote, and a security
parameter, and outputs a ballot. The vote is expressed as an integer\ifnocompress, rather
than alphanumeric strings,\fi\ for brevity. Beyond those inputs, the algorithm inputs
a number of candidates $\nC$, which is necessary in voting systems such as Helios,
because ballot construction depends on the number of candidates. Tallying is similarly
dependent on the number of candidates in Helios, hence inputs and outputs to
algorithm $\TallySymb$ are similarly needed.
Finally, the syntax restricts bulletin boards to sets, rather than multisets or lists.
This is a limitation:
Sets preclude the construction of schemes vulnerable to attacks that arise due to duplicate
ballots~\cite[\S2.1 \& \S4.3]{2014-ballot-secrecy}.
Systems vulnerable to such attacks cannot be modelled using the syntax: Analysts must not
abstract away the details of lists or multisets and model them as sets, since any ensuing analysis will
miss attacks. Analysts may abstractly model lists or multisets as sets
with some additional effort.
Election schemes may also include an algorithm
$\VerSymb$\ifconf\else, which is used\fi\ to audit elections. We omit that algorithm
from Definition~\ref{def:election}, because we focus on ballot secrecy, rather than
verifiability: Ballot secrecy must be upheld independently of auditing,
since voters' votes should not be revealed regardless of whether an election outcome is
correct (i.e., regardless of whether auditing succeeds). Hence, algorithm $\VerSymb$
must not be used to achieve privacy and can be omitted.
Nonetheless, algorithm $\TallySymb$ must output the tallying proof (that
would be input to algorithm $\VerSymb$), since tallying proofs can harm privacy. (For
instance, as an extreme example, a tallying proof may include the private key, which can
used to violate every voter's privacy.)
Voting systems must ensure that outcomes only include votes cast by voters,
as opposed to non-voters, and that only one vote of each voter has
influence~\cite{Smyth16:helios-eligibility}. The former can be achieved by
authentication. Traditionally, the latter was achieved by permitting each voter
to cast at most one ballot, whereas more recent systems permit multiple ballots
and count only the last. Our syntax is compatible with voting systems, such as
Helios, that rely on trusted external authentication services to ensure that collected ballots
satisfy these properties (i.e., collected ballots were cast by voters and contain at most
one ballot per voter), hence, election schemes need not achieve these properties
directly.
(An extension of the syntax is compatible with voting systems that introduce voter
credentials and use cryptography to achieve these properties directly~\cite{Smyth15:ElectionVerifiability,Smyth18:HeliosC,2019-Athena-voting-system}.)
Here be dragons: The security of external authentication services must be verified.
We will use our syntax to express a privacy property of election schemes,
and for modelling \& analyse of voting systems, including Helios (\S\ref{sec:helios})
and Helios Mixnet (\S\ref{sec:heliosMixnet}). Beyond those
systems, syntax is compatible with Helios-C~\cite{Cortier14:verifiability}
and the system by Juels, Catalano \& Jakobsson~\cite{JCJ10} (once extended
to include voter credentials), so Belenios
and Civitas should be included as well. These schemes are rather dominant in the literature, so the class
is interesting and rather general. Notable voting systems that are excluded include:
Systems relying on features implemented with paper %, e.g., Pr\^et \`a Voter~\cite{ChaumRyanSchneider2005}, MarkPledge~\cite{Neff04:MarkPledge}, and Scantegrity II~\cite{Chaum08II};
(e.g.,~\cite{Neff04:MarkPledge,ChaumRyanSchneider2005,Chaum08II}),
systems which require partially private ballots %, e.g.,~\cite{Moran06};
(e.g.,~\cite{Moran06}),
and schemes relying on partially honest bulletin boards %, e.g., Scytl's Pnyx.core ODBP 1.0~\cite{Scytl08}.
(e.g.,~\cite{Scytl08}).
We also exclude distributed tallying. These limitations
are further discussed in Section~\ref{sec:discussion}.
\iftutorial
\marginpar{@Paul, I guess we need to explain what this all means! The following might be useful \url{http://bristolcrypto.blogspot.fr/2015/05/52-things-number-32-difference-between.html}}
\fi
\begin{comment}
We formalise the
\ifev
nonce-based and encryption-based voting systems,
\else
encryption-based voting system,
\fi
introduced in the previous section, to demonstrate the suitability
of our syntax.
\end{comment}
\begin{comment}
We demonstrate the suitability of our syntax with two examples.
The first 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.\footnote{The example was originally
presented by Bernhard \emph{et al.}~\cite{2014:BallotIndependenceEprint,2013:BallotIndependenceESORICS,Bernhard11:Helios,Smyth11:HeliosProvableSecure}
in a slightly different setting.}
The second instructs each voter to
pair their vote with a nonce and instructs the tallier to
publish the number of votes for each candidate. Ballot secrecy
is satisfied by the former scheme, because asymmetric encryption
can ensure that votes cannot be recovered from ballots and the
tallying procedure ensures that votes are not revealed from
the election outcome.\footnote{Voters' votes are revealed during
the tallying procedure. Such revelations might be
tolerated if computations cannot be observed.
Otherwise, a more advanced tallying procedure is required.}
But, verifiability is not ensured. Indeed,
a spuriously announced outcome need not even correspond to the
encrypted votes. By comparison,
verifiability is ensured by the latter scheme, because
voter's can use their nonce to check that their ballot is recorded
(individual verifiability) and anyone can recompute the election outcome
to check that it corresponds to votes expressed in recorded ballots
(universal verifiability). But, ballot secrecy is not ensured, because all
votes are revealed.
\end{comment}
\iftutorial
\textcolor{red}{TO DO: Decide where to place case studies}
\begin{definition}[$\Nonce$~\cite{Smyth15:ElectionVerifiability}]\label{def:nonce}
We define $\Nonce$ as follows:
\begin{itemize}
\item $\Setup$ outputs $({\perp},{\perp},p_1(k),p_2(k))$, where $p_1$ and $p_2$ may be any polynomial functions.
\item $\Vote$ selects a nonce $r$ uniformly at random from $\mathbb Z_{2^k}$
and outputs $(r,\beta)$.
\item $\Tally$ computes a vector $\outcome$ of length $n_C$, such that
$\outcome$ contains the distribution of votes on $\bb$
for which the corresponding nonce is in $\mathbb Z_{2^k}$,
and outputs $(\outcome,\perp)$.
\item $\Verify$ outputs $1$ if $(\outcome,\tpf) =\Tally$, and
$0$ otherwise.
\end{itemize}
\end{definition}
\begin{lemma}\label{lemma:Nonce:correctness}
We have $\Nonce$ is an election scheme.
\end{lemma}
\noindent
Smyth, Frink \& Clarkson present a proof of Lemma~\ref{lemma:Nonce:correctness}~\cite{Smyth15:ElectionVerifiability}.
\marginpar{TO DO: Add proof of Lemma~\ref{lemma:Nonce:correctness} to~\cite{Smyth15:ElectionVerifiability}.}
\fi
%\subsection{Related work}
%\textcolor{blue}{Perhaps mention there are lots and just summarise my own and some
% of my co-authors.}
\ifev
```
# Verifiability
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 573, column 17): expecting \end{document} \end{definition} ^`
``` latex
\section{Verifiability}\label{sec:verifiability}
The Australian system is reliant on monitoring to ensure election outcomes
correspond to votes expressed in collected ballots, moreover, depositing
ballots into ballot boxes suffices to ensure they %\sout{are amongst those}
collected.
By comparison, election schemes compute outcomes in a manner that should not
be monitored. Indeed, such monitoring would reveal the tallier's private key,
which would compromise ballot secrecy. Furthermore, casting a ballot is insufficient
to ensure it is collected, because an adversary may discard or modify ballots.
Nevertheless, election schemes produce tallying proofs to provide
evidence that outcomes are correctly computed and voters can check whether
their ballot is collected. The former notion is formalised by universal
verifiability and the latter by individual verifiability.
\iftutorial\marginpar{Perhaps switch ordering of \emph{individual verifiability} and
\emph{universal verifiability}, since the former game is easier to understand.}\fi
\subsection{Universal verifiability}\label{sec:verifiability:uv}
Universal verifiability asserts that anyone must be able to check whether
an election outcome %\sout{produced by a voting system}
corresponds to %\sout{the}
votes expressed in collected ballots. Since checks can be performed by
algorithm $\VerifySymb$, it suffices that $\VerifySymb$ accept if and only if
the outcome corresponds to votes expressed in collected ballots.
The \emph{only if} requirement is captured by soundness, which requires
algorithm $\VerifySymb$ to only accept correct outcomes, and the \emph{if}
requirement is captured by completeness, which requires election outcomes
produced by algorithm $\TallySymb$ to be accepted by algorithm $\VerifySymb$.
\paragraph{Soundness.}
%\sout{The notion of a correct outcome is}
Correct outcomes are
formalised using function $\correcttally$.
That function uses a predicate $(\exists^{=\ell} x : P(x))$ that holds exactly
when there are $\ell$ distinct values of $x$ for which $P(x)$ is
satisfied~\cite{Schweikardt05}. (Variable $x$ is bound by the predicate and
integer $\ell$ is free.) Using the predicate, function $\correcttally$ is
defined such that
%
\begin{multline*}
\correcttally(\pk,\nC,\bb,\kk)[v] = \ell
\textrm{ iff } \\
\exists^{=\ell} b\in \bb \setminus \{\bot\} :
\exists r : b=\Vote[\pk,\allowbreak v,\allowbreak\nC,\allowbreak\kk;\allowbreak r],
\end{multline*}
%
where $\correcttally(\pk,\nC,\bb,\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 for vote $v$ on the bulletin
board. The function requires that ballots be interpreted for only one candidate,
which can be ensured by injectivity.
\begin{definition}[$\Injectivity$~\cite{Smyth15:ElectionVerifiability,Smyth18:HeliosMixnetVerifiability}]
An election scheme $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies $\Injectivity$,
\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}
\noindent
Our definition of injectivity ensures that a ballot for vote $v$ can never
be interpreted for a distinct vote $v'$, hence, votes expressed in
ballots correspond to unique outcomes.
Equipped with a notion of correct outcomes, we formalise soundness (Definition~\ref{def:UVSoundness})
as a game that tasks the adversary to compute inputs to algorithm $\VerifySymb$ (Line~\ref{alg:SoundnessGame:adv}),
including an election outcome and some ballots, that cause %successfully verification
the algorithm to accept when the outcome does not correspond to the votes expressed in
those ballots (Line~\ref{alg:SoundnessGame:ret}).
\begin{definition}[$\Soundness$~\cite{Smyth15:ElectionVerifiability}]\label{def:UVSoundness}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$
be an election scheme, $\adv$ be an adversary, $\kk$ be a security parameter, and
$\SoundnessGame$ be the following game.
{\upshape
\begin{inlineexperiment}{$\SoundnessGame$}
$(\pk,\bb,\nC,\outcome,\tpf) \leftarrow \adv(\kk)$\label{alg:SoundnessGame:adv}\;
\Return~$\VerSymb(\pk,\bb,\nC, \outcome,\tpf,\kk) = 1 \mathrel\wedge \outcome \not= \correcttally(\pk,\nC,\bb, \kk)$\label{alg:SoundnessGame:ret}\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies $\Soundness$, if $\Gamma$ satisfies injectivity and
for all probabilistic polynomial-time adversaries $\adv$, there exists a
negligible function $\negl$, such that for all security parameters $\kk$,
we have $\Succ(\SoundnessGame) \leq \neglK$.
\end{definition}
\noindent
An election scheme satisfies $\Soundness$ when algorithm $\VerifySymb$ only
accepts outcomes that correspond to votes expressed in collected ballots.
\begin{tcolorbox}
\begin{guideline}
Verification must only accept outcomes that correspond to votes expressed in
collected ballots.
\end{guideline}
\end{tcolorbox}
\paragraph{Completeness.} We formalise completeness (Definition~\ref{def:UVComplete})
as a game that tasks the adversary to compute a bulletin board and some number of candidates
(Line~\ref{alg:CompletenessGame:adv}) such that the corresponding election outcome computed
by algorithm $\TallySymb$ (Line~\ref{alg:CompletenessGame:tally}) is rejected by algorithm
$\VerifySymb$ (Line~\ref{alg:CompletenessGame:ret}), when the key pair is computed by
algorithm $\SetupSymb$ (Line~\ref{alg:CompletenessGame:setup}).
\begin{definition}[$\Completeness$~\cite{Smyth15:ElectionVerifiability}]\label{def:UVComplete}
\begin{sloppypar}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$
be an election scheme, $\adv$ be an adversary, $\kk$ be a security parameter, and
$\CompletenessGame$ be the following game.
\end{sloppypar}
{\upshape
\begin{inlineexperiment}{$\CompletenessGame$}
$(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC) \leftarrow\allowbreak \Setup$\label{alg:CompletenessGame:setup}\;
$(\bb,\nC)\leftarrow\adv(\pk,\kk)$\label{alg:CompletenessGame:adv}\;
$(\outcome,\allowbreak\tpf) \leftarrow\allowbreak \Tally$\label{alg:CompletenessGame:tally}\;
\Return $\VerSymb(\pk,\allowbreak\bb,\allowbreak\nC,\allowbreak\outcome,\allowbreak\tpf,\allowbreak\kk) \not=\allowbreak 1 \wedge |\bb| \leq \mB \wedge\allowbreak \nC\leq \mC\allowbreak$\label{alg:CompletenessGame:ret}\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies $\Completeness$, if for all probabilistic polynomial-time
adversaries $\adv$, there exists a negligible function $\negl$, such that
for all security parameters $\kk$, we have
$
\Succ(\CompletenessGame) \leq \neglK
$.
\end{definition}
\noindent
An election scheme satisfies $\Completeness$ when algorithm $\VerifySymb$ accepts
outcomes computed by algorithm $\TallySymb$, for key pairs computed by algorithm $\SetupSymb$.
It follows that completeness implies an aspect of accountability. Indeed, if verification fails, then
the tallier is responsible for that failure, in particular, they must have incorrectly computed
their key pair or the election outcome.
\begin{tcolorbox}
\begin{guideline}
Tallying must produce outcomes that will be accepted during verification.
\end{guideline}
\end{tcolorbox}
\noindent
We formalise universal verifiability by combining the above notions.
\begin{definition}[$\UV$~\cite{Smyth15:ElectionVerifiability,Smyth18:HeliosMixnetVerifiability}]\label{def:UV}
An election scheme $\Gamma$ satisfies $\UV$, if
$\Soundness$ and $\Completeness$ are satisfied.
\end{definition}
\subsection{Individual verifiability}\label{sec:verifiability:iv}
Individual verifiability asserts that voters must be able to check whether
their ballot is amongst those collected. %Since ballots should be recorded-as-cast
%(i.e., cast ballots should be collected and recorded as they are cast), it
%suffices for voters to
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 %, but not sufficient,
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.
We formalise individual verifiability (Definition~\ref{def:iv}) as a game that
tasks the adversary to compute inputs to algorithm $\VoteSymb$ (Line~\ref{alg:IVGame:adv})
that cause the algorithm to output ballots (Lines~\ref{alg:IVGame:ballot} \&~\ref{alg:IVGame:ballotB})
that collide (Line~\ref{alg:IVGame:ret}).
\begin{definition}[Individual verifiability~\cite{Smyth15:ElectionVerifiability}]\label{def:iv}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme, $\adv$ be an adversary, $\kk$ be a security parameter, and $\IVGame$ be the following game.
{\upshape
\begin{inlineexperiment}{$\IVGame$}
$(\pk, \nC,v,v') \leftarrow \adv(\kk)$\label{alg:IVGame:adv}\;
$b\leftarrow\Vote[\pk,\nC,v,\kk]$\label{alg:IVGame:ballot}\;
$b'\leftarrow\Vote[\pk,\nC,v',\kk]$\label{alg:IVGame:ballotB}\;
\Return $b = b' \wedge b \not= {\perp} \wedge b' \not= {\perp}$\label{alg:IVGame:ret}\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies $\IV$, if for all probabilistic polynomial-time
adversaries $\adv$, there exists a negligible function $\negl$, such that
for all security parameters $\kk$, we have $\Succ(\IVGame)\leq \neglK$.
\end{definition}
\noindent
An election scheme satisfies $\IV$ when algorithm $\VoteSymb$ generates
uniquely identifiable ballots, i.e., ballots that do not collide.\footnote{%
Correctness, individual verifiability and injectivity all require that
ballots do not collide, albeit under different assumptions. Indeed,
correctness requires that ballots do not collide, with overwhelming
probability, for public keys computed by algorithm $\SetupSymb$;
$\Injectivity$ requires that ballots for distinct votes never collide;
and $\IV$ requires that ballots do not collide with overwhelming
probability. Hence, $\IV$ implies that ballots do not collide in the
context of correctness. But, $\IV$ and $\Injectivity$ are orthogonal,
in particular, $\IV$ permits collisions with negligible probability
and $\Injectivity$ permits collisions between ballots for the same vote.}
\begin{tcolorbox}
\begin{guideline}
Ballots must be distinct.
\end{guideline}
\end{tcolorbox}
\subsection{Example}\label{sec:verifiability:example}
We model our $\Nonce$ voting system (\S\ref{sec:intro}) as the following election
scheme.
\begin{definition}[$\Nonce$~\cite{Smyth15:ElectionVerifiability}]\label{def:nonce}
$\Nonce$ is defined as follows:
\begin{itemize}
\item $\Setup$ outputs $({\perp},{\perp},p_1(k),p_2(k))$, where $p_1$ and $p_2$ are some polynomial functions.
\item $\Vote$ samples nonce $r\leftarrow_R\mathbb Z_{2^\kk}$ and outputs $(r,v)$.
\item $\Tally$ computes a vector $\outcome$ of length $\nC$, such that
$\outcome$ is the tally of each vote in set $\bb$ which is paired with
a nonce from $\mathbb Z_{2^\kk}$, and outputs $(\outcome,\perp)$.
\item $\Verify$ outputs $1$ if $(\outcome,\tpf) =\Tally[{\perp},\bb,\nC,\kk]$ and
$0$ otherwise.
\end{itemize}
\end{definition}
\begin{lemma}
$\Nonce$ is an election scheme.
\end{lemma}
\noindent
To prove our lemma, we show that $\Nonce$ satisfies the correctness
property of Definition~\ref{def:election}.
\iftutorial
\textcolor{blue}{Is it worth explaining that $\Nonce$ cannot be
called an election scheme without this proof?}
\fi
\begin{proof}
Let $\Nonce = (\SetupSymb,\allowbreak \VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$.
Moreover, let $\kappa$ be a security parameter, $\nB$ and $\nC$ be integers,
$v_1,\dots,v_{\nB}\in\{1,\dots,\nC\}$ be votes, and $\outcome$ be a
zero-filled vector of length $\nC$. Suppose $(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC)$
is an output of $\Setup$ such that $\nB \leq \mB \wedge \nC\leq \mC$.
Further suppose we compute
{\DontPrintSemicolon\llFor{$1 \leq i \leq \nB$}{%
$b_i \leftarrow \Vote[\pk,v_i,\nC,\kk];
\outcome[v_i] \leftarrow \outcome[v_i] + 1$%
}}.
Moreover, suppose $(\outcome',\tpf)$ is an output of
$\Tally[\sk,\{b_1,\dots,b_{\nB}\},\nC, \kk]$.
To prove correctness, it suffices to prove $\outcome = \outcome'$,
with overwhelming probability.
We have that $\outcome$ is the election outcome corresponding
to votes $v_1,\dots,v_{\nB}$. Moreover, by definition of
algorithms $\VoteSymb$ and $\TallySymb$, we have
$\outcome'$ is the tally of the votes in set
$\{(r_1,v_1),\dots,(r_{\nB},v_{\nB})\}$, where
$r_1,\dots,r_{\nB}$ are nonces chosen uniformly at random
from $\mathbb Z_{2^\kk}$.
Hence, $\outcome'$ is the election outcome corresponding
to votes $v_1,\dots,v_{\nB}$, i.e., $\outcome = \outcome'$,
assuming nonces $r_1,\dots,r_{\nB}$ are pairwise distinct, which
holds with overwhelming probability, thereby concluding
our proof.
\end{proof}
\noindent
Intuitively, election scheme $\Nonce$ satisfies $\IV$, because nonces collide with negligible
probability, hence, ballots collide with negligible probability too, which
suffices for $\IV$. Moreover, $\UV$ is satisfied too, because outcomes correspond
to votes expressed in collected ballots ($\Soundness$) and such
outcomes are accepted ($\Completeness$).
\begin{proposition}
$\Nonce$ satisfies $\IV$ and $\UV$.
\end{proposition}
\begin{proof}
\begin{sloppypar}
Let $\Nonce = (\SetupSymb,\allowbreak \VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$. We proceed by proving that $\IV$, $\Injectivity$ (which is a prerequisite
for $\Soundness$), $\Soundness$, and $\Completeness$ are satisfied.
\end{sloppypar}
For individual verifiability, suppose an adversary outputs
public key $\pk$, some number of candidates $\nC$, and votes
$v$ and $v'$. Further suppose $b$ is an output of $\Vote[\pk,\nC,v,\kk]$
and $b'$ is an output of $\Vote[\pk,\nC,v',\kk]$, for some security
parameter $\kk$. By definition of algorithm $\VoteSymb$, we have
$b = (r,v)$ and $b'=(r',v')$, where $r$ and $r'$ are nonces
chosen uniformly at random from $\mathbb Z_{2^\kk}$. Hence,
$r$ and $r'$ are distinct with overwhelming probability, thus,
$b \not= b'$ with overwhelming probability, as required.
Our proof of injectivity is similar to our proof of individual
verifiability, except we require $v \not= v'$, which ensures
$b\not=b'$.
For soundness, let $\adv$ be an adversary and $\kk$ be a security parameter.
Suppose $(\pk,\bb,\nC,\outcome,\tpf)$ is an output of $\adv(\kk)$ such that
$\VerSymb(\pk,\bb,\nC, \outcome,\tpf,\kk) = 1$. By definition of algorithm
$\VerSymb$, we have $(\outcome,\tpf) =\Tally[{\perp},\bb,\nC,\kk]$ and,
by definition of algorithm $\TallySymb$, we have $\outcome$ is a vector
of length $\nC$ such that $\outcome$ is the tally of each vote in set
$\bb$ which is paired with a nonce from $\mathbb Z_{2^\kk}$. Hence,
for each $v\in\{1,\dots,\nC\}$ we have
%
\begin{align*}
\outcome[v] = \ell
&\Leftrightarrow \exists^{=\ell} b\in \bb : \exists r \in \mathbb Z_{2^\kk} : b= (v,r)
%
\intertext{and, by definition of algorithm $\VoteSymb$ and since $\perp$ is not a pair, we have}
&\Leftrightarrow \exists^{=\ell} b\in \bb \setminus \{\bot\} :
\exists r : b=\Vote[\pk,\allowbreak v,\allowbreak\nC,\allowbreak\kk;\allowbreak r]
\end{align*}
%
Thus, $\outcome = \correcttally(\pk,\nC,\bb,\kk)$, as required.
For completeness, let $\adv$ be an adversary and $\kk$ be a security parameter.
Suppose $(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC)$ is an output
of $\Setup$, $(\bb,\nC)$ is an output of $\adv(\pk,\kk)$, and
$(\outcome,\allowbreak\tpf)$ is an output of $\Tally$. By definition of
algorithm $\SetupSymb$, we have $\pk = {\perp}$, hence,
$(\outcome,\tpf) =\Tally[{\perp},\bb,\nC,\kk]$. It follows by the
definition of algorithm $\VerifySymb$ that
$\VerSymb(\pk,\allowbreak\bb,\allowbreak\nC,\allowbreak\outcome,\allowbreak\tpf,\allowbreak\kk) =\allowbreak 1$, as required.
\end{proof}
\subsection{Related definitions of verifiability}
\label{sec:relatedVerif}
\label{sec:verifiability:related}
Discussion of verifiability originates from Cohen \& Fischer \cite{Benaloh85}
and is advanced by Fujioka, Okamoto \& Ohta~\cite{FOO},
Benaloh \& Tuinstra~\cite{Benaloh94} and Sako \& Kilian~\cite{Sako95}.
More recently, definitions of universal verifiability 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 vulnerabilities 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 vulnerabilities.
By comparison, the definition of universal verifiability that we consider
(Definition~\ref{def:UV}) detects these vulnerabilities and appears to be
the strongest definition in the literature.
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 \emph{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 prove that their notion of verifiability is strictly
stronger than global verifiability with that goal. Nonetheless, the ``gap'' is due
to an uninteresting technical detail and those definitions %of verifiability
might coincide if the gap is filled.
Beyond the computational model of security,
Smyth \emph{et al.}~\cite{Smyth10:ElectionVerifiabilityA} formulate a definition of
verifiability in the applied pi calculus. The definition is amenable
to automated reasoning, but it is stronger than necessary and cannot be satisfied
by many election schemes, including Helios.
Kremer \emph{et al.}~\cite{Smyth10:ElectionVerifiability} overcome this limitation
with a weaker definition that sacrifices amenability to automated reasoning, and
Smyth~\cite[\S3]{Smyth10:thesis} extends this definition.
\subsection{Further notions of verifiability}
\label{sec:verifiability:outlook}
Individual verifiability formalises a notion of uniquely identifiable ballots,
assuming ballots are constructed in the prescribed manner. We have seen that voting
system $\Nonce$ satisfies this notion, but individual verifiability does not
ensure ballots are unique when voters deviate from the prescribed voting procedure.
Indeed, a ballot's nonce serves as its unique identifier in $\Nonce$ and substituting
that
nonce for some other value may compromise individual verifiability. Further notions
of verifiability, such as cast-as-intended~\cite{AdidaN06}, are needed when deviations
from the voting procedure are possible, e.g., when the voting procedure is subverted
by an adversary.
The soundness aspect of universal verifiability formalises a notion of only accepting
election outcomes that correspond to votes expressed in collected ballots.
%We have seen that voting system $\Nonce$ satisfies this notion, but our soundness
Our definition
does not ensure outcomes include only voters' votes and at most one
vote each. Indeed, an adversary that controls ballot collection can ``stuff''
the bulletin board with ballots and the corresponding votes will be included in the
election outcome. Some voting systems rely on a trusted third party to authenticate
ballots and only tally %collected
ballots that have been authenticated. E.g., Helios supports authentication via
Facebook, Google and Twitter using OAuth.\footnote{%
Meyer \& Smyth describe the application of OAuth in
Helios~\cite{Smyth16:helios-eligibility}.}
Other voting systems use cryptography to ensure that only voters can construct
authorised ballots. E.g., the voting system by Juels, Catalano \& Jakobsson uses
a combination of encrypted nonces and plaintext equality tests for
authentication~\cite{JCJ10}. Albeit such systems seem to require expensive
infrastructures for voter credentials and are reliant on a trusted third party
to certify credentials.
Our soundness definition is suitable for analysing
the former class of voting systems, and Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}
formulate an alternative soundness definition to analyse the latter class.
(Quaglia \& Smyth~\cite{Smyth18:HeliosC} define a transformation from schemes satisfying our
soundness definition to schemes satisfying the alternative soundness
definition.)
Ultimately, we would prefer not to trust any third party, but that does not
seem possible in a scalable manner.
\fi
```
# \ifev{
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 751, column 1): unexpected } expecting \end{document} \Return $g = \beta \wedge\allowbreak \balanced(\bb,\nC,L) ^`
``` latex
\section{\ifev{}Ballot secrecy\else{}Privacy\fi}\label{sec:privacy}\label{sec:secrecy}
\begin{comment}
Our informal definition of ballot secrecy could be
formulated as a game similar to indistinguishability
games for asymmetric encryption: We could challenge
the adversary to determine whether a ballot is for one of two possible votes.
This formalisation is too weak. Election schemes also output
an outcome and a tallying proof, and such information
can be exploited to reveal voters' votes. Hence, to detect such exploits,
it is necessary to provide some tallying capability.
Albeit, it becomes trivial to win games that tally a single
challenge ballot.
\end{comment}
\ifev
The Australian system is reliant on uniform ballots to ensure voters'
votes are not revealed. Indeed, uniformity ensures ballots are
indistinguishable during distribution and the isolation of polling
booths ensures votes are not revealed whilst marking. Moreover, folded
ballots are indistinguishable during collection and indistinguishability
of markings can ensure votes are not revealed whilst tallying. Hence,
the Australian system derives ballot secrecy from physical characteristics
of the world. By comparison, election schemes cannot rely on such physical
characteristics,\footnote{%
Some electronic voting systems are reliant on physical characteristics
of the world. For instance, MarkPledge~\cite{Neff04:MarkPledge},
Pret \`{a} Voter~\cite{ChaumRyanSchneider2005},
Remotegrity~\cite{Zagorski13},
Scantegrity II~\cite{Chaum08II} and
Three Ballot~\cite{Rivest07:ThreeBallot} %Rivest06:ThreeBallot,
are reliant on features implemented with paper,
such as scratch-off surfaces and detachable columns.
But these systems fall outside the scope of our election scheme
syntax.
}
they must rely on cryptography to ensures voters' votes are not revealed.
\fi
Some scenarios inevitably reveal voters'
votes: Unanimous outcomes reveal how everyone voted. More generally,
outcomes can be coupled with partial knowledge %on the distribution
of voters' votes to deduce voters' votes.
For example, suppose Alice, Bob and
Mallory participate in a referendum and the outcome has frequency two for `yes' and
one for `no.' Mallory and Alice can deduce Bob's vote by pooling knowledge of their
own votes. Similarly, Mallory and Bob can deduce Alice's vote. Furthermore, Mallory
can deduce Alice and Bob both voted yes, if she voted no. For simplicity,
our informal definition of ballot secrecy (\S\ref{sec:intro}) deliberately omitted
side-conditions which exclude these inevitable revelations
and which are necessary for satisfiability.\ifev\else\ifnocompress\footnote{%
Voting systems that announce chosen representatives
(e.g.,~\cite{Benaloh86\ifnocompress,Hevia02\fi,Hevia04,Desmedt05}),
rather than frequency distributions of votes, could offer stronger
notions of privacy.}\fi\fi\
We now refine that definition as follows:
\newcommand{\BallotSecrecyDef}[1][A]{%
#1 voter's vote is not revealed to anyone, except when \ifnocompress the vote \else it \fi can be deduced from the election outcome and any partial knowledge %on the distribution of votes.
of voters' votes%
}
\newcommand{\ballotSecrecyDef}{\BallotSecrecyDef[a]}
\begin{quote}
\BallotSecrecyDef.
\end{quote}
\noindent
This refinement ensures the aforementioned examples are not violations of
ballot secrecy. By comparison, if Mallory votes yes and she can deduce the vote of
Alice, without knowledge of Bob's vote, then ballot secrecy is violated.
%Our refined ballot secrecy definition cannot be formulated as a game similar to
%indistinguishability games for asymmetric encryption, whereby the adversary is challenged
%to determine between an instance of the asymmetric encryption (and similarly voting system)
%which encrypts one message (similarly, vote) and another instance with a different message
%(similarly, different vote), because the adversary can trivially win such a game by
%tallying just Alice's ballot.
\ifev
\else
\begin{comment}
We could formulate ballot secrecy as a game that proceeds as follows. First,
the adversary picks a pair of votes $v_0$ and $v_1$. Secondly, the challenger
selects a bit $\beta$ uniformly at random and constructs a ballot for vote
$v_\beta$.
Thirdly, the adversary constructs some ballots. Finally, the challenger tallies
all the ballots and the adversary is tasked with determining bit $\beta$ without
causing an inevitable revelation (i.e., the adversary looses when votes can
be deduced from the election outcome and any partial knowledge on the distribution
of votes). This formalisation is still too weak. The ballot constructed by the challenger
is tallied, hence, the outcome includes vote $v_\beta$, from which bit $\beta$ can
inevitable be determined. Thus, no adversary can win the game winning is precluded.
We can derive a satisfiable game with a simple modification: the challenger constructs
ballots for vote $v_\beta$ and for $v_{1-\beta}$.
\end{comment}
We could formulate ballot secrecy as the following game: First,
the adversary picks a pair of votes $v_0$ and $v_1$. Secondly, the challenger
constructs a ballot $b_1$ for vote $v_\beta$ and a second ballot $b_2$ for
$v_{1-\beta}$, where $\beta$ is a bit chosen uniformly at random. Those
ballots are given to the adversary. Thirdly, the adversary constructs ballots
$b_3,\dots,b_n$. Fourthly, the challenger tallies all the ballots
(i.e., $b_1,\dots,b_n$) to the determine the election outcome, which the adversary
is given. Finally, the adversary is tasked with determining bit $\beta$.
\begin{comment}
Rather than challenging the adversary to determine
whether a ballot is for one of two possible votes,
\end{comment}
This
game challenges the adversary to determine if the first ballot is for $v_0$ and
the second is for $v_1$, or vice-versa. Intuitively, a losing adversary cannot
distinguish ballots; seemingly suggesting that Alice voting `yes' is indistinguishable
from Bob voting `no.'
The first release of Helios is not secure with respect to the aforementioned game,
due to a vulnerability identified by Cortier \& Smyth~\cite{Smyth12:Helios,Smyth11:Helios}.
Indeed, an adversary can observe a ballot constructed by the challenger, compute a
meaningfully related ballot (from a malleable Helios ballot), and exploit the relation
to win the game. This vulnerability can be
attributed to tallying meaningfully related ballots; omitting such ballots from
tallying, \emph{ballot weeding} is postulated defence%
\ifnocompress
~\cite{Smyth11:Helios,Smyth11:ReplayAttacks,Smyth12:HeliosFurtherReplays,Smyth12:Helios,2013:BallotIndependenceESORICS,BCGPW15,BCGPW15:eprint}.
\else
~\cite{Smyth11:Helios,Smyth12:Helios,2013:BallotIndependenceESORICS,BCGPW15,BCGPW15:eprint}.
\fi
%
%Indeed, Helios has been patched to use a ballot wedding mechanism,
%and can be proven secure with respect to our game.
%
%%TRUTHIFY: Helios has not been patched, albeit,
%
%\textcolor{red}{Indeed, the IACR are using a variant of Helios with a ballot weeding mechanism,
%that variant \sout{can be proven}\textcolor{magenta}{appears to be} secure with respect to our game.}
%
%%But let's stick to the general case.
%
Variants of Helios with ballot weeding \ifanon (\S\ref{sec:helios:ballotWeeding}) \fi seem
secure with respect to this game.
%
Unfortunately, ballot weeding mechanisms can be subverted by intercepting ballots
or by re-ordering ballots.
\begin{comment}
For instance,
\ifev
we will see that re-ordering ballots subverts
\else
Smyth, Frink \& Clarkson show how re-ordering ballots can subvert
\fi
weeding mechanisms in a manner that violates
universal verifiability~\ifev(\S\ref{}) \else\cite{Smyth15:ElectionVerifiability}, \fi
and \ifev\else we will see \fi that ballot secrecy can be violated too
(\S\ref{sec:helios:spec}).
\end{comment}
%Given that Helios <> has been proven secure~\cite{Bernhard12:Helios,Bernhard14:thesis,BCGPW15:eprint}, despite an attack, we must conclude that current definitions are unsuitable
Given that current definitions cannot detect such vulnerabilities (\S\ref{sec:related}),
we must conclude they're unsuitable, or assume the risk of tallying not working when
ballot collection is compromised.
%Indeed, they assume ballots are \emph{recorded-as-cast}, i.e., cast ballots are
%preserved with integrity through the ballot collection process~\cite[\S2]{AdidaN06},
%and cannot detect attacks by adversaries that control the bulletin board, the
%communication channel, or both.
Indeed, the challenger tallying \emph{all} ballots introduces an implicit
trust assumption: ballots are \emph{recorded-as-cast}, i.e., cast ballots are
preserved with integrity through the ballot collection process.\ifnocompress\footnote{%
The recorded-as-cast notion was introduced by Adida \& Neff~\cite[\S2]{AdidaN06}.}\fi\
%Thus, current definitions cannot detect attacks by adversaries that control the
%bulletin board, the communication channel, or both.
Thus, vulnerabilities that manipulate the ballot collection process cannot be detected,
including vulnerabilities that can be exploited to distinguish Alice voting `yes'
from Bob voting `no.' %We formulate a new definition
%, based upon our informal ballot secrecy game (\S\ref{sec:intro}),
%to overcome this shortcoming.
To overcome this shortcoming, we formulate a new definition of ballot secrecy
in which the adversary controls the ballot collection process, i.e.,
the bulletin board and the communication channel.
\fi
\subsection{\ifev{}Security definition\else{}Ballot secrecy\fi}
\label{sec:secrecy:def}
\begin{comment}
\ifev Smyth~\cite{Smyth15:BallotSecrecyFull} formalises \else We formalise \fi
ballot secrecy as the indistinguishability game
%between an adversary and a challenger, as
described in Section~\ref{sec:intro}.
\end{comment}
\begin{comment}
\sout{We formalise ballot secrecy (Definition~\ref{def:ballotSecrecy}) as a game that
tasks the adversary to distinguish between an instance of the voting system with some
cast votes, from another instance with a permutation of those votes.}
We formalise ballot secrecy (Definition~\ref{def:ballotSecrecy}) as a game that tasks the adversary to
select two distributions of votes and to distinguish between ballots for one distribution from ballots
for the other, or to construct a bulletin board from the ballots for one distribution and distinguish
%the election outcome produced by tallying that bulletin board
the resulting outcome
from the outcome %produced by tallying a bulletin board constructed
that would result
from ballots for the other distribution, where the votes cast
from one distribution are a permutation of the votes that would be
cast from the other.
\end{comment}
We formalise ballot secrecy (Definition~\ref{def:ballotSecrecy}) as a game that tasks the
adversary to: select two lists of votes; construct a bulletin board from ballots for
votes in one of those lists, which list is decided by a coin flip; and (non-trivially) determine the result of
the coin flip from the resulting election outcome and tallying proof. That is, the game tasks
the adversary to distinguish between an instance of the voting system for one list of votes,
from another instance with the other list of votes, when the votes cast from each list
are permutations of each other (hence, the distinction is non-trivial).
%, when the votes from the cast distribution are a permutation of the votes
%from the other distribution.
The game proceeds as follows: The challenger generates a key pair (Line~\ref{alg:BallotSecrecyGame:setup}), the adversary chooses some number of candidates
(Line~\ref{alg:BallotSecrecyGame:adv:nc}), and the challenger flips a coin
(Line~\ref{alg:BallotSecrecyGame:beta})
%and initialises an empty set (Line~\ref{alg:BallotSecrecyGame:L}).
and initialises a set to record lists of votes (Line~\ref{alg:BallotSecrecyGame:L}).
\begin{comment}
The adversary computes a bulletin board from ballots output by a left-right oracle
(Line~\ref{alg:BallotSecrecyGame:adv:bb}),
whereby $\oracle(v_0,v_1)$ outputs a ballot $b$ for $v_0$ or for $v_1$, depending on
the coin flip, and records triple $(b,v_0,v_1)$ in the set.
\end{comment}
The adversary computes a bulletin board from ballots for votes in one of two possible lists
(Line~\ref{alg:BallotSecrecyGame:adv:bb}), where the lists are chosen by the
adversary, the choice between lists is determined by the coin flip, and the
ballots (for votes in one of the lists) are
constructed by an \ifev\else left-right \fi oracle (further ballots may be constructed by
the adversary).\ifnocompress\ifev\else\footnote{Bellare \emph{et al.} introduced left-right oracles in the context of symmetric encryption~\cite{Bellare97} and Bellare \& Rogaway provide a tutorial on their use~\cite{Bellare05}.}\fi\fi\
The challenger tallies the bulletin board to derive the election outcome and tallying
proof (Line~\ref{alg:BallotSecrecyGame:tally}), which are given to the adversary
and the adversary is tasked with determining the result of the coin flip
(Line~\ref{alg:BallotSecrecyGame:adv:guess} \& \ref{alg:BallotSecrecyGame:ret}).
\begin{comment}
If the adversary is able to distinguish between the ballots output by the left-right
oracle, then the result of the coin flip can be determined independently of the
election outcome, hence, the bulletin board can be the empty set. Otherwise,
the adversary must determine the result of the coin flip from the election outcome.
\end{comment}
\begin{definition}[$\BallotSecrecy$\ifev~\cite{Smyth15:BallotSecrecyFull}\fi]\label{def:ballotSecrecy}
Let $\Gamma = (\SetupSymb,\VoteSymb,\TallySymb\ifev,\VerifySymb\fi)$ be an election scheme,
$\adv$ be an adversary, $\kk$ be a security parameter, and $\BallotSecrecy$ be
the following game.
{\upshape\LinesNumbered
\begin{inlineexperiment}{$\BallotSecrecyGame$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup$\label{alg:BallotSecrecyGame:setup}\;
$\nC \leftarrow \adv(\pk,\kk)$\label{alg:BallotSecrecyGame:adv:nc}\;
$\beta \leftarrow_R \{0,1\}$\label{alg:BallotSecrecyGame:beta}\;
$L \leftarrow \emptyset$\label{alg:BallotSecrecyGame:L}\;
$\bb \leftarrow \adv^{\oracle}()$\label{alg:BallotSecrecyGame:adv:bb}\;
$(\outcome, \tpf) \leftarrow \Tally$\label{alg:BallotSecrecyGame:tally}\;
$g\leftarrow \adv(\outcome, \tpf)$\label{alg:BallotSecrecyGame:adv:guess}\;
\Return $g = \beta \wedge\allowbreak \balanced(\bb,\nC,L)
\wedge\allowbreak 1\leq\nC\leq \mC \wedge\allowbreak |\bb| \leq \mB$\label{alg:BallotSecrecyGame:ret}\;
\end{inlineexperiment}
}
%%
%% The ballot secrecy definition assumes the number of candidates, respectively ballots, is less
%% than the maximum number of candidates, respectively ballots. Hence, individual ballots are
%% tallied correctly by correctness. We rely on this fact in proofs.
%%
\noindent
Predicate $\balanced$ and oracle $\oracle$ are defined as follows:
\begin{itemize}
\item $\balanced(\bb,\nC,L)$ holds if for all votes
$v\in\{1,\dots,\nC\}$ we have
$|\{b \mid b \in \bb \wedge \exists v_1 \mathrel. (b,v,v_1) \in L\}|
= |\{b \mid b \in \bb \wedge \exists v_0 \mathrel. (b,v_0,v) \in L\}|$; and
\item $\oracle{(v_0,v_1)}$ computes
$b\leftarrow \Vote[\pk,v_\beta,\nC,\kk]; L \leftarrow L \cup \{ (b,\allowbreak v_0,\allowbreak v_1)\}$ and
outputs $b$, where $v_0,v_1\in \{1, ...,\nC \}$.
\end{itemize}
\begin{sloppypar}
\noindent
We say $\Gamma$ satisfies $\BallotSecrecy$, if for all
probabilistic polynomial-time
adversaries $\adv$, there exists a negligible
function
$\negl$, such that for all security parameters $\kk$, we have $\Succ(\BallotSecrecyGame) \leq
\frac{1}{2} + \neglK$.
\end{sloppypar}
\end{definition}
\begin{comment}
\noindent
Game $\BallotSecrecy$ captures a setting in which the tallier generates a key
pair using the scheme's $\SetupSymb$ algorithm, publishes the public key, and only
uses the private key to compute the election outcome and tallying proof.
\end{comment}
\noindent
\ifconf
The game is satisfied
\else
An election scheme satisfies $\BallotSecrecy$
\fi
when \ifconf\else algorithm $\VoteSymb$ outputs \fi ballots
\ifconf\else that \fi
do not reveal votes and \ifconf\else algorithm $\TallySymb$ outputs \fi election outcomes
and proofs \ifconf\else that \fi
do not reveal the relation between votes expressed in collected
ballots and the outcome.%\footnote{Outputting the \emph{correct} election outcome is not
%strictly necessary for ballot secrecy, but election schemes that tally ballots incorrectly
%are not useful.}
Game $\BallotSecrecy$ tasks the adversary to compute a bulletin board, from ballots
constructed by \ifev an \else a left-right \fi oracle for votes in one of two possible lists, and determine which
list was used from the election outcome and proof generated from tallying
that board. The choice between lists is determined by the result $\beta$
of a coin flip, and the \ifev\else left-right \fi oracle outputs a ballot for vote $v_\beta$ on input of a pair of votes
$v_0,v_1$.
%inputs pairs of ballots $v_0,v_1$ and outputs ballots for $v_\beta$.
Hence, the \ifev\else left-right \fi oracle constructs ballots for votes in one of two possible lists,
where the lists are chosen by the adversary, and the bulletin board may
contain %ballots constructed by the oracle and
those ballots in addition to
ballots constructed by the adversary.
\ifev\else
\begin{comment}
In our game, the adversary has access to a left-right oracle which can
construct ballots on the adversary's behalf.\ifnocompress\ifev\else\footnote{Bellare \emph{et al.} introduced left-right oracles in the context of symmetric encryption~\cite{Bellare97} and Bellare \& Rogaway provide a tutorial on their use~\cite{Bellare05}.}\fi\fi\
The oracle constructs ballots in two ways, corresponding to a bit
$\beta$ chosen uniformly at random by the challenger.
If $\beta=0$, then, given a pair of votes $v_0,v_1$, the oracle constructs a ballot for $v_0$
and outputs the ballot to the adversary. Otherwise ($\beta=1$), the oracle
outputs a ballot for $v_1$.
The adversary computes a bulletin board, which may include ballots constructed by the oracle.
Thus, the game captures a setting where the bulletin board is computed by an adversary that casts ballots on behalf
of some voters and controls the votes cast by the remaining voters.
%
The challenger tallies the adversary's bulletin board to derive an election outcome and tallying proof.
The adversary is given the outcome and proof, and wins by determining whether $\beta=0$ or $\beta=1$.
Intuitively, if the adversary wins, then there exists a strategy to distinguish ballots, otherwise, the adversary is unable to distinguish between a ballot for vote $v_0$ and a ballot for vote $v_1$, therefore, voters' votes cannot be revealed.
\end{comment}
\fi
%Our notion of ballot secrecy considers
Election schemes %which
reveal the number of votes for each candidate (i.e., the election outcome).
Hence, to avoid trivial distinctions in game $\BallotSecrecy$,
we require that runs of the game are \emph{balanced}: ``left'' and ``right''
inputs to the \ifev\else left-right \fi oracle are equivalent, when the corresponding
outputs appear on the bulletin board.
For example, suppose the inputs to the \ifev\else left-right \fi oracle
are $(v_{1,0},v_{1,1}),\dots, (v_{n,0},v_{n,1})$ and the corresponding
outputs are $b_1,\dots,b_n$, further suppose the bulletin board
is $\{b_1,\dots,b_\ell\}$ such that $\ell \leq n$.
That game is balanced if the ``left'' inputs $v_{1,0},\dots,v_{\ell,0}$
are a permutation of the ``right'' inputs $v_{1,1},\dots,v_{\ell,1}$.
The balanced condition prevents trivial distinctions.\ifnocompress\ifev\else\footnote{%
A weaker balanced condition might be sufficient for
alternative formalisations of election schemes.
For instance, voting systems which only announce the winning
candidate could be analysed using a balanced condition
asserting that the winning candidate was input on both the
``left'' and ``right.''}\fi\fi\
For instance,
an adversary that computes a bulletin board containing only the
ballot output by \ifev an \else a left-right \fi oracle query with input $(1, 2)$
cannot win the game, because it is unbalanced. Albeit,
that adversary could trivially determine whether $\beta=0$ or $\beta=1$,
given the tally of that board. %(Formally defining a winning
%adversary is left as an exercise for the reader.)
Intuitively, if the adversary wins game $\BallotSecrecy$, then there exists a strategy
to distinguish ballots. Indeed, such an adversary can distinguish between an instance
of the voting system in which voters cast some votes, from another instance in which
voters cast a permutation of those votes, thus, voters' votes are revealed. Otherwise,
the adversary is unable to distinguish between a voter casting a ballot for vote $v_0$
and another voter casting a ballot for vote $v_1$, hence, voters' votes cannot be
revealed.
\ifev\else
Proving ballot secrecy is time consuming. Indeed, a
proof for the simple $\encToVoteSymb$ scheme
consumes around four and a half pages~\cite[Appendix C.6]{Smyth15:Hawk}.
%Thus, sufficient conditions for ballot secrecy should be sought, and we will see
%that ballot independence suffices.
To reduce the expense of such proofs, we introduce ballot independence (\S\ref{sec:independence})
and prove that it suffices for $\BallotSecrecy$ (\S\ref{sec:rel}).
%Indeed, Smyth uses this condition to prove ballot-secrecy for $\encToVoteSymb$ in just
%over a page~\cite[\S4.3]{Smyth18:voting-tutorial}.
Using this sufficient condition, the four and a half page proof can be reduced to
around one page~\cite[\S4.3]{Smyth18:voting-tutorial}.
\fi
\begin{comment}
\begin{color}{blue}
Our definition of ballot secrecy has stood the test of time: Since its first
appearance in 2015~\cite{}, it has been subject to eight rounds of peer review
(by conferences PKC'16, PKC'17, S\&P'18, CSF'18, CCS'18, and S\&P'19, and
journals TDSC in 2017 and JACM in 2019) and not a single reviewer has found
fault.
\end{color}
\end{comment}
\ifev
\subsection{Example}
\label{sec:secrecy:example}
\iftutorial
\textcolor{red}{We might like to provide an informal introduction to
asymmetric encryption scheme}
\fi
We recall syntax for asymmetric encryption scheme in the appendix and
model our $\encToVoteSymb$ voting system (\S\ref{sec:intro}) as the
following election scheme.
\begin{definition}[$\encToVoteSymb$\ifev\cite{Smyth15:BallotSecrecyFull}\fi]\label{def:mv}
Given an asymmetric encryption scheme
$\Pi = (\GenSymb,\allowbreak\EncSymb,\allowbreak\DecSymb)$,
we define $\encToVote =\allowbreak (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$
such that:
\begin{itemize}
\item $\Setup$ computes $(\pk,\sk,\votespace)\leftarrow\Gen;\pk'\leftarrow(\pk,\allowbreak\votespace);\allowbreak\sk'\leftarrow(\pk,\sk)$,
derives $\mC$ as the largest integer such that $\{0,\dots,\mC\}\subseteq\{0\} \cup\votespace$
and for all $m_0,m_1\in\{1,\dots,\mC\}$ we have $|m_0|=|m_1|$,
and outputs $(\pk',\allowbreak\sk',\allowbreak p(\kappa),\mC)$,
where $p$ is a polynomial function.
\item $\Vote[\pk',v,\nC,\kk]$ parses $\pk'$ as pair $(\pk,\votespace)$,
outputting $\perp$ if parsing fails or
$v\not\in\{1,\dots,\nC\} \vee \{1,\allowbreak\dots,\allowbreak\nC\}\not\subseteq\votespace$,
computes $b\leftarrow\Enc{v}$, and outputs $b$.
\item $\Tally[\sk',\bb,\nC,\kk]$ initialises $\outcome$ as a zero-filled vector of length $\nC$,
parses $\sk'$ as pair $(\pk,\sk)$, outputting $(\outcome,\perp)$ if parsing fails,
computes
{ \DontPrintSemicolon
\llFor{$b\in\bb$}{%
$v\leftarrow\Dec{b};$
\llIf{$1\leq v\leq \nC$}{$\outcome[v] \leftarrow \outcome[v]+1$}%
}%
}, and outputs
$(\outcome,\epsilon)$, where $\epsilon$ is a constant symbol.
\ifev
\item $\Verify$ outputs 1.
\fi
\end{itemize}
\end{definition}
\noindent
To ensure $\encToVote$ is an election scheme, we require asymmetric
encryption scheme $\Pi$ to produce distinct ciphertexts with overwhelming
probability, otherwise correctness cannot be satisfied, as the following
lemma demonstrates.
\begin{lemma}\label{lemma:enc2vote:correctnessIssue}
\begin{sloppypar}
There exists an asymmetric encryption scheme $\Pi$ such that
$\encToVote$ is not an election scheme.
\end{sloppypar}
\end{lemma}
\noindent
To prove our lemma, we show that colliding ciphertexts suffice to ensure
that election scheme $\encToVoteSymb$ cannot satisfy the correctness property
of Definition~\ref{def:election}.
\begin{proof}
Let $\encToVote = (\SetupSymb,\allowbreak \VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$.
Suppose $(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC)$ is an
output of $\Setup$ and $b$ and $b'$ are outputs of $\Vote[\pk,v,\nC,\kk]$
such that $2 \leq \mB \wedge 1\leq v \leq \nC \leq \mC$, where
$\kk$ is a security parameter. Further suppose $\outcome$ is
a zero-filled vector of length $\nC$, except for index $v$ which contains
two. Moreover, suppose $(\outcome',\tpf)$ is an output of
$\Tally[\sk,\{b,b'\},\nC, \kk]$. If $b$ and $b'$ collide, then outcome
$\outcome'$ is computed from set $\{b,b'\} = \{b\}$, therefore,
the correct outcome cannot have been computed, we have
$\outcome \not= \outcome'$, with non-negligible probability,
hence, correctness is not satisfied.
By definition of algorithm $\SetupSymb$, we have $\pk$ is a pair and,
by definition of algorithm $\VoteSymb$, we have $b$ and $b'$ are ciphertexts
on plaintext $v$. Thus, it remains to show that asymmetric encryption schemes
can produce ciphertexts that collide. Indeed, they can: Consider
$\Pi = (\GenSymb,\EncSymb,\allowbreak\DecSymb)$ such that $\Enc{m}$ outputs $m$
and $\Dec{c}$ outputs $c$. Although $\Pi$ is clearly not secure, it
is straightforward to see that $\Pi$ satisfies correctness, because
$\Dec{\Enc{m;r}} = m$ for all key pairs $(\pk,\sk)$, plaintexts $m$, and
coins $r$, which concludes our proof.
\end{proof}
\noindent
It follows from Lemma~\ref{lemma:enc2vote:correctnessIssue} that we must
restrict the class of asymmetric encryption schemes used to
instantiate $\encToVoteSymb$. We could consider a broad class of
schemes that produce distinct ciphertexts with overwhelming
probability, but we favour the narrower class of non-malleable
schemes, since we require non-malleability for ballot secrecy.
Definitions of non-malleability are complex and proofs of non-malleability
are relatively difficult, so we adopt the definition of indistinguishability
under parallel attack ($\INDPA$) by Bellare \& Sahai~\cite{Bellare99:IND-k-CPA},
which is simpler, yet equivalent to their definition of comparison based
non-malleability ($\CNMCPA$). We recall the definition of $\INDPA$ in
the appendix.
\begin{lemma}
Given an asymmetric encryption scheme $\Pi$ satisfying $\INDPA$, we have
$\encToVote$ is an election scheme.
\end{lemma}
\noindent
To prove our lemma, we show that $\encToVoteSymb$ satisfies the correctness
property of Definition~\ref{def:election} when ciphertexts do not
collide.
\begin{proof}
Let $\encToVote = (\SetupSymb,\allowbreak \VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$ and $\Pi = (\GenSymb,\EncSymb,\allowbreak\DecSymb)$.
Moreover, let $\kappa$ be a security parameter, $\nB$ and $\nC$ be integers,
$v_1,\dots,v_{\nB}\in\{1,\dots,\nC\}$ be votes, and $\outcome$ be a
zero-filled vector of length $\nC$. Suppose $(\pk',\allowbreak\sk',\allowbreak\mB,\allowbreak \mC)$
is an output of $\Setup$ such that $\nB \leq \mB \wedge \nC\leq \mC$.
Further suppose we compute
{\DontPrintSemicolon\llFor{$1 \leq i \leq \nB$}{%
$b_i \leftarrow \Vote[\pk,v_i,\nC,\kk];
\outcome[v_i] \leftarrow \outcome[v_i] + 1$%
}}.
Moreover, suppose $(\outcome',\tpf)$ is an output of
$\Tally[\sk,\{b_1,\dots,b_{\nB}\},\nC, \kk]$.
To prove correctness, it suffices to prove $\outcome = \outcome'$,
with overwhelming probability.
By definition of algorithm $\SetupSymb$, we have $\pk'$ is a pair $(\pk,\votespace)$
and $\sk'$ is a pair $(\pk,\sk)$ such that $(\pk,\sk,\votespace)$ was output by
$\Gen$. Moreover, $\mC$ is the largest integer such that
$\{0,\dots,\mC\}\subseteq\{0\} \cup\mathfrak m$, hence,
$\{1,\allowbreak\dots,\allowbreak\nC\}\subseteq\votespace$.
It follows by definition of algorithm $\VoteSymb$ that for each
$i\in\{1,\dots,\nB\}$ we have $b_i$ is an output of $\Enc{v_i}$.
Moreover, by definition of algorithm $\TallySymb$,
outcome $\outcome'$ is initialised as a zero-filled vector of length $\nC$
and computed as follows:
{\DontPrintSemicolon
\llFor{$b\in\{b_1,\dots,b_{\nB}\}$}{%
$v\leftarrow\Dec{b};$
\llIf{$1\leq v\leq \nC$}{$\outcome'[v] \leftarrow \outcome'[v]+1$}%
}%
}.
\noindent
Since $\Pi$ satisfies $\INDPA$, ciphertexts $b_1,\dots,b_{\nB}$
are distinct with overwhelming probability, hence, that computation
is equivalent to the following:
{\DontPrintSemicolon
\llFor{$1 \leq i \leq \nB$}{%
$v\leftarrow\Dec{b_i};$
\llIf{$1\leq v\leq \nC$}{$\outcome'[v] \leftarrow \outcome'[v]+1$}%
}%
}.
\noindent
Moreover, by correctness of $\Pi$, we have $\Dec{b_i} = v_i$
for all $i\in\{1,\dots,\nB\}$, with
overwhelming probability. Thus, the above computation is equivalent to
computing
{\DontPrintSemicolon
\llFor{$1 \leq i \leq \nB$}{%
$\outcome'[v_i] \leftarrow \outcome'[v_i]+1$}%
},
\noindent
with overwhelming probability. It follows that outcomes $\outcome$ and $\outcome'$
are computed identically, with overwhelming probability, thereby
concluding our proof.
\end{proof}
\noindent
Intuitively, election scheme $\encToVote$ satisfies ballot secrecy until
tallying, because asymmetric encryption scheme $\Pi$ can ensure that voters'
votes are not revealed, and tallying maintains ballot secrecy by revealing
only the election outcome.
\begin{proposition}\label{prop:encToVoteBS}
Given an asymmetric encryption scheme $\Pi$ satisfying $\INDPA$,
election scheme $\encToVote$ satisfies $\BallotSecrecy$.
\end{proposition}
\noindent
Proving this proposition and other ballot secrecy results is time consuming.
Indeed, Quaglia \& Smyth's proof of ballot secrecy for our simple $\encToVoteSymb$
voting system fills over six and a half pages~\cite[Appendix C.6]{Smyth15:Hawk}
and Cortier \emph{et al.} devoted one person-year to their proof of ballot
secrecy for Helios~\cite{Cortier17:HeliosMachineChecked}.
%Smyth introduces sufficient conditions for ballot secrecy that significantly simply
%proofs~\cite{Smyth15:BallotSecrecyFull} and our proof sketches in the remaining
%sections will rely on his results.
To reduce the expense of ballot-secrecy proofs, the following section introduces
sufficient conditions that enable the simplification of game $\BallotSecrecy$,
which gives way to simpler proofs. Indeed, we prove
Proposition~\ref{prop:encToVoteBS} in just over a page.
\LinesNotNumbered
\subsection{Simplifying proofs}\label{sec:secrecy:simpleProofs}
Tallying proofs may reveal voters' votes. For example, a variant of $\encToVoteSymb$
might define tallying proofs that map ballots to votes. Hence, such proofs are rightly
provided to the adversary in game $\BallotSecrecy$ (Line~\ref{alg:BallotSecrecyGame:adv:guess}).
Nevertheless, if tallying proofs
reveal nothing about the votes expressed in ballots on the bulletin board, then they
can be omitted from the game. This precondition is ensured by election schemes that use
zero-knowledge tallying proofs. Thus, the adversary need not be
provided with such proofs in game $\BallotSecrecy$ when analysing such schemes,
which achieves our first reduction in the expense of ballot-secrecy proofs. Our second
reduction involves modifying the computation of election outcomes.
Game $\BallotSecrecy$ computes the election outcome from ballots constructed by the
oracle and ballots constructed by the adversary (Line~\ref{alg:BallotSecrecyGame:tally}).
Intuitively, such an outcome can be equivalently computed as follows:
{\upshape
\begin{algorithm}[H]
$(\outcome, \tpf)\leftarrow \Tally[\sk,\bb\setminus\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
$(\outcome', \tpf')\leftarrow \Tally[\sk,\bb\cap\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
$\outcome \leftarrow \outcome + \outcome'$\;
\end{algorithm}
}
\noindent
Yet, a poorly designed tallying algorithm might not ensure equivalence. In particular,
ballots constructed by the adversary can cause the algorithm to behave unexpectedly.
(Such algorithms are nonetheless compatible with our correctness requirement, because
correctness does not consider an adversary.) Nevertheless, the equivalence holds when
individual ballots are tallied correctly. Moreover, the above computation is equivalent
to the following:
{\upshape
\begin{algorithm}[H]
$(\outcome, \tpf)\leftarrow \Tally[\sk,\bb\setminus\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$(\outcome', \tpf')\leftarrow \Tally[\sk,\{b\},\nC,\kappa]$\;
$\outcome \leftarrow \outcome + \outcome'$\;
}
\end{algorithm}
}
\noindent
Furthermore, by correctness of the election scheme, the above for-loop
can be equivalently computed as follows:
{\upshape
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_\beta] \leftarrow \outcome [v_\beta] +1$\;
}
\end{algorithm}
}
\noindent
Indeed, for each $b \in \bb \wedge (b,v_0,v_1) \in L$, we have $b$ is an output of
$\Vote[\pk,\allowbreak v_\beta,\allowbreak\nC,\allowbreak\kk]$, hence,
$\Tally[\sk,\{b\},\nC,\kappa]$ outputs $(\outcome, \tpf)$ such that $\outcome$
is a zero-filled vector, except for index $v_\beta$ which contains one,
and this suffices to ensure equivalence. In addition, for any adversary that wins
game $\BallotSecrecy$, we are assured that $\balanced(\bb,\nC,L)$ holds, hence,
the above for-loop can be computed as
{\upshape
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_0] \leftarrow \outcome [v_0] +1$\;
}
\end{algorithm}
}
\noindent
or
{\upshape
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_1] \leftarrow \outcome [v_1] +1$\;
}
\end{algorithm}
}
\noindent
without weakening the game. Thus, perhaps surprisingly, tallying ballots constructed
by the oracle does not
provide the adversary with an advantage (in determining whether $\beta = 0$ or
$\beta = 1$) and we can omit such ballots from tallying in game $\BallotSecrecy$.
That is, we need only consider the game derived from $\BallotSecrecy$ by
replacing $\adv(\outcome, \tpf)$
with $\adv(\outcome)$ and $\balanced(\bb,\nC,L)$ with $b\not\in\bb$, where the former
modification captures our first reduction in the expense of ballot-secrecy proofs
and the latter captures our second.
Smyth~\cite{Smyth15:BallotSecrecyFull} further reduces the expense of ballot-secrecy
proofs by removing the oracle in favour of a single challenge ballot:
\LinesNumbered
\begin{definition}[$\BallotIndependence$\ifev~\cite{Smyth15:BallotSecrecyFull}\fi]\label{def:ind-independence}
Let $\Gamma = (\SetupSymb,\VoteSymb,\TallySymb\ifev,\VerifySymb\fi)$ be
an election scheme, $\adv$ be an adversary, $\kk$ be the security parameter,
and $\BallotIndependence$ be the following game.
{\upshape
\begin{inlineexperiment}{$\BallotIndependenceGame$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup$\;
$(v_0,v_1,\nC) \leftarrow \adv(\pk,\kk)$\;
$\beta \leftarrow_R \{0,1\}$\;
$b \leftarrow \Vote[\pk,v_\beta,\nC,\kk]$\;
$\bb \leftarrow \adv(b)$\;
$(\outcome,\tpf) \leftarrow \Tally$\label{alg:BallotIndependenceGame:tally}\;
$g\leftarrow \adv(\outcome)$\;
\Return $g = \beta\mathrel\wedge\allowbreak
b\not\in\bb \mathrel\wedge\allowbreak 1 \leq v_0,v_1 \leq \nC \leq \mC \mathrel\wedge\allowbreak |\bb| \leq \mB$\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies \ifev $\BallotIndependence$\else
\emph{indistinguishability under chosen vote attack ($\BallotIndependence$)}\fi,
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\negl$, such that for all security parameters $\kk$,
we have $\Succ(\BallotIndependenceGame) \leq \frac{1}{2} + \neglK$.
\end{definition}
\LinesNotNumbered
\noindent
An election scheme satisfies
%indistinguishability under chosen vote attack ($\BallotIndependence$)
$\BallotIndependence$ when algorithm $\VoteSymb$ outputs non-malleable ballots.
Smyth proves that game
$\BallotSecrecy$ is strictly stronger than game $\BallotIndependence$, moreover,
he proves that the games coincide for election schemes with zero-knowledge tallying proofs
that tally individual ballots correctly~\cite[Theorems~2 \&~5]{Smyth15:BallotSecrecyFull}.
Furthermore, he proves that universally-verifiable election schemes tally
individual ballots correctly~\cite[Lemmata~9 \&~28]{Smyth15:BallotSecrecyFull}.
\begin{tcolorbox}
\begin{guideline}
Ballots must be non-malleable.
\end{guideline}
\end{tcolorbox}
%\noindent
These results significantly reduce the expense of ballot-secrecy proofs
and we now use them to prove Proposition~\ref{prop:encToVoteBS}.
\begin{proof}[Proof of Proposition~\ref{prop:encToVoteBS}]
We proceed by contradiction:
Suppose election scheme $\encToVote$ does not satisfy $\BallotSecrecy$.
Since $\BallotSecrecy$ is strictly stronger than
$\BallotIndependence$~\cite[Theorem~2]{Smyth15:BallotSecrecyFull},
scheme $\encToVote$ does not satisfy $\BallotIndependence$ either, hence,
there exists a probabilistic polynomial-time adversary $\adv$ that wins
$\BallotIndependenceGame[\encToVote,\allowbreak\adv,\allowbreak\kk]$ with
success greater than negligibly better than guessing, for some security
parameter $\kk$. From $\adv$, we construct the following adversary $\Adv$
that wins $\INDPA$.
\begin{itemize}
\item $\Adv(\pk,\votespace,\kk)$ computes
$\pk'\leftarrow (\pk,\votespace);(v_0,v_1,\nC) \leftarrow \adv(\pk',\kk)$ and
outputs $(v_0,v_1)$.
\item $\Adv(b)$ computes $\bb\leftarrow \adv(b)$, parses $\bb$ as a set
$\{b_1,\dots,b_{|\bb|}\}$, and outputs vector $(b_1,\dots,b_{|\bb|})$.
\item $\Adv({\bf m})$ initialises $\outcome$ as a zero-filled vector of length $\nC$,
computes
{\DontPrintSemicolon
\llFor{$1 \leq i \leq |{\bf m}|$}{%
$v\leftarrow {\bf m}[i]$;
\llIf{$1\leq v\leq \nC$}{$\outcome[v] \leftarrow \outcome[v]+1;$}
$g \leftarrow \adv(\outcome)$%
}%
} and outputs $g$.
\end{itemize}
\noindent
We prove that the success of adversary $\Adv$ is equivalent to the success of
adversary~$\adv$, which contradicts our assumption that $\Pi$ satisfies $\INDPA$.
Let $\Pi = (\GenSymb,\allowbreak\EncSymb,\allowbreak\DecSymb)$
and $\encToVote =\allowbreak (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$.
Suppose $(\pk,\sk,\votespace)$ is an output of $\Gen$, $(v_0,v_1)$
is an output of $\Adv(\pk,\allowbreak\votespace,\allowbreak\kk)$, and $b$ is an output of
$\Enc{v_\beta}$, for some bit $\beta$ chosen uniformly at random.
Moreover, suppose $(b_1,\dots,b_\ell)$ is an output of $\Adv(b)$.
By inspection of algorithms $\SetupSymb$ and $\VoteSymb$, and of
adversary $\Adv$, it is trivial to see that $\Adv$
simulates the challenger in $\BallotIndependence$ to adversary $\adv$.
Indeed, adversary $\Adv$ couples public key $\pk$ with message space $\votespace$,
and inputs the resulting pair $\pk'$ to $\adv$, which
corresponds to the public key computed by algorithm $\SetupSymb$, hence,
the public key input to $\adv$ by the challenger in $\BallotIndependence$.
Thus, adversary $\adv$ behaves as if playing game $\BallotIndependence$
and output $(v_0,v_1)$ is indistinguishable from outputs that
would be observed whilst playing that game. Moreover,
since $\adv$ wins with success greater than negligibly better
than guessing, we have $1 \leq v_0,v_1 \leq \nC \leq \mC$,
furthermore, $\{1,\dots,\nC\}\subseteq\votespace$, where
$\mC$ is the largest integer such that $\{0,\dots,\mC\}\subseteq{\{0\} \cup\votespace}$
and for all $m_0,m_1\in\{1,\dots,\mC\}$ we have $|m_0|=|m_1|$
(hence, $|v_0| = |v_1|$, which is required to win $\INDPA$), with the same probability.
It follows that outputs of $\Enc{v_\beta}$ and $\Vote[\pk,v_\beta,\nC,\kk]$ are indistinguishable. Thus, output $(b_1,\dots,b_\ell)$ is indistinguishable from outputs
that would be observed in game $\BallotIndependence$, with
the same probability. Moreover,
since $\adv$ wins, we have $b\not\in \{b_1,\dots,b_\ell\}$, hence,
$\bigwedge_{1\leq i \leq \ell} b \not= b_i$, again with the same
probability.
%It remains to show that the success of adversary $\Adv$ is equivalent
%to the success of $\adv$.
Let ${\bf m} = (\Dec{b_1},\dots,\Dec{b_\ell})$ and suppose $g$ is
an output of $\Adv({\bf m})$. By inspection of algorithm $\TallySymb$
and of adversary $\Adv$, it is straightforward to see that $\Adv$
simulates the challenger in $\BallotIndependence$ to adversary $\adv$.
Indeed, both the algorithm and adversary initialise $\outcome$
as a zero-filled vector of length $\nC$, then the adversary $\Adv$
computes
\begin{algorithm}[H]
\llFor{$1 \leq i \leq |{\bf m}|$}{%
$v\leftarrow {\bf m}[i]$;
{\DontPrintSemicolon
\llIf{$1\leq v\leq \nC$}{$\outcome[v] \leftarrow \outcome[v]+1$}%
}%
}
\end{algorithm}
\noindent
which is equivalent to algorithm $\TallySymb$ computing
\begin{algorithm}[H]
\llFor{$b\in\{b_1,\dots,b_\ell\}$}{%
$v\leftarrow\Dec{b};$
{\DontPrintSemicolon
\llIf{$1\leq v\leq \nC$}{$\outcome[v] \leftarrow \outcome[v]+1$}%
}%
}
\end{algorithm}
\noindent
because algorithm $\DecSymb$ is deterministic.
Thus, output $g$ is indistinguishable from outputs that would be
observed in game $\BallotIndependence$. It follows that the success
of adversary $\Adv$ is equivalent to the success of $\adv$, and we
conclude our proof by~\cite[Theorem~5]{Smyth15:BallotSecrecyFull},
since Smyth proves that games $\BallotIndependence$ and $\BallotSecrecy$
coincide for election schemes with zero-knowledge tallying proofs that tally
individual ballots correctly. (We omit proving that election scheme $\encToVote$
has zero-knowledge tallying proofs and tallies individual ballots correctly to avoid
recalling formal definitions of those properties. Proving the former
is trivial, because $\tpf$ is a constant, hence, it reveals nothing about
the votes expressed in ballots $b_1,\dots,b_\ell$. And the latter
follows from the definition of algorithm $\TallySymb$, by correctness
of $\Pi$, and since $\Pi$ satisfies $\INDPA$, which is required only
to ensure ciphertexts do not collide. Formally proving these details
is left as an exercise for the reader.)
\end{proof}
\begin{sloppypar}
We can exploit Proposition~\ref{prop:encToVoteBS} to achieve our
fourth and final reduction in the expense of ballot-secrecy proofs.
Indeed, if an election scheme tallies sets of ballots correctly (rather
than individual ballots, as previously required), then we can compute
the election outcome using function $\correcttally$ in game $\BallotIndependence$,
rather than the tallying algorithm, i.e., by replacing
$(\outcome,\tpf) \leftarrow \Tally$ with $\outcome \leftarrow \correcttally(\pk,\nC,\bb,\kk)$.
It follows that election scheme
$(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$
satisfies $\BallotSecrecy$ if and only if
$(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb',\allowbreak\VerifySymb')$
does, assuming algorithms $\TallySymb$ and $\TallySymb'$ both tally
sets of ballots correctly. Proposition~\ref{prop:encToVoteBS} proves that
election scheme $\encToVote$ satisfies $\BallotSecrecy$, assuming
$\Pi$ is an asymmetric encryption scheme satisfying $\INDPA$, and
Smyth~\cite[Lemma~14]{Smyth15:BallotSecrecyFull} proves that $\encToVote$ tallies
sets of ballots correctly, under the additional assumption that $\Pi$ satisfies
\emph{well-definedness}, i.e., ``ill-formed'' ciphertexts are distinguishable from
``well-formed'' ciphertexts.
Thus, $\BallotSecrecy$ is satisfied by any election scheme derived from
$\encToVote$ by replacing its tallying and verification algorithms, assuming
the replacement tallying algorithm tallies sets of ballots correctly and
uses zero-knowledge tallying proofs~\cite[Theorem~15]{Smyth15:BallotSecrecyFull}.
Moreover, Smyth proves that universally-verifiable election schemes tally sets of
ballots correctly~\cite[Lemma~28]{Smyth15:BallotSecrecyFull}. It follows that proofs
of ballot secrecy are trivial for a class of universally-verifiable,
encryption-based voting systems: Any universally-verifiable election scheme derived from
$\encToVote$ satisfies $\BallotSecrecy$ if $\Pi$ satisfies $\INDPA$ and well-definedness,
and tallying proofs are zero-knowledge.
\end{sloppypar}
We will use our third simplification to prove that a variant of Helios satisfies
$\BallotSecrecy$ and the fourth to prove that a variant of Helios Mixtnet does too
(the original schemes have known vulnerabilities and they do not satisfy $\BallotSecrecy$),
thereby demonstrating the application of these results.
\LinesNumbered
\ifev
\subsection{Related definitions of ballot secrecy}
\label{sec:secrecy:related}
\else
```
# Related work
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 666, column 13): unexpected } expecting \end{document} consideration. Moreover, no voting system is equivalent to the ideal functionality ^`
``` latex
\section{Related work}\label{sec:related}
\fi
Discussion of ballot secrecy originates from Chaum~\cite{Chaum:1981} and the earliest
definitions of ballot secrecy are due to Benaloh \emph{et al.}~\cite{Benaloh86,BT94:ReceiptFreeVoting,Benaloh96:Thesis}.\ifanon\else\ifev\else\footnote{%
Quaglia \& Smyth present a tutorial-style introduction to modelling
ballot secrecy~\cite{Smyth17:voting-tutorial}, and Bernhard \emph{et al.}
survey ballot secrecy definitions~\cite{BCGPW15,BCGPW15:eprint}.}\fi\fi\
More recently, Bernhard \emph{et al.} propose a series of ballot secrecy definitions\ifev\else:
They consider election schemes without tallying proofs~\cite{Smyth11:HeliosProvableSecure,Bernhard11:Helios}
and, subsequently, schemes with tallying proofs\fi~\cite{Bernhard12:Helios,2013:BallotIndependenceESORICS,2014:BallotIndependenceEprint,BCGPW15}.
\ifev
Smyth~\cite{Smyth15:BallotSecrecyFull} shows that these definitions do not
detect vulnerabilities that arise when an adversary controls the bulletin
board or the communication channel.
By comparison, the definition of ballot secrecy that we consider
(Definition~\ref{def:ballotSecrecy}) detects such vulnerabilities
and appears to be the strongest definition in the literature.
\else
The definition by Bernhard, Pereira \& Warinschi
computes tallying proofs using algorithm $\TallySymb$ or a simulator \cite{Bernhard12:Helios}, but that
definition is too weak\ifBPRIV\else\
and some strengthening is required\fi~\cite[\S3.4 \&~\S4]{BCGPW15}.
(Cortier \emph{et al.}~\cite{Cortier13,Cortier13b} propose a variant of the ballot secrecy
definition by Bernhard, Pereira \& Warinschi, which is also too weak~\cite{BCGPW15}.)
%%\ifBPRIV%
%%. \textcolor{red}{A strengthening is proposed~\cite[Definition~7]{BCGPW15}, but the strengthened
%%definition is also too weak, in particular, schemes without tallying proofs satisfy
%%the strengthened definition, yet such schemes may not ensure free-choice,
%%%and problems exist for schemes with tallying proofs too,
%%as shown in Appendix~\ref{app:BPRIV}.}
%%\fi
\ifBPRIV
A strengthening of the definition by Bernhard, Pereira \& Warinschi
is proposed~\cite[Definition~7]{BCGPW15}, but the strengthened
definition is also too weak, as shown in Appendix~\ref{app:BPRIV}.
The
\else
By comparison, the
\fi
definition by Smyth \& Bernhard
computes tallying proofs using only algorithm $\TallySymb$~\cite{2013:BallotIndependenceESORICS},
but their definition is too strong~\cite[\S3.5]{BCGPW15} and a weakening is
required~\cite{2014:BallotIndependenceEprint}.
We prove that our ballot secrecy definition is strictly stronger than the
weakened definition by Smyth \& Bernhard (Appendix~\ref{app:relation}).
\ifBPRIV\else
The relative merits of definitions
by Smyth \& Bernhard~\cite[Definition~5]{2014:BallotIndependenceEprint} and by Bernhard
\emph{et al.}~\cite[Definition~7]{BCGPW15} are unknown, in particular, it is
unknown whether one definition is stronger than the other.
\fi
\fi
%\footnotetext{
%The proposed strengthening seems to result in a definition of ballot
%secrecy~\cite[Definition~7]{BCGPW15} that is too strong.
%%
%% Discussion with David Bernhard suggests that it is not.
%%
% in particular, it cannot be satisfied by election schemes which use partial ElGamal decryptions,
% for reasons similar to those discussed in Section~\ref{sec:rel}.
%%
%% It seems that partial ElGamal decryptions are (to my surprise) zero-knowledge
%%
% In particular, their definition does not include an analogous notion of
% balanced, which prevents trivial distinctions (cf. \S\ref{sec:secrecyDef}).
%%
%% See below.
%%
% In particular, their definition does not include an analogous notion of
% balanced. Hence, if a scheme satisfies their definition, then tallying proofs
% can be simulated for incorrect outcomes. It follows that their definition
% of ballot secrecy is incompatible with verifiability, assuming simulation
% is efficient.
%%
%% It seems that the random oracle model prevents the simulator being used,
%% in particular, the simulator can patch the oracle, whereas the verifiability
%% adversary cannot. See email from David dated 8th September 2015.
%%
%}}
\ifev\else
%In the context of elections,
Discussion of ballot independence originates from Gennaro~\cite{Gennaro95:Independence:SK-voting}
and the apparent relationship between ballot secrecy and ballot independence has
been considered.
%\sout{Gennaro %~\cite{Gennaro95:Independence:SK-voting}
%shows that applying the Fiat-Shamir heuristic
%in the Sako-Kilian electronic voting protocol %~\cite{SK94:Voting}
%violates ballot independence.} \textcolor{red}{drop if no relation to privacy}
In particular, Benaloh
shows that a simplified version of his voting system allows the administrator's
private key to be recovered by an adversary who casts a ballot as a function of
other voters' ballots~\cite[\S2.9]{Benaloh96:Thesis}.
More generally, Sako \& Kilian~\cite[\S2.4]{Sako95:ImpactOfNoIndependence},
Michels \& Horster~\cite[\S3]{Michels96:ImpactOfNoIndependence},
Wikstr\"om~\cite{Wikstrom06:Independence,Wikstrom08:Independence,Wikstrom16:VerificatumManual} and
Cortier \& Smyth~\cite{Smyth12:Helios,Smyth11:Helios} discuss how malleable ballots
can be abused to compromise ballot secrecy.
The first definition of ballot independence seems to be due to
Smyth \& Bernhard~\cite{2013:BallotIndependenceESORICS,2014:BallotIndependenceEprint}.
Smyth \& Bernhard also formally prove relations between their definitions
of ballot secrecy and ballot independence.
Independence has also been studied beyond elections, e.g., \cite{Chor85:Independence},
and the possibility of compromising security
in the absence of independence has been considered, e.g., \cite{Chor87:Independence,Pfitzmann89:MixnetAttack,Pfitzmann94:MixnetAttack,Dolev91:Nonmalleable,Dolev00:Nonmalleable,Gennaro00:Independence}.
\fi
\ifev\else
All of the ballot secrecy definitions by Bernhard \emph{et al.}~\cite{Smyth11:HeliosProvableSecure,Bernhard11:Helios,Bernhard12:Helios,2013:BallotIndependenceESORICS,2014:BallotIndependenceEprint,BCGPW15}
\ifev\else and the ballot independence definition by Smyth \& Bernhard~\cite{2013:BallotIndependenceESORICS,2014:BallotIndependenceEprint} \fi
focus on detecting vulnerabilities exploitable by adversaries that control some voters.
Vulnerabilities that require control of the bulletin board or the communication channel
are not detected, i.e., the bulletin board is implicitly assumed to operate in
accordance with the election scheme's rules and the communication channel is
implicitly assumed to be secure.
\ifev
By comparison, the definition of ballot secrecy that we consider (Definition~\ref{def:ballotSecrecy})
detects these vulnerabilities.
\else
This introduces a trust assumption. Under
this assumption, Smyth \& Bernhard prove non-malleable ballots are unnecessary
for ballot secrecy~\cite[\S4.3]{2013:BallotIndependenceESORICS}.
\begin{comment}
and Bernhard, Pereira \& Warinschi~\cite{Bernhard12:Helios},
Bernhard~\cite{Bernhard14:thesis} and Bernhard \emph{et al.}~\cite{BCGPW15:eprint,BCGPW15}
prove that %variants of
\heliosspec\ satisfies various notions of ballot secrecy.
\end{comment}
By comparison, we prove non-malleable ballots are
necessary for ballot secrecy without this trust assumption.
\begin{comment}
Hence,
%the aforementioned variants of \heliosspec\ do not
\heliosspec\ does not satisfy our definition of ballot secrecy.
\end{comment}
Thus, our definition of ballot secrecy improves upon definitions by Bernhard \emph{et al.}
by detecting more vulnerabilities.
\fi
\fi
\ifev\else
\begin{comment}
Security definitions are fundamental. Yet inappropriate definitions may fail to detect
attacks %. Indeed, we have discussed ballot secrecy definitions which are
%inappropriate to capture attacks by adversaries that control the bulletin
%board or the communication channel, whereas our definition of ballot secrecy
%detects such attacks. Nonetheless,
and it remains to \sout{consider whether our definition
truly captures ballot secrecy (whatever it might be)}\textcolor{red}{establish
confidence in our definition}. This might be achieved by
\end{comment}
Confidence in our ballot secrecy definition might be improved by proving equivalence
with a simulation-based definition of ballot secrecy. However, it is unclear how to
formulate a suitable simulation-based definition. Bernhard \emph{et al.}
propose an ideal functionality that ``collects all votes from the voters, then
computes and announces the [election outcome]''~\cite[\S1]{BCGPW15},%
%KEEP FOOTNOTE IN SUBMISSION (it notes that stronger definitions exist)
\ifnocompress\footnote{In the context of voting systems that announce
the chosen representative (rather than the frequency distribution of votes),
a stronger ideal functionality might announce the chosen representative.}\fi\
but a voting system satisfying ballot secrecy need not be equivalent, because
ballot secrecy does not guarantee correct computation of the election outcome.
Equivalence can perhaps be shown between their ideal functionality and voting
systems satisfying ballot secrecy and some soundness condition (e.g.,
$\StrongTallySoundness$). Albeit, voting systems that bound the number of
ballots or candidates, e.g., Helios, may not be equivalent, because soundness
conditions (such as $\StrongTallySoundness$) need only provide guarantees when
operating within the aforementioned bounds. Thus, bounds need to be taken into
consideration. Moreover, no voting system is equivalent to the ideal functionality
by Bernhard \emph{et al.} in the presence of an adversary that controls the bulletin
board, because such an adversary can discard ballots, which creates a trivial
distinction.\ifanon\ (\else\footnote{\fi%
The real functionality by Bernhard \emph{et al.}
does not capture adversaries that control ballot collection.
Thus, the relation they prove between their game-based and
simulation-based definitions of ballot secrecy does not preclude vulnerabilities
exploitable by such adversaries. %This further highlights the difficulties of formulating
%an appropriate simulation-based definition of ballot secrecy.
Indeed, proving such relations %between game-based and simulation-based definitions
does not guarantee the absence of vulnerabilities.%
\ifanon)\else}\fi\
Nonetheless, equivalence can perhaps be shown for verifiable voting
systems in cases where the number of ballots and candidates are bounded, and all
voters successfully verify the presence of their ballot, but such a result has no
practical relevance, because it is well-known that many voters do not perform
checks necessary for verifiability~\cite[\S2.1.6]{Ryan17:sok-voting-challenges}.
Alternatively, the ideal functionality could be weakened such that a discarded
ballot in the real functionality corresponds to a discarded vote in the ideal
functionality. We leave further exploration of simulation-based definitions of
ballot secrecy as a possible extension for future work.
\ifconf\else
%\ifnocompress
Bulens, Giry \& Pereira pose the investigation of voting systems
which allow casting of meaningfully related ballots
as a means for voters to delegate candidate selection,
whilst preserving
ballot secrecy, as an interesting research question~\cite[\S3.2]{Pereira11:HeliosMixnet}.
Desmedt \& Chaidos claim to provide such a system~\cite{Desmedt12:Helios}.
Smyth \& Bernhard critique their work and argue that the security results
do not support their claims~\cite[\S5.1]{2013:BallotIndependenceESORICS}.
We have shown that
%meaningfully related ballots and ballot secrecy are incompatible,
non-malleable ballots are necessary to satisfy $\BallotSecrecy$ (\S\ref{sec:rel}),
providing a negative result for the question posed by Bulens, Giry \& Pereira.
\fi
\ifconf\else
\ifanon
Some of the ideas presented in this paper previously appeared in
technical reports (citations omitted for anonymity).
In particular, variants of Definition~\ref{def:ballotSecrecy} were considered
using syntax by Smyth \& Bernhard~\cite{2014:BallotIndependenceEprint,2013:BallotIndependenceESORICS}.
By comparison, this paper adopts
syntax from Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}.
\else
Some of the ideas presented in this \manuscript\ previously appeared in
\iffalse a \else my \fi technical report\iffalse by Smyth\fi~\cite{2014-ballot-secrecy-a} and an
extended version of that technical report by Bernhard \& Smyth~\cite{2014-ballot-secrecy}.
%\marginpar{Note to reviewers: the technical report~\cite{2014-ballot-secrecy-a,2014-ballot-secrecy} will not be published.}
In particular, the limitations of ballot secrecy definitions by Bernhard
\emph{et al.} were identified
\iffalse by Smyth~\cite{2014-ballot-secrecy-a} \fi
and Definition~\ref{def:ballotSecrecy} is based upon
\iffalse the definition of ballot secrecy proposed by
Smyth~\cite[Definition~3]{2014-ballot-secrecy-a} \else
my earlier definition~\cite{2014-ballot-secrecy-a}.
The main distinction between
Definition~\ref{def:ballotSecrecy} and the earlier definition~\cite[Definition~3]{2014-ballot-secrecy-a} is syntax: This
\manuscript\ adopts syntax for election schemes from Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability},
whereas the earlier definition adopts syntax by Smyth \& Bernhard~\cite{2014:BallotIndependenceEprint,2013:BallotIndependenceESORICS}.
\fi
The change in syntax is motivated by the superiority of syntax by
Smyth, Frink \& Clarkson.
\begin{comment}
Unfortunately, the change has a drawback:
we cannot immediately prove that
\ifanon
Definition~\ref{def:ballotSecrecy}
\else
the definition of ballot secrecy proposed in this \manuscript\
\fi
is strictly stronger than the definition proposed by
Smyth \& Bernhard~\cite{2014:BallotIndependenceEprint,2013:BallotIndependenceESORICS}.
By comparison, the technical reports contain such proofs.
Nevertheless, the advantages of the syntax change outweigh the disadvantages.
\end{comment}
Moreover, we can capitalise upon results by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}
and Quaglia \& Smyth~\cite{Smyth15:Hawk}.
\fi
Following the initial release of these results\ifanon\ (citations omitted for anonymity)\else~\cite{Smyth15:BallotSecrecyOrig,Smyth15:BallotSecrecyHeliosProof}\fi,
Cortier \emph{et al.} \cite{Cortier17:HeliosMachineChecked}
presented a machine-checked proof that variants of Helios
satisfy the notion of ballot secrecy by Bernhard
\emph{et al.}~\cite{BCGPW15}.
As discussed above, that notion is too weak%: it is vacously satisfied
%by schemes without tallying proofs and problems exist
%for schemes with proofs too (Appendix~\ref{app:BPRIV}),
%and
%. In particular,
%vulnerabilities that require control of ballot
%collection are not detected.
: It \ifBPRIV omits attacks (Appendix~\ref{app:BPRIV}) and \else cannot detect
vulnerabilities that require control of ballot collection.
Thus, our proof is more appropriate.
Nonetheless, their proof builds upon similar ideas.
In particular, their proof is dependent upon
non-malleable ballots and zero-knowledge tallying proofs.
Further to their earlier work~\cite{Smyth15:NM-CPA-ciphertexts}, Smyth \& Hanatani consider \heliosnext\ ballots
as non-malleable ciphertexts and build upon this \manuscript\ to further simplify ballot-secrecy
proofs~\cite{2018-ballot-secrecy-from-NM-CPA}, with proof in just two pages, compared to the five pages
used here.
\ifconf\else
Quaglia \& Smyth~\cite{Smyth18:HeliosC} extend game $\BallotSecrecy$
to syntax with voter credentials~\cite[Definition~6]{Smyth15:ElectionVerifiability}.
Moreover, they define a transformation to that syntax from our syntax (Definition~\ref{def:election})
and prove that their transformation
preserves secrecy and verifiability. Furthermore, they apply their transformation to
Helios. The resulting scheme is similar Helios-C~\cite{Cortier14:verifiability}, albeit
Quaglia \& Smyth observe Helios-C does not satisfy ballot secrecy when the adversary
controls ballot collection, whereas the scheme derived by applying their transformation
does.
\fi
\fi
\ifconf\else
%\ifnocompress
Beyond the computational model of security, Delaune, Kremer \& Ryan
formulate a definition of ballot secrecy in the
applied pi calculus~\cite{DKR06,DKR08} and Smyth~\emph{et al.} show that
this definition is amenable to automated reasoning~\cite{Smyth08:Obs,Smyth10:ObsA,Smyth10:thesis,2016-verifying-observational-equivalence,2017-verifying-observational-equivalence}. An alternative definition is proposed by
Cremers \& Hirschi, along with sufficient conditions which are
also amenable to automated reasoning~\cite{Hirschi17:SufficientConditionsSecrecyDKR}.
Scope of automated reasoning is limited by analysis tools
(e.g., ProVerif~\cite{2010-ProVerif-manual-version-1.96}), e.g., because function symbols and equational theory
might be unsuitable for automated analysis (cf.~\cite{DKR11:TPM-Horn-clauses,BlanchetPaiola12:EQ-lists,Bursuc12:EQ-reenc}).
%\fi
\fi
\ifev
\subsection{Further notions of privacy}
\fi
\label{sec:secrecy:outlook}
\label{sec:related:outlook}
\ifrfdef\else
\begin{comment}
Ballot secrecy formalises a notion of free-choice assuming the adversary's
capabilities are limited to controlling the bulletin board
and assuming ballots are constructed in the prescribed manner.
\end{comment}
Ballot secrecy formalises a notion of free-choice assuming ballots are
constructed and tallied in the prescribed manner. Moreover,
\ifev Smyth's definition assumes \else our definition of ballot secrecy assumes \fi
the adversary's capabilities are limited to
casting ballots on behalf of some voters and controlling the
votes cast by any remaining voters.
We have seen that
\ifev
voting system $\encToVoteSymb$ satisfies this definition%
\else
\heliosnext\ satisfies our definition%
\fi, but ballot
secrecy does not ensure free-choice when an adversary is able to
communicate with voters nor when voters deviate from the prescribed
voting procedure to follow instructions provided by an adversary.
Indeed, the coins used for encryption serve as proof of how a voter voted
in \ifev $\encToVoteSymb$ \else Helios \fi
and the voter may communicate those coins to the adversary.
Stronger notions of free-choice, such as receipt-freeness~\cite{Moran06,Kiayias15,Cortier16:BeleniosRF} and coercion resistance~\cite{JCJ05,Gardner09:CoercionDefinition,Unruh10,Kusters12:CoercionResistance},
are needed in the presence of such adversaries.
\fi
\begin{comment}
A voting system that instructs voters to transmit their encrypted vote
satisfies ballot secrecy, assuming the adversary's capabilities are limited
to controlling ballot collection. But, free-choice can be compromised by a
more powerful adversary that is able to communicate with the voter. Indeed,
the coins used for encryption serve as proof of how the voter voted and the
voter may communicate those coins to the adversary. Receipt-freeness formalises
a notion of free-choice in the presence of such communication.
\end{comment}
Our formalisation of ballot secrecy captures a notion of free-choice assuming voters' construct ballots as prescribed
and keyholders tally ballots as prescribed, with adversary capabilities limited to casting ballots on behalf of some voters
and controlling votes cast by any remaining voters.
We have seen
\ifev
voting system $\encToVoteSymb$ satisfies this definition%
\else
\heliosnext\ satisfies our definition%
\fi, but ballot
secrecy does not ensure free-choice when an adversary is able to
communicate with voters, nor when voters deviate from the prescribed
voting procedure to follow instructions provided by an adversary.
Indeed, the coins used for encryption serve as proof of how a voter voted
in \ifev $\encToVoteSymb$ \else Helios \fi
and the voter may communicate those coins to the adversary.
Stronger notions of free-choice, such as receipt-freeness\ifconf\else~\cite{DKR06,Moran06,Kiayias15,Cortier16:BeleniosRF,Smyth19:receipt-freeness}\fi\ and coercion resistance\ifconf\else~\cite{JCJ05,Gardner09:CoercionDefinition,Unruh10,Kusters12:CoercionResistance,2019-surveying-coercion-resistance}\fi,
are needed in the presence of such adversaries.\footnote{
\emph{Ballot secrecy} and \emph{privacy} occasionally appear as synonyms in the
literature. We favour ballot secrecy to avoid confusion with other privacy notions,
such as receipt-freeness and coercion resistance.
}
Appendix~\ref{app:rf} introduces
these notions, proves that our syntax cannot be used to construct (interesting)
schemes satisfying them, and discusses variants of our syntax that can.
\ifev\else\ifconf\else
McCarthy, Smyth \& Quaglia~\cite{2014-Hawk-and-Aucitas-auction-schemes}
have shown that auction schemes can be constructed from election schemes,
and Quaglia \& Smyth~\cite{Smyth15:Hawk} provide a generic construction
for auction schemes from election schemes. Quaglia \& Smyth also
adapt our definition of ballot secrecy to a definition of bid secrecy,
and prove that auction schemes produced by their construction satisfy bid secrecy.
(Similarly, they adapt the definition of \ifev election \fi verifiability by
Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability} to a
definition of \ifev auction verifiability\else verifiability for auctions\fi, and prove that their construction
produces schemes satisfying \ifev auction \fi verifiability.) Thus, this research
has applications beyond voting.
\fi\fi
\else
\subsection{Ballot independence}\label{sec:independence}
Ballot independence~\cite{Gennaro95:Independence:SK-voting,Smyth12:Helios,Chor85:Independence}
is seemingly related to ballot secrecy.
\begin{itemize}
\item{\it Ballot independence.} Observing another voter's interaction with the voting system does
not allow a voter to cast a meaningfully related vote. %, i.e., ballots are non-malleable.
\end{itemize}
\noindent
Our informal definition essentially states that an adversary is unable to construct a ballot
meaningfully related to a non-adversarial ballot, i.e., ballots are non-malleable. Hence,
we can formalise ballot independence %using non-malleability, and
%we formalise non-malleability for election schemes
as a straightforward adaptation of
the non-malleability definition for asymmetric encryption by Bellare \& Sahai~\cite{Bellare99:IND-k-CPA}.\ifnocompress\footnote{%
Non-malleability was first formalised by Dolev, Dwork \& Naor in the context of asymmetric encryption~\cite{Dolev91:Nonmalleable,Dolev00:Nonmalleable};
the definition by Bellare \& Sahai builds
upon their results and results by Bellare \emph{et al.}~\cite{Bellare98:RelationsCryptoDefs}.}\fi\
Such a formalisation captures an intuitive notion of
ballot independence, but %the definition is
%that formalisation is
it is
complex and proofs of non-malleability are relatively
difficult. Bellare \& Sahai observe similar complexities and show that their definition is equivalent to
a simpler, indistinguishability notion. In a similar direction, we derive a %simpler,
%equivalent
definition of ballot independence,
called indistinguishability under chosen vote attack~($\BallotIndependence$),
as a straightforward adaptation of their indistinguishability notion for asymmetric
encryption.
\iftutorial
\sout{
We present formal definitions of ballot independence in Appendix~\ref{app:independence} and demonstrate relations between definitions of secrecy and independence.
In particular, we prove that ballot secrecy implies ballot independence, hence,
ballot independence is necessary, assuming ballot secrecy
is required.
We also prove the inverse implication for a class of voting systems
with zero-knowledge tallying proofs.
And show that the inverse implication does not hold in general,
hence, ballot secrecy is strictly stronger than ballot independence.
}
\fi
%\input{independence-nm}
%\subsubsection{Indistinguishability game\iflncs.\fi}
\label{sec:ind}
%
%We adapt an indistinguishability game for asymetric encryption by Bellare \& Sahai~\cite{Bellare99:IND-k-CPA}
%to derive a simpler, equivalent definition (Definition~\ref{def:ind-independence}) of ballot independence ($\BallotIndependenceNM$).
%
%We adapt an indistinguishability game for asymetric encryption by Bellare \& Sahai~\cite{Bellare99:IND-k-CPA}
%to derive a simpler, equivalent definition (Definition~\ref{def:ind-independence}) of ballot independence ($\BallotIndependenceNM$).
%
%We formalise ballot independence as an indistinguishability game, called
%indistinguishability under chosen vote attack~($\BallotIndependence$).
\iffalse
The game proceeds as follows.
First, the challenger computes a key pair $(\pk,\sk)$.
Secondly, the adversary is given the public key $\pk$ and must pick
two votes $v_0,v_1$. % and a number of candidates.
Thirdly, the challenger randomly selects a bit $\beta$ and constructs a challenge ballot for vote $v_\beta$.
Fourthly, the adversary must compute a bulletin board $\bb$.
Finally, the challenger tallies $\bb$ to reveal the election outcome $\outcome$
and the adversary must derive $\beta$ from the outcome.
The election scheme satisfies ballot independence if the adversary has less than a negligible
advantage over guessing bit $\beta$.
\fi
\begin{definition}[$\BallotIndependence$\ifev~\cite{Smyth15:BallotSecrecyFull}\fi]\label{def:ind-independence}
Let $\Gamma = (\SetupSymb,\VoteSymb,\TallySymb\ifev,\VerifySymb\fi)$ be
an election scheme, $\adv$ be an adversary, $\kk$ be the security parameter,
and $\BallotIndependence$ be the following game.
{\upshape
\begin{inlineexperiment}{$\BallotIndependenceGame$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup$\;
$(v_0,v_1,\nC) \leftarrow \adv(\pk,\kk)$\;
$\beta \leftarrow_R \{0,1\}$\;
$b \leftarrow \Vote[\pk,v_\beta,\nC,\kk]$\;
$\bb \leftarrow \adv(b)$\;
$(\outcome,\tpf) \leftarrow \Tally$\label{alg:BallotIndependenceGame:tally}\;
$g\leftarrow \adv(\outcome)$\;
\Return $g = \beta\mathrel\wedge\allowbreak
b\not\in\bb \mathrel\wedge\allowbreak 1 \leq v_0,v_1 \leq \nC \leq \mC \mathrel\wedge\allowbreak |\bb| \leq \mB$\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies \ifev $\BallotIndependence$\else
\emph{indistinguishability under chosen vote attack ($\BallotIndependence$)}\fi,
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\negl$, such that for all security parameters $\kk$,
we have $\Succ(\BallotIndependenceGame) \leq \frac{1}{2} + \neglK$.
\end{definition}
\iffalse
The adversary selects votes $v_0$ and $v_1$, and is given a challenge ballot \marginpar{Wordsmithing (left) desirable}
for vote $v_\beta$, where bit $\beta$ is chosen uniformly at random by the challenger.
The adversary computes a bulletin board, which should not contain the challenge
ballot. The challenger tallies the adversary's bulletin board to derive an election
outcome. The adversary wins by determining if $\beta=0$ or $\beta=1$, from the outcome.
Intuitively, if the adversary wins, then there exists a strategy to construct related ballots.
\fi
\begin{comment}
\noindent
Similarly to game $\BallotSecrecy$, game $\BallotIndependence$ capture
key generation using algorithm $\SetupSymb$, publication of the public
key, and only using the private key to compute the election outcome and tallying proof.
\end{comment}
Game $\BallotIndependence$ is satisfied if the adversary cannot determine whether
the challenge ballot $b$ is for one of two possible votes $v_0$ and $v_1$.
In addition to the challenge ballot, the adversary is given the election
outcome derived by tallying a bulletin board computed by the adversary.
%The adversary is permitted to construct a bulletin board, which should
%not contain the challenge ballot. The challenger tallies the adversary's bulletin
%board to derive an election outcome. And the election outcome is given to the
%challenger.
To avoid trivial distinctions, the adversary's bulletin board
should not contain the challenge ballot.
Intuitively, the adversary wins if there exists a
strategy to construct related ballots, since this strategy enables the
adversary to construct a ballot $b'$, related to the challenge ballot $b$,
and determine if $b$ is for $v_0$ or $v_1$ from the outcome derived by
tallying a bulletin board containing $b'$.
\ifieee
\else
\paragraph{Comparing $\BallotIndependence$ and $\INDPA$}
\fi
The main distinction between indistinguishability for asymmetric
encryption ($\INDPA$)\ifconf~\cite{Bellare99:IND-k-CPA}\fi\
and indistinguishability for election schemes ($\BallotIndependence$)
is as follows: $\INDPA$ performs a parallel decryption, whereas $\BallotIndependence$ performs
a single tally.
Hence, indistinguishability for encryption reveals
plaintexts corresponding to ciphertexts, whereas indistinguishability for elections
reveals the number of votes for each candidate.\ifieee\else \\ \fi
\ifieee\else\noindent\fi
We present an alternative definition of ballot independence (Appendix~\ref{sec:nm}), based upon the
definition of non-malleability for asymmetric encryption by Bellare \& Sahai,
and prove that the definition is equivalent to
$\BallotIndependence$.
\subsection{Secrecy and independence coincide (for zero-knowledge tallying proofs)}
\label{sec:rel}
\label{sec:relation} %% necessary section
\label{sec}\label{sec:sufficient} %% sufficient section
%\subsection{Secrecy is strictly stronger}
The main distinctions between our ballot secrecy ($\BallotSecrecy$) and ballot independence ($\BallotIndependence$) games are as follows.
%
\begin{enumerate}
\item The challenger produces one challenge ballot for the adversary in game $\BallotIndependence$,
whereas the left-right oracle produces arbitrarily many challenge
ballots for the adversary in game $\BallotSecrecy$.
\end{enumerate}
%
%TRUTHIFY: These two formulations are similar and a hybrid argument will show that it does not matter if we give the \textcolor{blue}{ballot independence} adversary one challenge ballot or many challenge ballots.
%
\begin{enumerate}\setcounter{enumi}{1}
\item The adversary in game $\BallotSecrecy$
has access to a tallying proof, but the adversary in game $\BallotIndependence$
does not.
\end{enumerate}
%
\begin{enumerate}\setcounter{enumi}{2}
\item The winning condition in game $\BallotSecrecy$
requires the bulletin board to be
balanced, whereas the bulletin board must not contain the challenge ballot in
game $\BallotIndependence$.
\end{enumerate}
%
The second point distinguishes our games and shows $\BallotSecrecy$ is at
least as strong as $\BallotIndependence$. %\footnote{%
%Smyth \& Bernhard explain that alternative formalisations of election schemes
%might permit different results~\cite[\S5.2]{2013:BallotIndependenceESORICS}.}
Hence, non-malleable ballots are necessary in election schemes satisfying
$\BallotSecrecy$. \ifnmnecessary\else(Non-malleable ballots are not generally
necessary: Privacy definitions are sound but incomplete,
Section~\ref{sec:discussion}.)\fi
\begin{theorem}[$\BallotSecrecy \Rightarrow \BallotIndependence$]\label{thm:relation}
Given an election scheme $\Gamma$ satisfying $\BallotSecrecy$,
we have $\Gamma$ satisfies $\BallotIndependence$.
\end{theorem}
\noindent
A proof of Theorem~\ref{thm:relation} and all further proofs,
except where otherwise stated, appear in \refappendix{\ref{app:proofs}}.
Tallying proofs may reveal voters' votes. For example, a variant of $\encToVoteSymb$
might define tallying proofs that map ballots to votes. Since proofs are available
to the adversary in game $\BallotSecrecy$, but not in
game $\BallotIndependence$, it follows that $\BallotSecrecy$ is strictly stronger than
$\BallotIndependence$.
\begin{proposition}[$\BallotIndependence \not\Rightarrow \BallotSecrecy$]\label{prop:strictlyStronger}
%There exists an election scheme satisfying $\BallotIndependence$, but not $\BallotSecrecy$.
%
%%JCS Reviewer 2 remarked that the above assumes the existence of a secure public key encryption, so
%%weaken as:
%
An election scheme may satisfy $\BallotIndependence$, but not $\BallotSecrecy$.
\end{proposition}
\noindent Proposition~\ref{prop:strictlyStronger} follows from our
informal reasoning and we omit a formal proof.
%\subsection{Equivalence, without tallying proofs}
Game $\BallotSecrecy$ is generally (strictly) stronger than
game $\BallotIndependence$.
Nonetheless, we show that our games coincide for %the class of
election schemes without tallying proofs (Definition~\ref{def:withoutProofs}),
assuming %\sout{a soundness condition}
tallying is additive (Definition~\ref{def:soundness}),
%\sout{which asserts that adding a ballot for vote $v$ to a bulletin board
%(computed by an adversary), effects the election outcome by exactly vote $v$,
%hence, honestly constructed ballots are tallied correctly.}
that is, the sum of election outcomes derived by tallying distinct subsets of a
bulletin board is equivalent to the election outcome derived by
tallying the union of those subsets.
\begin{definition}\label{def:withoutProofs}
An election scheme $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$
is \emph{without tallying proofs}, if there exists a constant symbol $\epsilon$
such that for all private keys $\sk$, sets $\bb$, integers $\nC$, security
parameters $\kk$, and computations $(\outcome,\allowbreak \tpf) \leftarrow\allowbreak \Tally$,
we have $\tpf = {\epsilon}$.
\end{definition}
\newcommand{\outcomeDefault}{}
\begin{definition}[$\TallySoundness$]\label{def:soundness}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb\ifev,\allowbreak\VerifySymb\fi)$ be an election
scheme, $\adv$ be an adversary, $\kk$ be a security parameter, and
$\TallySoundness$ be the following game.
{\upshape
\begin{inlineexperiment}{$\TallySoundnessGame$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup[\kk]$\;
$(\nC,\bb,\bb') \leftarrow \adv(\pk,\kk)$\;
$(\outcome, \tpf) \leftarrow \Tally[\sk,\bb,\nC,\kk]$\;
$(\outcome_0, \tpf_0) \leftarrow \Tally[\sk,\bb\setminus\bb',\nC,\kk]$\;
$(\outcome_1, \tpf_1) \leftarrow \Tally[\sk,\bb\cap\bb',\nC,\kk]$\;
\Return $\outcome = \outcome_0+\outcome_1 \wedge\allowbreak \nC\leq \mC \wedge\allowbreak |\bb| \leq \mB$\;
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies $\TallySoundness$, if
for all probabilistic polynomial-time adversaries $\adv$, there exists a negligible
function $\negl$, such that for all security parameters $\kk$,
we have $\Succ(\TallySoundnessGame) > 1- \neglK$.
\end{definition}
\begin{comment}
When bounds on the maximum number of ballots and candidates are exceeded,
honest-ballot tally soundness asserts that adding a ballot
board effects the election outcome deterministically:
the election outcome is some function $\overflowOutcomeSymb$ of the outcome effected by exactly
vote $v$. For example, given an outcome $\outcome$ and vote $v\in\{1,\dots,|\outcome|\}$
such that $\outcome[v] > \mB$, we might have $f(\outcome)[v] = 0$. Thus,
honest-ballot tally soundness tolerates overflows.
\end{comment}
%\subsubsection{No tallying proofs}
%\label{sec:sufficient:no-proof}
\begin{proposition}[$\BallotSecrecy = \BallotIndependence$, without proofs]\label{proppp}
Let $\Gamma$ be an election scheme without tallying proofs.
Suppose $\Gamma$ satisfies $\TallySoundness$.
We have $\Gamma$ satisfies $\BallotSecrecy$ iff $\Gamma$ satisfies $\BallotIndependence$.
\end{proposition}
%\subsection{Equivalence, with zero-knowledge tallying proofs}
Our equivalence result generalises to %the class of
election schemes with \emph{zero-knowledge tallying proofs}
(Definition~\ref{def:zkTallying}), i.e., schemes that compute proofs using
non-interactive zero-knowledge proof systems.
%%As defined below, we don't know if proofs output by \ProveSymb((\pk,\bb,\nC,\outcome),w,\kk;r)
%%are indistinguishable from those output by the simulator, because $r$ isn't chosen
%%uniformly at random.
%
\begin{comment}
\begin{definition}[Zero-knowledge tallying proofs]\label{def:zkTallying}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\TallySymb)$ be an election
scheme. We say $\Gamma$ has \emph{zero-knowledge tallying proofs},
if there exists a zero-knowledge non-interactive proof system $(\ProveSymb, \VerifySymb)$ and
for all probabilistic polynomial-time adversaries $\adv$ and security parameters $\kk$, we have:\\
{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kk]$;\\
\begin{algorithm}[H]
$(\nC,\bb) \leftarrow \adv(\pk,\kk)$\;
$(\outcome,\tpf) \leftarrow \Tally{\bb,\nC, \kk}:$\\
$|\bb| \leq \mB \wedge \nC\leq \mC\Rightarrow \exists w,r \mathrel . \ProveSymb((\pk,\bb,\nC,\outcome),w,\kk;r) = \tpf] = 1$.
\end{algorithm}
}
\end{definition}
\end{comment}
\begin{theorem}[$\BallotSecrecy = \BallotIndependence$, with ZK proofs]\label{thm:equivalent}
Let $\Gamma$ be an election scheme with zero-knowledge tallying proofs.
Suppose $\Gamma$ satisfies $\TallySoundness$. We have
$\Gamma$ satisfies $\BallotSecrecy$ iff $\Gamma$ satisfies $\BallotIndependence$.
\end{theorem}
\begin{proof}[Proof sketch]
Game $\BallotSecrecy$ computes the election outcome from ballots constructed by the
oracle and ballots constructed by the adversary. Intuitively, such an outcome can be
equivalently computed as follows:
{\upshape
\begingroup\removelatexerror
\begin{algorithm}[H]
$(\outcome, \tpf)\leftarrow \Tally[\sk,\bb\setminus\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
$(\outcome', \tpf')\leftarrow \Tally[\sk,\bb\cap\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
$\outcome \leftarrow \outcome + \outcome'$\;
\end{algorithm}
\endgroup
}
\noindent
Yet, a poorly designed tallying algorithm might not ensure equivalence. In particular,
ballots constructed by the adversary can cause the algorithm to behave unexpectedly.
(Such algorithms are nonetheless compatible with our correctness requirement, because
correctness does not consider an adversary.) Our $\TallySoundness$
property ensures equivalence. Moreover, our $\TallySoundness$ property ensures
the above computation is equivalent to the following:
{\upshape
\begingroup\removelatexerror
\begin{algorithm}[H]
$(\outcome, \tpf)\leftarrow \Tally[\sk,\bb\setminus\{b \mid (b,v_0,v_1)\in L\},\nC,\kappa]$\;
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$(\outcome', \tpf')\leftarrow \Tally[\sk,\{b\},\nC,\kappa]$\;
$\outcome \leftarrow \outcome + \outcome'$\;
}
\end{algorithm}
\endgroup
}
\noindent
Furthermore, by correctness of the election scheme, the above for-loop
can be equivalently computed as follows:
{\upshape
\begingroup\removelatexerror
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_\beta] \leftarrow \outcome [v_\beta] +1$\;
}
\end{algorithm}
\endgroup
}
\noindent
Indeed, for each $b \in \bb \wedge (b,v_0,v_1) \in L$, we have $b$ is an output of
$\Vote[\pk,\allowbreak v_\beta,\allowbreak\nC,\allowbreak\kk]$, hence,
$\Tally[\sk,\{b\},\nC,\kappa]$ outputs $(\outcome, \tpf)$ such that $\outcome$
is a zero-filled vector, except for index $v_\beta$ which contains one,
and this suffices to ensure equivalence. In addition, for any adversary that wins
game $\BallotSecrecy$, we are assured that $\balanced(\bb,\nC,L)$ holds, hence,
the above for-loop can be computed as
{\upshape
\begingroup\removelatexerror
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_0] \leftarrow \outcome [v_0] +1$\;
}
\end{algorithm}
\endgroup
}
\noindent
or
{\upshape
\begingroup\removelatexerror
\begin{algorithm}[H]
\For{$b \in \bb \wedge (b,v_0,v_1) \in L$}{
$\outcome [v_1] \leftarrow \outcome [v_1] +1$\;
}
\end{algorithm}
\endgroup
}
\noindent
without weakening the game. Thus, perhaps surprisingly, tallying ballots constructed
by the oracle does not
provide the adversary with an advantage (in determining whether $\beta = 0$ or
$\beta = 1$) and we can omit such ballots from tallying in game $\BallotSecrecy$.
Thus, game $\BallotSecrecy$ is equivalent to game $\BS$ (Definition~\ref{def:BS}), which modifies the tallying
procedure as described and simulates tallying proofs. Thereafter, we proceed with
a hybrid argument (for which Shoup presents a brief tutorial~\cite{Shoup04:HybridArgument}).
\end{proof}
\noindent
Additivity is implied by universal verifiability %\ifappendix\
(Lemmata~\ref{lem:TallySoundnessStrongerHBTallySoundness} \&~\ref{lem:uvImpliesSoundness}). %\else~\cite{tr}\fi.
Thus, a special case of
Theorem~\ref{thm:equivalent} requires the election scheme to satisfy universal
verifiability, which is useful to simplify its application.
Indeed, we exploit this result in the following
section to prove $\BallotSecrecy$.
\ifnmnecessary
\subsection{I was wrong: Non-malleable ballots are necessary for secrecy}
Should secrecy be preserved when ballots are suppressed? \emph{Bien s\^ur}!
It follows that non-malleable ballots are necessary. In an earlier version of this work,
I argued the contrary~\cite[\S{}7]{Smyth15:BallotSecrecyJCS}, I was wrong:
Tallying a meaningfully related ballot, rather than multiple related ballots,
suffices to violate secrecy. Indeed, in the extreme, secrecy is violated by
an adversary suppressing all ballots except one relating to their victim's,
who believes they didn't even cast a ballot.
\fi
%
```
[^1]: Earlier systems permitted non-uniform ballots, even vibrantly coloured party tickets in a variety of sizes (**Brent06:AustralianBallot?**).