Automated Privacy Verification of Voting Systems.

Voting systems aim to provide trustworthiness in elections; however, they have always been a target of malicious behaviours due to difficulties in designing such complex systems and the enormous value of controlling the election results, causing unfair election outcome, loss of personal privacy and trust in democracy. This thesis aims to shed light on how voting systems, in particular, paper-based ones can be evaluated so as to provide a better level of confidence in their trustworthiness. This thesis advances the evaluation of the paper-based voting systems using formal methods with automated analysis. In analysis of security protocols, the formal definitions of protocol requirements need to be constructed precisely. To this end, a formal framework regarding the anonymity requirement has been given and demonstrated to be appropriate for the analysis of voting systems. Similarly, it has been demonstrated that the assumptions under which voting systems are secure should be well-defined for a rigorous security analysis with the automated analysis of the ThreeBallot voting system. Moreover, a novel approach has been proposed to analyse cryptographic voting systems under a passive attacker model using the Pret a Voter voting system as case study. Finally, an active powerful attacker has been adapted into the analysis of voting systems, and an automated formal analysis of vVote voting system has been conducted, which is under development for use in Victorian Electoral Commission (VEC) elections, Australia in 2014. With the analyses of voting systems performed in this thesis, the formal approach developed here has been demonstrated to be successful in the automated analysis of such complex systems using the process algebra, Communicating Sequential Processes (CSP), and the model checker, Failures-Divergence Refinement (FDR)