Nordic Journal of Computing Bibliography

Martín Abadi and Andrew D. Gordon. A Bisimulation Method for Cryptographic Protocols. Nordic Journal of Computing, 5(4):267-303, Winter 1998.

We 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


  • Nordic Journal of Computing homepage
  • Bibliography top level
  • Nordic Journal of Computing Author Index
  • Search the HBP database