Skip to main content
SpringerLink
Log in

Comparing State Spaces in Automatic Security Protocol Analysis

  • Chapter
Formal to Practical Security

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 5458))

Abstract

There are several automatic tools available for the symbolic analysis of security protocols. The models underlying these tools differ in many aspects. Some of the differences have already been formally related to each other in the literature, such as difference in protocol execution models or definitions of security properties. However, there is an important difference between analysis tools that has not been investigated in depth before: the explored state space. Some tools explore all possible behaviors, whereas others explore strict subsets, often by using so-called scenarios.

We identify several types of state space explored by protocol analysis tools, and relate them to each other. We find previously unreported differences between the various approaches. Using combinatorial results, we determine the requirements for emulating one type of state space by combinations of another type.

We apply our study of state space relations in a performance comparison of several well-known automatic tools for security protocol analysis. We model a set of protocols and their properties as homogeneously as possible for each tool. We analyze the performance of the tools over comparable state spaces. This work enables us to effectively compare these automatic tools, i.e., using the same protocol description and exploring the same state space. We also propose some explanations for our experimental results, leading to a better understanding of the tools.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 16.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Amadio, R., Charatonik, W.: On name generation and set-based analysis in the Dolev-Yao model. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 499–514. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.-C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Santiago, M.R.J., Turuani, M., Viganò, L., Vigneron, L.: 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)

    Chapter  Google Scholar 

  3. Armando, A., Basin, D.A., Bouallagui, M., Chevalier, Y., Compagna, L., Mödersheim, S., Rusinowitch, M., Turuani, M., Viganò, L., Vigneron, L.: The AVISS security protocol analysis tool. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 349–353. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Armando, A., Compagna, L.: An optimized intruder model for SAT-based model-checking of security protocols. In: Armando, A., Viganò, L. (eds.) ENTCS, vol. 125, pp. 91–108. Elsevier Science Publishers, Amsterdam (2005)

    Google Scholar 

  5. AVISPA Project. AVISPA protocol library, http://www.avispa-project.org/

  6. Basin, D., Mödersheim, S., Viganò, L.: An On-The-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Bellovin, S., Merritt, M.: Encrypted Key Exchange: Password-based protocols secure against dictionary attacks. In: SP 1992, p. 72 (1992)

    Google Scholar 

  8. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proc. CSFW 2001, pp. 82–96. IEEE Comp. Soc. Press, Los Alamitos (2001)

    Google Scholar 

  9. Bogart, K.P.: An obvious proof of Burnside’s Lemma. Am. Math. Monthly 98(12), 927–928 (1991)

    Article  MATH  Google Scholar 

  10. Boichut, Y., Héam, P.-C., Kouchnarenko, O., Oehl, F.: Improvements on the Genet and Klay technique to automatically verify security protocols. In: Proc. AVIS 2004 (April 2004)

    Google Scholar 

  11. Boreale, M.: Symbolic trace analysis of cryptographic protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, p. 667. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  12. Bozga, L., Lakhnech, Y., Perin, M.: HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 219–222. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Burnside, W.: Theory of groups of finite order. Cambridge University Press, Cambridge (1897)

    MATH  Google Scholar 

  14. Burrows, M., Abadi, M., Needham, R.: A logic of authentication. In: Proc. 12th ACM Symposium on Operating System Principles (SOSP 1989), pp. 1–13 (1989)

    Google Scholar 

  15. Cheminod, M., Bertolotti, I.C., Durante, L., Sisto, R., Valenzano, A.: Experimental comparison of automatic tools for the formal analysis of cryptographic protocols. In: DepCoS-RELCOMEX, pp. 153–160. IEEE Computer Society Press, Los Alamitos (2007)

    Google Scholar 

  16. Clark, J., Jacob, J.: A survey of authentication protocol literature (1997)

    Google Scholar 

  17. Comon-Lundh, H., Cortier, V.: Security properties: two agents are sufficient. Science of Computer Programming 50(1-3), 51–71 (2004)

    Article  MATH  Google Scholar 

  18. Comtet, L.: Advanced Combinatorics. Reidel, Dordrecht (1974)

    Book  MATH  Google Scholar 

  19. Corin, R., Etalle, S.: An improved constraint-based system for the verification of security protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 326–341. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security 14(1), 1–43 (2006)

    Article  Google Scholar 

  21. Cremers, C.: Scyther - Semantics and Verification of Security Protocols. Ph.D. dissertation, Eindhoven University of Technology (2006)

    Google Scholar 

  22. Cremers, C.: 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)

    Chapter  Google Scholar 

  23. Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: 15th ACM Conference on Computer and Communications Security (CCS 2008), pp. 119–128. ACM, New York (2008)

    Google Scholar 

  24. Cremers, C., Lafourcade, P.: Protocol tool comparison test archive, http://people.inf.ethz.ch/cremersc/downloads/performancetest.tgz

  25. Cremers, C., Mauw, S., de Vink, E.: Injective synchronisation: An extension of the authentication hierarchy. Theoretical Computer Science (2006)

    Google Scholar 

  26. Delaune, S., Kremer, S., Steel, G.: Formal analysis of pkcs#11. In: CSF 2008, pp. 331–344 (2008)

    Google Scholar 

  27. Donovan, B., Norris, P., Lowe, G.: Analyzing a library of security protocols using Casper and FDR. In: Proceedings of the Workshop on Formal Methods and Security Protocols (1999)

    Google Scholar 

  28. Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Proc. Workshop FMSP 1999 (1999)

    Google Scholar 

  29. Hoare, C.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  30. Hussain, M., Seret, D.: A Comparative study of Security Protocols Validation Tools: HERMES vs. AVISPA. In: Proc. ICACT 2006, vol. 1, pp. 303–308 (2006)

    Google Scholar 

  31. Jacquemard, F.: Security protocols open repository, http://www.lsv.ens-cachan.fr/spore/index.html

  32. Kerber, A.: Applied finite group actions, 2nd edn. Algorithms and Combinatorics, vol. 19. Springer, Berlin (1999)

    Book  MATH  Google Scholar 

  33. Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using fdr. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  34. Lowe, G.: A hierarchy of authentication specifications. In: Proc. 10th IEEE Computer Security Foundations Workshop (CSFW), pp. 31–44 (1997)

    Google Scholar 

  35. Lowe, G.: Casper: a compiler for the analysis of security protocols. J. Comput. Secur. 6(1-2), 53–84 (1998)

    Article  Google Scholar 

  36. Meadows, C.: 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)

    Chapter  Google Scholar 

  37. Meadows, C.: Language generation and verification in the NRL protocol analyzer. In: Proc. CSFW 1996, pp. 48–62. IEEE Comp. Soc. Press, Los Alamitos (1996)

    Google Scholar 

  38. Millen, J.: A necessarily parallel attack. In: Heintze, N., Clarke, E. (eds.) Workshop on Formal Methods and Security Protocols (1999)

    Google Scholar 

  39. Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murphi. In: IEEE Symposium on Security and Privacy (May 1997)

    Google Scholar 

  40. Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communication of the ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  41. Paulson, L.C.: Inductive analysis of the internet protocol TLS. ACM Trans. Inf. Syst. Secur. 2(3), 332–351 (1999)

    Article  Google Scholar 

  42. Roscoe, A.W.: Model-checking CSP. Prentice Hall, Englewood Cliffs (1994)

    Google Scholar 

  43. Roscoe, A.W.: Modelling and verifying key-exchange protocols using CSP and FDR. In: IEEE Symposium on Foundations of Secure Systems (1995)

    Google Scholar 

  44. Song, D., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9(1/2), 47–74 (2001)

    Article  Google Scholar 

  45. Tsalapati, E.: Analysis of pkcs#11 using avispa tools. Master’s thesis, University of Edinburgh (2007)

    Google Scholar 

  46. Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277–286. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  47. Viganò, L.: Automated security protocol analysis with the AVISPA tool. ENTCS 155, 61–86 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, ETH Zurich, 8092, Zurich, Switzerland

    Cas J. F. Cremers

  2. Verimag, University of Grenoble, 38610, Giéres, France

    Pascal Lafourcade

  3. Faculty of Mathematics of the University of Vienna, Austria

    Philippe Nadeau

Authors
  1. Cas J. F. Cremers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pascal Lafourcade
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Philippe Nadeau
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LORIA, Équipe Cassis, Bât. A, Campus Scientifique, BP 239, 54506, Vandoeuvre-lès-Nancy Cedex, France

    Véronique Cortier

  2. Centre de Recherche, INRIA Bordeaux – Sud-Ouest, Bât. A29, 351 Cours de la Libération, 33405, Talence, France

    Claude Kirchner

  3. Department of Philosophy, Keio University, 2-15-45 Mita, Minato-ku, 108-8345, Tokyo, Japan

    Mitsuhiro Okada

  4. 3-1 Morinosato Wakamiya Atsugi-shi, 243-0198, Kanagawa, Japan

    Hideki Sakurada

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Cremers, C.J.F., Lafourcade, P., Nadeau, P. (2009). Comparing State Spaces in Automatic Security Protocol Analysis. In: Cortier, V., Kirchner, C., Okada, M., Sakurada, H. (eds) Formal to Practical Security. Lecture Notes in Computer Science, vol 5458. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02002-5_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-02002-5_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-02001-8

  • Online ISBN: 978-3-642-02002-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation