Under consideration for publication in Formal Aspects of Computing Verifying Anonymity in Voting Systems Using CSP

Abstract. We present formal definitions of anonymity for voting protocols using the process algebra CSP. We analyse a number of anonymity definitions, and give formal definitions for strong and weak anonymity by highlighting the difference between these definitions. We show that the strong anonymity definition is too strong, whereas the weak anonymity definition is shown to be a suitable property for analysing voting systems. We model and analyse a conventional voting system, and Prêt a ̀ Voter, a paper-based, voter-verifiable e-voting system, as two case studies to demonstrate the validity of our formal definitions by specification checks using the trace equivalence notion in CSP and the refinement checker Failures-Divergences Refinement (FDR2). We give a detailed discussion on the results from the analysis, emphasizing the assumptions that we made in our model as well as the challenges in modelling electronic voting systems using CSP