Science Alert
Curve Top
Information Technology Journal
  Year: 2011 | Volume: 10 | Issue: 2 | Page No.: 293-334
DOI: 10.3923/itj.2011.293.334
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

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

Bo Meng

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
  •    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
  •    Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model
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






Curve Bottom