ASAP: Election Verifiability with ProVerif

Election Verifiability with ProVerif

Véronique Cortier, Alexandre Debant, and Vincent Cheval. Election Verifiability with ProVerif. In 36th IEEE Computer Security Foundations Symposium (CSF'23), Dubrovnik, Croatia, July 2023.

Download

[PDF]

Abstract

Electronic voting systems should guarantee (at least) vote privacy andverifiability. Formally proving these two properties is challenging.Indeed, vote privacy is typically expressed as an equivalenceproperty, hard to analyze for automatic tools, while verifiabilityrequires to count the number of votes, to guaranteethat all honest votes are properly tallied.
We provide a full characterization of E2E-verifiability in terms oftwo simple properties, that are shown to be both sufficient andnecessary. In contrast, previous approaches proposed sufficientconditions only.These two properties can easily be expressed in a formal tool likeProVerif but remain hard to prove automatically. Therefore, weprovide a generic election framework, together with a library oflemmas, for the (automatic) proof of E2E-verifiability.We successfully apply our framework to several protocols of theliterature that include two complex, industrial-scale votingprotocols, namely Swiss Post and CHVote, designed for the Swiss context.

BibTeX

@InProceedings{CSF23,
  author = 	 {V\'eronique Cortier and Alexandre Debant and Vincent Cheval},
  title = 	 {Election Verifiability with ProVerif},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {36th IEEE Computer Security Foundations Symposium (CSF'23)},
  year = 	 {2023},
  abstract = {Electronic voting systems should guarantee (at least) vote privacy and
verifiability. Formally proving these two properties is challenging.
Indeed, vote privacy is typically expressed as an equivalence
property, hard to analyze for automatic tools, while verifiability
requires to count the number of votes, to guarantee
that all honest votes are properly tallied.
\par
We provide a full characterization of E2E-verifiability in terms of
two simple properties, that are shown to be both sufficient and
necessary. In contrast, previous approaches proposed sufficient
conditions only.
These two properties can easily be expressed in a formal tool like
ProVerif but remain hard to prove automatically. Therefore, we
provide a generic election framework, together with a library of
lemmas, for the (automatic) proof of E2E-verifiability.
We successfully apply our framework to several protocols of the
literature that include two complex, industrial-scale voting
protocols, namely Swiss Post and CHVote, designed for the Swiss context.},
  month = 	 {July},
  address = 	 {Dubrovnik, Croatia},
  OPTdoi = {},
  url =          {https://hal.inria.fr/hal-03700492/document},
}