Reference : A Modular Multi-Modal Specification of Real-Timed, End-To-End Voter-Verifiable Voting...

	Document type :	Scientific congresses, symposiums and conference proceedings : Paper published in a book
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/25976

Title :	A Modular Multi-Modal Specification of Real-Timed, End-To-End Voter-Verifiable Voting Systems
Language :	English
Author, co-author :	Kramer, Simon [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > > ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)]
	Ryan, Peter [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Publication date :	2011
Main document title :	2011 International Workshop on Requirements Engineering for Electronic Voting Systems (REVOTE)
Publisher :	IEEE
Pages :	9 - 21
Peer reviewed :	Yes
Audience :	International
ISBN :	978-1-4577-0951-7
Event name :	REVOTE
Event date :	29-08-2011
Event place (city) :	Trento
Event country :	Italy
Keywords :	[en] accountability (including auditability) ; applied modal logic ; formal requirements engineering ; real-timed distributed and multi-agent systems ; trustworthy, remote and/or ballot-box electronic voting (including electronic elections)
Abstract :	[en] We propose a modular multi-modal specification of real-timed, end-to-end voter-verifiable voting systems, i.e., a formal but intuitive specification of real-timed voting systems that are accountable (and thus trustworthy) to their users. Our specification is expressed as a single but well-compounded formula in a logical language of temporal, epistemic, and provability modalities. The intuitiveness of the specification is the fruit of its modular and multi-modal form. This means that the specification can be appreciated compound-wise, as a logical conjunction of separate sub-requirements, each of which achieving the ideal of a formal transcription of a suitable natural-language formulation, thanks to powerful descriptive idioms in the form of our multiple modalities. The modular form reduces our proof of the satisfiability (consistency) and thus implementability of the specification to a proof by inspection, and induces the parallelisability of implementation-correctness verifications. The specification also pinpoints the implementation-specific part of particular voting systems, reuses a generic definition of accountability inducing trust in a formal sense, and, last but not least, counter-balances by its implementability some previous results about the contradictory conjunction of certain desirable property pairs of voting systems. So in some sense, ideal voting systems do exist. Our specific formalisation principles are agent correctness, i.e., the behavioural correctness of the voting-system-constituting agents, and data adequacy, i.e., the soundness and (relative) completeness of the voting data processed by the system.
Permalink :	http://hdl.handle.net/10993/25976
DOI :	10.1109/REVOTE.2011.6045911
Commentary :	Simon Kramer’s contribution was funded with Grant AFR 894328 from the National Research Fund, Luxembourg cofunded under the Marie-Curie Actions of the European Commission (FP7-COFUND), and written during an invited stay at the Institute of Mathematical Sciences, Chennai, India. Proceedings of the RE-affiliated Workshop on Requirements Engineering for Electronic Voting Systems

	File(s) associated to this reference
	Fulltext file(s): File Commentary Version Size Access Limited access 06045911.pdf Publisher postprint 219.52 kB Request a copy

All documents in ORBi^lu are protected by a user license.

 

University of Luxembourg Library |  Feedback |  Legal notices Site Map