Sciweavers

CSFW
2010
IEEE

Automating Open Bisimulation Checking for the Spi Calculus

13 years 6 months ago
Automating Open Bisimulation Checking for the Spi Calculus
We consider the problem of automating open bisimulation checking for the spi-calculus, an extension of the pi-calculus with cryptographic primitives. The notion of open bisimulation considered here 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. Our decision procedure uses techniques that have been well developed in the area of symbolic trace analysis for security protocols. More specifically, we make use of techniques for symbolic trace refinement, which transform a symbolic trace into a finite set of sym...
Alwen Tiu, Jeremy E. Dawson
Added 08 Sep 2010
Updated 08 Sep 2010
Type Conference
Year 2010
Where CSFW
Authors Alwen Tiu, Jeremy E. Dawson
Comments (0)