KIT | KIT-Bibliothek | Impressum | Datenschutz
Open Access Logo
§
Volltext
DOI: 10.5445/IR/1000042284

Formal Verification of an Electronic Voting System

Bruns, Daniel

Abstract:
Electronic voting (e-voting) systems that are used in public elections need to fulfil a broad range of strong requirements concerning both safety and security. Among these requirements are reliability, robustness, privacy of votes, coercion resistance and universal verifiability. Bugs in or manipulations of an e-voting system may have considerable influence on the life of the humans living in a country where such a system is used. Hence, e-voting systems are an obvious target for software verification.
In this paper, we report on an implementation of such a system in Java and the formal verification of functional properties thereof in the KeY verification system. Even though the actual components are clearly modularized, the challenge lies in the fact that we need to prove a highly nonlocal property: After all voters have cast their votes, the server calculates the correct votes for each candidate w.r.t. the original ballots. This kind of trace property is dificult to prove with static techniques like verification and typically yields a large specification overhead.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Forschungsbericht
Jahr 2014
Sprache Englisch
Identifikator ISSN: 2190-4782
URN: urn:nbn:de:swb:90-422842
KITopen-ID: 1000042284
Verlag Karlsruhe
Umfang 15 S.
Serie Karlsruhe Reports in Informatics ; 2014,11
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page