Towards Automatic Bisimilarity Checking in the Spi Calculus
Anders Strandløv Elkjær, Michael Höhle, Hans Hüttel · 2002
The spi calculus by Abadi and Gordon, an extension of Robin Milner's π-calculus, is designed to model cryptographic protocols. Classic security properties are easily expressed in spi using the notion of testing equivalence by De Nicola and Hennessy. However, proving processes testing equivalent is a daunting task. Thus framed bisimilarity, a bisimulation method implying testing equivalence, has been proposed by Abadi and Gordon. Unfortunately this method is immediately not suited for automation, as the definition of framed bisimilarity uses several levels of quantification over infinite domains. In this paper we define fenced bisimilarity, a concept similar to framed bisimilarity in which one of these quantifiers has been eliminated. We prove that fenced bisimilarity is a sound and complete characterization of framed bisimilarity. Though fenced bisimilarity is a step towards automation, there is still work to be done before a fully automated tool can be implemented.