Skip to main content
SpringerLink
Log in

Verifying Security Protocols: An Application of CSP

  • Chapter
Book cover Communicating Sequential Processes. The First 25 Years

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3525))

Abstract

The field of protocol analysis is one area in which CSP has proven particularly successful, and several techniques have been proposed that use CSP to reason about security properties such as confidentiality and authentication. In this paper we describe one such approach, based on theorem-proving, that uses the idea of a rank function to establish the correctness of protocols. This description is motivated by the consideration of a simple, but flawed, authentication protocol. We show how a rank function analysis can be used to locate this flaw and prove that a modified version of the protocol is correct.

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. Abadi, M.: Secrecy by typing in security protocols. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 611–638. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  2. Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Information and Computation (1998); also DEC Research Report 149,(1998)

    Google Scholar 

  3. Bistarelli, S., Cervesato, I., Lenzini, G., Martinelli, F.: Relating process algebras and multiset rewriting for security protocol analysis. In: WITS 2003: Workshop on Issues in the Theory of Security (2003)

    Google Scholar 

  4. Broadfoot, P.J., Roscoe, A.W.: Proving security protocols with model checkers by data independence techniques. Journal of Computer Security 7(2/3) (1999)

    Google Scholar 

  5. Broadfoot, P.J., Roscoe, A.W.: Capturing parallel attacks within the data independence framework. In: Proceedings of the 15th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  6. Bryans, J.W., Schneider, S.A.: CSP, PVS, and a recursive authentication protocol. In: DIMACS Workshop on Design and Formal Verification of Crypto Protocols (1997)

    Google Scholar 

  7. Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: Proceedings of the 12th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  8. Cervesato, I., Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: A meta-notation for protocol analysis. In: 12th IEEE Computer Security Foundations Workshop (1999)

    Google Scholar 

  9. Cervesato, I., Durgin, N., Mitchell, J.C., Lincoln, P., Scedrov, A.: Relating strands and multiset rewriting for security protocol analysis. In: Proceedings of The 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  10. Durante, A., Focardi, R., Gorrieri, a.R.: A compiler for analyzing cryptographic protocols using non-interference. ACM Transactions on Software Engineering and Methodology 9(4) (2000)

    Google Scholar 

  11. Dutertre, B., Schneider, S.A.: Embedding CSP in PVS: an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  12. Delicata, R., Schneider, S.A.: Towards the rank function verification of protocols with temporary secrets. In: WITS 2004: Workshop on Issues in the Theory of Security (2004)

    Google Scholar 

  13. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2) (1983)

    Google Scholar 

  14. Evans, N., Schneider, S.A.: Analysing time dependent security properties in CSP using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 222–237. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  15. Evans, N., Schneider, S.A.: Verifying security protocols with PVS: Widening the rank function approach. In: Journal of Logic and Algebraic Programming (in press)

    Google Scholar 

  16. Evans, N.: Investigating Security Through proof. PhD thesis, Royal Holloway, University of London (2003)

    Google Scholar 

  17. Focardi, R., Gorrieri, a.R.: The compositional security checker: A tool for the verification of information flow security properties. IEEE Transactions on Software Engineering 23(9) (1997)

    Google Scholar 

  18. Formal Systems (Europe) Ltd. FDR2 user manual (2003)

    Google Scholar 

  19. Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. In: Proceedings of the 14th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2001)

    Google Scholar 

  20. Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security 12(3/4) (2004); Also in Proceedings of the 15th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  21. Heather, J.A.: Oh! Is it really you?—Using rank functions to verify authentication protocols. PhD thesis, Royal Holloway, University of London (2000)

    Google Scholar 

  22. Heather, J.A.: Strand spaces and rank functions: More than distant cousins. In: Proceedings of The 15th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2002)

    Google Scholar 

  23. Hui, M.L., Lowe, G.: Fault-preserving simplifying transformations for security protocols. Journal of Computer Security 9(1/2) (2001)

    Google Scholar 

  24. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  25. Heather, J.A., Schneider, S.A.: Towards automatic verification of authentication protocols on unbounded networks. In: Proceedings of the 13th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (2000)

    Google Scholar 

  26. Heather, J.A., Schneider, S.A.: A decision procedure for the existence of a rank function. Journal of Computer Security (in press)

    Google Scholar 

  27. Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56, 131–133 (1995)

    Article  MATH  Google Scholar 

  28. Lowe, G.: A hierarchy of authentication specifications. In: Proceedings of the 10th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1997)

    Google Scholar 

  29. Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security 6(1/2) (1998)

    Google Scholar 

  30. Lowe, G.: Towards a completeness result for model checking of security protocols. Journal of Computer Security 7(2/3) (1999)

    Google Scholar 

  31. Lowe, G., Roscoe, A.W.: Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering (1996)

    Google Scholar 

  32. Meadows, C.: Applying formal methods to the analysis of a key management protocol. Journal of Computer Security 1(1) (1992)

    Google Scholar 

  33. Millen, J.: The interrogator model. In: IEEE Computer Society Symposium on Research in Security and Privacy (1995)

    Google Scholar 

  34. Menezes, A.J., Van Oorschott, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)

    Book  Google Scholar 

  35. Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Communications of the ACM 21(12) (1978)

    Google Scholar 

  36. Owre, S., Shankar, N., Rushby, J.: The PVS specification language. Technical report, Computer Science Lab, SRI International (1993)

    Google Scholar 

  37. Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1/2) (1998)

    Google Scholar 

  38. Paulson, L.: Verifying the SET protocol: Overview. In: Abdallah, A.E., Ryan, P.Y.A., Schneider, S. (eds.) FASec 2002. LNCS, vol. 2629, pp. 4–14. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  39. Pereira, O., Quisquater, J.-J.: On the perfect encryption assumption. In: WITS 2000: Workshop on Issues in the Theory of Security (2000)

    Google Scholar 

  40. Roscoe, A.W.: Modeling and verifying key-exchange protocols using CSP and FDR. In: Proceedings of the 8th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1995)

    Google Scholar 

  41. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1997)

    Google Scholar 

  42. Ryan, P.Y.A., Schneider, S.A.: Process algebra and non-interference. Journal of Computer Security 9(1/2) (2000); Also in Proceedings of the 12th Computer Security Foundations Workshop. IEEE Computer Society Press, Los Alamitos (1999)

    Google Scholar 

  43. Ryan, P.Y.A., Schneider, S.A., Goldsmith, M.H., Lowe, G., Roscoe, A.W.: Modelling and Analysis of Security Protocols. Addison-Wesley, Reading (2000)

    Google Scholar 

  44. Song, D.X., Berezin, S., Perrig, A.: Athena: A novel approach to efficient automatic security protocol analysis. Journal of Computer Security 9(1/2) (2001)

    Google Scholar 

  45. Schneider, S.A.: Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering (1998)

    Google Scholar 

  46. Schneider, S.A.: Concurrent and Real-time Systems: the CSP Approach. Addison-Wesley, Reading (1999)

    Google Scholar 

  47. Schneider, S.A.: Verifying security protocol implementations. In: FMOODS 2002: Formal Methods for Open Object-based Distributed Systems (2002)

    Google Scholar 

  48. Thayer Fábrega, F.J., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. Journal of Computer Security 7(1) (1999)

    Google Scholar 

  49. Woo, T., Lam, S.: A semantic model for authentication protocols. In: IEEE Computer Society Symposium on Research in Security and Privacy (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computing, University of Surrey,  

    Steve Schneider & Rob Delicata

Authors
  1. Steve Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rob Delicata
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of BCIM, Institute for Computing Research, London South Bank University, 103 Borough Road, SE1 0AA, London, UK

    Ali E. Abdallah

  2. School of Computing Science, Newcastle University, UK

    Cliff B. Jones

  3. International Institute for Software Technology, United Nations University, Macao

    Jeff W. Sanders

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Schneider, S., Delicata, R. (2005). Verifying Security Protocols: An Application of CSP. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds) Communicating Sequential Processes. The First 25 Years. Lecture Notes in Computer Science, vol 3525. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11423348_14

Download citation

  • DOI: https://doi.org/10.1007/11423348_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-25813-1

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation