文章基本信息

标题：Automatic Verification of Remote Internet Voting Protocol in Symbolic Model
本地全文：下载
作者：Meng, Bo ; Huang, Wei ; Wang, Dejun 等
期刊名称：Journal of Networks
印刷版ISSN：1796-2056
出版年度：2011
卷号：6
期号：9
页码：1262-1271
DOI：10.4304/jnw.6.9.1262-1271
语种：English
出版社：Academy Publisher
摘要：Acquisti protocol is one of the leading remote internet voting protocols that claims to satisfy formal definitions of key properties, such as soundness, individual verifiability, receipt-freeness and coercion resistance without strong physical constrains. But the analysis of its claimed security properties is finished in manual way which depends on experts’ knowledge and skill and is prone to make mistakes. In this paper firstly the review of the formal method of security protocols is presented. Secondly Acquisti protocol is modeled in applied pi calculus. Finally soundness and coercion-resistance are verified with the automatic tool ProVerif. The result shows that Acquisti protocol has the soundness and coercion-resistance in some conditions. To our best knowledge, the first automatic analysis of Acquisti protocol for an unbounded number of honest and corrupted voters is provided.
关键词：automatic proof; remote internet voting; applied pi calculus; ProVerif; protocol security