### Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios

Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang

##### Abstract

Election verifiability aims to ensure that the outcome produced by electronic voting systems correctly reflects the intentions of eligible voters, even in the presence of an adversary that may corrupt various parts of the voting infrastructure. Protecting such systems from manipulation is challenging because of their distributed nature involving voters, election authorities, voting servers and voting platforms. An adversary corrupting any of these can make changes that, individually, would go unnoticed, yet in the end will affect the outcome of the election. It is, therefore, important to rigorously evaluate whether the measures prescribed by election verifiability achieve their goals. We propose a formal framework that allows such an evaluation in a systematic and automated way. We demonstrate its application to the verification of various scenarios in Helios and Belenios, two prominent internet voting systems, for which we capture features and corruption models previously outside the scope of formal verification. Relying on the Tamarin protocol prover for automation, we derive new security proofs and attacks on deployed versions of these protocols, illustrating trade-offs between usability and security.

##### Metadata
Available format(s)
Category
Foundations
Publication info
Published elsewhere. MINOR revision.CSF2021
Keywords
applicationselectronic votingformal verification
Contact author(s)
sevdenur baloglu @ uni lu
sergiu bursuc @ uni lu
sjouke mauw @ uni lu
jun pang @ uni lu
History
2021-08-16: last of 3 revisions
2020-08-18: received
See all versions
Short URL
https://ia.cr/2020/982
License

CC BY

BibTeX

@misc{cryptoeprint:2020/982,
author = {Sevdenur Baloglu and Sergiu Bursuc and Sjouke Mauw and Jun Pang},
title = {Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios},
howpublished = {Cryptology ePrint Archive, Paper 2020/982},
year = {2020},
note = {\url{https://eprint.iacr.org/2020/982}},
url = {https://eprint.iacr.org/2020/982}
}

Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.