Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Véronique Cortier; Constantin Catalin Dragan; François Dupressoir; Benedikt Schmidt; Pierre-Yves Strub; Bogdan Warinschi

doi:10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

31 Citations (Scopus)

471 Downloads (Pure)

Abstract

We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme.

In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.

Original language	English
Title of host publication	2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017)
Subtitle of host publication	Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	993-1008
Number of pages	17
ISBN (Electronic)	9781509055333
ISBN (Print)	9781509055340
DOIs	https://doi.org/10.1109/SP.2017.28
Publication status	Published - Jul 2017

Publication series

Name
ISSN (Print)	2375-1207

Access to Document

10.1109/SP.2017.28

Full-text PDF (accepted author manuscript)
This is the author accepted manuscript (AAM). The final published version (version of record) is available online via IEEE at http://ieeexplore.ieee.org/document/7958621/. Please refer to any applicable terms of use of the publisher.
Accepted author manuscript, 447 KB

Handle.net

Persistent link

Dr François Dupressoir
- f.dupressoirbristol.acuk
- School of Computer Science - Associate Professor in Cryptography
Person: Academic
Bogdan Warinschi
- csxbwbristol.acuk
- School of Computer Science - Professor of Computer Science
- Cryptography and Information Security
Person: Academic , Member

Cite this

Cortier, V., Dragan, C. C., Dupressoir, F., Schmidt, B., Strub, P.-Y., & Warinschi, B. (2017). Machine-Checked Proofs of Privacy for Electronic Voting Protocols. In 2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017): Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA (pp. 993-1008). Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/SP.2017.28

@inproceedings{ad3a24afe69c40949776b33589ca4f90,

title = "Machine-Checked Proofs of Privacy for Electronic Voting Protocols",

abstract = "We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.",

author = "V{\'e}ronique Cortier and Dragan, {Constantin Catalin} and Fran{\c c}ois Dupressoir and Benedikt Schmidt and Pierre-Yves Strub and Bogdan Warinschi",

year = "2017",

month = jul,

doi = "10.1109/SP.2017.28",

language = "English",

isbn = "9781509055340",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

pages = "993--1008",

booktitle = "2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017)",

address = "United States",

}

Cortier, V, Dragan, CC, Dupressoir, F, Schmidt, B, Strub, P-Y & Warinschi, B 2017, Machine-Checked Proofs of Privacy for Electronic Voting Protocols. in 2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017): Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA. Institute of Electrical and Electronics Engineers (IEEE), pp. 993-1008. https://doi.org/10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols. / Cortier, Véronique; Dragan, Constantin Catalin; Dupressoir, François et al.
2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017): Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA. Institute of Electrical and Electronics Engineers (IEEE), 2017. p. 993-1008.

Research output: Chapter in Book/Report/Conference proceeding › Conference Contribution (Conference Proceeding)

TY - GEN

T1 - Machine-Checked Proofs of Privacy for Electronic Voting Protocols

AU - Cortier, Véronique

AU - Dragan, Constantin Catalin

AU - Dupressoir, François

AU - Schmidt, Benedikt

AU - Strub, Pierre-Yves

AU - Warinschi, Bogdan

PY - 2017/7

Y1 - 2017/7

N2 - We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.

AB - We provide the first machine-checked proof of privacy-related properties (including ballot privacy) for an electronic voting protocol in the computational model. We target the popular Helios family of voting protocols, for which we identify appropriate levels of abstractions to allow the simplification and convenient reuse of proof steps across many variations of the voting scheme. The resulting framework enables machine-checked security proofs for several hundred variants of Helios and should serve as a stepping stone for the analysis of further variations of the scheme. In addition, we highlight some of the lessons learned regarding the gap between pen-and-paper and machine-checked proofs, and report on the experience with formalizing the security of protocols at this scale.

U2 - 10.1109/SP.2017.28

DO - 10.1109/SP.2017.28

M3 - Conference Contribution (Conference Proceeding)

SN - 9781509055340

SP - 993

EP - 1008

BT - 2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017)

PB - Institute of Electrical and Electronics Engineers (IEEE)

ER -

Cortier V, Dragan CC, Dupressoir F, Schmidt B, Strub PY, Warinschi B. Machine-Checked Proofs of Privacy for Electronic Voting Protocols. In 2017 IEEE 38th IEEE Symposium on Security and Privacy (SP 2017): Proceedings of a meeting held 22-26 May 2017, San Jose, California, USA. Institute of Electrical and Electronics Engineers (IEEE). 2017. p. 993-1008 Epub 2017 Jun 26. doi: 10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Abstract

Publication series

Access to Document

Handle.net

Fingerprint

Profiles

Dr François Dupressoir

Bogdan Warinschi

Cite this