## Abstract

Trust in the correctness of an election outcome requires

proof of the correctness of vote counting. By formalising

particular voting protocols as rules, correctness of vote counting

amounts to

verifying 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 an

independently checkable certificate of the validity of the result.

This reduces

the need to trust, or otherwise verify, the

correctness of the vote counting software once the certificate has

been validated. Using a rule-based formalisation of voting

protocols inside a theorem prover, we synthesise vote counting

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

a set of given rules.

proof of the correctness of vote counting. By formalising

particular voting protocols as rules, correctness of vote counting

amounts to

verifying 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 an

independently checkable certificate of the validity of the result.

This reduces

the need to trust, or otherwise verify, the

correctness of the vote counting software once the certificate has

been validated. Using a rule-based formalisation of voting

protocols inside a theorem prover, we synthesise vote counting

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

a set of given rules.

Original language | English |
---|---|

Title of host publication | Proceedings of 28th Australasian Joint Conference on Artificial Intelligence |

Editors | Bernhard Pfahringer, Jochen Renz |

Number of pages | 11 |

Volume | LNAI 9457 |

Place of Publication | Canberra |

Publisher | Springer |

Publication date | 1 Dec 2015 |

Edition | 2015 |

Pages | 464-475 |

ISBN (Print) | 978-3-319-26349-6 |

ISBN (Electronic) | 978-3-319-26350-2 |

Publication status | Published - 1 Dec 2015 |

## Keywords

- Election trust
- Vote counting verification
- Rule-based protocols
- Theorem proving
- Independently verifiable certificates