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.
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.
@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},
lsv-category = {autc},
wwwpublic = {public and ccsb},
}