TY - GEN
T1 - Schulze voting as evidence carrying computation
AU - Pattinson, Dirk
AU - Tiwari, Mukesh
N1 - Publisher Copyright:
© 2017, Springer International Publishing AG.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85029506121&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-66107-0_26
DO - 10.1007/978-3-319-66107-0_26
M3 - Conference contribution
SN - 9783319661063
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 410
EP - 426
BT - Interactive Theorem Proving - 8th International Conference, ITP 2017,Proceedings
A2 - Munoz, Cesar A.
A2 - Ayala-Rincon, Mauricio
PB - Springer Verlag
T2 - 8th International Conference on Interactive Theorem Proving, ITP 2017
Y2 - 26 September 2017 through 29 September 2017
ER -