## Verifying Properties of Electronic Voting Protocols

Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Verifying Properties of Electronic Voting Protocols. In * Proceedings of the IAVoSS Workshop On Trustworthy Elections (WOTE'06)*, pp. 45–52, Cambridge, UK, June 2006.

### Download

### Abstract

In this paper we report on some recent work to formally specify and verify electronic voting protocols. In particular, we use the formalism of the applied pi calculus: the applied pi calculus is a formal language similar to the pi calculus but with useful extensions for modelling cryptographic protocols. We model several important properties, namely fairness, eligibility, privacy, receipt-freeness and coercion-resistance. Verification of these properties is illustrated on two cases studies and has been partially automated using the Blanchet's ProVerif tool.

### BibTeX

@inproceedings{DKR-wote06, abstract = {In this paper we report on some recent work to formally specify and verify electronic voting protocols. In particular, we use the formalism of the applied pi calculus: the applied pi calculus is a formal language similar to the pi calculus but with useful extensions for modelling cryptographic protocols. We model several important properties, namely fairness, eligibility, privacy, receipt-freeness and coercion-resistance. Verification of these properties is illustrated on two cases studies and has been partially automated using the Blanchet's ProVerif tool.}, address = {Cambridge, UK}, author = {Delaune, St{\'e}phanie and Kremer, Steve and Ryan, Mark D.}, booktitle = {{P}roceedings of the {IAVoSS} {W}orkshop {O}n {T}rustworthy {E}lections ({WOTE}'06)}, month = jun, pages = {45-52}, title = {Verifying Properties of Electronic Voting Protocols}, year = {2006}, acronym = {{WOTE}'06}, nmonth = {6}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-wote06.pdf}, }