Skip to main content
SpringerLink
Log in

Formal verification of cryptographic protocols: A survey

  • Invited Lecture 2
  • Conference paper
  • First Online:
Book cover Advances in Cryptology — ASIACRYPT'94 (ASIACRYPT 1994)

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

Included in the following conference series:

Abstract

In this paper we give a survey of the state of the art in the application of formal methods to the analysis of cryptographic protocols. We attempt to outline some of the major threads of research in this area, and also to document some emerging trends. ...

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martín Abadi and Mark Tuttle. A Semantics for a Logic of Authentication. In Proceedings of the Tenth ACM Symposium on Principles of Distributed Computing, pages 201–216. ACM Press, August 1991.

    Google Scholar 

  2. A. Aziz and W. Diffie. Privacy and Authentication for Wireless Local Area Networks. IEEE Personal Communications, 1(1):25–31, 1994.

    Google Scholar 

  3. M. Bellare and P. Rogaway. Entity Authentication and Key Distribution. In Advances in Cryptology — CRYPTO '93, volume to appear. Springer-Verlag, 1994.

    Google Scholar 

  4. P. Bieber. A Logic of Communication in a Hostile Environment. In Proceedings of the Computer Security Foundations Workshop III, pages 14–22. IEEE Computer Society Press, June 1990.

    Google Scholar 

  5. J. Burns and C. J. Mitchell. A Security Scheme for Resource Sharing Over a Network. Computers and Security, 19:67–76, February 1990.

    Google Scholar 

  6. Michael Burrows, Martín Abadi, and Roger Needham. A Logic of Authentication. ACM Transactions in Computer Systems, 8(1):18–36, February 1990.

    Google Scholar 

  7. Michael Burrows, Martín Abadi, and Roger Needham. Rejoinder to Nessett. Operating Systems Review, 24(2):39–40, April 1990.

    Google Scholar 

  8. U. Carlsen. Generating Formal Cryptographic Protocol Specifications. In Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 137–146. IEEE Computer Society Press, May 16–18 1994.

    Google Scholar 

  9. CCITT. CCITT Draft Recomendation X.509. The Directory-Authentication Framework, Version 7, November 1987.

    Google Scholar 

  10. D. E. Denning and G. M. Sacco. Timestamps in Key Distribution Protocols. Communications of the ACM, 24(8):198–208, 1981.

    Google Scholar 

  11. Whitfield Diffie, Paul C. van Oorschot, and Michael J. Wiener. Authentication and Authenticated Key Exchanges. Designs, Codes, and Cryptography, 2:107–125, 1992.

    Google Scholar 

  12. D. Dolev, S. Even, and R. Karp. On the Security of Ping-Pong Protocols. Information and Control, pages 57–68, 1982.

    Google Scholar 

  13. D. Dolev and A. Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory, 29(2):198–208, March 1983.

    Google Scholar 

  14. Shimon Even, Oded Goldreich, and Adi Shamir. On the Security of Ping-Pong Protocols When Implemented Using the RSA. In Hugh C. Williams, editor, Advances in Cryptology — CRYPTO '85, pages 58–72. Springer-Verlag, 1985.

    Google Scholar 

  15. Joan Feigenbaum. Overview of Interactive Proof Systems and Zero Knowledge. In G. J. Simmons, editor, Contemperary Cryptology: The Science of Information Integrity, chapter 8, pages 423–439. IEEE Press, 1991.

    Google Scholar 

  16. L. Gong, R. Needham, and R. Yahalom. Reasoning about belief in cryptographic protocols. In IEEE Computer Society Symposiun in Security and Privacy, pages 234–248. IEEE Computer Society Press, May 1990.

    Google Scholar 

  17. Nevin Heintze and J. D. Tygar. A Model for Secure Protocols and Their Compositions. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 2–13. IEEE Computer Society Press, May 1994.

    Google Scholar 

  18. R. Kailar, V. D. Gligor, and L. Gong. On the Security Effectiveness of Cryptographic Protocols. In Proceedings of the Fourth Internation Working Conference on Dependable Computing For Critical Applications, 1994. to appear.

    Google Scholar 

  19. Richard Kemmerer. Using Formal Methods to Analyze Encryption Protocols. IEEE Journal on Selected Areas in Communication, 7(4):448–457, 1989.

    Google Scholar 

  20. Richard Kemmerer, Catherine Meadows, and Jonathan Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2), 1994.

    Google Scholar 

  21. T. M. A. Lomas, L. Gong, J. H. Saltzer, and R. H. Needham. Reducing Risks From Poorly Chosen Keys. Operating Systems Reviews, 23(5):14–18, 1989.

    Google Scholar 

  22. D. Longley and S. Rigby. An Automatic Search for Security Flaws in Key Management Schemes. Computers and Security, 11(1):75–90, 1992.

    Google Scholar 

  23. C. Meadows. Representing Partial Knowledge in an Algebraic Security Model. In Proceedings of the Computer Security Foundations Workshop III, pages 23–31. IEEE Computer Society Press, June 1990.

    Google Scholar 

  24. C. Meadows. A System for the Specification and Analysis of Key Management Protocols. In Proceedings of the 1991 IEEE Computer Society Symposium on Research in Security and Privacy, pages 182–195. IEEE Computer Society Press, Los Alamitos, California, 1991.

    Google Scholar 

  25. C. Meadows. Applying Formal Methods to the Analysis of a Key Management Protocol. Journal of Computer Security, 1:5–53, 1992.

    Google Scholar 

  26. C. Meadows. A Model of Computation for the NRL Protocol Analyzer. In Proceedings of the 7th Computer Security Foundations Workshop. IEEE Computer Society Press, June 1994.

    Google Scholar 

  27. M. J. Merritt. Cryptographic Protocols. Ph.d. thesis, Georgia Institute of Technology, 1983.

    Google Scholar 

  28. J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol Security Analysis. IEEE Transactions on Software Engineering, SE-13(2), 1987.

    Google Scholar 

  29. L. Moser. A Logic of Knowledge and Belief for Reasoning About Computer Security. In Proceedings of the Computer Security Foundations Workshop II, pages 57–63. IEEE Computer Society Press, June 1989.

    Google Scholar 

  30. R. M. Needham and M. D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Communications of the ACM, 21(12):993–999, December 1978.

    Google Scholar 

  31. D. M. Nessett. A Critique of the Burrows, Abadi, and Needham Logic. Operating Systems Review, 24(2):35–38, April 1990.

    Google Scholar 

  32. Birgit Pfitzmann. Sorting Out Signature Schemes. In Proceedings of the First ACM Conference on Computer and Communications Security, pages 74–85. ACM SIGSAC, ACM, November 3–5 1993.

    Google Scholar 

  33. G. B. Purdy, G. J. Simmons, and J. A. Studier. A Software Protection Scheme. In Proceedings of the 1982 Symposium on Security and Privacy, pages 99–103. IEEE Computer Society Press, April 1982.

    Google Scholar 

  34. P. V. Rangan. An Axiomatic Basis of Trust in Distributed Systems. In Proceedings of the 1988 Symposium on Security and Privacy, pages 204–211. IEEE Computer Society Press, April 1988.

    Google Scholar 

  35. G. J. Simmons. How to (Selectively) Broadcast a Secret. In Proceedings of the 1985 Symposium on Security and Privac, pages 108–113. IEEE Computer Society Press, April 1985.

    Google Scholar 

  36. S. Stubblebine and V. Gligor. On Message Integrity in Cryptographic Protocols. In Proceedings of the 1992 Symposium on Security and Privacy, pages 85–104. IEEE Computer Society Press, May 1992.

    Google Scholar 

  37. S. Stubblebine and V. Gligor. Protecting the Integrity of Privacy-Enhanced Mail. In PSRG Workshop on Network and Distributed System Security, pages 75–80, February 11–12 1993.

    Google Scholar 

  38. P. Syverson. Formal Semantics for Logics of Cryptographic Protocols. In Proceedings of the Computer Security Foundations Workshop III, pages 32–41. IEEE Computer Society Press, June 1990.

    Google Scholar 

  39. Paul Syverson. Adding Time to a Logic of Authentication. In Proceedings of the First ACM Conference on Computer and Communications Security, pages 97–101. ACM SIGSAC, ACM, November 3–5 1993.

    Google Scholar 

  40. Paul Syverson and Catherine Meadows. A Logical Language for Specifying Cryptographic Protocol Requirements. In Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy, pages 165–177. IEEE Computer Society Press, Los Alamitos, California, 1993.

    Google Scholar 

  41. Paul Syverson and Catherine Meadows. Formal Requirements for Key Distribution Protocols. In Proceedings of Eurocrypt '94, 1994. to appear.

    Google Scholar 

  42. Paul F. Syverson. Knowledge, Belief, and Semantics in the Analysis of Cryptographic Protocols. Journal of Computer Security, 1(3):317–334, 1992.

    Google Scholar 

  43. Paul F. Syverson and Paul C. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 14–28. IEEE Computer Society, May 1994.

    Google Scholar 

  44. M.-J. Toussaint. Verification of Cryptographic Protocols. Ph.d. thesis, Universite de Liege (Belgium), 1991.

    Google Scholar 

  45. M.-J. Toussaint. Deriving the Complete Knowledge of Participants in Cryptographic Protocols. In CRYPTO '91 (Advances in Cryptology— CRYPTO '91). Springer-Verlag, 1992.

    Google Scholar 

  46. M.-J. Toussaint. Separating the Specification and Implementation. Phases in Cryptology. In Computer Security — ESORICS 92, volume LMCS 638, pages 77–102. Springer-Verlag, 1992.

    Google Scholar 

  47. T. Y. C. Woo and S. Lam. A Semantic Model for Authentication Protocols. In Proceedings of the 1993 Symposium on Research in Security and Privacy, pages 178–194. IEEE Computer Society Press, May 1993.

    Google Scholar 

  48. R. Yahalom. Optimality of Asynchronous Two-Party Secure Data-Exchange Protocols. Journal of Computer Security, 2(2–3):191–209, 1994.

    Google Scholar 

  49. R. Yahalom, Birgit Klein, and Thomas Beth. Trust relationships in secure systems: A distributed authentication perspective. In Proceedings of the 1993 IEEE Symposium on Security and Privacy, pages 150–164. IEEE Computer Society Press, May 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center for High Assurance Computer Systems, Naval Research Laboratory, 20375, Washington, DC

    Catherine A. Meadows & Catherine A. Meadows

Authors
  1. Catherine A. Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Catherine A. Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Josef Pieprzyk Reihanah Safavi-Naini

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Meadows, C.A., Meadows, C.A. (1995). Formal verification of cryptographic protocols: A survey. In: Pieprzyk, J., Safavi-Naini, R. (eds) Advances in Cryptology — ASIACRYPT'94. ASIACRYPT 1994. Lecture Notes in Computer Science, vol 917. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000430

Download citation

  • DOI: https://doi.org/10.1007/BFb0000430

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59339-3

  • Online ISBN: 978-3-540-49236-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation