Machine-Checked Proofs of Privacy for Electronic Voting Protocols
- Submitting institution
-
The University of Surrey
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 9025525_1
- Type
- D - Journal article
- DOI
-
10.1109/SP.2017.28
- Title of journal
- 2017 IEEE Symposium on Security and Privacy (SP)
- Article number
- -
- First page
- 0
- Volume
- 0
- Issue
- 0
- ISSN
- 2375-1207
- Open access status
- Compliant
- Month of publication
- -
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 6
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This work provides the first machine-checked proof of privacy in the computational model for the deployed electronic voting protocol Helios, and hundreds of its variants-with some already deployed in real-world elections. This is significant as all previous proofs of privacy for voting protocols have either been in pen-and-paper style (that are prone to mistakes), or automatic only in the symbolic model (that are more abstract and assume perfect cryptographic primitives). Furthermore, this work considerably generalizes to allow for hundreds of variants to be machine-checked, a task impossible to achieve with pen-and-paper with the same degree of confidence.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -