Analysis of an Electronic Boardroom Voting System

  • Mathilde Arnaud
  • Véronique Cortier
  • Cyrille Wiedling
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7985)


We study a simple electronic boardroom voting system. While most existing systems rely on opaque electronic devices, a scientific committee of a research institute (the CNRS Section 07) has recently proposed an alternative system. Despite its simplicity (in particular, no use of cryptography), each voter can check that the outcome of the election corresponds to the votes, without having to trust the devices.

In this paper, we present three versions of this system, exhibiting potential attacks. We then formally model the system in the applied pi-calculus, and prove that two versions ensure both vote correctness (even if the devices are corrupted) and ballot secrecy (assuming the devices are honest).


Ballot Secrecy Boardroom Voting Correctness Formal Methods 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th ACM Symp. on Principles of Programming Languages (POPL 2001), pp. 104–115 (2001)Google Scholar
  2. 2.
    Adida, B.: Helios: web-based open-audit voting. In: 17th Conference on Security Symposium, SS 2008, pp. 335–348. USENIX Association (2008)Google Scholar
  3. 3.
    Benaloh, J., Tuinstra, D.: Receipt-free secret-ballot elections. In: Proceedings of the 26th Annual ACM Symposium on Theory of Computing (STOC 1994), pp. 544–553. ACM (1994)Google Scholar
  4. 4.
    Bernhard, D., Cortier, V., Pereira, O., Warinschi, B.: Measuring vote privacy, revisited. In: 19th ACM Conference on Computer and Communications Security (CCS 2012), Raleigh, USA. ACM (October 2012)Google Scholar
  5. 5.
    Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: Toward a secure voting system. In: 2008 IEEE Symposium on Security and Privacy, pp. 354–368 (2008)Google Scholar
  6. 6.
    Cortier, V., Smyth, B.: Attacking and fixing Helios: An analysis of ballot secrecy. In: 24th IEEE Computer Security Foundations Symposium (CSF 2011), pp. 297–311 (2011)Google Scholar
  7. 7.
    Cortier, V., Wiedling, C.: A formal analysis of the norwegian E-voting protocol. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol. 7215, pp. 109–128. Springer, Heidelberg (2012)CrossRefGoogle 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.
    Feldman, A., Halderman, A., Felten, E.: Security Analysis of the Diebold AccuVote-TS Voting Machine. In: 2007 USENIX/ACCURATE Electronic Voting Technology Workshop, EVT 2007 (2007)Google Scholar
  10. 10.
    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
  11. 11.
    Groth, J.: Efficient maximal privacy in boardroom voting and anonymous broadcast. In: Juels, A. (ed.) FC 2004. LNCS, vol. 3110, pp. 90–104. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  12. 12.
    Hao, F., Ryan, P.Y.A., Zielinski, P.: Anonymous voting by two-round public discussion. IET Information Security 4(2), 62–67 (2010)CrossRefGoogle Scholar
  13. 13.
    Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. 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. 37–63. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  14. 14.
    Kremer, S., Ryan, M.D., 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
  15. 15.
    Küsters, R., Truderung, T., Vogt, A.: Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study. In: IEEE Symposium on Security and Privacy (S&P 2011), pp. 538–553. IEEE Computer Society (2011)Google Scholar
  16. 16.
    Küsters, R., Truderung, T., Vogt, A.: Clash Attacks on the Verifiability of E-Voting Systems. In: IEEE Symposium on Security and Privacy (S&P 2012), pp. 395–409. IEEE Computer Society (2012)Google Scholar
  17. 17.
    Liu, J.: A proof of coincidence of labeled bisimilerity and observational equivalence in applied pi calculus. Technical report (2011)Google Scholar
  18. 18.
    Schneier, B.: Applied Cryptography, ch. 6. John Wiley & Sons (1996)Google Scholar
  19. 19.
    Wolchok, S., Wustrow, E., Halderman, J.A., Prasad, H.K., Kankipati, A., Sakhamuri, S.K., Yagati, V., Gonggrijp, R.: Security analysis of India’s electronic voting machines. In: 17th ACM Conference on Computer and Communications Security, CCS 2010 (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Mathilde Arnaud
    • 1
  • Véronique Cortier
    • 1
  • Cyrille Wiedling
    • 1
  1. 1.LORIA - CNRSNancyFrance

Personalised recommendations