TY - GEN

T1 - Automating open bisimulation checking for the Spi calculus

AU - Tiu, Alwen

AU - Dawson, Jeremy

PY - 2010

Y1 - 2010

N2 - 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 symbolic traces in a certain "solved form". Crucially, we show that refinements of a projection of a bitrace can be uniquely extended to refinements of the bi-trace, and that consistency of all instances of the original bi-trace can be reduced to consistency of its finite set of refinements. We then give a sound and complete procedure for deciding open bisimilarity for finite spi-processes.

AB - 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 symbolic traces in a certain "solved form". Crucially, we show that refinements of a projection of a bitrace can be uniquely extended to refinements of the bi-trace, and that consistency of all instances of the original bi-trace can be reduced to consistency of its finite set of refinements. We then give a sound and complete procedure for deciding open bisimilarity for finite spi-processes.

KW - Intruder deduction

KW - Open bisimulation

KW - Spi-calculus

KW - Symbolic trace analysis

UR - http://www.scopus.com/inward/record.url?scp=77957574536&partnerID=8YFLogxK

U2 - 10.1109/CSF.2010.28

DO - 10.1109/CSF.2010.28

M3 - Conference contribution

SN - 9780769540825

T3 - Proceedings - IEEE Computer Security Foundations Symposium

SP - 307

EP - 321

BT - 23rd IEEE Computer Security Foundations Symposium, CSF 2010

T2 - 23rd Computer Security Foundations Symposium, CSF 2010

Y2 - 17 July 2010 through 19 July 2010

ER -