Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Verifying Privacy-type Properties of Electronic Voting Protocols. Journal of Computer Security, 17(4):435–487, IOS Press, July 2009.
Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. We study three privacy-type properties of electronic voting protocols: in increasing order of strength, they are vote-privacy, receipt-freeness, and coercion-resistance.
We use the applied pi calculus, a formalism well adapted to modelling such protocols, which has the advantages of being based on well-understood concepts. The privacy-type properties are expressed using observational equivalence and we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies vote-privacy.
We illustrate our definitions on three electronic voting protocols from the literature. Ideally, these three properties should hold even if the election officials are corrupt. However, protocols that were designed to satisfy receipt-freeness or coercion-resistance may not do so in the presence of corrupt officials. Our model and definitions allow us to specify and easily change which authorities are supposed to be trustworthy.
@article{DKR-jcs08,
abstract = {Electronic voting promises the possibility of a
convenient, efficient and secure facility for
recording and tallying votes in an election. Recently
highlighted inadequacies of implemented systems have
demonstrated the importance of formally verifying the
underlying voting protocols. We study three
privacy-type properties of electronic voting
protocols: in increasing order of strength, they are
vote-privacy, receipt-freeness, and
coercion-resistance.\par We use the applied pi
calculus, a formalism well adapted to modelling such
protocols, which has the advantages of being based on
well-understood concepts. The privacy-type properties
are expressed using observational equivalence and we
show in accordance with intuition that
coercion-resistance implies receipt-freeness, which
implies vote-privacy.\par We illustrate our
definitions on three electronic voting protocols from
the literature. Ideally, these three properties
should hold even if the election officials are
corrupt. However, protocols that were designed to
satisfy receipt-freeness or coercion-resistance may
not do so in the presence of corrupt officials. Our
model and definitions allow us to specify and easily
change which authorities are supposed to be
trustworthy.},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
OPTDOI = {10.3233/JCS-2009-0340},
journal = {Journal of Computer Security},
month = jul,
number = {4},
pages = {435-487},
publisher = {{IOS} Press},
title = {Verifying Privacy-type Properties of Electronic
Voting Protocols},
volume = {17},
year = {2009},
nmonth = {7},
lsv-category = {jour},
wwwpublic = {public and ccsb},
}