Verifying Properties of Electronic Voting Protocols

Mark Ryan · Steve Kremer · Stephanie Delaune

About electronic voting

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes.  It can be used for a variety of types of elections, from small committees or on-line communities through to full-scale national elections.  However, the electronic voting machines used in recent US elections have been fraught with problems.  Recent work has analysed the source code of the machines sold by the second largest and fastest-growing vendor, which are in use in 37 US states. This analysis has produced a catalogue of vulnerabilities and possible attacks.

A potentially much more secure system could be implemented, based on formal protocols that specify the messages sent between the voters and administrators. Such protocols have been studied for several decades (see, e.g., references [1-8] below, and surveys). These protocols aim to provide security properties which go beyond those that can be achieved by paper-based voting systems. Such properties include

  • Fairness: no early results can be obtained which could influence the remaining voters.
  • Eligibility: only legitimate voters can vote, and only once.
  • Individual verifiability: a voter can verify that her vote was really counted.
  • Universal verifiability: the published outcome really is the sum of all the votes.
  • Privacy: the fact that a particular voted in a particular way is not revealed to anyone.
  • Coercion-resistance: a voter cannot cooperate with a coercer to prove to him that she voted in a certain way.

Our work is about formally verifying the correctness of protocols with respect to these properties. We have analysed protocols using the applied pi calculus of Abadi and Fournet. Our analysis was partially automated by the ProVerif tool.

Privacy-type properties

We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness, and coercion-resistance. We use the applied pi calculus, a formalism well adapted to modelling such protocols, which moreover offers partially automated tool support. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy.

We illustrate our definitions on three electronic voting protocols from the literature: Fujioka/Okamoto/Ohta, Okamota, and Lee et al. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.

An earlier shorter paper verifies privacy and some other properties for the Fujioka/Okamoto/Ohta protocol:

These earlier papers attempt to characterise the coercion-resistance property using the notion of adaptive simulation. We were not able to make that work entirely to our satisfaction in later papers, and modified the definition of coercion-resistance for the journal paper mentioned above.

Verifiability properties

Automated reasoning for election verifiability in electronic voting (Abstract)

We propose a new definition of election verifiability for electronic voting protocols. Our definition is presented in terms of reachability properties using the applied pi calculus. In contrast with previous formalisations our approach is amenable to automation. Furthermore the definition is extended to provide the first framework to establish sufficient voter capabilities for election verifiability when using hostile computer services. More precisely the voter is assumed to vote using Satan's computer. The applicability of our methodology is demonstrated by showing the protocols due to Fujioka, Okamoto & Ohta and Juels, Catalano & Jakobsson satisfy election verifiability. Satan's computer paradigm allows us to compare the relative degrees of election verifiability offered by these protocols.

Presentations

Electronic Voting: practice and theory

Collaborators