Reference : A Modular Multi-Modal Specification of Real-Timed, End-To-End Voter-Verifiable Voting...
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/25976
A Modular Multi-Modal Specification of Real-Timed, End-To-End Voter-Verifiable Voting Systems
English
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) >]
2011
2011 International Workshop on Requirements Engineering for Electronic Voting Systems (REVOTE)
IEEE
9 - 21
Yes
International
978-1-4577-0951-7
REVOTE
29-08-2011
Trento
Italy
[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)
[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.
http://hdl.handle.net/10993/25976
10.1109/REVOTE.2011.6045911
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):

FileCommentaryVersionSizeAccess
Limited access
06045911.pdfPublisher postprint219.52 kBRequest a copy

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.