Design and Formal Verification of E-Voting Protocols

Summary

We proposed the design of new voting protocols that realize a novel approach for democracy, called random sample voting. Moreover, we provided new formal foundations for reasoning about voting protocols, their security properties, and their underlying system assumptions.

Novel approaches for democracy

Novel forms of democracy are an actively discussed research area in political economy. One of these approaches, random sample voting, proposes that solely a randomly chosen subset of the electorate actually votes on such decisions. Random sample voting is not only interesting by itself but also as a building block for other novel voting approaches, such as Assessment voting and Co-​voting. To meaningfully assess the benefits of such novel forms of democracy, we studied them from a security perspective in a collaboration with the Zurich Risk Center.

Specifically, our contribution consists of the design of Alethea, the first random sample voting protocol that satisfies end-​to-end verifiability and receipt-​freeness. A new challenge in random sample voting is that the chosen voters must be randomly selected while preserving their anonymity. Moreover, the small number of selected voters leaves little room for error and only a few manipulations of the votes may significantly change the outcome.

Our protocol makes explicit the distinction between human voters and their devices. This allows for more fine-​grained statements about the required capabilities and trust assumptions of each agent than is possible in previous work. We define new security properties related to the randomness and anonymity of the sample group and the probability of undetected manipulations. We prove correctness of the protocol and its properties both using traditional paper and pen proofs and with the Tamarin prover.

Dispute Resolution in Voting

Disputes arise in voting when a voter claims that his ballot was not correctly included in the tally while the authority running the election claims to have followed the protocol. A dispute can be resolved if any third party can unambiguously determine who is right. In this project, we analyzed which disputes are relevant for a generic, practically relevant, class of voting protocols. Based on this characterization, we then propose a new definition of dispute resolution for voting that accounts for both the possibility that voters and the voting authority can make false claims and that voters may abstain from voting.

Our definition includes a notion of timeliness requiring that a voter must possess the evidence required to resolve disputes no later than the election’s end. We then fully characterize what system and adversary assumptions are necessary and sufficient for the timeliness property to hold. Our results provide the basis for verification of dispute resolution for a broad class of protocols, which we demonstrated in example case studies.

Publications

• Election Security and Economics: It’s All About Eve, by David Basin and Hans Gersbach and Akaki Mamageishvili and Lara Schmid and Oriol Tejada. external pageE-Vote-ID 2017call_made. external pageDOIcall_made. DownloadFull version (PDF, 378 KB)vertical_align_bottom of the paper.
• Alethea: A Provably Secure Random Sample Voting Protocol, by David Basin, Saša Radomirović, and Lara Schmid. external pageIEEE CSF 2018call_made. DownloadFull version (PDF, 423 KB)vertical_align_bottom of the paper, external pagesourcescall_made.
• Dispute Resolution in Voting, by David Basin, Saša Radomirović and Lara Schmid. external pageIEEE CSF 2020call_made. DownloadFull version (PDF, 473 KB)vertical_align_bottom of the paper and external pagesourcescall_made.