Towards automatic analysis of election verifiability properties

Ben Smyth, Mark D. Ryan, Steve Kremer & Mounira Kourjieh (2010) Towards automatic analysis of election verifiability properties. In ARSPA-WITS'10: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, LNCS 6186, Springer, pp. 165-182.

See ESORICS paper.

Download

Abstract

We present a symbolic definition that captures some cases of election verifiability for electronic voting protocols. Our definition is given in terms of reachability assertions in the applied pi calculus and is amenable to automated reasoning using the software tool ProVerif. The definition distinguishes three aspects of verifiability, which we call individual, universal, and eligibility verifiability. We demonstrate the applicability of our formalism by analysing the protocols due to Fujioka, Okamoto & Ohta and a variant of the one by Juels, Catalano & Jakobsson (implemented as Civitas by Clarkson, Chong & Myers).

Bibtex Entry

@inproceedings{2010-towards-verifiability-definition-for-electronic-voting,
	author = "Ben Smyth and Mark D. Ryan and Steve Kremer and Mounira Kourjieh",
	title = "{Towards automatic analysis of election verifiability properties}",
	year = "2010",
	booktitle = "ARSPA-WITS'10: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security",
	publisher = "Springer",
	series = "LNCS",
	volume = "6186",
	pages = "165--182",
	doi = "10.1007/978-3-642-16074-5_11",
}