The Spi-calculus is a process calculus intended for the description and verification of security protocols. Abadi and Gordon have described how common notions of correctness can be described by means of behavioural equivalence for the Spi-calculus. They suggest using testing equivalence as the notion of behavioural equivalence. However, proving testing equivalence is hard, wherefore some alternative notions of equivalence have been proposed.

Abadi and Gordon introduced the notion of framed bisimilarity and Boreale et al. introduced the notion of environment sensitive bisimilarity. Both equivalences are already known to be sound approximations of may-testing equivalence.

In this report we show that framed bisimilarity and a strong late version of environment sensitive bisimilarity are in fact one and the same relation. We have also formulated an early version of framed bisimilarity, called frameless framed bisimilarity, and shown that this is the same as a strong early environment sensitive bisimilarity.

Finally, we propose some modal logics for the Spi-calculus and show that strong early and strong late environment sensitive bisimilarity can be characterized by these logics.