
	Information Technology Journal
	Year: 2011 \| Volume: 10 \| Issue: 2 \| Page No.: 293-334 DOI: 10.3923/itj.2011.293.334

Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif

Bo Meng

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.

PDF Fulltext XML References Citation Report Citation

RELATED ARTICLES:

•	Automatic Formal Framework of Coercion-resistance in Internet Voting Protocols with CryptoVerif in Computational Model

•	Automated Proof of Resistance of Denial of Service Attacks in Remote Internet Voting Protocol with Extended Applied Pi Calculus

•	A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model

•	Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus

•	Applying SMV for Security Protocol Verification

•	A Secure Non-Interactive Deniable Authentication Protocol with Strong Deniability Based on Discrete Logarithm Problem and its Application on Internet Voting Protocol

•	A Critical Review of Receipt-Freeness and Coercion-Resistance

How to cite this article:

Bo Meng , 2011. Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif. Information Technology Journal, 10: 293-334.

DOI: 10.3923/itj.2011.293.334

URL: https://scialert.net/abstract/?doi=itj.2011.293.334

COMMENT ON THIS PAPER

Navigation


		Online First
		Current Issue
		Previous Issues
		Editorial Board
		Submit a Manuscript
		Guide to Authors
		Subscribe to E-alerts

Indexed In


		ASCI-Database
		Asian Digital Library
		Google Scholar

Science Alert