On Bisimulations for the Spi Calculus*
Johannes Borgström, Uwe Nestmann · Lecture notes in computer science · 2002
The spi calculus is an extension of the pi calculus with cryptographic primitives, designed for the verification of cryptographic protocols. Due to the extension, the naive adaptation of labeled bisimulations for the pi calculus is too strong to be useful for the purpose of verification. Instead, as a viable alternative, several “environment-sensitive” bisimulations have been proposed. In this paper we formally study the differences between these bisimulations. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.