Vote Counting as Mathematical Proof

8 years 11 days ago

Download users.cecs.anu.edu.au

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 certiﬁcate of the validity of the result. This eliminates the need to trust, or otherwise verify, the correctness of the vote counting software once certiﬁcate 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 veriﬁable certiﬁcates. 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

Real-time Traffic