Formal Verification and Solutions for Estonian E-Voting

BALOGLU, Sevdenur; BURSUC, Sergiu; MAUW, Sjouke; PANG, Jun

doi:10.1145/3634737.3657009

Download

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

Formal Verification and Solutions for Estonian E-Voting

BALOGLU, Sevdenur; BURSUC, Sergiu; MAUW, Sjouke et al.

2024 • In ACM AsiaCCS 2024 - Proceedings of the 19th ACM Asia Conference on Computer and Communications Security

Peer reviewed

Permalink
https://hdl.handle.net/10993/66914

DOI
10.1145/3634737.3657009

Files (1)Send to Details Statistics Bibliography Similar publications

Files

Full Text

3634737.3657009.pdf

Publisher postprint (922.14 kB)

Creative Commons License - Public Domain Dedication

Download

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink X Linkedin

Details

Keywords :

Formal verification; Privacy; Verifiability; Electronic voting; Receipt-freeness

Abstract :

[en] Estonia has been deploying electronic voting for its government elections since 2005. The underlying e-voting system and protocol have been continuously improved, aiming to fix the vulnerabilities found over the years and to provide election verifiability, which is now the standard way to ensure election integrity despite corrupt infrastructure or parties. Another goal is receipt-freeness, to ensure privacy even if voters are coerced. However, several recent attacks against its verifiability and privacy show the need of rigorous, realistic formal specifications for the protocol and its security, of new solutions to mitigate attacks, and of automated security proofs to ensure all attacks have been covered. In this paper we propose: • a formal specification of the Estonian E-Voting protocol in a symbolic model suited for automated verification tools; • a general symbolic model for specifying privacy and receipt-freeness in presence of corrupt parties and infrastructure; • automated verification of security with respect to an exhaustive set of corruption scenarios, discovering new attacks on verifiability (with Tamarin) and on privacy (with ProVerif). • new solutions, focused on practical deployment and ease of use, and their automated proofs of security.

Disciplines :

Computer science

Author, co-author :

BALOGLU, Sevdenur ; University of Luxembourg > Faculty of Science, Technology and Medicine > Department of Computer Science > Team Sjouke MAUW

BURSUC, Sergiu ; University of Luxembourg > Faculty of Science, Technology and Medicine > Department of Computer Science > Team Sjouke MAUW

MAUW, Sjouke ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

PANG, Jun ; University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS)

External co-authors :

yes

Language :

English

Title :

Formal Verification and Solutions for Estonian E-Voting

Publication date :

July 2024

Event name :

19th ACM Asia Conference on Computer and Communications Security (AsiaCCS)

Event place :

Singapore, Sgp

Event date :

01-07-2024 => 05-07-2024

Audience :

International

Main work title :

ACM AsiaCCS 2024 - Proceedings of the 19th ACM Asia Conference on Computer and Communications Security

Publisher :

Association for Computing Machinery, Inc

ISBN/EAN :

9798400704826

Peer reviewed :

Peer reviewed

Additional URL :

https://dl.acm.org/doi/10.1145/3634737.3657009

FnR Project :

FNR17238244 - AVVA - Automated Verification Of Privacy In Electronic Voting For Strong Adversaries, 2022 (01/04/2023-31/03/2025) - Sjouke Mauw

Funding text :

This work was supported by the Luxembourg National Research Fund (FNR) under the grant agreement C22/IS/17238244/AVVA.

Available on ORBilu :

since 18 December 2025

Statistics

Number of views

22 (0 by Unilu)

Number of downloads

7 (0 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

OpenCitations

OpenAlex citations

WoS citations^™

Bibliography

a1 [n. d.]. Additional material: code files for the specifications. https://github.com/sbaloglu/eev-codes
a2 [n. d.]. Statistics about internet voting in Estonia. https://www.valimised.ee/en/archive/statistics-about-internet-voting-estonia
a3 [n. d.]. Estonian online voting system. https://github.com/valimised/ivxvhttps://github.com/valimised/ivxv.
a4 [n. d.]. Helios - Verifiable Online Elections. https://heliosvoting.org/ https://heliosvoting.org/.
a5 [n. d.]. Belenios - Verifiable Online Voting System. https://belenios.org/https://belenios.org/.
a6 [n. d.]. SwissPost e-voting system. https://gitlab.com/swisspost-evotinghttps://gitlab.com/swisspost-evoting.
a7 [n. d.]. Tamarin Prover. https://tamarin-prover.github.io
a8 [n. d.]. ProVerif: Cryptographic protocol verifier in the formal model. https://bblanche.gitlabpages.inria.fr/proverif/
Kushal Babel, Vincent Cheval, and Steve Kremer. 2020. On the semantics of communications when verifying equivalence properties. J. Comput. Secur. 28, 1 (2020), 71–127. https://doi.org/10.3233/JCS-191366
Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang. 2021. Election Verifiability Revisited: Automated Security Proofs and Attacks on Helios and Belenios. In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021. IEEE, 1–15. https://doi.org/10.1109/CSF51468.2021. 00019
Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang. 2021. Provably Improving Election Verifiability in Belenios. In Electronic Voting, Robert Krimmer, Melanie Volkamer, David Duenas-Cid, Oksana Kulyk, Peter Rønne, Mihkel Solvak, and Micha Germann (Eds.). Springer International Publishing, Cham, 1–16.
Sevdenur Baloglu, Sergiu Bursuc, Sjouke Mauw, and Jun Pang. 2023. Election Verifiability in Receipt-Free Voting Protocols. In 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023. IEEE, 59–74. https://doi.org/10.1109/CSF57540.2023.00005
Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, and Itsaka Rakotonirina. 2022. Tidy: Symbolic Verification of Timed Cryptographic Protocols. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi (Eds.). ACM, 263–276. https://doi.org/10.1145/3548606.3559343
David Bernhard, Véronique Cortier, David Galindo, Olivier Pereira, and Bogdan Warinschi. 2015. SoK: A Comprehensive Analysis of Game-Based Ballot Privacy Definitions. In 2015 IEEE Symposium on Security and Privacy, SP 2015, San Jose, CA, USA, May 17-21, 2015. IEEE Computer Society, 499–516. https://doi.org/10.1109/SP.2015.37
Bruno Blanchet. 2016. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security 1, 1-2 (2016), 1–135. https://doi.org/10.1561/3300000004
Bruno Blanchet, Martín Abadi, and Cédric Fournet. 2008. Automated verification of selected equivalences for security protocols. J. Log. Algebraic Methods Program. 75, 1 (2008), 3–51. https://doi.org/10.1016/J.JLAP.2007.06.002
Bruno Blanchet, Vincent Cheval, and Véronique Cortier. 2022. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022. IEEE, 69–86. https://doi.org/10.1109/SP46214.2022.9833653
Pyrros Chaidos, Véronique Cortier, Georg Fuchsbauer, and David Galindo. 2016. BeleniosRF: A Non-interactive Receipt-Free Electronic Voting Scheme. In 23rd ACM Conference on Computer and Communications Security (CCS’16). ACM, Vienna, Austria, 1614–1625. https://doi.org/10.1145/2976749.2978337
Vincent Cheval, Charlie Jacomme, Steve Kremer, and Robert Künnemann. 2022. SAPIC+: protocol verifiers of the world, unite!. In 31st USENIX Security Symposium, USENIX Security 2022, Boston, MA, USA, August 10-12, 2022, Kevin R. B. Butler and Kurt Thomas (Eds.). USENIX Association, 3935–3952. https://www.usenix.org/conference/usenixsecurity22/presentation/cheval
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2018. DEEPSEC: Deciding Equivalence Properties in Security Protocols Theory and Practice. In 2018 IEEE Symposium on Security and Privacy, SP 2018, Proceedings, 21-23 May 2018, San Francisco, California, USA. IEEE Computer Society, 529–546. https://doi.org/10.1109/SP.2018.00033
Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. 2020. The Hitchhiker’s Guide to Decidability and Complexity of Equivalence Properties in Security Protocols. In Logic, Language, and Security - Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday (Lecture Notes in Computer Science, Vol. 12300), Vivek Nigam, Tajana Ban Kirigin, Carolyn L. Talcott, Joshua D. Guttman, Stepan L. Kuznetsov, Boon Thau Loo, and Mitsuhiro Okada (Eds.). Springer, 127–145. https://doi.org/10.1007/978-3-030-62077-6_10
Michael R. Clarkson, Stephen Chong, and Andrew C. Myers. 2008. Civitas: Toward a Secure Voting System. In 2008 IEEE Symposium on Security and Privacy (S&P 2008), 18-21 May 2008, Oakland, California, USA. 354–368. https://doi.org/10.1109/SP.2008.32
Véronique Cortier. 2017. Electronic Voting: How Logic Can Help. In Implementation and Application of Automata - 22nd International Conference, CIAA 2017, Marne-la-Vallée, France, June 27-30, 2017, Proceedings (Lecture Notes in Computer Science, Vol. 10329), Arnaud Carayol and Cyril Nicaud (Eds.). Springer, xi–xii. https://link.springer.com/content/pdf/bfm%3A978-3-319-60134-2%2F1.pdf
Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, and Bogdan Warinschi. 2018. Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018. IEEE Computer Society, 298–312. https://doi.org/10.1109/CSF.2018.00029
Véronique Cortier, Constantin Cătălin Drăgan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, and Bogdan Warinschi. 2017. Machine-Checked Proofs of Privacy for Electronic Voting Protocols. In IEEE Symposium on Security and Privacy. 993–1008. https://doi.org/10.1109/SP.2017.28
Véronique Cortier, Alicia Filipiak, and Joseph Lallemand. 2019. BeleniosVS: Secrecy and Verifiability Against a Corrupted Voting Device. In 32nd IEEE Computer Security Foundations Symposium, Hoboken, NJ, USA, June 25-28, 2019. 367–381. https://doi.org/10.1109/CSF.2019.00032
Véronique Cortier, Pierrick Gaudry, and Stéphane Glondu. 2019. Belenios: A Simple Private and Verifiable Electronic Voting System. In Foundations of Security, Protocols, and Equational Reasoning - Essays Dedicated to Catherine A. Meadows (Lecture Notes in Computer Science, Vol. 11565), Joshua D. Guttman, Carl E. Landwehr, José Meseguer, and Dusko Pavlovic (Eds.). Springer, 214–238. https://doi.org/10.1007/978-3-030-19052-1_14
Véronique Cortier and Steve Kremer (Eds.). 2011. Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, Vol. 5. IOS Press. http://www.iospress.nl/loadtop/load.php?isbn=9781607507130
Véronique Cortier and Joseph Lallemand. 2018. Voting: You Can’t Have Privacy without Individual Verifiability. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, October 15-19, 2018, David Lie, Mohammad Mannan, Michael Backes, and XiaoFeng Wang (Eds.). ACM, 53–66. https://doi.org/10.1145/3243734.3243762
Véronique Cortier, Joseph Lallemand, and Bogdan Warinschi. 2020. Fifty Shades of Ballot Privacy: Privacy against a Malicious Board. In 33rd IEEE Computer Security Foundations Symposium, CSF 2020, Boston, MA, USA, June 22-26, 2020. IEEE, 17–32. https://doi.org/10.1109/CSF49147.2020.00010
Véronique Cortier and Ben Smyth. 2011. Attacking and Fixing Helios: An Analysis of Ballot Secrecy. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011. IEEE Computer Society, 297–311. https://doi.org/10.1109/CSF.2011.27
Cas Cremers, Charlie Jacomme, and Philip Lukert. 2023. Subterm-Based Proof Techniques for Improving the Automation and Scope of Security Protocol Analysis. In 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023. IEEE, 200–213. https://doi.org/10.1109/CSF57540.2023. 00001
Stéphanie Delaune, Steve Kremer, and Mark Ryan. 2009. Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17, 4 (2009), 435–487. https://doi.org/10.3233/JCS-2009-0340
Stéphanie Delaune and Joseph Lallemand. 2022. One Vote Is Enough for Analysing Privacy. In Computer Security - ESORICS 2022 - 27th European Symposium on Research in Computer Security, Copenhagen, Denmark, September 26-30, 2022, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 13554), Vijayalakshmi Atluri, Roberto Di Pietro, Christian Damsgaard Jensen, and Weizhi Meng (Eds.). Springer, 173–194. https://doi.org/10.1007/978-3-031-17140-6_9
Sven Heiberg, Kristjan Krips, and Jan Willemson. 2020. Planning the next steps for Estonian Internet voting. Proceedings of the E-Vote-ID (2020), 82.
Sven Heiberg, Peeter Laud, and Jan Willemson. 2011. The Application of I-Voting for Estonian Parliamentary Elections of 2011. In E-Voting and Identity - Third International Conference, VoteID 2011, Tallinn, Estonia, September 28-30, 2011, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 7187), Aggelos Kiayias and Helger Lipmaa (Eds.). Springer, 208–223. https://doi.org/10.1007/978-3-642-32747-6_13
Sven Heiberg, Tarvi Martens, Priit Vinkel, and Jan Willemson. 2016. Improving the Verifiability of the Estonian Internet Voting Scheme. In Electronic Voting - First International Joint Conference, E-Vote-ID 2016, Bregenz, Austria, October 18-21, 2016, Proceedings (Lecture Notes in Computer Science, Vol. 10141), Robert Krimmer, Melanie Volkamer, Jordi Barrat, Josh Benaloh, Nicole J. Goodman, Peter Y. A. Ryan, and Vanessa Teague (Eds.). Springer, 92–107. https://doi.org/10.1007/978-3-319-52240-1_6
Sven Heiberg and Jan Willemson. 2014. Verifiable internet voting in Estonia. In 6th International Conference on Electronic Voting: Verifying the Vote, EVOTE 2014, Lochau / Bregenz, Austria, October 29-31, 2014, Robert Krimmer and Melanie Volkamer (Eds.). IEEE, 1–8. https://doi.org/10.1109/EVOTE.2014.7001135
Lucca Hirschi, Lara Schmid, and David A. Basin. 2021. Fixing the Achilles Heel of E-Voting: The Bulletin Board. In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021. IEEE, 1–17. https://doi.org/10.1109/CSF51468.2021.00016
Ari Juels, Dario Catalano, and Markus Jakobsson. 2005. Coercion-resistant electronic elections. In Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, WPES 2005, Alexandria, VA, USA, November 7, 2005. 61–70. https://doi.org/10.1145/1102199.1102213
Steve Kremer, Mark Ryan, and Ben Smyth. 2010. Election Verifiability in Electronic Voting Protocols. In Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings (Lecture Notes in Computer Science, Vol. 6345), Dimitris Gritzalis, Bart Preneel, and Marianthi Theoharidou (Eds.). Springer, 389–404. https://doi.org/10.1007/978-3-642-15497-3_24
Ralf Küsters, Tomasz Truderung, and Andreas Vogt. 2011. Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study. In 32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA. 538–553. https://doi.org/10.1109/SP.2011.21
Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In 25th International Conference on Computer Aided Verification (Lecture Notes in Computer Science, Vol. 8044). Springer. https://doi.org/10.1007/978-3-642-39799-8_48
David Mestel, Johannes Mueller, and Pascal Reisert. 2022. How Efficient are Replay Attacks against Vote Privacy? A Formal Quantitative Analysis. In 35th IEEE Computer Security Foundations Symposium, CSF.
Johannes Müller. 2022. Breaking and Fixing Vote Privacy of the Estonian E-Voting Protocol IVXV. In 7th Workshop on Advances in Secure Electronic Voting, FC22. https://orbilu.uni.lu/handle/10993/49442
Olivier Pereira. 2022. Individual Verifiability and Revoting in the Estonian Internet Voting System. In 7th Workshop on Advances in Secure Electronic Voting, FC22. https://eprint.iacr.org/2021/1098
Peter Y. A. Ryan, Peter B. Rønne, and Vincenzo Iovino. 2016. Selene: Voting with Transparent Verifiability and Coercion-Mitigation. In Financial Cryptography and Data Security - FC 2016 International Workshops, BITCOIN, VOTING, and WAHC, Christ Church, Barbados, February 26, 2016, Revised Selected Papers (Lecture Notes in Computer Science, Vol. 9604). Springer, 176–192. https://doi.org/10.1007/978-3-662-53357-4_12
Stefan Santesson, Michael Myers, Rich Ankney, Ambarish Malpani, Slava Galperin, and Dr. Carlisle Adams. 2013. X.509 Internet Public Key Infrastructure Online Certificate Status Protocol - OCSP. RFC 6960. https://doi.org/10.17487/ RFC6960
Benedikt Schmidt, Simon Meier, Cas Cremers, and David A. Basin. 2012. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, Stephen Chong (Ed.). IEEE Computer Society, 78–94. https://doi.org/10.1109/CSF.2012.25
Drew Springall, Travis Finkenauer, Zakir Durumeric, Jason Kitcat, Harri Hursti, Margaret MacAlpine, and J. Alex Halderman. 2014. Security Analysis of the Estonian Internet Voting System. In Proceedings of the 21st ACM Conference on Computer and Communications Security. ACM.
Anggrio Sutopo, Thomas Haines, and Peter Roenne. 2023. On the Auditability of the Estonian IVXV System and an Attack on Individual Verifiability. In Workshop on Advances in Secure Electronic Voting.
Misni Suwito, Bayu Tama, Bagus Santoso, Sabyasachi Dutta, Haowen Tan, Ueshige Yoshifumi, and Kouichi Sakurai. 2022. A Systematic Study of Bulletin Board and Its Application. In Proceedings of the 2022 ACM on Asia Conference on Computer and Communications Security (Nagasaki, Japan) (ASIACCS 2022). Association for Computing Machinery, New York, NY, USA, 1213–1215. https://doi.org/10.1145/3488932.3527280
Robert Zuccherato, Patrick Cain, Dr. Carlisle Adams, and Denis Pinkas. 2001. Internet X.509 Public Key Infrastructure Time-Stamp Protocol (TSP). RFC 3161. https://doi.org/10.17487/RFC3161