Formalization &Analysis of Electronics Voting Protocols by using Applied PI Calculus

Abstract

In this paper we report recent work on analysis of protocols in remote electronics voting protocols. A potentially much more secure system could be implemented, based on formal protocols that specify the messages sent to electronics voting machines.Protocols which were thought to be correct for several years have, by means of formal verification techniques, been discovered to have major flaws [1, 2]. Our aim is to use verification techniques to analyze the protocol. We model it in the applied pi calculus [3], which has the advantages of being based on well-understood concepts.