ChevalCortieretalCSF26

Vincent Cheval, Véronique Cortier, Alexandre Debant, and Florian Moser. Simultaneously Proving Privacy and Verifiability: A ProVerif Framework for Internet Voting. In CSF 2026 - 39th IEEE Computer Security Foundations Symposium. IEEE, July 2026. To appear. Case study

Links

Long version

Abstract

Electronic voting aims to guarantee the same security properties than traditional paper-based voting, namely vote privacy and verifiability. While the formal verification of security protocols is now a mature field with several powerful tools such as ProVerif or Tamarin, verifying voting protocols still pushes existing tools at their limits. We present in this work a proof framework for ProVerif that models an extensible election setting with an unbounded number of concurrent elections, voters and votes. We also develop a library of lemmas to aid the automatic verification. Crucially, the framework allows to reuse the same protocol model for both privacy and verifiability proofs. We apply the framework to several protocols of the literature and industry, showing the flexibility and applicability of our framework.

Bibtex

@INPROCEEDINGS{ChevalCortieretalCSF26,
  AUTHOR = {Vincent Cheval and V{\'e}ronique Cortier and Alexandre Debant and Florian Moser},
  TITLE = {Simultaneously Proving Privacy and Verifiability: A {P}ro{V}erif Framework for Internet Voting},
  BOOKTITLE = {CSF 2026 - 39th IEEE Computer Security Foundations Symposium},
  YEAR = 2026,
  OPTPAGES = {},
  MONTH = JUL,
  PUBLISHER = {{IEEE}},
  NOTE = {To appear}
}