University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Formal Framework for Modelling Coercion Resistance and Receipt Freeness

Schneider, SA and Heather, JA A Formal Framework for Modelling Coercion Resistance and Receipt Freeness In: FM 2012: 18th International Symposium on Formal Methods, 2012-08-27 - 2012-08-31.

Available under License : See the attached licence file.

Download (359kB)
PDF (licence)

Download (33kB)


Coercion resistance and receipt freeness are critical properties for any voting system. However, many di fferent de finitions of these properties have been proposed, some formal and some informal; and there has been little attempt to tie these definitions together or identify relations between them. We give here a general framework for specifying di fferent coercion resistance and receipt freeness properties using the process algebra CSP. The framework is general enough to accommodate a wide range of defi nitions, and strong enough to cover both randomization attacks and forced abstention attacks. We provide models of some simple voting systems, and show how the framework can be used to analyze these models under di fferent de finitions of coercion resistance and receipt freeness. Our formalisation highlights the variation between the defi nitions, and the importance of understanding the relations between them.

Item Type: Conference or Workshop Item (Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Contributors :
PublisherSpringer, UNSPECIFIED
Additional Information : Copyright Springer-Verlag Berlin Heidelberg 2012. The original publication is available at
Depositing User : Symplectic Elements
Date Deposited : 17 Oct 2012 10:28
Last Modified : 23 Sep 2013 19:40

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800