View article

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 …