Automatic Margin Computation for Risk-Limiting Audits

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Michael Kirsten, Vladimir Klebanov, and Carsten Schürmann
In:First International Joint Conference on Electronic Voting – formerly known as EVOTE and VoteID (E-Vote-ID 2016)
Publisher:Springer
Series:LNCS
Volume:10141
Year:2017
Pages:18-35
PDF:
DOI:10.1007/978-3-319-52240-1_2

Abstract

A risk-limiting audit is a statistical method to create confidence in the correctness of an election result by checking samples of paper ballots. In order to perform an audit, one usually needs to know what the election margin is, i.e., the number of votes that would need to be changed in order to change the election outcome.
In this paper, we present a fully automatic method for computing election margins. It is based on the program analysis technique of bounded model checking to analyse the implementation of the election function. The method can be applied to arbitrary election functions without understanding the actual computation of the election result or without even intuitively knowing how the election function works.
We have implemented our method based on the model checker CBMC; and we present a case study demonstrating that it can be applied to real-world elections.

BibTeX

@InProceedings{BeckertKirstenEA2017,
  author		= {Bernhard Beckert and Michael Kirsten
  			   and Vladimir Klebanov and Carsten Schürmann},
  title			= {Automatic Margin Computation for Risk-Limiting Audits},
  booktitle		= {First International Joint Conference on Electronic Voting 
  			   – formerly known as EVOTE and VoteID (E-Vote-ID 2016)},
  editor		= {Robert Krimmer and
			   Melanie Volkamer and
			   Jordi Barrat and
			   Josh Benaloh and
			   Nicole J. Goodman and
			   Peter Y. A. Ryan and
			   Vanessa Teague},
  publisher		= {Springer},
  series		= {LNCS},
  pages			= {18--35},
  volume		= {10141},
  month			= jan,
  year			= {2017},
  doi			= {10.1007/978-3-319-52240-1_2},
  abstract              = {A risk-limiting audit is a statistical method to create confidence
  			   in the correctness of an election result by checking samples of
  			   paper ballots. In order to perform an audit, one usually needs to know
  			   what the election margin is, i.e., the number of votes that would need
  			   to be changed in order to change the election outcome.
                           \newline

  			   In this paper, we present a fully automatic method for computing
  			   election margins. It is based on the program analysis technique of
  			   bounded model checking to analyse the implementation of the election
  			   function. The method can be applied to arbitrary election functions
  			   without understanding the actual computation of the election result or
  			   without even intuitively knowing how the election function works.
                           \newline

  			   We have implemented our method based on the model checker CBMC; and
  			   we present a case study demonstrating that it can be applied to
  			   real-world elections.},
  place			= {Lochau / Bregenz, Austria},
  date			= {October 18-21}
}