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.