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.