Background.

Formally verified vote counting is a crucial aspect of building trust in electronic elections. More precisely, we seek tallying algorithms that are universally verifiable so that any member of the general public, or political party, can satisfy themselves that the count was conducted correctly. That is, in addition to the outcome of the tallying process, we also produce an independently verifiable certificate that attests to the correctness of the count. This was exemplified with two voting schemes, and the goal of this project is to examine to what extent this can be applied to real-world voting protocols. 

Technical Content.

To give a formalisation of the voting protocol used by the ANU students union (single transferable vote) and to produce a provaby correct program that counts votes according to this scheme. To formally etablish properties of this variant of single transferable vote in a theorem prover.

Skills gained.

Exposure to real-world voting protocols. A good working knowledge of formal theorem proving. Familiarity with logic and type theory beyond what is being offered at course level.

Skills required.

A good understanding and working knowledge of first-order logic, as for example discussed in COMP2600 (Formal Methods in Software Engineering) or equivalent.