Computer Science – Cryptography and Security
Scientific paper
2009-01-15
Computer Science
Cryptography and Security
This is a revised and extended version of a conference paper presented at APLAS 2007
Scientific paper
A notion of open bisimulation is formulated for the spi calculus, an extension of the pi-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 relation on finite processes. As far as we know, this is the first formulation of open bisimulation for the spi calculus for which the congruence result is proved.
No associations
LandOfFree
A Trace Based Bisimulation for the Spi Calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Trace Based Bisimulation for the Spi Calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Trace Based Bisimulation for the Spi Calculus will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-589582