Sciweavers

AUSAI
2015
Springer

Vote Counting as Mathematical Proof

8 years 6 months ago
Vote Counting as Mathematical Proof
Trust in the correctness of an election outcome requires proof of the correctness of vote counting. By formulating particular voting protocols as rules, correctness amounts to demonstrating that all rules have been applied correctly. A proof of the outcome of any particular election then consists of a sequence (or tree) of rule applications and provides and independently checkable certificate of the validity of the result. This eliminates the need to trust, or otherwise verify, the correctness of the vote counting software once certificate has been validated. Using a rule-based formalisation of voting protocols inside a theorem prover, we synthesise vote coating programs that are not only provably correct, but also produce independently verifiable certificates. These programs are generated from a (formal) proof that every initial set of ballots allows to decide the election winner according to the given rules.
Dirk Pattinson, Carsten Schürmann
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where AUSAI
Authors Dirk Pattinson, Carsten Schürmann
Comments (0)