Submit Manuscript

Information Technology Journal

Year: 2010 | Volume: 9 | Issue: 8 | Page No.: 1521-1556
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Article Trend

Total views 165

Authors

Bo Meng

Wei Huang

Jun Qin

Keywords

Research Article

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

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
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

Leave a Comment

Your email address will not be published. Required fields are marked *