Deciding Framed Bisimilarity

Hans Huttel


Abstract

The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the pi-calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for finite (non-recursive) spi-calculus processes.