CONCUR 2004 START ConferenceManager    

Symbolic Bisimulation in the Spi Calculus

Johannes Borgström, Sébastien Briais, Uwe Nestmann

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


The spi calculus is an executable model for the description and analysis of cryptographic protocols. Security objectives like secrecy and authenticity can be formulated as equations between spi calculus terms, where equality is interpreted as a contextual equivalence.

One problem common to message-passing process calculi is the infinite branching on process input. We propose a general symbolic semantics for the full spi calculus, where an input prefix gives rise to only one transition.

Due to the usual problems of verifying contextual equivalences, concrete bisimulations closely approximating barbed equivalence have been defined. In this paper, we propose a symbolic bisimulation that is sound with respect to barbed equivalence, and brings us closer to automated bisimulation checks.

START Conference Manager (V2.47.4)