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}, }