Towards semi automated equivalence checking of spi calculus processes

Temesghen Kahsai

(Swansea)

We model the notion of Framed Bisimulation in the interactive theorem
prover Isabelle using the logic HOL-Nominal. Framed Bisimulation was
introduced in 1998 by Abadi and Gordon, who used it in order to reason
about cryptographic protocols formulated in Spi-Calculus. The logic
HOL-Nominal is a novel way of reasoning for calculi with binding
operators, such as Lambda calculus, Pi-calculus, and
Spi-calculus. Based on HOL-Nominal, we have developed a proof
environment which automates part of the decision procedure if two
processes are equivalent w.r.t. Framed Bisimulation. In our work we
use some of the ideas of Huttel's algorithm for deciding the
bisimilarity between processes. In particular, we decrease the search
space during the proof. Our proof environment makes it possible to
write proofs in Isabelle which closely correspond to the (traditional)
manual proofs presented in the literature.



Thursday 30th November 2006, 14:00
Robert Recorde Room
Department of Computer Science