Logic and Computation Group

Formal Methods Applied to Electronic Voting Systems

Abstract: The 2000 election debacle in the USA has sparked huge interest in electronic voting. There are a multitude of risks: voter identification, vote auditing, network security and correct counting of votes to name a few. We are using formal specification and verification techniques to investigate the correctness of the electronic vote counting model used in the 2001 ACT election in Canberra, Australia. We are also developing our own vote counting system in the computer language Standard ML. These pages report on our work to date.

Table of Contents

1. Introduction and Overview
2. Formal Specification of the ACT Hare-Clark Legislation
3. A Review of the Hare-Clark Counting Module of eVACS
4. Hare-Clark Counting in the Language C
5. Hare-Clark Counting in the Language Standard ML
6. Conclusions and Further Work

Further Information

1. Contacts
2. Links

Site Map and Table of Contents  |  Disclaimer  |  Page content Copyright 2003 NICTA