Reference : Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and...
E-prints/Working papers : Already available on another site
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/45565
Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios
English
Baloglu, Sevdenur mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > PI Mauw >]
Bursuc, Sergiu mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > PI Mauw >]
Mauw, Sjouke mailto [University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) >]
Pang, Jun mailto [University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) >]
Aug-2020
Cryptology ePrint Archive
31
No
[en] foundations / applications ; electronic voting ; formal verification
[en] 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 Helios, our analysis is the first one to be, at the same time, fully automated (with the Tamarin protocol prover) and to precisely capture its end-to-end verifiability guarantees, allow- ing us to derive new security proofs and new attacks on deployed versions of it. For Belenios, similarly, we capture precisely the end-to-end verifiability guarantees when all election authorities are corrupted, which is outside the scope of previous formal definitions. We also find new attacks that apply in weaker corruption scenarios that are expected to be secure. In general, our framework allows a unified analy- sis and comparison of cryptographic voting protocols, corruption scenarios and verifiability procedures towards ensuring the end goal of election integrity.
R-AGR-3433-11
Researchers ; Professionals ; Students
http://hdl.handle.net/10993/45565
https://eprint.iacr.org/2020/982

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
2020-982.pdfAuthor preprint419.63 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.