This dissertation argues that a property based approach is the best start towards a fully verified voting system. First, we look at specific techniques to reduce privacy vulnerabilities in a range of voting technologies. We implement our techniques in a prototype voting system. The componentised design of the voting system makes it amenable to easily validating security properties. Finally, we describe software analysis techniques that guarantee that ballots will only be stored if they can later be accurately reconstructed for counting. The analysis uses static analysis to enable dynamic checks in a fail-stop model.

These successes provide strong evidence that it is possible to design voting systems with verifiable security properties, and the belief that in the future, voting technologies will be free of security problems.