Submit Manuscript

Information Technology Journal

Year: 2012 | Volume: 11 | Issue: 7 | Page No.: 741-750
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail

Article Trend

Total views 104

Authors

Bo Meng

Keywords

Research Article

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

Bo Meng
Automatic proof for internet voting protocols is a hotspot issue in security protocol world. To our best knowledge, until now analysis of coercion-resistance and internet voting protocols with automatic tool in computational model does not exist. So in this study, we initiatively proposed the automatic framework of coercion-resistance and internet voting protocols based on computational model with active adversary. In the proposed framework observational equivalence is used to formalize coercion-resistance. At the same time we propose a method to prove the observational equivalence between the two processes have the same structure and differ only by the terms and term evaluations with mechanized tool CryptoVerif. Based on the proposed method to prove with CryptoVerif the observational equivalence, the proposed mechanized framework can be used to automatically analyze coercion-resistance of internet voting protocols with CryptoVerif.
PDF Fulltext XML References Citation

Leave a Comment

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