Ceremonies for End-to-End Verifiable Elections

Abstract

State-of-the-art e-voting systems rely on voters to perform certain actions to ensure that the election authorities are not manipulating the election result. This so-called “end-to-end (E2E) verifiability” is the hallmark of current e-voting protocols; nevertheless, thorough analysis of current systems is still far from being complete.

In this work, we initiate the study of e-voting protocols as ceremonies. A ceremony, as introduced by Ellison [23], is an extension of the notion of a protocol that includes human participants as separate nodes of the system that should be taken into account when performing the security analysis. that centers on the two properties of end-to-end verifiability and voter privacy and allows the consideration of arbitrary behavioural distributions for the human participants.

We then analyse the Helios system as an e-voting ceremony. Security in the e-voting ceremony model requires the specification of a class of human behaviours with respect to which the security properties can be preserved. We show how end-to-end verifiability and voter privacy are sensitive to human behaviour in the protocol by characterizing the set of behaviours under which the security can be preserved and also showing explicit scenarios where it fails.

We then provide experimental evaluation with human subjects from two different sources where people used Helios: the elections of the International Association for Cryptologic Research (IACR) and a poll of senior year computer science students. We report on the auditing behaviour of the participants as we measured it and we discuss the effects on the level of certainty that can be given by each of the two electorates.

The outcome of our analysis is a negative one: the auditing behaviour of people (including cryptographers) is not sufficient to ensure the correctness of the tally with good probability in either case studied. The same holds true even for simulated data that capture the case of relatively well trained participants while, finally, the security of the ceremony can be shown but under the assumption of essentially ideally behaving human subjects. We note that while our results are stated for Helios, they automatically transfer to various other e-voting systems that, as Helios, rely on client-side encryption to encode the voter’s choice.

A. Kiayias, T. Zacharias, B. Zhang—This research was partly supported by ERC project $\#259152$ (CODAMODA), Horizon 2020 project $\#653497$ (PANORAMIX), and project FINER, Greek Secretariat of Research and Technology, funded under action ARISTEIA 1.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

A ceremony, introduced by Ellison [23], extends the notion of a security protocol to include “human nodes” in the protocol specification together with regular computer nodes. Human nodes, are computationally limited and error-prone; they are able to interact with computer nodes via a user interface (UI) as well as communicate with each other via direct communication lines. In this model, computer nodes can be thought of as stateful and probabilistic interactive Turing machines, while human nodes, even though they are stateful, they are limited in terms of computational power and their behaviour can only be considered as a random variable following some arbitrary probability distribution over a set of “admissible behaviours” that are dictated by the UI’s they are provided with. Designing and analyzing the security of ceremonies has proven to be valuable for problems that non-trivially rely on human node interaction to ensure their security properties, such as key provisioning and web authentication, see e.g., [10, 23, 31, 44].

In this work, we initiate the study of secure E-voting ceremonies. An e-voting ceremony is a protocol between computer and human nodes that aims to assist a subset of the humans (the voters) to cast a ballot for a specified election race. We argue that viewing e-voting as a ceremony (i.e., a protocol with human and computer nodes) captures the security intricacies of the e-voting problem much more effectively than standard protocol based modelling as it was done so far. The reason for this, is that the properties of an election system, most importantly verifiability, rely on human participant behaviour in a highly non-trivial manner. The ability of human nodes to compromise overall security due to their negligence is well known in e-voting system design (cf. [29]) and it is high time that cryptographic models extend to incorporate formally the human participants.

The capability to perform auditing is widely accepted as the most important characteristic for modern e-voting systems. However, even widely deployed¹ systems such as Helios [1] that are touted to be verifiable via auditing still provide only unquantified guarantees of verifiability. The main reason for this is that the correctness of the election result when the election authorities are adversarial is impossible to verify unless the humans that participate in the protocol follow a suitable behaviour. This means that the voters, beyond the ballot-casting procedure, are supposed to carry out additional steps that many may find to be counterintuitive, see e.g., [43] for more discussion of this issue. This potentially leads to the defective execution of the appropriate steps that are to be carried out for verifiability to be supported and hence the verifiability of the election may collapse. Recent studies have shown that voters have rather limited participation and interest to perform the verification steps (e.g., [22] reports about 23 out of a sample of 747 people performed a verifiability check in a deployed end-to-end (E2E) verifiable system). Given that the auditing performed by the voters is critical for the integrity of the election result as a whole, it is imperative to determine the class of distributions of behaviours that are able to detect (significant) misbehaviour of the election authorities. Once this class is characterised then one may then try to influence participants to approximate the behaviour by training them.

Traditionally (cf. [11, 12, 14, 28, 42, 45]), election verifiability was considered at the “individual level” (i.e., a single voter is able to verify her vote intent is properly included in the tally) and the “universal level” (i.e., the election transcript appears to be properly formed). No voter behavioural characteristics were taken into account in the security analysis and the protocols were deemed “end-to-end verifiable” as long as they satisfied merely these two features². The work of [37,38,39] showed that individual verifiability and universal verifiability, even if combined, can still fail to guarantee that the election tally is correct. To mend the concept of verifiability, a “holistic” notion of global verifiability was introduced. Nevertheless, such global verifiability is unattainable without any assumption on human behaviour. Indeed, [39] establishes the verifiability of the Helios system by assuming that voters perform an unbounded number of independent coin flips — an assumption which should be at best considered of theoretical interest, since no voter using the Helios system (or any e-voting system for that matter) should be expected to actually perform ballot-casting via the employment of independent coin flips.

Beyond verifiability, an e-voting system is supposed to also satisfy privacy and other desired properties such as receipt-freeness/coercion resistance. These properties interact with verifiability in various important ways: First, without privacy it is substantially easier to achieve verifiability (this is due to the fact that verification of the recording of one’s vote can be done in relatively straightforward manner assuming a public “bulletin-board” [4]). Second, receipt-freeness combined with verifiability suggests that the receipt obtained by the voter from ballot-casting can be delegated to a third-party without fear of coercion or privacy leakage. Given these reasons, a proper analysis of an e-voting system should also include the analysis of at least these properties. The fact that privacy will be entrusted to a set of “trustees” that are human participants in the e-voting system, points again to the importance of the ceremony approach for the case of privacy.

Our Results. Our results are as follows.

$\blacksquare$ We initiate the study of e-voting ceremonies, i.e., e-voting protocols that involve computer and human nodes, and enable the human participant voters to cast privately their ballots and calculate their tally. In an execution of an e-voting ceremony, human nodes follow a certain behaviour which is sampled according to some distribution over all possible admissible behaviours. No specific assumptions can be made about how human nodes behave and thus the distribution of each human node is a parameter of the security analysis. It follows that the security properties of e-voting ceremonies are conditional on vectors of probability distributions of human behaviours. Such vectors are specified over sets of suitably defined deterministic finite state machines with output (transducers³) that determine all possible ways that each human participant may interact with the UI’s of the computer nodes that are available to them.

$\blacksquare$ Extending the work of [34, 39], we provide a threat model for (end-to-end) verifiability for e-voting ceremonies. Our threat model has the following characteristics: (i) it provides a holistic approach to argue about end-to-end verifiability by casting the property as an “attack game” played between the adversary and a challenger. (ii) it provides an explicit final goal the adversary wants to achieve by introducing a metric over all possible election outcomes and stating an explicit amount of deviation that the adversary wants to achieve in this metric space. (iii) the adversary is successful provided that the election tally appears to be correct even though it deviates from the true tally according to the stated metric while the number of complaining voters in any failed ballot-casting processes is below a threshold (a ballot-casting process may fail because of adversarial interference). (iv) the resources of the adversary include the complete control of all trustees, election authorities, all voter PC’s as well as a subset of the voters themselves. Regarding privacy, we extend the work of [8, 34], by providing a threat model for privacy and passive coercion resistance in the sense of [2] for e-voting ceremonies.

$\blacksquare$ We cast Helios as an e-voting ceremony: voters and trustees are the human participants of the protocol that are supposed to handle credentials and receipts as well as generate and validate ciphertexts. During ballot-casting, voters perform the Benaloh challenge process [5] and are free to choose to cast their ballot. Voters may further choose to audit their ballot in the bulletin board if they wish to. Trustees are supposed to execute deterministic steps in order to perform the public-key generation during the setup stage of the election and are able to verify their public-key in the bulletin board if they wish. The set of admissible behaviours for voters include any number of Benaloh challenges followed by casting the ciphertext and choosing whether to audit it in the bulletin board.

$\blacksquare$ We analyse the Helios e-voting ceremony with respect to the threat-model for privacy and passive coercion and end-to-end verifiability. The behaviours of voters are an explicit component of the security analysis. Specifically, for end-to-end verifiability, we characterise the space of admissible behaviours that enable the verifiability of the election result and we prove an infeasibility and a feasibility result:

• 1. It is infeasible to detect a large deviation in the published tally of the election even if a high number of voters audit it, if (i) there is some $i^*$ that the average voter will perform exactly $i^*$ Benaloh audits with high enough probability compared to the tolerance level of complaints, or (ii) there is a set of indices $\mathcal {J}^*$ that if the average voter performs $j\in \mathcal {J}^*$ Benaloh audits, this can be used as a predictor for not auditing the bulletin board; (see Theorem 1 for the precise formulation of the infeasibility result).

• 2. It is feasible to detect a deviation in the tally if a suitable number of voters audit the election, provided that (i) for all i the probability that the adversary performs exactly i Benaloh audits is sufficiently small, and (ii) if the number j of Benaloh audits can be used as a predictor of not auditing the bulletin board, then it holds that the likelihood of j Benaloh audits is sufficiently small; (see Theorem 2 for the precise formulation of the feasibility result).

Regarding privacy, we show that assuming the trustees audit with sufficiently high probability the correct posting of the public-key information, Helios maintains privacy under the assumption that the underlying public-key encryption scheme is IND-CPA.

$\blacksquare$ We provide an experimental evaluation from two different sources of human data where people used Helios. We report on the auditing behaviour of the participants as we measured it and we discuss the effects on the level of certainty that can be given in each of the two elections. The message from our evaluation is a negative one: The behaviour profile of people is not such that it can provide sufficient certainty on the correctness of the election result. For instance, as we show from the data collected from the elections of the directors of the International Association for Cryptologic Research (IACR), for elections in the order of hundreds (500) more than 3% of the votes could be overturned with significant probability of no detection (25%), cf. Fig. 2. Based on public data on recent election results of the IACR the votes for elected candidates were sufficiently close to candidates that lost in the election and consequently, the results could have been overturned with significant probability without being detected, cf. Table 3. Our results are similarly negative in the second case study. Given our negative results for actual human data, we turn to simulated results for investigating the case when the voters are supposedly well trained with respect to election guidelines. Even for a voter behaviour distribution with supposedly relatively well trained voters our simulated experiment show that the validity of the election result is sustained with rather low confidence.

We note that even though we focused on Helios in this work, our results (including our threat-model analysis for ceremonies and associated security theorems) immediately apply to a number of other e-voting systems. Such systems (that have been identified as single-pass systems in [8]) include [18,19,20, 32, 47].

Related Work

Ceremony Study. In 2008, protocol ‘ceremony’ was introduced by Ellison [23] to expand a security protocol with out-of-band channels and the human users. Subsequently, Karlof et al. [30] formalised the ‘conditioned-safe ceremony’ notion, that encompasses forcing functions, defence in depth, and human tendencies. They then evaluated an e-mail web authentication ceremony with 200 participants. Later, the strengths and weaknesses of the ‘ceremony’ notion were examined by Radke et al. [44] in the context of HTTPS, EMV and Opera Mini protocols/ceremonies. In 2013, Carlos et al. [9, 40] claimed that even though Dolev-Yao’s threat model can represent the most powerful attacker in a ceremony, the attacker in this model is not realistic in certain scenarios, especially those related to human peers. They then proposed a threat model that can be adjusted according to each ceremony and consequently adapt the model and the ceremony analysis to realistic scenarios. In 2014, Hatunic-Webster et al. [26] proposed an Anti-Phishing Authentication Ceremony Framework for investigating phishing attacks in authentication ceremonies, which builds on the human-in-the-loop security framework of communication processing. Bella and Coles-Kemp [3] introduced a layered analysis of security ceremonies. Their work focuses on the human-computer interaction layer, which features a socio-technical protocol between a user “persona” and a computer interface. As a more related work, in 2015, Johansen and Jøsang [27] proposed a formal probabilistic model for verifying a security ceremony. In their work, the human agent interaction with the user interface are modelled as a non-deterministic process.

E-Voting Modelling. Conventionally, the verifiability and privacy of an e-voting system is modelled and analysed separately. In terms of the verifiability, individual verifiability [11] and universal verifiability [28, 45] was introduced about 20 years ago. End-to-end verifiability in the sense of cast-as-intended, recorded-as-cast, tallied-as-recorded was introduced by [12, 42] in 2004. The term of End-to-end verifiability/integrity also appeared in [16]. Later, Küsters et al. [37] formally proposed symbolic and computational definitions of verifiability. The verifiability of Helios was studied in both symbolic model [36] and computational model [46]. [38] showed that individual verifiability and universal verifiability are not sufficient to guarantee the “global” verifiability of an e-voting system and In [39], they introduced clash attacks, which break the verifiability of some variants of Helios. In terms of privacy, computational privacy was introduced by Benaloh and Fischer [15], while receipt-freeness has been first studied by Benaloh and Tuinstra [6]. Formal definitions for privacy and receipt-freeness have been proposed in the context of applied pi calculus [21] and the universal composability model [25, 41]. In [38], the level of privacy of an e-voting system is measured w.r.t. to the observation power the adversary has in a protocol run. In [7], Bernhard et al. proposed a game-based notion of ballot privacy and study the privacy of Helios. Their definition was extended by Bernhard et al. [8] by allowing the adversary to statically corrupt election authorities. Both these definitions, although they imply a strong indistinguishability property, do not consider receipt-freeness.

Roadmap. The rest of the paper is organised as follows. In Sect. 2, we introduce the entities, the syntax and the security framework of an e-voting ceremony. In Sect. 3, we describe the Helios e-voting ceremony according to our syntax. In Sect. 4, we analyse the E2E verifiability of Helios ceremony. Namely, we prove (I) an infeasibility and (II) a feasibility result under specific classes of voter behaviours, and we comment on the logical tightness of the two classes. In Sect. 5, we prove the voter privacy/passive coercion resistance of the Helios ceremony. In Sect. 6, we present evaluations of our results for the E2E verifiability of Helios ceremony. Our evaluations are based on actual human data obtained by elections using Helios as well as simulated data for various sets of parameters. Finally, in the concluding Sect. 7, where we recall the objectives, methodology, analysis and results of this paper and discuss future work.

2 E-Voting Ceremonies

A ceremony [23] is an extension of a network protocol that involves human nodes along side computer nodes. Computer nodes will be modeled in a standard way while we will model humans as probability distributions over a support set of simple finite state machines. We base our framework for ceremonies on the e-voting system modeling from [34] suitably extending it to our setting.

2.1 The Entities of the E-Voting Ceremony

An e-voting ceremony $\varvec{\mathcal {VC}}$ is associated with three parameters set to be polynomial in the security parameter $\lambda$; the number of voters n, the number of options m and the number of trustees k. We use the notation $\mathcal {O}=\{\mathsf {opt}_1,...,\mathsf {opt}_m\}$ for the set of options, $\mathcal {V}=\{V_1,...,V_n\}$ for the set of voters and $\mathcal {T} = \{T_1,\ldots , T_k\}$ for the set of trustees. The allowed ways to vote is determined by the collection of subsets $\mathcal {U}\subseteq 2^\mathcal {O}$ an the option selection $\mathcal {U}_\ell$ of voter $V_\ell$ is an element in $\mathcal {U}$.

Let $\mathcal {U}^*$ be the set of vectors of option selections of arbitrary length. Let f be the election evaluation function from $\mathcal {U}^*$ to the set $\mathbb {Z}^m_+$ so that $f(\mathcal {U}_1,\ldots ,\mathcal {U}_n)$ is equal to an m-vector whose i-th location is equal to the number of times $\mathsf {opt}_j$ was chosen in the option selections $\mathcal {U}_1,\ldots ,\mathcal {U}_n$.

The interaction among the entities involved in an e-voting ceremony is depicted in Fig. 1. The said entities comprise:

$\blacksquare$ The human nodes are the trustees $T_1,\ldots , T_k$, the voters $V_1,\ldots ,V_n$ and the credential distributor ($\mathsf {CD}$). The latter additional entity is responsible for issuing the credentials generated at the setup phase to the voters. Note that in practice, the $\mathsf {CD}$ may be an organization of more than one human nodes executing another ceremony but we do not model this as part of the e-voting ceremony. Here we make the simplifying choice of modeling $\mathsf {CD}$ as a single human node (that is able to identify voters using an external identification mechanism operating among humans).

$\blacksquare$ The computer nodes are the voting supporting devices (VSDs), the trustee supporting devices (TSDs), the auditing supporting devices (ASDs), the election authority ($\mathsf {EA}$), and the bulletin board ($\mathsf {BB}$).

Modelling Human Nodes. We model each human node as a collection of simple finite state machines that can communicate with computer nodes (via a user interface) as well as with each other via direct communication. Specifically, we consider a – potentially infinite – collection of transducers, i.e. finite state machines with an input and an output tape, that is additionally equipped with a communication tape.

Fig. 1.

The entities and the channels active in an e-voting ceremony. The human nodes and the computer nodes used are shown as circles and rectangles respectively. Each voter or trustee human node, interacts with two computer nodes (supporting devices) while the $\mathsf {CD}$ human node interacts with the $\mathsf {EA}$. The dotted lines denote read-only access on the $\mathsf {BB}$. The dotted lines denote read-only access on the $\mathsf {BB}$. The grey dashed lines denote channels between human nodes.

We restrict the size of each voter transducer to depend only on the number of options m. Note that this has the implication that the voter transducer cannot be used to perform cryptographic operations, which require polynomial number of steps in $\lambda$. Transducers may interact with computer nodes, (supporting devices) and use them to produce ciphertexts and transmit them to other computer nodes. The transducers interact with each other via human level communication channels (depicted as dashed gray lines in Fig. 1), where the exchanged messages are readable by humans (e.g. credentials, PINs, or short message texts but not cryptographic data).

Transducer collections corresponding to voter nodes, trustee nodes and the $\mathsf {CD}$ will be denoted as the sets $\mathcal {M}^V$, $\mathcal {M}^T$, and $\mathcal {M}^{\mathsf {CD}}$ respectively. We assume that all sets $\mathcal {M}^V,\mathcal {M}^T$ and $\mathcal {M}^{\mathsf {CD}}$ are polynomial time samplable, i.e., one can produce the description of a transducer from the set in polynomial-time and they have an efficient membership test.

2.2 Syntax and Semantics

In order to express the threat model for the e-voting ceremony, we need to formally describe the syntax and semantics of the procedures executed by the ceremony. We think of an e-voting ceremony $\varvec{\mathcal {VC}}$ as a quintuple of algorithms and ceremonies denoted by $\langle \mathbf {Setup}, \mathbf {Cast}, \mathbf {Tally},$ $\mathbf {Result},\mathbf {Verify}\rangle$ together with the sets of transducers $\mathcal {M}^V, \mathcal {M}^T$ and $\mathcal {M}^\mathrm {CD}$ that express the human node operations; these are specified as follows:

The setup phase is a ceremony executed by the $\mathsf {EA}$, the $\mathsf {BB}$, the transducers $M_{i_1},\ldots , M_{i_n}\in \mathcal {M}^V$ that determine the behaviour of voter $V_1,\ldots ,V_n$ respectively, a transducer $M^{\mathsf {CD}}\in \mathcal {M}^{\mathsf {CD}}$ describing the behaviour of $\mathsf {CD}$, the transducers $M_i^{T}\in \mathcal {M}^T$, $i=1,\ldots ,k$ describing the behaviour of the trustees $T_1,\ldots T_k$ respectively and their TSDs. The ceremony generates $\varvec{\mathcal {VC}}$’s public parameters $\mathsf {info}$ (which include $\mathcal {O},\mathcal {V},\mathcal {U}$) and the voter credentials $\mathsf {cr}_1,\ldots ,\mathsf {cr}_n$. After the ceremony execution, each TSD has a private state $\mathsf {st}_i$, each trustee $T_i$ obtains a secret $\overline{s}_i$ and the $\mathsf {CD}$ obtains the credentials $\mathsf {cr}_1,\ldots ,\mathsf {cr}_n$. In addition, the $\mathsf {EA}$ posts an election transcript $\tau$ initialised as $\mathsf {info}$ on $\mathsf {BB}$. At the end of the $\mathbf {Setup}$, the $\mathsf {CD}$ will provide $\mathsf {cr}_1,\ldots ,\mathsf {cr}_n$ to the voters $V_1,\ldots , V_n$.

The voting phase is a ceremony executed by the $\mathsf {EA}$, the $\mathsf {BB}$, a transducer $M_{i_\ell }\in \mathcal {M}^V$ that determines the behaviour of voter $V_\ell$ and her supporting devices $\mathsf {VSD}_\ell$, $\mathsf {ASD}_\ell$. $V_\ell$ executes the $\mathbf {Cast}$ ceremony according to the behaviour $M_{i_\ell }$ as follows: $M_{i_\ell }$ has input $(\mathsf {cr}_\ell ,\mathcal {U}_\ell )$, where $\mathsf {cr}_\ell$ is the voter’s credential and $\mathcal {U}_\ell$ represents the option selection of $V_\ell$. All communication between the voter $V_\ell$ and $\mathsf {EA}$ (resp. $\mathsf {BB}$) happens via $\mathsf {VSD}_\ell$ (resp. $\mathsf {ASD}_\ell$), where $\mathsf {BB}$ has input $\tau$. Upon successful termination, $M_{i_\ell }$’s output tape contains the individual audit information $\mathsf {audit}_\ell$ returned by $\mathsf {VSD}_\ell$. If the termination is not successful, $M_{i_\ell }$’s output tape possibly contains a special symbol ‘$\mathsf {Complain}$’, indicating that voter $V_\ell$ has decided to complain about the incorrect execution of the election procedure. In any case of termination (successful or not), $M_{i_\ell }$’s output tape may contain a special symbol ‘$\mathsf {Audit}$’, indicating that $V_\ell$ has taken the decision to use her individual audit information $\mathsf {audit}_\ell$ to perform verification at the end of the election; in this case, the individual audit information $\mathsf {audit}_\ell$ will be provided as input to the ASD of $V_\ell$. At the end of the ceremony, $\mathsf {EA}$ updates its state and $\mathsf {BB}$ updates the public transcript $\tau$ as necessary.

After voting period ends, the tally phase is a ceremony executed by the $\mathsf {EA}$, the $\mathsf {BB}$ and the trustees $M_i^{T}\in \mathcal {M}^T$, $i=1,\ldots ,k$ as well as their TSDs. Namely, the $\mathsf {EA}$ provides each trustee with the set of cast votes $\mathsf {V}_\mathsf {tally}$. Then, the trustees collectively compute the election result and upon successful termination and update the public transcript $\tau$ in the $\mathsf {BB}$ either directly or via the $\mathsf {EA}$.

The election result can be computed from any party by parsing the election transcript.

The verification algorithm outputs a value in $\{0,1\}$, where $\mathsf {audit}$ is a voter’s individual audit information obtained after the voter’s engagement in the $\mathbf {Cast}$ protocol.

The definition of correctness of an honest execution of $\varvec{\mathcal {VC}}$ is straightforward and is provided in the full version of this paper [33, Definition 1].

2.3 Threat Model for E2E Verifiability

In order to define the threat model for E2E verifiability we need first to determine the adversarial objective. Intuitively, the objective of the adversary is to manipulate the election result without raising suspicion amongst the participating voters. To express this formally, we have to introduce a suitable notation; given that option selections are elements of a set of m choices, we may encode them as m-bit strings, where the bit in the i-th position is 1 if and only if option $P_i$ is selected. Further, we may aggregate the election results as the list with the number of votes each option has received, thus the output of the $\mathbf {Result}$ algorithm is a vector in $\mathbb {Z}_+^m$. In this case, a result is feasible if and only if the sum of any of its coordinates is no greater than the number of voters.

Vote Extractor. Borrowing from [34], in order to express the threat model for E2E verifiability properly, we will ask for a vote extractor algorithm $\mathcal {E}$ (not necessarily efficient, e.g., not running in polynomial-time) that receives as input the election transcript $\tau$ and the set of individual audit information $\{ \alpha _\ell \}_{\ell \in \mathcal {V}_\mathsf {succ}}$, where by $\mathcal {V}_\mathsf {succ}$, we denote the set of honest voters that voted successfully. Given such input, $\mathcal {E}$ will attempt to compute $n-|\mathcal {V}_\mathsf {succ}|$ vectors $\langle \mathcal {U}_\ell \rangle _{V_\ell \in \mathcal {V} \setminus \mathcal {V}_\mathsf {succ}}$ in $\{0,1\}^m$ which correspond to all the voters outside of $\mathcal {V}_\mathsf {succ}$ and can be either a option selection, if the voter has voted adversarially or a zero vector, if the voter has not voted successfully. In case $\mathcal {E}$ is incapable of presenting such selection, the symbol $\bot$ will be returned instead. The purpose of the algorithm $\mathcal {E}$ is to express the requirement that the election transcript $\tau$ that is posted by the EA in the BB at the end of the procedure contains (in potentially encoded form) a set of well-formed actual votes. Using this notion of extractor, we are capable to express the “actual” result encoded in an election transcript despite the fact that the adversary controls some voters. Note when the extractor $\mathcal {E}$ fails it means that $\tau$ is meaningless as an election transcript and thus unverifiable.

Election Result Deviation. Next, we want to define a measure of deviation from the actual election result, as such deviation is the objective of the adversary in an E2E verifiability attack. This will complete the requirements for expressing the adversarial objective in the E2E attack game. To achieve this, it is natural to equip the space of results with a metric. We use the metric derived by the 1-norm, $\Vert \cdot \Vert _1$ scaled to half, i.e., $\mathrm {d}_1:$ $\mathbb {Z}_+^m\times \mathbb {Z}_+^m\longrightarrow \mathbb {R}$ and $\mathrm {d}_1(R,R')=\frac{1}{2}\cdot \sum _{i=1}^m|R_i-R'_i|,$ where $R_i,R'_i$ is the i-th coordinate of $R,R'$ respectively. Intuitively, moving $\delta$ votes from one option to another translates to a distance $\mathrm {d}_1(R,R')$ of exactly $\delta$.

The E2E Verifiability Game. Let $\varvec{\mathcal {D}}=\langle \mathbf {D}_1,\ldots , \mathbf {D}_n, \mathbf {D}^T_1, \ldots , \mathbf {D}^T_k, \mathbf {D}^{\mathsf {CD}} \rangle$ be a vector of distributions that consists of the distributions $\mathbf {D}_1,\ldots ,\mathbf {D}_n$ over the collection of voter transducers $\mathcal {M}^V$, the distributions $\mathbf {D}^T_1, \ldots , \mathbf {D}^T_k$ over the collection of trustee transducers $\mathcal {M}^T$ and the distribution $\mathbf {D}^{\mathsf {CD}}$ over the collection of $\mathsf {CD}$ transducers $\mathcal {M}^{\mathsf {CD}}$. We define the E2E verifiability Ceremony game $G_{\mathrm {E2E}}^{\mathcal {A}, \mathcal {E}, {\varvec{\mathcal {D}}},\delta ,\theta ,\phi }$ between the adversary $\mathcal {A}$ and a challenger $\mathcal {C}$ w.r.t. ${\varvec{\mathcal {D}}}$ and the vote extractor $\mathcal {E}$ which takes as input the security parameter $\lambda$, the number of voters n, the number of options m, and the number of trustees k and is parameterised by (i) the deviation amount, $\delta$, (according to the metric $\mathrm {d}_1(\cdot ,\cdot )$) that the adversary wants to achieve, (ii) the number of honest voters, $\theta$, that terminate the $\mathbf {Cast}$ ceremony successfully and (iii) the number of honest voters, $\phi$, that submit a complaint in case of unsuccessful termination during the $\mathbf {Cast}$ ceremony.

Throughout the game, the adversary fully controls the election by corrupting the $\mathsf {EA}$ and all the trustees $\mathcal {T}=\{T_1,\ldots T_k\}$, while the $\mathsf {CD}$ remains honest during the setup phase. In addition, it corrupts all the voters VSDs and manages the $\mathbf {Cast}$ ceremony executions. For each voter $V_\ell$, the adversary may choose to corrupt $V_\ell$ or to allow the challenger to play on her behalf. Note that the challenger retains the control of the ASD⁴ for honest voters and samples for each honest voter a transducer from the corresponding distribution. If a voter $V_\ell$ is uncorrupted, the adversary provides the option selection that $V_\ell$ should use in the $\mathbf {Cast}$ ceremony; the challenger samples a transducer $M_{i_\ell }\overset{\mathbf {D_\ell }}{\longleftarrow }\mathcal {M}^V$ from voter transducer distribution $\mathbf {D}_\ell$ and then executes the $\mathbf {Cast}$ ceremony according to $M_{i_\ell }$’s description to vote the given option selection and decide whether to audit the election result at the end. The adversary finally posts the election transcript in the $\mathsf {BB}$. The adversary will win the game provided that there are at least $\theta$ of honest voters that terminate the ballot-casting successfully and at most $\phi$ complaining honest voters, but the deviation of the tally is bigger than $\delta$ w.r.t. $\mathrm {d}_1$ or the extractor fails to produce the option election of the dishonest voters. The attack game is specified in detail in Fig. 2.

Definition 1

Let $\epsilon \in [0,1]$ and $n,m,k,\delta ,\theta ,\phi \in \mathbb {N}$ with $\theta ,\phi \le n$. The e-voting ceremony $\varvec{\mathcal {VC}}$ w.r.t. the election function f achieves E2E verifiability with error $\epsilon$, transducer distribution vector ${\varvec{\mathcal {D}}}$, a number of at least $\theta$ honest successful voters, at most $\phi$ honest complaining voters and tally deviation at most d if there exists a (not necessarily polynomial-time) vote extractor $\mathcal {E}$ such that for every PPT adversary $\mathcal {A}$:

$$\begin{aligned} \Pr [G_{\mathrm {E2E}}^{\mathcal {A},\mathcal {E},{\varvec{\mathcal {D}}},\delta ,\theta ,\phi }(1^{\lambda },n,m,k)=1] \le \epsilon . \end{aligned}$$

Remark 1

(Universal voter distribution). In some e-voting systems, the voters can be uniquely identified during the $\mathbf {Cast}$ ceremonies, e.g. the voter’s real ID is used. Hence, the adversary is able to identify each voter $V_\ell$ and learn its profile expressed by $\mathbf {D}_\ell$. Then, the adversary may choose the best attack strategy depending on $\mathbf {D}_\ell$. Nevertheless, in case the credentials are randomly and anonymously assigned to the voters by the CD, the adversary will not be able to profile voters given his view in the ballot-casting ceremony (recall that in the E2E game the $\mathsf {CD}$ remains honest). Therefore, it is possible to unify the distributions to a universal voter distribution, denoted as $\mathbf {D}$, which reflects the profile of the “average voter.” Specifically, in this case, we will have $\mathbf {D}_1 = \cdots = \mathbf {D}_n= \mathbf {D}$.

Fig. 2.

The E2E verifiability ceremony game between the challenger $\mathcal {C}$ and the adversary $\mathcal {A}$ w.r.t. the vote extractor $\mathcal {E}$ and the vector of transducer distributions ${\varvec{\mathcal {D}}}=\langle \mathbf {D}_1,\ldots , \mathbf {D}_n, \mathbf {D}^T_1, \ldots , \mathbf {D}^T_k, \mathbf {D}^{\mathsf {CD}} \rangle$.

2.4 Threat Model for Voter Privacy

The threat model of privacy concerns the actions that may be taken by the adversary to figure out the choices of the honest voters. We specify the goal of the adversary in a very general way. In particular, for an attack against privacy to succeed, we ask that there is an election result, for which the adversary is capable of distinguishing how people vote while it has access to (i) the actual individual audit information that the voters obtain after ballot-casting as well as (ii) a set of ceremony views that are consistent with all the honest voters’ views in the $\mathbf {Cast}$ ceremony instances they participate.

Observe that any system that is secure against such a threat scenario possesses also “passive coercion resistance”, i.e., voters cannot prove how they voted by showing the individual audit information ceremony or even presenting the view they obtain from the $\mathbf {Cast}$. Given that in the threat model we allow the adversary to observe the view of the voter in the $\mathbf {Cast}$ ceremony, we need to allow the voter to be able to lie about her view (otherwise an attack could be trivially mounted). We stress that the simulated view of the voter in the $\mathbf {Cast}$ ceremony does not contain the view of the internals of the VSD. This means that, with respect to privacy, the adversary may not look into the internals of the VSD for the honest voters. The above is consistent, for instance, with the scenario that the voter can give to the VSD her option choice to be encoded. While the adversary will be allowed to observe a simulated view of the voter during the $\mathbf {Cast}$ ceremony, it will be denied access to the internals of the VSD during the $\mathbf {Cast}$ execution. This increases the opportunities where the voter can lie about how she executes the $\mathbf {Cast}$ ceremony.

The Voter Privacy Game. Following the same logic as in the E2E Verifiability game, we specify a vector of transducer distributions over the collection of voter transducers $\mathcal {M}^V$, trustee transducers $\mathcal {M}^T$ and $\mathsf {CD}$ transducers $\mathcal {M}^\mathrm {CD}$ denoted by $\mathcal {D}=\langle \mathbf {D}_1,\ldots , \mathbf {D}_n,\mathbf {D}^T_1, \ldots , \mathbf {D}^T_k, \mathbf {D}^\mathrm {CD} \rangle$. We then express the threat model as a Voter Privacy game, denoted by $G_{t\text{- }\mathrm {priv}}^{\mathcal {A},\mathcal {S}, \mathcal {D}}$, that is played between an adversary $\mathcal {A}$ and a challenger $\mathcal {C}$, that takes as input the security parameter $\lambda$, the number of voters n, the number of options m, and the number of trustees k as described in Fig. 3 and returns 1 or 0 depending on whether the adversary wins. An important feature of the voter privacy game is the existence of an efficient simulator $\mathcal {S}$ that provides a simulated view of the voter in the $\mathbf {Cast}$ ceremony. Note that the simulator is not responsible to provide the view of the voter’s supporting device (VSD). Intuitively, this simulator captures the way the voter can lie about her choice in the $\mathbf {Cast}$ ceremony in case she is coerced to present her view after she completes the ballot-casting procedure.

The attack game is parameterised by t, v. The adversary starts by selecting the voter, option and trustee identities for given parameters n, m, k and determines the allowed ways to vote. The challenger subsequently flips a coin b (that will change its behaviour during the course of the game) and will perform the $\mathbf {Setup}$ ceremony with the adversary playing the role of the $\mathsf {EA}$, the $\mathsf {CD}$ and up to t trustees along with their associated TSDs and ASDs.

Fig. 3.

The voter privacy game between the challenger $\mathcal {C}$ and the adversary $\mathcal {A}$ w.r.t. the view simulator $\mathcal {S}$ and the vector of transducer distributions ${\varvec{\mathcal {D}}}=\langle \mathbf {D}_1,\ldots , \mathbf {D}_n, \mathbf {D}^T_1, \ldots , \mathbf {D}^T_k, \mathbf {D}^{\mathsf {CD}} \rangle$.

The honest trustees’ behaviours will be determined by transducers selected at random by the challenger from $\mathcal {M}^T$ according to the corresponding distribution. Subsequently, the adversary will schedule all $\mathbf {Cast}$ ceremonies selecting which voters it prefers to corrupt and which ones it prefers to allow to vote honestly. The adversary is allowed to corrupt at most v voters and their VSDs. In addition, $\mathcal {A}$ is allowed to corrupt the ASDs of all voters. The voters that remain uncorrupted are operated by the challenger and they are given two option selections to vote. For each uncorrupted voter $V_\ell$, the challenger first samples a transducer $M_{i_\ell }\leftarrow \mathbf {D_\ell }$ and then executes the $\mathbf {Cast}$ ceremony according to $M_{i_\ell }$’s description to vote one of its two option selections based on b.

The adversary will also receive the individual audit information that is obtained by each voter as well as either (i) the actual view (if $b=0$) or (ii) a simulated view, generated by $\mathcal {S}$ (if $b=1$), of each voter during the $\mathbf {Cast}$ ceremony (this addresses the individual audit information-freeness aspect of the attack game). Upon completion of ballot-casting, the adversary will execute with the challenger the $\mathbf {Tally}$ ceremony and subsequently the adversary will attempt to guess b. The attack is successful provided that the election result is the same with respect to the two alternatives provided for each honest voter by the adversary and the adversary manages to guess the challenger’s bit b correctly. The game is presented in detail in Fig. 3.

Definition 2

Let $m,n,k,t,v\in \mathbb {N}$ with $t\le k$ and $v\le n$. Let $\varvec{\mathcal {VC}}$ be an e-voting ceremony with m options, n voters and k trustees w.r.t. the evaluation election unction f. We say that $\varvec{\mathcal {VC}}$ achieves voter privacy with error $\epsilon$ for transducer distribution vector ${\varvec{\mathcal {D}}}$, at most t corrupted trustees and v corrupted voters, if there is an efficient simulator $\mathcal {S}$ such that for any PPT adversary $\mathcal {A}$:

$$\begin{aligned} \left| \Pr [G_{\mathrm {priv}}^{\mathcal {A},\mathcal {S},{\varvec{\mathcal {D}}},t,v}(1^{\lambda },n,m,k)=1] - \frac{1}{2} \right| \le \epsilon \;, \end{aligned}$$

Threat Model Alternatives. The framework presented in this section is a first attempt to model human behaviour in the cryptographic e-voting analysis, therefore various approaches or extensions could be considered. In the full version of this paper [33, Sect. 2.5], we discuss on some selected possible alternatives on this subject.

3 Syntax of Helios Ceremony

In this section, we present a formal description of Helios ceremony according to the syntax provided in Subsect. 2.2. For simplicity, we consider the case of 1-out-of-m elections, where the set of allowed selections $\mathcal {U}$ is the collection of singletons, $\left\{ \{\mathsf {opt}_1\},\ldots ,\{\mathsf {opt}_m\}\right\}$, from the set of options $\mathcal {O}$. Our syntax does not reflect the current implemented version of Helios, as it adapts necessary minimum modifications to make Helios secure. For instance, we ensure that each voter is given a unique identifier to prevent Helios from the clash attacks introduced in [39]. In addition, we consider a hash function $H(\cdot )$ that all parties have oracle access to, used for committing to election information and ballot generation, as well as the Fiat-Shamir transformations [24] in the NIZK proofs that the system requires. As we state below, in the generation of the NIZK proofs for ballot correctness, the unique identifier is included in the hash to prevent replaying attacks presented in [17]. Moreover, we apply strong Fiat-Shamir transformations, where the statement of the NIZK should also be included in the hash. As shown in [8], strong Fiat-Shamir based NIZKs are simulation sound extractable, while weak Fiat-Shamir based NIZKs make the Helios vulnerable.

Finally, we stress that we model trustees’ behaviour by considering the event that the trustee will or will not the verify the correct posting of its partial public key. This is done so that we capture the possible privacy vulnerability in Helios’s implementation architecure studied in [35]; that is, in the case where no honest trustee performs such verification then a malicious $\mathsf {EA}$ may act as man-in-the-middle and replace the trustees’ partial public keys with ones it adversarially generates, thus resulting to a total break of voters’ privacy.

The Helios’s transducers: We define the collections of transducers $\mathcal {M}^V,\mathcal {M}^T, \mathcal {M}^{\mathsf {CD}}$ that reflect the admissible behaviours of voters, trustees and $\mathsf {CD}$ respectively.

The set of admissible voter transducers is denoted by $\mathcal {M}^V:=\left\{ M_{i,c,a}\right\} ^{c,a\in \left\{ 0,1\right\} }_{i\in [0,q]}$, where $q\in \mathbb {N}$; The transducer $M_{i,c,a}$ audits the ballot created by the VSD exactly i times (using its ASD) and then submits the $(i+1)$-th ballot created by the VSD; Upon successful termination, it outputs a individual audit information $\mathsf {audit}$ obtained from the VSD; If the termination is not successful and $c=1$, $M_{i,c,a}$ outputs a special symbol ‘$\mathsf {Complain}$’ to complain about its failed engagement in the $\mathbf {Cast}$ ceremony. In any case of termination, when $a=1$, $M_{i,c,a}$ also outputs a special symbol ‘$\mathsf {Audit}$’ and sends $\mathsf {audit}$ to the ASD. To guarantee termination, we limit the maximum number of ballot audits by threshold q.

The admissible trustee transducers are two and labelled as $M^T_0,M^T_1$ (so that $\mathcal {M}^T = \left\{ M^T_0,M^T_1\right\}$). At a high level, both $M^T_0$ and $M^T_1$ will utilise the TSD to generate a partial public/secret key pair in the $\mathbf {Setup}$ ceremony. However, only $M^T_1$ will verify the correct posting of its partial public key in the $\mathsf {BB}$, whereas $M^T_0$ will have no other interaction with the election.

The $\mathsf {CD}$ is required to check the validity of the credentials $\mathsf {cr}_1,\ldots ,\mathsf {cr}_n$ generated by the potentially malicious $\mathsf {EA}$ before distributing them. In Helios, we define the credential $\mathsf {cr}_i:=(\mathrm {ID}_i,t_i)$, where $\mathrm {ID}_i$ is a unique voter identity and $t_i$ is an authentication token. The credential distributor first checks for all $i,j\in [n]$: if $i\ne j$ then $\mathrm {ID}_i \ne \mathrm {ID}_j$, and halts if the verification fails. Upon success, it randomly sends each voter $V_\ell$ a credential though some human channels. Hence, we define the set of $\mathsf {CD}$ transducers as $\mathcal {M}^{\mathsf {CD}}:=\left\{ M^{{\mathsf {CD}}}_\sigma \right\} _{\sigma \in S_n}$, where $S_n$ stands for all possible permutations $[n]\mapsto [n]$.

We define the Helios ceremony quintuple $\langle \mathbf {Setup}, \mathbf {Cast}, \mathbf {Tally},$ $\mathbf {Result},\mathbf {Verify}\rangle$, using the hash function $H(\cdot )$ as follows:

Each trustee transducer $M^{T_i}_{b_i}\in \left\{ M^T_0,M^T_1\right\}$, $i=1,\ldots ,k$ sends signal to its TSD. The TSD generates a pair of threshold ElGamal partial keys $( \mathsf {pk}_i,\mathsf {sk}_i)$ and sends $\mathsf {pk}_i$ together with a Schnorr (strong Fiat-Shamir) NIZK proof of knowledge of $\mathsf {sk}_i$ to the $\mathsf {EA}$. In addition, the TSD returns a trustee secret $\bar{s}_i:= (H(\mathsf {pk}_i),\mathsf {sk}_i)$ to $M^{T_i}_{b_i}$. If there is a proof that $\mathsf {EA}$ does not verify, then $\mathsf {EA}$ aborts the protocol. Next, $\mathsf {EA}$ computes the election public key $\mathsf {pk}= \prod _{i\in [k]}\mathsf {pk}_i$. The public parameters, $\mathsf {info}$, which include $\mathsf {pk}$ and the partial public keys $\mathsf {pk}_1,\ldots ,\mathsf {pk}_k$ as well as the related NIZK proofs of knowledge are posted in the $\mathsf {BB}$ by the $\mathsf {EA}$.

Trustee Auditing Step [35]: for $i=1,\ldots ,k$, if $b_i=1$, then $M^{T_i}_{b_i}$ sends $H(\mathsf {pk}_i)$ to its ASD, and the ASD will fetch $\mathsf {info}$ from the BB to verify if there exists a partial public key $\mathsf {pk}_*$ such that its hash matches $H(\mathsf {pk}_i)$. In case this verification fails, $T_i$ sends a message ‘Invalid public key’ to all the voters via the human communication channels shown in Fig. 1.

Finally, the $\mathsf {EA}$ generates the voter credentials $\mathsf {cr}_1,\ldots ,\mathsf {cr}_n$, where $\mathsf {cr}_i:=(\mathrm {ID}_i,t_i)$, and $t_i$ is a random authentication code. Then, forwards the credentials to the CD transducer $M^{{\mathsf {CD}}}$. The CD transducer $M^{{\mathsf {CD}}}_\sigma$ checks the uniqueness of each $\mathrm {ID}_i$ and distributes them to the voter transducers $M_{i_\ell ,c_\ell ,a_\ell }$ for $\ell \in [n]$, according to the permutation $\sigma$ over [n] that specifies its behaviour.

For each voter $V_\ell$, the corresponding transducer $M_{i_\ell ,c_\ell ,a_\ell }$ has a pre-defined number of $i_\ell$ ballot auditing steps, where $i_\ell \in [0,q]$. The input of $M_{i_\ell ,c_\ell ,a_\ell }$ is $(\mathsf {cr}_\ell ,\mathcal {U}_\ell )$. If $V_\ell$ has received an ‘Invalid public key’ from at least one trustee, then it aborts the ceremony. If no such message was sent, then for $u\in [i_\ell ]$, the following steps are executed:

• 1. $M_{i_\ell ,c_\ell ,a_\ell }$ sends $(\mathrm {ID}_\ell ,\mathcal {U}_\ell )$ to its VSD, labelled as $\mathsf {VSD}_\ell$. Let $\mathsf {opt}_{j_\ell }$ be the option selection of $V_\ell$, i.e. $\mathcal {U}_\ell =\{\mathsf {opt}_{j_\ell }\}$.

• 2. For $j=1,\ldots ,m$, $\mathsf {VSD}_\ell$ creates a ciphertext, $C_{\ell ,j}$, that is a lifted ElGamal encryption under $\mathsf {pk}$ of 1, if $j=j_\ell$ (the selected option position), or 0 otherwise. In addition, it attaches a NIZK proof $\pi _{\ell ,j}$ showing that $C_{\ell ,j}$ is an encryption of 1 or 0. Finally, an overall NIZK proof $\pi _\ell$ is generated, showing that exactly one of these ciphertexts is an encryption of 1. These proofs are strong Fiat-Shamir transformations of disjunctive Chaum-Pedersen (CP) proofs [13]. To generate the CP proofs, the unique identifier $\mathrm {ID}_\ell$ is included in the hash. The ballot generated is $\psi _{\ell ,u}=\langle \psi _{\ell ,u}^0,\psi _{\ell ,u}^1\rangle$, where $\psi ^0_{\ell ,u}=\big \langle (C_{\ell ,1},\pi _{\ell ,1}),\ldots ,(C_{\ell ,m},\pi _{\ell ,m}),\pi _\ell \big \rangle$ and $\psi _{\ell ,u}^1=H(\psi _{\ell ,u}^0)$. The VSD responds to $M_{i_\ell ,c_\ell ,a_\ell }$ with the ballot $\psi _{\ell ,u}$.

• 3. Then, $M_{i_\ell ,c_\ell ,a_\ell }$ sends a Benaloh audit request to $\mathsf {VSD}_\ell$. In turn, $\mathsf {VSD}_\ell$ returns the randomness $r_{\ell ,u}$ that was used to create the ballot $\psi _{\ell ,u}$. The $M_{i_\ell ,c_\ell ,a_\ell }$ sends $(\mathrm {ID}_\ell ,\psi _{\ell ,u}, r_{\ell ,u})$ to its ASD, which will audit the validity of the ballot. If the verification fails, $M_{i_\ell ,c_\ell ,a_\ell }$ halts. If the latter happens and $c_\ell =1$, $M_{i_\ell ,c_\ell ,a_\ell }$ outputs a special symbol ‘$\mathsf {Complain}$’, otherwise it returns no output.

After the $i_\ell$-th successfully Benaloh audit, $M_{i_\ell ,c_\ell ,a_\ell }$ invokes $\mathsf {VSD}_\ell$ to produce a new ballot $\psi _{\ell }$ as described in step 2 above; however, upon receiving $\psi _{\ell }$, $M_{i_\ell ,c_\ell ,a_\ell }$ now sends $\mathsf {cr}_\ell$ to $\mathsf {VSD}_\ell$, indicating it to submit the ballot to the $\mathsf {EA}$. The $M_{i_\ell ,c_\ell ,a_\ell }$ then outputs $\mathsf {audit}_\ell :=(\mathrm {ID}_\ell ,\psi _{\ell }^1)$. If $a_\ell =1$, $M_{i_\ell ,c_\ell ,a_\ell }$ also outputs a special symbol ‘$\mathsf {Audit}$’ which indicates that it will send $\mathsf {audit}_\ell$ to $\mathsf {ASD}_\ell$ which will audit the $\mathsf {BB}$ afterwards, as specified in the $\mathbf {Verify}$ algorithm below.

When $\mathsf {EA}$ receives a cast vote $(\mathsf {cr}_\ell ,\psi _{\ell })$ from $\mathsf {VSD}_\ell$, it checks the validity of the credential $\mathsf {cr}_\ell$ and that $\psi _\ell$ is a well-formed ballot by verifying the NIZK proofs. If the check fails, then it aborts the protocol. After voting ends, $\mathsf {EA}$ updates its state with the pairs $\left\{ (\psi _{\ell },\mathrm {ID}_\ell )\right\} _{V_\ell \in \mathcal {V}_\mathsf {succ}}$ of cast votes and the associated identifiers, where $\mathcal {V}_\mathsf {succ}$ is the set of voters that voted successfully.

In the $\mathbf {Tally}$ ceremony, $\mathsf {EA}$ sends $\left\{ \psi _{\ell }\right\} _{V_\ell \in \mathcal {V}_\mathsf {succ}}$ to all trustee transducers $M^{T_i}_{b_i}$’s TSD, $i=1,\ldots ,k$. Next, the TSD of each $M^{T_i}_{b_i}$, $i=1,\ldots ,k$, performs the following computation: it constructs the product ciphertext $\mathbf {C}_j=\prod _{V_\ell \in \mathcal {V}_\mathsf {succ}}C_{\ell ,j}$ for $j=1,\ldots ,m$. By the additive homomorphic property of (lifted) ElGamal, each $\mathbf {C}_j$ is a valid encryption of the number of votes that the option $\mathsf {opt}_j$ received. Then, the TSD uses $\mathsf {sk}_i$ to produce the partial decryption of all $C_j$, denoted by $x^i_j$, and sends it to the $\mathsf {EA}$ along with NIZK proofs of correct partial decryption. The latter are Fiat-Shamir transformations of CP proofs. If there is a proof that $\mathsf {EA}$ does not verify, then it aborts the protocol. After all trustees finish their computation, $\mathsf {EA}$ updates $\tau$ with $\left\{ (x^i_1,\ldots ,x^i_m)\right\} _{i\in [k]}$ and the NIZK proofs.

For each option $\mathsf {opt}_j$, the $\mathbf {Result}$ algorithm computes the number of votes, $x_j$, that $\mathsf {opt}_j$ has received using the partial decryptions $x^1_j,\ldots ,x^k_j$. The output of the algorithm is the vector $\langle x_1, \ldots ,x_m\rangle$.

The algorithm $\mathbf {Verify}(\tau ,\mathsf {audit}_\ell )$ outputs 1 if the following conditions hold:

• 1. The structure of $\tau$ and all election information is correct (using $\mathsf {info}$).

• 2. There exists a ballot in $\tau$, indexed by $\mathrm {ID}_\ell$, that contains the hash value $\psi ^1_\ell$.

• 3. The NIZK proofs for the correctness of all ballots in $\tau$ verify.

• 4. The NIZK proofs for the correctness of all trustees’ partial decryptions verify.

• 5. For $j=1,\ldots ,m$, $x_j$ is a decryption of $\mathbf {C}'_j$, where $\mathbf {C}'_j$ is the homomorphic ciphertext created by multiplying the respective ciphertexts in the ballots published on the BB (in an honest execution, $\mathbf {C}'_j$ should be equal to $\mathbf {C}_j$).

4 E2E Verifiability of Helios E-Voting Ceremony

In a Helios e-voting ceremony, an auditor can check the correct construction of the ballots and the valid decryption of the homomorphic tally by verifying the NIZK proofs. In our analysis, it is sufficient to require that all NIZK proofs have negligible soundness error $\epsilon (\cdot )$ in the RO model. Note that in Sect. 3, we explicitly modify Helios to associate ballots with the voters’ identities, otherwise a clash attack [39] would break verifiability. For simplicity in presentation, we assume that the identifiers are created by the adversary, i.e. the set $\left\{ \mathrm {ID}_\ell \right\} _{\ell \in [n]}$ matches the set of voters $\mathcal {V}$.

Throughout our analysis, we assume the honesty of the $\mathsf {CD}$ and thus the distribution of the credentials is considered to be an arbitrary permutation over [n]. Since there are only two admissible trustee transducers $M^T_0,M^T_1$, the distribution of trustee transducers $\mathbf {D}^T_p$ is set as the p-biased coin-flip below:

$$\begin{aligned} \underset{\mathbf {D}^T_p}{\Pr }[M] = \left\{ \begin{array}{cl} p, &{} \text{ if } M=M^T_1 \\ 1-p, &{} \text{ if } M= M^T_0 \end{array} \right. \end{aligned}$$

(1)

Moreover, in the $\mathbf {Cast}$ ceremony, the ballots and individual audit information are produced before the voters show their credentials to the system. Since the $\mathsf {CD}$ is honest, the adversary is oblivious the the maps between the credentials to the voter transducers. The credentials are only required when the voters want to submit their ballots, hence, according to the discussion in Remark 1, we will consider only a universal voter transducer distribution $\mathbf {D}$ in the case study of Helios. Namely, $\mathbf {D}_1 = \cdots = \mathbf {D}_n= \mathbf {D}$.

4.1 Attacks on Verifiability

As mentioned earlier, we have modified Helios to prevent the system from clash attacks [39]. For simplicity, we exclude all the trivial attacks that the adversary may follow, i.e. the ones that will be detected with certainty (e.g. malformed or unreadable voting interface and public information). Therefore, the meaningful (non-trivial) types of attack that an adversary may launch are the following:

$\blacksquare$ Collision attack: the adversary computes two votes which hash to the same value. The collision resistance of the hash function $H(\cdot )$, prevents from these attacks except from some negligible probability $\epsilon '$ ⁵.

$\blacksquare$ Invalid vote attack: the adversary creates a vote for some invalid plaintext, i.e. a vector that does not encode a candidate selection (e.g., multiple votes for some specific candidate). This attack can be prevented by the soundness of the NIZK proofs, except from the negligible soundness error $\epsilon$. The NIZK verification is done via the voter’s ASD.

$\blacksquare$ VSD attack: the adversary creates a vote which is valid, but corresponds to different selection than the one that the voter intended. A Benaloh audit at the $\mathbf {Cast}$ ceremony step can detect such an attack with certainty, as the randomness provided by the VSD perfectly binds the plaintext with the audited ElGamal ciphertext.

$\blacksquare$ Replacement attack: the adversary deletes/inserts an honest vote from/to the $\mathsf {BB}$, or replaces it with some other vote of its choice, after voting has ended. Assuming no hash collisions, any such modification will be detected if the voter chooses to audit the $\mathsf {BB}$ via her ASD.

$\blacksquare$ Invalid tally decryption attack: the adversary provides a decryption which is not the plaintext that the homomorphic tally vector encrypts. The NIZK proofs of correct decryption prevent this attack, except for a negligible soundness error $\epsilon$.

Remark 2

(Completeness of the attack list). It can be easily shown that the above list exhausts all possible non-trivial attack strategies against Helios in our threat model. Namely, in an environment with no clash, collision and invalid encryption attacks, the set of votes is in the correct (yet unknown) one-to-one correspondence with the set of voters, and all votes reflect a valid candidate selection of the unique corresponding voter. As a result, a suitably designed vote extractor will decrypt (in super-polynomial time) and output the actual votes from the non-honest-and-successful voters, up to permutation. Consequently, if no honest vote has been modified during and after voting, and the homomorphic tally of the votes is correctly computed and decrypted, then the perfect binding of the plaintexts and ciphertexts of ElGamal implies that the decryption of the tally matches the intended election result.

4.2 Attacking the Verifiability of Helios E-Voting Ceremony

As explained in the previous subsection, any attempt of collision, invalid vote and invalid tally decryption attacks has negligible probability of success for the adversary due to the collision resistance of the hash function and the soundness of the ZK proofs. Therefore, in a setting where no clash attacks are possible, the adversary’s chances to break verifiability rely on combinations of VSD and Replacement attacks. The probability of these attacks being detected depends on the voter transducer distribution $\mathbf {D}$ which expresses their auditing behaviour during and after voting. In the following theorem, we prove that the verifiability of Helios is susceptible to VSD or/and Replacement attacks, when the voters sample from a class of assailable voter transducer distributions.

Theorem 1

( Vulnerability of Helios ceremony ). Assume an election run of Helios with n voters, m candidates and k trustees. Let $q,\delta ,\theta ,\phi \in \mathbb {N}$, where $0<\theta ,\phi \le n$ and q is the maximum number of Benaloh audits. Let $\mathbf {D}$ be a (universal) voter transducer distribution s.t. for some $\kappa _1,\kappa _2,\kappa _3,\mu _1,\mu _2\in [0,1)$ at least one of the two following conditions holds:

• (i) There is an $i^*\in \{0,\ldots ,q\}$ that determines “vulnerable VSD auditing behaviour”. Namely, (i.a) the probability that a voter executes at least $i^*$ Benaloh audits is $1-\kappa _1$ AND (i.b) the probability that a voter, given that she has executed at least $i^*$ Benaloh audits, will cast her vote after exactly $i^*$ Benaloh audits is $1-\kappa _2$ AND (i.c) the probability that a voter, given that she will execute exactly $i^*$ Benaloh audits, will not complain in case of unsuccessful audit is $\kappa _3$.

• (ii) There is a subset $\mathcal {J}^*\subseteq \{0,\ldots ,q\}$ that determines “vulnerable BB auditing behaviour”. Namely, (ii.a) the probability that a voter executes j Benaloh audits for some $j\in \mathcal {J}^*$ is $1-\mu _1$ AND (ii.b) for every $j\in \mathcal {J}^*$, the probability that a voter, given she has executed j Benaloh audits, will not audit the BB is at least $1-\mu _2$.

Let ${\varvec{\mathcal {D}}}=\big \langle \mathbf {D},\ldots , \mathbf {D}, \mathbf {D}^{T_1}, \ldots , \mathbf {D}^{T_k}, \mathbf {D}^{\mathsf {CD}} \big \rangle$ be a transducer distribution vector where $\mathbf {D}^{T_i}=\mathbf {D}^T_{p_i}$, $i=1,\ldots , k$, is the $p_i$-biased coin-flip trustee transducer distribution in Eq. (1) for arbitrary $p_i\in [0,1]$ and $\mathbf {D}^{\mathsf {CD}}$ is an arbitrary $\mathsf {CD}$ transducer distribution. Then, there is a PPT adversary $\mathcal {A}$ that wins the E2E verifiability ceremony game $G_{\mathrm {E2E}}^{\mathcal {A},\mathcal {E},{\varvec{\mathcal {D}}},\delta ,\theta ,\phi }(1^{\lambda },n,m,k)$ in Fig. 2 for any vote extractor $\mathcal {E}$, any $\varDelta \in [0,1)$ as follows:

• under condition (i), provided the parameters $\delta ,\theta ,\phi$ satisfy:

  

  with probability of success at least where $\beta _1=(1-\varDelta )(1-\kappa _1)n \text{ and } \beta _2=(\kappa _2-\varDelta +\varDelta \kappa _2)(1-\kappa _2)$.

• under condition (ii), provided the parameter $\delta$ satisfies $\delta \le (1-\varDelta )(1-\mu _1)n$ with probability of success at least .

Proof

We prove the Theorem in the full version [33, Theorem 1].

4.3 End-to-End Verifiability Theorem Helios E-Voting Ceremony

In this subsection, we prove the E2E verifiability of Helios e-voting ceremony in the RO model, when the voter transducer distribution satisfies two conditions. As we will explain at length in the next subsection, these conditions are logically complementary to the ones stated in Theorem 1, as long as the complaining behaviour of the voters is balanced (i.e. the voters have 1/2 probability of complaining in case of unsuccessful termination).

Theorem 2

( Verifiability of Helios ceremony ). Assume an election run of Helios with n voters, m candidates and k trustees. Assume that the hash function $H(\cdot )$ considered in Sect. 3 is a random oracle. Let $q,\delta ,\theta ,\phi \in \mathbb {N}$, where $0<\theta ,\phi \le n$ and q is the maximum number of Benaloh audits. Let $\mathbf {D}$ be a (universal) transducer distribution and some $\kappa _1,\kappa _2,\kappa _3,\mu _1,\mu _2\in [0,1)$ s.t. the two following conditions hold:

• (i) There is an $i^*\in \{0,\ldots ,q+1\}$ that guarantees “resistance against VSD attacks”. Namely, (i.a) the probability that a voter executes at least $i^*$ Benaloh audits is $\kappa _1$ and (i.b) for every $i\in \{0,\ldots ,q\}$, if $i< i^*$, then the probability that a voter, given that she will execute at least i Benaloh audits, will cast her vote after exactly i Benaloh audits, is no more than $\kappa _2$ AND the probability that a voter, given that she will execute exactly i Benaloh audits, will complain in case of unsuccessful audit is at least $1-\kappa _3$.

• (ii) There is a subset $\mathcal {J}^*\subseteq \{0,\ldots ,q\}$ that guarantees “resistance against Replacement attacks”. Namely, (ii.a) the probability that a voter executes j Benaloh audits for some $j\in \mathcal {J}^*$ is $1-\mu _1$ AND (ii.b) for every $j\in \mathcal {J}^*$, the probability that a voter, given she has executed j Benaloh audits, will audit the BB is at least $1-\mu _2$.

Let ${\varvec{\mathcal {D}}}=\big \langle \mathbf {D},\ldots , \mathbf {D}, \mathbf {D}^{T_1}, \ldots , \mathbf {D}^{T_k}, \mathbf {D}^{\mathsf {CD}} \big \rangle$ be a transducer distribution vector where $\mathbf {D}^{T_i}=\mathbf {D}^T_{p_i}$, $i=1,\ldots , k$, is the $p_i$-biased coin-flip trustee transducer distribution in Eq. (1) for arbitrary $p_i\in [0,1]$ and $\mathbf {D}^{\mathsf {CD}}$ is an arbitrary $\mathsf {CD}$ transducer distribution. Then, for any $\varDelta \in [0,1)$ for any $\delta ,\theta$, and under the constraint

$$\begin{aligned} \phi \le (1-\varDelta )(1-\kappa _3)\Big (\frac{1}{(1+\varDelta )\kappa _2}-1\Big )\Big (\frac{\delta }{2}-(1+\varDelta )\kappa _1n\Big )\;, \end{aligned}$$

the Helios e-voting ceremony achieves E2E verifiability for ${\varvec{\mathcal {D}}}$, a number of $\theta$ honest successful voters, a number of $\phi$ honest complaining voters and tally deviation $\delta$ with error

$$\begin{aligned} {\begin{matrix} \quad &{}e^{-\mathrm {min}\big \{\kappa _1n\frac{\varDelta ^2}{3}\;,\;\mu _1n\frac{\varDelta ^2}{3} \;,\; \gamma (\frac{\delta }{2}-(1+\varDelta )\kappa _1n)\frac{\varDelta ^2}{3} \;,\; \mathsf {ln}\big (\frac{1}{\mu _2}\big )(\frac{\delta }{2}-(1+\varDelta )\mu _1n)\big \}} +\\ &{}\quad \quad \quad +(\mu _1+\mu _2-\mu _1\mu _2)^\theta +\mathsf {negl}(\lambda )\;, \end{matrix}} \end{aligned}$$

where $\gamma =\mathrm {min}\left\{ \kappa _2\;,\frac{3}{2}(1-\kappa _3)\big (\frac{1}{(1+\varDelta )\kappa _2}-1\big )\right\} \;.$

Proof

We prove the Theorem in the full version [33, Theorem 2].

4.4 Illustrating Theorems 1 and 2

In order to provide intuition, we provide examples of assailable and resistant voter transducer distributions, in the full version [33, Subsects. 4.2.1 and 4.3.1]. For every case, we illustrate our analysis via comprehensive graphs. Among other remarks, we study the role of $\varDelta$ as trade off factor between (a) optimising the bounds stated in Theorems 1 and 2, and (b) the corresponding “effectiveness zone” determined by the parameters $\delta ,\theta ,\phi$ (normalised by the electorate size n).

4.5 On the tightness of the conditions of Theorems 1 and 2

The conditions stated in Theorems 1 and 2 determine two classes of voter transducer distributions that correspond to vulnerable and insusceptible settings, respectively. We observe that weakening the condition (i) of Theorem 1 (resp. (i) of Theorem 2) cannot imply vulnerability (resp. security). Namely, in condition (i) of Theorem 1, if one of (1.a), (1.b) or (1.c) does not hold, then the adversary cannot be certain that it will achieve a sufficiently large deviation from VSD attacks without increasing rapidly the number of complaints. On the other hand, if condition (i.a) of Theorem 2 does not hold, then E2E verifiability cannot be preserved when (1.b) becomes a disjunction, since a high complaint rate alone is meaningless if the adversary has high success rate of VSD attacks.

Consequently, it is not possible to achieve logical (i.e. probability thresholds are considered either sufficiently high or sufficiently low) tightness for interesting sets of parameters $\delta ,\theta ,\phi$ only by negating the conditions of each of the two theorems. However, this is possible if we assume that the voter’s complaining behaviour is balanced by setting $\kappa _3=1-\kappa _3=1/2$. Namely, the voters flip coins in order to decide whether they will complain in case of unsuccessful termination. Given that $\kappa _3=1/2$ is a “neutral” value, we have that

The above statement is argued in detail in the full version [33, Subsect. 4.4].

5 Voter Privacy of Helios E-Voting Ceremony

In this section, we prove the voter privacy of the Helios e-voting ceremony. The proof is carried out via a reduction. Namely, we show that unless no honest trustee verifies the correct posting of their public data, if there exists a PPT adversary $\mathcal {A}$ that wins the voter privacy/PCR game for Helios with non-negligible distinguishing advantage, then there exists a PPT adversary $\mathcal {B}$ that breaks the IND-CPA security of the ElGamal encryption scheme with blackbox access to $\mathcal {A}$. Throughout the proof, we view $H(\cdot )$ as a RO.

Theorem 3

( Voter Privacy of Helios ceremony ). Assume an election run of Helios with n voters, m candidates and k trustees. Assume that the hash function $H(\cdot )$ considered in Sect. 3 is a random oracle and the underlying ElGamal encryption scheme is IND-CPA secure. Let $t,v\in \mathbb {N}$, where $t<k$ and $v<n$.

Let ${\varvec{\mathcal {D}}}=\big \langle \mathbf {D},\ldots , \mathbf {D}, \mathbf {D}^{T_1}, \ldots , \mathbf {D}^{T_k}, \mathbf {D}^{\mathsf {CD}} \big \rangle$ be a transducer distribution vector where $\mathbf {D}^{T_i}=\mathbf {D}^T_{p_i}$, $i=1,\ldots , k$, is the $p_i$-biased coin-flip trustee transducer distribution in Eq. (1) for arbitrary $p_i\in [0,1]$ and $\mathbf {D}^{\mathsf {CD}}$ is an arbitrary $\mathsf {CD}$ transducer distribution.

Assume that $p_1,\ldots ,p_k$ are sorted in increasing order as $p_{i_1}\le \cdots \le p_{i_k}$. Then, Helios e-voting ceremony achieves voter privacy for ${\varvec{\mathcal {D}}}$, at most t corrupted trustees and v corrupted voters with error

$$\begin{aligned} \frac{1}{2}\cdot \prod _{x=1}^{k-t}(1-p_{i_x})+\mathsf {negl}(\lambda )\;. \end{aligned}$$

Proof

We prove the Theorem in the full version [33, Theorem 3].

6 Evaluating the E2E Verifiability of an E-Voting Ceremony

In this section, we evaluate our results for the E2E verifiability of Helios, by instantiating the bounds in Theorems 1 and 2 for various voter transducer distributions. Our evaluations are separated into two categories: (i) evaluations that are based on actual human data that derive from elections using Helios and (ii) evaluations that are based on simulated data for various sets of parameters.

6.1 Evaluations Based on Human Data

Our human data are sampled from two independent surveys: the first sample is from the member elections of the Board of Directors of the International Association for Cryptographic Research (IACR); the second is a non-binding poll among the students of the Department of Informatics and Telecommunications (DI&T) of the University of Athens.

Due to space limitations, we present at length the methodology for both our surveys in the full version [33, Subsect. 6.1.1]. Here, we provide the computed parameters $\kappa _1,\kappa _2,\kappa _3,\mu _1,\mu _2$ of Theorem 1 for the IACR and the DI&T surveys in Table 1. For both surveys, no complaints or audit failures were reported. Hence, due to lack of data, we choose a “neutral” value for $\kappa _3$ equal to 0.5 (see also Subsect. 4.5). Note that our analysis will hold for any other value of $\kappa _3$ not close to 0. The case of $\kappa _3 =0$, i.e., when the voter always complains to the authority when a Benaloh audit goes wrong, would make VSD attacks unattractive in the case that $\phi$ is small and would suggest that the attacker will opt for Replacement attacks, if such attacks are feasible.

The parameters $\kappa _1,\kappa _2,\kappa _3,\mu _1,\mu _2$ used in Theorem 1 express the vulnerability of Helios ceremony against verifiability attacks w.r.t. a specific voter transducer distribution. Namely, parameters $\kappa _1,\kappa _3,\mu _1$ determine the size of the subsets of vulnerable voters, while $\kappa _2,\mu _2$ can be seen as measures of the quality of the VSD and Replacement attacks.

Table 1. Instantiated parameters $\kappa _1,\kappa _2,\kappa _3,\mu _1,\mu _2$ of Theorem 1 for the IACR and the DI&T surveys.

Analysis of the IACR Survey: From the first row of Table 1, we read that $\mu _2=0.084$ which is a very small value as opposed to $\kappa _2=0.315$. Thus, we expect that elections where the electorate follows the voter transducer distribution of IACR elections are much more vulnerable to Replacement attacks rather than VSD attacks. Indeed, this is consistent with the analysis that we describe below.

We computed the percentage of tally deviation/No. of voters that the adversary can achieve when the success probability is lower bounded by $25\%$, $10\%$, $5\%$ and $1\%$ for various electorate scales. Specifically, we observed that the success probability bounds stated in Theorem 1 express more accurately the effectiveness of the adversarial strategy for (i) medium to large scale elections when the adversary attacks via the VSD and (ii) for small to medium scale elections when the adversary attacks via the BB. As a consequence, we present our analysis for $n=100,500,1000,2500$ and 5000 voters w.r.t. Replacement attack effectiveness and for $n=5000,10000$ and 50000 voters w.r.t. VSD attack effectiveness.

Table 2. Percentage of tally deviation/No. of voters achieved in elections under Replacement attack strategies against electorates following the voter transducer distribution of IACR elections. The attack succeeds even when $\theta =n$ and $\phi =0$.

The data in Table 2 illustrate the power of Replacement attacks against compact bodies of voters (e.g. organizations, unions, board elections, etc.) where $\mathsf {BB}$ auditing is rare. We can see that in the order of hundreds, more than 5% of the votes could be swapped with significant probability of no detection. This power deteriorates rapidly as we enter the order of thousands, yet the election result could still be undermined, as deviation between 1%–2%, is possible, without the risk of any complaint due to unsuccessful engagement in the $\mathbf {Cast}$ ceremony (i.e. $\theta =n, \phi =0$). Therefore, even in a setting of high complaint rate ($\kappa _3$ is close to 0), the adversary may turn into a Replacement attack strategy and still be able to alter radically the election result, as marginal differences are common in all types of elections. We stress that from published data we are aware of, there have been elections for the IACR board where the votes for winning candidates were closer than 3% to the votes of candidates that lost in the election. Therefore, if the voter distribution had been as the one derived by Table 1, and 500 members had voted, the result could have been overturned with success probability $25\%$ even if a single complaint was considered a “stop election event” (since $\phi =0$).

To provide more context, in Table 3, we provide the cutoff between elected and non-elected candidates for the last 11 years of IACR elections for the Board of Directors, followed by the exact success probability of a hypothetical Replacement attack strategy to overturn the election result given the actual number of cast ballots per year. We observe that the attacker success probability for many of the elections is considerable (2011, 2014, 2015, 2016), or even unacceptable (2006, 2008, 2009, 2013), at least in our estimation.

Table 3. Success probability of a hypothetical Replacement attack strategy against the IACR elections for the Board of Directors per election year. The success probability is computed given the number of participants and the cutoff between the last elected director and the first candidate that was not elected. The dashed line denotes the actual start of Helios use for IACR elections. Regarding the year 2007, no data were recorded in https://www.iacr.org/elections/.

On the other hand, the effectiveness of a VSD attack strategy against an election that follows the voter distribution in IACR elections would not have a great impact unless an unnatural number of complaints could be tolerated. Indeed, from our evaluation, it appears even for the scale of 5000, 10000 and 50000 that voters, the rate of complaints that is ignored must be close to 24%, 21% and 17% respectively, which is rather unacceptable in a real world setting. Such number of complaints would most definitely lead to a stop election event.

We conclude that the IACR voter behaviour is susceptible to Replacement attacks with significant probability of success but not VSD attacks unless there is high tolerance in voter complaints.

Analysis of the DI&T Poll: Due to space limitations, we present the analysis of the DI&T poll in the full version [33, Subsect. 6.1.3]. In few words, from the second row of Table 1, we read that $\kappa _2=0.069$ which is a very small value leading to significant VSD vulnerability.

6.2 Evaluations Based on Simulated Data

Our human data analysis is obtained by real bodies of voters that have an imperfect voting behaviour. To understand what would be the security level of a Helios e-voting ceremony when executed by an “ideally trained” electorate, we evaluated the security of simulated elections. Namely, we computed the detection probability that Theorem 2 can guarantee defined as $(1-\epsilon )\cdot 100\%$, where $\epsilon$ is the error stated in Theorem 2.

The voter distributions we considered were chosen from $\{\mathbf {D}_{p,q}\}_{p\in [0,1],q\in \mathbb {N}}$, a collection of distributions defined as follows: when behaving according to distribution $\mathbf {D}_{p,q}$, the voter flips a coin b with bias p to perform Benaloh audits when $b=1$, up to a maximum number of q audits. In any case of termination, she flips a coin $b'$ with bias p to perform $\mathsf {BB}$ audit when $b'=1$.

By the above description, we select as VSD resistance index $i^*=q$ and $\mathsf {BB}$ resistance set $\mathcal {J}^*=\{0,\ldots ,q\}$. For these $i^*,\mathcal {J}^*$ we compute the parameters $\kappa _1=\mu _1=p^{q}$ and $\kappa _2=\mu _2=1-p$, while we also set $\kappa _3$ to the balanced parameter 1/2. Intuitively, this type of voter behaviour should result in a sufficient level of resistance against of VSD and Replacement attacks, if the values $1-p$ and $p^q$ are small enough.

As an instance of our search, we present our findings for $n=250000$ voters for distributions $\mathbf {D}_{p,q}$, where $p=0.25,0.5,0.75$ and $q=3,5,8,10$ in Table 4. In particular, we present the deviation cutoff that can be guaranteed with detection probability 90%, 99% and 99.9%, in an election where the ratio of complaining voters is no more than 0.1%. For a more detailed description of our methodology, we refer the reader to the full version [33, Sect. 6.2].

Table 4. Security w.r.t. detection probability $90\%,99\%$ and $99,9\%$ of $\delta /n\cdot \%:=$ (tally deviation)/(No. of voters) percentage for elections with $n=250000$ voters and $\phi /n\le 0,1\%$ for distributions $\mathbf {D}_{p,q}$, where $p=0.25,0.5,0.75$ and $q=3,5,8,10$. The detection probability is defined as $(1-\epsilon )\cdot 100\%$, where $\epsilon$ is the error stated in Theorem 2.

By reading the data in Table 4, we observe that the security guarantee is optimised for the fair coin flipping case $p=0.5$. Nevertheless, even for this case, acceptable levels of security (e.g., (tally deviation)/(No. of voters) $\le 3\%$ or error probability $\le 1\%$) can be achieved only for relatively high values of $q\ge 8$. Besides, recall that these values are reached in the setting where a very small rate ($\le$0.1%) of complaining voters is allowed. As a result, the auditing behaviour of the voters and the complaint tolerance must be almost ideal in order for a high level of security to be achieved.

7 Conclusion

We have introduced the concept of ceremonies to the setting of e-voting systems. Our framework enables the modelling of all human participants to an e-voting protocol as nodes in the protocol execution. Human nodes are modelled as random variables over a set of admissible protocol behaviours which are described by (finite state) transducers. Our analysis enables the exploration of feasibility and infeasibility results regarding the verifiability of the Helios system (suitably modified to be a ceremony) conditioning on general classes of possible voter behaviours. The results from our characterization are essentially tight in the sense that behaviours excluded from our security theorem are too weak/predictable to offer a reasonable level of verifiability.

Our results are only an initial step in the direction of fully incorporating human behavior and interaction within cryptographic modeling. There are many ways to extend the way human nodes are affected by the environment (e.g., taking into account the timing of other nodes) or being manipulated to perform the protocol steps in a wrong order (cf. [29]). Still, even with our limited analysis, we demonstrated that current election procedures, even those performed by cryptographers, are extremely prone to manipulation. Our positive results, albeit also modest, show that there exist behaviors that if uniformly regimented they can provide a reasonable level of e-voting security. Designing e-voting protocols for which this set of behaviors can be efficiently learnable by humans is a further interesting direction motivated by our work.