Alethea: A Provably Secure Random Sample Voting Protocol

Authors: David Basin, Sasa Radomirovic and Lara Schmid

Paper Information

Title:Alethea: A Provably Secure Random Sample Voting Protocol
Authors:David Basin, Sasa Radomirovic and Lara Schmid
Proceedings:CSF CSF Proceedings
Editors: Stephen Chong, Stephanie Delaune and Deepak Garg
Keywords:random sample voting, e-voting, formal verification, automated reasoning

ABSTRACT. In random sample voting, only a randomly chosen subset of all eligible voters vote. We propose Alethea, the first random sample voting protocol that satisfies end-to-end verifiability and receipt-freeness. Our protocol makes explicit the distinction between the human voters and their devices. This allows us to make more fine-grained statements about the required capabilities and trust assumptions of each agent than is possible in previous work. Consequently, we can make more precise statements about the adversary models under which our protocol is secure.

Alethea is the first formally verified random sample voting protocol. This necessitates defining new security properties, in particular that the sample group is chosen randomly and that the chosen voters remain anonymous. We model the protocol and its properties in a symbolic model amenable to tool support. We verify most of the properties automatically and complete our analysis using traditional hand-written proofs when automatic analysis is either infeasible or when we desire a more fine-grained analysis than our symbolic abstractions allow.

Talk:Jul 11 16:00 (Session 67A: Electronic voting)