# Secret, verifiable auctions from elections (Technical Report)
## Abstract
Auctions and elections are seemingly disjoint. Nevertheless, similar cryptographic primitives are used in both domains. For instance, mixnets, homomorphic encryption and trapdoor bit-commitments have been used by state-of-the-art schemes in both domains. These developments have appeared independently. For example, the adoption of mixnets in elections preceded a similar adoption in auctions by over two decades. In this paper, we demonstrate a relation between auctions and elections: we present a generic construction for auctions from election schemes. Moreover, we show that the construction guarantees secrecy and verifiability, assuming the underlying election scheme satisfies analogous security properties. We demonstrate the applicability of our work by deriving auction schemes from the Helios family of election schemes. Our results advance the unification of auctions and elections, thereby facilitating the progression of both domains.
#### Keywords.
Auctions, elections, privacy, secrecy, verifiability.
# Introduction
We present a construction for auction schemes from election schemes, and prove the construction guarantees security, assuming the underlying election scheme is secure.
#### Auctions.
An auction is a process for the trade of goods and services from sellers to bidders (**Krishna09:Auctions?**; **McAfee87:Auctions?**), with the support of an auctioneer. We study first-price sealed-bid auctions (**brandt2009auctions?**), whereby bidders create bids which encapsulate the price they are willing to pay, and the auctioneer opens the bids to determine the winning price (namely, the highest price bid) and winning bidder.
#### Elections.
An election is a decision-making procedure used by voters to choose a representative from some candidates (**Gumbel05:StealThisVote?**; **Alvarez10:ElectronicElections?**), with the support of a tallier. We study first-past-the-post secret ballot elections (**Lijphart84?**; **Saalfeld95?**), which are defined as follows. First, each voter creates a ballot which encapsulates the voter’s chosen candidate (i.e., the voter’s vote). Secondly, all ballots are tallied by the tallier to derive the distribution of votes. Finally, the representative – namely, the candidate with the most votes – is announced.
Bidders and voters should express their choice freely in auctions and elections; this can be achieved by participating in private (**OSCE:HumanRights?**; **ShermanAct?**; **UN:HumanRights?**; **OAS:HumanRights?**), which has led to the emergence of the following requirements.
- Bid secrecy: A losing bidder cannot be linked to a price.
- Ballot secrecy: A voter cannot be linked to a vote.
Ballot secrecy aims to protect the privacy of all voters, whereas bid secrecy is only intended to protect the privacy of losing bidders. This intuitive weakening is necessary, because the auctioneer reveals the winning price and winning bidder, hence, a winning bidder can be linked to the winning price.
Bidders and voters should be able to check that auctions and elections are run correctly (**JCJ02?**; **DagstuhlAccord07?**; **ChaumRyanSchneider2005?**; **BenAdidaThesis?**; **Adida08?**; **Dreier13:VerifiableAuctions?**); this is known as *verifiability*. Sometimes we write *auction verifiability* and *election verifiability* to distinguish verifiability in each field.
Kremer, Ryan & Smyth (**Smyth10:ElectionVerifiability?**) decompose verifiability
into the following properties.
- Individual verifiability: bidders/voters can check whether their bid/ballot is included.
- Universal verifiability: anyone can check whether the result is computed properly.
Conceptually, individual and universal verifiability do not differ between auctions and elections.
## Constructing auctions from elections
Our construction for auction schemes from election schemes works as follows.
1. We represent prices as candidates, and instruct bidders to create bids by “voting” for the candidate that represents the price they are willing to pay.
2. Bids are “tallied” to derive the distribution of prices and the winning price is determined from this distribution.
The relation between auctions and elections is so far straightforward. The challenge is to establish the winning bidder. This is non-trivial, because election schemes satisfying ballot secrecy ensure voters cannot be linked to votes, hence, the bidder mentioned above cannot be linked to the price they are willing to pay. We overcome this by extending the tallier’s role to additionally reveal the set of ballots for a specific vote,[^1] and exploit this extension to complete the final step.
3. The tallier determines the winning bids and a winning bidder can be selected from these bids.[^2]
Extending the tallier’s role is central to our construction.
## Motivation and related work
There is an abundance of rich research on elections which can be capitalised upon to advance auctions.
This statement can be justified with hindsight:
Chaum (**Chaum:1981?**) exploited mixnets in elections twenty-three years before Peng *et al.* (**peng2004efficient?**) made similar advances in auctions (Jakobsson & Juels (**jakobsson2000mix?**) use mixnets in a distinct way from Chaum and Peng *et al.*), Benaloh & Fischer (**Benaloh85?**) proposed using homomorphic encryption seventeen years before Abe & Suzuki (**abe2002m+?**), and Okamoto (**Oka96?**) demonstrated the use of trapdoor bit-commitments six years before Abe & Suzuki (**abe2002receipt?**).
Magkos, Alexandris & Chrissikopoulos (**Emmanouil02?**) and Her, Imamot & Sakurai (**her2005analysis?**) have studied the relation between auctions and elections.
Magkos, Alexandris & Chrissikopoulos remark that auctions and elections have a similar structure and share similar security properties. And Her, Imamot & Sakurai contrast privacy properties of auctions and elections, and compare the use of homomorphic encryption and mixnets between fields. More concretely, McCarthy, Smyth & Quaglia (**2014-Hawk-and-Aucitas-auction-schemes?**) derive auction schemes from the Helios and Civitas election schemes. And Lipmaa, Asokan & Niemi study the converse (**Lipmaa02:auctionToVoting?**).
## Contribution
We *formally* demonstrate a relation between auctions and elections: we present a generic construction for auction schemes from election schemes, moreover, we prove that auction schemes produced by our construction satisfy bid secrecy and auction verifiability, assuming the underlying election scheme satisfies ballot secrecy and election verifiability. To achieve this, we formalise syntax and security definitions for auction schemes, since these are prerequisites to rigorous, formal results.
#### Summary of contributions and paper structure.
We summarise our contributions as follows.
- We propose auction scheme syntax, and the first computational security definitions of bid secrecy and verifiability for auctions (§2).
- We present a construction for auction schemes from election schemes (§3).
- We prove that our construction guarantees bid secrecy (§4) and verifiability (§5), assuming the underlying election scheme satisfies analogous security properties.
- We show that our construction is applicable to a large class of election schemes and justify our choice of security definitions (§6).
- We use our construction to derive auction schemes from the Helios family of election schemes (§7).
- We define cryptographic primitives and relevant security definitions in Appendix [sec:crypto], and we present further supplementary material in the remaining appendices.
It follows from our results that secure auction schemes can be constructed from election schemes, allowing advances in election schemes to be capitalised upon to advance auction schemes.
## Comparison with McCarthy, Smyth & Quaglia
The idea underlying our construction was introduced by McCarthy, Smyth & Quaglia (**2014-Hawk-and-Aucitas-auction-schemes?**). Our contributions improve upon their work by providing a strong theoretical foundation to their idea. In particular, we provide a generic construction for auction schemes from election schemes, they consider the derivation of only two auction schemes from Helios and Civitas. We prove that auction schemes produced by our construction satisfy bid secrecy and verifiability, they do not provide security proofs. Thus, the auction schemes we construct from Helios satisfy bid secrecy and verifiability, whereas the auction schemes they derive have no such proofs. Moreover, we are the first to introduce computational security definitions of bid secrecy and auction verifiability.
# Auction schemes
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 446, column 1): unexpected } expecting \end{definition} \end{inlineexperiment} ^`
``` latex
\section{Auction schemes}
\newcommand{\syntaxComparision}{Our proposed syntax is based upon syntax by McCarthy, Smyth \& Quaglia \cite{2014-Hawk-and-Aucitas-auction-schemes}.\ifnocompress\ Moreover, our correctness, completeness and injectivity properties are based upon similar properties of election schemes. \ifnocompress(Cf. Section~\ref{sec:elections:syntax}.)\fi\fi}
\ifnocompress
\subsection{Syntax}
\fi
We formulate syntax for \emph{auction schemes}, %\ifnocompress\else\footnote{\syntaxComparision}\fi\
which capture the class of auctions that consist of the following four steps.
First, an auctioneer generates a key pair. Secondly, each bidder constructs and casts a bid
for their price. These bids are recorded on a bulletin board. Thirdly, the auctioneer opens the recorded
bids and announces the winning price and the winning bids, i.e., bids that contain the winning
price. Finally, bidders and other interested parties check that the result corresponds to
the recorded bids.
%\marginpar{Setup should output a proof. Bid should take the proof as input. Also, I suggest calling the proofs ``proofs" rather than ``auxilliary data."}
\begin{definition}[Auction scheme]\label{def:b-auction}
%\marginpar{BEN: Objections have risen regarding our syntax. I see absolutely nothing wrong with it, except the upper-bound on $\nP$. This could be addressed in part by introducing and motivating \emph{price flexibility}, and by explaining that some schemes forego price flexibility for efficiency.}
%
An \emph{auction scheme} is a tuple of efficient algorithms $(\SetupSymb,\BidSymb,\OpenSymb,\VerSymb)$ such that:
\begin{description}
\item $\SetupSymb$, denoted\footnotemark\ $(\pk,\sk,\mB,\mP)\leftarrow\Setup$,%
%
\footnotetext{Let $A(x_1,\dots,x_n; r)$ denote the output of probabilistic algorithm $A$ on inputs $x_1,\dots,x_n$ and coins $r$.
Let $A(x_1,\dots,x_n)$ denote $A(x_1,\dots,x_n;r)$, where $r$ is chosen uniformly at random.
And let $\leftarrow$ denote assignment.}
%
is run by the auctioneer,
%\ifnocompress{}\footnotemark\fi.
%
%\ifnocompress{}\footnotetext{\sout{Some auction schemes permit the auctioneer's role to be distributed amongst several auctioneers. For simplicity, we consider only a single auctioneer in this paper. Generalising syntax and security definitions to multiple auctioneers is a possible direction for future work. Similarly, we consider only a single tallier in election schemes.}
%}\fi%
%
$\SetupSymb$ takes a security parameter $\kappa$ as input and outputs a key pair
$\pk,\sk$, a maximum number of bids $\mB$,
and a maximum price $\mP$.
%\footnotetext{\textcolor{blue}{\sout{The auctioneer is implicitly assumed to be trusted throughout this paper, in particular, the auctioneer is assumed not to disclose the contents of individual bids. Generalising this work to multiple auctioneers is a possible direction for future work.}}}
\item $\BidSymb$, denoted $b\leftarrow\BidSymb{(\pk\ifincludeVerify,\kpf\fi, \nP, p, \kappa)}$,
is run by bidders. $\BidSymb$ takes as input a public key $\pk$\ifincludeVerify, a proof $\kpf$\fi, an upper-bound $\nP$ on the range of biddable prices,\footnote{An upper-bound on the range of biddable prices is sometimes useful for efficiency reasons, as can be observed from our case studies (\S\ref{sec:helios}).} a bidder's chosen price $p$,
and a security parameter $\kappa$.
A bidder's price should be selected from the range $1,\dots,\nP$ of
prices.
$\BidSymb$ outputs a bid $b$ or error symbol $\perp$.
\item $\OpenSymb$, denoted $(p, \mathfrak{b}, \tpf) \leftarrow \OpenSymb(\sk, \nP, \bb, \kappa)$,
is run by the auctioneer. $\OpenSymb$ takes as input a private key $\sk$,
an upper-bound $\nP$ on the range of biddable prices, a bulletin board $\bb$,
and a security parameter $\kappa$, where $\bb$ is a set.
It outputs a (winning) price $p$, a set of (winning) bids $\mathfrak{b}$, and a non-interactive proof $\tpf$ of correct opening.
%\footnotetext{Here, a range is of the form $\[1, ..., \nP \]$.}
\item $\VerSymb$, denoted $s \leftarrow \VerSymb(\pk\ifincludeVerify,
\kpf\fi,\nP, \bb, p, \mathfrak{b}, \tpf, \kappa)$, is run to audit an auction.
It takes as input a public key $\pk$,
an upper-bound $\nP$ on the range of biddable prices,
a bulletin board $\bb$,
a price $p$, a set of bids $\mathfrak{b}$,
a proof $\tpf$, and a security parameter $\kappa$.
It outputs a bit $s$, which is $1$
if the auction verifies successfully
and $0$ otherwise.
\ifincludeVerify
\textcolor{red}{BEN please check Verify I am not convinced have not given it too much thought at the mo}
\item $\VerSymb$, denoted $\beta \leftarrow \VerSymb(\pk\ifincludeVerify, \kpf\fi, \bb, \nP, p, b, \tpf)$,
takes as input a public key $\pk$\ifincludeVerify, a proof $\kpf$\fi, a bulletin board $\bb$, some range of biddable prices $\nP$, a winning price $p$,
a winning bib $b$, and a proof $\tpf$. It outputs a bit $\beta$ equal to $1$ if successful or $0$ to denote failure.
\fi
\end{description}
\noindent
Auction schemes must satisfy \emph{correctness}, \emph{completeness}, and
\emph{injectivity}, which we define in \refappendix{\ref{cciforauc}}.
\end{definition}
\ifnocompress
\syntaxComparision
\fi
\ifnocompress
\subsubsection{Example: $\mathsf{Enc2Bid}$}\label{sec:auctions:example}
\iffalse \textcolor{red}{BEN: The term $\mathsf{Enc2Bid}$ does not correspond to $\mathsf{Enc2Vote}$; $\mathsf{Enc2Price}$ does, and so does $\mathsf{Enc2Bid}$. Similarly, $\mathsf{Enc2Bid}$ corresponds to $\mathsf{Enc2Ballot}$}
\textcolor{blue}{LIZ: I disagree. As fas as I understand $\mathsf{Enc2Vote}$ stands for \emph{encrypt to vote} - both verbs (it does not stand for \emph{encrypt your vote}, in which case it would be verb+noun).
So $\mathsf{Enc2Bid}$, meaning encrypt to bid,
corresponds in my opinion to $\mathsf{Enc2Vote}$ since encrypt and bid are both verbs. Furthermore, it is also sound pleasing.}
\textcolor{red}{BEN: Our syntax assigns a technical meaning to ballot and bid... Perhaps this doesn't matter.} \fi
We demonstrate the applicability of our syntax with a construction ($\mathsf{Enc2Bid}$)
for auction schemes from asymmetric encryption schemes.%\footnotemark
%\footnotetext{\iftr{}We present definitions of cryptographic primitives and relevant security definitions in
% \refappendix{\ref{sec:crypto}}.\else{}We adopt standard definitions of cryptographic primitives and security definitions throughout; we omit recalling them for brevity. See \refappendix{\ref{sec:crypto}} for details.\fi}
%\footnotetext{We present definitions of cryptographic primitives and relevant security definitions in \refappendix{\ref{sec:crypto}}.}
\begin{definition}[$\mathsf{Enc2Bid}$]\label{def:Enc2Bid}
Given an asymmetric encryption scheme $\Pi = (\GGenSymb,\allowbreak\EEncSymb,\DDecSymb)$,
we define $\mathsf{Enc2Bid}(\Pi)$ as follows.
\begin{itemize}
\item $\Setup$ computes $(\pk,\sk)\leftarrow\GGen$ and outputs $(\pk,\allowbreak\sk,\allowbreak\textit{poly}(\kappa),|\votespace|)$.
\item $\BidSymb(\pk,\nP,p,\kappa)$ computes $b\leftarrow\EEnc{p}$ and outputs $b$ if $1\leq p \leq \nP\leq|\votespace|$
and $\perp$ otherwise.
\item $\OpenSymb(\sk, \nP, \bb,\kappa)$ proceeds as follows.
Computes $\mathfrak{d} \leftarrow \{(b,\DDec{b}) \mid b\in\bb\}$.
Finds the largest integer $p$ such that $(b,p)\in\mathfrak{d}\wedge1\leq p\leq \nP$, outputting $(0,\emptyset,\epsilon)$ if no such integer exists.
Computes $\mathfrak b \leftarrow \{b \mid (b,p')\in\mathfrak d \wedge p' = p\}$.
Outputs $(p,\mathfrak b,\epsilon)$.
\item $\VerSymb(\pk,\nP,\bb,p,\mathfrak b,\tpf,\kappa)$ outputs 1.
\end{itemize}
\noindent Algorithm $\SetupSymb$ requires $\textit{poly}$ to be a polynomial function,
algorithms $\SetupSymb$ and $\BidSymb$ require $\mathfrak m = \{1,\dots,|\mathfrak m|\}$
to be the encryption scheme's plaintext space, and algorithm $\OpenSymb$ requires $\epsilon$
to be a constant symbol.
\end{definition}
\noindent
To ensure $\mathsf{Enc2Bid}(\Pi)$ is an auction scheme, we require asymmetric
encryption scheme $\Pi$ to produce distinct ciphertexts with overwhelming
probability. Hence, we must restrict the class of asymmetric encryption
schemes used to instantiate $\mathsf{Enc2Bid}$. We could consider a broad
class of schemes that produce distinct ciphertexts with overwhelming
probability, but we favour the narrower class of schemes satisfying
$\INDCPA$, because we require $\INDPA$ (which implies $\INDCPA$) for
bid secrecy.
\begin{lemma}\label{lemma:Enc2Bid:correctness}
Suppose $\Pi$ is an asymmetric encryption scheme with
perfect correctness that satisfies
$\INDCPA$. We have $\mathsf{Enc2Bid}(\Pi)$ is an
auction scheme (i.e., correctness, completeness and
injectivity are satisfied).
\end{lemma}
\noindent The proof of Lemma~\ref{lemma:Enc2Bid:correctness} and all
further proofs, except where otherwise stated, appear in
\refappendix{\ref{sec:proofs}}.
\fi
\subsection{Bid secrecy}\label{sec:bid:section}
%\marginpar{BEN: I think we need to address issues raised regarding bid secrecy.
%As a first step, we could probably provide a better introduction to the defintion.
%As a second step, we need to justify that it is a ``reasonable" definition, that
%can perhaps be achieved by explaining that the notion is used elsewhere.}
Our informal definition of bid secrecy (\S\ref{sec:intro}) omits a side condition
which is necessary for satisfiability. In particular, we did not stress that a losing bidder
can be linked to a price when a link can be deduced from the winning bidder and knowledge
about the distribution of prices bidders are willing to pay. For example, suppose Alice,
Bob and Charlie participate in an auction and Alice wins. Bob and Charlie can both
deduce the price the other is willing to pay. Accordingly, our definitions must concede
that auction results reveal partial information about prices bidders are willing to pay,
hence, we refine our informal definition of bid secrecy as follows:
\begin{quote}
A losing bidder cannot be linked to a price, except when a link can be deduced from
auction results and any partial knowledge about the distribution of prices bidders are
willing to pay.
\end{quote}
\noindent
This refinement ensures that the aforementioned example does not constitute a violation
of bid secrecy. %\ifhorriblehacks\pagebreak[1]\fi
And we formalise the refined notion of bid secrecy as an indistinguishability game between an adversary and a challenger.%
\footnote{Games are algorithms that output $0$ or $1$. An adversary \emph{wins}
a game by causing it to output $1$. We denote an adversary's \emph{success} $\Succ(\Exp(\cdot))$ in a game $\Exp(\cdot)$ as the probability that the adversary wins, i.e., $\Succ(\Exp(\cdot)) =\mathrm{Pr}[g\leftarrow\Exp(\cdot) : g= 1]$.
Adversaries are assumed to be \emph{stateful}, i.e.,
information persists across invocations of the adversary
in a single game,\ifnocompress\ in particular\else\ e.g.\fi, the adversary can access
earlier assignments.}
Our game captures a setting where the challenger generates
a key pair using the $\SetupSymb$ algorithm, publishes
the public key, and only uses the private key for opening.
The adversary has access to a left-right
oracle which can compute bids
on the adversary's behalf.\footnote{Bellare \emph{et al.} introduced left-right oracles in the context of symmetric encryption~\cite{Bellare97}. And Bellare \& Rogaway provide a tutorial on their use~\cite{Bellare05}.}
Bids can be computed by the left-right oracle
in two ways, corresponding to a randomly chosen bit $\beta$. If $\beta=0$,
then, given a pair of prices $p_0,p_1$, the oracle outputs a bid for $p_0$.
Otherwise ($\beta=1$), the oracle outputs a bid for $p_1$.
The left-right oracle essentially allows the adversary to control
the distribution of prices in bids, but bids
computed by the oracle are always computed using the prescribed $\BidSymb$
algorithm.
The adversary outputs a bulletin board (this may contain bids output by the oracle and bids generated by the adversary),
which is opened by the challenger to reveal price $p$, set of winning bids $\mathfrak{b}$, and non-interactive proof $\tpf$ of correct opening.
Using these values, the adversary must determine whether $\beta=0$ or $\beta=1$.
To avoid trivial distinctions, we insist that a bid for
price $p$ was not output by the left-right oracle, assuming $p$ is the
winning price. This assumption is
required to capture attacks that exploit poorly designed
$\OpenSymb$ algorithms, in particular, we cannot assume that
$\OpenSymb$ outputs the winning price,
because algorithm $\OpenSymb$ might have been designed maliciously or
might contain a design flaw.
We ensure winning bids were not output by the left-right oracle
using a logical proposition. The proposition uses predicate $\correctprice(\pk,\nP, \bb,p,\kappa)$,
which holds when: $(p=0 \vee(\exists r \mathrel . \BidSymb(\pk,\nP,p,\kappa; r)\in \bb \setminus \{\bot\} \wedge 1 \leq p \leq \nP)) \wedge
(\lnot\exists p',r' \mathrel . \BidSymb(\pk,\nP,p',\kappa; r') \in
\bb \setminus \{\bot\} \wedge p < p' \leq \nP )$. Intuitively, the predicate holds when price $p$ has been correctly computed: when there exists a bid for price $p$ on the bulletin board and there is no bid for a higher price\ifnocompress, i.e., when $p$ is the winning price\fi.
Moreover, injectivity ensures that the bid was created for that price.\ifnocompress\footnote{The existential quantifiers in $\correctprice$ demonstrate the importance of defining injectivity \emph{perfectly} rather than \emph{computationally}. In particular, $\correctprice$ cannot interpret a bid for more than one price.}\fi
By design, our notion of bid secrecy is satisfiable by auction schemes which reveal
losing prices,\footnotemark\
assuming that these prices cannot be linked to bidders, except in the aforementioned cases.
%\footnote{We propose a stronger definition of bid secrecy for schemes which do not reveal losing prices in Appendix~\ref{app:strongBidSecrecy}.}\
And our construction will produce auction schemes of this type.
Hence, to avoid trivial distinctions, we insist, for each price $p$, that the number of bids on the bulletin board
produced by the left-right oracle with left input $p$, is
equal to the number of bids produced by the left-right oracle with right input $p$. This can be formalised using predicate $\balanced(\bb,\nP,L)$,
which holds when: for all prices
$p\in\{1,\dots,\nP\}$ we have
$ |\{b \mid b \in \bb \wedge (b,p,p_1) \in L\}| =
|\{b \mid b \in \bb \wedge (b,p_0,p) \in L\}|
$, where $L$ is the set of oracle call inputs and outputs.
\footnotetext{The class of auctions that reveal losing prices seem to have been first considered by
Franklin \& Reiter~\cite{SMR96}. Auctions that do not reveal losing prices have also been considered, e.g.,~\cite{HarkavyTK98}.}
Intuitively, if the adversary loses the game,
then the adversary is unable to distinguish between bids for different prices, assuming that a bid is not a winning
bid; it follows that losing prices cannot be linked to bidders.
By comparison, if the adversary wins\ifnocompress\ the game\fi, then there exists a strategy to
distinguish honestly cast bids.
\begin{definition}[Bid secrecy]
Let $\Sigma = (\SetupSymb,\BidSymb,\OpenSymb, \VerSymb)$ be
an auction scheme, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\BidSecrecy(\Sigma,\adv,\kappa)$ be the following game.\footnote{We write $x\leftarrow_R S$ for the assignment to $x$ of an element chosen uniformly at random from set $S$.}
{\upshape
\begin{inlineexperiment}{$\BidSecrecy(\Sigma,\adv,\kappa)$}
$(\pk,\sk,\mB,\mP\ifincludeVerify, \kpf\fi) \leftarrow \Setup[\kappa]$\;
$\beta \leftarrow_R \{0,1\};\;L \gets \emptyset$\;
$\nP \leftarrow \adv(\pk,\kappa);\; \bb \leftarrow \adv^{\oracleSymb}()$\;
$(p, \mathfrak b, \tpf) \leftarrow \OpenSymb(\sk, \nP, \bb,\kappa)$\;
$g \leftarrow \adv(p,\mathfrak b,\tpf)$\;
\eIf{$g = \beta \land \balanced(\bb,\nP,L)\wedge |\bb| \leq \mB \allowbreak \wedge \nP\leq \mP \allowbreak
\mathrel \land
(\correctprice(\pk,\nP, \bb,p,\kappa) \Rightarrow
\forall b\in\bb \mathrel. (b,p,p_1) \not\in L \land (b,p_0,p) \not\in L)$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
Oracle $\oracleSymb$ is defined as follows:\ifnocompress\footnote{The oracle may access game parameters, e.g.,
$\pk$. Henceforth, we allow oracles to access game parameters without an explicit mention.}\fi
\ifnocompress
\begin{itemize}
\item
\fi
$\oracle{p_0,p_1}$ computes $b \leftarrow \BidSymb(\pk,\nP,p_\beta,\kappa);L \gets L \cup \{ (b, p_0, p_1) \}$ and outputs $b$, where $p_0,p_1\in \{1, ..., \nP\}$.
\ifnocompress
\end{itemize}
\fi
\ifnocompress
\noindent
\fi%
We say $\Sigma$ satisfies \emph{bid secrecy ($\BidSecrecy$)}, 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 $\Succ(\allowbreak\BidSecrecy(\allowbreak\Sigma,\allowbreak\adv,\allowbreak\kappa)) \leq \frac{1}{2} + \mathsf{negl}(\kappa)$.
\end{definition}
\begin{comment}
\sout{
Our definition of bid secrecy is based upon
the notion of ballot secrecy proposed by Smyth%~\cite{Smyth15-ballot-independence}\ifnocompress\ (cf. Section~\ref{sec:ballot-secrecy})\fi\
and, roughly speaking, corresponds to a symbolic bid secrecy
definition proposed by Dreier, Lafourcade \& Lakhnech %~\cite[Definition 15]{Dreier13:BidSecrecy}.
}
\end{comment}
%\marginpar{By dropping the relation to ballot secrecy, we direct attention to the relation to
%an existing definition of bid secrecy. Perhaps that helps address the reviewers concerns.}
\noindent
Roughly speaking, our definition of bid secrecy corresponds to a symbolic bid secrecy
definition by Dreier, Lafourcade \& Lakhnech~\cite[Definition 15]{Dreier13:BidSecrecy}.
\subsection{Auction verifiability}
\newcommand{\blahA}{Our definitions are based upon analogous definitions for election schemes by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}\ifnocompress\ (cf. Section~\ref{sec:verifiability})\fi.}
\newcommand{\blahB}{We discuss our motivation to base the definitions on the notions of verifiability by Smyth, Frink \& Clarkson in\ifnocompress\ Section~\ref{sec:applicability}\else\ \S\ref{sec:applicability}\fi.}
\newcommand{\blahC}{In \cite{Dreier13:VerifiableAuctions}, the notion of verifiability in the context of electronic auctions is studied. The definition of verifiability proposed by the authors omits many details. This is done deliberately, since it is claimed that further details will depend on the protocol model. Because of this, a formal definition of verifiability for auctions in the computational model cannot be unequivocally derived from the definition in \cite{Dreier13:VerifiableAuctions}, and therefore, as is, we consider it unsuitable for modelling and
analysing verifiability of auction protocols.}
We formalise individual and universal verifiability as
games\ifnocompress\ between an adversary and a challenger\fi.%
\ifnocompress\ \blahA%\footnote{\blahC}%\textsuperscript{,}
\footnote{\blahB}
\else\footnote{\blahA\ \blahB}%\textsuperscript{,}\footnote{\blahC}
\fi
%Sections~\ref{sec:iv:election} \& \ref{sec:uv:election}).
\ifnocompress
\subsubsection{Individual verifiability}
\fi
Individual verifiability challenges the adversary to
generate a collision from algorithm $\BidSymb$.
If the adversary cannot win, then bidders can uniquely identify their bids, hence, bidders can check whether their bid is included.
\begin{definition}[Individual verifiability]\label{def:auction-iv}
Let $\Sigma = (\SetupSymb,\allowbreak\BidSymb,\allowbreak\OpenSymb,\allowbreak \VerSymb)$ be an auction scheme, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpAIV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpAIV$}
$(\pk,\nP,p,p') \leftarrow \adv(\kappa)$\;
$b\leftarrow\BidSymb(\pk,\nP,p,\kappa)$\;
$b'\leftarrow\BidSymb(\pk,\nP,p',\kappa)$\;
\eIf{
$b = b'
\wedge b \not= {\perp}
\wedge b' \not= {\perp}
$}{
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
We say $\Sigma$ satisfies \emph{individual verifiability ($\ExpAIVSymb$)},
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 $\SuccAIV \leq \mathsf{negl}(\kappa)$.
\end{definition}
\ifnocompress
\noindent
Individual verifiability resembles injectivity,
but game $\ExpAIVSymb$ allows an adversary to choose
the public key and prices, whereas there is no adversary
in the definition of injectivity (the public key is
an output of algorithm $\SetupSymb$ and prices are
universally quantified, under the restriction that prices
are distinct).
\fi
\ifnocompress
\subsubsection{Universal verifiability}
\fi
Universal verifiability challenges the adversary to concoct
a scenario in which $\VerSymb$ accepts, but the winning price
or the set of winning bids is not correct.\footnote{Universal verifiability captures a notion of non-repudiation, i.e., anyone can check whether the winning bids encapsulate the winning price.}
Formally, we check
the validity of the winning price using predicate $\correctprice$.
And we check the validity of the set of winning bids using
predicate $\correctballots(\allowbreak\pk,\allowbreak\nP,\allowbreak\bb,\allowbreak p,\allowbreak\mathfrak b,\allowbreak\kappa)$,
which holds when $\mathfrak b = \bb\cap \{ b \mid b = \BidSymb(\pk, \nP, p, \kappa;r )\}$, i.e.,
it holds when $\mathfrak b$ is the intersection of the bulletin board and
the set of all bids for the winning price.
Since function $\correctprice$ will be parameterised with a public key
constructed by the adversary, rather than one constructed by
algorithm $\SetupSymb$ (\S\ref{sec:bid:section}),
we must adopt a stronger definition of injectivity
which holds for adversarial keys. We define \emph{strong injectivity}
in \refappendix{\ref{cciforauc}}.
\begin{definition}[Universal verifiability]
Let $\Sigma = (\SetupSymb,\allowbreak\BidSymb,\allowbreak\OpenSymb,\allowbreak\VerSymb)$ be an auction scheme satisfying strong injectivity, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpAUV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpAUV$}
$(\pk,\nP,\bb,p,\mathfrak{b}, \tpf) \leftarrow \adv(\kappa)$\;
%\textcolor{red}{\sout{$p'\leftarrow \correctprice(\pk,\nP,\bb, \kappa)$}}\;
\eIf{$(\lnot\correctprice(\pk,\allowbreak\nP,\allowbreak \bb,\allowbreak p,\allowbreak\kappa)\allowbreak\mathrel\vee \allowbreak\lnot\correctballots(\pk,\allowbreak\nP,\allowbreak\bb,\allowbreak p,\allowbreak\mathfrak b,\allowbreak\kappa))\allowbreak
\mathrel\wedge \allowbreak\VerSymb(\pk,\allowbreak\nP,\allowbreak\bb,\allowbreak p,\allowbreak\mathfrak{b},\allowbreak\tpf,\allowbreak\kappa) = 1 $}{
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
We say $\Sigma$ satisfies \emph{universal verifiability ($\ExpAUVSymb$)},
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 $\SuccAUV \leq \mathsf{negl}(\kappa)$.
\end{definition}
\iffalse
\subsubsection{Example: $\Nonce$}
We demonstrate the applicability of our definitions with an auction scheme
based upon nonces.
\begin{definition}\label{def:nonce}
Auction scheme $\Nonce$ is defined as follows:
\begin{itemize}
\item $\Setup[\kappa]$ outputs $({\perp},{\perp},\mathit{poly}(\kappa),\infty)$,
where $\mathit{poly}$ is a polynomial function.
\item $\BidSymb(\pk,\nP,p,\kappa)$ selects a nonce $r$ uniformly at random from $\mathbb Z_{2^\kappa}$
and outputs $(r,p)$.
\item $\OpenSymb(\sk,\nP,\bb,\kappa)$ proceeds as follows.
Compute the largest subset $\mathfrak b \subseteq \bb$ such that for all $(r,p)\in\mathfrak b$
we have $p$ is the winning price and $r\in\mathbb Z_{2^\kappa}$.
Output $(p,\mathfrak b,\perp)$ if $\mathfrak b\not=\emptyset$,
and $(0,\emptyset,\perp)$ otherwise.
\item $\VerSymb(\pk,\nP,\bb,p,\mathfrak b,\tpf,\kappa)$ outputs $1$ if $(p,b,\tpf) =\OpenSymb({\perp},{\perp},\nP,\bb,\kappa)$ and
$0$ otherwise.
\end{itemize}
\end{definition}
\noindent Intuitively, $\Nonce$ satisfies individual verifiability, because voters can use their nonce to check that their own ballot appears on the bulletin board.
With overwhelming probability, voters will select unique nonces, hence generate distinct ballots.
$\Nonce$ also satisfies universal verifiability, because plaintext candidate choices are posted on the bulletin board.
We defer a formal proof to Section~\ref{sec:transformation}, where we can use our election to
auction scheme construction and accompanying security results.
\fi
%%%%%%%
%%%%%%%
%
% correct-price
%
%Function $\correctprice$ is defined such that for all
%$\pk$, $\nP$, $\bb$, $\kappa$, and $p \in \{1,\ldots,\nP\}$,\marginpar{\textcolor{blue}{To check!}}
%we have
%\begin{multline*}
%\correctprice(\pk,\nP,\bb,\kappa) = p' \\
%\iff \exists \ b' \in (\bb \setminus \{\bot\}) :
%\exists r' : b=\BidSymb(\pk,\nP,p',\kappa; r) \ \land \\
%(\not\exists \ r : b=\BidSymb(\pk,\nP,p,\kappa; r) :
% b \in (\bb \setminus \{\bot\}) \land p > p').
%\end{multline*}
```
# Auctions from elections
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 363, column 1): unexpected } expecting \end{definition} } ^`
``` latex
\section{Auctions from elections}\label{sec:transformation}
\ifnocompress
\subsection{Election scheme syntax}\fi\label{sec:elections:syntax}
We recall\iffalse\footnotemark\fi \ syntax for \emph{election schemes}~\cite{Smyth15:ElectionVerifiability}, which capture the class of elections that consist
of the following four steps.
First, a tallier generates a key pair.
Secondly, each voter constructs and casts a ballot for their choice.
These ballots are recorded on a bulletin board.
Thirdly, the tallier tallies the recorded ballots and
announces an outcome, i.e., a distribution of choices.
This distribution is used to select a representative.
For example, in first-past-the-post elections
the representative corresponds to the choice with highest frequency.
Finally, voters and other interested parties check that the outcome
corresponds to votes expressed in recorded ballots.\footnote{Smyth, Frink \&
Clarkson use the syntax to model first-past-the-post voting systems and Smyth shows
the syntax is sufficiently versatile to capture ranked-choice voting systems too~\cite{2017-FPTP-suffices-for-ranked-voting}.}
This class of elections includes state-of-the-art schemes
such as the Helios family, but notably excludes schemes reliant
on paper, e.g., Pret \`{a} Voter~\cite{ChaumRyanSchneider2005},
Scantegrity II~\cite{Chaum08II}, and Remotegrity~\cite{Zagorski13}.
\begin{definition}[Election scheme~\cite{Smyth15:ElectionVerifiability}] \label{def:election}
An \emph{election scheme} is a tuple of efficient algorithms
$(\SetupSymb,\VoteSymb,\TallySymb, \VerSymb)$ such that:
\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 $\VoteSymb$, denoted $b\leftarrow\Vote{v,\kappa}$, is run by voters. $\VoteSymb$ takes as input a
public key $\pk$\ifincludeVerify, a proof $\kpf$\fi, some number of candidates
$\nC$, a voter's vote $v$, and a security parameter $\kappa$.
A voter's vote should be selected from a sequence $1,\dots,\nC$ of
candidates.\footnote{Votes are (abstractly) modelled as integers, rather than alphanumeric strings (such as representatives' names), for brevity.}
$\VoteSymb$ outputs a ballot $b$ or error symbol $\perp$.
\item $\TallySymb$, denoted $(\outcome, \tpf)\leftarrow\TallySymb(\sk,
\nC, \bb,\kappa)$, is run by the tallier.
$\TallySymb$ takes as input a private key $\sk$, some number
of candidates $\nC$, a bulletin board $\bb$, 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\footnotemark\ the number of votes for candidate $v$.
\footnotetext{Let $\outcome[v]$ denote component $v$ of vector $\outcome$.}
\item $\VerSymb$, denoted $s \leftarrow \VerSymb(\pk\ifincludeVerify,
\kpf\fi,\nC, \bb, \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 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 must satisfy \emph{correctness}\ifnocompress\else~\cite[Definition~1]{Smyth15:ElectionVerifiability}\fi, \emph{completeness}\ifnocompress\else\ \cite[Definition~2]{Smyth15:ElectionVerifiability}\fi,
and \emph{injectivity}, which we define in \refappendix{\ref{cciforelec}}.
\end{definition}
\ifnocompress
\subsubsection{Example: $\mv$}
We demonstrate the applicability of our syntax using
a construction ($\mv$) for election schemes from
asymmetric encryption schemes.\footnote{The construction was originally
presented by Bernhard \emph{et
al.}~\cite{2014:BallotIndependenceEprint,2013:BallotIndependenceESORICS,Bernhard11:Helios,Smyth11:HeliosProvableSecure} in a slightly different setting.}
\begin{definition}[$\mv$]\label{def:mv}
Given an asymmetric encryption scheme $\Pi =
(\GGenSymb,\allowbreak\EEncSymb,\DDecSymb)$,
we define $\mv(\Pi)$ 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\ifincludeVerify,
\kpf\fi,\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
To ensure $\mv(\Pi)$ is an election scheme, we require asymmetric
encryption scheme $\Pi$ to produce distinct ciphertexts with overwhelming
probability (cf. \S\ref{sec:auctions:example}). Hence, we restrict the
class of asymmetric encryption schemes used to instantiate $\mv$.
\begin{lemma}\label{lemma:Enc2Vote:correctness}
Suppose $\Pi$ is an asymmetric encryption scheme with perfect correctness
that satisfies $\INDCPA$.
We have $\mv(\Pi)$ is an election scheme.
\end{lemma}
\fi
\subsubsection{Comparing auction and election schemes}
Auction schemes are distinguished from election schemes
% in the final step of their execution:
as follows: auction schemes open the bulletin board to recover the
winning price and winning bids, whereas, election schemes tally the bulletin board
to recover the distribution of votes. Our goal is to bridge this gulf; we
introduce \emph{reveal algorithms} to do so.
\subsection{Reveal algorithm}\label{sec:reveal}
To achieve the functionality required to construct auction schemes from
election schemes,
we define \emph{reveal algorithms} which link
a vote to a set of ballots for that vote,
given the tallier's private key. We stress that ballot secrecy does
not prohibit the existence of such algorithms, because ballot secrecy
asserts that the tallier's private key cannot be derived by the adversary.
\begin{definition}[Reveal algorithm]
A \emph{reveal algorithm} is an efficient algorithm $\RevealSymb$ defined as follows:
\begin{description}
\item $\RevealSymb$, denoted $\mathfrak b \leftarrow \RevealSymb{(\sk, \nC, \bb,v,\kappa)}$, is run by the tallier. $\RevealSymb$ takes as input a private key $\sk$, some number of candidates $\nC$, a bulletin board $\bb$, a vote $v$, and a security parameter $\kappa$.
It outputs a set of ballots $\mathfrak b$.
\end{description}
\noindent
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme.
A reveal algorithm is \emph{correct with respect to $\Gamma$}, if
there exists a negligible function $\mathsf{negl}$,
such that for all \ifnocompress{}security parameters\fi $\kappa$,
integers $\nB$ and $\nC$, and
votes $v,v_1,\dots,v_{\nB}\in\{1,\dots,\nC\}$, it holds that: \\
{\upshape
\begin{inlineprobability}{$\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$}
\For{$1 \leq i \leq \nB$}{
$b_i \leftarrow \VoteSymb(\pk,\nC,v_i,\kappa)$;\\
}
$ \mathfrak b \leftarrow \RevealSymb(\sk,\nC, \{b_1,\dots,b_{\nB}\},v,\kappa)$\\
$:\nB \leq \mB \wedge \nC\leq \mC\Rightarrow \mathfrak{b} = \{b_i \mid v_i = v \wedge 1 \leq i \leq \nB\}] > 1 - \mathsf{negl}(\kappa)$.
%\exists r \mathrel. b_i = \VoteSymb(\pk,\nC,v,\kappa)
\end{inlineprobability}
}
\end{definition}
Reveal algorithms are run by talliers to disclose sets of ballots for a specific vote.
Hence, we extend the tallier's role to include the execution of a reveal algorithm (cf. Section \ref{sec:intro:construction}), thereby bridging the gap between elections and auctions.
%The execution of this algorithm embodies the extension of the tallier's role discussed in Section \ref{sec:intro:construction} and is key to overcoming the gap between elections and auctions.
It is natural to consider whether this extension is meaningful, i.e.,
given an arbitrary election scheme, does there exist a reveal algorithm that is correct with respect to that election scheme? We answer this question positively in \refappendixaux{\ref{sec:existence}}{the}. \iftr\else
\ifnocompress
In particular, we show that, given an election scheme, we can run its $\TallySymb$ algorithm on every ballot on the bulletin board and compute the set of ballots encapsulating a specific vote, thereby deriving a reveal algorithm which is correct with respect to that election scheme. The result is largely theoretical, because the class of reveal algorithms introduced
leak the ballot-vote mapping for every ballot on the bulletin board during execution.
This does not violate ballot secrecy, because the
tallier is assumed to be trusted, i.e., the tallier is assumed not
to disclose mappings. Nevertheless, reveal algorithms which only
disclose a set of ballots for a particular vote, i.e., revealing the minimal amount of information, are preferable for privacy, and we demonstrate the existence of such algorithms in our case study.
\fi
\fi
%\marginpar{BEN: I dropped the discussion on how the generic reveal works because we don't have the room...}
%As a first step, we show that the above construction yields a \emph{correct} e-auction scheme.
%\begin{lemma}[Correctness]
%Let $\Gamma$ be a correct e-voting scheme and let $\RevealSymb$ be a reveal algorithm.
%Then $\Lambda$ built as above is a correct e-auction scheme.
%\end{lemma}
%\begin{proof}
%Suppose $\Gamma = (\SetupSymb,\VoteSymb,\BBSymb,\TallySymb)$ is an election scheme and
%$\RevealSymb$ is a reveal algorithm.
%We have $\Lambda(\Gamma,\RevealSymb) = (\SetupSymb,\VoteSymb,\BBSymb,\OpenSymb)$,
%where $\OpenSymb$ is defined in Definition~\ref{def:transform}.
%Further suppose $n$ is a security parameter, $\nC$ and $m$ are positive integers,
%$p_1,\dots,p_m \in \{1,\dots,\nC\}$ are prices,
%$(\pk,\sk,\bb_0) \leftarrow \Setup$.
%Let $b_i\leftarrow \Vote{p_i}; \bb_i \leftarrow \BB{\bb_{i-1}}{b_i}$ for each $1\leq i\leq m$,
%and $(p,b,\aux) \leftarrow \Open{\bb_m}$.
%By definition of $\OpenSymb$, we have
%$p$ is the largest integer in $\langle \outcome \rangle$,
%where $(\outcome,\aux) \leftarrow \TallySymb{(\sk,\nC,\bb_m)}$.
%It follows by the correctness property of $\Gamma$ that
%$\langle \outcome \rangle = \{p_1,\dots,p_m\}$ with overwhelming probability.
%By definition of $\OpenSymb$, we also have
%$b$ was output by $\RevealSymb{(\sk, \nC, \bb_m, p)}$.
%It follows from the definition of reveal algorithms (Definition~\ref{def:transform})
%that there exists $i\in\{1,\dots,m\}$ such that $v_i = v \wedge b_i = b$ with overwhelming probability.
%\end{proof}
\iffalse
\begin{definition}[Reveal algorithm]
Let $(\SetupSymb,\VoteSymb,\TallySymb\ifincludeVerify, \VerSymb\fi)$ be an election scheme,
$\kappa$ be a security parameter, $\nC$ and $m$ be positive integers, and
$v_1,\dots,v_m \in \{1,\dots,\nC\}$ be votes.
Suppose $(\pk,\sk,\mB,\mC) \leftarrow \Setup$, $b_i\leftarrow \Vote{v_i}$ for each $1\leq i\leq m$, and $\bb=\{b_1, ..., b_m\}$.
Let $\RevealSymb$ be an algorithm that takes as input a private key $\sk$, integers $\nC$ and $v$ such that $1 \leq v \leq \nC$, and a set $\bb$, and outputs bid $b$ and proof $\tpf$.
We say $\RevealSymb$ is a \emph{reveal algorithm} if, with overwhelming probability,
for all $v\in\{v_1,\dots,v_m\}$ we have that $b \in\{b_i \ | \ 1\leq i \leq m \wedge v_i=v\}$, where $(b,\tpf) \leftarrow \RevealSymb{(\sk, \nC, v, \bb)}$.
\end{definition}
\begin{color}{blue}
\begin{definition}[Reveal algorithm]\label{def:reveal}
Let $(\SetupSymb,\VoteSymb,\TallySymb\ifincludeVerify, \VerSymb\fi)$ be an election scheme.
A \emph{reveal algorithm} is an algorithm
\begin{description}
\item $\RevealSymb$, denoted $(b,\tpf) \leftarrow \RevealSymb{(\sk, \nC, v, \bb)}$, run by the tallier. $\RevealSymb$ takes as input a private key $\sk$, some number of candidates $\nC$, a vote $v$, and a bulletin board $\bb$. It outputs ballot $b$ and proof $\tpf$.
\end{description}
\noindent
Reveal algorithms must satisfy the following correctness property:
there exists a negligible function $\mathsf{negl}$, such that for all
security parameters $\kappa$, integers $\nB$ and $\nC$, and
votes $v,v_1,\dots,v_{\nB} \in \{1,\dots,\nC\}$, we have\\
{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$;\\
\begin{algorithm}
\For{$1 \leq i \leq \nB$}{
$b_i \leftarrow \VoteSymb(\pk,\nC,v_i)$;\\
}
$(b,\tpf) \leftarrow \RevealSymb{(\sk, \nC, v, \{b_1,\dots,b_{n_B}\})}:$
$b \in\{b_i \ | \ 1\leq i \leq \nB \wedge v_i=v\}] > 1 - \mathsf{negl}(\kappa)$.
\end{algorithm}
}
\textcolor{red}{BEN: The above isn't strong enough.}
\noindent
Reveal algorithms must satisfy the following property:
there exists a negligible function $\mathsf{negl}$, such that for all
security parameters $\kappa$, we have\\
{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$;\\
\begin{algorithm}
$(\nC,v,bb)\leftarrow \adv(\pk)$;\\
$(b,\tpf) \leftarrow \RevealSymb{(\sk, \nC, v, \bb)}:$\\
$|\bb| \leq \mB \wedge 1\leq v \leq \nC \leq \mC\Rightarrow \exists r \mathrel. b = \VoteSymb(\pk,\nC,v; r) \wedge b \in \bb] > 1 - \mathsf{negl}(\kappa)$.
\end{algorithm}
}
\textcolor{red}{BEN: The above still isn't right; reveal might not succeed, e.g., if
$\bb=\emptyset$. We could remain general and allow reveal to fail, or we could redefine as follows}\\
\end{color}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Let $(\SetupSymb,\VoteSymb,\TallySymb\ifincludeVerify, \VerSymb\fi)$ be an election scheme.
A \emph{reveal algorithm} is an algorithm
\begin{description}
\item $\RevealSymb$, denoted $b \leftarrow \RevealSymb{(\sk, \nC, \bb,\outcome,v)}$, run by the tallier. $\RevealSymb$ takes as input a private key $\sk$, some number of candidates $\nC$, a bulletin board $\bb$, an election outcome $\outcome$ and a vote $v$.
It outputs ballot $b$.
\end{description}
\noindent
Reveal algorithms must satisfy the following property:
there exists a negligible function $\mathsf{negl}$, such that for all
security parameters $\kappa$, we have\\
\textcolor{red}{BEN: We need to know what $b$ is to simulate it.}
{\upshape
\noindent $\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$;\\
\begin{algorithm}
$(\nC,v,\bb)\leftarrow \adv(\pk)$;\\
$(\outcome, \tpf) \leftarrow \TallySymb(\sk, \nC, \bb,\kappa)$;\\
$b \leftarrow \RevealSymb{(\sk, \nC, \bb, \outcome, v)}$\\
$\quad: 1\leq v \leq\nC \wedge \outcome[v] = 0 \wedge b = {\perp} \mathrel{\bigvee}$\\
$\qquad \exists r \mathrel . \outcome[v] > 0 \wedge 1\leq v \leq\nC$\\
$\qquad \mathrel\wedge b = \VoteSymb(\pk,\nC,v,\kappa; r) \land b \in \bb ] > 1 - \mathsf{negl}(\kappa)$.
\end{algorithm}
}
\end{definition}
\fi
\subsection{Construction}
\iffalse
\sout{We build algorithm $\OpenSymb$ from algorithms $\TallySymb$ and
$\RevealSymb$. This results in our first construction for auction schemes from election schemes (\S\ref{sec:trans:1}) and we shall see that this construction
produces auction schemes satisfying bid secrecy (\S\ref{sec:secrecy:non-verifiable:schemes}). Building upon this result,
our second construction (\S\ref{sec:trans:2}) enables the production of auction schemes
satisfying bid secrecy (\S\ref{sec:secrecy:verifiable:schemes}) \emph{and} auction verifiability (\S\ref{sec:result:verifiability}). }
\fi
We show how to construct auction schemes from election schemes.
\ifnocompress
We first describe a construction which can produce auction schemes satisfying bid secrecy\iftr\ (\S\ref{sec:trans:1})\fi. Building upon this result, we present
our second construction which can produce auction schemes
satisfying bid secrecy \emph{and} auction verifiability\iftr\ (\S\ref{sec:trans:2})\fi.
\fi
%
\ifnocompress
\subsubsection{Non-verifiable auction schemes}\label{sec:trans:1}
Our first construction follows intuitively from our informal description (\S\ref{sec:intro:construction}).
Algorithm $\BidSymb$ is derived from $\VoteSymb$, simply by representing prices as candidates.
Algorithm $\OpenSymb$ uses algorithm $\TallySymb$ to derive the distribution of prices and the winning price is determined from this distribution.
Moreover, we exploit a reveal algorithm $\RevealSymb$ to disclose the set of winning bids.
\begin{definition}\label{def:transform-secrecy-only}
Given an election scheme $\Gamma = (\SetupSymb_{\Gamma},\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb_{\Gamma})$ and a reveal algorithm $\RevealSymb$, we define
$\Lambda(\Gamma,\allowbreak\RevealSymb) = (\SetupSymb_{\Lambda},\allowbreak\BidSymb,\allowbreak\OpenSymb,\allowbreak\VerSymb_{\Lambda})$ as follows.
\begin{description}
\item $\SetupSymb_{\Lambda}(\kappa)$ computes $(\pk,\sk,\mB,\mC) \leftarrow \SetupSymb_\Gamma(\kappa)$ and outputs $(\pk,\sk,\mB,\mC)$.
\item $\BidSymb(\pk,\nP,p,\kappa)$ computes $b\leftarrow\VoteSymb(\pk,\nP,p,\kappa)$ and outputs $b$.
\item $\OpenSymb(\sk, \nP, \bb,\kappa)$ proceeds as follows.
Computes $(\outcome, \tpf) \leftarrow \TallySymb(\sk, \nP, \bb,\kappa)$.
Finds the largest integer $p$ such that $\outcome[p] > 0 \ \wedge \ 1 \leq p \leq \nP$, outputting $(0,\emptyset,\epsilon)$ if no such integer exists.
Computes
$\mathfrak b \leftarrow \RevealSymb(\sk, \nP, \bb, p,\kappa)$.
And outputs $(p, \mathfrak b, \epsilon)$.
\item $\VerSymb_{\Lambda}(\pk, \nP, \bb, p, \mathfrak b, \tpf', \kappa)$
outputs 1.
\end{description}
\noindent
Algorithm $\OpenSymb$ requires $\epsilon$ to be a constant symbol.
\end{definition}
\begin{lemma}\label{lemma:trans:1:correctness}
Let $\Gamma$ % = (\SetupSymb_{\Gamma},\allowbreak\VoteSymb,\TallySymb,\allowbreak \VerSymb_{\Gamma})$
be an election scheme and $\RevealSymb$ be a reveal algorithm.
Suppose $\RevealSymb$ is correct with respect to $\Gamma$.
We have $\Lambda(\Gamma,\RevealSymb)$
is an auction scheme. % (i.e., Correctness, Completeness and Injectivity are satisfied).
\end{lemma}
%\noindent The proof of Lemma~\ref{lemma:trans:1:correctness} and all
% other results, except where otherwise stated, appear in the
% Appendix~\ref{sec:proofs}.
%We prove Lemma~\ref{lemma:trans:1:correctness} in~\refappendix{\ref{sec:proof:transform}}.
\subsubsection{Verifiable auction schemes}\label{sec:trans:2}
Our second construction extends our first construction to ensure
verifiability, in particular, algorithm $\OpenSymb$ is extended to
include a proof of correct tallying and a proof of correct revealing.
Moreover, algorithm $\VerifySymb$ is used to check proofs.
\else
%
\ifnocompress
Our construction follows from our informal description (\S\ref{sec:intro:construction}). \fi
Algorithm $\BidSymb$ is derived from $\VoteSymb$, simply by representing prices as candidates.
Algorithm $\OpenSymb$ uses algorithm $\TallySymb$ to derive the distribution of prices and the winning price is determined from this distribution.
Moreover, we exploit a reveal algorithm $\RevealSymb$ to disclose the set of winning bids.
In addition, Algorithm $\OpenSymb$ includes a proof of correct tallying and a proof of correct revealing.
And algorithm $\VerifySymb$ is used to check proofs.
\fi
%
\begin{definition}\label{def:transform}
Given an election scheme $\Gamma = (\SetupSymb_{\Gamma},\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb_{\Gamma})$, a reveal algorithm $\RevealSymb$, and
a non-interactive proof system
%\footnote{For details on the cryptographic primitives used in this paper, please refer to \ifnocompress{}Appendix \ref{sec:crypto}\else{}\cite{tr}\fi.}
$\Delta = (\ProveSymb, \VerifySymb)$, we define
$\Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta) = (\SetupSymb_{\Lambda},\allowbreak\BidSymb,\allowbreak\OpenSymb,\allowbreak\VerSymb_{\Lambda})$ as follows.
\begin{description}
\item $\SetupSymb_{\Lambda}(\kappa)$ computes $(\pk,\sk,\mB,\mC) \leftarrow \SetupSymb_\Gamma(\kappa)$ and outputs $(\pk,\sk,\mB,\mC)$.
\item $\BidSymb(\pk,\nP,p,\kappa)$ computes $b\leftarrow\VoteSymb(\pk,\nP,p,\kappa)$ and outputs $b$.
\item $\OpenSymb(\sk, \nP, \bb,\kappa)$ proceeds as follows.
Computes $(\outcome, \tpf) \leftarrow \TallySymb(\sk, \nP, \bb,\kappa)$.
Finds the largest integer $p$ such that $\outcome[p] > 0 \ \wedge \ 1 \leq p \leq \nP$,
outputting $(0,\emptyset,\epsilon)$ if no such integer exists.
Computes $\mathfrak b \leftarrow \RevealSymb(\sk, \nP, \bb, p,\kappa)$
and $\tpf' \leftarrow \ProveSymb((\pk,\nP,\bb,p,\mathfrak b,\kappa),\sk,\kappa)$,
and outputs $(p, \mathfrak b, (\outcome, \tpf,\tpf'))$.
\item $\VerSymb_{\Lambda}(\pk, \nP, \bb, p, \mathfrak b, \sigma, \kappa)$
proceeds as follows.
Parses $\sigma$ as $(\outcome, \tpf,\tpf')$, outputting $0$ if parsing fails.
The algorithm performs the following checks:
\begin{enumerate}
\item\label{def:transform:checkA} Checks that $\VerSymb_{\Gamma}(\pk,\nP, \bb, \outcome, \tpf, \kappa) = 1$.
\item\label{def:transform:checkB} Checks that $p$ is the largest integer such that $\outcome[p] > 0 \ \wedge \ 1 \leq p \leq \nP$
or there is no such integer and $(p,\mathfrak b,\tpf') = (0,\emptyset,\epsilon)$.
\item\label{def:transform:checkC} Checks that $\VerSymb((\pk,\nP,\bb,p,\mathfrak b,\kappa),\tpf',\kappa) = 1$.
\end{enumerate}
Outputs $1$ if all of the above checks hold, and outputs $0$ otherwise.
\end{description}
\noindent
Algorithms $\TallySymb$ and $\VerSymb$ require $\epsilon$ to be a constant symbol.
\end{definition}
\noindent
To ensure that our construction produces auction schemes, the non-interactive
proof system must be defined for a suitable relation. We define it
as follows.
\begin{definition}\label{def:relation}
Given an election scheme $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$
and a reveal algorithm $\RevealSymb$, we define binary relation $R(\Gamma,\RevealSymb)$
over vectors of length $6$ and bitstrings such that
$((\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak{}v,\allowbreak\mathfrak b,\allowbreak\kappa),\;\sk) \in R(\Gamma,\RevealSymb)
\Leftrightarrow \exists \mB,\mC,r,r' \mathrel .
\mathfrak b = \RevealSymb(\sk,\allowbreak \nC,\allowbreak \bb,\allowbreak v,\allowbreak\kappa;\allowbreak{}r) \allowbreak\mathrel\wedge
(\pk,\allowbreak\sk,\allowbreak\mB,\allowbreak\mC) =\allowbreak \SetupSymb(\kappa;r') \allowbreak \mathrel\wedge\allowbreak 1 \leq v\leq \nC\leq \mC
\wedge |\bb| \leq \mB$.
\end{definition}
\begin{lemma}\label{lemma:trans:2:correctness}
Let $\Gamma$ % = (\SetupSymb_{\Gamma},\allowbreak\VoteSymb,\allowbreak\TallySymb, \allowbreak\VerSymb_{\Gamma})$,
be an election scheme,
$\RevealSymb$ be a reveal algorithm, and
$\Delta$ %$(\ProveSymb, \VerifySymb)$
be a non-interactive proof system
for relation $R(\Gamma,\RevealSymb)$.
Suppose $\RevealSymb$ is correct with respect to $\Gamma$.
We have $\Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta
%(\ProveSymb,\allowbreak \VerifySymb)
)$
is an auction scheme. % (i.e., Correctness, Completeness and Injectivity are satisfied).
\end{lemma}
\ifnocompress\else
\noindent The proof of Lemma~\ref{lemma:trans:2:correctness} and all
further proofs appear in \refappendix{\ref{sec:proofs}}.
\fi
\ifnocompress
Next, we study the security of auction schemes produced by our constructions, in particular, we
present conditions under which our constructions produce auction schemes satisfying bid secrecy
and verifiability.
\fi
\iffalse
%\begin{framed}
\begin{figure}
\textcolor{red}{BEN: Syntax is wrong.}
\begin{description}\label{def:transform}
\item[$\SetupSymb_{\Lambda}(\kappa)$:] Run $\SetupSymb_{\Gamma}(\kappa)$ to obtain $\pk, \sk$ and $\kpf$.
\smallskip
\item[$\BidSymb_{\Lambda}(\pk, \kpf, \nP, p)$:] Run $\VoteSymb_{\Gamma}(\pk, \kpf, \nP, p)$ to obtain bid $b$.
\smallskip
\item[$\OpenSymb_{\Lambda}(\sk, \nP, \bb)$:] Run $\TallySymb_{\Gamma}(\sk, \nP, \bb,\kappa)$ to obtain $(\outcome, \tpf_{0})$. Find $p$, the largest integer in $\langle \outcome \rangle$ and run $\RevealSymb(\sk, \nP, \bb, p)$ to obtain $(b, \tpf_{1})$. Finally output $(p, b, (\outcome,
\tpf_{0}, \tpf_{1}))$.
\ifincludeVerify
\item[$\VerSymb_{\Lambda}(\pk, \kpf, \bb, \sk, \nP, p, b, \tpf)$:] TO DO
\fi
\end{description}
\caption{Our transform}
\label{fig:transform}
\end{figure}
%\end{framed}
\fi
\iffalse
\noindent It is easy \textcolor{red}{BEN: It isn't easy any more!} to see that by correctness of the election scheme and the definition of
reveal algorithms, we have $\Lambda$ is a construction for auction schemes, i.e.,
$\Lambda(\Gamma,\RevealSymb)$ satisfies the correctness property of auction schemes.
\textcolor{red}{Do we want to formally state this result? LIZ: No I think it is pretty straightforward.}
Proving that the resulting scheme satisfies bid secrecy is the focus of the remainder
of this paper.
\textcolor{red}{LIZ: Actually, thanks to all the new definitions we have introduced the security proof is quite simple. What we should provide is an intuition as to why this is the case
i.e. we can easily obtain auction schemes from election schemes if the latter have non-malleable ballots..}
\fi
%We have shown that our construction generates auction schemes satisfying
%bid secrecy (Theorem~\ref{thm:mainResult}), but, nonetheless, the algorithm presented
%in the proof of Proposition~\ref{prop:completeness} can link a vote to
%a voter. This is due to an implicit assumption in our bid secrecy definition:
%the auctioneer is trusted. A similar assumption is made in the ballot secrecy
%game. Accordingly, Proposition~\ref{prop:completeness} is only of theoretical
%importance.
\iffalse
\subsection{Security results \textcolor{red}{OLD -- to be dropped/merged}}
While functionality-wise the transform we propose is very intuitive, the
security guarantees we seek from it are more subtle to achieve. Indeed, it is
not immediate to see how the reduction from ballot secrecy to bid secrecy could
go through.
The introduction and study of the notion of \emph{non-malleable ballots} will
shed light on this, and, in particular, will allow us to prove our main
result.\\
\begin{theorem}\label{thm:mainResult}
Suppose $\Gamma$ is an election scheme satisfying \sINDCVA.
Further suppose $\RevealSymb$ is a reveal algorithm.
We have $\Lambda(\Gamma,\RevealSymb)$ is an auction scheme satisfying bid secrecy.
\end{theorem}
\begin{proof}
Let $\adv = (A_1,A_2)$ be an adversary against the bid privacy of $\Lambda$. We
will construct an \sINDCVA adversary $\mathcal{B} = (B_1,B_2)$ against $\Gamma$
using
$\adv$.
$B_1$ receives public key $\pk$ and passes it on to $A_1$.
$A_1$'s oracle queries are handled as follows: $B_1$ forwards each query
$(p_0,p_1)$ to its own oracle and receives the corresponding $b$ in response.
$B_1$ maintains
a list $L$ of tuples of the form $(b, p_0,p_1)$, where $b$ is the response to
query $(p_0,p_1)$.
$B_1$ passes $b$ to $A_1$.
At some point $A_1$ outputs the set $\bb$ and state $s$. Let $\bb = \bb^{O} \cup \bb^{'}$,
where $\bb^{O}$ contains all the bids in $\bb$ output by oracle calls, and
let $m$ me the
size of $\bb^{'}$, i.e. we can write $\bb'= \{b_i^{'}\}_{i \in \{1,...,m\}}.$
$B_1$ outputs $\bbv$, where $\bbv = [ \bb^{O}, \{b_1^{'}\}, ..., \{b_m^{'}\} ]$
and receives back the election result $\vv =[ \vv^{O}, \{v_1^{'}\}, ..., \{v_m^{'}\} ]$. Let $v^{*}$ be the highest element
in the set $\{v_i^{'}\}_{i \in \{1,...,m\}}$ and $b^{*}$ the corresponding bid.
$B_2$ passes $(v^{*}, b^{*}, \perp, s)$ to $A_2$, which finally outputs bit $\beta$. $B_2$ outputs the same value.
It is straightforward to see that $\mathcal{B}$ perfectly simulates $\adv$'s environment and by construction it has the same winning probability of $\adv$.
\end{proof}
\fi
```
# Privacy results
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 256, column 1): unexpected } expecting \end{definition} } ^`
``` latex
\section{Privacy results}\label{sec:privacy:results}
\ifnocompress
We introduce a definition of ballot secrecy
which is sufficient to ensure that our construction produces auction
schemes satisfying bid secrecy (assuming some soundness conditions on the underlying election
scheme and reveal algorithm).\footnote{Our privacy results could be extended to other definitions of bid secrecy and ballot secrecy, by modifying our proofs.}
\subsection{Ballot secrecy}
Our definition of ballot secrecy strengthens an earlier definition
by Smyth \linebreak \cite{Smyth15-ballot-independence}.\footnote{We discuss the suitability of Smyth's definition in Section~\ref{sec:applicability}.}\textsuperscript{,}\footnote{Quaglia \& Smyth present a tutorial-style introduction to modelling ballot secrecy~\cite{Smyth17:voting-tutorial}, and Smyth provides a technical introduction~\cite{Smyth18:voting-tutorial}.}
\else
We strengthen an earlier definition of ballot secrecy by Smyth \cite{Smyth15-ballot-independence} and show that it is sufficient to ensure that our construction produces auction
schemes satisfying bid secrecy, assuming some soundness conditions on the underlying election
scheme and reveal algorithm.%
\footnote{\sout{Our privacy results could be extended to other definitions of bid secrecy and ballot secrecy, by modifying our proofs.}}
\fi
\label{sec:ballot-secrecy}
\begin{comment}
\footnotetext{%
\ifnocompress Smyth's definition
is based upon a technical report by Smyth~\cite{2014-ballot-secrecy-a}
and an extended version of that technical report by Bernhard \& Smyth~\cite{2014-ballot-secrecy}.
We build upon this
\else
We build upon Smyth's
\fi
definition
because it
strengthens earlier definitions by Bernhard \emph{et al.}~\cite{Smyth11:HeliosProvableSecure,Bernhard11:Helios,2013:BallotIndependenceESORICS,2014:BallotIndependenceEprint,BCGPW15}
to detect attacks\ifnocompress\ that arise\fi\ when the adversary controls the
bulletin board and the communication channel.
(Quaglia \& Smyth~\cite{Smyth17:voting-tutorial} provide an introduction
to definitions of ballot secrecy and a high-level comparison
between definitions. Smyth \cite[\S7]{Smyth15-ballot-independence}
and Bernhard \emph{et al.}~\cite{BCGPW15}
provide detailed comparisons.)
Our privacy results
could be extended to other definitions of bid secrecy and ballot
secrecy, by modifying our proofs.
}
\end{comment}
\begin{definition}[Ballot secrecy]\label{def:ballotSecrecy}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$ be
an election scheme, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\BallotSecrecy(\allowbreak\Gamma,\allowbreak\adv,\allowbreak\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\BallotSecrecy(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB,\mC\ifincludeVerify, \kpf\fi) \leftarrow \Setup$\;
$\beta \leftarrow_R \{0,1\}; L \leftarrow \emptyset; W \leftarrow \emptyset$\;
$\nC \leftarrow \adv(\pk, \kappa);\bb \leftarrow \adv^{\oracleSymb}()$\;
$(\outcome, \tpf) \leftarrow \Tally{\bb,\kappa}$\;
\For{$b \in \bb \wedge (b,v_0,v_1) \notin L$}{
$(\outcome', \tpf')\leftarrow \Tally{\{b\},\kappa}$\;
$W \leftarrow W \cup \{(b, \outcome')\} $\;
}
$g\leftarrow\adv(\outcome, \tpf, W)$\;
\eIf{$g = \beta \land\allowbreak \balanced(\bb,\nC,L) \wedge\allowbreak |\bb| \leq \mB \wedge\allowbreak \nC\leq \mC$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
Oracle $\oracleSymb$ is defined as follows:
\ifnocompress
%
\begin{itemize}
\item
\fi
$\oracle{v_0,v_1}$ computes
$b\leftarrow \Vote{v_\beta,\kappa}; L \leftarrow L \cup \{ (b, v_0, v_1)\}$
and
outputs $b$, where $v_0,v_1\in \{1, ...,\nC \}$.
\ifnocompress
\end{itemize}
\fi
\ifnocompress
\noindent
\fi%
We say $\Gamma$ satisfies \emph{ballot secrecy ($\BallotSecrecy$)}, 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
$\Succ(\BallotSecrecy(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \allowbreak\leq \frac{1}{2}+
\mathsf{negl}(\kappa)$.
\end{definition}
Our formalisation of ballot secrecy challenges an adversary to determine
whether the left-right oracle produces ballots for ``left'' or ``right'' inputs. In addition to the
oracle's outputs, the adversary is given the election outcome and tallying proof derived by tallying the
board\ifnocompress\ (intuitively, this captures a setting where the bulletin board is constructed by an adversary
that casts ballots on behalf of a subset of voters and controls the distribution of votes cast by the remaining voters)\fi. The adversary is also given a mapping, denoted $W$ in Definition~\ref{def:ballotSecrecy}, from ballots to votes, for all ballots on the bulletin board which were not output by the oracle.
To avoid trivial distinctions, we insist that oracle queries are balanced, i.e.,
predicate $\balanced$ must hold.
Intuitively, if the adversary does not succeed, then ballots for different votes cannot be distinguished, hence, a voter cannot be linked to a vote, i.e., ballot secrecy is preserved. By comparison, if the adversary succeeds, then ballots can be distinguished and ballot secrecy is not preserved.
\ifnocompress
\paragraph{Comparing notions of ballot secrecy.}
The adversary is given the outcome corresponding to tallying \emph{any} ballot that was
\emph{not} computed by the oracle in $\BallotSecrecy$, whereas
the adversary does not have this capability in the definition by
Smyth \cite{Smyth15-ballot-independence}. Formally, the definition of ballot secrecy by Smyth, henceforth $\SBBallotSecrecy$,
can be derived from $\BallotSecrecy$ by removing the for-loop and replacing
$\adv(\outcome, \tpf, W)$ with $\adv(\outcome, \tpf)$.
%
%\sINDCVAX\ strengthens XYZ by giving the adversary access to $W$, hence,
It is trivial to see that $\BallotSecrecy$ strengthens $\SBBallotSecrecy$, because
any adversary against $\SBBallotSecrecy$ (without access to $W$) is also an adversary
against $\BallotSecrecy$ (with access to $W$).
%\sout{In \refappendix{\ref{app:ballot-secrecy}}, we show that $\BallotSecrecy$
%is strictly stronger using a scheme that satisfies $\SBBallotSecrecy$ but not $\BallotSecrecy$, hence
%separating the two notions.}
Moreover, $\BallotSecrecy$ is strictly stronger (Proposition~\ref{prop:ballot-secrecy-relatedd}), because the outcome might leak information.\footnote{Parallel decryption leaks information similarly~\cite[Appendix~A]{Bernhard11:Helios}.}
\begin{proposition}\label{prop:ballot-secrecy-relatedd}
$\BallotSecrecy$ is strictly stronger than $\SBBallotSecrecy$.
\end{proposition}
\ifincludeBS
\noindent
Nonetheless, we present conditions under which the two notions coincide (\S\ref{sec:scope-bs}).
\fi
\fi
\ifnocompress
\subsubsection{Example: $\mv$ satisfies ballot secrecy}
Intuitively, given an encryption scheme $\Pi$ satisfying non-malleability, the
election scheme $\mv(\Pi)$ derives ballot secrecy from the
encryption scheme until tallying and tallying maintains ballot secrecy by only disclosing the number of votes for each candidate. Formally, the following holds.\footnote{Bellare \& Sahai~\cite[\S5]{Bellare99:IND-k-CPA} show that their notion of non-malleability ($\gameShortNM$) coincides with
a simpler indistinguishability notion ($\INDPA$), thus it suffices to consider $\INDPA$
in Proposition~\ref{prop:mv}.}
\begin{proposition}\label{prop:mv}
Suppose $\Pi$ is an asymmetric encryption scheme with perfect correctness.
If $\Pi$ satisfies $\INDPA$, then $\mv(\Pi)$ satisfies $\BallotSecrecy$.
\end{proposition}
\fi
%\noindent We prove Proposition~\ref{prop:mv} in~\refappendix{\ref{sec:proof:privacy}}.
\iffalse
\subsection{Correctness with malicious bulletin boards}
\begin{definition}
Let $\Gamma = (\SetupSymb,\VoteSymb,\TallySymb, \VerSymb)$ be
an election scheme, $\RevealSymb$ be a reveal algorithm, $\adv$ be an
adversary,
$\kappa$ be a security parameter, and $\textsf{Mal-Correct}$ be the following
game.
\textcolor{red}{BEN: We need to know what $b$ is to simulate it.}
\begin{inlineexperiment}{$\textsf{Mal-Correct}(\Gamma,\RevealSymb,\adv,\kappa)$}
$(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$;\\
$(\nC,v,\bb)\leftarrow \adv(\pk)$;\\
$(\outcome, \tpf) \leftarrow \TallySymb(\sk, \nC, \bb)$;\\
$b \leftarrow \RevealSymb{(\sk, \nC, \bb, \outcome, v,\kappa)}$;\\
\eIf{$1\leq v\leq \nC \wedge \left(\outcome[v] \geq 1 \not\Rightarrow
\exists r \mathrel . b = \VoteSymb(\pk,\nC,v; r) \wedge b \in \bb\right) \wedge
\left(\outcome[v] = 0 \not\Rightarrow b={\perp}\right)$
}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
\noindent
We say $\RevealSymb$ satisfies correctness with malicious bulletin boards for
$\Gamma$, 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(\textsf{Mal-Correct}(\Gamma,\RevealSymb,\adv,\kappa)) \leq
\mathsf{negl}(\kappa)$.
\end{definition}
\fi
\ifnocompress
\subsection{Relations between ballot and bid secrecy}
\fi
\label{sec:result-privacy}
%\marginpar{The text in blue needs to be \emph{truthified}, that is,
%any factual errors need to be removed!}
\iffalse
\sout{Correctness properties for election schemes and reveal algorithms ensure
that our construction operates correctly under ideal conditions. To ensure that
our construction will operate correctly in the presence of an adversary, we
formulate soundness properties. These soundness properties are also sufficient
to prove that our construction achieves bid secrecy, assuming the underlying
election scheme satisfies ballot secrecy.}
\fi
The main distinctions between\ifnocompress\ our formalisations of\fi\ privacy for elections
and auctions are\ifnocompress\ as follows.\else:\fi
\begin{enumerate}
\item Our ballot secrecy game \emph{tallies} the bulletin board, whereas our
bid secrecy game \emph{opens} the bulletin board.
\item Our ballot secrecy game is intended to protect the privacy of
all voters, whereas our bid secrecy game is only intended to protect the privacy
of losing bidders. %\sout{, hence, our bid secrecy game avoids crediting the
%adversary for trivial and unavoidable distinctions which hold iff the adversary
%casts a winning bid on behalf of an honest bidder}.
\item Our ballot secrecy game provides the adversary with the
vote corresponding to \emph{any} ballot that was \emph{not} computed by the
oracle,
whereas the adversary is not given a similar mapping in our bid secrecy game.
\iffalse
\sout{This final point is crucial to our main security proof, since it allows
a ballot secrecy adversary to simulate the bid secrecy challenger, in
particular, the adversary can simulate algorithm $\RevealSymb$, which
is used to derive the winnings bids.}
\fi
\end{enumerate}
%\noindent Thus, ballot secrecy is intuitively stronger than bid secrecy,
%which is indeed the desired result. This intuition is true for the
%class of election schemes that satisfy the soundness properties that we formulate
%below.
\noindent
These distinctions support our intuition: we can construct auction schemes
satisfying bid secrecy from election schemes satisfying ballot secrecy.
Yet, interestingly, ballot secrecy alone is insufficient to ensure that our construction
produces auction schemes satisfying bid secrecy. This is because our construction
is reliant upon the underlying tally algorithm, and a poorly designed tally algorithm could lead to the construction of
auction schemes that do not satisfy bid secrecy.
In particular, a tally algorithm that outputs an incorrect winning price (in the presence of an adversary) can cause the set of bids for this price to be disclosed, thereby enabling losing bidders that bid at this price to be identified, which violates bid secrecy.
(E.g., suppose Alice, Bob and Charlie bid for 1, 2 and 3, respectively. And suppose 2 is incorrectly announced as the winning price. Hence, Bob is linked to his bid, which violates bid secrecy.)
Tallying algorithms that output incorrect winning prices can satisfy
correctness, because correctness does not consider an adversary, hence, tallying
might produce correct output under ideal conditions and incorrect output in the presence
of an adversary.
%\sout{Similarly, our construction is reliant upon the underlying reveal algorithm
%to ensure bid secrecy.}
This leads to a separation result (cf. \refappendix{\ref{app:separationBidBallotSecrecy}}).
Moreover, our construction is also reliant upon the underlying reveal algorithm,
which might output an incorrect set of ballots (in the presence of an adversary),
hence, there is a further separation.
Nevertheless, we can formulate soundness conditions (that must hold in the presence of adversaries) which capture a class of election
schemes for which our intuition holds.
%\textcolor{blue}{BEN: I'm slightly inclined to switch the ordering of tally soundness and reveal soundness,
%because reveal soundness is more important for our results. But, I don't feel particularly strongly.
%Liz, if you think it will be useful, then let's switch.}
%\marginpar{BEN: I renamed \emph{tally soundness} ($\mathsf{Tally}\textrm{-}\allowbreak\mathsf{Soundness}$) as \emph{weak tally soundness} ($\TallySoundness$), because it doesn't capture what is typically considered to be soundness. If I remember correctly, a reviewer questioned the validity of the definition and I wonder if that was why. By renaming I think we avoid criticism.}
\ifnocompress
\paragraph{Weak tally soundness.}
\fi
\label{sec:tally:soundness}
Correctness for election schemes ensures that algorithm $\TallySymb$
produces the expected election outcome under ideal conditions. A similar
property, which we call \emph{weak tally soundness},
can hold in the presence of an adversary. Our formulation of weak tally soundness (Definition~\ref{def:tally-soundness}) challenges the adversary to concoct
a scenario in which the election outcome does not include the votes of all ballots on the bulletin board that were produced by $\VoteSymb$.\footnote{%
Our construction produces\ifnocompress\ auction\fi\ schemes satisfying bid secrecy when the\ifnocompress\ underlying\fi\ tallying algorithm produces\ifnocompress\ election\fi\ outcomes containing too many votes for some candidates. (E.g., suppose Alice, Bob and Charlie bid for 1, 2 and 3, respectively\ifnocompress. And suppose\else, and\fi\ 4 is incorrectly announced as the winning price. In this case no bids are linked to that price, thus bid secrecy is preserved.) And weak tally soundness can be satisfied by such schemes.\ifnocompress\ Thus, there is a further distinction between weak tally soundness and correctness.\fi}
\ifnocompress
\fi
We capture correct
election outcomes using function $\correcttally$,\footnotemark\linebreak which is defined such that for all
$\pk$, $\nC$, $\bb$, $\kappa$, $\ell$, and $v \in \{1,\ldots,\nC\}$,
we have $\correcttally(\pk,\nC,\bb,\kappa)$ is a vector of length $\nC$ and
%\begin{multline*}
$\correcttally(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak\kappa)[v] = \ell %\\
\iff \exists^{=\ell} b\in \bb \setminus \{\bot\} :
\exists r : b=\VoteSymb(\pk,\nC,v,\kappa; r)$.
%\end{multline*}
That is, component $v$ of vector
$\correcttally(\pk,\bb,\allowbreak \nC,k)$
equals $\ell$ iff there exist $\ell$ ballots on the bulletin board that are votes for candidate $v$.
%
\footnotetext{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.}
%
\begin{definition}[Weak tally soundness]\label{def:tally-soundness}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$ be
an election scheme, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\TallySoundness(\allowbreak\Gamma,\allowbreak\adv,\allowbreak\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\TallySoundness(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$\;
$(\nC,\bb) \leftarrow \adv(\pk,\kappa)$\;
$(\outcome,\tpf) \leftarrow \TallySymb(\sk, \nC,\bb,\kappa)$\;
\eIf{$\exists v\in\{1,\dots,\nC\} \mathrel . \outcome[v] < \correcttally(\pk,\nC,\bb, \kappa)[v]\wedge\allowbreak
|\bb| \leq \mB \wedge\allowbreak \nC \leq \mC$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies \emph{weak tally soundness ($\TallySoundness$)}, 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(\TallySoundness(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \leq \mathsf{negl}(\kappa)$.
\end{definition}
\oldlater{\textcolor{red}{A result along the following lines would be nice}
\begin{proposition}
Let $\Gamma$ be exists an election scheme, $\RevealSymb$ be a reveal algorithm,
and $\Delta$ be a non-interactive proof system for relation $R(\Gamma,\RevealSymb)$.
Moreover, let $\Sigma = \Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta)$.
If $\Gamma$ satisfies ballot secrecy, $\Delta$ is zero-knowledge,
$\RevealSymb$ is correct with respect to $\Gamma$, and
$\Gamma$ does not satisfy weak tally soundness,
then $\Sigma$ does not satisfy bid secrecy.
\end{proposition}
}
\iffalse
\subsubsection{Partial tallying}
\emph{Partial tallying} asserts that independently tallying a ballot $b$
and a bulletin board $\bb$ produces the same result as tallying $\bb \cup \{b\}$. \textcolor{red}{...XYZ...}
\begin{definition}[Partial tallying]
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$ be
an election scheme, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\PartialTallying(\Gamma,\adv,\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\PartialTallying(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$\;
$(\nC,b,\bb) \leftarrow \adv(\pk,\kappa)$\;
$(\outcome_1,\tpf_1) \leftarrow \TallySymb(\sk, \nC,\bb,\kappa)$\;
$(\outcome_2,\tpf_2) \leftarrow \TallySymb(\sk, \nC,\{b\},\kappa)$\;
$(\outcome,\tpf) \leftarrow \TallySymb(\sk, \nC,\bb\cup\{b\},\kappa)$\;
\eIf{$\outcome \not= \outcome_1 + \outcome_2 \wedge b\not\in\bb\wedge\allowbreak
|\bb\cup\{b\}| \leq \mB \wedge\allowbreak \nC \leq \mC$}{
\Return $1$
}{
\Return $0$
}
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies \emph{partial tallying}, 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(\PartialTallying(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \leq \mathsf{negl}(\kappa)$.
\end{definition}
\noindent
Given that election scheme correctness ensures the expected election outcome under ideal conditions, we have by weak
tally soundness that the election outcome includes the votes of
all ballots on the bulletin board that were produced by $\VoteSymb$.
\fi
\ifnocompress
\paragraph{Reveal soundness.}
\fi
%\sout{Correctness for reveal algorithms provides guarantess under ideal condititions and a similar property %, which we call reveal soundness,
%can hold in the presence of an adversary.}
Correctness for reveal algorithms ensures that algorithm $\RevealSymb$
produces the set of ballots for a particular vote under ideal conditions. A similar
property, which we call \emph{reveal soundness},
can hold in the presence of an adversary.
%
%\begin{itemize}
% \item \sout{{Reveal soundness}: \textcolor{red}{$\RevealSymb$ outputs the set of all (if any) ballots encapsulating a specific price, even when the bulletin
% board is maliciously generated.}
% \textcolor{magenta}{BEN: I favour the following (it is shorter!)} \textcolor{red}{the set of ballots for a particular vote is computed properly.} \textcolor{magenta}{BEN: but perhaps it is too abstract?}
%}
%\end{itemize}
%
%\noindent
Our formulation of reveal soundness %(Definition~\ref{def:reveal-soundness})
challenges the adversary to
output a vote and bulletin board for which
the reveal algorithm produces a set of ballots
that does not coincide with the set of ballots on the bulletin board
that tally to that vote.
%\subsubsection{Reveal \textcolor{red}{XYZ}}
%We formalise a property for the $\RevealSymb$ algorithm, namely
%\emph{\textcolor{blue}{reveal soundness}}.
\begin{definition}[Reveal soundness]\label{def:reveal-soundness}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$ be
an election scheme, $\RevealSymb$ be a reveal algorithm,
$\adv$ be an adversary,
$\kappa$ be a security parameter, and $\RevealSoundness(\Gamma,\allowbreak\adv,\allowbreak\kappa)$ be the following game.
{\upshape
\begin{inlineexperiment}{$\RevealSoundness(\Gamma,\adv,\kappa)$}
$(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa]$\;
$(\nC,\bb,v)\leftarrow\adv(\pk, \kappa)$\;
$\mathfrak b \leftarrow \RevealSymb{( \sk, \nC, \bb, v,\kappa)}$\;
$W\leftarrow \emptyset$\;
\For{$b\in\bb$}{
$(\outcome, \tpf)\leftarrow\TallySymb( \sk, \nC,
\{b\},\kappa)$\;
$W\leftarrow W \cup \{(b,\outcome)\}$\;
}
\eIf{$\mathfrak b \not= \{b \mid (b,\outcome)\in W \wedge \outcome[v] = 1 \}\wedge\allowbreak|\bb| \leq \mB \wedge \allowbreak 1 \leq v \leq \nC \leq \mC$}{
\Return $1$
}{
\Return $0$
}
\begin{comment}
%This simplification might help the \emph{scope} section, and it might make proofs easier. (Albeit, we'll need to modify current proofs.) I don't yet know whether we can/should adopt it.}
%It doesn't seem plausible to remove reveal soundness, because we don't know whether Tally works in non-verifiable schemes. This causes problems in proofs, e.g., "B [simulating] Reveal to produce b" in Prop~\ref{prop:privacyResult}.
\begin{color}{red}
\sout{$W\leftarrow \emptyset$}\;
\For{\sout{$b\in\bb$}}{
\sout{$(\outcome, \tpf)\leftarrow\TallySymb( \sk, \nC,
\{b\},\kappa)$}\;
\sout{$W\leftarrow W \cup \{(b,\outcome)\}$}\;
}
\end{color}
\eIf{$\mathfrak b \not=
\textcolor{red}{\textrm{\sout{$\{b \mid (b,\outcome)\in W \wedge \outcome[v] = 1 \}$}}}
\textcolor{blue}{\{b \mid b\in \bb \wedge \correcttally(\pk,\nC,\{b\}, \kappa)[v] = 1 \}}
\wedge\allowbreak|\bb| \leq \mB \wedge \allowbreak 1 \leq v \leq \nC \leq \mC$}{
\Return $1$
}{
\Return $0$
}
\end{comment}
\end{inlineexperiment}
}
\noindent
We say $\RevealSymb$ satisfies \emph{reveal soundness with respect to} $\Gamma$, 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(\allowbreak\RevealSoundness(\Gamma,\allowbreak\adv,\allowbreak\kappa)) \leq \mathsf{negl}(\kappa)$.
\end{definition}
\ifnocompress
\begin{lemma}\label{lemma:revealSoundnessImpliesCorrectness}
Let $\Gamma$ be an election scheme and $\RevealSymb$ be a reveal algorithm.
If $\RevealSymb$ satisfies reveal soundness with respect to $\Gamma$,
then $\RevealSymb$ is correct with respect to $\Gamma$.
\end{lemma}
\fi
%\ifincludeScope
%\textcolor{red}{We demonstrate that reveal algorithms satisfying
%reveal soundness exists for all election schemes in \refappendix{\ref{sec:existence}}.}
%\fi
\oldlater{\textcolor{red}{A result along the following lines would be nice}
\begin{proposition}\label{prop:separationBidBallotSecrecyB}
Let $\Gamma$ be exists an election scheme, $\RevealSymb$ be a reveal algorithm,
and $\Delta$ be a non-interactive proof system for relation $R(\Gamma,\RevealSymb)$.
Moreover, let $\Sigma = \Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta)$.
If $\Gamma$ satisfies ballot secrecy, $\Delta$ is zero-knowledge,
$\RevealSymb$ is correct with respect to $\Gamma$, and
$\RevealSymb$ does not satisfy reveal soundness with respect to $\Gamma$,
then $\Sigma$ does not satisfy bid secrecy.
\end{proposition}
}
\oldlater{\textcolor{red}{A result along the following lines would be nice}
\begin{proposition}%\label{prop:separationBidBallotSecrecy}
There exists an election scheme $\Gamma$, a reveal algorithm $\RevealSymb$,
and a non-interactive proof system $\Delta$ for relation $R(\Gamma,\RevealSymb)$,
such that $\Gamma$ satisfies ballot secrecy, $\Delta$ is zero-knowledge,
$\RevealSymb$ is correct with respect to $\Gamma$, and
$\Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta)$ does not satisfy bid secrecy,
assuming either $\Gamma$ does not satisfy weak tally soundness or
$\RevealSymb$ does not satisfy reveal soundness with respect to $\Gamma$.
\end{proposition}
}
\ifnocompress
\subsubsection{Bid secrecy for non-verifiable auction schemes}\label{sec:secrecy:non-verifiable:schemes}
We prove that our construction presented in Section \ref{sec:trans:1} produces auction schemes satisfying bid secrecy, assuming the underlying election scheme satisfies ballot secrecy and weak tally soundness,
and the underlying reveal algorithm satisfies reveal soundness.
\begin{proposition}\label{prop:privacyResult}
Let $\Gamma$ be an election scheme and $\RevealSymb$ be a reveal algorithm.
%Moreover, let $\Sigma = \Lambda(\Gamma,\RevealSymb)$.
If $\Gamma$ satisfies $\BallotSecrecy$ and $\TallySoundness$, and
$\RevealSymb$ satisfies reveal soundness with respect to $\Gamma$,
then $\Lambda(\Gamma,\RevealSymb)$ satisfies $\BidSecrecy$.
\end{proposition}
%\noindent We prove Proposition~\ref{prop:privacyResult} in~\refappendix{\ref{sec:proof:privacy}}.
\noindent We demonstrate the applicability of our result in the following example.
\newcommand{\tsduhfuskdhf}{Example: $\mathsf{Enc2Bid}$ satisfies bid secrecy}
\iftr
\subsubsection*{\tsduhfuskdhf}
\else
\paragraph{\tsduhfuskdhf.}
\fi
%
Intuitively, given a non-malleable asymmetric encryption scheme $\Pi$, auction scheme $\mathsf{Enc2Bid}(\Pi)$ derives bid secrecy from
the encryption scheme until opening and opening maintains bid secrecy by only disclosing winning bids and the winning price. We can use our construction and accompanying security results to formally prove this result.
\begin{proposition}\label{prop:enc2bid}
Suppose $\Pi$ is an asymmetric encryption scheme with perfect
correctness. If $\Pi$ satisfies $\INDPA$, then $\mathsf{Enc2Bid}(\Pi)$
satisfies $\BidSecrecy$.
\end{proposition}
\begin{proof}
Let us suppose there exists
a reveal algorithm $\RevealSymb\textrm{-}\mathsf{Enc2Bid}(\Pi)$ such
that $\mathsf{Enc2Bid}(\Pi)$ is equivalent to
$\Lambda(\mathsf{Enc2Vote}(\Pi),\allowbreak {\RevealSymb\textrm{-}\mathsf{Enc2Bid}(\Pi)})$.
Hence, we can use Proposition~\ref{prop:privacyResult} to prove that
$\mathsf{Enc2Bid}(\Pi)$ satisfies bid secrecy.
We defer formalising a suitable reveal algorithm to \refappendix{\ref{sec:proofs}}.
\end{proof}
%\noindent We prove Proposition~\ref{prop:enc2bid} in~\refappendix{\ref{sec:proof:privacy}}.
\subsubsection{Bid secrecy for verifiable auction schemes}\label{sec:secrecy:verifiable:schemes}
We generalise Proposition~\ref{prop:privacyResult} to verifiable auction schemes, assuming the non-interactive proof system
is zero-knowledge.
\else
\ifnocompress
\subsubsection{Bid secrecy}\fi\label{sec:secrecy:verifiable:schemes}
We prove that our construction produces auction schemes satisfying bid secrecy, assuming the underlying election scheme satisfies ballot secrecy and weak tally soundness,
the underlying reveal algorithm satisfies reveal soundness, and
the non-interactive proof system is zero-knowledge.
\fi
%\marginpar{\iftr BEN: I wonder if the weaker definition of ballot secrecy suffices when we have extractability.\\ Perhaps we can show that the weaker definition coincides with our definition when we have extractability. We'll need a definition of extractability for election schemes, rather than one involving the Fiat-Shamir transformation. \fi}
\begin{theorem}\label{thm:privacyResult}
Let $\Gamma$ be an election scheme, $\RevealSymb$ be a reveal algorithm,
and $\Delta$ %$(\ProveSymb, \VerifySymb)$
be a non-interactive proof system for relation $R(\Gamma,\RevealSymb)$.
%Moreover, let $\Sigma = \Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak
%\Delta %(\ProveSymb,\allowbreak \VerifySymb)
%)$.
If $\Gamma$ satisfies $\BallotSecrecy$ and $\TallySoundness$,
$\RevealSymb$ satisfies reveal soundness with respect to $\Gamma$, and
$\Delta$ is zero-knowledge, then
$\Lambda(\Gamma,\allowbreak\RevealSymb,\allowbreak\Delta)$ satisfies $\BidSecrecy$.
\end{theorem}
%\noindent We prove Theorem~\ref{thm:privacyResult} in~\refappendix{\ref{sec:proof:privacy}}.
%\marginpar{Section~\ref{sec:uv:election} appears in long version.}
In \ifnocompress{}Section~\ref{sec:uv:election}\else{the companion technical report}\fi, we show that weak tally soundness is implied by universal verifiability, hence, a special case of the above theorem requires that
$\Gamma$ satisfies universal verifiability, rather than weak tally soundness.
\begin{comment}
The scope of Theorem~\ref{thm:privacyResult} depends on
the existence of a reveal algorithm $\RevealSymb$ and
a non-interactive proof system $\Delta$ for relation $R(\Gamma,\RevealSymb)$,
such that $\Delta$ satisfies zero-knowledge and
$\RevealSymb$ satisfies reveal soundness with respect to $\Gamma$.
We have seen that suitable reveal algorithms exist for all
election schemes (Section~\ref{sec:reveal}).
And we demonstrate that suitable non-interactive proof systems
exist for a large class of election schemes in Appendix~\ref{sec:scope-zk}.
\ifincludeBS Moreover, we provide conditions under which
$\BallotSecrecy$ coincides with an existing notion of ballot secrecy.
\end{comment}
%\ifincludeScope
%\textcolor{red}{We demonstrate the scope of Theorem~\ref{thm:privacyResult} in
%Section~\ref{sec:scope}, and show that it is useful to derive a secure auction scheme
%from Helios in Section~\ref{sec:helios}.}
%\fi
```
# Verifiability results
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 246, column 1): unexpected } expecting \end{definition} } ^`
``` latex
\section{Verifiability results}\label{sec:verifiability:results}
\ifnocompress
We recall definitions of verifiability
by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}.\footnote{We discuss the suitability of the definition by Smyth, Frink \& Clarkson in Section~\ref{sec:applicability}.}\textsuperscript{,}\footnote{Quaglia \& Smyth present a tutorial-style introduction to modelling verifiability~\cite{Smyth17:voting-tutorial}, and Smyth provides a technical introduction~\cite{Smyth18:voting-tutorial}.}
We show that these definitions are sufficient to ensure that our construction produces
schemes satisfying auction verifiability.
\else
We show that definitions of individual ($\ExpIVSymb$) and universal
($\ExpUVSymb$) verifiability by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}
are sufficient to ensure that our construction produces
schemes satisfying auction verifiability.
\fi
\begin{comment}
\footnotetext{
%
We adopt verifiability definitions by Smyth, Frink \& Clarkson~\cite{Smyth15:ElectionVerifiability}
for the following reasons.
First, their definitions improve upon earlier definitions,
e.g.,~\cite{JCJ10,Cortier14:verifiability,Kiayias15}, to detect attacks that arise when
tallying and verification procedures collude, when verification procedures reject legitimate
outcomes, and when the adversary controls the bulletin board and the communication channel.
Secondly, their definitions are strictly stronger than some notions of
global verifiability.
Thirdly, their definitions have proven to be useful in correctly identifying
three schemes that do not satisfy verifiability, and in identifying two schemes
that do.
Finally, Helios satisfies their definitions,
which will be useful in our case study\ifnocompress\ (Section~\ref{sec:helios})\fi.
Our verifiability results could be extended to other definitions of verifiability,
e.g.,~\cite{Kusters10,Cortier16:VerifiabilitySoK}, by modifying our proofs.
}
\end{comment}
\ifnocompress
\subsection{Election verifiability}\label{sec:verifiability}
\subsubsection{Individual verifiability}\label{sec:iv:election}
Individual verifiability challenges the adversary to
generate a collision from algorithm $\VoteSymb$.
\begin{definition}[Individual verifiability~\cite{Smyth15:ElectionVerifiability}]\label{def:election-iv}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme, $\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 \emph{individual verifiability ($\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}
\subsubsection{Universal verifiability}\label{sec:uv:election}
Universal verifiability challenges the adversary to concoct
a scenario in which $\VerSymb$ accepts, but the election outcome is not correct.
%
\iffalse %%Now appears earlier
Formally, we capture the notion of a correct
tally using function $\correcttally$, which is defined such that for all
$\pk$, $\nC$, $\bb$, $\kappa$, $\ell$, and $v \in \{1,\ldots,\nC\}$,
we have\footnotemark
\begin{multline*}
\correcttally(\pk,\nC,\bb,\kappa)[v] = \ell \\
\iff \exists^{=\ell} b\in \bb \setminus \{\bot\} :
\exists r : b=\VoteSymb(\pk,\nC,v,\kappa; r)
\end{multline*}
That is, component $v$ of vector
$\correcttally(\pk,\bb,\allowbreak \nC,k)$
equals $\ell$ iff there exist $\ell$ ballots on the bulletin board that are votes for candidate $v$.
The vector produced by $\correcttally$ must be of length $\nC$.
%
\footnotetext{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.}
%
\fi
%
Formally, we capture the correct election outcome
using function $\correcttally$.
Since function $\correcttally$ will now be parameterised with a public key
constructed by the adversary, rather than a public key constructed by
algorithm $\SetupSymb$ (cf. Section~\ref{sec:tally:soundness}), we must adopt a stronger definition of injectivity
which holds for adversarial keys. We define \emph{strong injectivity}
in \refappendix{\ref{cciforelec}}.
\begin{definition}[Universal verifiability~\cite{Smyth15:ElectionVerifiability}]\label{def:EEEEUV}
Let $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak\VerSymb)$ be an election scheme satisfying strong injectivity, $\adv$ be an adversary,
$\kappa$ be a security parameter, and $\ExpUV$ be the following game.
{\upshape
\begin{inlineexperiment}{$\ExpUV$}
$(\pk,\nC,\bb,\outcome, \tpf) \leftarrow \adv(\kappa)$\;
\eIf{$\outcome \not= \correcttally(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak \kappa) \allowbreak\mathrel\wedge \VerSymb(\pk,\allowbreak\nC,\allowbreak\bb,\allowbreak \outcome,\allowbreak\tpf,\allowbreak\kappa) = 1 $}{
\Return 1
}{
\Return 0
}
\end{inlineexperiment}
}
\noindent
We say $\Gamma$ satisfies \emph{universal verifiability ($\ExpUVSymb$)},
if for all probabilistic polynomial-time adversaries $\adv$,
there exists a negligible function $\mathsf{negl}$, such that
for all security parameters $\kappa$, we have $\SuccUV \leq \mathsf{negl}(\kappa)$.
\end{definition}
%\textcolor{red}{LIZ: Is the following in your verifiability paper? If so, we dont need it. If not, I still think we do not need to demonstrate the applicability
%of notions we have not introduced here. Hence I propose to remove the following subsection.}
\iffalse
\begin{definition}[Reveal soundness]
Suppose $(\SetupSymb,\VoteSymb,\TallySymb, \VerSymb)$ is an election scheme and $\RevealSymb{(\pk, \sk, \nC, \bb, v, \kappa)}$ is a reveal algorithm,
we say $\RevealSymb$ satisfies \textcolor{blue}{reveal soundness} if there exists a negligible function $\mathsf{negl}$, such that for all security parameters $\kappa$, bulletin boards $\bb$, integers $\nC$, and votes $v\in\{1,\dots,\nC\}$, we have
%
\begin{multline*}
\Pr[(\pk,\sk,\mB, \mC) \leftarrow \Setup[\kappa];
\mathfrak b \leftarrow \RevealSymb{(\pk, \sk, \nC, \bb, v,\kappa)}:\\
((\pk,\nC,\bb,v,\mathfrak b,\kappa),\;\sk) \in R]\geq 1-\mathsf{negl}(\kappa).
\end{multline*}
\end{definition}
\fi
%\textcolor{red}{LIZ: The following (up to Corollary 11) seems a bit of a digression and takes focus away from results. Do we need it here?} \textcolor{red}{BEN: Given that Corollary~\ref{cor:uv:soundness} is a corollary of Lemma~\ref{lem:uv:soundness}, removing Lemma~\ref{lem:uv:soundness} means that Corollary~\ref{cor:uv:soundness} is no longer a corollary. Also, Lemma~\ref{lem:uv:soundness} is used in a proof sketch of Helios, so this proof sketch would need revising if you remove Lemma~\ref{lem:uv:soundness}.}
Universal verifiability is similar to weak tally soundness, in particular,
both notions challenge the adversary to concoct a scenario in which the
election outcome is not correct.
The election outcome is computed by the challenger using algorithm
$\TallySymb$ in $\TallySoundness$. By comparison, the outcome is chosen
by the adversary in $\ExpUVSymb$, under the condition that it
must be accepted by algorithm $\VerSymb$. Since completeness
asserts that outcomes output by $\TallySymb$ will
be accepted by $\VerSymb$, we have the following result.
\begin{lemma}\label{lem:uv:soundness}
Let $\Gamma$ be an election scheme. If $\Gamma$ satisfies $\ExpUVSymb$, then $\Gamma$ satisfies $\TallySoundness$.
\end{lemma}
\noindent
It is trivial to see that universal verifiability is strictly stronger
than weak tally soundness, because $\mv$ satisfies weak
tally soundness (see proof of Proposition~\ref{prop:enc2bid}\iftr\else, in \refappendix{\ref{app-proofs}}\fi),
but not universal verifiability (it accepts any election outcome).
\begin{corollary}\label{cor:uv:soundness}
$\ExpUVSymb$ is strictly stronger than $\TallySoundness$.
\end{corollary}
\noindent
The proof of Corollary~\ref{cor:uv:soundness} follows from Lemma~\ref{lem:uv:soundness}
and the above reasoning. We omit a formal proof.
%\noindent We prove Lemma~\ref{lem:uv:soundness} in~\refappendix{\ref{sec:proof:verifiability}}.
\subsection{Election verifiability implies auction verifiability}\label{sec:result:verifiability}
The following results demonstrate that our second construction (\S\ref{sec:trans:2}) produces verifiable auction schemes from verifiable election schemes.
\fi
\begin{theorem}\label{thm:iv}
Let $\Gamma$ be an election scheme, $\RevealSymb$ be a reveal algorithm, and
$\Delta$ %$(\ProveSymb, \VerifySymb)$
be a non-interactive proof system for relation $R(\Gamma,\RevealSymb)$,
such that $\RevealSymb$ is correct with respect to $\Gamma$.
If $\Gamma$ satisfies $\ExpIVSymb$,
then $\Lambda(\Gamma,\RevealSymb,
\Delta%(\ProveSymb, \VerifySymb)
)$ satisfies $\ExpAIVSymb$.
\end{theorem}
\ifnocompress
\noindent The proof of Theorem~\ref{thm:iv} follows from Definitions~\ref{def:auction-iv}, \ref{def:transform} \&~\ref{def:election-iv} and we omit
a formal proof.
\fi
For universal verifiability, we require the non-interactive proof system to satisfy a notion of
soundness. This notion can be captured by the following property on relation $R(\Gamma,\RevealSymb)$.
%\ifincludeScope
%\textcolor{red}{Moreover, we demonstrate that the notion can be satisfied
%for all election schemes in \refappendix{\ref{sec:existence}}.}
%\fi
\begin{definition}
Given an election scheme $\Gamma = (\SetupSymb,\allowbreak\VoteSymb,\allowbreak\TallySymb,\allowbreak \VerSymb)$
and a reveal algorithm $\RevealSymb$, we say relation $R(\Gamma,\RevealSymb)$
is \emph{\verifiableRelation}, if $((\pk,\allowbreak\nP,\allowbreak\bb,\allowbreak{}p,\allowbreak\mathfrak b,\allowbreak\kappa),\;\sk) \in R(\Gamma,\allowbreak\RevealSymb)$
implies $\correctballots(\pk,\nP,\bb,p,\mathfrak b,\kappa)$
\ifhorriblehacks\pagebreak[1]\fi
with overwhelming probability.
\end{definition}
\begin{theorem}\label{thm:uv}
Let $\Gamma$ be an election scheme, $\RevealSymb$ be a reveal algorithm
that is correct with respect to $\Gamma$, and
$\Delta$ %$(\ProveSymb, \VerifySymb)$
be a non-interactive proof system for relation $R(\Gamma,\RevealSymb)$.
If $\Gamma$ satisfies $\ExpUVSymb$, $\Delta$ satisfies {soundness},
and $R(\Gamma,\RevealSymb)$ is \verifiableRelation, then $\Lambda(\Gamma,\RevealSymb,
\Delta %(\ProveSymb, \VerifySymb)
)$ satisfies $\ExpAUVSymb$.
\end{theorem}
%\noindent We prove Theorem~\ref{thm:uv} in~\refappendix{\ref{sec:proof:verifiability}}.
\iffalse
\subsection{Example: $\Nonce$ satisfies auction verifiability}
\textcolor{red}{BEN: This is a bad example to use, because we cannot rely on our results in an
elegant manner. This is because our results are intended to simultaneously permit
secrecy and verifiability, hence, to merely derive verifiability our results are
overkill. For instance, compare the auction scheme derived from $\NonceVote$ using our
transformation with $\Nonce$. Much of what our transformation does is redundant, because $\Nonce$ doesn't
preserve privacy. I suggest we drop this section. The following section can serve as
an example. I am also slightly in favour of dropping $\Nonce$, because its value is now
rather limited. (If we don't drop it, then we should remove
``\emph{We defer a formal proof to Section~\ref{sec:transformation}, where we can use our election to
auction scheme transformation and accompanying security results.}" and omit a formal proof.}
\textcolor{red}{We haven't included $\NonceVote$, so technically we aren't self-contained...}
Let $\Nonce'$ be a variant of $\Nonce$ such that opening outputs $(p,\mathfrak b,({\perp},\allowbreak{\perp},\allowbreak{\perp}))$,
rather than $(p,\mathfrak b,\perp)$, and verification fails if the proof is not a vector of length $3$.
Moreover, let $\NonceVote$ be the election scheme proposed by Smyth, Frink \& Clarkson~\cite[\S2.4]{Smyth15:ElectionVerifiability}. We present a reveal algorithm $\RevealSymb\textrm{-}\Nonce$
and a non-interactive proof system $(\ProveSymb, \VerifySymb)$ for a reveal relation such that
$\Nonce'$ is equivalent to $\Lambda(\NonceVote,\allowbreak\RevealSymb\textrm{-}\Nonce,\allowbreak(\ProveSymb, \VerifySymb))$.
We prove that $\Nonce'$ satisfies individual and universal verifiability by
Theorems~\ref{thm:iv} \&~\ref{thm:uv}. It follows immediately that $\Nonce$
satisfies individual and universal verifiability too.
\begin{proposition}\label{prop:simpleNonceScheme}
$\Nonce$ satisfies individual and universal verifiability.
\end{proposition}
\begin{proof}
Let $\RevealSymb\textrm{-}\Nonce$ be the following reveal algorithm:
%
\begin{itemize}
\item $\RevealSymb{(\pk, \sk, \nC, \bb, v, \kappa)}$ computes $\mathfrak b \subseteq \bb$
such that for all $(r,p)\in\mathfrak b$ we have $p=v$ and $r\in\mathbb Z_{2^\kappa}$,
and outputs $\mathfrak b$.
\end{itemize}
\noindent
Let $(\ProveSymb, \VerifySymb)$ be the following non-interactive proof system for some reveal relation:
%
\begin{itemize}
\item ...
\item ...
\end{itemize}
\noindent
It follows from Definitions~\ref{def:nonce} \& \ref{def:transform} and
the definition of $\NonceVote$ that $\Nonce'$ and $\Lambda(\NonceVote,\RevealSymb\textrm{-}\Nonce,(\ProveSymb, \VerifySymb))$ are equivalent. Hence, $\Nonce'$ satisfies individual and universal verifiability
by Theorems~\ref{thm:iv} \&~\ref{thm:uv}. It follows immediately that $\Nonce$
satisfies individual and universal verifiability too, concluding our proof.
\end{proof}
\fi
\iffalse
We recall results from to
demonstrate the applicability of our definition.
\begin{definition}\label{def:nonce}
Election scheme $\Nonce$ is defined as follows:
\begin{itemize}
\item $\Setup[\kappa]$ outputs $({\perp},{\perp},\mathit{poly}(\kappa),\infty)$,
where $\mathit{poly}$ is a polynomial function.
\item $\VoteSymb(\pk,\nC,v,\kappa)$ selects a nonce $r$ uniformly at random from $\mathbb Z_{2^\kappa}$
and outputs $(r,v)$.
\item $\TallySymb(\pk,\sk,\nC,\bb,\kappa)$ computes a vector $\outcome$ of length $\nC$, such that
$\outcome$ is a tally of the votes on $\bb$
for which the nonce is in $\mathbb Z_{2^\kappa}$,
and outputs $(\outcome,\perp)$.
\item $\VerSymb(\pk,\nC,\bb,\outcome,\tpf,\kappa)$ outputs $1$ if $(\outcome,\tpf) =\TallySymb({\perp},{\perp},\nC,\bb,\kappa)$ and
$0$ otherwise.
\end{itemize}
\end{definition}
\begin{proposition}\label{prop:simpleNonceScheme}
$\Nonce$ satisfies individual and universal verifiability.
\end{proposition}
\fi
```
# Scope of results
Given an election scheme $\Gamma$, the scope of key results (Proposition [prop:privacyResult] and Theorems [thm:privacyResult] & [thm:uv]) depend on the existence of a reveal algorithm $\mathsf{Reveal}$ that is correct with respect to $\Gamma$ and a non-interactive proof system $\Delta$ for relation $R(\Gamma,\mathsf{Reveal})$, such that $\Delta$ satisfies soundness and zero-knowledge, $\mathsf{Reveal}$ satisfies reveal soundness with respect to $\Gamma$, and $R(\Gamma,\mathsf{Reveal})$ is $\Lambda$-suitable. We show that suitable reveal algorithms exist for all election schemes in Appendix [sec:existence]. And we demonstrate that suitable non-interactive proof systems exist for a large class of election schemes (§1.1).
Furthermore, since our privacy results (Proposition [prop:privacyResult] and Theorem [thm:privacyResult]) depend on a new notion of ballot secrecy, we provide conditions under which the new notion coincides with an existing notion (§1.2).[^3]
Finally, our results apply to election schemes that satisfy definitions of ballot secrecy (Definition [def:ballotSecrecy]) and verifiability (Definitions [def:election-iv] & [def:EEEEUV]), and we consider the suitability of these definitions (§1.3).
## Non-interactive proof systems suitable for our construction
Intuitively, a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$ must prove $\mathsf{Reveal}{( \mathit{sk}, \mathit{nc}, \mathfrak{bb}, v,\kappa)}$ outputs the set of ballots $\mathfrak{b}$ on bulletin board $\mathfrak{bb}$ for vote $v$. Assuming $\Gamma$ is a verifiable election scheme, this can be achieved by exploiting the scheme’s tallying algorithm $\mathsf{Tally}$. In particular, if $\mathfrak{b}$ is a set of ballots for vote $v$, then $\mathsf{Tally}(\mathit{sk},\allowbreak \mathit{nc},\allowbreak \mathfrak b,\allowbreak\kappa)$ will output $({\bf v}_{\mathfrak b}, \mathit{pf}_{\mathfrak b})$ such ${\bf v}_{\mathfrak b}$ is a zero-filled vector except for index $v$ which will contain $|\mathfrak{b}|$ (i.e., outcome ${\bf v}_{\mathfrak b}$ contains $|\mathfrak b|$ votes for candidate $v$ and no votes for the other candidates) and this can be witnessed by proof $\mathit{pf}_{\mathfrak b}$. Moreover, if $\mathfrak{b}$ is the set of ballots on the bulletin board $\mathfrak{bb}$ for vote $v$, then $\mathfrak b\subseteq\mathfrak{bb}$, and $\mathsf{Tally}(\mathit{sk}, \mathit{nc}, \mathfrak{bb},\kappa)$ will output $({\bf v}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak{bb}})$ such that ${\bf v}_{\mathfrak b}[v] = {\bf v}_{\mathfrak bb}[v]$ and this can be witnessed by proof $\mathit{pf}_{\mathfrak{bb}}$. Thus, to prove $\mathsf{Reveal}{( \mathit{sk}, \mathit{nc}, \mathfrak{bb}, v,\kappa)}$ outputs the set of ballots $\mathfrak{b}$ on bulletin board $\mathfrak{bb}$ for vote $v$, it suffices to output proofs $\mathit{pf}_{\mathfrak b}$ and $\mathit{pf}_{\mathfrak bb}$. We formalise such a proof system.
**Definition 1**. *Given an election scheme $\Gamma = (\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify}_{\Gamma})$, we define $\delta(\Gamma) = (\mathsf{Prove}, \mathsf{Verify})$ as follows.*
*$\mathsf{Prove}(s,\mathit{sk},\kappa)$ parses $s$ as vector $(\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{}v,\allowbreak\mathfrak b,\allowbreak\kappa)$, outputting $\perp$ if parsing fails; computes $({\bf v}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak{bb}}) \leftarrow \mathsf{Tally}(\mathit{sk}, \mathit{nc}, \mathfrak{bb},\kappa);
({\bf v}_{\mathfrak b}, \mathit{pf}_{\mathfrak b}) \leftarrow \mathsf{Tally}(\mathit{sk},\allowbreak \mathit{nc},\allowbreak \mathfrak b,\allowbreak\kappa)$; and outputs $(\mathit{pf}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak b})$.*
*$\mathsf{Verify}(s,\sigma,\kappa)$ proceeds as follows. Parse $s$ as vector $(\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{}v,\allowbreak\mathfrak b,\allowbreak\kappa)$ and $\sigma$ as $(\mathit{pf}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak b})$, outputting $0$ if parsing fails. Let ${\bf v}_{\mathfrak b}$ be a vector of length $\mathit{nc}$ which is zero-filled, except for index $v$ which contains $|\mathfrak b|$, and let ${\bf v}_{\mathfrak{bb}}$ be the election outcome. If such a vector exists and $\mathsf{Verify}_{\Gamma}(\mathit{pk},\allowbreak\mathit{nc},\allowbreak \mathfrak{bb},\allowbreak {\bf v}_{\mathfrak{bb}},\allowbreak \mathit{pf}_{\mathfrak{bb}},\allowbreak \kappa) =\allowbreak 1 \wedge\allowbreak
\mathsf{Verify}_{\Gamma}(\mathit{pk},\allowbreak\mathit{nc},\allowbreak \mathfrak b,\allowbreak {\bf v}_{\mathfrak b},\allowbreak \mathit{pf}_{\mathfrak b},\allowbreak \kappa) =\allowbreak 1 \wedge\allowbreak
{\bf v}_{\mathfrak{bb}}[v] = {\bf v}_{\mathfrak b}[v] \wedge\allowbreak
\mathfrak b\subseteq \mathfrak{bb}$, then output $1$, otherwise, output $0$.*
**Lemma 1**. *Let $\Gamma$ be an election scheme and $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. If $\Gamma$ satisfies $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ and $\mathsf{Reveal}$ satisfies reveal soundness with respect to $\Gamma$, then $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$.*
For election schemes ensuring honest key generation (Definition 2), our construction $\delta$ produces non-interactive proof systems that are sound (Lemma 2).
**Definition 2** (Honest key generation). *An election scheme $(\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify})$ ensures *honest key generation*, if for all probabilistic polynomial-time adversaries $\mathcal A$, there exists a negligible function $\mathsf{negl}$, such that for all security parameters $\kappa$, we have $$\begin{gathered}
\Pr[(\mathit{pk},\mathit{nc},\mathfrak{bb},{\bf v},\mathit{pf}) \leftarrow \mathcal A(\kappa):
\mathsf{Verify}(\mathit{pk},\mathit{nc}, \mathfrak{bb}, {\bf v}, \mathit{pf}, \kappa) = 1
\Rightarrow \exists \mathit{sk},\mathit{mb},\mathit{mc},r \\\mathrel . (\mathit{pk},\allowbreak\mathit{sk},\allowbreak\mathit{mb},\allowbreak\mathit{mc}) =\allowbreak \mathsf{Setup}(\kappa;r) \wedge |\mathfrak{bb}|\leq\mathit{mb}\wedge\mathit{nc}\leq\mathit{mc}] > 1 - \mathsf{negl}(\kappa).
\end{gathered}$$*
Honest key generation assures that a public key is produced by an election scheme’s $\mathsf{Setup}$ algorithm, parameterised by some security parameter and coins. There is no assurance that those coins were chosen uniformly at random. Correctness and completeness, however, assume coins are chosen uniformly at random, while perfect correctness and perfect completeness do not. Consequently, tallying produces the expected election outcome and verification succeeds for that outcome, when perfect correctness and perfect completeness are satisfied.
**Lemma 2**. *Let $\Gamma$ be an election scheme with perfect correctness and perfect completeness, and let $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. Suppose $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$. If $\Gamma$ satisfies $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ and ensures honest key generation, and $\mathsf{Reveal}$ satisfies reveal soundness with respect to $\Gamma$, then $\delta(\Gamma)$ is sound.*
For election schemes that construct tallying proofs using a zero-knowledge non-interactive proof systems (Definition 3), our construction $\delta$ produces proof systems satisfying zero-knowledge (Lemma 3).
**Definition 3** (Tallying proof system). *Let $\Gamma = (\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify}_{\Gamma})$ be an election scheme and $\Delta = (\mathsf{Prove}, \mathsf{Verify})$ be a non-interactive proof system. We say *$\Delta$ is a tallying proof system for $\Gamma$*, if for all security parameters $\kappa$, integers $\mathit{nc}$, bulletin boards $\mathfrak{bb}$, outputs $(\mathit{pk},\mathit{sk},\mathit{mb}, \mathit{mc})$ of $\mathsf{Setup}(\kappa)$, and outputs $({\bf v},\mathit{pf})$ of $\mathsf{Tally}(\mathit{sk},\mathit{nc},\mathfrak{bb},\mathit{nc}, \kappa)$, we have $\mathit{pf}=\mathsf{Prove}((\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{\bf v}),\allowbreak\mathit{sk},\allowbreak\kappa;r)$, where coins $r$ are chosen uniformly at random by $\mathsf{Tally}$.*
**Lemma 3**. *Let $\Gamma$ be an election scheme and $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. Suppose $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$. If there exists a tallying proof system for $\Gamma$ that satisfies zero-knowledge, then $\delta(\Gamma)$ satisfies zero-knowledge.*
## Notions of ballot secrecy
Proposition [prop:ballot-secrecy-relatedd] shows that $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ is strictly stronger than the definition by Smyth ($\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$) (**Smyth15-ballot-independence?**). Intuitively, this is because it is not possible to simulate tallying in the general case (cf. Section [sec:ballot-secrecy]). Nevertheless, if an election scheme proves correct key generation using a non-interactive proof system satisfying simulation sound extractability, then the witness used to construct the proof can be extracted. This typically enables the private key to be extracted too. Hence, it is possible to simulate tallying, which suffices to ensure $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ and $\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$ coincide. We prove this result (Proposition 4), using a suitably formulated precondition (Definition 4) that we straightforwardly derive from simulation sound extractability.
**Definition 4**. *Let $\Gamma = (\mathsf{Setup},\mathsf{Vote},\mathsf{Tally}, \mathsf{Verify})$ be an election scheme and $\mathcal H$ be a random oracle. We say $\Gamma$ satisfies *simulation sound private key extractibility*, if there exists a probabilistic polynomial-time algorithm $\mathcal K$, such that for all coins $r$, there exists a negligible function $\mathsf{negl}$ and for all security parameters $\kappa$, we have $\Pr[
(\mathit{pk},\mathit{sk},\mathit{mb},\mathit{mc}) \leftarrow\mathsf{Setup}^{\mathcal H}(\kappa;r);
\mathit{sk}' \leftarrow \mathcal K^{\mathsf{Setup}'}({\bf H},\mathit{pk})
%
: \mathit{sk}= \mathit{sk}'] > 1-\mathsf{negl}(\kappa)$, where ${\bf H}$ is a transcript of the random oracle’s input and output, and oracle $\mathsf{Setup}'$ computes $(\mathit{pk}',\mathit{sk}',\mathit{mb}',\mathit{mc}')\leftarrow\mathsf{Setup}(\kappa;r)$, forwarding any oracle queries by $\mathsf{Setup}$ to $\mathcal K$, and outputs $(\mathit{pk}',\mathit{sk}',\mathit{mb}',\mathit{mc}')$.*
**Proposition 4**. *Given an election scheme $\Gamma$ satisfying simulation sound private key extractibility, we have $\Gamma$ satisfies $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ iff $\Gamma$ satisfies $\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$.*
## Suitability of security definitions
### Ballot secrecy
Discussion of ballot secrecy originates from Chaum (**Chaum:1981?**) and the earliest definitions of ballot secrecy are due to Benaloh *et al.* (**Benaloh86?**; **BT94:ReceiptFreeVoting?**; **Benaloh96:Thesis?**). More recently, Bernhard, Pereira & Warinschi (**Bernhard12:Helios?**) and Cortier *et al.* (**Cortier13?**; **Cortier13b?**) propose definitions of ballot secrecy.
Bernhard *et al.* (**BCGPW15?**) show that those definitions are too weak and propose a strengthening of the definition by Bernhard, Pereira & Warinschi. Smyth (**Smyth15-ballot-independence?**) shows that the definition by Bernhard *et al.*, and other definitions, do not detect attacks that arise when the adversary controls the bulletin board or the communication channel, and proposes a definition that does. [^4]
We build upon Smyth’s definition of ballot secrecy because it appears to detect the largest class of attacks.
The aforementioned definitions of ballot secrecy all assume
the tallier is trusted.[^5] Hence, an election scheme that leaks the ballot-vote relation during tallying can satisfy those definitions, because the tallier is assumed not to disclose mappings.
Indeed, election scheme $\mathsf{Enc2Vote}$ satisfies ballot secrecy (Proposition [prop:mv]), despite leaking such a map to the tallier.
It is desirable to distribute the tallier’s role amongst several talliers and define a definition of ballot secrecy that detects such mappings, assuming at least one tallier is honest. However, formulating such a definition would advance the state-of-the-art in a manner that is beyond the scope of this paper, and extending our results in this direction is left as a possibility for future work.
### Election verifiability
Discussion of universal verifiability seems to originate from Cohen & Fischer (**Benaloh85?**) and advanced by Benaloh & Tuinstra (**Benaloh94?**) and Sako & Kilian (**Sako95?**). More recently, Juels, Catalano & Jakobsson (**JCJ02?**; **JCJ10?**), Cortier *et al.* (**Cortier14:verifiability?**) and Kiayias, Zacharias & Zhang (**Kiayias15?**) present definitions of election verifiability. Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) show that definitions by Juels, Catalano & Jakobsson and Cortier *et al.* do not detect attacks that arise when tallying and verification procedures collude nor when verification procedures reject legitimate outcomes. Moreover, they show that the definition by Kiayias, Zacharias & Zhang does not detect the latter class of attacks. Smyth, Frink & Clarkson propose a definition of election verifiability (§[sec:verifiability]) that detects these attacks.[^6] We adopt their definition because it appears to detect the largest class of attacks. Moreover, their definition has proven to be useful in correctly identifying three schemes that do not satisfy verifiability, and in identifying two schemes that do. Furthermore, Helios satisfies their definitions, which will be useful in our case study (§[sec:helios]).
Küsters *et al.* (**Kusters10?**; **Kusters11:UniversalVerifiability?**; **Kusters12:ClashAttacks?**) propose an alternative, holistic notion of verifiability called *global verifiability*, which must be instantiated with a goal. Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) show that goals proposed by Küsters *et al.* (**Kusters10b?**) and by Cortier et al. (**Cortier16:VerifiabilitySoK?**)
are too strong. Moreover, Smyth, Frink & Clarkson propose a weakening of the goal by Küsters *et al.* and show that their definition of election verifiability (§[sec:verifiability]) is strictly stronger than global verifiability with that goal, which further motivates the adoption of their definition of election verifiability. Nonetheless, the “gap" exists due to an uninteresting technical detail, hence, similar verifiability results might-well be derivable from global verifiability. Moreover, global verifiability would suffice if the gap is filled.
# Case study: Helios
We demonstrate the applicability of our construction by deriving auction schemes from Helios (**Adida08?**; **AdidaPereiraMarneffeQuisquater?**; **Pereira11:HeliosMixnet?**; **Olivier16:Helios?**), 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?**),[^7] 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. [^8],[^9] Helios defines two modes of tallying: tallying by homomorphically combining ciphertexts (**AdidaPereiraMarneffeQuisquater?**) and tallying by mixnet (**Adida08?**; **Pereira11:HeliosMixnet?**). In the former mode, Helios has been proved to satisfy ballot secrecy and verifiability, hence our results are immediately applicable. In the latter mode, no such results exist, thus our results are only applicable if ballot secrecy and verifiability are satisfied. This mode is nonetheless interesting, because the auction scheme we derive is more efficient.
## Tallying by homomorphic combinations
Informally, Helios with tallying by homomorphically combining ciphertexts(**AdidaPereiraMarneffeQuisquater?**) can be modelled as the following election scheme:
$\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 in zero-knowledge that the ciphertext is correctly constructed and that the vote is selected from the sequence of candidates, 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,[^10] and defences against those attacks have been proposed (**Smyth11:Helios?**; **Smyth11:ReplayAttacks?**; **Smyth12:HeliosFurtherReplays?**; **Smyth12:Helios?**; **2013:BallotIndependenceESORICS?**; **2014:BallotIndependenceEprint?**; **Smyth15-ballot-independence?**; **Bernhard12:Helios?**; **Essex16:HeliosVerifiability?**). We adopt the formal definition of Helios proposed by Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**), which adopts non-malleable ballots (**Smyth15:NM-CPA-ciphertexts?**) and uses the Fiat–Shamir transformation with the inclusion of statements in hashes (**Bernhard12:Helios?**) to defend against those attacks. We recall that formalisation in Appendix [app:helios-construction] and henceforth refer to it as .
We derive an auction scheme from using our construction parameterised with a reveal algorithm $\mathsf{Helios}\textrm{-}\mathsf{Reveal}$ and non-interactive proof system $\delta(\textrm{\HeliosSFC})$. [^11] Reveal algorithm $\mathsf{Helios}\textrm{-}\mathsf{Reveal}$ exploits some technical details of that we have not yet discussed, so we defer the formal description to Appendix [app:hawk]. Our privacy and verifiability results allow us to prove security of the derived auction scheme.
**Theorem 1**.
*Auction scheme*
*$\Lambda(\allowbreak\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal},\allowbreak\delta(\textrm{\HeliosSFC}))$ satisfies $\mathsf{Bid}\textrm{-}\mathsf{Secrecy}$.*
We have $\delta(\textrm{\HeliosSFC})$ is a non-interactive proof system for relation $R(\allowbreak\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal})$ (Lemma [lem:deltaProofSystem]) satisfying zero-knowledge (Lemma [lem:scope:zk]), assuming there exists a tallying proof system for that satisfies zero-knowledge. Moreover, since Smyth has shown that satisfies $\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$ (**Smyth15-ballot-independence?**), we have satisfies $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ (Proposition [prop:ballot-secrecy-notions-coincide-NEW]), assuming satisfies simulation sound private key extractibility. Furthermore, since Smyth, Frink & Clarkson have shown that satisfies $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ (**Smyth15:ElectionVerifiability?**), we have satisfies $\mathsf{W}\textrm{-}\mathsf{Tally}\textrm{-}\allowbreak\mathsf{Soundness}$ (Lemma [lem:uv:soundness]). Hence, by Theorem [thm:privacyResult], it suffices to prove that reveal algorithm $\mathsf{Helios}\textrm{-}\mathsf{Reveal}$ satisfies reveal soundness with respect to and to prove our earlier assumptions. We defer those proofs to Lemmata [lem:hawk:zkProofs], [lem:hawk:keyExt] & [lem:hawk:reveal:soundness] in Appendix [app:hawk].
**Theorem 2**. *Auction scheme $\Lambda(\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal},\allowbreak\delta(\textrm{\HeliosSFC}))$ satisfies $\mathsf{Exp}\text{-}\mathsf{IV}$ and $\mathsf{Exp}\text{-}\mathsf{UV}$.*
Smyth, Frink & Clarkson have shown that satisfies $\mathsf{Exp}\text{-}\mathsf{IV}\text{-}\mathsf{Ext}$ and $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ (**Smyth15:ElectionVerifiability?**). Hence, we have $\Lambda(\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal},\allowbreak\delta(\textrm{\HeliosSFC}))$ satisfies $\mathsf{Exp}\text{-}\mathsf{IV}$ (Theorem [thm:iv]). We have $\delta(\textrm{\HeliosSFC})$ is a non-interactive proof system for relation $R(\textrm{\HeliosSFC},\mathsf{Reveal})$ (Lemma [lem:deltaProofSystem]) satisfying soundness (Lemma [lem:scope:sound]), assuming ensures honest key generation. Hence, to show $\mathsf{Exp}\text{-}\mathsf{UV}$ is satisfied, it suffices (Theorem [thm:uv]) to prove that $\textrm{\HeliosSFC}$ satisfies perfect correctness and perfect completeness, $R(\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal})$ is $\Lambda$-suitable, and our previous assumption. We defer those proofs to Lemmata [lem:helios:correct] & [lem:helios:complete] in Appendix [app:helios-construction] and Lemmata [lem:hawk:reveal:verifiable] & [lem:hawk:honKeys] in Appendix [app:hawk].
Our construction $\delta$ for non-interactive proof systems (§[sec:scope]) demonstrates the scope of our results. But, more efficient proof systems might exist. Indeed, we tailor a proof system for in Appendix [app:hawk:alt], which is more efficient than $\delta(\textrm{\HeliosSFC})$.
Deriving auction schemes from Helios with tallying by homomorphically combining ciphertexts is not new. Indeed, McCarthy, Smyth & Quaglia (**2014-Hawk-and-Aucitas-auction-schemes?**) derive the *Hawk* auction scheme. However, they only provide an informal security analysis for Hawk. By contrast, we derive an auction scheme for which we provide formal security results.
## Tallying by mixnet
Informally, Helios with tallying by mixnet (**Adida08?**; **Pereira11:HeliosMixnet?**) can be modelled as the following election scheme:
$\mathsf{Setup}$ as per above.
$\mathsf{Vote}$ encrypts the vote, proves correct ciphertext construction, 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 mixed. Thirdly, the ciphertexts output by the mix are 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}$ checks the proofs and outputs $1$ if these checks succeed and $0$ otherwise.
Unlike Helios with tallying by homomorphically combining ciphertexts, there is no description of Helios with tallying by mixnet in the cryptographic model (indeed, (**Adida08?**) introduces the idea, and (**Pereira11:HeliosMixnet?**) describes the general work-flow of mixnet-based elections). Thus, we must formalise a suitable description.
We formalise Helios with tallying by mixnet as the class of election schemes (see Appendix [app:heliosM-construction]). Given an election scheme $\Gamma$ from , we derive auction scheme $\Lambda(\allowbreak\Gamma,\allowbreak\mathsf{HeliosM}\textrm{-}\allowbreak\mathsf{Reveal},\allowbreak\delta(\Gamma))$ using a reveal algorithm that works as follows:
$\mathsf{HeliosM}\textrm{-}\allowbreak\mathsf{Reveal}$ constructs a ciphertext for the winning bid, performs plaintext equality tests between that ciphertext and the ciphertexts input to the mix, and outputs any ballots for which the test succeeds.[^12]
We defer a formal definition to Appendix [app:hawk-mixnet:reveal].
Our privacy and verifiability results allow us to prove security.
**Theorem 3**. *Given an election scheme $\Gamma\in \textrm{\HeliosM}$, auction scheme $\Lambda(\allowbreak\Gamma,\allowbreak\mathsf{HeliosM}\textrm{-}\allowbreak\mathsf{Reveal},\allowbreak\delta(\Gamma))$ satisfies $\mathsf{Bid}\textrm{-}\mathsf{Secrecy}$, $\mathsf{Exp}\text{-}\mathsf{IV}$, and $\mathsf{Exp}\text{-}\mathsf{UV}$.*
The proof of Theorem 3 is similar in structure to the proofs of Theorems 1 & 2, and we defer the details to Appendix [app-helios-mixnet].
# Conclusion
We present a generic construction for auction schemes from election schemes, and we formulate precise conditions under which auction schemes produced by our construction are secure. Thereby demonstrating that the seemingly disjoint research fields of auctions and elections are related. Our results advance the unification of auctions and elections; facilitating the progression of both fields. In particular, secure auction schemes can now be constructed from election schemes, allowing advances in election schemes to be capitalised upon to advance auction schemes.
# Acknowledgements
This research was conducted in part at École Normale Supérieure and INRIA, with support from the European Research Council under the European Union’s Seventh Framework Programme (FP7/2007-2013) / ERC project *CRYSP* (259639).
# Scope of results
## Non-interactive proof systems suitable for our construction
Intuitively, a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$ must prove $\mathsf{Reveal}{( \mathit{sk}, \mathit{nc}, \mathfrak{bb}, v,\kappa)}$ outputs the set of ballots $\mathfrak{b}$ on bulletin board $\mathfrak{bb}$ for vote $v$. Assuming $\Gamma$ is a verifiable election scheme, this can be achieved by exploiting the scheme’s tallying algorithm $\mathsf{Tally}$. In particular, if $\mathfrak{b}$ is a set of ballots for vote $v$, then $\mathsf{Tally}(\mathit{sk},\allowbreak \mathit{nc},\allowbreak \mathfrak b,\allowbreak\kappa)$ will output $({\bf v}_{\mathfrak b}, \mathit{pf}_{\mathfrak b})$ such ${\bf v}_{\mathfrak b}$ is a zero-filled vector except for index $v$ which will contain $|\mathfrak{b}|$ (i.e., outcome ${\bf v}_{\mathfrak b}$ contains $|\mathfrak b|$ votes for candidate $v$ and no votes for the other candidates) and this can be witnessed by proof $\mathit{pf}_{\mathfrak b}$. Moreover, if $\mathfrak{b}$ is the set of ballots on the bulletin board $\mathfrak{bb}$ for vote $v$, then $\mathfrak b\subseteq\mathfrak{bb}$, and $\mathsf{Tally}(\mathit{sk}, \mathit{nc}, \mathfrak{bb},\kappa)$ will output $({\bf v}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak{bb}})$ such that ${\bf v}_{\mathfrak b}[v] = {\bf v}_{\mathfrak bb}[v]$ and this can be witnessed by proof $\mathit{pf}_{\mathfrak{bb}}$. Thus, to prove $\mathsf{Reveal}{( \mathit{sk}, \mathit{nc}, \mathfrak{bb}, v,\kappa)}$ outputs the set of ballots $\mathfrak{b}$ on bulletin board $\mathfrak{bb}$ for vote $v$, it suffices to output proofs $\mathit{pf}_{\mathfrak b}$ and $\mathit{pf}_{\mathfrak bb}$. We formalise such a proof system.
**Definition 1**. *Given an election scheme $\Gamma = (\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify}_{\Gamma})$, we define $\delta(\Gamma) = (\mathsf{Prove}, \mathsf{Verify})$ as follows.*
*$\mathsf{Prove}(s,\mathit{sk},\kappa)$ parses $s$ as vector $(\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{}v,\allowbreak\mathfrak b,\allowbreak\kappa)$, outputting $\perp$ if parsing fails; computes $({\bf v}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak{bb}}) \leftarrow \mathsf{Tally}(\mathit{sk}, \mathit{nc}, \mathfrak{bb},\kappa);
({\bf v}_{\mathfrak b}, \mathit{pf}_{\mathfrak b}) \leftarrow \mathsf{Tally}(\mathit{sk},\allowbreak \mathit{nc},\allowbreak \mathfrak b,\allowbreak\kappa)$; and outputs $(\mathit{pf}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak b})$.*
*$\mathsf{Verify}(s,\sigma,\kappa)$ proceeds as follows. Parse $s$ as vector $(\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{}v,\allowbreak\mathfrak b,\allowbreak\kappa)$ and $\sigma$ as $(\mathit{pf}_{\mathfrak{bb}}, \mathit{pf}_{\mathfrak b})$, outputting $0$ if parsing fails. Let ${\bf v}_{\mathfrak b}$ be a vector of length $\mathit{nc}$ which is zero-filled, except for index $v$ which contains $|\mathfrak b|$, and let ${\bf v}_{\mathfrak{bb}}$ be the election outcome. If such a vector exists and $\mathsf{Verify}_{\Gamma}(\mathit{pk},\allowbreak\mathit{nc},\allowbreak \mathfrak{bb},\allowbreak {\bf v}_{\mathfrak{bb}},\allowbreak \mathit{pf}_{\mathfrak{bb}},\allowbreak \kappa) =\allowbreak 1 \wedge\allowbreak
\mathsf{Verify}_{\Gamma}(\mathit{pk},\allowbreak\mathit{nc},\allowbreak \mathfrak b,\allowbreak {\bf v}_{\mathfrak b},\allowbreak \mathit{pf}_{\mathfrak b},\allowbreak \kappa) =\allowbreak 1 \wedge\allowbreak
{\bf v}_{\mathfrak{bb}}[v] = {\bf v}_{\mathfrak b}[v] \wedge\allowbreak
\mathfrak b\subseteq \mathfrak{bb}$, then output $1$, otherwise, output $0$.*
**Lemma 1**. *Let $\Gamma$ be an election scheme and $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. If $\Gamma$ satisfies $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ and $\mathsf{Reveal}$ satisfies reveal soundness with respect to $\Gamma$, then $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$.*
For election schemes ensuring honest key generation (Definition 2), our construction $\delta$ produces non-interactive proof systems that are sound (Lemma 2).
**Definition 2** (Honest key generation). *An election scheme $(\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify})$ ensures *honest key generation*, if for all probabilistic polynomial-time adversaries $\mathcal A$, there exists a negligible function $\mathsf{negl}$, such that for all security parameters $\kappa$, we have $$\begin{gathered}
\Pr[(\mathit{pk},\mathit{nc},\mathfrak{bb},{\bf v},\mathit{pf}) \leftarrow \mathcal A(\kappa):
\mathsf{Verify}(\mathit{pk},\mathit{nc}, \mathfrak{bb}, {\bf v}, \mathit{pf}, \kappa) = 1
\Rightarrow \exists \mathit{sk},\mathit{mb},\mathit{mc},r \\\mathrel . (\mathit{pk},\allowbreak\mathit{sk},\allowbreak\mathit{mb},\allowbreak\mathit{mc}) =\allowbreak \mathsf{Setup}(\kappa;r) \wedge |\mathfrak{bb}|\leq\mathit{mb}\wedge\mathit{nc}\leq\mathit{mc}] > 1 - \mathsf{negl}(\kappa).
\end{gathered}$$*
Honest key generation assures that a public key is produced by an election scheme’s $\mathsf{Setup}$ algorithm, parameterised by some security parameter and coins. There is no assurance that those coins were chosen uniformly at random. Correctness and completeness, however, assume coins are chosen uniformly at random, while perfect correctness and perfect completeness do not. Consequently, tallying produces the expected election outcome and verification succeeds for that outcome, when perfect correctness and perfect completeness are satisfied.
**Lemma 2**. *Let $\Gamma$ be an election scheme with perfect correctness and perfect completeness, and let $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. Suppose $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$. If $\Gamma$ satisfies $\mathsf{Exp}\text{-}\mathsf{UV}\text{-}\mathsf{Ext}$ and ensures honest key generation, and $\mathsf{Reveal}$ satisfies reveal soundness with respect to $\Gamma$, then $\delta(\Gamma)$ is sound.*
For election schemes that construct tallying proofs using a zero-knowledge non-interactive proof systems (Definition 3), our construction $\delta$ produces proof systems satisfying zero-knowledge (Lemma 3).
**Definition 3** (Tallying proof system). *Let $\Gamma = (\mathsf{Setup},\allowbreak\mathsf{Vote},\allowbreak\mathsf{Tally},\allowbreak \mathsf{Verify}_{\Gamma})$ be an election scheme and $\Delta = (\mathsf{Prove}, \mathsf{Verify})$ be a non-interactive proof system. We say *$\Delta$ is a tallying proof system for $\Gamma$*, if for all security parameters $\kappa$, integers $\mathit{nc}$, bulletin boards $\mathfrak{bb}$, outputs $(\mathit{pk},\mathit{sk},\mathit{mb}, \mathit{mc})$ of $\mathsf{Setup}(\kappa)$, and outputs $({\bf v},\mathit{pf})$ of $\mathsf{Tally}(\mathit{sk},\mathit{nc},\mathfrak{bb},\mathit{nc}, \kappa)$, we have $\mathit{pf}=\mathsf{Prove}((\mathit{pk},\allowbreak\mathit{nc},\allowbreak\mathfrak{bb},\allowbreak{\bf v}),\allowbreak\mathit{sk},\allowbreak\kappa;r)$, where coins $r$ are chosen uniformly at random by $\mathsf{Tally}$.*
**Lemma 3**. *Let $\Gamma$ be an election scheme and $\mathsf{Reveal}$ be a reveal algorithm that is correct with respect to $\Gamma$. Suppose $\delta(\Gamma)$ is a non-interactive proof system for relation $R(\Gamma,\mathsf{Reveal})$. If there exists a tallying proof system for $\Gamma$ that satisfies zero-knowledge, then $\delta(\Gamma)$ satisfies zero-knowledge.*
## Notions of ballot secrecy
Proposition [prop:ballot-secrecy-relatedd] shows that $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ is strictly stronger than the definition by Smyth ($\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$) (**Smyth15-ballot-independence?**). Intuitively, this is because it is not possible to simulate tallying in the general case (cf. Section [sec:ballot-secrecy]). Nevertheless, if an election scheme proves correct key generation using a non-interactive proof system satisfying simulation sound extractability, then the witness used to construct the proof can be extracted. This typically enables the private key to be extracted too. Hence, it is possible to simulate tallying, which suffices to ensure $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ and $\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$ coincide. We prove this result (Proposition 4), using a suitably formulated precondition (Definition 4) that we straightforwardly derive from simulation sound extractability.
**Definition 4**. *Let $\Gamma = (\mathsf{Setup},\mathsf{Vote},\mathsf{Tally}, \mathsf{Verify})$ be an election scheme and $\mathcal H$ be a random oracle. We say $\Gamma$ satisfies *simulation sound private key extractibility*, if there exists a probabilistic polynomial-time algorithm $\mathcal K$, such that for all coins $r$, there exists a negligible function $\mathsf{negl}$ and for all security parameters $\kappa$, we have $\Pr[
(\mathit{pk},\mathit{sk},\mathit{mb},\mathit{mc}) \leftarrow\mathsf{Setup}^{\mathcal H}(\kappa;r);
\mathit{sk}' \leftarrow \mathcal K^{\mathsf{Setup}'}({\bf H},\mathit{pk})
%
: \mathit{sk}= \mathit{sk}'] > 1-\mathsf{negl}(\kappa)$, where ${\bf H}$ is a transcript of the random oracle’s input and output, and oracle $\mathsf{Setup}'$ computes $(\mathit{pk}',\mathit{sk}',\mathit{mb}',\mathit{mc}')\leftarrow\mathsf{Setup}(\kappa;r)$, forwarding any oracle queries by $\mathsf{Setup}$ to $\mathcal K$, and outputs $(\mathit{pk}',\mathit{sk}',\mathit{mb}',\mathit{mc}')$.*
**Proposition 4**. *Given an election scheme $\Gamma$ satisfying simulation sound private key extractibility, we have $\Gamma$ satisfies $\mathsf{Ballot}\textrm{-}\mathsf{Secrecy}$ iff $\Gamma$ satisfies $\mathsf{Smy}\textrm{-}\allowbreak\mathsf{Ballot}\textrm{-}\allowbreak\mathsf{Secrecy}$.*
## Suitability of security definitions
### Ballot secrecy
Discussion of ballot secrecy originates from Chaum (**Chaum:1981?**) and the earliest definitions of ballot secrecy are due to Benaloh *et al.* (**Benaloh86?**; **BT94:ReceiptFreeVoting?**; **Benaloh96:Thesis?**). More recently, Bernhard, Pereira & Warinschi (**Bernhard12:Helios?**) and Cortier *et al.* (**Cortier13?**; **Cortier13b?**) propose definitions of ballot secrecy.
Bernhard *et al.* (**BCGPW15?**) show that those definitions are too weak and propose a strengthening of the definition by Bernhard, Pereira & Warinschi. Smyth (**Smyth15-ballot-independence?**) shows that the definition by Bernhard *et al.*, and other definitions, do not detect attacks that arise when the adversary controls the bulletin board or the communication channel, and proposes a definition that does. [^13]
We build upon Smyth’s definition of ballot secrecy because it appears to detect the largest class of attacks.
### Election verifiability
Discussion of universal verifiability seems to originate from Cohen & Fischer (**Benaloh85?**) and advanced by Benaloh & Tuinstra (**Benaloh94?**) and Sako & Kilian (**Sako95?**). More recently, Juels, Catalano & Jakobsson (**JCJ02?**; **JCJ10?**), Cortier *et al.* (**Cortier14:verifiability?**) and Kiayias, Zacharias & Zhang (**Kiayias15?**) present definitions of election verifiability. Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) show that definitions by Juels, Catalano & Jakobsson and Cortier *et al.* do not detect attacks that arise when tallying and verification procedures collude nor when verification procedures reject legitimate outcomes. Moreover, they show that the definition by Kiayias, Zacharias & Zhang does not detect the latter class of attacks. Smyth, Frink & Clarkson propose a definition of election verifiability (§[sec:verifiability]) that detects these attacks.[^14] We adopt their definition because it appears to detect the largest class of attacks. Moreover, their definition has proven to be useful in correctly identifying three schemes that do not satisfy verifiability, and in identifying two schemes that do. Furthermore, Helios satisfies their definitions, which will be useful in our case study (§[sec:helios]).
Küsters *et al.* (**Kusters10?**; **Kusters11:UniversalVerifiability?**; **Kusters12:ClashAttacks?**) propose an alternative, holistic notion of verifiability called *global verifiability*, which must be instantiated with a goal. Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**) show that goals proposed by Küsters *et al.* (**Kusters10b?**) and by Cortier et al. (**Cortier16:VerifiabilitySoK?**)
are too strong. Moreover, Smyth, Frink & Clarkson propose a weakening of the goal by Küsters *et al.* and show that their definition of election verifiability (§[sec:verifiability]) is strictly stronger than global verifiability with that goal, which further motivates the adoption of their definition of election verifiability. Nonetheless, the “gap" exists due to an uninteresting technical detail, hence, similar verifiability results might-well be derivable from global verifiability. Moreover, global verifiability would suffice if the gap is filled.
[^1]: Ballot secrecy does not prohibit such behaviour, because ballot secrecy assumes the tallier is trusted.
[^2]: Handling tie-breaks (i.e., selecting a winning bid from a set of winning bids) is straightforward. For instance, the set could be sampled uniformly at random. So this paper does not address this problem.
[^3]: Helios satisfies the existing notion, which will be useful in our case study (§[sec:helios]).
[^4]: Smyth’s definition is based upon a technical report by Smyth (**2014-ballot-secrecy-a?**) and an extended version of that technical report by Bernhard & Smyth (**2014-ballot-secrecy?**).
[^5]: Perfect ballot secrecy formalises a privacy notion without trusting the tallier, but it is only known to be satisfied by decentralised voting systems, e.g., (**Schoenmakers99:PVSS?**; **KY02?**; **G04?**; **HRZ09?**; **Smyth12:decentralised-voting-system?**), which are unsuitable for large-scale elections.
[^6]: Cortier *et al.* (**Cortier16:VerifiabilitySoK?** & §10.1) claim that the definition by Smyth, Frink & Clarkson is flawed, but that claim is false (**Smyth15:ElectionVerifiability?**).
[^7]: , accessed 13 Jul 2017.
[^8]: , accessed 13 Jul 2017.
[^9]: , accessed 13 Jul 2017.
[^10]: Beyond secrecy and verifiability, attacks against eligibility are also known (**2013-truncation-attacks-to-violate-beliefs?**; **2014-truncation-attacks-to-violate-beliefs?**; **Smyth16:helios-eligibility?**).
[^11]: Formally, $\Lambda(\textrm{\HeliosSFC},\allowbreak\mathsf{Helios}\textrm{-}\mathsf{Reveal},\allowbreak\delta(\textrm{\HeliosSFC}))$ is an auction scheme by Lemmata [lemma:trans:2:correctness], [lem:deltaProofSystem], & [lem:hawk:reveal].
[^12]: A plaintext equality test (**jakobsson2000mix?**) is a cryptographic primitive which allows a key holder to check whether two ciphertexts contain the same plaintext, without decrypting.
[^13]: Smyth’s definition is based upon a technical report by Smyth (**2014-ballot-secrecy-a?**) and an extended version of that technical report by Bernhard & Smyth (**2014-ballot-secrecy?**).
[^14]: Cortier *et al.* (**Cortier16:VerifiabilitySoK?** & §10.1) claim that the definition by Smyth, Frink & Clarkson is flawed, but that claim is false (**Smyth15:ElectionVerifiability?**).