Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Coercion-Resistance and Receipt-Freeness in Electronic Voting. In Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp. 28–39, IEEE Computer Society Press, Venice, Italy, July 2006.
In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter \(A\) cannot prove to a potential coercer \(C\) that she voted in a particular way. We assume that \(A\) cooperates with \(C\) in an interactive way. Receipt-freeness is a weaker property, for which we assume that \(A\) and \(C\) cannot interact during the protocol, but \(A\) later provides evidence (the receipt) of how she voted. While receipt-freeness can be expressed using observational equivalence from the applied pi calculus, we need to introduce a new relation to capture coercion-resistance. Our formalization of coercion-resistance and receipt-freeness are quite different. Nevertheless, we show in accordance with intuition that coercion-resistance implies receipt-freeness, which implies privacy, the basic anonymity property of voting protocols, as defined in previous work. Finally we illustrate the definitions on a simplified version of the Lee et al. voting protocol.
@inproceedings{DKR-csfw06,
abstract = {In this paper we formally study important properties
of electronic voting protocols. In particular we are
interested in coercion-resistance and
receipt-freeness. Intuitively, an election protocol
is coercion-resistant if a voter \(A\) cannot prove
to a potential coercer~\(C\) that she voted in a
particular way. We assume that \(A\) cooperates
with~\(C\) in an interactive way. Receipt-freeness is
a weaker property, for which we assume that \(A\)
and~\(C\) cannot interact during the protocol, but
\(A\) later provides evidence (the receipt) of how
she voted. While receipt-freeness can be expressed
using observational equivalence from the applied pi
calculus, we need to introduce a new relation to
capture coercion-resistance. Our formalization of
coercion-resistance and receipt-freeness are quite
different. Nevertheless, we show in accordance with
intuition that coercion-resistance implies
receipt-freeness, which implies privacy, the basic
anonymity property of voting protocols, as defined in
previous work. Finally we illustrate the definitions
on a simplified version of the Lee~\emph{et~al.}\
voting protocol.},
address = {Venice, Italy},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Ryan, Mark D.},
booktitle = {{P}roceedings of the 19th {IEEE} {C}omputer
{S}ecurity {F}oundations {W}orkshop ({CSFW}'06)},
OPTDOI = {10.1109/CSFW.2006.8},
month = jul,
pages = {28-39},
publisher = {{IEEE} Computer Society Press},
title = {Coercion-Resistance and Receipt-Freeness in
Electronic Voting},
year = {2006},
acronym = {{CSFW}'06},
nmonth = {7},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}