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.

• Type: Journal
• Year: 2015
• Where: AUSAI
• Authors: Dirk Pattinson, Carsten Schürmann
• Keywords: Artificial Intelligence, AUSAI 2015