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.
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 (Conference Paper)|
|Divisions :||Faculty of Engineering and Physical Sciences > Computing Science|
|Additional Information :||Copyright Springer-Verlag Berlin Heidelberg 2012. The original publication is available at http://www.springerlink.com|
|Depositing User :||Symplectic Elements|
|Date Deposited :||17 Oct 2012 10:28|
|Last Modified :||23 Sep 2013 19:40|
Actions (login required)
Downloads per month over past year