ISSN : 1796-203X
Volume : 4    Issue : 3    Date : March 2009

A Formal Logic Framework for Receipt-freeness in Internet Voting Protocol
Bo Meng
Page(s): 184-192
Full Text:
PDF (208 KB)

The practical Internet voting protocols should have: privacy, completeness, soundness,
unreusability, fairness, eligibility, and invariableness, universal verifiability, receipt-freeness,
coercion-resistant. Receiptfreeness is a key property. Receipt-freeness means that the voter can't
produce a receipt to prove that he votes a special ballot. Its purpose is to protect against vote buying.
Formal method is an important tool to assess receipt-freeness of Internet voting protocols. In this
paper we give a formal logic framework for receipt-freeness based on V. Kessler and H. Neumann
logic. The framework is then applied to analyze receipt-freeness of two typical voting protocols: FOO
and Meng Internet voting protocol.

Index Terms
logic framework, internet voting protocol, formal method, receipt-freeness, protocol security,
electronic government