Paper 2021/1071

Improved Verifiability for BeleniosVS

Thomas Haines and Rajeev Gore


The BeleniosVS electronic voting scheme offers an attractive mix of verifiability and privacy properties. Moreover, using the ProVerif protocol-verification tool, BeleniosVS has automatic machine-aided analysis of (end-to-end) verifiability in 96 different threat models with the machine-aided analysis finding proofs in 22 cases and finding attacks in the remaining 74 cases. The high number of threat models covered by ProVerif delivers a much richer security analysis than the norm. We revisit the BeleniosVS scheme and propose several refinements to the ProVerif security model and scheme which increase the number of threat models in which the scheme has verifiability from 22 to 28. Our new ProVerif security model also implies end-to-end verifiability but the requirements are easier to satisfy. Interestingly, in all six improvements, both the changes to the security model and one or more changes to the scheme are necessary to prove verifiability.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Sixth International Joint Conference on Electronic Voting
VerifiabilityMachine-checked proofsProVerifBeleniosVS
Contact author(s)
thomas haines @ anu edu au
2021-08-23: received
Short URL
Creative Commons Attribution


      author = {Thomas Haines and Rajeev Gore},
      title = {Improved Verifiability for {BeleniosVS}},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1071},
      year = {2021},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.