Paper 2021/1071
Improved Verifiability for BeleniosVS
Thomas Haines and Rajeev Gore
Abstract
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.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Sixth International Joint Conference on Electronic Voting
- Keywords
- VerifiabilityMachine-checked proofsProVerifBeleniosVS
- Contact author(s)
- thomas haines @ anu edu au
- History
- 2021-08-23: received
- Short URL
- https://ia.cr/2021/1071
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2021/1071,
author = {Thomas Haines and Rajeev Gore},
title = {Improved Verifiability for BeleniosVS},
howpublished = {Cryptology ePrint Archive, Paper 2021/1071},
year = {2021},
note = {\url{https://eprint.iacr.org/2021/1071}},
url = {https://eprint.iacr.org/2021/1071}
}
