Paper 2020/982

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

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


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.

Available format(s)
Publication info
Published elsewhere. MINOR revision.CSF2021
applicationselectronic votingformal verification
Contact author(s)
sevdenur baloglu @ uni lu
sergiu bursuc @ uni lu
sjouke mauw @ uni lu
jun pang @ uni lu
2021-08-16: last of 3 revisions
2020-08-18: received
See all versions
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.