A Formal Model for the Requirement of Verifiability in Electronic Voting by Means of a Bulletin Board

  • Katharina Bräunlich
  • Rüdiger Grimm
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7985)


Trust in an electronic voting system is an essential premise for electronic elections. Trust in a system can be strengthened by controlling its correct functioning. There are two ways to assure the correct functioning of a system. Firstly, before using a system, neutral experts can evaluate and certify the security of its implementation. Secondly, while using the system, its users can verify its outcome by appropriate verification tools. Verifiability is a specific security function, which is subject to certification itself. This paper presents a formal security requirements model for the verifiability of electronic voting systems by means of a Bulletin Board that publishes all important communication steps without violating the secrecy of voting.


Electronic Voting Verifiability Formal Specification Common Criteria IT System Evaluation and Certification Bulletin Board 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Adida, B., Neff, C.: Ballot casting assurance. In: USENIX/Accurate Electronic Voting Technology Workshop, p. 7. USENIX Association, Berkeley (2006)Google Scholar
  2. 2.
    Volkamer, M., Schryen, G., Langer, L., Schmidt, A., Buchmann, J.: Elektronische Wahlen: Verifizierung vs. Zertifizierung. In: GI Jahrestagung, pp. 1827–1836 (2009)Google Scholar
  3. 3.
    Common criteria for information technology security evaluation, and common methodology for information technology security evaluation, version 3.1 (2006)Google Scholar
  4. 4.
    Volkamer, M., Vogt, R.: Common criteria protection profile for basic set of security requirements for online voting products. BSI-CC-PP-0037, Version 1.0 (April 18, 2008), (May 02, 2013)
  5. 5.
    Mantel, H., Stephan, W., Ullmann, M., Vogt, R.: Guideline for the development and evaluation of formal security policy models in the scope of itsec and common criteria. BSI, DFKI, Tech. Rep. (2004)Google Scholar
  6. 6.
    Benaloh, J.D.C.: Verifiable secret-ballot elections. Ph.D. dissertation, Yale University, Department of Computer Science, Technical Report number 561 (1987)Google Scholar
  7. 7.
    Bräunlich, K., Grimm, R.: Formalization of receipt-freeness in the context of electronic voting. In: ARES, pp. 119–126 (2011)Google Scholar
  8. 8.
    Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), 435–487 (2009)Google Scholar
  9. 9.
    Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proc. IAVoSS Workshop on Trustworthy Elections (2006)Google Scholar
  10. 10.
    Jonker, H.L., de Vink, E.P.: Formalising receipt-freeness. In: Katsikas, S.K., López, J., Backes, M., Gritzalis, S., Preneel, B. (eds.) ISC 2006. LNCS, vol. 4176, pp. 476–488. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    Kremer, S., Ryan, M.: Analysis of an electronic voting protocol in the applied pi calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF, pp. 195–209 (2008)Google Scholar
  13. 13.
    Grimm, R., Hupf, K., Volkamer, M.: A Formal IT-Security Model for the Correction and Abort Requirement on Electronic Voting. In: EVOTE (2010)Google Scholar
  14. 14.
    Volkamer, M., Grimm, R.: Development of a formal it security model for remote electronic voting systems. In: Electronic Voting, pp. 185–196 (2008)Google Scholar
  15. 15.
    Bohli, J.-M., Müller-Quade, J., Röhrich, S.: Bingo voting: Secure and coercion-free voting using a trusted random number generator. In: Alkassar, A., Volkamer, M. (eds.) VOTE-ID 2007. LNCS, vol. 4896, pp. 111–124. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Chaum, D., Ryan, P.Y.A., Schneider, S.: A practical voter-verifiable election scheme. In: De Capitani di Vimercati, S., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 118–139. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  17. 17.
    Popoveniuc, S., Hosp, B.: An introduction to punchScan. In: Chaum, D., Jakobsson, M., Rivest, R.L., Ryan, P.Y.A., Benaloh, J., Kutylowski, M., Adida, B. (eds.) Towards Trustworthy Elections. LNCS, vol. 6000, pp. 242–259. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  18. 18.
    Ryan, P.Y.A., Peacock, T.: Prêt-à-voter: A Systems Perspective. Technical Report CS-TR 929, School of Computing Science, Newcastle University (2005)Google Scholar
  19. 19.
    Baskar, A., Ramanujam, R., Suresh, S.P.: Knowledge-based modelling of voting protocols. In: TARK, pp. 62–71 (2007)Google Scholar
  20. 20.
    Talbi, M., Morin, B., Tong, V.V.T., Bouhoula, A., Mejri, M.: Specification of electronic voting protocol properties using ADM logic: FOO case study. In: Chen, L., Ryan, M.D., Wang, G. (eds.) ICICS 2008. LNCS, vol. 5308, pp. 403–418. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  21. 21.
    Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  22. 22.
    Jonker, H., Pang, J.: Bulletin boards in voting systems: Modelling and measuring privacy. In: ARES. IEEE Computer Society Press (2011)Google Scholar
  23. 23.
    Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  24. 24.
    Dolev, D., Yao, A.C.: On the Security of Public Key Protocols. In: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, pp. 350–357. IEEE Computer Society, Washington, DC (1981)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Katharina Bräunlich
    • 1
  • Rüdiger Grimm
    • 1
  1. 1.Department of Computer ScienceUniversity of Koblenz-LandauKoblenzGermany

Personalised recommendations