On the Specification and Verification of Voting Schemes

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Bernhard Beckert, Rajeev Goré und Carsten Schürmann
In:4th International Conference on E-Voting and Identity (Vote-ID 2013)
Verleger:Springer
Reihe:LNCS
Band:7985
Jahr:2013
Seiten:25-40
DOI:10.1007/978-3-642-39185-9_2

Abstract

The ability to count ballots by computers allows us to design new voting schemes that are arguably fairer than existing schemes designed for hand-counting. We argue that formal methods can and should be used to ensure that such schemes behave as intended and are conform to the desired democratic properties. Specifically, we define two semantic criteria for single transferable vote (STV) schemes, formulated in first-order logic, and show how bounded model-checking can be used to test whether these criteria are met. As a case study, we then analyse an existing voting scheme for electing the board of trustees for a major international conference and discuss its deficiencies.

BibTeX

@inproceedings{BeckertGoreSchuermann2013b,
  author    = {Bernhard Beckert and Rajeev Gor\'e and Carsten Sch\"urmann},
  title     = {On the Specification and Verification of Voting Schemes},
  pages     = {25--40},
  doi       = {10.1007/978-3-642-39185-9_2},
  booktitle = {4th International Conference on E-Voting and Identity (Vote-ID 2013)},
  editor    = {James Heather and Steve A. Schneider and Vanessa Teague},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7985},
  year      = {2013},
  month     = jul,
  date      = {July 17-19},
  abstract  = {The ability to count ballots by computers allows us to design
  	       new voting schemes that are arguably fairer than existing schemes designed
  	       for hand-counting. We argue that formal methods can and should
  	       be used to ensure that such schemes behave as intended and are conform
  	       to the desired democratic properties. Specifically, we define two
  	       semantic criteria for single transferable vote (STV) schemes, formulated
  	       in first-order logic, and show how bounded model-checking can be used
  	       to test whether these criteria are met. As a case study, we then analyse
  	       an existing voting scheme for electing the board of trustees for a major
  	       international conference and discuss its deficiencies.},
  place     = {Guildford, UK}
}