Formally Verified Vote Counting: The case of Fractional Transfer Values

Research areas

Description

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. 

 

Goals

Goals.

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.

 

Requirements

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.

Background Literature

Dirk Pattinson, Carsten Schürmann: Vote Counting as Mathematical Proof. Australasian Conference on Artificial Intelligence 2015:464-475

Y. Bertot, P. Casteran, G. Huet, and C. Paulin-Mohring. Interactive theorem proving and program development : Coq’Art : the calculus of inductive constructions. Texts in theoretical computer science. Springer, 2004. 

 

 

Gain

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.

 

Keywords

electronic voting

program verification

logic

Updated:  1 November 2018/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing