A Bisimulation Method for Cryptogaphic Protocols

摘要

We introduce a definition of bisimulation for cryptogaphic protocols. The definition includes a simple and precise model of the knowledge of the environment with which a prtocol interacts. Bisimulation is the basis of an effective proof technique, which yields proofs of classical security properties of protocols nad also justifies certain protocol optimisations. The setting for our work is the spi calculus, an extension of the pi calculus with crypptographic primitives. We prove the soundness of the bisiumlation proof technique within the spi calculus.