Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Verification of cryptographic protocols: An experiment

  • Conference paper
  • First Online:
FME '97: Industrial Applications and Strengthened Foundations of Formal Methods (FME 1997)

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

Included in the following conference series:

  • 263 Accesses

Abstract

The objective of this paper is to present the verification of some confidentiality features of the SESAME protocol, an extension of Kerberos. We do that by using the formal approach presented in [7]. This approach is based on the use of state-based general purpose formal methods. It makes a clear separation between modeling of reliable agents and that of intruders. After we have extended this approach to take into account the use of signatures, we use it to formalize SESAME which includes many functionalities among them access control, delegation and multi-level security facilities. The approach is then transposed together with the protocol description quite directly into the Coq prover's formalism. For the sake of conciseness we only describe here formal proofs of confidentiality properties. We prove more precisely the privacy of the session keys in addition to that of the secret keys the principals share with servers. The main advantage of the approach is to provide within a completely formal framework, a systematic verification of a protocol based on its exact and precise specification and not an approximation or simplification of it. The approach is thus complementary with modal logic based methods which allow for a concise, elegant, but superficial verification of protocols: in such logics confidentiality properties, which we prove here to be preserved provided they are true initially, are considered to be hypotheses that are not verified or justified by any formal means.

This work was done while the author was at LAMSADE-Université Paris IX Dauphine

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. M. Abadi and Marc.R. Tuttle. A Semantics for a Logic of Authentication. In Proceedings of the 10th Annual ACM Symposium On Principles of Distributed Computing, pages 201–216, August 1991.

    Google Scholar 

  2. M. Ayadi. Logics for Cryptographic Protocols: a Survey. Technical report, University of Paris IX-Dauphine, 1997.

    Google Scholar 

  3. J.P. Banâtre and D. LeMétayer. Programming by Multiset Transformation. Technical Report 117, IRISA Rennes, March 1990.

    Google Scholar 

  4. S.M. Bellovin and M. Merritt. Limitations of the Kerberos Authentication System. In Computer Communications Review 20(5), pages 119–132., October 1990.

    Article  Google Scholar 

  5. P. Bieber and N. Boulahia-Cuppens. Formal Development of Authentication Protocols. In BCS-FAGS sixth Refinement Workshop, 1994.

    Google Scholar 

  6. D. Bolignano. Vérification Formelle de Protocoles Cryptographiques à l'aide de Coq. In Actes des journés GDR, 1995.

    Google Scholar 

  7. D. Bolignano. Formal Verification of Cryptographic Protocols. In Proceedings of the third ACM Conference on Computer and Communication Security, 1996.

    Google Scholar 

  8. M. Burrows, M. Abadi, and R. Needham. A Logic of Authentication. In Proceedings of the Royal Society of London A Vol.426, pages 233–271, 1989.

    Google Scholar 

  9. K.M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, 1990.

    Google Scholar 

  10. P.C. Chen and V.D. Gligor. On the Formal Specification and Verification of a Multiparty Session Protocol. In Proceedings of the IEEE Symposium on Research in Security and Privacy, 1990.

    Google Scholar 

  11. G.Huet. The Gilbreath Trick: A Case Study in Axiomatization and Proof Development in the Coq Proof Assistant. In INRIA Research Report 1511, September 1991.

    Google Scholar 

  12. L. Gong, R. Needham, and R. Yahalom. Reasoning about Belief in Cryptographic Protocols. In Proceedings of the IEEE Symposium on Research in Security and Privacy, pages 234–248. IEEE, 1990.

    Google Scholar 

  13. B.C. Neuman J.G. Steiner and J.I. Schiller. Kerberos: An Authentication Service for Open Network Systems. Usenix Conference Proceedings, Dallas, Texas, pages 191–202, Feb 1988.

    Google Scholar 

  14. R.A. Kemmerer. Analyzing Encryption Protocols Using Formal Verification Techniques. IEEE Journal on Selected Area in Communications, volume 7(4), 1989.

    Google Scholar 

  15. J.T Kohl. The Evolution of the Kerberos Authentication Service. European Conference Proceedings, Troms, Norway, pages 295–313, May 1991.

    Google Scholar 

  16. J.T Kohl and B.C. Neuman. The Kerberos Network Authentication Service (V5). Internet RFC 1510, Sep 1993.

    Google Scholar 

  17. Armin Liebl. Authentification in Distributed Systems: A Bibliography. ACM Operating Systems Review, 27(4), pages 31–41, October 1993.

    Google Scholar 

  18. Gavin Lowe. An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Information Processing Letters, 1995.

    Google Scholar 

  19. C. Meadows. Using Narrowing in the Analysis of Key Management. In Proceedings of the IEEE Symposium on Research in Security and Privacy., June 1989.

    Google Scholar 

  20. C. Meadows. Representing Partial Knowledge in an Algebraic Security Model. In Proceedings of the IEEE Computer Security Foundations Workshop VII, Franconia, New-Hampshire., June 1990.

    Google Scholar 

  21. C. Meadows. A System for the Analysis of a Key Management Protocol. In Proceedings of the IEEE Symposium on Research in Security and Privacy., June 1991.

    Google Scholar 

  22. C. Meadows. Applying Formal Methods to the Analysis of a Key Management Protocol. In Journal of Computer Security., June 1992.

    Google Scholar 

  23. T.A. Parker. A Secure European System for Applications in a Multi-vendor Environment (The SESAME project). In Proceedings of the 14th American National Security Conference., 1991.

    Google Scholar 

  24. D. Pinkas and T.A. Parker. SESAME Technology Version Two-an Overview., Sep 1994.

    Google Scholar 

  25. D. Pinkas and T.A. Parker. SESAME Technology Version Three-Overview., Sep 1995.

    Google Scholar 

  26. A. W. Roscoe. Developing and Verifying Protocols in CSP. In Proceedings of Mierlo-workshop on protocols. TU Eindhoven, 1993.

    Google Scholar 

  27. A.D. Rubin and P. Honeyman. Formal Methods for the Analysis of Authentication Protocols. Technical report, Center for Information Technology Integration, 1993. University of Michigan. Internal Draft.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Cap Gemini/Division Finance, 76, avenue Kléber, 75784, Paris, France

    Marc Mehdi Ayadi

  2. Dyade, B.P.105, 78153, Le Chesnay Cedex, France

    Dominique Bolignano

Authors
  1. Marc Mehdi Ayadi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dominique Bolignano
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ayadi, M.M., Bolignano, D. (1997). Verification of cryptographic protocols: An experiment. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_19

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_19

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation