(Swansea)

We model the notion of Framed Bisimulation in the interactive theoremprover 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.

Robert Recorde Room

Department of Computer Science