Time: August 15, 2002, 13.00-14.30
Place: Fredrik Bajersvej 7, room E2-215
Joint work with: Ulrik Frendrup and Jesper Nyholm Jensen
We present three modal logics for the spi-calculus and show that they capture strong versions of the environment sensitive bisimulation introduced by Boreale et al. Our logics differ from conventional modal logics for process calculi in that they allow us to describe the knowledge of an attacker directly.
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 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 Bjorn 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.