One Vote is Enough for Analysing Privacy

Stéphanie Delaune (1) , Joseph Lallemand (1) , Arthur Outrey (2)

1 SPICY - Security & PrIvaCY
2 ENS de Lyon - École normale supérieure de Lyon

Electronic voting promises the possibility of convenient and efficient systems for recording and tallying votes in an election. To be widely adopted, ensuring the security of the cryptographic protocols used in e-voting is of paramount importance. However, the security analysis of this type of protocols raises a number of challenges, and they are often out of reach of existing verification tools. In this paper, we study vote privacy, a central security property that should be satisfied by any e-voting system. More precisely, we propose the first formalisation of the recent BPRIV notion in the symbolic setting. To ease the formal security analysis of this notion, we propose a reduction result allowing one to bound the number of voters and ballots needed to mount an attack. We first consider the case where voters do not revote, and the ballot box is trusted before relaxing these two conditions. Our result applies on a number of case studies including several versions of Helios, Belenios, JCJ/Civitas, and Prêt-à-Voter. For some of these protocols, thanks to our result, we are able to conduct the analysis relying on the automatic tool Proverif.

Mots clés: Electronic voting; Formal methods; Protocol verification; Privacy

Domaines: Informatique [cs]

Stéphanie Delaune, Joseph Lallemand, Arthur Outrey. One Vote is Enough for Analysing Privacy. CNRS. 2023. ⟨hal-04262499⟩