Refinement of mechanized proof of security properties of remote internet voting protocol in applied PI calculus with proverif

Abstract

Secure remote internet voting protocols play an important role in electronic government. In order to assess its claimed security, several formal models of soundness and coercion-resistance have been proposed in the past literatures, but these formal models are not supported by mechanized tools. Recently, Backes et al. propose a new mechanized formal model of security properties including soundness and coercion-resistance in applied PI calculus. Acquisti protocol is one of the most important remote internet voting protocols that claims to satisfy formal definitions of key properties without strong physical constrains. But in the study the analysis of its claimed security is finished by hand. Owning to the contribution of Backes et al., Acquisti protocol can be analyzed with mechanized tool. In this study, firstly the review of the formal analysis of electronic voting protocols are introduced we can find that the formal model and analysis of security properties mainly focus on receipt-freeness and coercion-resistance. Until now the security analysis model based on computational model have not been proposed; then applied PI calculus and the mechanized proof tool ProVerif are examined. After that Acquisti protocol is modeled in applied PI calculus. Finally security properties, including soundness and coercion resistance, are proved with ProVerif, a resolution-based mechanized theorem prover for security protocols. The result we obtain is that Acquisti protocol has the soundness and coercion- resistance in some conditions. To our best knowledge, the first mechanized proof of Acquisti protocol for an unbounded number of honest and corrupted voters is presented. © 2011 Asian Network for Scientific Information.