Skip to main content
SpringerLink
Log in

Specifying Authentication Protocols Using Rewriting and Strategies

  • Conference paper
  • First Online:
Book cover Practical Aspects of Declarative Languages (PADL 2001)

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

Included in the following conference series:

Abstract

Programming with rewrite rules and strategies has been already used for describing several computational logics. This paper describes the way the Needham-Schroeder Public-Key protocol is specified in ELAN, the system developed in Nancy to model and compute in the rewriting calculus. The protocol aims to establish a mutual authentication between an initiator and a responder that communicate via an insecure network. The protocol has been shown to be vulnerable and a correction has been proposed. The behavior of the agents and of the intruders as well as the security invariants the protocol should verify are naturally described by conditional rewrite rules whose application is controlled by strategies. Similar attacks to those already described in the literature have been discovered. We show how different strategies using the same set of rewrite rules can improve the efficiency in finding the attacks and we compare our results to existing approaches.

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

Access this chapter

Log in via an institution
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.

References

  1. P. Borovanský, C. Kirchner, H. Kirchner, P.-E. Moreau, and C. Ringeissen. An overview of ELAN. In 2nd International Workshop on Rewriting Logic and its Applications, volume 15, Pont-à-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science.

    Google Scholar 

  2. D. Dill, A. Drexler, A. Hu, and C. Yang. Protocol verification as a hardware design aid. In IEEE International Conference on Computer Design: VLSI in Computers and Processors, pages 522–525, 1992.

    Google Scholar 

  3. G. Denker. From rewrite theories to temporal logic theories. In 2nd International Workshop on Rewriting Logic and its Applications, volume 15, Pont-à-Mousson (France), September 1998. Electronic Notes in Theoretical Computer Science.

    Google Scholar 

  4. G. Denker and J. Millen. Capsl intermediate language. In Formal Methods and Security Protocols, 1999. FLOC’ 99 Workshop.

    Google Scholar 

  5. C. Kirchner, H. Kirchner, and M. Vittek. Designing constraint logic programming languages using computational systems. In Principles and Practice of Constraint Programming. The Newport Papers., chapter 8, pages 131–158. The MIT press, 1995.

    Google Scholar 

  6. G. Lowe. An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters, 56:131–133, 1995.

    Article  MATH  Google Scholar 

  7. G. Lowe. Breaking and fixing the Needham-Schroeder public key protocol using CSP and FDR. In Proceedings of 2nd TACAS Conf., volume 1055 of Lecture Notes in Computer Science, pages 147–166, Passau (Germany), 1996. Springer-Verlag.

    Google Scholar 

  8. G. Lowe. Casper: a compiler for the analysis of security protocols. Journal of Computer Security, 6(1):53–84, 1998.

    Google Scholar 

  9. C. Meadows. Analyzing the Needham-Schroeder Public Key Protocol: A Comparison of two Approaches. In Proceedings of 4th ESORICS Symp., volume 1146 of Lecture Notes in Computer Science, pages 351–364, Rome (Italy), 1996. Springer-Verlag.

    Google Scholar 

  10. J. C. Mitchell, M. Mitchell, and U. Stern. Analysis of cryptographic protocols using murphi. In IEEE Symposium on Security and Privacy, pages 141–153, Oakland, 1997.

    Google Scholar 

  11. D. Monniaux. Abstracting cryptographic protocols with tree automata. In Proceedings of 6th SAS, Venezia (Italy), 1999.

    Google Scholar 

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

    Article  MATH  Google Scholar 

  13. A. Roscoe. Model-checking CSP. In A Classical Mind, Essays in Honour of C.A.R.Hoare. Prentice-Hall, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LORIA and INRIA, Campus Scientifique, BP 239, 54506, Vandoeuvre-lès-Nancy, France

    Horatiu Cirstea

Authors
  1. Horatiu Cirstea
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, State University of New York, Stony Brook, 11794, NY, USA

    I. V. Ramakrishnan

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cirstea, H. (2001). Specifying Authentication Protocols Using Rewriting and Strategies. In: Ramakrishnan, I.V. (eds) Practical Aspects of Declarative Languages. PADL 2001. Lecture Notes in Computer Science, vol 1990. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45241-9_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-45241-9_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41768-2

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation