Subscribe Now Subscribe Today
Science Alert
Curve Top
Information Technology Journal
  Year: 2010 | Volume: 9 | Issue: 8 | Page No.: 1521-1556
DOI: 10.3923/itj.2010.1521.1556
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model

Bo Meng, Wei Huang and Jun Qin

Soundness and coercion resistance are the important and intricate security requirements for remote voting protocols. In this study firstly the review of the formal methods of security protocols is introduced, then applied pi calculus and the automatic tool ProVerif are examined. Thirdly Meng et al. protocol recently proposed is modeled in applied pi calculus. Finally soundness and coercion resistance are verified with automatic tool ProVerif. The result we obtain is that Meng et al. protocol has coercion resistance. But it has not soundness because ProVerif found an attack on soundness. Finally the improvement of Meng et al. protocol is proposed and also modeled in applied pi calculus and automatically analyzed in ProVerif. The result we get is that the improvement of protocol has soundness. To our best knowledge, the first automated analysis of Meng et al. protocol for an unbounded number of honest and corrupted voters is finished.
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
  •    Refinement of Mechanized Proof of Security Properties of Remote Internet Voting Protocol in Applied PI Calculus with Proverif
  •    A Survey on Analysis of Selected Cryptographic Primitives and Security Protocols in Symbolic Model and Computational Model
  •    Applying SMV for Security Protocol Verification
  •    Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus
  •    A Critical Review of Receipt-Freeness and Coercion-Resistance
  •    A Secure Non-Interactive Deniable Authentication Protocol with Strong Deniability Based on Discrete Logarithm Problem and its Application on Internet Voting Protocol
How to cite this article:

Bo Meng, Wei Huang and Jun Qin, 2010. Automatic Verification of Security Properties of Remote Internet Voting Protocol in Symbolic Model. Information Technology Journal, 9: 1521-1556.

DOI: 10.3923/itj.2010.1521.1556






Curve Bottom