Paper 2021/1201

Provably Improving Election Verifiability in Belenios

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


Belenios is an online voting system that provides a strong notion of election verifiability, where no single party has to be trusted, and security holds as soon as either the voting registrar or the voting server is honest. It was formally proved to be secure, making the assumption that no further ballots are cast on the bulletin board after voters verified their ballots. In practice, however, revoting is allowed and voters can verify their ballots anytime. This gap between formal proofs and use in practice leaves open space for attacks, as has been shown recently. In this paper we make two simple additions to Belenios and we formally prove that the new version satisfies the expected verifiability properties. Our proofs are automatically performed with the Tamarin prover, under the assumption that voters are allowed to vote at most four times.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. MINOR revision.E-VOTE-ID 2021
electronic votingformal verificationverifiability
Contact author(s)
sevdenur baloglu @ uni lu
sergiu bursuc @ uni lu
sjouke mauw @ uni lu
jun pang @ uni lu
2021-09-17: received
Short URL
Creative Commons Attribution


      author = {Sevdenur Baloglu and Sergiu Bursuc and Sjouke Mauw and Jun Pang},
      title = {Provably Improving Election Verifiability in Belenios},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1201},
      year = {2021},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.