Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus
Title:
Formal Analysis of Key Properties in the Internet Voting Protocol Using Applied Pi Calculus
Author:
Bo Meng
Appeared in:
Information technology journal
Paging:
Volume 7 (2008) nr. 8 pages 1133-1140
Year:
2008
Contents:
The internet voting protocols is the core part of the internet voting system. In order to put the internet voting protocols into practice they should have several key properties, such as privacy, completeness, soundness, unreusability, fairness, eligibility and invariableness, universal verifiability, receipt-freeness and coercion-resistance. Formal method is an important tool to assess these properties. But most of these properties are analyzed with informal method. The applied pi calculus can be used to model and verify the security protocols, such as internet voting protocol. In this study, firstly, privacy and coercion-resistance properties are researched. Then a typical internet voting protocol is modeled with applied pi calculus. Thirdly privacy and coercion-resistance of the typical internet voting protocol are analyzed with applied pi calculus. According to the result of analysis the typical internet voting protocol has privacy and coercion-resistance properties.
Publisher:
Asian Network for Scientific Information, Pakistan (provided by DOAJ)
Journal description