Coercion-Resistance and Receipt-Freeness in Electronic Voting

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.
doi:10.1109/CSFW.2006.8

Download

[PDF] [PDF (long version)] [PS] [PS (long version)] [HTML] 

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 et al. voting protocol.

BibTeX

@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)},
  DOI =           {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},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-csfw06.pdf},
}