Skip to main content
SpringerLink
Log in

Analyzing Cryptographic Protocols in a Reactive Framework

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2002)

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

Abstract

In this paper, we analyze the suitability of reactive frameworks for modelling and verification of cryptographic protocols. Our study shows that cryptographic protocols can be modelled easily and naturally including the communication feature of the Internet wherein a point-to-point communication could be interpreted as broadcast mechanism due to the underlying routing and LAN architectures. The reactive framework provides an effective modelling of attacks/intruders as well as the capturing of the security properties such as secrecy and authenticity as observers. The observer-based approach of synchronous reactive frameworks aids in the modelling of properties incrementally and the use of the simulate-compile-verify cycle of the synchronous programming environment. The anomalies that could arise due to possible concurrent runs of agents can be detected. For illustration purposes, we use the TMN protocol. We will also argue that the reactive frameworks also provide a basis for specifying cryptographic protocols.

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. M. Abadi, A. Gordon, A Calculus for Cryptographic Protocols: The Spi Calculus, 4th ACM Conf. on Computers and Communications Security, (1997) 36–47.

    Google Scholar 

  2. G. Berry and G. Gonthier, The Esterel Synchronous Programming Language: Design, semantics, Implementation, SCP, 19 (2):87–152, November 1992.

    MATH  Google Scholar 

  3. B. Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, In 14th IEEE Computer Security Foundations Workshop (CSFW-14), Canada, 2001.

    Google Scholar 

  4. D. Bolignano, An approach to the formal verification of cryptographic protocols, 3rd ACM Conf. on Computer and Communications Security, pp. 106–118, 1996.

    Google Scholar 

  5. M. Burrows, M. Abadi, R. Needham, A Logic of Authentication, ACM Transactions on Computer Systems, 8(1), (1990) 18–36.

    Article  Google Scholar 

  6. D. Dolev, A. Yao, On the Security of Public Key Protocols, IEEE Trans. on Information Theory, 29(2), (1983) 198–208.

    Article  MATH  MathSciNet  Google Scholar 

  7. D. Harel, A. Pnueli, On the development of reactive systems: logics and models of concurrent systems, Proc. NATO ASI Series, 477–498, Springer Verlag, 1985.

    Google Scholar 

  8. R. Kemmerer, Analyzing encryption protocols using formal verification techniques, IEEE J. on Selected Areas in Communications, 7(4), (1989) 448–457.

    Article  Google Scholar 

  9. R. Kemmerer, C. Meadows and J. Millen, Three Systems for Cryptographic Protocol Analysis, J Cryptology (1994), 7:79–130.

    Article  MATH  Google Scholar 

  10. J.G. Larrecq, Clap, a simple language for cryptographic protocols, INRIA, 2001.

    Google Scholar 

  11. G. Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proc. TACAS, LNCS 1055, 147–166, 1996, Springer Verlag.

    Google Scholar 

  12. G. Lowe, and B. Roscoe, Using CSP to detect errors in the TMN protocol, In IEEE Tr. on Software Engg., v. 23, 10, 1997.

    Google Scholar 

  13. J.C. Mitchell, M. Mitchell, U. Stern, Automated Analysis of Cryptographic Protocols Using Murϕ, Proc. IEEE Symp. on Security and Privacy, 1997, 141–151.

    Google Scholar 

  14. G. Pace, N. Halbwachs, and P. Raymond, Counter-Example Generation in Symbolic Abstract Model Checking, FMICS, 2001.

    Google Scholar 

  15. L.C. Paulson, The Inductive approach to verifying cryptographic protocols, J.Computer Security, 6, 1998, 85–128.

    Google Scholar 

  16. N. Raja and R.K. Shyamasundar, A Cryptographic Protocol Analysis: an annotated bibliography, Tutorial at Int. Conf. on Information Tech., Bhuvaneshwar, Dec. 2000.

    Google Scholar 

  17. M. Tatebayashi, N. Matsuzaki, D. Neuman, Key distribution protocol for digital mobile communication systems, Proc. CRYPTO’ 89, (90) 324–333, Springer Verlag.

    Google Scholar 

  18. C. Weidenbach, Towards an automatic analysis of security protocols in first-order logic, in H. Ganzinger, ed., 16th CADE-16, 1999, LNAI 1632, Springer, 378–382.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Technology and Computer Science, Tata Institute of Fundamental Research, 400005, Mumbai, India

    R. K. Shyamasundar

Authors
  1. R. K. Shyamasundar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università Ca’ Foscari di Venezia, Via Torino 155, 30170, Mestre-Venezia, Italy

    Agostino Cortesi

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Shyamasundar, R.K. (2002). Analyzing Cryptographic Protocols in a Reactive Framework. In: Cortesi, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2002. Lecture Notes in Computer Science, vol 2294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47813-2_4

Download citation

  • DOI: https://doi.org/10.1007/3-540-47813-2_4

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43631-7

  • Online ISBN: 978-3-540-47813-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation