Sciweavers

Share
APLAS
2007
ACM

A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract

9 years 5 months ago
A Trace Based Bisimulation for the Spi Calculus: An Extended Abstract
: An Extended Abstract Alwen Tiu Computer Sciences Laboratory Australian National University Abstract. A notion of open bisimulation is formulated for the spi calculus, an extension of the -calculus with cryptographic primitives. In this formulation, open bisimulation is indexed by pairs of symbolic traces, which represent the history of interactions between the environment with the pairs of processes being checked for bisimilarity. The use of symbolic traces allows for a symbolic treatment of bound input in bisimulation checking which avoids quantification over input values. Open bisimilarity is shown to be sound with respect to testing equivalence, and futher, it is shown to be an equivalence relation on processes and a congruence on finite processes.
Alwen Tiu
Added 12 Aug 2010
Updated 12 Aug 2010
Type Conference
Year 2007
Where APLAS
Authors Alwen Tiu
Comments (0)
books