AbstractWe introduce a definition of bisimulation for cryptographic protocols. The definition includes a simple and precise model of the knowledge of the environment with which a protocol interacts. Bisimulation is the basis of an effective proof technique, which yields proofs of classical security properties of protocols and also justifies certain protocol optimizations. The setting for our work is the spi calculus, an extension of the pi calculus with cryptographic primitives. We prove the soundness of the bisimulation proof technique within the spi calculus.
Categories and Subject Descriptors: C.2.2 [Computer-Communication Networks]: Network Protocols; D.1.3 [Programming Techniques]: Concurrent Programming; E.3 [Data Encryption]; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs
Additional Key Words and Phrases: cryptographic protocols, verification, bisimulation, process calculus
Selected references
- Martín Abadi and Andrew D. Gordon. Reasoning about cryptographic protocols in the spi calculus. In Antoni Mazurkiewicz and Józef Winkowski, editors, CONCUR '97: Concurrency Theory, 8th International Conference, volume 1243 of Lecture Notes in Computer Science, pages 59-73, Warsaw, Poland, 1-4 July 1997. Springer-Verlag.
- Jonathan K. Millen, Sidney C. Clark, and Sheryl B. Freedman. The interrogator: Protocol security analysis. IEEE Transactions on Software Engineering, 13(2):274-288, February 1987.
- Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Information and Computation, 100(1):1-40, September 1992.
- Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Information and Computation, 100(1):41-77, September 1992.
- Benjamin Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, October 1996.
- Andrew M. Pitts and Ian D. B. Stark. Observable properties of higher order functions that dynamically create local names, or What's new? In Andrzej M. Borzyszkowski and Stefan Sokolowski, editors, Mathematical Foundations of Computer Science 1993, 18th International Symposium, volume 711 of Lecture Notes in Computer Science, pages 122-141, Gdansk, Poland, 30 August-3 September 1993. Springer.