# Authentication with weaker trust assumptions for voting systems
Elizabeth A. Quaglia, Ben Smyth
## Abstract
Some voting systems are reliant on external authentication services. Others use cryptography to implement their own. We combine digital signatures and non-interactive proofs to derive a generic construction for voting systems with their own authentication mechanisms, from systems that rely on external authentication services. We prove that our construction produces systems satisfying ballot secrecy and election verifiability, assuming the underlying voting system does. Moreover, we observe that works based on similar ideas provide neither ballot secrecy nor election verifiability. Finally, we demonstrate applicability of our results by applying our construction to the Helios voting system.
# Introduction
An election is a decision-making procedure to choose representatives (**Lijphart84?**; **Saalfeld95?**; **Gumbel05:StealThisVote?**; **Alvarez10:ElectronicElections?**). Choices should be made freely by voters with equal influence, and this must be ensured by voting systems (**UN:HumanRights?**; **OSCE:HumanRights?**; **OAS:HumanRights?**). Some voting systems rely on *external* authentication services to ensure choices are made by voters. E.g., Helios (**AdidaPereiraMarneffeQuisquater?**; **Olivier16:Helios?**) supports authentication via Facebook, Google and Yahoo using OAuth. Other voting systems use cryptography to implement their own authentication mechanisms. E.g., the voting system by Juels, Catalano & Jakobsson uses a combination of encrypted nonces and plaintext equality tests for authentication (**JCJ10?**). We combine digital signatures and non-interactive proofs to derive a construction for voting systems with their own authentication mechanisms from systems that rely on external service providers. Our construction produces voting systems which require less trust, since systems built upon cryptography are typically preferable to systems trusting external service providers.
Many voting systems rely on art, rather than science, to ensure that choices are made freely by voters with equal influence. Such systems build upon creativity and skill, rather than scientific foundations, and are typically broken in ways that compromise free choice, e.g., (**Rop07:NetherlandsVoting?**; **Halderman10:IndiaVoting?**; **Halderman12:DCVoting?**; **Halderman14:EstoniaVoting?**; **DebraBowenCalifornia07?**), or permit adversaries to unduly influence the outcome, e.g., (**JonesSimons12:VotingBook?**; **GermanyCourt09?**; **DebraBowenCalifornia07?**; **ElectoralCommision07?**). By contrast, we prove that our construction produces voting systems that satisfy rigorous and precise security definitions of ballot secrecy and election verifiability that capture voters voting freely with equal influence.[^1]
We demonstrate applicability of our construction by deriving voting systems with their own authentication mechanisms from Helios. Moreover, we compare those systems to Helios-C (**Cortier14:verifiability?**; **Cortier14:verifiabilityTech?**), a variant of Helios for two-candidate elections in which ballots are digitally signed. Our comparison reveals some subtle distinctions and we show that Helios-C does not satisfy our security definition, whereas our construction produces voting systems that do.
#### Structure.
Section [sec:syntax] recalls election scheme syntax. Section [sec:construction] presents our construction. Section [sec:secrecy] proves that our construction produces systems satisfying ballot secrecy. Section [sec:verifiability] proves that election verifiability is also satisfied. Section [sec:example] demonstrates the application of our construction to the Helios voting system and compares the resulting systems to Helios-C. We conclude in Section [sec:conclusion].
Appendix [app:crypto] presents cryptographic primitives and associated security definitions, and the remaining appendices recall security definitions for voting systems and present proofs. technical report (**tr?**).
# Election scheme syntax
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 187, column 1): unexpected } expecting \end{document} } ^`
``` latex
\section{Election scheme syntax}\label{sec:syntax}
We recall syntax by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}
for a class of voting systems that consist of the following four steps.
First, a tallier\footnote{Some voting systems permit the tallier's role to be distributed amongst several talliers. For simplicity, we consider only a single tallier in this paper.} generates a key pair and (optionally) a registrar generates credentials for voters.
Secondly, each voter constructs and casts a ballot for their vote.
These ballots are recorded on a bulletin board.
Thirdly, the tallier
tallies the recorded ballots and
announces an outcome, i.e., a frequency distribution of votes.
Finally, voters and other interested parties check that
the outcome corresponds to votes expressed in recorded ballots.\iftr \footnote{Smyth, Frink \&
Clarkson use the syntax to model first-past-the-post voting systems and Smyth shows
ranked-choice voting systems can be modelled too~\cite{2017-FPTP-suffices-for-ranked-voting}.}\fi
\begin{definition}[Election scheme~\cite{Smyth15:ElectionVerifiability}] %\label{def:election}
An \emph{election scheme with external authentication} is a tuple of efficient algorithms
$(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$ and
an \emph{election scheme with internal authentication} is a tuple of efficient algorithms
$(\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$,
such that:\footnote{Let $A(x_1,\dots,x_n; r)$ denote the output of probabilistic algorithm $A$ on inputs $x_1,\dots,x_n$ and random coins $r$.
Let $A(x_1,\dots,x_n)$ denote $A(x_1,\dots,x_n;r)$, where $r$ is chosen uniformly at random.
And let $\leftarrow$ denote assignment. Moreover, let $\langle x \rangle$ denote an optional input and $\outcome[v]$ denote component $v$ of vector $\outcome$.}
\begin{description}
\item $\SetupSymb$, denoted $(\pk,\sk,\mB,\mC) \leftarrow \SetupSymb(\kappa)$, is run by the tallier.
$\SetupSymb$ takes a security parameter $\kappa$ as input and outputs a key pair
$\pk,\sk$, a maximum number of ballots $\mB$,
and a maximum number of candidates $\mC$.
\item $\RegisterSymb$, denoted $(\pd,\sd) \leftarrow \Register[\pk,\kappa]$, is run by the registrar.
It takes as input the public key $\pk$ of the tallier %, the proof $Q$ of correct key pair construction,
and a security parameter $\kappa$, and it outputs a \emph{credential pair} $(\pd,\sd)$,
where $\pd$ is a public credential and $\sd$ is a private credential.
\item $\VoteSymb$, denoted $b\leftarrow\Vote[\langle\sd\rangle,\pk,\nC]{v,\kappa}$, is run by voters. $\VoteSymb$ takes as input a private credential $\sd$ (optional), a
public key $\pk$, some number of candidates
$\nC$, a voter's vote $v$, and a security parameter $\kappa$.
The vote should be selected from a sequence $1,\dots,\nC$ of
candidates.
$\VoteSymb$ outputs a ballot $b$ or error symbol $\perp$.
\item $\TallySymb$, denoted $(\outcome, \tpf)\leftarrow\TallySymb(\sk, \nC, \bb,\langle\electoralroll\rangle,\kappa)$, is run by the tallier.
$\TallySymb$ takes as input a private key $\sk$, some number
of candidates $\nC$, a bulletin board $\bb$,
an electoral roll $\electoralroll$ (optional),
and a security parameter $\kappa$,
where $\bb$ is a set. It
outputs an election outcome $\outcome$ and a non-interactive proof $\tpf$ that
the outcome is correct.
An election outcome is a vector $\outcome$ of length $\nC$ such that
$\outcome[v]$
indicates the number of votes for candidate $v$.
\item $\VerSymb$, denoted $s \leftarrow \VerSymb(\pk,\nC, \bb,\langle\electoralroll\rangle, \outcome, \tpf, \kappa)$, is run to audit an election.
It takes as input a public key $\pk$,
some number of candidates $\nC$,
a bulletin board $\bb$,
an electoral roll $\electoralroll$ (optional),
an election outcome $\outcome$,
a proof $\tpf$, and a security parameter $\kappa$.
It outputs a bit $s$, which is $1$
if the election verifies successfully
and $0$ otherwise.
\end{description}
\noindent
Election schemes with internal authentication must always use optional inputs,
whereas election schemes with external authentication must not. Both schemes
must satisfy \emph{correctness}:
there exists a negligible function $\mathsf{negl}$,
such that for all security parameters $\kappa$,
integers $\nB$ and $\nC$, and
votes $v_1,\allowbreak\dots,\allowbreak{}v_{\nB}\allowbreak\in\allowbreak\{1,\allowbreak\dots,\allowbreak\nC\}$, it holds that
if $\outcome$ is a vector of length $\nC$ whose components are all $0$, then\\
{\upshape
\begin{inlineprobability}{$\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$}
\For{$1 \leq i \leq \nB$}{
$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$;\\
$b_i \leftarrow \Vote[\langle\sd_i\rangle,\pk,\nC]{v_i,\kappa}$;\\
$\outcome[v_i] \leftarrow \outcome[v_i] + 1$;
}
$(\outcome',\tpf) \leftarrow \Tally[\sk,\nC,\{b_1,\dots,b_{\nB}\}]{\langle\{\pd_1,\dots,\pd_{\nB}\}\rangle,\kappa}$ \\
$\mathrel:\nB \leq \mB \wedge \nC\leq \mC\Rightarrow \outcome = \outcome'] > 1 - \mathsf{negl}(\kappa)$,
\end{inlineprobability}
}
\noindent
where algorithm $\RegisterSymb$ is only applied for election scheme with internal authentication
and optional inputs are only used for election scheme with internal authentication.
\end{definition}
%\textcolor{blue}{Correctness for election schemes with internal authentication \sout{implicitly} captures that all authorized votes (i.e., votes associated to an honestly generated credential pair) are included in the election outcome. BEN: Correctness captures that all votes used to construct ballots are included in the election outcome. }
\begin{comment}
\textcolor{blue}{Election schemes must satisfy both privacy and verifiability properties. In particular, we consider \emph{ballot secrecy} as the \emph{de facto} (and intuitively straightforward) privacy requirement, and \emph{individual, universal} and \emph{eligibility verifiability} requirements in the context of verifiability.
Intuitively, individual verifiability challenges the adversary to
generate a collision from algorithm $\VoteSymb$, while universal verifiability challenges the adversary to concoct
a scenario in which either: $\VerSymb$ accepts, but the election outcome is not correct, or
$\TallySymb$ produces an election outcome that $\VerSymb$ rejects.
Hence, the formal definitions require algorithm $\VerSymb$ to accept if and only if
the election outcome is correct. And, finally, eligibility verifiability challenges an adversary, which can corrupt voters, to generate a valid ballot under an uncorrupted voter's private credential. Detailed definitions for the above properties are provided in the Appendix.}
\end{comment}
\begin{comment}
\ifnotes
\textcolor{red}{LIZ: I have a fundamental question here and perhaps it is worth a voice discussion. Where is \emph{authentication} captured as a security property? or as a functionality requirement? Only BS and V are discussed later and I am struggling to understand where authentication comes in and whether this is the right model.}
\textcolor{magenta}{BEN: No one has formalized eligibility/authentication in the computational model. I have formalized eligibility verifiability, but that's subtlety different. It requires some checks to be made. (Authentication is implicitly included as part of the correct definition, in particular, all votes must be included, i.e., authorized.)}
\fi
\end{comment}
```
# Our construction
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 130, column 17): expecting \end{document} \end{definition} ^`
``` latex
\section{Our construction}\label{sec:construction}
Election schemes with internal authentication can be derived from schemes
with external authentication using a digital signature scheme and a non-in\-ter\-ac\-tive
proof system: Each voter publishes
a ballot constructed using the underlying scheme with external authentication,
along with a signature on that ballot and a proof that they constructed both the ballot
and the signature.
Signatures and proofs are used to
ensure that each tallied vote was cast by an authorised voter.
Our construction is formal described in Definition~\ref{def:sig-proof}.
It is parameterised by an election scheme with external authentication,
a digital signature scheme, and a non-interactive proof system, derived from
an underlying sigma protocol and a hash function, using the Fiat-Shamir transformation.\footnote{Let $\sFS{\Sigma}{\mathcal H}$ denote the non-interactive proof system derived
by application of the Fiat-Shamir transformation to sigma protocol $\Sigma$
and hash function $\mathcal H$.}
Hence, we denote election schemes
derived using our construction as $\Trans(\Gamma,\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$,
where the underlying
election scheme, signature scheme, sigma protocol and hash function are $\Gamma$, $\Omega$, $\Sigma$
and $\mathcal H$, respectively.
To ensure our construction produces election schemes with
internal authentication, the non-interactive proof system must
be defined for a suitable relation, and we define such a relation
as follows.
\begin{definition}
Given an election scheme with external authentication $\Gamma =\allowbreak (\SetupSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$
and a digital signature scheme $\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$,
we define binary relation $R(\Gamma,\Omega)$ over vectors of
length $6$ and vectors of length $4$ such that
$((\pk,\allowbreak b,\allowbreak \sigma,\allowbreak\nC,\allowbreak\kappa),\allowbreak (v,\allowbreak r,\allowbreak \sd,\allowbreak r')) \allowbreak\in R(\Gamma,\Omega) \Leftrightarrow \allowbreak
b = \VoteSymb(\pk,\allowbreak \nC,\allowbreak v,\allowbreak \kappa;r) \wedge\allowbreak
\sigma = \SgnSymb_\Omega(\sd,\allowbreak b;\allowbreak r')$.
\end{definition}
\begin{definition}[Construction]\label{def:sig-proof}
Suppose $\Gamma = (\SetupSymb_\Gamma, \VoteSymb_\Gamma, \TallySymb_\Gamma, \VerifySymb_\Gamma)$ is an election scheme with external authentication, $\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$ is a digital signature scheme, $\Sigma$ is a sigma protocol for a binary relation $R(\Gamma,\Omega)$,
and $\mathcal H$ is a hash function.
Let $\sFS{\Sigma}{\mathcal H} = (\ProveSymb_\Sigma, \VerSymb_\Sigma)$.
We define $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$ such that:
\begin{itemize}
\item $\Setup[\kappa]$ computes $(\pk,\sk,\mB,\mC) \leftarrow \SetupSymb_\Gamma(\allowbreak{}\kappa)$ and outputs
$(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak\mC)$.
\item $\Register[\pk,\kappa]$ computes $(\pd,\sd)\leftarrow \GGenSymb_\Omega(\kappa)$ and outputs $(\pd,(\pd,\sd))$.
\item $\Vote[\sd',\pk,\nC]{v,\kappa}$ parses $\sd'$ as $(\pd,\sd)$ and outputs $\perp$ if parsing fails, selects coins $r$ and $r'$ uniformly at random, computes
{\upshape
\begin{algorithm}[H]
$b \leftarrow \VoteSymb_\Gamma(\pk,\allowbreak \nC,\allowbreak v,\allowbreak \kappa;r)$\;
$\sigma\leftarrow \SgnSymb_\Omega(\sd,\allowbreak b;\allowbreak r')$\;
$\tau\leftarrow\ProveSymb_\Sigma((\pk,b,\sigma,\nC,\kappa),(v,r,\sd,r'),\kappa)$,
\end{algorithm}
}
and outputs $(\pd,b,\sigma,\tau)$.
\item $\TallySymb(\sk, \nC, \bb,\electoralroll,\kappa)$ computes $(\outcome,\allowbreak \tpf) \leftarrow\allowbreak \TallySymb_\Gamma(\allowbreak\sk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak{}\nC,\allowbreak{}\kappa)$ and outputs $(\outcome,\allowbreak \tpf)$.
\item $\VerSymb(\pk,\nC, \bb,\electoralroll, \outcome, \tpf, \kappa)$ computes $s \leftarrow\allowbreak \VerifySymb_\Gamma(\allowbreak\pk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak\nC,\allowbreak\outcome,\allowbreak \tpf,\allowbreak \kappa)$ and outputs $s$.
\end{itemize}
Set $\mathsf{auth}(\bbb,\electoralroll) = \{ b \mid (\pd,\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\in \bbb \allowbreak\wedge\allowbreak
\VrfySymb_\Omega(\allowbreak \pd,\allowbreak b,\allowbreak \sigma) = 1 \allowbreak\wedge\allowbreak
\VerSymb_\Sigma((\pk,\allowbreak b,\allowbreak \nC,\allowbreak\kappa),\allowbreak\tau,\allowbreak\kappa) = 1 \allowbreak\wedge\allowbreak
\pd \in \electoralroll \wedge
(\pd,\allowbreak b',\allowbreak\sigma',\allowbreak\tau')\not\in \bbb \setminus\{(\pd,\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\} \allowbreak\wedge\allowbreak
\VrfySymb_\Omega(\allowbreak \pd,\allowbreak b',\allowbreak \sigma') = 1
\}$.
%
\end{definition}
Our construction uses function $\mathsf{auth}$ to ensure tallied ballots are authorised
and to discard ballots submitted under the same credential (i.e., if there is more than
one ballot submitted with a private credential, then all ballots submitted under that
credential are discarded). Since election schemes with internal authentication must
satisfy correctness, the underlying digital signature scheme must ensure that key pairs
are distinct. Hence, correctness of our construction depends on security of
the underlying digital signature scheme, albeit in a tedious manner.
Since we exploit %the security property of
\SufficientConditionOnSignatures\ of the signature scheme for results in the following sections, we assume the same property here (to ensure key pairs are distinct). Weaker conditions could be used for generality.
\begin{comment}
\textcolor{red}{BEN: This could probably be made clearer. Liz, can you try to understand
what I'm trying to say and make it clearer? Also, should we give reasons for assuming
\SufficientConditionOnSignatures? (Because we'll be using it elsewhere.)}
\end{comment}
\begin{lemma}\label{lem:construction:correct}
Let $\Gamma$ be an election scheme with external authentication,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a random oracle.
Suppose $\Omega$ satisfies \SufficientConditionOnSignatures.
We have $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ is an election scheme with
internal authentication.
\end{lemma}
\noindent The proof of Lemma~\ref{lem:construction:correct} appears in \iftr Appendix~\ref{app-proof-correctness}\else our companion technical report~\cite{tr}\fi.
```
# Our construction ensures ballot secrecy
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 167, column 17): expecting \end{document} \end{definition} ^`
``` latex
\section{Our construction ensures ballot secrecy}\label{sec:secrecy}
We adopt the definition of ballot secrecy for election schemes with external authentication
($\BallotSecrecy$) by Smyth~\cite{Smyth16:ballotSecrecy}. That definition appears to be the most
suitable in the literature, because it detects the largest class of attacks~\cite[\S7]{Smyth16:ballotSecrecy}. In particular, it detects attacks that arise when the adversary
controls the bulletin board or the communications channel, whereas other definitions, e.g.,
\cite{Smyth11:HeliosProvableSecure,Bernhard11:Helios,Bernhard12:Helios,2013:BallotIndependenceESORICS,Cortier13,Cortier13b,BCGPW15},
fail to detect such attacks. A definition of ballot secrecy for election schemes with
internal authentication ($\BallotSecrecyy$) can be derived from Smyth's definition by a
natural, straightforward extension that takes credentials into account. Both definitions are presented in Appendix~\ref{app:ballot-secrecy}. %, along with a proof of the following result.
The definition of ballot secrecy we recall challenges an adversary, who has access to the election outcome, to distinguish between ballots.
We can prove that our construction ensures ballot secrecy (a formal proof of Theorem~\ref{thm:privacy} appears in Appendix~\ref{app:ballot-secrecy}), assuming the underlying election scheme
satisfies ballot secrecy and the underlying sigma protocol satisfies \SufficientConditionOnSignaturesSigma.
\begin{theorem}\label{thm:privacy}
Let $\Gamma$ be an election scheme with external authentication,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a random oracle.
Suppose $\Gamma$ satisfies $\BallotSecrecy$,
$\Sigma$ satisfies \SufficientConditionOnSignaturesSigma, and
$\Omega$ satisfies \SufficientConditionOnSignatures.
Election scheme with internal authentication $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies $\BallotSecrecyy$.
\end{theorem}
\begin{proof}[Proof sketch]
Ballot secrecy of election scheme $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ follows from
secrecy of the underlying scheme $\Gamma$, because signatures and non-interactive
zero-knowledge proofs do not leak information. (\SufficientConditionOnSignaturesSigma[S]
\iftr suffice to \fi ensure proof system $\sFS{\Sigma}{\mathcal H}$ is zero-knowledge~\cite{Bernhard12:Helios}.)
\end{proof}
We demonstrate applicability of Theorem~\ref{thm:privacy} using a construction
for election schemes from asymmetric encryption.\iftr
\footnote{The construction was originally presented by Bernhard \emph{et al.}~\cite{Smyth11:HeliosProvableSecure,Bernhard11:Helios,2013:BallotIndependenceESORICS} in a slightly different setting.}%
\textsuperscript{,}\fi%
\footnote{We omit a formal definition of asymmetric encryption for brevity.}
\begin{definition}[$\mv$~\cite{Smyth15:auctions}]\label{def:mv}
Given a perfectly correct asymmetric encryption scheme $\Pi =
(\GGenSymb,\allowbreak\EEncSymb,\DDecSymb)$ satisfying $\INDCPA$,
election scheme with external authentication $\mv(\Pi)$ is defined as follows:
\begin{itemize}
\item $\Setup$ computes $(\pk,\sk)\leftarrow\GGen$ and outputs
$(\pk,\allowbreak\sk,\allowbreak\textit{poly}(\kappa),\allowbreak|\votespace|)$.
\item $\Vote{v,\kappa}$ computes $b\leftarrow\EEnc{v}$ and outputs $b$ if $1\leq v
\leq \nC \leq|\votespace|$ and $\perp$ otherwise.
\item $\TallySymb(\sk, \nC, \bb, \kappa)$ initialises vector $\outcome$ of length
$\nC$,
computes
{ \DontPrintSemicolon
\llFor{$b\in\bb$}{
$v\leftarrow\DDec{b};$
\llIf{$1\leq v\leq \nC$}{${\bf v}[v] \leftarrow {\bf v}[v]+1$}%
}%
}, and outputs
$(\outcome,\epsilon)$.
\item $\VerSymb(\pk,\nC, \bb, \outcome, \tpf, \kappa)$ outputs 1.
\end{itemize}
\noindent Algorithm $\SetupSymb$ requires $\textit{poly}$ to be a polynomial function,
algorithms $\SetupSymb$ and $\VoteSymb$ require $\mathfrak m = \{1,\dots,|\mathfrak m|\}$
to be the encryption scheme's plaintext space, and algorithm $\TallySymb$ requires $\epsilon$
to be a constant symbol.
\end{definition}
\noindent
Intuitively, given a non-malleable asymmetric encryption scheme $\Pi$,\footnotemark\
$\mv(\allowbreak\Pi)$ derives ballot secrecy from $\Pi$ until tallying and tallying
maintains ballot secrecy by returning only the number of votes for each candidate.
%A formal proof of ballot secrecy follows from
%Quaglia \& Smyth~\cite[Proposition 5 \& 16]{Smyth15:auctions}, as noted by Smyth~\cite[Corollary~2]{Smyth16:ballotSecrecy}.
\footnotetext{We adopt the formal definition of comparison based non-malleability under chosen
plaintext attack, which coincides with indistinguishability under a
parallel chosen-ciphertext attack ($\INDPA$)~\cite{Bellare99:IND-k-CPA}. We omit formal security
definitions for brevity.}
\begin{proposition}[\cite{Smyth15:auctions,Smyth16:ballotSecrecy}]
Let $\Pi$ be an encryption scheme with perfect correctness.
If $\Pi$ satisfies $\INDPA$, then election scheme with external authentication
$\mv(\Pi)$ satisfies $\BallotSecrecy$.
\end{proposition}
\noindent
Hence, by Theorem~\ref{thm:privacy}, we have the following result.
\begin{corollary}
Let $\Pi$ be an asymmetric encryption scheme with perfect correctness,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\mv(\Pi),\Omega)$,
and $\mathcal H$ be a random oracle.
Suppose $\Pi$ satisfies $\INDPA$,
$\Sigma$ satisfies \SufficientConditionOnSignaturesSigma,
and $\Omega$ satisfies \SufficientConditionOnSignatures.
Election scheme with internal authentication $\Trans(\mv(\Pi),\Omega,\Sigma,\mathcal H)$
satisfies $\BallotSecrecyy$.
\end{corollary}
\noindent
Clearly election scheme $\mv$ does not satisfy universal verifiability,
because it will accept any election outcome.
```
# Our construction ensures election verifiability
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 178, column 17): expecting \end{document} \end{definition} ^`
``` latex
\section{Our construction ensures election verifiability}\label{sec:verifiability}
We adopt definitions of individual ($\ExpIVSymb$) and universal ($\ExpUVSymb$) verifiability
for election schemes with external authentication from Smyth, Frink, \& Clarkson~\cite{Smyth15:ElectionVerifiability}.
We also adopt their definitions of individual ($\ExpIVVSymb$),
universal ($\ExpUVVSymb$) and eligibility ($\ExpEVVSymb$) verifiability for schemes with
internal authentication.
Those definitions seem to be the most suitable in the literature, because they detect the largest class of attacks. In particular, they detect collusion and biasing attacks~\cite[\S7]{Smyth15:ElectionVerifiability}, whereas other definitions, e.g.,~\cite{JCJ10,Cortier14:verifiability,Kiayias15}, fail to detect such attacks.
The definitions are presented in Appendix~\ref{app:verifiability}. %, along with a proof of the following result.
The definitions by Smyth, Frink, \& Clarkson work as follows:
Individual verifiability challenges the adversary to
generate a collision from algorithm $\VoteSymb$.
Universal verifiability challenges the adversary to concoct
a scenario in which either: $\VerSymb$ accepts, but the election
outcome is not correct, or $\TallySymb$ produces an election outcome
that $\VerSymb$ rejects. Hence, universal verifiability requires
algorithm $\VerSymb$ to accept if and only if the election outcome
is correct. Finally, eligibility verifiability challenges an adversary,
which can corrupt voters, to generate a valid ballot under a
non-corrupt voter's private credential.
We can prove that our construction ensures election verifiability.
Individual and eligibility verifiability of $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ follow from
security of the underlying signature scheme, and
universal verifiability follows from universal verifiability of the underlying election scheme $\Gamma$.
%\marginpar{BEN: \emph{Existential unforgeability under adaptive chosen-message attack} might not suffice. A different property (namely, strong unforgeability~\cite{Dodis02,Boneh06}) is used in my paper with Michael, albeit, we considered a different construction.}
\begin{theorem}\label{thm:verif}
Let $\Gamma$ be an election scheme with external authentication,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a random oracle.
Suppose $\Omega$ satisfies \SufficientConditionOnSignatures,
$\Sigma$ satisfies \SufficientConditionOnSignaturesSigma, and
$\Gamma$ satisfies $\ExpUVSymb$.
Election scheme with internal authentication $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies $\ExpIVVSymb$,
$\ExpEVVSymb$, and $\ExpUVVSymb$.
\end{theorem}
\begin{proof}[Proof sketch]
Individual verifiability is satisfied because voters can
check that their signatures appear on the bulletin board.
Universal verifiability is satisfied because the underlying voting scheme does, and the properties of $\Omega$ and $\Sigma$ ensure only authorised ballots are tallied.
And eligibility verifiability is satisfied because anyone can check
that signatures belong to registered voters.
\end{proof}
\noindent
A formal proof of Theorem~\ref{thm:verif} follows immediately from our proofs
of individual, universal and eligibility verifiability, which we defer to
Appendix~\ref{app:verifiability} (Lemmata~\ref{lem:simpleSignSchemeIVAlt}\iftr,
\ref{lem:simpleSignSchemeUV} \&~\else--\fi\ref{lem:simpleSignSchemeIVEV}).
We demonstrate applicability of our results
for election schemes from nonces.
\begin{definition}[$\Nonce$~\cite{Smyth15:ElectionVerifiability}]\label{def:nonce}
Election scheme with external authentication $\Nonce$ is defined as follows:
\begin{itemize}
\item $\Setup[\kappa]$ outputs $({\perp},{\perp},p_1(\kappa),p_2(\kappa))$, where $p_1$ and $p_2$ may be any polynomial functions.
\item $\Vote[\pk,\nC]{v,\kappa}$ selects a nonce $r$ uniformly at random from $\mathbb Z_{2^\kappa}$
and outputs $(r,v)$.
\item $\TallySymb(\sk, \nC, \bb,\kappa)$ computes a vector $\outcome$ of length $\nC$, such that
$\outcome$ is a tally of the votes on $\bbb$
for which the nonce is in $\mathbb Z_{2^\kappa}$,
% MRC: this feels like gratuitous formalism to me:
%$\langle {\bf X} \rangle = [\beta \mid (r,\beta)\in\bbb \wedge r\in\mathbb Z_{2^k} \wedge 1 \leq \beta \leq n_C ]$
and outputs $(\outcome,{\perp})$.
\item $\Verify[\pk,\bbb,\nC,\outcome,\tpf,\kappa]$ outputs $1$ if
$(\outcome,\tpf) = \TallySymb({\perp}, \nC, \bb,\kappa)$, and
$0$ otherwise.
\end{itemize}
\end{definition}
\noindent
Intuitively, election scheme $\Nonce$ ensures verifiability because
voters 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).
%Smyth, Frink, \& Clarkson~\cite[Proposition~1]{Smyth15:ElectionVerifiability}
%state the following result.
\begin{proposition}[\cite{Smyth15:ElectionVerifiability}]%\label{prop:example:nonce}
Election scheme with external authentication $\Nonce$
satisfies $\ExpIVSymb$ and $\ExpUVSymb$.
\end{proposition}
\noindent
Hence, by Theorem~\ref{thm:verif}, we have the following result.
\begin{corollary}%\label{prop:example:nonce}
Let $\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Nonce,\Omega)$,
and $\mathcal H$ be a random oracle.
Suppose $\Omega$ satisfies \SufficientConditionOnSignatures\ and
$\Sigma$ satisfies \SufficientConditionOnSignaturesSigma.
Election scheme with internal authentication
$\Trans(\Nonce,\Omega,\Sigma,\mathcal H)$
satisfies $\ExpIVVSymb$, $\ExpUVVSymb$, and $\ExpEVVSymb$.
\end{corollary}
\noindent
Clearly election scheme $\Nonce$ does not satisfy ballot secrecy.
%\newcommand{\HeliosSFC}{Helios'16}
```
# Case study: A secret, verifiable election scheme with internal authentication
Helios is an open-source, web-based electronic voting system which has been used in binding elections. The International Association of Cryptologic Research has used Helios annually since 2010 to elect board members (**IACRHelios10b?**; **IACRHelios10?**),[^2] the ACM used Helios for their 2014 general election (**ACM14:Helios?**), the Catholic University of Louvain used Helios to elect the university president in 2009 (**AdidaPereiraMarneffeQuisquater?**), and Princeton University has used Helios since 2009 to elect student governments. [^3],[^4] Informally, Helios can be modelled as the following election scheme with external authentication:
$\mathsf{Setup}$ generates a key pair for an asymmetric homomorphic encryption scheme, proves correct key generation in zero-knowledge, and outputs the public key coupled with the proof.
$\mathsf{Vote}$ encrypts the vote, proves correct ciphertext construction and that the vote is selected from the sequence of candidates (both in zero-knowledge), and outputs the ciphertext coupled with the proof.
$\mathsf{Tally}$ proceeds as follows. First, any ballots on the bulletin board for which proofs do not hold are discarded. Secondly, the ciphertexts in the remaining ballots are homomorphically combined, the homomorphic combination is decrypted to reveal the election outcome, and correctness of decryption is proved in zero-knowledge. Finally, the election outcome and proof of correct decryption are output.
$\mathsf{Verify}$ recomputes the homomorphic combination, checks the proofs, and outputs $1$ if these checks succeed and $0$ otherwise.
The original scheme (**AdidaPereiraMarneffeQuisquater?**) is known to be vulnerable to attacks against ballot secrecy and verifiability,[^5] and defences against those attacks have been proposed (**Smyth11:Helios?**; **Bernhard12:Helios?**; **2013:BallotIndependenceESORICS?**; **Smyth16:ballotSecrecy?**). We adopt the formal definition of a Helios variant by Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**), which adopts non-malleable ballots (**Smyth15:NM-CPA-ciphertexts?**; **Smyth16:ballotSecrecy?**) and uses the Fiat–Shamir transformation with statements in hashes (**Bernhard12:Helios?**) to defend against those attacks. Henceforth, we write *Helios’16* to refer to that formalisation.
Using our construction we derive an election scheme with internal authentication from Helios’16 and prove privacy and verifiability using our results.
Let $\Omega$ be a digital signature scheme, $\Sigma$ be a sigma protocol for relation $R(\textrm{Helios'16},\Omega)$, and $\mathcal H$ be a random oracle. Suppose $\Omega$ satisfies strong unforgeability and $\Sigma$ satisfies special soundness and special honest verifier zero-knowledge. Election scheme with internal authentication $\mathsf{Ext}2\mathsf{Int}(\textrm{Helios'16},\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ satisfies $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}\textrm{-}\mathsf{Int}$, $\mathsf{Exp}\text{-}\mathsf{IV}\text{-}\mathsf{Int}$, $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Int}$, and $\mathsf{Exp}\text{-}\mathsf{EV}\text{-}\mathsf{Int}$.
Smyth shows that Helios’16 satisfies $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}\textrm{-}\mathsf{Ext}$ (**Smyth16:ballotSecrecy?**) and Smyth, Frink & Clarkson show that $\mathsf{Exp}\text{-}\mathsf{IV}\text{-}\mathsf{Ext}$ and $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ are satisfied too (**Smyth15:ElectionVerifiability?**). Moreover, $\mathsf{FS}(\Sigma,\mathcal H)$ satisfies zero-knowledge by Theorem [thm:sigma]. Hence, we conclude by Theorems [thm:privacy] & [thm:verif].
#### Comparison with Helios-C.
Schemes derived from Helios using our construction are similar to Helios-C (**Cortier14:verifiability?**; **Cortier14:verifiabilityTech?**). Indeed, they use ballots that include a Helios ballot and a signature on that Helios ballot. The schemes derived by our construction also include proofs of correct construction, unlike Helios-C. We will see that this distinction is crucial to ensure ballot secrecy.
Cortier *et al.* (**Cortier14:verifiability?**) analysed Helios-C using the definition of ballot secrecy by Bernhard et al. (**Bernhard12:Helios?**). That definition assumes “ballots are *recorded-as-cast*, i.e., cast ballots are preserved with integrity through the ballot collection process" (**Smyth16:ballotSecrecy?**). Unfortunately, ballot secrecy is not satisfied without this assumption, because Helios-C uses malleable ballots.
An adversary can observe and block a voter’s ballot,[^6] extract the underlying Helios ballot, sign that ballot, and post the ballot and signature on the bulletin board. The adversary can then exploit the relation between ballots to recover the voter’s vote from the election outcome. (Cf. (**Smyth11:Helios?**).)
$\mathsf{Ext}2\mathsf{Int}(\textrm{Helios'16},\Omega,\Sigma,\mathcal H)$ ballots extend non-malleable Helios’16 ballots with a signature and a proof demonstrating construction of both the embedded Helios’16 ballot and signature, thus, $\mathsf{Ext}2\mathsf{Int}(\textrm{Helios'16},\Omega,\Sigma,\mathcal H)$ uses non-malleable ballots, so it is not similarly effected.
Beyond secrecy, Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) have shown that Helios-C does not satisfy $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Int}$. Hence, we improve upon Helios-C by satisfying $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}\textrm{-}\mathsf{Ext}$ and $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Int}$.
Our results can also be applied to the variant of Helios that applies a mixnet to encrypted votes and decrypts the mixed encrypted votes to reveal the outcome (**Adida08?**; **Pereira11:HeliosMixnet?**), rather than homomorphically combining encrypted votes and decrypting the homomorphic combination to reveal the outcome. Tsoukalas *et al.* (**Tsoukalas13:HeliosToZeus?**) released *Zeus* as a fork of Helios spliced with mixnet code to derive an implementation of that variant, and Yingtong Li released *helios-server-mixnet* as an extension of Zeus with threshold asymmetric encryption.[^7] We could use our construction to derive an election scheme with internal authentication from the mixnet variant of Helios and use our privacy and verifiability results to prove security. Since the ideas remain the same, we do not pursue further details.
# Conclusion
This work was initiated by a desire to eliminate trust assumptions placed upon the operators of external authentication services. Cortier *et al.* made progress in this direction with Helios-C, which builds upon Helios by signing ballots. We discovered that Helios-C does not satisfy ballot secrecy in the presence of an adversary that controls the bulletin board or the communication channel, and it is known that verifiability is not satisfied either. We realised that proving correct construction of both the Helios ballot and the signature suffices for non-malleability. This prompted the design of our construction and led to the accompanying security proofs that it produces voting systems satisfying ballot secrecy and verifiability. Finally, we demonstrated the applicability of our results by applying our construction to the Helios voting system. The next step would be to select a suitable sigma protocol and signature scheme to instantiate our construction concretely. And an interesting and useful direction for future work will be to consider, in general, the practical challenges of implementing our construction efficiently.
# Acknowledgements
In the context of (**Smyth15:ElectionVerifiability?**), Smyth conceived the fundamental ideas of our construction for election schemes with internal authentication
. In addition, Smyth discovered that Helios-C does not satisfy ballot secrecy, whilst analysing election verifiability. Smyth and his co-authors, Frink & Clarkson, decided not to publish these results. This paper builds upon those unpublished results and we are grateful to Frink & Clarkson for their part in inspiring this line of work.
# Cryptographic primitives and security definitions %Foundations: Signatures and proof systems
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 112, column 17): expecting \end{document} \end{definition} ^`
``` latex
\section{Cryptographic primitives and security definitions
%Foundations: Signatures and proof systems
}\label{app:crypto}
\begin{definition}[Signature scheme (as formalized in \cite{Katz07})]
A \emph{signature scheme} is a tuple $(\GGenSymb,\allowbreak\SgnSymb,\allowbreak\VrfySymb)$ of probabilistic polynomial-time (PPT) algorithms such that:
%
\begin{itemize}
\item \emph{\textbf{Gen}}, denoted $(\pk,\sk) \leftarrow \GGen$, takes a security parameter $\kk$ as input and outputs a key pair $(\pk,\sk)$.
\item \emph{\textbf{Sign}}, denoted $\sigma \leftarrow \Sgn$, takes a private key $\sk$ and message $m$ as input, and outputs a signature $\sigma$.
\item \emph{\textbf{Verify}}, denoted $v \leftarrow \Vrfy$, takes a public key $\pk$, message $m$, and signature $\sigma$ as input, and outputs a bit $v$, which is $1$ if the signature successfully verifies and $0$ otherwise. We assume $\VrfySymb$ is deterministic.
\end{itemize}
\noindent
Moreover, the scheme must be \emph{correct}: there exists a negligible function $\mathsf{negl}$, such that for all security parameters $\kk$ and messages $m$, we have $\Pr [(\pk,\sk) \leftarrow \GGen;\sigma \leftarrow \Sgn;\Vrfy[\allowbreak \pk,\allowbreak m,\allowbreak \sigma] = 1] > 1-\mathsf{negl}(\kk)$.
\end{definition}
\begin{comment}
\begin{definition}[$\EUCMA$~\cite{Katz07}]
A signature scheme $\Gamma = (\GGenSymb,\SgnSymb,\VrfySymb)$ satisfies
\emph{existential unforgeability under adaptive chosen-message attack ($\EUCMA$)}
if for all PPT adversaries $\adv$, there exists a negligible function $\mu$, such that
for all security parameters $k$, we have $\Succ(\Exp\text{-}\mathsf{Sign}(\Gamma,\allowbreak\adv,k)) \leq \mu(k)$, where experiment $\Exp\text{-}\mathsf{Sign}$ is defined as follows:
{\upshape
\begin{inlineexperiment}{$\Exp\text{-}\mathsf{Sign}(\Gamma,\adv,k)$}
$(\pk,\sk) \leftarrow \GGen[k]$\;
$\mathit{Msg}\leftarrow\emptyset$\;
$(m,\sigma) \leftarrow A^{\oracleSymb}(\pk,k)$\;
\eIf{$\Vrfy = 1 \wedge m\not\in\mathit{Msg}$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}}
\noindent
The experiment defines an oracle $\oracleSymb$. On invocation $\oracleSymb(m)$, oracle $\oracleSymb$
computes a signature $\sigma \leftarrow \Sgn[\sk,m]$, records that the adversary requested a signature
on $m$ by updating $\mathit{Msg}$ to be $\mathit{Msg} \cup \{m\}$, and outputs $\sigma$.
\end{definition}
\end{comment}
\begin{definition}[Strong unforgeability (as formalized in \cite{Smyth15:ElectionVerifiability})]
A signature scheme $\Gamma = (\GGenSymb,\SgnSymb,\allowbreak\VrfySymb)$ satisfies \emph{strong unforgeability}
if for all PPT adversaries $\adv$, there exists a negligible function $\mathsf{negl}$, such that for all security parameters
$\kk$, we have $\Succ(\Exp\text{-}\mathsf{StrongSign}(\Gamma,\allowbreak\adv,\kk)) \leq \mathsf{negl}(\kk)$, where experiment $\Exp\text{-}\mathsf{StrongSign}$ is defined as follows:
{\upshape % Need \upshape to keep the semi-colons in the experiment in the right font, because of the enclosing definition environment
\begin{inlineexperiment}{$\Exp\text{-}\mathsf{StrongSign}(\Gamma,\adv,\kk)$}
$(\pk,\sk) \leftarrow \GGen[\kk]$\;
$\mathit{Msg}\leftarrow\emptyset$\;
$(m,\sigma) \leftarrow A^{\oracleSymb}(\pk,\kk)$\;
\eIf{$\Vrfy = 1 \wedge (m,\sigma)\not\in\mathit{Msg}$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}}
\noindent
The experiment defines an oracle $\oracleSymb$. On invocation $\oracleSymb(m)$, oracle $\oracleSymb$
computes a signature $\sigma \leftarrow \Sgn[\sk,m]$, records the request and response $(m,\sigma)$ by updating $\mathit{Msg}$ to be $\mathit{Msg} \cup \{(m,\sigma)\}$, and outputs $\sigma$.
\end{definition}
\begin{comment}
\begin{definition}[Sigma protocol~\cite{Smyth15:ElectionVerifiability,Damgard10,Hazay10}]\label{def:sigmaProtocol}
A \emph{sigma protocol} for a relation $R$
is a tuple $(\CommSymb,\ChallSymb,\allowbreak\RespSymb,\VerSymb)$ of PPT algorithms such that:
\begin{itemize}
\item \emph{\textbf{Comm}}, denoted $(\comm,t) \leftarrow \CommSymb(s,w,\kk)$,
is executed by a \emph{prover}. $\CommSymb$ takes a statement $s$, witness $w$
and security parameter $\kk$ as input, and
outputs a commitment $\comm$ and some state information $t$.
\item \emph{\textbf{Chal}}, denoted $\chal \leftarrow \ChallSymb(s,\comm,\kk)$, is executed
by a \emph{verifier}. $\ChallSymb$ takes a statement $s$, a commitment $\comm$ and a
security parameter $\kk$ as input, and outputs a string $\chal$.
\item \emph{\textbf{Resp}}, denoted $\resp\leftarrow \RespSymb(\chal,t,\kk)$,
is executed by a prover. $\RespSymb$ takes a challenge $\chal$, state information $t$ and
security parameter $\kk$ as input, and outputs a response $\resp$.
\item \emph{\textbf{Verify}}, denoted $v \leftarrow \VerSymb(s,(\comm,\chal,
\resp),\kk)$ is executed by a verifier. $\VerSymb$ takes a statement $s$, a transcript $(\comm,\allowbreak\chal,\resp)$ and a security parameter $\kk$ as input, and outputs a bit $v$, which is $1$ if the transcript successfully verifies and $0$ otherwise. We assume $\VerSymb$ is deterministic.
\end{itemize}
\noindent
Moreover, the sigma protocol must be \emph{complete}: there exists a negligible function $\mathsf{negl}$,
such that for all statements and witnesses $(s,w) \in R$ and security parameters $\kk$, we have
$\Pr[(\comm,t)\leftarrow\CommSymb(s,w,\kk);\chal\leftarrow\ChallSymb(s,\comm,\kk);\resp \leftarrow \Resp{\chal}{t,k}:\VerSymb(s,(\comm,\allowbreak\chal,\resp),\kk)= 1] > 1 - \mathsf{negl}(\kk)$.
\end{definition}
\end{comment}
%\marginpar{Ben: Nested brackets can be avoided by replacing ``(as formalized in X)" with ``, formalized in X". Also, there's a US v. Brit issue.}
\begin{definition}[Non-interactive proof system (as formalized in \cite{Smyth15:ElectionVerifiability})]
A \emph{non-in\-ter\-ac\-tive proof system} for a relation $R$
is a tuple of PPT algorithms $(\ProveSymb, \VerifySymb)$
such that:
\begin{itemize}
\item \emph{\textbf{Prove}}, denoted $\sigma \leftarrow \ProveSymb(s,w,\kk)$,
is executed by a prover to prove $(s,w) \in R$.
\item \emph{\textbf{Verify}}, denoted $v\leftarrow \VerifySymb(s,\sigma,\kk)$,
is executed by anyone to check the validity of a proof. We assume
$\VerifySymb$ is deterministic.
\end{itemize}
\noindent
Moreover, the system must be \emph{complete}:
there exists a negligible function $\mathsf{negl}$, such that
for all statement and witnesses $(s,w)\in R$ and security parameters $\kk$,
we have $\Pr[\sigma \leftarrow \ProveSymb(s,w,\kk):\VerifySymb(s,\sigma,\kk) = 1] > 1 - \mathsf{negl}(\kk)$.
\end{definition}
\iftr
\begin{definition}[Fiat-Shamir transformation~\cite{FS87}]\label{def:fs}
Given a sigma protocol $\Sigma = (\CommSymb,\ChallSymb,\allowbreak\RespSymb,\VerSymb_\Sigma)$
for relation $R$ and a hash function $\mathcal H$, the \emph{Fiat-Shamir transformation}, denoted $\sFS{\Sigma}{\mathcal H}$, is the non-interactive proof system $(\ProveSymb, \VerifySymb)$, defined as follows:\par
{\upshape
\begin{inlineexperiment}{$\ProveSymb(s,w,\kk)$}
$(\comm,t) \leftarrow \CommSymb(s,w,\kk)$\;
$\chal \leftarrow\mathcal H(\comm,s)$\;
$\resp\leftarrow\RespSymb(\chal,t,\kk)$\;
\Return $(\comm,\resp)$
\end{inlineexperiment}%
\begin{inlineexperiment}{$\VerSymb(s,(\comm, \resp),\kk)$}
$\chal \leftarrow\mathcal H(\comm,s)$\;
\Return $\VerSymb_\Sigma(s,(\comm,\allowbreak \chal,\resp),\kk)$
\end{inlineexperiment}%
}
\end{definition}
\fi
\begin{comment}
\begin{color}{red}
\noindent
BEN: If you want to add ``formalized in~\cite{Smyth15:auctions}," then surely
you need to add it everywhere... I don't think it is necessary. The definition
was from~\cite{Smyth15:auctions}, nothing more. That's clear to me.\\
LIZ: I am not happy without that. It suggests QS15 introduced ZK. Very easy point to criticize as a reviewer.\\
BEN: I disagree. It merely suggests that QS15 introduced the definition. It is a style I've always used and I have never been criticized by a reviewer. That said, I'm not objecting to your inclusion of formalized, I'm objecting to a lack of consistency: If you want to include \emph{formalized}, then it must appear in every definition (where the formalisation isn't due to the inventors). Otherwise, a reviewer has better grounds to critize, e.g., it currently looks like we are attributing the formalization of zero-knowledge to QS15, but we are attributing the invention of digital signatures to Katz \& Lindell. Personally, I think dropping \emph{formalized} is fine. Since you don't want to do that, I see three options: 1) add \emph{formalized} everywhere (I'd really rather not), 2) mention in a footnote at the start of this section how we include citations (I'm not sure how to phrase such a footnote -- maybe ask on \url{https://academia.stackexchange.com}), or 3) include citations to the inventors and the formalisers (that seems quite nice, but perhaps overkill). Go with the one you prefer. Or perhaps propose something else.
\end{color}
\end{comment}
\iftr
\begin{definition}[Zero-knowledge (as formalized in~\cite{Smyth15:auctions})] Let $\Delta = (\ProveSymb,\allowbreak \VerifySymb)$ be a non-interactive proof system for a relation $R$,
derived by application of the Fiat-Shamir transformation~\cite{FS87} to a random oracle $\mathcal H$
and the sigma protocol. Moreover, let $\mathcal S$ be an algorithm, $\adv$ be an
adversary, $\kappa$ be a security parameter, and $\ZK(\allowbreak\Delta,\allowbreak\adv,\allowbreak\mathcal H,\allowbreak\mathcal S,\allowbreak\kappa)$
be the following game.
{\upshape
\begin{inlineexperiment}{$\ZK(\Delta,\adv,\mathcal H,\mathcal S,\kappa)$}
$\beta \leftarrow_R \{0,1\} $\;
$g\leftarrow \adv^{\mathcal H,\mathcal P}(\kappa)$\;
\eIf{$g = \beta$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
Oracle $\mathcal P$ is defined on inputs $(s,w)\in R$ as follows:
\begin{itemize}
\item $\mathcal P(s,w)$ computes { \DontPrintSemicolon\lleIf{$\beta = 0$}{$\sigma\leftarrow \ProveSymb(s,w,\kappa)$}{$\sigma\leftarrow \mathcal S(s,\kappa)$}} and outputs $\sigma$.
\end{itemize}
And algorithm $\mathcal S$ can patch random oracle $\mathcal H$.\footnote{%
Random oracles can be \emph{programmed} or \emph{patched}.
We will not need the details of how patching works, so we omit them here;
see Bernhard et al.~\cite{Bernhard12:Helios} for a formalisation.
}\
We say $\Delta$ satisfies \emph{zero-knowledge}, if there exists a probabilistic
polynomial-time algorithm $\mathcal S$, such that for all probabilistic polynomial-time algorithm adversaries $\adv$, there exists a negligible function $\mathsf{negl}$, and for all
security parameters $\kappa$, we have $\Succ(\allowbreak\ZK(\allowbreak\Delta,\allowbreak\adv,\allowbreak\mathcal H,\allowbreak\mathcal S,\allowbreak\kappa))
\allowbreak\leq \allowbreak\frac{1}{2} \allowbreak+ \allowbreak\mathsf{negl}(\kappa)$. An algorithm $\mathcal S$ for which zero-knowledge holds is called a \emph{simulator} for $(\ProveSymb, \VerifySymb)$.
\end{definition}
\fi
\iffalse
\begin{definition}[Simulation sound extractability (as formalized in \cite{Smyth15:ElectionVerifiability,Bernhard12:Helios,Groth06:SimulationSoundExtractability})]
Suppose $\Sigma$ is a sigma protocol for relation $R$,
$\mathcal H$ is a random oracle, and $(\ProveSymb, \allowbreak\VerifySymb)$ is a non-interactive proof system, such that $\sFS{\Sigma}{\mathcal H} = (\ProveSymb, \allowbreak\VerifySymb)$.
Further suppose $\mathcal S$ is a simulator for $(\ProveSymb, \VerifySymb)$
and $\mathcal H$ can be patched by $\mathcal S$.
Proof system $(\ProveSymb, \VerifySymb)$ satisfies \emph{simulation sound extractability}
if there exists a probabilistic polynomial-time algorithm $\mathcal K$, such that
for all probabilistic polynomial-time adversaries $\adv$ and coins $r$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kk$,
we have:\footnote{We extend set membership notation to vectors: we write $x\in{\bf x}$
if $x$ is an element of the set $\{ {\bf x}[i] : 1 \leq i \leq |{\bf x}| \}$.}
%
\begin{multline*}
\Pr[{\bf P}\leftarrow();
{\bf Q} \leftarrow\adv^{\mathcal H,\mathcal P}(\mbox{---};r);
{\bf W} \leftarrow \mathcal K^{\adv'}({\bf H},{\bf P},{\bf Q})
%
: \\
|{\bf Q}|\not=|{\bf W}| \vee \exists j\in\{1,\dots,|{\bf Q}|\} \mathrel . ({\bf Q}[j][1],{\bf W}[j])\not\in R \mathrel \wedge \\
\forall (s,\sigma) \in {\bf Q},(t,\tau) \in {\bf P} \mathrel . \VerifySymb(s,\sigma,\kk) = 1 \mathrel\wedge \sigma\not=\tau] \leq \mathsf{negl}(\kappa)
\end{multline*}
\noindent where $\adv(\mbox{---};r)$ denotes running adversary $\adv$ with an empty input and coins $r$, where ${\bf H}$ is a transcript of the random oracle's input and output, and
where oracles $\adv'$ and $\mathcal P$ are defined below:
\begin{itemize}
\item $\adv'()$. Computes ${\bf Q'}\leftarrow\adv(\mbox{---};r)$, forwarding any of $\adv$'s oracle queries to
$\mathcal K$, and outputs ${\bf Q'}$. By running $\adv(\mbox{---};r)$, $\mathcal K$ is rewinding the adversary.
\item $\mathcal P(s)$. Computes $\sigma \leftarrow \mathcal S(s); {\bf P} \leftarrow ({\bf P}[1],\allowbreak\dots,\allowbreak{\bf P}[|{\bf P}|],\allowbreak(s,\sigma))$
and outputs $\sigma$.
\end{itemize}
\noindent
Algorithm $\mathcal K$ is an \emph{extractor} for $(\ProveSymb, \VerifySymb)$.
\end{definition}
\fi
\begin{theorem}[\cite{Bernhard12:Helios}]\label{thm:sigma}
Let $\Sigma$ be a sigma protocol for relation $R$, and let $\mathcal H$ be a random oracle.
Suppose $\Sigma$ satisfies special soundness and special honest verifier zero-knowledge.
Non-interactive proof system $\sFS{\Sigma}{\mathcal H}$ satisfies zero-knowledge.
% and simulation sound extractability.
\end{theorem}
\fi
\iftr
```
# Proof of Lemma [lem:construction:correct]
Let $\Gamma = (\mathsf{Setup}_\Gamma, \mathsf{Vote}_\Gamma, \mathsf{Tally}_\Gamma, \mathsf{Verify}_\Gamma)$, $\Omega = (\mathsf{Gen}_\Omega,\allowbreak\mathsf{Sign}_\Omega,\allowbreak\mathsf{Verify}_\Omega)$, $\mathsf{FS}(\Sigma,\allowbreak\mathcal H) = (\mathsf{Prove}_\Sigma, \mathsf{Verify}_\Sigma)$, and $\mathsf{Ext}2\mathsf{Int}(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H) = (\mathsf{Setup},\allowbreak\mathsf{Register},\allowbreak \mathsf{Vote},\allowbreak \mathsf{Tally},\allowbreak \mathsf{Verify})$. Suppose $\kappa$ is a security parameter, $\mathit{nb}$ and $\mathit{nc}$ are integers, and $v_1,\allowbreak\dots,\allowbreak{}v_{\mathit{nb}}\allowbreak\in\allowbreak\{1,\allowbreak\dots,\allowbreak\mathit{nc}\}$ are votes. Further suppose $(\mathit{pk},\mathit{sk},\mathit{mb}, \mathit{mc})$ is an output of $\mathsf{Setup}(\kappa)$ such that $\mathit{nb}\leq \mathit{mb}\wedge \mathit{nc}\leq \mathit{mc}$. By definition of $\mathsf{Setup}$, we have $(\mathit{pk},\mathit{sk},\mathit{mb}, \mathit{mc})$ is an output of $\mathsf{Setup}_\Gamma(\kappa)$. Suppose for each $i\in\{1,\dots,\mathit{nb}\}$ that $(\mathit{pd}_i,\mathit{d}_i)$ is an output of $\mathsf{Register}(\mathit{pk},\kappa)$ and ${\bf b}_i$ is an output of $\mathsf{Vote}(\mathit{d}_i,\mathit{pk},\mathit{nc},v_i,\kappa)$. By definition of $\mathsf{Register}$, we have for each $i\in\{1,\dots,\mathit{nb}\}$ that $(\mathit{pd}_i,\mathit{d}_i)$ is an output of $\mathsf{Gen}_\Omega(\kappa)$. And by definition of $\mathsf{Vote}$, we have for each $i\in\{1,\dots,\mathit{nb}\}$ that ${\bf b}_i$ is a tuple $(\mathit{pd}_i,b_i,\sigma_i,\tau_i)$ such that $b_i = \mathsf{Vote}_\Gamma(\mathit{pk},\allowbreak \mathit{nc},\allowbreak v,\allowbreak \kappa;r)$, $\sigma_i = \mathsf{Sign}_\Omega(\mathit{d},\allowbreak b;\allowbreak r')$, and $\tau_i$ is an output of $\mathsf{Prove}_\Sigma((\mathit{pk},b,\sigma,\mathit{nc},\kappa),(v,r,\mathit{d},r'),\kappa)$, where $r_i$ and $r'_i$ are coins. Let $\mathfrak{bb}= \{{\bf b}_1,\dots,{\bf b}_{\mathit{nb}}\}$ and $L= \{\mathit{pd}_1,\dots,\mathit{pd}_{\mathit{nb}}\}$. Suppose ${\bf v}$ is the tally of votes $v_1,\allowbreak\dots,\allowbreak{}v_{\mathit{nb}}$ and $({\bf v}',\mathit{pf})$ is an output of $\mathsf{Tally}(\mathit{sk},\mathit{nc},\mathfrak{bb},L,\kappa)$. By definition of $\mathsf{Tally}$, we have $({\bf v}',\mathit{pf})$ is an output of $\mathsf{Tally}_\Gamma(\allowbreak\mathit{sk},\allowbreak\mathsf{auth}(\mathfrak{bb},L),\allowbreak{}\mathit{nc},\allowbreak{}\kappa)$. It suffices to prove $b\in\mathsf{auth}(\mathfrak{bb},L)$ iff $(\mathit{pd},\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\in \mathfrak{bb}$, because correctness of $\Gamma$ ensures outputs $({\bf v}_\Gamma,\mathit{pf}_\Gamma)$ of $\mathsf{Tally}_\Gamma(\allowbreak\mathit{sk},\allowbreak\mathfrak{bb},\allowbreak{}\mathit{nc},\allowbreak{}\kappa)$ are such that ${\bf v}= {\bf v}_\Gamma$, with overwhelming probability. By correctness of $\Omega$ and completeness of $(\mathsf{Prove}_\Sigma, \mathsf{Verify}_\Sigma)$, we have $\mathsf{auth}(\mathfrak{bb},L) = \{ b \mid (\mathit{pd},\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\in \mathfrak{bb}\allowbreak\wedge\allowbreak (\mathit{pd},\allowbreak b',\allowbreak\sigma',\allowbreak\tau')\not\in \mathfrak{bb}\setminus\{(\mathit{pd},\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\} \allowbreak\wedge\allowbreak
\mathsf{Verify}_\Omega(\allowbreak \mathit{pd},\allowbreak b',\allowbreak \sigma') = 1\}$, with overwhelming probability. Moreover, since $\Gamma$ satisfies strong unforgeability, we have $\mathsf{auth}(\mathfrak{bb},L) = \{ b \mid (\mathit{pd},\allowbreak b,\allowbreak\sigma,\allowbreak\tau)\in \mathfrak{bb}\}$, with overwhelming probability.
# %\iftr Ballot privacy: Definitions and proofs %\else Security definitions and proofs \fi
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 132, column 1): unexpected } expecting \end{document} } ^`
``` latex
\section{%\iftr
Ballot privacy: Definitions and proofs
%\else Security definitions and proofs \fi
}\label{app:ballot-secrecy}
%\iftr We \else \textbf{Ballot privacy.} We \fi
We
recall Smyth's definition of ballot secrecy for election schemes with external authentication
(Definition~\ref{def:SBBallotSecrecy}),
and present a natural, straightforward extension of that definition to capture
ballot secrecy for election schemes with internal authentication (Definition~\ref{def:SBBallotSecrecyy}).
Our definitions both use predicate $\balanced$ such that $\balanced(\bb,\nC,B)$ holds when: 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 B\}|
= |\{b \mid b \in \bb \wedge \exists v_0 \mathrel. (b,v_0,v) \in B\}|$.
Intuitively, the definitions challenge an adversary to determine
whether the left-right oracle produces ballots for ``left'' or ``right'' inputs, by giving the adversary the oracle's outputs, as well as the election outcome and tallying proof. The definitions prevent the adversary from trivially distinguishing ballots by requiring
predicate $\balanced$ to hold.
\begin{definition}[$\BallotSecrecy$~\cite{Smyth16:ballotSecrecy}]\label{def:SBBallotSecrecy}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be
an election scheme with external authentication, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\BallotSecrecy(\Gamma,\adv,\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\BallotSecrecy(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup[\kappa]$\;
$\nC \leftarrow \adv(\pk,\kappa)$\;
$\beta \leftarrow_R \{0,1\};B \leftarrow \emptyset$\;
$\bb \leftarrow \adv^{\oracleSymb}()$\;
$(\outcome, \tpf) \leftarrow \Tally{\bb,\kappa}$\;
$g\leftarrow\adv(\outcome, \tpf)$\;
\eIf{$g = \beta \land \balanced(\bb,\nC,B) \wedge 1\leq \nC\leq \mC \allowbreak\mathrel\wedge |\bb| \leq \mB$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
Oracle $\oracleSymb$ is defined as follows:\footnote{Oracles may access game parameters, e.g.,
$\pk$.}
\begin{itemize}
\item $\oracle{v_0,v_1}$ computes
{\DontPrintSemicolon\llIf{$v_0,v_1\in \{1, ...,\nC \}$}{$b\leftarrow \Vote[\pk,\allowbreak\nC]{v_\beta,\allowbreak\kappa};\allowbreak B \leftarrow B \cup \{ (b, v_0, v_1)\};\Return\ b$}}.
\end{itemize}
\noindent
We say $\Gamma$ satisfies $\BallotSecrecy$, if for all
probabilistic polynomial-time
adversaries $\adv$, there exists a negligible
function
$\mathsf{negl}$, such that for all security parameters $\kappa$, we have $\Succ(\BallotSecrecy(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \allowbreak\leq \frac{1}{2}+
\mathsf{negl}(\kappa)$.
\end{definition}
\begin{definition}[$\BallotSecrecyy$]\label{def:SBBallotSecrecyy}
Let $\Gamma = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be
an election scheme with internal authentication, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\BallotSecrecyy(\Gamma,\adv,\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\BallotSecrecyy(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB,\mC) \leftarrow \Setup[\kappa]$\;
$\nV \leftarrow \adv(\pk,\kappa)$\;
\For{$1 \leq i \leq \nV$}{
$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$;
}
$\nC \leftarrow \adv(\pd_1,\dots,\pd_{\nV})$\;
$\beta \leftarrow_R \{0,1\};B \leftarrow \emptyset; R\leftarrow \emptyset$\;
$\bb \leftarrow \adv^{\oracleSymb}()$\;
$(\outcome, \tpf) \leftarrow \Tally{\bb,\{\pd_1,\dots,\pd_{\nV}\},\kappa}$\;
$g\leftarrow\adv(\outcome, \tpf)$\;
\eIf{$g = \beta \land \balanced(\bb,\nC,B) \wedge 1\leq \nC\leq \mC \allowbreak\mathrel\wedge |\bb| \leq \mB$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
Oracle $\oracleSymb$ is defined as follows:
\begin{itemize}
\item $\oracle{i,v_0,v_1}$ computes {\DontPrintSemicolon\llIf{$v_0,v_1\in \{1, ...,\nC \} \wedge i\not\in R$}{$b\leftarrow \Vote[\sd_i,\allowbreak\pk,\allowbreak\nC]{v_\beta,\allowbreak\kappa};\allowbreak B \leftarrow B \cup \{ (b, v_0, v_1)\}; R\leftarrow R \cup \{i\};\Return\ b$}}; and
\item $\oracle{i}$ computes {\DontPrintSemicolon\llIf{$i\not\in R$}{$R\leftarrow R \cup \{i\};\Return\ \sd_i$}}.
\end{itemize}
\noindent
We say $\Gamma$ satisfies $\BallotSecrecyy$, if for all
probabilistic polynomial-time
adversaries $\adv$, there exists a negligible
function
$\mathsf{negl}$, such that for all security parameters $\kappa$, we have $\Succ(\BallotSecrecyy(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \allowbreak\leq \frac{1}{2}+
\mathsf{negl}(\kappa)$.
\end{definition}
\noindent
Game $\BallotSecrecyy$ extends $\BallotSecrecy$ to take credentials
into account. In particular, the challenger constructs $\nV$ credentials,
where $\nV$ is chosen by the adversary.
These credentials are used to construct ballots and for tallying.
Public and private credentials are available to the adversary. Albeit,
the oracle will only reveal a private credential if it has not used it
to construct a ballot. Moreover, the oracle may only
use a private credential to construct a ballot if it has not revealed it
nor constructed a previous ballot with it.
\begin{proof}[Proof of Theorem~\ref{thm:privacy}]
Suppose $\BallotSecrecyy$ is not satisfied by $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$, i.e., there exists a adversary $\adv$
such that for all negligible functions $\mathsf{negl}$ there exists a security parameter $\kappa$
and $\Succ(\BallotSecrecyy(\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H),\allowbreak\adv,\allowbreak\kappa)) \allowbreak\leq \frac{1}{2}+
\mathsf{negl}(\kappa)$.
We construct an adversary $\Adv$ against $\Gamma$ from $\adv$.
Let $\Gamma = (\SetupSymb_\Gamma, \VoteSymb_\Gamma, \TallySymb_\Gamma, \VerifySymb_\Gamma)$,
$\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$,
$\sFS{\Sigma}{\allowbreak\mathcal H} = (\ProveSymb_\Sigma, \VerSymb_\Sigma)$, and
$\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$.
By \SSE, non-interactive proof system $(\ProveSymb_\Sigma, \VerSymb_\Sigma)$
satisfies zero-knowledge, i.e., there exists a simulator for $(\ProveSymb_\Sigma, \VerifySymb_\Sigma)$. Let
$\mathcal S$ be such a simulator. We define $\Adv$ as follows:
\begin{itemize}
\item $\Adv(\pk,\kappa)$ computes
$\nV \leftarrow \adv(\pk,\kappa)$;
{\DontPrintSemicolon\llFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\allowbreak\kappa];$}}
$\nC \leftarrow \adv(\pd_1,\dots,\pd_{\nV})$
and outputs $\nC$.
\item $\Adv()$ computes $R\leftarrow \emptyset; \bb \leftarrow \adv^{\oracleSymb}();
\bb\leftarrow \mathsf{auth}(\bbb,\{\pd_1,\dots,\pd_{\nV}\})$
and outputs $\bb$, handling oracle calls from $\adv$ as follows.
Given an oracle call $\oracle{i,v_0,v_1}$
such that $v_0,v_1\in \{1, ...,\nC \} \wedge i\not\in R$, adversary $\Adv$ computes
$b\leftarrow \oracle{v_0,v_1};
\sigma\leftarrow \SgnSymb_\Omega(\sd_i,\allowbreak b);
\tau\leftarrow \mathcal S((\pk,b,\sigma,\nC,\kappa),\kappa);
R\leftarrow R \cup \{i\}$
and returns $(\pd_i,b,\sigma,\tau)$ to $\adv$. Moreover, given an oracle call $\oracle{i}$
such that $i\not\in R$, adversary $\Adv$ computes $R\leftarrow R \cup \{i\}$ and returns $\sd_i$ to $\adv$.
\item $\Adv(\outcome, \tpf)$ computes $g\leftarrow\adv(\outcome, \tpf)$ and outputs $g$.
\end{itemize}
\noindent
We prove that $\Adv$ wins $\BallotSecrecy$ against $\Gamma$.
Suppose $(\pk,\sk,\mB,\mC)$ is an output of $\SetupSymb_\Gamma(\kappa)$ and $\nC$
is an output of $\Adv(\pk,\kappa)$. It is trivial to see that $\Adv(\pk,\kappa)$
simulates $\adv$'s challenger to $\adv$. Let $\beta$ be a bit.
%%
%%
Suppose $\bb$ is an output of $\Adv()$. Since $\mathcal S$ is a simulator for
$(\ProveSymb_\Sigma, \VerSymb_\Sigma)$, we have $\Adv()$ simulates $\adv$'s
challenger to $\adv$. In particular, $\Adv()$ simulates oracle calls $\oracle{i,v_0,v_1}$.
Indeed, adversary $\Adv$ computes
$
b\leftarrow \oracle{v_0,v_1};\sigma\leftarrow \SgnSymb_\Omega(\sd_i,\allowbreak b);
\tau\leftarrow \mathcal S((\pk,b,\sigma,\nC,\kappa),\kappa)
$,
which, by definition of $\Adv$'s oracle, is equivalent to
$
b\leftarrow \VoteSymb_\Gamma(\pk,\allowbreak\nC,v_\beta,\allowbreak\kappa);
\sigma\leftarrow \SgnSymb_\Omega(\sd_i,\allowbreak b);
\tau\leftarrow \mathcal S((\pk,b,\sigma,\nC,\kappa),\kappa)
$.
And $\adv$'s oracle computes $b\leftarrow \Vote[\sd_i,\allowbreak\pk,\allowbreak\nC]{v_\beta,\allowbreak\kappa}$, i.e.,
$
b \leftarrow \VoteSymb_\Gamma(\pk,\allowbreak \nC,\allowbreak v_\beta,\allowbreak \kappa;r);
\sigma\leftarrow \SgnSymb_\Omega(\sd_i,\allowbreak b;\allowbreak r');
\tau\leftarrow\ProveSymb_\Sigma((\pk,\allowbreak b,\allowbreak\sigma,\allowbreak\nC,\allowbreak\kappa),(v_\beta,r,\sd_i,r'),\kappa)
$,
where $r$ and $r'$ are coins chosen uniformly at random.
Hence, computations of $b$, $\sigma$ and $\tau$ by $\Adv$ and $\adv$'s oracle
are equivalent, with overwhelming probability.
%%
%%
Suppose $(\outcome, \tpf)$ is an output of $\TallySymb_\Gamma(\allowbreak\sk,\bbb,\allowbreak{}\nC,\allowbreak{}\kappa)$ and
$g$ is an output of $\Adv(\outcome, \tpf)$. We have $\Adv(\outcome, \tpf)$
simulates $\adv$'s challenger to $\adv$, because outputs of $\TallySymb_\Gamma(\allowbreak\sk',\mathsf{auth}(\bbb',L),\allowbreak{}\nC',\allowbreak{}\kappa')$ and $\TallySymb(\sk',\nC',\bb',L,\kappa')$ are indistinguishable for all $\sk'$, $\bb'$, $L$, $\nC'$, and $\kappa'$. Indeed, $\TallySymb$ computes
$(\outcome',\allowbreak \tpf') \leftarrow\allowbreak \TallySymb_\Gamma(\allowbreak\sk',\allowbreak\mathsf{auth}(\bbb',\electoralroll),\allowbreak{}\nC',\allowbreak{}\kappa')$ and outputs $(\outcome',\allowbreak \tpf')$.
%%
%%
Since adversary $\Adv$ simulates $\adv$'s challenger, with overwhelming
probability. It follows that $\Adv$ determines $\beta$ correctly with the
same success as $\adv$ with overwhelming probability. Hence, $\Adv$ wins
$\BallotSecrecy(\Gamma,\adv,\allowbreak\kappa)$, with overwhelming probability,
deriving a contradiction and concluding our proof.
\end{proof}
%\iftr \section{Election verifiability: Definitions and proofs}\label{app:verifiability} \else \textbf{Election verifiability.}
%\fi
```
# Election verifiability: Definitions and proofs
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 142, column 1): unexpected } expecting \end{document} } ^`
``` latex
\section{Election verifiability: Definitions and proofs}\label{app:verifiability}
\iftr
We recall definitions of individual, universal and eligibility verifiability
by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}, and prove that
our construction ensures each of these verifiability properties.
\else
%We prove that our construction satisfies definitions of individual, universal and
%eligibility verifiability by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}.
\fi
%\iftr
\subsection{Individual verifiability}
%\fi
\begin{definition}[$\ExpIVSymb$~\cite{Smyth15:ElectionVerifiability}]
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme with external authentication, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpIV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpIV$}
$(\pk,\nC,v,v') \leftarrow \adv(\kappa)$\;
$b\leftarrow\VoteSymb(\pk,\nC,v,\kappa)$\;
$b'\leftarrow\VoteSymb(\pk,\nC,v',\kappa)$\;
\eIf{
$b = b'
\wedge b \not= {\perp}
\wedge b' \not= {\perp}
$}{
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies $\ExpIVSymb$,
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have $\SuccIV \leq \mathsf{negl}(\kappa)$.
\end{definition}
%\vspace{-0,9cm}
\begin{definition}[$\ExpIVVSymb$~\cite{Smyth15:ElectionVerifiability}]
Let $\Gamma = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$ be an election scheme with external authentication, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpIVV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpIVV$}
$(\pk, \nV) \leftarrow \adv(\kappa)$\;
\lFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$}
$\electoralroll \leftarrow \{\pd_1,\dots,\pd_{\nV}\}$\;
$\mathit{Crpt}\leftarrow\emptyset;$\\
$(\nC,v,v',i,j) \leftarrow \adv^{\corruptOracle}(\electoralroll)$\;
$b\leftarrow\Vote[\sd_i,\pk,\nC]{v,\kappa}$\;
$b'\leftarrow\Vote[\sd_j,\pk,\nC]{v',\kappa}$\;
\eIf{
$b = b'
\wedge b \not= {\perp}
\wedge b' \not= {\perp}
\wedge i \not= j
\wedge \sd_i \not\in \mathit{Crpt}
\wedge \sd_j\not\in \mathit{Crpt}
$}{
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
Oracle $\corruptOracle$ is defined such that $\corruptOracle(i)$ computes $\mathit{Crpt}\leftarrow\mathit{Crpt} \cup \{d_i\}$ and outputs $d_i$, where $1\leq i \leq \nV$.
We say $\Gamma$ satisfies $\ExpIVVSymb$,
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have $\SuccIVV \leq \mathsf{negl}(\kappa)$.
\end{definition}
%\subsubsection{Our construction ensures individual verifiability}
\iftr
Lemma~\ref{lem:simpleSignSchemeIVAlt} proves that our construction
ensures individual verifiability. Moreover, the assumption that the
underlying signature scheme satisfies strong unforgeability can be
replaced by the assumption that the underlying election scheme satisfies
individual verifiability (Lemma~\ref{lem:simpleSignSchemeIV}). \fi
\begin{lemma}\label{lem:simpleSignSchemeIVAlt}
Let $\Gamma= (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme with external authentication,
$\Omega= (\GGenSymb,\allowbreak\SgnSymb,\allowbreak\VrfySymb)$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a hash function.
Suppose $\Omega$ satisfies \SufficientConditionOnSignatures.
We have $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ satisfies $\ExpIVVSymb$.
\end{lemma}
\begin{proof}
\begin{comment}
\textcolor{red}{...signatures are unique, otherwise they can be forged, hence IV
reduces to security of the digital signature scheme...}
\end{comment}
Suppose $\Trans(\Gamma,\Pi,\Sigma,\mathcal H)$ does not satisfy $\ExpIVVSymb$. Hence,
there exists a PPT adversary $\adv$, such that for all negligible functions
$\mathsf{negl}$, there exists a security parameter $\kappa$ and
$\mathsf{negl}(\kappa) <\Succ(\ExpIVVSymb(\Trans(\Gamma,\Pi,\Sigma,\mathcal H), \allowbreak \adv, \allowbreak \kappa))$.
We construct the following adversary $\Adv$ against strong unforgeability
from $\adv$:
\begin{inlineexperiment}{$\Adv(\pd,\kappa)$}
$(\pk, \nV) \leftarrow \adv(\kappa)$\;
$i^* \leftarrow_R \{1,\dots,\nV\}$\;
\lFor{$i \in\{1,\dots,\nV\}\setminus\{i^*\}$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$}
$(\nC,v,v',j,k) \leftarrow \adv^{\corruptOracle}(\{\pd_1,\dots,\pd_{i^*-1},\pd,\pd_{i^*+1},\dots,\pd_{\nV}\})$\;
\uIf{$i^* = k$}{
$(\pd_j,b,\sigma,\tau) \leftarrow \Vote[\sd_j,\pk,\nC]{v,\kappa}$\;
\Return $(\sigma,b)$\;
}
\uElseIf{$i^* = j$}{
$(\pd_k,b,\sigma,\tau) \leftarrow \Vote[\sd_k,\pk,\nC]{v',\kappa}$\;
\Return $(\sigma,b)$\;
}
\Else{
\Abort\;
}
\end{inlineexperiment}
\noindent
where $\corruptOracle(i)$ %computes $\mathit{Crpt}\leftarrow\mathit{Crpt}\cup \{i\}$ and
outputs $\sd_i$ if $i\not=i^*$ and aborts otherwise.
We prove that $\Adv$ wins strong unforgeability against $\Omega$.
Since adversary $\Adv$ chooses $i^*$ uniformly at random and independently of adversary $\adv$,
and since $\adv$ is a winning adversary, hence, does not corrupt at least two distinct credentials, we have that $\Adv$ aborts with a probability upper-bounded by $\frac{\nV-2}{\nV}$.
Let us consider the probability that $\Adv$ wins, when there is no abort.
Suppose $(\pd,\sd)$ is an output of $\GGen[\kk]$, $(\pk, \nV)$
is an output of $\adv(\kappa)$, and $i^*$ is chosen uniformly at random
from $\{1,\dots,\nV\}$. Further suppose $(\pd_i,\sd_i)$ is an output
of $\Register[\pk,\kappa]$ for each $i \in\{1,\dots,\nV\}\setminus\{i^*\}$.
It is straightforward to see that $\Adv$ simulates the challenger and oracle
in $\ExpIVVSymb$ to $\adv$. Suppose $(\nC,\allowbreak v,\allowbreak v',\allowbreak j,\allowbreak k)$ is an output of $\adv^{\corruptOracle}(\{\pd_1,\dots,\pd_{i^*-1},\pd,\pd_{i^*+1},\dots,\pd_{\nV}\})$.
Since $\adv$ is a winning adversary, outputs of $\Vote[\sd_j,\pk,\nC]{v,\kappa}$
and $\Vote[\sd_k,\pk,\nC]{v',\allowbreak\kappa}$ collide with non-negligible probability.
Hence, if $i^*=k$, then $\Vote[\sd_j,\pk,\nC]{\allowbreak v,\allowbreak\kappa}$ outputs $(\pd_j,\allowbreak b,\allowbreak\sigma,\allowbreak\tau)$
such that $\sigma$ is a signature on $b$ with respect to private key $\sd_{i^*}$, otherwise
$(i^*=j)$, $\Vote[\sd_k,\pk,\nC]{v',\kappa}$ outputs $(\pd_k,b,\sigma,\tau)$
such that $\sigma$ is a signature on $b$ with respect to private key $\sd_{i^*}$.
Thus, $\Succ(\Exp\text{-}\mathsf{StrongSign}(\Gamma,\allowbreak\Adv,\kk))$ is at least
$\frac{2}{\nV} \cdot \Succ(\ExpIVVSymb(\Trans(\Gamma,\Pi,\Sigma,\mathcal H), \allowbreak \adv, \allowbreak \kappa))$, which is non-negligible.
\end{proof}
\begin{comment}
\textcolor{blue}{LIZ: I understand your intuition here. You can identify uniquely your bid since signatures are unique. However, I provide a proof sketch below (proving a slightly different lemma), and I am puzzled as to why it goes through. Would like to discuss.}
\textcolor{blue}{BEN: You can't drop the assumption that ``$\Omega$ satisfies \SufficientConditionOnSignatures,"
because it is needed for correctness. Hence, your lemma will require more assumptions than this one. (I already
proved something similar to your lemma. It was commented out in the source. I've uncommented. See above. (It may not be exactly right because things have changed, but it is probably reasonably close.))}
\end{comment}
\begin{comment}
\begin{color}{purple}
\begin{lemma}\label{lem:simpleSignSchemeIVAlt2}
Let $\Gamma$ be an election scheme with external authentication,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a hash function.
Suppose $\Gamma$ satisfies $\ExpIVSymb$.
We have $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies $\ExpIVVSymb$.
\end{lemma}
\begin{proof}[Proof sketch]
Suppose $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ does not satisfy $\ExpIVVSymb$.
That means that $\Adv$ is able to output $(\nC,v,v',i,j)$ such that $b=b'$, i.e., $(pd_i, \hat{b}, \sigma, \tau) = (pd_i', \hat{b}', \sigma', \tau')$. Which means, in particular, that $\hat{b}=\hat{b}'$, contradicting the hypothesis that $\Gamma$ satisfies $\ExpIVSymb$.
\end{proof}
\end{color}
\end{comment}
\iftr
\begin{lemma}\label{lem:simpleSignSchemeIV}
Let $\Gamma$ be an election scheme with external authentication,
$\Omega$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a hash function.
Suppose $\Omega$ satisfies \SufficientConditionOnSignatures.
If $\Gamma$ satisfies $\ExpIVSymb$, then
$\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies $\ExpIVVSymb$.
\end{lemma}
\noindent
Since voters can check that their ballots appear on the bulletin board in $\Gamma$
and ballots in $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ embed ballots from $\Gamma$, we have voters
can check that their ballots appear on the bulletin board in $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ too, i.e., $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies individual verifiability. In the context of~\cite{Smyth15:ElectionVerifiability}, Frink proved a similar
lemma and the following proof adapts his unpublished work.
\begin{proof}
\begin{comment}
\textcolor{red}{\texttt{svn blame -r 786 sig-proof.tex} includes ``\emph{Steven's proof follows, with some minor adaption and clarifications}". It looks like I adapted the proof from Steven's individual verifiability proof of Helios-C, which appears in \texttt{heliosC-proof.tex}. Steven's contribution must be acknowledged.}
\end{comment}
Suppose $\Trans(\Gamma,\Pi,\Sigma,\mathcal H)$ does not satisfy $\ExpIVVSymb$. Hence,
there exists a PPT adversary $\adv$, such that for all negligible functions
$\mathsf{negl}$, there exists a security parameter $\kappa$ and
$\mathsf{negl}(\kappa) <\Succ(\ExpIVVSymb(\Trans(\Gamma,\Pi,\Sigma,\mathcal H), \allowbreak \adv, \allowbreak \kappa))$.
We construct the following adversary $\Adv$ against $\ExpIVSymb$
from $\adv$.
\begin{inlineexperiment}{$\Adv(\kappa)$}
$(\pk,n_V) \leftarrow \adv(\kappa)$\;
\lFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$}
$L\leftarrow \{\pd_1,\dots,\pd_{\nV}\}$\;
$(\nC,v,v',i,j)\leftarrow \adv^{C}(L)$\;
\Return $(\nC,v,v')$
\end{inlineexperiment}
\noindent
Adversary $\Adv$ responds to $\adv$'s oracle calls $C(\ell)$ by outputting $\sk_\ell$.
We prove that $\Adv$ wins $\ExpIVSymb$.
It is trivial to see that $\Adv$ simulates $\adv$'s challenger and oracle to $\adv$.
Moreover, by definition of $\Trans(\Gamma,\Pi,\Sigma,\mathcal H)$, we have ballots in $\Trans(\Gamma,\Pi,\Sigma,\mathcal H)$
embed ballots from $\Gamma$. It follows that any collision in $\Trans(\Gamma,\Pi,\Sigma,\mathcal H)$
implies a collision in $\Gamma$. Hence,
$\Succ(\ExpIVVSymb(\Trans(\Gamma,\Pi,\Sigma,\mathcal H), \allowbreak \adv, \allowbreak \kappa)) \allowbreak \leq \Succ(\ExpIVSymb(\allowbreak\Gamma, \allowbreak \Adv, \allowbreak \kappa))$, concluding our proof.
\end{proof}
\fi
%\iftr
\subsection{Universal verifiability}
%\else
% \textbf{Universal verifiability for external authentication.}
%\fi
%Universal verifiability challenges the adversary to concoct
%a scenario in which either: $\VerSymb$ accepts, but the election outcome is not correct, or
%$\TallySymb$ produces an election outcome that $\VerSymb$ rejects.
%Hence, the formal definitions require algorithm $\VerSymb$ to accept if and only if
%the election outcome is correct.
\iftr
\subsubsection{Election schemes with external authentication.}
\else
\paragraph{External authentication}
\fi
Algorithm $\VerSymb$ is required to accept iff
the election outcome is correct.
The notion of a correct outcome is captured using
function $\correcttally$, which is defined such that for all
$\pk$, $\nC$, $\bb$, $\kk$, $\ell$, and $v \in \{1,\allowbreak\ldots,\allowbreak\nC\}$,
we have
$
\correcttally(\pk,\nC,\bb,\kk)[v]\allowbreak = \ell$
iff $\exists^{=\ell} b\in \bb \setminus \{\bot\} :
\exists r : b=\VoteSymb(\pk,\nC,v,\kappa; r)
$,\footnote{Function $\correcttally$ uses a
\emph{counting quantifier}~\cite{Schweikardt05} denoted $\exists^{=}$.
Predicate $(\exists^{=\ell} x : P(x))$ holds exactly when there are
$\ell$ distinct values for $x$ such that $P(x)$ is satisfied.
Variable $x$ is bound by the quantifier, whereas $\ell$ is free.}
\iftr
and the vector produced by $\correcttally$ is of length $\nC$.
\else
and the produced vector is of length $\nC$.
\fi
Hence, component $v$ of vector
$\correcttally(\pk,\allowbreak \nC,\bb,\kk)$
equals $\ell$ iff there exist $\ell$ ballots on the bulletin board that are votes for candidate $v$. The function requires ballots to be interpreted for only
one candidate, which can be ensured by injectivity.
\iftr
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]\label{InjExt}
An election scheme with external authentication $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies \emph{Injectivity},
if for all security parameters $\kk$,
public keys $\pk$,
integers $\nC$, and
votes $v$ and $v'$, such that $v\not=v'$, we have
%
$
\Pr [ b\leftarrow \VoteSymb(\pk,\nC,v,\kappa);\allowbreak
b'\leftarrow \VoteSymb(\pk,\nC,v',\kappa)
%
:b\neq \bot \wedge b'\neq \bot \Rightarrow b\neq b'] = 1
$.
\end{definition}
\fi
The \emph{if} requirement of universal verifiability is captured by Completeness, which
stipulates that election outcomes produced by algorithm $\TallySymb$
will actually be accepted by algorithm $\VerSymb$.
And the \emph{only if} requirement
is captured by Soundness, which challenges an adversary to concoct
a scenario in which algorithm $\VerSymb$ accepts, but the election outcome is not correct.
\iftr
Combining these definitions we can formulate universal verifiability.
\fi
\iftr
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]
An election scheme with external authentication $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies \emph{Completeness},
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kk$ it holds that
%
$
\Pr [(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC) \leftarrow\allowbreak \Setup[\kk];\allowbreak
(\bb,\nC) \leftarrow \adv(\pk,\kk);\allowbreak
(\outcome,\allowbreak\tpf) \leftarrow\allowbreak \Tally{\bb,\allowbreak\kk}
%
:\allowbreak |\bb| \leq \mB \wedge\allowbreak \nC\leq \mC\allowbreak\Rightarrow\VerSymb(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak\outcome,\allowbreak\tpf,\allowbreak\kk) =\allowbreak 1] >\allowbreak 1 - \mathsf{negl}(\kappa)
$.
\end{definition}
\fi
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]\label{def:uv}
An election scheme with external authentication $(\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ satisfies \emph{Soundness},
if the scheme satisfies Injectivity\iftr\else~\cite{Smyth15:ElectionVerifiability}\fi\ and
for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kk$, we have
$
\Pr [(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak\outcome,\allowbreak\tpf) \leftarrow\allowbreak \adv(\kk);\allowbreak
\Return\ \outcome \not=\allowbreak \correcttally(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak \kk) \mathrel\wedge\allowbreak \VerSymb(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak \outcome,\allowbreak\tpf,\allowbreak\kk) =\allowbreak 1] \leq \mathsf{negl}(\kappa)$.
\end{definition}
\iftr
\begin{definition}[$\ExpUVSymb$~\cite{Smyth15:ElectionVerifiability}]
\fi
\noindent
An election scheme with external authentication satisfies $\ExpUVSymb$,
if Injectivity, Completeness and Soundness are satisfied\iftr\else,
where formal definitions of Injectivity and Completeness appear in
\cite{Smyth15:ElectionVerifiability}\fi.
\iftr
\end{definition}
\fi
\iftr
\subsubsection{Election schemes with internal authentication.}
\else
\paragraph{Internal authentication}
\fi
Function $\correcttally$ is now modified to tally only authorised ballots:
let function $\correcttally$ now
be defined such that
for all $\pk$, $\nC$, $\bbb$, $\electoralrollprivate$, $\kappa$, $\ell$, and $v \in \{1,\ldots,\nC\}$,
we have
$\correcttally(\pk,\allowbreak\nC,\allowbreak\bbb,\allowbreak\electoralrollprivate,\allowbreak\kappa)[v] =\allowbreak \ell$ iff
$\exists^{=\ell} b\in\authorized(\pk,\nC,(\bbb \setminus \{\bot\}),\electoralrollprivate, \kappa) \mathrel: \exists \sd, r : b=\Vote[\sd,\pk,\nC]{v,\kappa; r}$.
A ballot is \emph{authorised} if it is constructed with a private credential from $\electoralrollprivate$, and that private credential was not used to construct any other ballot on $\bbb$.
Let $\authorized$ be defined as follows:
$
\authorized(\pk,\allowbreak\nC,\allowbreak\bbb,\allowbreak\electoralrollprivate,\allowbreak\kappa) =\allowbreak \{ b \mathrel{:}\; b \in \bbb
\mathrel\wedge \exists \pd,\sd, v, r \mathrel : b=\Vote[\sd,\pk,\nC]{v,\kappa; r}
\mathrel\wedge (\pd,\sd)\in\electoralrollprivate \mathrel\wedge \neg \exists b',v',r' : b' \in (\bbb \setminus \{b\})
\mathrel\wedge b'=\Vote[\sd,\pk,\nC]{v',\kappa; r'}\}
$.
%
\iftr
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]\label{InjInt}
An election scheme with internal authentication
$(\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$
satisfies \emph{Injectivity}, if for all security parameters $\kappa$, public keys $\pk$,
integers $\nC$, and
votes $v$ and $v'$, such that $v\not=v'$, we have
$
\Pr[(\pd,\sd)\leftarrow\Register[\pk,\kappa];
(\pd',\sd')\leftarrow\Register[\pk,\kappa];
b\leftarrow \Vote[\sd,\pk,\nC]{v,\kappa};\allowbreak
b'\leftarrow \Vote[\sd',\pk,\nC]{v',\kappa}
\mathrel : b\neq \bot \wedge b'\neq \bot \Rightarrow b\neq b'] = 1
$.
\end{definition}
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]\label{CompleteInt}
An election scheme with internal authentication
$(\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$
satisfies \emph{Completeness}, if for all probabilistic poly\-no\-mi\-al-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have
$\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa];
\nV \leftarrow \adv(\pk,\kappa);$
{\DontPrintSemicolon
\llFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa];$}%
}
$\electoralroll \leftarrow \{\pd_1,\dots,\pd_{\nV}\};
M \leftarrow \{(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})\};
(\bb,\nC)\leftarrow \adv(M);
(\outcome,\tpf) \leftarrow \TallySymb(\sk, \nC, \bb,\electoralroll,\kappa)
\mathrel :|\bbb| \leq \mB \wedge \nC\leq \mC \Rightarrow \Verify[\pk,\nC,\bbb,\electoralroll,\outcome,\tpf,\kappa] = 1] > 1 - \mathsf{negl}(\kappa)
$.
\end{definition}
\fi
\begin{definition}[\cite{Smyth15:ElectionVerifiability}]\label{SoundInt}
An election scheme with internal authentication $(\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$ satisfies \emph{Soundness}, if
the scheme satisfies Injectivity\iftr\else~\cite{Smyth15:ElectionVerifiability}\fi\ and for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have
$\Pr[\allowbreak (\pk,\allowbreak\nV) \leftarrow \adv(\kappa);$
{\DontPrintSemicolon
\llFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$;}
}
$\electoralroll \leftarrow \{\pd_1,\allowbreak\dots,\allowbreak\pd_{\nV}\};
\electoralrollprivate \leftarrow \{(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})\};
(\bbb,\nC,\outcome, \tpf) \leftarrow \adv(\electoralrollprivate); \Return\ \outcome \not= \correcttally(\pk,\allowbreak\nC,\allowbreak\bbb,\allowbreak\electoralrollprivate,\allowbreak \kappa) \mathrel\wedge \Verify[\pk,\nC,\bbb,\electoralroll, \outcome,\tpf,\kappa] = 1] \leq \mathsf{negl}(\kappa)
$.
\end{definition}
\iftr
\begin{definition}[$\ExpUVVSymb$~\cite{Smyth15:ElectionVerifiability}]
\fi
\noindent
An election scheme with internal authentication satisfies $\ExpUVVSymb$,
if Injectivity, Completeness and Soundness are satisfied.
\iftr
\end{definition}
\fi
\iftr
\subsubsection{Our construction ensures universal verifiability.}
We prove that our construction ensures Injectivity, Completeness,
and Soundness.
%verifiability, from which Theorem~\ref{thm:verif} follows immediately.
\fi
\begin{lemma}\label{lem:simpleSignSchemeUV}
Let $\Gamma = (\SetupSymb_\Gamma, \VoteSymb_\Gamma, \TallySymb_\Gamma, \VerifySymb_\Gamma)$ be an election scheme with external authentication,
$\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$ be a perfectly correct digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a random oracle.
Moreover, let $\sFS{\allowbreak\Sigma}{\mathcal H} = (\ProveSymb_\Sigma, \VerSymb_\Sigma)$.
Suppose $\Gamma$ satisfies $\ExpUVSymb$, $\Omega$ satisfies \SufficientConditionOnSignatures and $\Sigma$ satisfies perfect \SufficientConditionOnSignaturesSigma.
Election scheme with internal authentication
$\Trans(\Gamma,\Omega,\Sigma,\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$
satisfies $\ExpUVVSymb$.
\end{lemma}
\begin{proof}
We prove that $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Injectivity, Completeness and Soundness:
\iftr
\paragraph{Injectivity.}
\begin{comment}
Injectivity of $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ follows from Injectivity of $\Gamma$.
Indeed, let $A$, respectively $B$, be the event whose probability is described in Definition \ref{InjExt}, respecively Definition \ref{InjInt}. It is trivial to see that $A$ implies $B$,
%
% BEN: A only implie B in the context of this proof, but I think that's clear.
%
because algorithm $\VoteSymb_\Gamma$ produces distinct ballots, and algorithm $\VoteSymb$ will consequently produce distinct ballots, because ballots output by $\VoteSymb$ embed ballots output by $\VoteSymb_\Gamma$. More precisely, $\VoteSymb$ outputs tuples $(\pd,b,\sigma,\tau)$ such that $b$ is an output of $\VoteSymb_\Gamma$.
Since $A$ implies $B$, we have $\Pr[A] \leq \Pr[B]$, and since $\Pr[A]=1$ by assumption, we have that $\Pr[B]=1$, hence $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Injectivity.
\end{comment}
Algorithm $\VoteSymb$ outputs ballots $(\pd,b,\sigma,\tau)$ such that
$b$ is an output of $\VoteSymb_\Gamma$. Hence, injectivity of
$\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ follows from Injectivity of
$\Gamma$, because injectivity guarantees that $b$ is distinct from
other ballots output by $\VoteSymb_\Gamma$.
\begin{comment}
Suppose $\kappa$ is a security parameter, $\pk$ is a public key, $\nC$ is an integer,
and $v$ and $v'$ are votes such that $v\not=v'$. Further suppose
$(\pd,\sd)$ and $(\pd',\sd')$ are outputs of $\Register[\pk,\kappa]$,
$(\pd,b,\sigma,\tau)$ is an output of $\Vote[\sd,\pk,\nC]{v,\kappa}$, and
$(\pd',b',\sigma',\tau')$ is an output of $\Vote[\sd',\pk,\nC]{v',\kappa}$.
By definition of $\VoteSymb$, we have $b$ is an output of
$\VoteSymb_\Gamma(\pk,\allowbreak \nC,\allowbreak v,\allowbreak \kappa)$
and $b'$ is an output of $\VoteSymb_\Gamma(\pk,\allowbreak \nC,\allowbreak v',\allowbreak \kappa)$.
Since $\Gamma$ satisfies injectivity, we have $b\not=b'$, and it follows that
$\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Injectivity.
\end{comment}
\paragraph{Completeness.}
\begin{comment}
Let $\kappa$ be a security parameter. Suppose $(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak \mC)$ is an output of $\Setup[\kappa]$ and $(\bb,\nC)$ is an output of $\adv(\pk,\kappa)$ such that $| \bb | \leq \mB \wedge \nC\leq \mC$.
%$v_1,\allowbreak\dots,\allowbreak{}v_{\nB}\allowbreak\in\allowbreak\{1,\allowbreak\dots,\allowbreak\nC\}$ are votes
Further suppose $(\pd_i,\sd_i)$ is an output of $\Register[\pk,\kappa]$,
for each $i\in\{1,\dots,\nB\}$. Let $\electoralroll = \{\pd_1,\dots,\pd_{\nB}\}$
and $M = \{(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})\}$.
Suppose $(\bb,\nC)$ is an output of $\adv(M)$ and $(\outcome,\tpf)$
is an output of $\TallySymb(\sk, \nC, \bb,\electoralroll,\kappa)$.
By definition of $\SetupSymb$, we have $(\pk,\sk,\mB, \mC)$ is an output of
$\SetupSymb_\Gamma(\kappa)$. Moreover, by definition of $\TallySymb$ we have
$(\outcome,\tpf)$ is an output of $\TallySymb_\Gamma(\allowbreak\sk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak{}\nC,\allowbreak{}\kappa)$.
Furthermore, by definition of $\VerifySymb$ we have
$\Verify[\pk,\nC,\bbb,\electoralroll,\outcome,\tpf,\kappa] =
\VerifySymb_\Gamma(\allowbreak\pk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak{}\nC, \allowbreak{}\outcome, \allowbreak{}\tpf, \allowbreak{}\kappa)$.
By Completeness of $\Gamma$, we have $\VerifySymb_\Gamma(\allowbreak\pk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak{}\nC, \allowbreak{}\outcome, \allowbreak{}\tpf, \allowbreak{}\kappa) = 1$,
\textcolor{red}{BEN: This isn't immediately true ($\VerifySymb_\Gamma$ doesn't necessarily holds for $\mathsf{auth}(\bbb,\electoralroll)$). Perhaps you can explain in a few lines why it is? Or maybe a reductionist security argument is needed.}
with overwhelming probability, hence $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Completeness.
\textcolor{red}{LIZ: I believe it can be proved by reduction as you suggest. I do believe it can be proved directly too, though there seems to be need for a "composition" argument on tally and outcomes. Perhaps interesting to discuss.
Below, a the new proof for completeness.}
\end{comment}
We prove that $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Completeness by contradiction.
Suppose $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ does not satisfy Completeness, i.e., there exists an adversary $\adv$
such that for all negligible functions $\mathsf{negl}$ there exists a security parameter $\kappa$
and the probability defined in Definition \ref{CompleteInt} is less or equal to $
\mathsf{negl}(\kappa)$. We use $\adv$ to construct an adversary $\Adv$ that breaks Completeness of $\Gamma$.
\begin{inlineexperiment}{$\Adv(\kappa)$}
$(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$\; %I think it should be Setup_Gamma
$\nV \leftarrow \adv(\pk, \kappa)$\;
\For{$1 \leq i \leq \nV$}{
$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$\;
}
$\electoralroll = \{\pd_1,\dots,\pd_{\nV}\}$\;
$\electoralrollprivate \leftarrow \{(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})\} $\;
$(\bb,\nC) \leftarrow \adv(\electoralrollprivate)$\;
\Return $(\mathsf{auth}(\bbb,\electoralroll), \nC)$
\end{inlineexperiment}
%\marginpar{LIZ: Maybe the correct set to input is $\{\mathsf{auth}(\bbb,\electoralroll) \setminus \perp\}$. To check}
\noindent
We prove that $\Adv$ breaks Completeness of $\Gamma$.
Suppose $(\pk,\sk,\mB, \mC)$ is an output of $\Setup[\kappa]$, $\nV$ is an output of $\adv(\pk, \kappa)$, and
$(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})$ are outputs of $\Register[\pk,\kappa]$.
Let $\electoralroll = \{\pd_1,\allowbreak\dots,\allowbreak\pd_{\nV}\}$ and
$\electoralrollprivate = \{(\pd_1,\allowbreak\sd_1),\allowbreak\dots,\allowbreak(\pd_{\nV},\allowbreak\sd_{\nV})\}$.
Suppose $(\bb,\nC)$ is an output of $\adv(\electoralrollprivate)$.
Further suppose $(\allowbreak\mathsf{auth}(\bbb,\electoralroll),\nC)$ is an output of $\Adv(\kk)$. Suppose $(\outcome,\allowbreak \tpf)$ is the output of $\TallySymb(\sk, \nC, \bb,\electoralroll,\kappa)$. By definition, this is the output of $\TallySymb_\Gamma(\allowbreak\sk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak{}\nC,\allowbreak{}\kappa)$.
Since $\adv$ is a winning adversary, we have $\Verify[\pk,\nC,\bbb,\electoralroll, \outcome,\tpf,\kappa] = 1$ with probability less or equal to $1 - \mathsf{negl}(\kappa)$. By definition, $\VerifySymb$'s output coincides with the output of $\VerifySymb_\Gamma(\allowbreak\pk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak\nC,\allowbreak\outcome,\allowbreak \tpf,\allowbreak \kappa)$, which will, by the above, be equal to 1 with probability less or equal to $1 - \mathsf{negl}(\kappa)$, meaning that Completeness of $\Gamma$ does not hold. Thereby deriving a contradiction and concluding our proof.
\else
The proofs for Injectivity and Completeness are quite straightforward and can be found in our technical report~\cite{tr}.
\fi
\paragraph{Soundness.}
%\marginpar{BEN. I haven't checked soundness yet.}
We prove that $\Trans(\Gamma,\Omega,\Sigma,\mathcal H)$ satisfies Soundness by contradiction.
Suppose $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ does not satisfy Soundness, i.e., there exists an adversary $\adv$
such that for all negligible functions $\mathsf{negl}$ there exists a security parameter $\kappa$
and the probability defined in Definition \ref{SoundInt} is greater than $
\mathsf{negl}(\kappa)$. We use $\adv$ to construct an adversary $\Adv$ that wins the Soundness game against $\Gamma$.
\begin{inlineexperiment}{$\Adv(\kappa)$}
$(\pk, \nV) \leftarrow \adv(\kappa)$\;
\For{$1 \leq i \leq \nV$}{
$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$\;
}
$\electoralroll = \{\pd_1,\dots,\pd_{\nV}\}$\;
$\electoralrollprivate \leftarrow \{(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})\} $\;
$(\bb,\nC, \outcome, \tpf) \leftarrow \adv(\electoralrollprivate)$\;
\Return $(\pk, \nC, \mathsf{auth}(\bbb,\electoralroll), \outcome, \tpf)$
\end{inlineexperiment}
%\marginpar{LIZ: Maybe the correct set to input is $\{\mathsf{auth}(\bbb,\electoralroll) \setminus \perp\}$. To check}
\noindent
We prove that $\Adv$ wins the Soundness game against $\Gamma$.
%\sout{To prove that $\Adv$ breaks the Soundness of $\Gamma$, we need to prove
%for all security parameters $\kappa$ that $\Adv(\kappa)$ outputs
%$(\pk, \nC, \mathsf{auth}(\bbb,\electoralroll), \outcome, \tpf)$} \textcolor{red}{BEN: The following is more verbose to help me check.}
Suppose $(\pk, \nV)$ is an output of $\adv(\kappa)$ and
$(\pd_1,\sd_1),\dots,(\pd_{\nV},\sd_{\nV})$ are outputs of $\Register[\pk,\kappa]$.
Let $\electoralroll = \{\pd_1,\dots,\pd_{\nV}\}$ and
$\electoralrollprivate = \{(\pd_1,\allowbreak\sd_1),\allowbreak\dots,\allowbreak(\pd_{\nV},\allowbreak\sd_{\nV})\}$.
Suppose $(\bb,\nC, \outcome, \tpf)$ is an output of $\adv(\electoralrollprivate)$.
Further suppose $(\pk,\allowbreak\nC,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak\outcome,\allowbreak\tpf)$ is an output of $\Adv(\kk)$.
Since $\adv$ is a winning adversary, we have $\Verify[\pk,\nC,\bbb,\electoralroll, \outcome,\tpf,\kappa] = 1$, with non-negligible probability.
By inspection of algorithm $\VerifySymb$, we have $\Verify[\pk,\nC,\bbb,\electoralroll, \outcome,\tpf,\kappa] = 1$ implies $\VerifySymb_\Gamma(\allowbreak\pk,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak\nC,\allowbreak\outcome,\allowbreak \tpf,\allowbreak \kappa) = 1$. Hence, it remains to show
$\outcome \neq \correcttally(\pk,\allowbreak\nC,\allowbreak\mathsf{auth}(\bbb,\electoralroll),\allowbreak \kk)$, with probability greater than $\mathsf{negl}(\kappa)$.
\makeatletter
\newcommand{\pushright}[1]{\ifmeasuring@#1\else\omit\hfill$\displaystyle#1$\fi\ignorespaces}
\newcommand{\pushleft}[1]{\ifmeasuring@#1\else\omit$\displaystyle#1$\hfill\fi\ignorespaces}
\makeatother
By definition of function $\correcttally$, we have $\outcome$ is a vector of length $\nC$ such that
%
\begin{align}
&\correcttally(\pk,\nC,\mathsf{auth}(\bbb,\electoralroll),\kk)[v] = \ell \nonumber\\
&\quad\Leftrightarrow \exists^{=\ell} b\in \mathsf{auth}(\bbb,\electoralroll) \setminus \{\bot\} :
\exists r : b=\VoteSymb(\pk,\nC,v,\kappa; r) \nonumber
%
\intertext{%
Since $\adv$ is a winning adversary, it suffices to derive
}
%
&\quad\Leftrightarrow\exists^{=\ell} b\in\authorized(\pk,\nC,(\bbb \setminus \{\bot\}),\electoralrollprivate, \kappa)\nonumber\\
& \pushright{\hfill\mathrel: \exists \sd, r : b=\Vote[\sd,\pk,\nC]{v,\kappa; r}}
\label{stepiff}
\end{align}
%
\noindent
Let set $auth^* (\pk,\nC,\bbb,\electoralrollprivate,\kappa)=\{b^*| (\pd, b^*, \sigma, \tau) \in \authorized(\pk,\nC,\bbb,\electoralrollprivate,\kappa) \}$.
To prove (\ref{stepiff}), it suffices to show $\mathsf{auth}(\bbb,\electoralroll)\setminus\{\perp\} = auth^* (\pk,\nC,\bbb,\electoralrollprivate,\kappa)\setminus\{\perp\}$, since this would imply that $\correcttally$ is computed on sets of corresponding ballots in both the external and internal authentication setting.
\begin{comment}
\textcolor{blue}{BEN:I can't follow it. There's a jump between authorized and auth*, how does that work?}
\textcolor{orange}{LIZ: authorized is the set of full ballots, while auth* is the set of ballots output by the underlying Vote algorithm.}
\end{comment}
\iftr We proceed the proof as follows.\fi
\begin{itemize}
\begin{sloppypar}
\item $auth^*(\pk,\nC,\bbb,\electoralrollprivate,\kappa)\setminus\{\perp\} \subseteq \mathsf{auth}(\bbb,\electoralroll)\setminus\{\perp\}$
If $b^* \in auth^*(\pk,\nC,\bbb,\electoralrollprivate,\kappa)$, then $b^* \neq \ \perp$ and there exists $b \in \authorized(\allowbreak\pk,\allowbreak \nC,\bbb,\electoralrollprivate,\kappa)$ such that\iftr:\fi\
%
\iftr
\begin{enumerate}
\fi
\iftr\item\label{item:soundness:i}\else (i) \fi
$b \in \bb$;
%
\iftr\item\else (ii) \fi
$\exists \pd,\sd, v, r,r',r'' \mathrel : b = (\pd,b^*,\sigma,\tau)$, $b^* = \VoteSymb_\Gamma(\pk,\nC,v,\kappa;r)$,
$\sigma = \SgnSymb_\Omega(\sd,b^*;r')$, and
$\tau = \ProveSymb_\Sigma((\pk,\allowbreak b^*,\allowbreak\sigma,\allowbreak\nC,\allowbreak\kappa),\allowbreak(v,\allowbreak r,\allowbreak\sd,\allowbreak r'),\allowbreak\kappa; r'')$,
which\iftr, \else\ -- \fi by correctness of $\Omega$ and completeness of $\Sigma$\iftr, \else\ -- \fi implies $\VerifySymb_\Omega(\pd,\allowbreak b^*, \sigma) =1$ and $\VerifySymb_\Sigma((\pk, \allowbreak b^*, \nC, \kappa), \tau, \kappa))=1$;
%
\iftr\item\else (iii) \fi
$ (\pd,\sd)\in\electoralrollprivate$, which implies $\pd\in\electoralroll$ by construction; and
%
\iftr\item\label{item:soundness:iv}\else (iv) \fi
$\neg \exists b', v', r,r',r'' \mathrel : b' \in (\bbb \setminus \{b\}) \land b' = (\pd, b^{*'}, \sigma', \tau')$,
$b^{*'} = \VoteSymb_\Gamma(\pk,\nC,v',\kappa;r)$, $\sigma' = \SgnSymb_\Omega(\sd,b^{*'};r')$, and
$\tau' = \ProveSymb_\Sigma((\pk,b^{*'},\allowbreak \sigma',\nC,\kappa),(v',r,\sd,r'),\kappa; r'')$,
which, by correctness of $\Omega$, implies $\VerifySymb_\Omega(\allowbreak\pd,\allowbreak b^{*'}, \sigma') =1$.
%
\iftr
\end{enumerate}
\fi
%
It follows by \iftr (\ref{item:soundness:i})--(\ref{item:soundness:iv}) \else
(i)--(iv) \fi
that $b^* \in auth^*(\pk,\nC,\bbb,\electoralrollprivate,\kappa)$ implies $b^* \in \mathsf{auth}(\bbb,\electoralroll)\setminus\{\perp\}$.
\end{sloppypar}
\item $ \mathsf{auth}(\bbb,\electoralroll)\setminus\{\perp\} \subseteq auth^*(\pk,\nC,\bbb,\electoralrollprivate,\kappa)\setminus\{\perp\}$
If $b^* \in \mathsf{auth}(\bbb,\electoralroll)\setminus\{\perp\}$, then $b^* \neq \ \perp$ such that\iftr:\fi\
%
\iftr
\begin{enumerate}
\fi
\iftr\item\else (i) \fi
$(\pd, b^*, \sigma, \tau) \in \bb$;
%
\iftr\item\else (ii) \fi
$\VerifySymb_\Omega(\pd,\allowbreak b^*, \sigma) =1$ and $\VerifySymb_\Sigma((\pk, \allowbreak b^*, \nC, \kappa), \tau, \kappa))=1$, which\iftr, \else\ -- \fi by the security of $\Omega$ and $\Sigma$\iftr, \else\ -- \fi implies $\exists \pd,\sd, v, r,r',r'' \mathrel : $
$b^* = \VoteSymb_\Gamma(\pk,\nC,v,\kappa;r)$,
$\sigma = \SgnSymb_\Omega(\sd,b^*;r')$, and $\tau = \ProveSymb_\Sigma((\pk,b^*,\sigma,\nC,\kappa),\allowbreak(v,r,\sd,r'),\kappa; r'')$. Indeed, suppose this is not true, i.e., such values do not exist. Then $(b^*, \sigma)$ and $((\pk, b^*, \nC, \kappa), \tau)$ could be used by adversaries to break the unforgeability property of $\Omega$ and the \SufficientConditionOnSignaturesSigma\ property of $\Sigma$, respectively.
%
\iftr\item\else Furthermore, we have (iii) \fi
$\pd\in\electoralroll$, which implies $ (\pd,\sd)\in\electoralrollprivate$ by construction; and
%
\iftr\item\else (iv) \fi
$b' = (\pd, b^{*'}, \sigma', \tau') \notin (\bbb \setminus \{(\pd, b^*, \sigma, \tau)\}) \land \VerifySymb_\Omega(\pd,\allowbreak b^{*'}, \sigma') =1$, which implies $\neg \exists b', v', r,r',r'' \mathrel : b' \in (\bbb \setminus \{b\}) \land b' = (\pd, b^{*'}, \sigma', \tau')$, $b^{*'} = \VoteSymb_\Gamma(\pk,\nC,v',\kappa;r)$, $\sigma' = \SgnSymb_\Omega(\sd,b^{*'};r')$, and $\tau' = \ProveSymb_\Sigma((\pk,\allowbreak b^{*'},\allowbreak\sigma',\allowbreak\nC,\allowbreak\kappa),\allowbreak (v',\allowbreak r,\allowbreak\sd,\allowbreak r'),\allowbreak\kappa;\allowbreak r'')$, as per definition of $\authorized$, concluding our proof.\qedhere
\iftr
\end{enumerate}
\fi
\end{itemize}
\end{proof}
%\iftr
\subsection{Eligibility verifiability}
%\fi
\begin{definition}[Eligibility verifiability\cite{Smyth15:ElectionVerifiability}]
Let $\Gamma = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerifySymb)$ be an election scheme with internal authentication, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpEVV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpEVV$}
$(\pk,\nV) \leftarrow \adv(\kappa)$\;
\lFor{$1 \leq i \leq \nV$}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$}
$\electoralroll \leftarrow \{\pd_1,\dots,\pd_{\nV}\}$\;
$\mathit{Crpt}\leftarrow\emptyset;~\mathit{Rvld}\leftarrow\emptyset$\;
$(\nC,v,i,b)\leftarrow \adv^{\corruptOracle,\revealOracle}(\electoralroll)$\;
\eIf{$\exists r \mathrel :
b=\Vote[\sd_i,\pk,\nC]{v,\kappa; r}
\mathrel\wedge b \not= {\perp}
\mathrel\wedge b\not\in \mathit{Rvld}
\mathrel\wedge \sd_i \not\in \mathit{Crpt}$
} {
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
Oracle $\corruptOracle$ is the same oracle as in $\ExpIVVSymb$, and
oracle $\revealOracle$ is defined such that $\revealOracle(i,v, \allowbreak \nC)$ computes $b \leftarrow \Vote[\sd_i,\pk,\nC]{v,k};\mathit{Rvld}\leftarrow\mathit{Rvld} \cup \{b\}$ and outputs $b$.
We say $\Gamma$ satisfies $\ExpEVVSymb$,
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have $\SuccEVV \leq \mathsf{negl}(\kappa)$.
\end{definition}
%\subsubsection{Our construction ensures eligibility verifiability}
\begin{comment}
\textcolor{red}{LIZ: The KEY revelation here is that the primitive we need is not a signature scheme, but an \textbf{identity-based signature scheme}. Intuitively, identities correspond to credentials, which can be corrupted and for which signatures can be queried in their standard security model. BEN: I don't see why signature schemes are insufficient. Surely we want to remain general and prove for signature schemes?}
\end{comment}
\begin{lemma}\label{lem:simpleSignSchemeIVEV}
Let $\Gamma = (\SetupSymb_\Gamma, \VoteSymb_\Gamma, \TallySymb_\Gamma, \VerifySymb_\Gamma)$ be an election scheme with external authentication,
$\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$ be a digital signature scheme,
$\Sigma$ be a sigma protocol for relation $R(\Gamma,\Omega)$,
and $\mathcal H$ be a hash function.
Suppose $\Sigma$ satisfies \SufficientConditionOnSignaturesSigma,
and $\Omega$ satisfies strong unforgeability.
Election scheme with internal authentication
$\Trans(\Gamma,\Omega,\Sigma,\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$
satisfies $\ExpEVVSymb$.
\end{lemma}
%\textcolor{red}{LIZ: For the standars definition of identity-based signature scheme and corresponding security notion please refer to https://eprint.iacr.org/2006/080.pdf Section 2.\\
%Of course, if we agree this is the primitive we are going to use, then we will put these details in Appendix A and update things as needed, for instance, adding the public credential to the input of $\Omega$'s signing algorithm.}
\begin{proof}
Suppose $\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H)$ does not satisfy $\ExpEVVSymb$, i.e., there exists an adversary $\adv$
such that for all negligible functions $\mathsf{negl}$ there exists a security parameter $\kappa$
and $\SuccEVV > \mathsf{negl}(\kappa)$.
%
\begin{comment}
This adversary can be used to construct an adversary $\Adv$
against the strong unforgeability of $\Omega$.
Let $\Gamma = (\SetupSymb_\Gamma, \VoteSymb_\Gamma, \TallySymb_\Gamma, \VerifySymb_\Gamma)$,
$\Omega = (\GGenSymb_\Omega,\allowbreak\SgnSymb_\Omega,\allowbreak\VrfySymb_\Omega)$,
$\sFS{\Sigma}{\allowbreak\mathcal H} = (\ProveSymb_\Sigma, \VerSymb_\Sigma)$, and
$\Trans(\Gamma,\allowbreak\Omega,\allowbreak\Sigma,\allowbreak\mathcal H) = (\SetupSymb,\allowbreak\RegisterSymb,\allowbreak \VoteSymb,\allowbreak \TallySymb,\allowbreak \VerifySymb)$.
By \SSE, non-interactive proof system $(\ProveSymb_\Sigma, \VerSymb_\Sigma)$
satisfies zero-knowledge, i.e., there exists a simulator for $(\ProveSymb_\Sigma, \VerifySymb_\Sigma)$. Let
$\mathcal S$ be such a simulator. We define $\Adv$ as follows:
\end{comment}
%
% BEN: I pushed most of the lets into the lemma's statement.
% There seems no need for (\ProveSymb_\Sigma, \VerSymb_\Sigma),
% so I dropped.
% I pushed discussion of the simulator into the oracle definition.
%
We construct the following adversary $\Adv$
against the strong unforgeability of $\Omega$ from $\adv$.
\begin{comment}
\begin{itemize}
\item $\Adv^{\oracleSymb}(\pd,\kappa)$ proceeds as follows.
Adversary $\Adv$ runs $(\pk,\nV) \leftarrow \adv(\kappa),$ and draws $i^*\leftarrow \{1, ..., \nV \}$ at random and sets $\pd_{i^*} \leftarrow \pd$. It then computes
{\DontPrintSemicolon\llFor{$ i \in \{1, ..., \nV\}\setminus \{ i^* \} $}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa];$}}
computes
$\electoralroll \leftarrow \{\pd_{1},\dots,\pd_{\nV}\};\mathit{Rvld}, \mathit{Crpt} \leftarrow \emptyset;
(\nC, v, i, b) \leftarrow \adv^{C,R}(L)$, handling oracle calls from $\adv$ as follows.
\begin{itemize}
\item Given an oracle call $C(i)$, if $i=i^*$, then $\Adv$ aborts, otherwise, it computes $\mathit{Crpt} \leftarrow \mathit{Crpt} \cup \{ \sd_i \}$ and returns $\sd_i$ to $\adv$.
\item Given an oracle call $R(i, v,\nC)$, if $i=i^*$, then $\Adv$ computes $b^* \leftarrow \VoteSymb_\Gamma(\allowbreak\pk,\allowbreak \nC,\allowbreak v,\allowbreak\kappa);\allowbreak \sigma \leftarrow \oracleSymb(b^*)$, simulates proof $\tau$, computes $\mathit{Rvld} \leftarrow \mathit{Rvld} \cup \{ (\pd_i, b^*, \sigma, \tau)\}$, and returns $(\pd_i, b^*, \sigma, \tau)$.
Otherwise, $\Adv$ computes $b \leftarrow \VoteSymb(\sd_i, \pk, \nC, v, \kappa);\mathit{Rvld} \leftarrow \mathit{Rvld} \cup \{ b\}$ and returns $b$.
\end{itemize}
Adversary $\Adv$ parses $b$ as $(\pd_i, b^*,\sigma, \tau)$. If
$i=i^*$, then $\Adv$ outputs $(b^*,\sigma)$, otherwise $\Adv$ aborts
We denote by $\textsf{Good}$ the event that $i=i^*$.
\end{itemize}
\end{comment}
\begin{inlineexperiment}{$\Adv(\pd,\kappa)$}
$(\pk,\nV) \leftarrow \adv(\kappa)$\;
$i^*\leftarrow_R \{1, ..., \nV \}$\;
%$\pd_{i^*} \leftarrow \pd$\;
%{\DontPrintSemicolon
\llFor{$ i \in \{1, ..., \nV\}\setminus \{ i^* \} $}{$(\pd_i,\sd_i) \leftarrow \Register[\pk,\kappa]$}
%}
%$\electoralroll \leftarrow \{\pd_{1},\dots,\pd_{\nV}\}$\;
$\mathit{Rvld}\leftarrow \emptyset; \mathit{Crpt} \leftarrow \emptyset$\;
%$(\nC, v, i, b) \leftarrow \adv^{C,R}(\{\pd_{1},\dots,\pd_{\nV}\})$\;
$(\nC, v, i, b) \leftarrow \adv^{C,R}(\{\pd_{1},\dots,\pd_{i^*-1},\pd,\pd_{i^*+1},\dots,\pd_{\nV}\})$\;
%\eIf{$b[1] = \pd_{i^*}$}{
\eIf{$b[1] = \pd$}{
\Return $(b[2],b[3])$\;
}{
\Abort\;
}
\end{inlineexperiment}
\noindent
where oracle calls are handled as follows:
\begin{itemize}
\item
%\sout{Given an oracle call $C(i)$, if $i=i^*$, then $\Adv$ aborts, otherwise, it computes $\mathit{Crpt} \leftarrow \mathit{Crpt} \cup \{ \sd_i \}$ and returns $\sd_i$ to $\adv$.}
%\textcolor{red}{BEN: I think we can just write:}\\
$C(i)$ computes $\mathit{Crpt} \leftarrow \mathit{Crpt} \cup \{ \sd_i \}$ and returns $\sd_i$, if $i\not=i^*$ and aborts otherwise.
\item $R(i, v,\nC)$ distinguishes two cases: If $i=i^*$, then $\Adv$ computes $b \leftarrow \VoteSymb_\Gamma(\allowbreak\pk,\allowbreak \nC,\allowbreak v,\allowbreak\kappa);\allowbreak \sigma \leftarrow \oracleSymb(b);\tau\leftarrow \mathcal S((\pk,b,\sigma,\nC,\kappa),\kappa)$,
computes $\mathit{Rvld} \leftarrow \mathit{Rvld} \cup \{ (\pd, b, \sigma, \tau)\}$,
and returns $(\pd, b, \sigma, \tau)$, where $\mathcal S$ is a simulator for $\sFS{\Sigma}{\allowbreak\mathcal H}$ that exists by \SSE.
Otherwise, $\Adv$ computes $b \leftarrow \VoteSymb(\sd_i, \pk, \nC, v, \kappa)$, $\mathit{Rvld} \leftarrow \mathit{Rvld} \cup \{ b\}$ and returns $b$.
%\textcolor{red}{BEN: There seems no need to track $\mathit{Rvld}$.}
\end{itemize}
\noindent
We prove that $\Adv$ wins the strong unforgeability game against $\Omega$.
%It is easy to see that, if $\Adv$ does not abort, then $\Adv$ simulates the correct environment for $\adv$.
%Hence, $\Adv$ outputs a winning tuple for the strong unforgeability game with the same probability with which $\adv$ wins (which, by assumption, is non-negligible).
Let $\kk$ be a security parameter. Suppose $(\pd,\sd)$ is an output of $\GGen[\kk]$
and $(\pk,\nV)$ is an output of $\adv(\kappa)$. Let $i^*$ be an integer chosen
uniformaly at random from $\{1, ..., \nV \}$. Suppose $(\pd_i,\sd_i)$ is an output
of $\Register[\pk,\kappa]$, for each $i \in \{1, ..., \nV\}\setminus \{ i^* \} $.
Let us consider an execution of $\adv(\{\pd_{1},\allowbreak\dots,\allowbreak\pd_{i^*-1},\allowbreak\pd,\allowbreak\pd_{i^*+1},\allowbreak\dots,\allowbreak\pd_{\nV}\})$. Let $(\nC, v, i, b)$ be the output of $\adv$.
By definition of algorithm $\RegisterSymb$,
it is trivial to see that $\Adv$ simulates $\adv$'s challenger to $\adv$. Moreover,
$\Adv$ simulates oracle $C$ to $\adv$, except when $\Adv$ aborts. Furthermore,
$\Adv$ simulates oracle $R$ to $\adv$ as well. In particular, simulator $\mathcal S$
produces proofs that are indistinguishable from proofs constructed by non-interactive
proof system $\sFS{\Sigma}{\allowbreak\mathcal H}$.
We denote by $\textsf{Good}$ the event that $i=i^* $.
Now, let us assess $\Adv$'s probability not to abort, to determine the success probability of $\Adv$. Since $\adv$ is not allowed to corrupt the credential it finally outputs (as $\adv$ is a winning adversary, $\sd_{i} \notin \mathit{Crpt}$ must hold), a sufficient condition for $\Adv$ not to be asked for the unknown private credential $\sd_i$ is to be lucky when drawing $i^*\leftarrow \{1, ..., \nV \}$ at random and have event $\textsf{Good}$ occurring.
This is the case with probability $\Pr [\textsf{Good}] = \frac{1}{\nV}$ since the choice of $i^*$ is completely independent of $\adv$'s view.
Therefore we have
\iftr\[\else$\fi
\SuccEVV \leq \nV \cdot \textsf{Succ}(\Exp\text{-}\mathsf{StrongSign}(\Omega,\Adv,k))
\iftr, \] thereby concluding our proof\else$\fi.
%
\begin{comment}
The above is just a simple probability calculation.
If $A \land B $ imply $C$, then $\Pr[A \land B] \leq \Pr[C]$
\end{comment}
%
%\textcolor{purple}{LIZ: This is the exact same line of reasoning I did years ago in my broadcast encryption paper - good that I reminded myself!}
%
\end{proof}
\begin{comment}
\ifnotes
\textcolor{red}{There might need to be some reasoning somewhere that $\Adv$ doesn't get the signed ballot from its oracle.} \textcolor{orange}{This comment is not clear to me.} \textcolor{red}{$b$ cannot be an output of $R$, I think. (I read this over a month ago.)}\textcolor{orange}{Yes, I will reinstate Rvld, that for some reason you thought was not needed.}
\textcolor{red}{LIZ: Do we want to mention the whole identity-based part? And where/how?}\\
\textcolor{blue}{BEN: I suggest mentioning if you have a solution (or partial solution)
and you're motivated to add discussion on it. From what I recall it was an interesting
crypto point. If you aren't motivated to add discussion, then don't mention it.}
\fi
\textcolor{red}{LIZ 09/01/18: Is it interesting? From a theoretical perspective, it is a cute observation that internal authentication and eligibility verifiability are mirrored in the IBE world. But would anyone consider developing a new voting scheme based on IBE? If so, then I think it is worth looking into this but with a wider scope, i.e., a whole new paper. So I would not give it away here. These are my thoughts.
\end{comment}
%\input{app-helios}
\bibliographystyle{splncs03}
%\bibliographystyle{alpha}
\bibliography{main-heliosc}
```
[^1]: Quaglia & Smyth (**Smyth17:voting-tutorial?**) provide a tutorial-style introduction to definitions of ballot secrecy and election verifiability, and Smyth (**Smyth18:voting-tutorial?**) provides a technical introduction.
[^2]: , accessed 3 Apr 2013.
[^3]: , accessed 13 Jul 2017.
[^4]: , accessed 8 Feb 2013.
[^5]: Beyond secrecy and verifiability, attacks against eligibility are also known (**2013-truncation-attacks-to-violate-beliefs?**; **Smyth16:helios-eligibility?**).
[^6]: Ballot blocking violates the recorded-as-cast assumption used in Cortier *et al.*’s proof.
[^7]: Smyth (**Smyth18:HeliosMixnetVerifiability?**) shows that vulnerabilities in Helios cause vulnerabilities in implementations of the mixnet variant and proves verifiability is satisfied when a fix is applied.