Advertisement

Formal verification of cryptographic protocols: A survey

  • Catherine A. Meadows
  • Catherine A. Meadows
Invited Lecture 2
Part of the Lecture Notes in Computer Science book series (LNCS, volume 917)

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. ...

Keywords

Formal Method IEEE Computer Society Authentication Protocol Cryptographic Protocol Security Flaw 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 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. 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. 7.
    Michael Burrows, Martín Abadi, and Roger Needham. Rejoinder to Nessett. Operating Systems Review, 24(2):39–40, April 1990.Google Scholar
  8. 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. 9.
    CCITT. CCITT Draft Recomendation X.509. The Directory-Authentication Framework, Version 7, November 1987.Google Scholar
  10. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 20.
    Richard Kemmerer, Catherine Meadows, and Jonathan Millen. Three Systems for Cryptographic Protocol Analysis. Journal of Cryptology, 7(2), 1994.Google Scholar
  21. 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. 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. 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. 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. 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. 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. 27.
    M. J. Merritt. Cryptographic Protocols. Ph.d. thesis, Georgia Institute of Technology, 1983.Google Scholar
  28. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 41.
    Paul Syverson and Catherine Meadows. Formal Requirements for Key Distribution Protocols. In Proceedings of Eurocrypt '94, 1994. to appear.Google Scholar
  42. 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. 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. 44.
    M.-J. Toussaint. Verification of Cryptographic Protocols. Ph.d. thesis, Universite de Liege (Belgium), 1991.Google Scholar
  45. 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. 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. 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. 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. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Catherine A. Meadows
    • 1
  • Catherine A. Meadows
    • 1
  1. 1.Center for High Assurance Computer SystemsNaval Research LaboratoryWashington, DC

Personalised recommendations