Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Veronique Cortier; Constantin Catalin Dragan; Francois Dupressoir; Benedikt Schmidt; Pierre Yves Strub; Bogdan Warinschi

doi:10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Veronique Cortier
, Constantin Catalin Dragan
, Francois Dupressoir
, Benedikt Schmidt
, Pierre Yves Strub
, Bogdan Warinschi

École Polytechnique

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 Symposium on Security and Privacy, SP 2017 - Proceedings
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	993-1008
Number of pages	16
ISBN (Electronic)	9781509055326
DOIs	https://doi.org/10.1109/SP.2017.28
Publication status	Published - 23 Jun 2017
Event	2017 IEEE Symposium on Security and Privacy, SP 2017 - San Jose, United States Duration: 22 May 2017 → 24 May 2017

Publication series

Name	Proceedings - IEEE Symposium on Security and Privacy
ISSN (Print)	1081-6011

Conference

Conference	2017 IEEE Symposium on Security and Privacy, SP 2017
Country/Territory	United States
City	San Jose
Period	22/05/17 → 24/05/17

Keywords

Electronic voting
Helios
Machine-checked proofs

Access to Document

10.1109/SP.2017.28

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 Symposium on Security and Privacy, SP 2017 - Proceedings (pp. 993-1008). Article 7958621 (Proceedings - IEEE Symposium on Security and Privacy). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/SP.2017.28

@inproceedings{1f5ad35ed8af446bb47900960aa8110c,

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.",

keywords = "Electronic voting, Helios, Machine-checked proofs",

author = "Veronique Cortier and Dragan, \{Constantin Catalin\} and Francois Dupressoir and Benedikt Schmidt and Strub, \{Pierre Yves\} and Bogdan Warinschi",

note = "Publisher Copyright: {\textcopyright} 2017 IEEE.; 2017 IEEE Symposium on Security and Privacy, SP 2017 ; Conference date: 22-05-2017 Through 24-05-2017",

year = "2017",

month = jun,

day = "23",

doi = "10.1109/SP.2017.28",

language = "English",

series = "Proceedings - IEEE Symposium on Security and Privacy",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "993--1008",

booktitle = "2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings",

}

Cortier, V, Dragan, CC, Dupressoir, F, Schmidt, B, Strub, PY & Warinschi, B 2017, Machine-Checked Proofs of Privacy for Electronic Voting Protocols. in 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings., 7958621, Proceedings - IEEE Symposium on Security and Privacy, Institute of Electrical and Electronics Engineers Inc., pp. 993-1008, 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, United States, 22/05/17. https://doi.org/10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols. / Cortier, Veronique; Dragan, Constantin Catalin; Dupressoir, Francois et al.
2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings. Institute of Electrical and Electronics Engineers Inc., 2017. p. 993-1008 7958621 (Proceedings - IEEE Symposium on Security and Privacy).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

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

AU - Cortier, Veronique

AU - Dragan, Constantin Catalin

AU - Dupressoir, Francois

AU - Schmidt, Benedikt

AU - Strub, Pierre Yves

AU - Warinschi, Bogdan

PY - 2017/6/23

Y1 - 2017/6/23

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.

KW - Electronic voting

KW - Helios

KW - Machine-checked proofs

UR - https://www.scopus.com/pages/publications/85025167463

U2 - 10.1109/SP.2017.28

DO - 10.1109/SP.2017.28

M3 - Conference contribution

AN - SCOPUS:85025167463

T3 - Proceedings - IEEE Symposium on Security and Privacy

SP - 993

EP - 1008

BT - 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 2017 IEEE Symposium on Security and Privacy, SP 2017

Y2 - 22 May 2017 through 24 May 2017

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 Symposium on Security and Privacy, SP 2017 - Proceedings. Institute of Electrical and Electronics Engineers Inc. 2017. p. 993-1008. 7958621. (Proceedings - IEEE Symposium on Security and Privacy). doi: 10.1109/SP.2017.28

Machine-Checked Proofs of Privacy for Electronic Voting Protocols

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this