Stéphanie Delaune and Joseph Lallemand. One vote is enough for analysing privacy. In Proceedings of the 27th European Symposium on Research in Computer Security (ESORICS'22), pp. 173–194, Lecture Notes in Computer Science, Springer, Copenhague, Denmark, 2022.
Electronic voting promises the possibility of convenient and efficientsystems for recording and tallying votes in an election. To be widelyadopted, ensuring the security of the cryptographic protocols used in e-voting is ofparamount importance. However, the security analysis of this type of protocols raises a number ofchallenges, and they are often out of reach of existing verificationtools.In this paper, we study vote privacy, a central security propertythat should be satisfied by any e-voting system.More precisely, we propose the first formalisation ofthe recent BPriv notion in the symbolic setting.To ease the formal security analysis of this notion, we propose a reductionresult allowing one to bound the number of voters and ballots needed to mount an attack. Our result applies on a number of casestudies 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 onthe automatic tool Proverif.
@inproceedings{DL-esorics22,
address = {Copenhague, Denmark},
abstract = {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. 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.
},
author = {St{\'{e}}phanie Delaune and
Joseph Lallemand},
title = {One vote is enough for analysing privacy},
booktitle = {{P}roceedings of the 27th {E}uropean {S}ymposium on {R}esearch in {C}omputer {S}ecurity (ESORICS'22)},
year = {2022},
pages = {173--194},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
acronym = {{ESORICS}'22},
}