KIT | KIT-Bibliothek | Impressum | Datenschutz

Automatic Margin Computation for Risk-Limiting Audits

Beckert, Bernhard ORCID iD icon; Kirsten, Michael ORCID iD icon; Klebanov, Vladimir; Schürmann, Carsten

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.


Postprint §
DOI: 10.5445/IR/1000092709
Veröffentlicht am 28.03.2019
Originalveröffentlichung
DOI: 10.1007/978-3-319-52240-1_2
Scopus
Zitationen: 2
Dimensions
Zitationen: 2
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Buchaufsatz
Publikationsjahr 2017
Sprache Englisch
Identifikator ISBN: 978-3-319-52240-1
ISSN: 0302-9743, 1611-3349
urn:nbn:de:swb:90-927090
KITopen-ID: 1000092709
Erschienen in Electronic Voting - First International Joint Conference, E-Vote-ID 2016, Bregenz, Austria, October 18-21, 2016, Proceedings. Ed.: R. Krimmer, M. Volkamer, J. Barrat, J. Benaloh, N. J. Goodman, P. Y. A. Ryan, V. Teague
Verlag Springer International Publishing
Seiten 18–35
Serie Lecture Notes in Computer Science
Vorab online veröffentlicht am 26.01.2017
Schlagwörter Risk-limiting audit, Margin computation, Software bounded model checking, Static analysis
Nachgewiesen in Dimensions
Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page