Florence Verity's 2016 honours thesis in mathematics, on "Electronic vote counting as mathematical proof", supervised by
Dirk Pattinson and
Scott Morrison, is available here.
Abstract
Electronic vote counting is replacing manual counting, and with this comes the problem of verification to provide trust in the outcome of an electronic count. In this thesis, I explain and build on the 'vote counting as mathematical proof' approach to the problem by first presenting the underpinning theory of proofs and types. I then prove that the formalisation of a particular vote counting protocol under this approach satisfies the majority criterion. I also develop a generic approach to formalising vote counting protocols as natural deduction systems, called 'generic termination', and demonstrate that it can be readily applied to simple and real-world vote counting protocols.
Introduction
The aim of this thesis is to build on work by Pattinson in [16], which established an approach to electronic vote counting called 'vote counting as mathematical proof'. This relies on the observation that vote counting rules may be given the same status as deduction rules in proof theory. Such a rules-based formalisation may be implemented inside the interactive theorem prover Coq, allowing the extraction of a provably correct vote counting program. Along with the outcome of the count, this program produces a proof of the result in the form of a sequence of rule applications, which may then be independently verified for correctness.
In this thesis, I prove that the formalisation of a single transferable vote (STV) counting protocol in [16] satisfies the majority criterion, a mathematical property used to compare voting systems. I address the problem of abstracting the properties common to all vote counting protocols under the proof rules approach by building a generic framework. I prove that in this framework, there are properties local to the list of rules that if satisfied, ensure a provable outcome of the count. This makes it easier to implement different vote counting protocols under the mathematical proof approach, which I demonstrate by applying the framework to the first past the past (FPTP) and STV protocols in [16], as well as a more complex real-world protocol.
Chapter 1 provides the context to the problem of trust in electronic vote counting and describes the status of electronic vote counting in Australia. It introduces the approach taken in this thesis by illustrating the analogy to proof theory by formalising FPTP as deduction rules. Finally, it compares vote counting as mathematical proof to related work. Chapter 2 presents the theory of types that underpins the approach. This focuses on replacing truth conditions in natural deduction by proof conditions to get a constructive logic, which we then compare to type theory by the Curry-Howard isomorphism.
Chapter 3 describes the specification and Coq implementation of STV as proof rules, before proving that it satisfies the majority criterion. Finally, Chapter 4 develops the generic framework, called 'generic termination'. It includes the implementation of FPTP and STV inside this framework, as well as the specification and implementation of the ANU Union vote counting protocol. Appendix A gives the relevant part of the ANU Union constitution specifying the vote counting procedure that is formalised in Chapter 4.
Accompanying this thesis is Coq code of the implementations. Throughout the thesis, the definitions made and theorems proved in the code are explained, both mathematically and with snippets of code. While the nature of an interactive theorem prover means that provided the theorems have been given correctly, the proofs are correct, it is recommended to open the code and step through some of it to gain a sense of the formal proof environment. Instructions on how to do this, as well as the code, may be downloaded at https://github.com/floverity/coq-vote-counting.
