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 -