Verification of STAR-Vote and Evaluation of FDR and ProVerif

  • Murat MoranEmail author
  • Dan S. Wallach
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


We present the first automated privacy analysis of STAR-Vote, a real world voting system design with sophisticated “end-to-end” cryptography, using FDR and ProVerif. We also evaluate the effectiveness of these tools. Despite the complexity of the voting system, we were able to verify that our abstracted formal model of STAR-Vote provides ballot-secrecy using both formal approaches. Notably, ProVerif is radically faster than FDR, making it more suitable for rapid iteration and refinement of the formal model.


Security protocols Formal methods Privacy E-voting STAR-Vote FDR ProVerif 



This work was carried out under the NSF-funded Voting Systems Architectures for Security and Usability project. The principal author is also partly funded by TUBITAK. We would like to thank Ben Smyth, Olivier Pereira, and Thomas Gibson-Robinson for their helpful technical discussions.


  1. 1.
    Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005). doi: 10.1007/11513988_27 CrossRefGoogle Scholar
  2. 2.
    Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF (2008)Google Scholar
  3. 3.
    Benaloh, J.: Simple verifiable elections. In: Proceedings of the USENIX/ACCURATE Electronic Voting Technology Workshop (EVT 2006), Vancouver, B.C., Canada, June 2006Google Scholar
  4. 4.
    Benaloh, J., Byrne, M., Kortum, P.T., McBurnett, N., Pereira, O., Stark, P.B., Wallach, D.S.: STAR-Vote: a secure, transparent, auditable, and reliable voting system. CoRR, abs/1211.1904 (2012)Google Scholar
  5. 5.
    Blanchet, B., Smyth, B.: Automated reasoning for equivalences in the applied pi calculus with barriers. In: CSF (2016)Google Scholar
  6. 6.
    Boichut, Y., Heam, P.C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Workshop on Automated Verification of Infinite States Systems (2004)Google Scholar
  7. 7.
    Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-28869-2_6 CrossRefGoogle Scholar
  8. 8.
    Chothia, T., Smyth, B., Staite, C.: Automatically checking commitment protocols in ProVerif without false attacks. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 137–155. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46666-7_8 Google Scholar
  9. 9.
    Cortier, V., Eigner, F., Kremer, S., Maffei, M., Wiedling, C.: Type-based verification of electronic voting protocols. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 303–323. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46666-7_16 Google Scholar
  10. 10.
    Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-70545-1_38 CrossRefGoogle Scholar
  11. 11.
    Cremers, C.J.F., Lafourcade, P., Nadeau, P.: Comparing state spaces in automatic security protocol analysis. In: Formal to Practical Security - Papers Issued from the 2005–2008 French-Japanese Collaboration (2009)Google Scholar
  12. 12.
    Dalal, N., Shah, J., Hisaria, K., Jinwala, D.: A comparative analysis of tools for verification of security protocols. IJCNS 3(10), 779–787 (2010)CrossRefGoogle Scholar
  13. 13.
    Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefzbMATHGoogle Scholar
  14. 14.
    Dolev, D., Yao, A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Heather, J., Schneider, S.: A formal framework for modelling coercion resistance and receipt freeness. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 217–231. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-32759-9_19 CrossRefGoogle Scholar
  16. 16.
    Hussain, M., Seret, D.: A comparative study of security protocols validation tools: hermes vs. avispa. In: 2006 8th International Conference Advanced Communication Technology, vol. 1, pp. 303–308, 6 pages, February 2006Google Scholar
  17. 17.
    Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Foundations and Practice of Security (FPS 2015), Clermont-Ferrand, France, October 2015Google Scholar
  18. 18.
    Lafourcade, P., Terrade, V., Vigier, S.: Comparison of cryptographic verification tools dealing with algebraic properties. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 173–185. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-12459-4_13 CrossRefGoogle Scholar
  19. 19.
    Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–133 (1995)CrossRefzbMATHGoogle Scholar
  20. 20.
    Meadows, C.A.: Analyzing the needham-schroeder public key protocol: a comparison of two approaches. In: Bertino, E., Kurth, H., Martella, G., Montolivo, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 351–364. Springer, Heidelberg (1996). doi: 10.1007/3-540-61770-1_46 CrossRefGoogle Scholar
  21. 21.
    Moran, M., Heather, J.: Automated analysis of voting systems with dolev-yao intruder model. In: AVOCS 2013, September 2013Google Scholar
  22. 22.
    Moran, M., Heather, J., Schneider, S.: Verifying anonymity in voting systems using CSP. Formal Aspects Comput., 1–36 (2012)Google Scholar
  23. 23.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), December 1978Google Scholar
  24. 24.
    Smyth, B.: Formal verification of cryptographic protocols with automated reasoning. Ph.D. thesis, School of Computer Science, University of Birmingham (2011)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Computer Science DepartmentWilliam Marsh Rice UniversityHoustonUSA

Personalised recommendations