# Cast-as-intended: A formal definition and case studies
Peter B. Rønne, Peter Y. A. Ryan, Ben Smyth
## Abstract
Verifiable voting systems allow voters to check whether their ballot is correctly recorded (individual verifiability) and allow anyone to check whether votes expressed in recorded ballots are correctly counted (universal verifiability). This suffices to ensure that honest voters’ votes are correctly counted, assuming ballots are properly generated.
Achieving ballot assurance, i.e., assuring each voter that their vote is correctly encoded inside their ballot, whilst ensuring privacy, is a challenging aspect of voting system design. This assurance property is known as cast-as-intended. Unlike many properties of voting systems, it has yet to be formalised. We provide the first formal definition and apply our definition to MarkPledge, Prêt à Voter, Selene, ThreeBallot, and schemes based upon Benaloh challenges.
# Introduction
End-to-end Verifiable (E2E V) voting systems produce evidence of correct operation: Cast ballots (which contain the vote in encrypted or encoded form) are published on a public bulletin board (ledger), so voters can check whether their ballot is collected (individual verifiability), and tallies are coupled with proofs, so anyone can check whether votes expressed in collected ballots are correctly counted (universal verifiability). By additionally providing means to check whether votes are correctly encoded in ballots, we achieve end-to-end verifiability. This is not yet enough to guarantee that the outcome is correct, for this we need extra measures such as eligibility verifiablity to prevent ballot stuffing and clash attacks [^1] etc., but this is beyond the scope of this paper.
For many end-to-end verifiability systems (but not all, e.g., (**randell2006voting?**; **rivest2006threeballot?**)), ballots are constructed using cryptographic operations, which are typically beyond the mathematical capabilities of even the most studious scholar. Moreover, assurance of correct encoding has to be provided without undermining privacy. Arguably, providing ballot assurance, in the face of coercion threats, is is the most challenging aspect of End-to-end verifiability. Nonetheless, various ingenious methods have been devised to provide voters with suitable, non-transferable assurance.
One notion of checking whether ballots correctly encode votes is known as *cast-as-intended* (aka *ballot assurance*).
- *Cast-as-intended*. A voter can check whether their ballot correctly expresses their vote.
Discussion of cast-as-intended originates from Chaum (**Chaum02:PunchScanDraft?**; **Chaum04:PunchScan?**) and was taken further by Neff (**Neff04:MarkPledge?**), Adida & Neff (**AdidaN06?**), and Benaloh (**Benaloh06:BallotAudit?**; **Benaloh07:BallotAudit?**). Yet, formal study of cast-as-intended is limited: Unlike other properties of voting systems, a definition of cast-as-intended has yet to be formalised. (Cf. the rich literature on formal definitions of verifiability (**JCJ10?**; **Smyth10:ElectionVerifiabilityA?**; **Smyth10:ElectionVerifiability?**; **Kusters10?**; **Kiayias15?**; **Smyth15:ElectionVerifiability?**; **Cortier16:VerifiabilitySoK?**; **Smyth20:GV?**; **DBLP:conf/csfw/IovinoRRR20?**) and privacy (**JCJ10?**; **Moran06?**; **DKR08?**; **Unruh10?**; **Kusters12:CoercionResistance?**; **2013:BallotIndependenceESORICS?**; **BCGPW15?**; **Smyth15:BallotSecrecyFull?**; **Kiayias15?**; **2017-verifying-observational-equivalence?**; **Hirschi17:SufficientConditionsSecrecyDKR?**; **2019-surveying-receipt-freeness?**; **2019-surveying-coercion-resistance?**).) Here, we formalise cast-as-intended as a game in the computational model of cryptography, thus filling a gap in the literature.
In this paper we consider two categories of End-to-End Verifiable voting system: *conventional*, wherein each voter checks that a *protected ballot* [^2] that represents their vote, typically an encryption of their vote, appears on the bulletin board, and *tracker-based*, where each voter checks their (plaintext) vote appears in the election outcome, using a private tracker. Examples of the former include Prêt à Voter, Helios, and Belenios. Examples of the latter, Selene (**ryan2016selene?**) and sElect (**kusters2016select?**). Cast-as-intended is achieved very differently across these categories, so we apply our definition to examples in each. In the first category, voters cast ballots that are encryptions of their votes and tallies should correspond votes embedded in those ballots. Since voters cannot compute ciphertexts, they rely on a device or process to encrypt. Assuring the voter that the resulting ballot correctly encodes their vote without undermining privacy, and in a manner that is usable and understandable, is highly non-trivial, and various techniques have been presented in the literature.
The second category provides verifiability in a more direct and transparent fashion: the voter is able to identify their (plaintext) vote in the tally. In fact, such systems provide *tallied as intended* verification and, in contrast to the conventional schemes, cast as intended is not strictly necessary. Some subtleties nonetheless remain. For example, each voter should be assured that their tracker is unique. We discuss the details later.
For conventional voting systems, in contrast to tracker-based schemes, it is essential that the voter be able to verify that their vote is correctly embedded in the ballot. This is typically achieved via some form of cut-and-choose mechanism: the device is required to commit to one or more encryptions of the voter’s vote and all but one of these are randomly selected then audited to confirm that the correct vote was encoded. The remaining, non-audited ballot can then be cast.
Benaloh proposed a mechanism, in effect a sequential cut-and-choose, to provide such assurance (**Benaloh06:BallotAudit?**): A voter inputs a vote into a device, the device computes an encryption of the vote, and commits to the resulting ciphertext, by printing the ciphertext or digitally signing it, for instance. Next, the voter chooses to audit or cast the ciphertext. For the former, if auditing fails, the voter should raise an alarm, otherwise (auditing succeeds), the audit or cast process repeats, until the voter chooses to cast.
Auditing typically reveals coins used to construct ciphertexts, enabling ciphertext reconstruction, which suffices to convince a voter that their ballot expresses their vote, assuming they can reconstruct the ciphertext themselves (using a system they trust) or a trusted third party can. Thus, cast-as-intended can be unconditionally achieved, assuming perfect correctness of the underlying encryption scheme.
Reliance on a trusted system or trusted third party to perform ballot audits may seem disingenuous; after all, trust is contrary to the goal of verifiability. However, ciphertexts can be reconstructed by multiple systems, third parties, or both, thereby removing the need to trust any individual device or service.
Most schemes that reveal coins do not allow audited ballots to be cast, to avoid compromising receipt-freeness. (A notable exception is Neff’s MarkPledge (**neff2004practical?**).) A consequence of this observation is that ballot assurance is probabilistic rather than deterministic.
# Security definition
For schemes in the conventional category, cast-as-intended requires ballots be correctly constructed. For many schemes, correct ballot construction simply requires computing a valid encryption of the vote, with respect to the public key of the tabulation process. For universally-verifiable voting systems, it follows that if a voter’s ballot correctly encodes the voter’s vote, and that ballot is correctly tallied, then the voter’s vote will be correctly included in the tally.
We formalise cast-as-intended in the syntax proposed by Smyth, Frink & Clarkson (**Smyth15:ElectionVerifiability?**): Construction is defined by a probabilistic polynomial-time algorithm $\mathsf{Vote}$, wherein
$\mathsf{Vote}$ takes as input a public key $\mathit{pk}$, a voter’s vote $v$, some number of candidates $\mathit{nc}$, and a security parameter $\kappa$, and outputs a ballot $b$ or error symbol $\perp$, where vote $v$ should be selected from a sequence $1,\dots,\mathit{nc}$ of candidates.
Universal verifiability assures us that votes expressed in ballots constructed using algorithm $\mathsf{Vote}$ will be correctly counted, and cast-as-intended enables voters to check that their vote is expressed in a ballot constructed using algorithm $\mathsf{Vote}$.
Ballot construction differs between systems. In some cases, the ballot may be generated by software on the voter’s computer. Other cases may be more elaborate, e.g., Prêt à Voter involves authorities generating and distributing blank two-column paper ballots, and voters physically marking their selections before discarding the left column. Yet further systems (e.g., code-voting, PunchScan, Scantegrity, and PGD) encode votes by means other than encryption, using material from an initialisation phase. For example, in code voting, a correspondence between vote options and codes is committed in print on the code sheets, and this should be consistent with the mapping of codes to votes that is committed to the bulletin board. Some verifiable schemes even avoid cryptography, e.g., Randell/Ryan (**randell2006voting?**) and ThreeBallot (**rivest2006threeballot?**).
Formalising cast-as-intended involves defining what it means for a ballot to be correctly constructed and the means to verify this, which can be captured as a game that challenges an adversary to achieve the opposite: To dupe a voter into believing their ballot encodes their vote, when it does not. We model ballot construction as an algorithm $\mathcal A$ parametrised by a public key $\mathit{pk}$, some number of candidates $\mathit{nc}$, and a security parameter $\kappa$, and we model the voter as an algorithm $\mathcal V$ that takes a vote $v$ and a distinct security parameter $\hat\kappa$ as input. The latter security parameter determines the probability of breaking cast-as-intended, whereas the former determines the probability of breaking other security properties, such as individual and universal verifiability. We use distinct security parameters, because the complexity of algorithm $\mathcal V$ should be upper-bounded by the capability of a voter’s mind, whereas algorithm $\mathcal A$ should be computable by machine.
The system is assumed to be adversarial and, to achieve cast-as-intended, some trustworthy device is also required. (Alternatively, a multitude of devices may be used, only one of which need be trustworthy.) We model such a device as an algorithm $\mathcal T$ that takes the same parameters as algorithm $\mathcal A$. Hence, ballot construction is modelled by the computation $b\leftarrow \mathcal V^{\mathcal T,\mathcal A}(v,\hat\kappa)$, where algorithm $\mathcal T$ is parameterised by $\mathit{pk}$, $\mathit{nc}$, and $\kappa$. If cast-as-intended is achieved, then such computations should result in a ballot $b = \mathsf{Vote}(\mathit{pk},\allowbreak v,\allowbreak\mathit{nc},\allowbreak\kappa; r)$ for some coins $r$ or the error symbol $\perp$ (representing a voter detecting malice), which leads to to our security definition (Definition [def:castAsIntended]). In that definition, we extend algorithm $\mathcal A$ with the capabilities of a malicious administrator that defines the public key, the voter’s vote, and the number of candidates, when parametrised by security parameters $\kappa$ and $\hat\kappa$.
An adversary $\mathcal A$ that wins $\mathsf{Cast}\textrm{-}\mathsf{As}\textrm{-}\mathsf{Intended}$ is able to identify a strategy, including choosing a public key $\mathit{pk}$, a vote $v$, and a number of candidates $\mathit{nc}$, such that a voter $\mathcal V$ will be deceived into casting a ballot $b$ that does not express their vote $v$. That is, winning signifies an attack against cast-as-intended.
An election scheme satisfying cast-as-intended guarantees that a voter can check whether their ballot is an output of algorithm $\mathsf{Vote}$, parametrised with their vote $v$ along with public key $\mathit{pk}$, number of candidates $\mathit{nc}$, and security parameter $\kappa$, for some coins $r$. Supposing universal verifiability, a voter can check whether the election outcome corresponds to votes expressed in tallied ballots.
Our definition assumes that each voter performs verification steps correctly. Beyond the definition’s scope, we must consider the practicality of voters correctly performing verification. Thus, even when a voting system satisfies cast-as-intended, that system may still be vulnerable to attacks arising from voter error or negligence (possibly attacker induced).
Let us finally remark on an important point, namely, that the definition depends crucially on the protocol description for the honest voter $\mathcal V$. If we have a protocol that always aborts the casting, then this would reduce the adversary’s advantage to zero and we would claim it satisfies cast-as-intended. Hence, we also require a soundness condition asserting that $\mathcal V$ should only abort if the ballot is ill-formed, or more exactly, that this should only occur with bounded probability: We assume that $\mathcal V$ only aborts when indeed she has detected the $b$ is ill-formed. In practice, whether we can check if a voter is maliciously aborting enters into the territory of *dispute resolution*.
# Examples
**\[tex2md\] this section could not be converted; its LaTeX follows verbatim:** `Error at (line 341, column 14): expecting \end{center} \end{tabular} ^`
``` latex
\section{Examples}
\subsection{Pr\^et \`a Voter}
\begin{figure}
\begin{center}
\begin{tabular}{c@{\qquad}c@{\qquad\qquad\qquad\qquad}c@{\qquad}c}
\begin{tabular}{c}
(a)
\end{tabular}
&
\begin{tabular}{|l|p{36pt}|} \hline
Obelix & \\ \hline Idefix & \\ \hline Asterix & \\ \hline
Panoramix &
\\ \hline
& {$7304944$} \\ \hline
\end{tabular}
&
\begin{tabular}{c}
(b)
\end{tabular}
&
\begin{tabular}{|c|} \hline
\\ \hline X
\\ \hline
\\ \hline
\\ \hline ${7304944}$ \\ \hline
\end{tabular}
\end{tabular}
\end{center}
\caption{Pr\^et \`a Voter ballot (a) and receipt (b) for vote ``Idefix''} \label{fig:pret}
\end{figure}
In Pr\^et \`a Voter \cite{chaum2005practical} the voter gets a ballot with a left and right hand side. The candidates are listed in plaintext in a random order on the left hand side (LHS) and this order is embedded cryptographically in a value on the right hand side (RHS). In the privacy of the booth, the voter marks their selection on the right hand side against the candidate(s) as indicated on the LHS. Once they have made their mark(s) they detach and destroy the LHS, i.e. removes the plaintext list of candidates, thus concealing the selection and creating the receipt.
The universal verifiability of the scheme will afterwards guarantee that the vote is processed according to the encrypted order.
The ballot is thus correctly constructed, if the encrypted candidate order on the RHS matches the one displayed in plaintext on the LHS. To check this the voter can perform ballot audits to verify this, but cannot verify the actual cast ballot. Additionally, ballots can be randomly audited by observers. Note that for Pr\^et \`a Voter ballot auditing can be delegated and is entirely privacy preserving and indeed dispute resolving.
Let us first consider the case where voters are instructed to choose $\kkk$ ballots and audit all of these but one. In a worst case scenario, the adversary is able to inject a chosen number of maliciously created ballots into this selection $\kkk$ ballots. The adversary obtains the best advantage by injecting precisely one ballot and wins if this is used for vote-casting, i.e. $P_{\textrm{Adv succ}}=1/\kkk$, i.e. $\delta\geq 1/\kkk$.
We can also consider the case, where a voter audits a ballot with a probability $p$. We further assume that the probability that a ballot is audited by observers is $q$. We then find %, and we use the calculation for the adversary advantage resulting from the voter's Benaloh challenges given in the next section, then we get:
$$P_{\textrm{Adv succ}}=(1-q) \cdot (1-p).$$
Using the arguments for Benaloh challenges below, this also holds if the voter audits multiple times with the same probability.
Here we are assuming that the random audits are unpredictable and that chain-of-custody of the set of ballot forms is guaranteed, i.e. fake ballot forms cannot be injected after the observer audits are performed. In fact, observer audits can be performed before, during and after voting, so this assumption is quite mild.
\subsection{Benaloh}
Let us now make a simplified analysis of Benaloh challenges. We ignore all information that could be leaked by the vote choice used by the voter. Let us assume that the voter has fixed probability in each round to audit. We can argue that this makes sense since the voter obtains no other knowledge during the Benaloh challenge process to influence the probability, and we ignore vote choices. For the adversary, we will also assume he has a fixed probability in each round. Let $p_i$ denote the probability of the voter doing an audit in round $i$ and $q_i$ the probability that the adversary changes a vote in this round.
The probability that the adversary is successful is obtained by sum of the probabilities that he is successful in round $i$ which is the probability that the voter challenges all earlier rounds, that the adversary was honest in all of these, and then he cheated in round $i$. That is
$$P_{\textrm{Adv succ}}=\sum_{i=1}^\infty p_1\cdots p_{i-1}(1-q_1)\cdots (1-q_{i-1})(1-p_i)q_i$$.
We only aim to make a simplified analysis and we do this by assuming that the probabilities will not depend on the rounds. For the voter this could happen if we specify to the voter to make an audit with a certain probability. Then we get
$$P_{\textrm{Adv succ}}=\sum_{i=1}^\infty p^{i-1}(1-q)^{i-1}(1-p)q=\frac{(1-p)q}{1-p(1-q)}.$$
This function is increasing in cheat probability $q$. Thus if the adversary wants to maximise this, he chooses $q=1$ i.e. to always cheat. The winning probability is then
$$P_{\textrm{Adv succ}}=1-p,$$
corresponding to the probability that the voter casts in the first round.
That is we have $\delta\geq 1-p$. Note that the average number of challenge rounds in the vote casting is $1/(1-p)$ (without an adversary present). Abusing notation, we thus have that $\delta\geq1/\kkk$ where $\kkk$ is the number of challenge rounds.
Note however, that if the voter is not prescribed a certain audit probability $p$ and doesn't care about the effort of doing the audits, then $P_{\textrm{Adv succ}}$ is a decreasing function in $p$ i.e. the voter would choose $p\approx1$, i.e. to almost always audit. A full analysis should be done via game theory, see also \cite{culnane2016strategies}.
\subsection{MarkPledge}
MarkPledge, \cite{Neff04:MarkPledge}, is of particular interest in the context of cast-as-intended as it provides assurance of correctness of the ballot that is actually cast. This is in contrast to cut-and-choose style ballot assurance, e.g. Benaloh challenges, where an audited ballot cannot be cast.
At a very high level, MarkPlegde involves the voter interacting with a device in the booth to perform an interactive zero-knowledge proof of correctness of the ballot. In essence, this proof serves to convince the voter that a 1 is encrypted against the candidate of choice and a transcript of this proof is printed on the receipt. As part of this interactive ZK proof, the voter provides a random challenge, e.g. a string of $k$ digits.
This alone would not of course be receipt-free, so the chosen vote is masked by the device constructing fake ZK proof transcripts that an encryption of 1 against the other candidates. The device also provides a ZK proof that there is exactly one encryption of 1 and the other encryptions are of 0. Anyone later seeing the receipt cannot distinguish the real and fake proofs and hence cannot identify which candidate was selected. Only the voter will know for which candidate they executed the real, interactive proof.
During tabulation, the candidates with an encryption of zero are weeded out, exploiting the homomorphic properties of the encryption, leaving just those with the encryption of 1.
The ballot assurance provided by MarkPledge is therefore dependent on the size of the challenge space. So if the challenges are strings of $k^*$ digits, we get a bound on the chance of the device being about to cheat the voter of $p=1/10^{k^*}$.
\subsection{ThreeBallot}
In the ThreeBallot scheme by Rivest \cite{rivest2006threeballot} a voter distributes their vote intent over three ballots. The scheme is interesting in this context as it does not employ cryptography, and voter can tell directly whether the (three)ballot is correctly constructed. We will also assume here that mechanisms are in place to ensure that the (three)ballot is well formed, i.e. obeys the rules (two votes for the chosen candidate and one for the others).
The ballots contain unique serial numbers. These are sent to a Bulletin Board, but the voter chooses one of the single ballots and gets a copy of it. The voter's choice of which of the three ballots should be concealed from the system. At home, the voter checks that the single ballot with the corresponding serial number appears online and that the partial vote choice in that ballot is correctly stored.
Note that this example is special since this verification step is also a stored-as-cast verification. With a malicous authority involved the serial numbers might not be unique, and could give rise to clash attacks. In this case it is not really meaningful to say that the displayed ballot is the voters ballot, since it will be assigned to one or more voters. However, in the scope of cast-as-intended, we we will focus on a single voter setting, and leave such problems to other parts of verifiability.
If we assume that the voter chooses the receipt slip uniformly at random and the adversary is unaware of this choice, then the adversary can try to change one single ballot of three, and will succeed with an undetected change of the ballot with probability $2/3$. Thus $\delta\geq2/3$
\begin{table}
\centering
\begin{tabular}{|l|c|c|c|c|c|}
\hline
% after \\: \hline or \cline{col1-col2} \cline{col3-col4} ...
Scheme & Pr\^et \`a Voter & Benaloh & MarkPledge & ThreeBallot & Selene \\ \hline
$\delta$ & $1/\kkk_1$ & $1/\kkk_2$ & $1/10^{\kkk}$ & $2/3$ & $0$ \\ \hline
Delegable &\ding{51} & \ding{51} & \ding{55} & \ding{51} & \ding{55} \\
\hline
\end{tabular}
\caption{The different cast-as-intended protocols and their respective cast-as-intended $\delta$-value. $\kkk_1 = (1-p) \cdot (1-q)$, $\kkk_2 = (1-p)$. We also note if the verification checks, or parts thereof, are delegable.}
\label{tab:table1}
\end{table}
```
# Tracker-based schemes
Ryan, Rønne, & Iovino recently (**ryan2016selene?**) introduced an orthogonal approach in which the cast-as-intended is first established after tallying. For traditional voting systems, voters perform a cast-as-intended check to ensure their ballot correctly expresses their vote, an individual-verifiability check to ensure their ballot is collected, and a universal-verifiability check to ensure their vote is counted. By comparison, Ryan, Rønne, & Iovino propose that voters simply check whether their plaintext vote is present in the tally, using a private tracker—the standard early cast-as-intended and individual-verifiability checks are not necessary; a more direct, more transparent form of verification is achieved. Voting systems Selene (**ryan2016selene?**) and sElect (**kusters2016select?**) achieve this new form of tracker-based verifiability, with the main difference being that Selene first releases the tracker to the voter after tallying to provide coercion-mitigation - the voter can equivocate the tracker to a tracker for another vote.
## Example: Selene
Selene, (**ryan2016selene?**) is an example of a tracker-based verifiable scheme in which the voter can confirm directly that their vote is included in the tally. The mechanism can be applied to various forms of e-voting schemes (**DBLP:conf/fc/IovinoRRR17?**; **ronne2018electryo?**; **DBLP:conf/icdcs/SallalSCDTDRW20?**; **alsadi2020verify?**), has been studied formally (**DBLP:conf/fc/ZollingerRR20?**; **DBLP:conf/voteid/JamrogaKK18?**), and has been studied from a usability viewpoint (**DBLP:conf/chi/DistlerZLRRK19?**; **zollinger2019user?**). In Selene the voters hold secret trapdoor keys. After the end of election and after the tally has been made public, the voters will receive an cryptographic term, called the alpha term. This is combined with a public beta term which is available on the bulletin board to form an ElGamal encryption of the tracker under the voter’s trapdoor key. The voter can now decrypt this to retrieve their tracker. The tracker is then used to check the plaintext vote on the final tally board.
The authorities could send a fake alpha term to the voter, however, as is proven in (**ryan2016selene?**) the chance of such an alpha term opening to an existing tracker is negligible assuming that the authorities do not know the voter’s trapdoor key and under a computational assumption (hardness of computing $g^{x^2}$ given $g^x$ without knowing $x$). Thus if the voter’s trapdoor key is not leaked and the computational assumption holds, then $\delta$ is negligible. This presupposes that the proofs and verifiable computations on the bulletin board are verified, which can be done by the voter herself, or any third party.
In a tracker based scheme, traditional cast-as-intended and individual- and universal-verifiable checks are all bundled into a single tallied-as-cast check.
# Outlook
Verifiability has emerged as a means to ensure integrity of elections. Several aspects of verifiability have been identified: well studied notions of individual- and universal-verifiability, and the seemingly less well understood notion of cast-as-intended. We propose the first formal definition of cast-as-intended, closing a gap in the literature and enabling analysis of systems purporting to achieve cast-as-intended.
Future work could flesh out and make more rigorous the arguments we sketch for MarkPledge, Prêt à Voter, Selene, ThreeBallot, and schemes based upon Benaloh challenges. Other voting systems could also be analysed, e.g., Pretty Good Democracy and Bingo Voting. It would also be interesting to analyse any relation between cast-as-intended and dispute resolution, privacy during ballot construction, or both. Perhaps most importantly: A suitable security notion to bridge the gap between individual verifiability and cast-as-intended should be sought, see also (**Smyth20:mind-the-gap?**) which points out that individual- and universal-verifiability plus cast-as-intended does not yield end-to-end verifiable voting systems, e.g. clash attacks are not captured. It would also be interesting to see to which extent trust can be removed from the cast-as-intended verification (**DBLP:conf/csfw/IovinoRRR20?**).
Another interesting future path is to relate the parameter $\hat\kappa$ more tightly to usability in order to compare the achieved level of security to the amount and complexity of user-interaction required. We already did a preliminary attempt of this with the values shown in Table [tab:table1] where $\hat\kappa$ represents the number of interactions or the number of digits a voter needs to handle, but comparing and understanding the usability, especially across systems, will require actual user studies.
#### Acknowledgements.
This work received financial support from the Luxembourg National Research Fund (FNR) under the PolLux/CORE project STV (12685695) and the FNR CORE project EquiVox (13643617).
[^1]: where more than one voter gets assigned the same ballot
[^2]: to use Rivest’s terminology