Analysis of an Electronic Boardroom Voting System

Analysis of an Electronic Boardroom Voting System. Mathilde Arnaud, Véronique Cortier, and Cyrille Wiedling. In 4th International Conference on e-Voting and Identity (VoteID'13), Lecture Notes in Computer Science 7985, Springer, Surrey, UK, July 2013.

Download

[PDF] [HTML]

Abstract

We study a simple electronic boardroom voting system. While most existing systems rely on opaque electronic devices, a scientific committee of a research institute (the CNRS Section 07) has recently proposed an alternative system. Despite its simplicity (in particular, no use of cryptography), each voter can check that the outcome of the election corresponds to the votes, without having to trust the devices.
In this paper, we present three versions of this system, exhibiting potential attacks. We then formally model the system in the applied pi-calculus, and prove that two versions ensure both vote correctness (even if the devices are corrupted) and ballot secrecy (assuming the devices are honest).

BibTeX

@InProceedings{ACW-voteCNRS-VoteID13,
  author = 	 {Mathilde Arnaud and V\'eronique Cortier and Cyrille Wiedling},
  title = 	 {Analysis of an Electronic Boardroom Voting System},
  booktitle = {4th International Conference on e-Voting and Identity (VoteID'13)},
  OPTpages = 	 {},
  year = 	 {2013},
  OPTeditor = 	 {},
 volume = 	 {7985},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  address = 	 {Surrey, UK},
  month = 	 {July},
  OPTorganization = {},
  publisher = {Springer},
  DOI = {10.1007/978-3-642-39185-9_7},
  abstract = {We study a simple electronic boardroom voting system. While most existing systems rely on opaque electronic devices, a scientific committee of a research institute (the CNRS Section 07) has recently proposed an alternative system. Despite its simplicity (in particular, no use of cryptography), each voter can check that the outcome of the election corresponds to the votes, without having to trust the devices.
\par
In this paper, we present three versions of this system, exhibiting potential attacks. We then formally model the system in the applied pi-calculus, and prove that two versions ensure both vote correctness (even if the devices are corrupted) and ballot secrecy (assuming the devices are honest).},
}