Skip to main content
SpringerLink
Log in

Reasoning about cryptographic protocols in the spi calculus

  • Contributions
  • Conference paper
  • First Online:
CONCUR '97: Concurrency Theory (CONCUR 1997)

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

Included in the following conference series:

Abstract

The spi calculus is an extension of the pi calculus with constructs for encryption and decryption. This paper develops the theory of the spi calculus, focusing on techniques for establishing testing equivalence, and applying these techniques to the proof of authenticity and secrecy properties of 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. To appear in the Proceedings of the Fourth ACM Conference on Computer and Communications Security, 1997.

    Google Scholar 

  2. M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Technical Report 414, University of Cambridge Computer Laboratory, January 1997.

    Google Scholar 

  3. M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, January 1996.

    Google Scholar 

  4. M. Burrows, M. Abadi, and R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London A, 426:233–271, 1989. A preliminary version appeared as Digital Equipment Corporation Systems Research Center report No. 39, February 1989.

    Google Scholar 

  5. G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, April 1992.

    Article  Google Scholar 

  6. M. Boreale and R. De Nicola. Testing equivalence for mobile processes. Information and Computation, 120(2):279–303, August 1995.

    Google Scholar 

  7. Data encryption standard. Fed. Inform. Processing Standards Pub. 46, National Bureau of Standards, Washington DC, January 1977.

    Google Scholar 

  8. R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.

    Article  Google Scholar 

  9. J. Gray and J. McLean. Using temporal logic to specify and verify cryptographic protocols (progress report). In Proceedings of the 8th IEEE Computer Security Foundations Workshop, pages 108–116, 1995.

    Google Scholar 

  10. R. A. Kemmerer. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 7, 1989.

    Google Scholar 

  11. A. Liebl. Authentication in distributed systems: A bibliography. ACM Operating Systems Review, 27(4):31–41, 1993.

    Google Scholar 

  12. G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 147–166. Springer Verlag, 1996.

    Google Scholar 

  13. J. K. Millen, S. C. Clark, and S. B. Freedman. The Interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, SE-13(2):274–288, February 1987.

    Google Scholar 

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

    Google Scholar 

  15. R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.

    Google Scholar 

  16. R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119–141, 1992.

    Google Scholar 

  17. J. K. Millen. The Interrogator model. In IEEE Symposium on Security and Privacy, pages 251–260, 1995.

    Google Scholar 

  18. R. Milner. The π-calculus. Undergraduate lecture notes, Cambridge University, 1995.

    Google Scholar 

  19. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Information and Computation, pages 1–40 and 41–77, September 1992.

    Google Scholar 

  20. S. Schneider. Security properties and CSP. In IEEE Symposium on Security and Privacy, pages 174–187, 1996.

    Google Scholar 

  21. B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Systems Research Center, Digital Equipment Corporation, UK

    Martín Abadi

  2. Computer Laboratory, University of Cambridge, UK

    Andrew D. Gordon

Authors
  1. Martín Abadi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew D. Gordon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Antoni Mazurkiewicz Józef Winkowski

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abadi, M., Gordon, A.D. (1997). Reasoning about cryptographic protocols in the spi calculus. In: Mazurkiewicz, A., Winkowski, J. (eds) CONCUR '97: Concurrency Theory. CONCUR 1997. Lecture Notes in Computer Science, vol 1243. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63141-0_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-63141-0_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63141-5

  • Online ISBN: 978-3-540-69188-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation