A Formal Analysis of Coercion-Resistance of the Internet Voting Protocol Based on DKR Formal Model

The practical Internet voting protocols should have: privacy, completeness, soundness, unreusability, fairness, eligibility, invariableness, universal verifiability, receipt-freeness and coercion-resistance. Formal method is an important tool to assess coercion-resistance of internet voting protocols. But the coercion-resistance of many Internet voting protocols is analyzed without formal method. The applied pi calculus can be used to model and verify the security protocols, such as internet voting protocol. In this paper, firstly, we research the coercion-resistance . Then we model a typical internet voting protocol with applied pi calculus. Thirdly we analyze the typical internet voting protocol with DKR coercion-resistance formal model. According to the result of analysis we point out that the typical protocol is coercion-resistance.