Movatterモバイル変換

[0]ホーム
URL:

Skip to main content

Advertisement

Springer Nature Link
Log in

Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR

  • Regular Sessions Session 4: Security
  • Conference paper
  • First Online:

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

Abstract

In this paper we analyse the well known Needham-Schroeder Public-Key Protocol using FDR, a refinement checker for CSP. We use FDR to discover an attack upon the protocol, which allows an intruder to impersonate another agent. We adapt the protocol, and then use FDR to show that the new protocol is secure, at least for a small system. Finally we prove a result which tells us that if this small system is secure, then so is a system of arbitrary size.

Similar content being viewed by others

Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. Colin Boyd. Hidden assumptions in cryptographic protocols.Proceedings of the IEE, 137, Part E(6):433–436, November 1990.

    Google Scholar 

  2. Michael Burrows, Martín Abadi, and Roger Needham. A logic of authentication.Proceedings of the Royal Society of London A, 426:233–271, 1989. A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, 1989.

    Google Scholar 

  3. Dorothy E. Denning and Giovanni Maria Sacco. Timestamps in key distribution protocols.Communications of the ACM, 24(8):533–536, 1981.

    Google Scholar 

  4. W. Diffie and M. Hellman. New directions in cryptography.IEEE Transactions on Information Theory, 22:644–654, 1976.

    Google Scholar 

  5. Formal Systems (Europe) Ltd.Failures Divergence Refinement—User Manual and Tutorial, 1993. Version 1.3.

    Google Scholar 

  6. C. A. R. Hoare.Communicating Sequential Processes. Prentice Hall, 1985.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  9. R. L. Rivest, A. Shamir, and L. Adleman. A method for obtaining digital signatures and public-key cryptosystems.Communications of the ACM, 21(2):120–126, February 1978.

    Google Scholar 

  10. A. W. Roscoe. Developing and verifying protocols in CSP. InProceedings of Mierlo workshop on protocols. TU Eindhoven, 1993.

    Google Scholar 

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

    Google Scholar 

  12. A. W. Roscoe and Helen MacCarthy. Verifying a replicated database: A case study in model-checking CSP. Submitted for publication.

    Google Scholar 

  13. Steve Schneider. Security properties and CSP. In preparation, 1995.

    Google Scholar 

  14. Bruce Schneier.Applied Cryptography. Wiley, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Gavin Lowe

Authors
  1. Gavin Lowe

    You can also search for this author inPubMed Google Scholar

Editor information

Tiziana Margaria Bernhard Steffen

Rights and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lowe, G. (1996). Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_43

Download citation

Publish with us

[8]ページ先頭
©2009-2025 Movatter.jp