Development of A Formal Security Model for Electronic Voting Systems

Development of A Formal Security Model for Electronic Voting Systems

Katharina Bräunlich (Department of Information Systems Research, University of Koblenz-Landau, Koblenz, Germany) and Rüdiger Grimm (Department of Information Systems Research, University of Koblenz-Landau, Koblenz, Germany)
Copyright: © 2013 |Pages: 28
DOI: 10.4018/jisp.2013040101
OnDemand PDF Download:
List Price: $37.50
10% Discount:-$3.75


Trust that an electronic voting system realizes the security requirements in an adequate manner is an essential premise for electronic elections. Trust in a system can be achieved by controlling the system security. There are two ways to assure system security. One way is the evaluation and certification of the implementation’s security by neutral experts. Another way is the verification of the outcome by the users. Both approaches, verification and certification, should be combined to reasonably justify the voter’s trust in the electronic voting system. In this paper a formal security model with respect to the requirements of Fairness, Eligibility, Secrecy and Receipt-Freeness, Verifiability and Protection against Precipitation is given. This formal model helps to clarify and truly understand these requirements. Furthermore, it can be used for the evaluation and certification of online voting products according to the Common Criteria.
Article Preview


Security is an elementary property of electronic voting systems. Security objectives for electronic voting were first collected in an informal way, for example by a European-wide accepted recommendation adopted by the Council of Europe (Council of Europe, 2004). Later the semi-formal method of the Common Criteria (CC) (Common Criteria, 2006) was used to specify a basic set of security requirements for online voting products (Volkamer & Vogt, 2008). Furthermore, the method KORA (Konkretisierung rechtlicher Anforderungen/Concretisation of Legal Requirements) (Hammer, Pordesch, & Roßnagel, 1993) was used to derive security objectives for electronic voting from legal specifications (Bräunlich, Grimm, Richter, & Roßnagel, 2013).

Besides their differences, there is common agreement that the following security objectives have to be granted by an electronic voting system:

  • Fairness: Each voter can cast exactly one vote and no voter loses his voting right without having cast a vote.

  • Eligibility: Only eligible voters who are unmistakeably identified and authenticated are allowed to cast a vote that is stored in the ballot box.

  • Protection Against Precipitation: The voter can abort his voting process at any time prior to the final casting of the vote without losing his right to vote and there is no limit on the number of corrections a voter can make to his vote until the final casting of the vote.

  • Secrecy and Receipt-Freeness: The voter's voting decision must be kept secret (ballot secrecy) and must be enforced even against the voter himself (receipt-freeness). I.e. the voter does not gain any information that enables him to prove his voting decision to others. By hiding a voter's voting decision, the voter is protected against unlawful influence.

In the context of electronic voting, it is necessary that the voters have trust in the system security of the electronic voting system. One way to strengthen the trust of the voters in the electronic voting system is the assurance of system security by means of verifiability.

  • Verifiability: To grant traceability of the whole voting procedure, so called end-to-end-verifiability (Adida & Neff, 2006), the essential steps of an election must be open for examination by the voter. The essential steps are the marking and encryption of the vote, the casting of the encrypted vote (=ballot) and the counting of the ballots from the ballot box, or more precisely:

    • o

      Cast-As-Intended: The voter can ascertain himself that the ballot is correctly encrypted and represents his voting decision correctly. In order to protect ballot secrecy, cast-as-intended can only be verified by the voter himself. It can be verified by the voter only before the ballot has been cast into the ballot box. Because otherwise, this verification functionality could be used by an attacker to reveal the voter's voting decision.

    • o

      Recorded-as-Cast: The voter can retrace that his ballot is correctly transmitted and stored in the ballot box. In order to protect receipt-freeness, recorded-as-cast has to be implemented such that the voter cannot prove his voting decision (to others). The verification of recorded-as-cast can take place directly after the ballot casting or after the voting phase.

    • o

      Counted-as-Recorded: The voter as well as the broad public can verify the election result. I.e. it has to be verifiable that all ballots from the ballot box are counted-as-recorded.

Complete Article List

Search this Journal:
Volume 17: 1 Issue (2023): Forthcoming, Available for Pre-Order
Volume 16: 4 Issues (2022): 2 Released, 2 Forthcoming
Volume 15: 4 Issues (2021)
Volume 14: 4 Issues (2020)
Volume 13: 4 Issues (2019)
Volume 12: 4 Issues (2018)
Volume 11: 4 Issues (2017)
Volume 10: 4 Issues (2016)
Volume 9: 4 Issues (2015)
Volume 8: 4 Issues (2014)
Volume 7: 4 Issues (2013)
Volume 6: 4 Issues (2012)
Volume 5: 4 Issues (2011)
Volume 4: 4 Issues (2010)
Volume 3: 4 Issues (2009)
Volume 2: 4 Issues (2008)
Volume 1: 4 Issues (2007)
View Complete Journal Contents Listing