Skip to main content
SpringerLink
Log in

Analysis of a Security Protocol in μCRL

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2002)

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

Included in the following conference series:

Abstract

In this paper, we present how the process-algebraic language μCRL can be used to specify security protocols and discuss the analysis process using the μCRL toolset and CADP. To illustrate the feasibility of our approach, we analyzed the Needham-Schroeder public-key protocol and reproduced the error found by Gavin Lowe [7]. Two more definitions of authentication are also studied. We give some remarks on our approach and discuss some possible directions for future work.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. S.C.C. Blom, W.J. Fokkink, J.F. Groote, I.Z. vanLangevelde, B. Lisser and J.C. van de Pol. μCRL: A toolset for analysing algebraic specification. In Proc. CAV’2001, LNCS 2102, Springer-Verlag, pp. 250–254.

    Google Scholar 

  2. D. Dolev and A. Yao. On the security of public-key protocols. IEEE Transactions on Information Theory 29(2) (1983).

    Google Scholar 

  3. N. Durgin and J. Mitchell. Analysis of security protocols. In Calculational System Design (1999), ISO Press, pp. 369–395.

    Google Scholar 

  4. J.-C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu and M. Sighireanu. CADP-a protocol validation and verification toolbox. In Proc. CAV’1997, LNCS 1102, Springer-Verlag, pp. 437–440.

    Google Scholar 

  5. W.J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer-Verlag, 2000.

    Google Scholar 

  6. G. Leduc and F. Germeau. Verification of security protocols using Lotos-method and application. Computer Communications 23 (2000), 1089–1103.

    Google Scholar 

  7. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using CSP and FDR. In 2nd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (1996), Springer-Verlag, pp. 147–166.

    Google Scholar 

  8. G. Lowe. Some new attacks upon security protocols. In 9th IEEE Computer Security Foundations Workshop (1996), IEEE Press, pp. 162–169.

    Google Scholar 

  9. R. Mateescu and M. Sighireanu. Efficient on-the-fly model-cheching for regular alternation-free mu-calculus. In Proc. FMICS’2000, pp. 65–86.

    Google Scholar 

  10. J. Mitchell, M. Mitchell and U. Stern. Automated analysis of cryptographic protocols using Murø. In Proc. of IEEE Symposium on Security and Privacy (1997), pp. 141–151.

    Google Scholar 

  11. R. Needham and M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM 21 (1978), 120–126.

    Google Scholar 

  12. J. Pang. Analysis of a security protocol in μCRL. Tech. Rep. SEN-R0201, CWI, Amsterdam, 2002.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centrum voor Wiskunde en Informatica, P.O. Box 94079, 1090 GB, Amsterdam, The Netherlands

    Jun Pang

Authors
  1. Jun Pang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, P.O. Box 3058, Macao

    Chris George

  2. School of Computer Engineering and Science, Shanghai University, 149 Yanchang Road, Shanghai, 200072, P.R. China

    Huaikou Miao

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Pang, J. (2002). Analysis of a Security Protocol in μCRL. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_40

Download citation

  • DOI: https://doi.org/10.1007/3-540-36103-0_40

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-36103-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation