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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Technical Report 414, University of Cambridge Computer Laboratory, January 1997.
M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, January 1996.
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.
G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, April 1992.
M. Boreale and R. De Nicola. Testing equivalence for mobile processes. Information and Computation, 120(2):279–303, August 1995.
Data encryption standard. Fed. Inform. Processing Standards Pub. 46, National Bureau of Standards, Washington DC, January 1977.
R. De Nicola and M. C. B. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83–133, 1984.
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.
R. A. Kemmerer. Analyzing encryption protocols using formal verification techniques. IEEE Journal on Selected Areas in Communications, 7, 1989.
A. Liebl. Authentication in distributed systems: A bibliography. ACM Operating Systems Review, 27(4):31–41, 1993.
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.
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.
C. Meadows. Applying formal methods to the analysis of a key management protocol. Journal of Computer Security, 1(1):5–36, 1992.
R. Milner. Communication and Concurrency. Prentice-Hall International, 1989.
R. Milner. Functions as processes. Mathematical Structures in Computer Science, 2:119–141, 1992.
J. K. Millen. The Interrogator model. In IEEE Symposium on Security and Privacy, pages 251–260, 1995.
R. Milner. The π-calculus. Undergraduate lecture notes, Cambridge University, 1995.
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.
S. Schneider. Security properties and CSP. In IEEE Symposium on Security and Privacy, pages 174–187, 1996.
B. Schneier. Applied Cryptography: Protocols, Algorithms, and Source Code in C. John Wiley & Sons, Inc., second edition, 1996.
Author information
Authors and Affiliations
Editor information
Rights 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