## 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

[PDF]

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