Automating Open Bisimulation Checking for the Spi Calculus

Title: Automating Open Bisimulation Checking for the Spi Calculus
Speaker: Alwen Tiu (Joint work with Jeremy Dawson), Australian National University
Time: 3:00pm, Thursday,Nov.25
Venue: Lecture Room, Level 3 Building #5, Institute of Software, CAS

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.