Paper Info
Title
Schulze Voting As Evidence Carrying Computation
Abstract
The correctness of vote counting in electronic election is one of the main pillars that engenders trust in electronic elections. However, the present state of the art in vote counting leaves much to be desired: while some jurisdictions publish the source code of vote counting code, others treat the code as commercial in confidence. None of the systems in use today applies any formal verification. In this paper, we formally specify the so-called Schulze method, a vote counting scheme that is gaining popularity on the open source community. The cornerstone of our formalisation is a (dependent, inductive) type that represents all correct executions of the vote counting scheme. Every inhabitant of this type not only gives a final result, but also all intermediate steps that lead to this result, and can so be externally verified. As a consequence, we do not even need to trust the execution of the (verified) algorithm: the correctness of a particular run of the vote counting code can be verified on the basis of the evidence for correctness that is produced along with determination of election winners.
Year
DOI
Venue
2017
10.1007/978-3-319-66107-0_26
INTERACTIVE THEOREM PROVING (ITP 2017)
Field
DocType
Volume
Publication,Mathematical economics,Voting,Computer science,Source code,Correctness,Popularity,Algorithm,Theoretical computer science,Computation,Formal verification,Schulze method
Conference
10499
ISSN
Citations 
PageRank 
0302-9743
2
0.45
References 
Authors
7
2
Name
Order
Citations
PageRank
Dirk Pattinson161751.32
Mukesh Tiwari252.54