Formal Verification of Trustworthy Voting Systems
- When?
- Tuesday 31 May 2011, 11:00 to 12:00
- Where?
- 39BB02
- Open to:
- Staff, Students
- Speaker:
- Mr Murat Moran
Fair elections are essential processes in ideal representative democracies since ancient Greece. Thus, as being an indispensable part of fair elections, a various number of trustworthy voting systems has been designed and improved over decades. However, due to insufficient amount of proofs, the lack of trustworthiness of such systems still precipitates quite a number of system attacks violating citizens' privacy, modifying election results, which have as a consequence controversial elections and unfair democracies.
This work aims to give precise characterisations of desired trustworthy voting system properties, i.e. anonymity, receipt-freeness, coercion-resistance, individual and universal verifiability, and fairness by analysing and providing a numerous literature on these properties. In particular, we modelled conventional voting system (CVS) and conducted a formal verification of CVS with respect to anonymity as specification using the process algebra Communicating Sequential Processes (CSP) and Failures-Divergences Refinement (FDR2) model checker. We also experimented that different formal anonymity definitions gave different results about the systems' behaviour. For instance, we showed through our analysis that CVS is an anonymous voting system with respect to the weak anonymity definition but is not defined as strongly anonymous according to the strong anonymity definition. The results from our work demonstrated that the framework of the desired properties need to be defined carefully and precisely along with the formal analysis of existing voting systems, Prêt à Voter, ThreeBallot and Scantegrity II, which are claimed to satisfy certain properties. In order to achieve our objectives we also presented a wide range of different definitions of the properties, whose frameworks are being planned to construct, and gave a strong literature review of these trustworthy voting systems to be formalised and the attacks that have been exploited on them, so far.
