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.
Official URL: http://dx.doi.org/10.1007/978-3-642-32759-9_19
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)|
|Additional Information:||Copyright Springer-Verlag Berlin Heidelberg 2012. The original publication is available at http://www.springerlink.com|
|Divisions:||Faculty of Engineering and Physical Sciences > Computing Science|
|Deposited By:||Symplectic Elements|
|Deposited On:||17 Oct 2012 11:28|
|Last Modified:||16 Feb 2013 15:49|
Repository Staff Only: item control page