Abstract:
The spi-calculus, proposed by Abadi and Gordon, is a process
calculus based on the 
-calculus and is intended for reasoning about the
behaviour of cryptographic protocols. We consider the finite-control fragment
of the spi-calculus, showing it to be Turing-powerful (a result which is
joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.) Next, we
restrict our attention to finite (non-recursive) spi-calculus. Here, we show
that framed bisimilarity, an equivalence relation proposed by Abadi and
Gordon, showing that it is decidable for this fragment
-calculus and is intended for reasoning about the
behaviour of cryptographic protocols. We consider the finite-control fragment
of the spi-calculus, showing it to be Turing-powerful (a result which is
joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.) Next, we
restrict our attention to finite (non-recursive) spi-calculus. Here, we show
that framed bisimilarity, an equivalence relation proposed by Abadi and
Gordon, showing that it is decidable for this fragmentAvailable as PostScript, PDF, DVI.