Is one vote really enough? Vote privacy with re-voting and a dishonest ballot box

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 protocol 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 bind 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. Then, we extend this reduction result, as well as our formalisation of BPRIV , to account for the case of re-voting and a dishonest ballot box. We apply our reduction results to 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 .