Skip to main content
SpringerLink
Log in

Symbolic Trace Analysis of Cryptographic Protocols

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 2001)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2076))

Included in the following conference series:

Abstract

A cryptographic protocol can be described as a system of concurrent processes, and analysis of the traces generated by this system can be used to verify authentication and secrecy properties of the protocol. However, this approach suffers from a state-explosion problem that causes the set of states and traces to be typically infinite or very large. In this paper, starting from a process language inspired by the spi-calculus, we propose a symbolic operational semantics that relies on unification and leads to compact models of protocols. We prove that the symbolic and the conventional semantics are in full agreement, and then give a method by which trace analysis can be carried out directly on the symbolic model. The method is proven to be complete for the considered class of properties and is amenable to automatic checking.

A preliminary version of this paper has been circulated as [5]. Research partly supported by the Italian MURST Project TOSCA (Teoria della Concorrenza, Linguaggi di Ordine Superiore e Strutture di Tipi).

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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.

Similar content being viewed by others

References

  1. M. Abadi, A.D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  2. M. Abadi, A.D. Gordon. A Bisimulation Method for Cryptographic Protocols. Nordic Journal of Computing, 5(4):267–303, 1998.

    MATH  MathSciNet  Google Scholar 

  3. R. Amadio, S. Prasad. The game of the name in cryptographic tables. RR 3733 INRIA Sophia Antipolis. In Proc. of Asian’00, LNCS, 2000.

    Google Scholar 

  4. R.M. Amadio, S. Lugiez. On the reachability problem in cryptographic protocols. In Proc. of Concur’00, LNCS, 2000. Full version: RR 3915 Inria Sophia Antipolis.

    Google Scholar 

  5. M. Boreale. Symbolic analysis of cryptographic protocols in the spi-calculus. Manuscript, 2000. Available at http://www.dsi.unifi.it/~boreale/papers.html.

  6. M. Boreale. STA: a tool for trace analysis of cryptographic protocols. ML object code and examples, 2001. Available at http://www.dsi.unifi.it/~boreale/tool.html.

  7. M. Boreale, R. De Nicola, R. Pugliese. Proof Techniques for Cryptographic Processes. In Proc. of LICS’99, IEEE Computer Society Press, 1999. Full version to appear in SIAM Journal on Computing.

    Google Scholar 

  8. M. Burrows, M. Abadi, R.M. Needham. A logic of authentication. Proc. of the Royal Society of London, 426:233–271, 1989.

    Article  MATH  MathSciNet  Google Scholar 

  9. E.M. Clarke, S. Jha, W. Marrero. Using state exploration and a natural deduction style message derivation engine to verify security protocols. In Proc. of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET), 1998.

    Google Scholar 

  10. N. Durgin, P. Lincoln, J. Mitchell, A. Scedrov. Undecidability of bounded security protocols. In Proc. of Workshop on Formal Methods and Security Protocols, Trento, 1999.

    Google Scholar 

  11. D. Dolev, A.C. Yao. On the security of public key protocols. In IEEE Transactions on Information Theory 29(2):198–208, 1983.

    Article  MATH  MathSciNet  Google Scholar 

  12. A. Huima. Efficient infinite-state analysis of security protocols. In Proc. of Workshop on Formal Methods and Security Protocols, Trento, 1999.

    Google Scholar 

  13. G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In Proceedings of TACAS’96, (T. Margaria, B. Steffen, Eds.), LNCS 1055, pp. 147–166, Springer-Verlag, 1996.

    Google Scholar 

  14. G. Lowe. A Hierarchy of Authentication Specifications. In 10th IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, 1997.

    Google Scholar 

  15. G. Lowe. Towards a completeness result for model checking of security protocols. In 11th Computer Security Foundations Workshop, IEEE Computer Society Press, 1998.

    Google Scholar 

  16. D. Marchignoli, F. Martinelli. Automatic verification of cryptographic protocols through compositional analysis techniques. In Proc. of TACAS99, LNCS 1579:148–163, 1999.

    Google Scholar 

  17. R. Milner, J. Parrow, D. Walker. A calculus of mobile processes, (Part I and II). Information and Computation, 100:1–77, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  18. L.C. Paulson. Proving Security Protocols Correct. In Proc. of LICS’99, IEEE Computer Society Press, 1999.

    Google Scholar 

  19. A.W. Roscoe. Modelling and verifying key-exchange using CSP and FDR. In 8th Computer Security Foundations Workshop, IEEE Computer Society Press, 1995.

    Google Scholar 

  20. A.W. Roscoe. Proving security protocols with model checkers by data independent techniques. In 11th Computer Security Foundations Workshop, IEEE Computer Society Press, 1998.

    Google Scholar 

  21. S. Schneider. Verifying Authentication Protocols in CSP. IEEE Transactions on Software Engineering, 24(8):743–758, 1998.

    Google Scholar 

  22. S. Stoller. A reduction for automated verification of security protocols. In Proc. Of Workshop on Formal Methods and Security Protocols, Trento, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dipartimento di Sistemi e Informatica, Università di Firenze, Via Lombroso 6/17, 50134, Firenze, Italia

    Michele Boreale

Authors
  1. Michele Boreale
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departament de Llenguatges i Sistemes Informátics, Univ. Politècnica de Catalunya, C/Jordi Girona Salgado 1-3, 08034, Barcelona, Spain

    Fernando Orejas

  2. Computer Technology Institute (CTI), University of Patras, 61 Riga Feraiou street, 26221, Patras, Greece

    Paul G. Spirakis

  3. Institute of Information and Computing Sciences, Utrecht University, Padualaan 14, 3584, CH, Utrecht, The Netherlands

    Jan van Leeuwen

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Boreale, M. (2001). Symbolic Trace Analysis of Cryptographic Protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds) Automata, Languages and Programming. ICALP 2001. Lecture Notes in Computer Science, vol 2076. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48224-5_55

Download citation

  • DOI: https://doi.org/10.1007/3-540-48224-5_55

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42287-7

  • Online ISBN: 978-3-540-48224-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation