**Title**:Automating Open Bisimulation Checking for
the Spi Calculus

**
Speaker**:

**Abstract**:The spi-calculus is an extension of the pi-calculus
with cryptographic primitives. Unlike the pi-calculus, due to the presence of
encryption operators, bisimulation equivalence in the spi-calculus needs to
take into account the capabilities of the intruder (or the environment) for
it to be useful in proving security properties such as secrecy and authentication.
In this talk, I will present the latest result in automating bisimulation checking
for finite spi-calculus. The notion of bisimulation considered here is called
open bisimulation, and is indexed by a (symbolic) environment, represented as
bi-traces (i.e., pairs of symbolic traces), which encode the history of interaction
between the intruder with the processes being checked for bisimilarity. A crucial
part of the definition of this open bisimulation, that is, the notion of consistency
of bi-traces, involves infinite quantification over a certain notion of respectful
substitutions. We show that one needs only to check a finite number of respectful
substitutions in order to check bi-trace consistency. We then give a sound and
complete procedure for deciding open-bisimilarity for finite spi-processes.

**Bio:**

Dr. Alwen Tiu is a research fellow at the Australian National University since
2006. He did his PhD at the Pennsylvania State University from 2001 - 2004,
but spent the last two years as a visiting student at Ecole Polytechnique, France.
Prior joining ANU, he spent one year at LORIA

(France) as a postdoc. His research interests include proof theory, logical
frameworks, process calculi and theorem proving. He has been particularly interested
in applying proof theoretic techniques to reason about process equivalence for
the pi-calculus and its extensions.