Symbolic Bisimulation in the Spi Calculus
2004 (English)In: CONCUR 2004: Concurrency theory, proceedings / [ed] P. Gardner and N. Yoshida, Berlin Heidelberg: Springer Berlin/Heidelberg, 2004, Vol. 3170, 161-176 p.Conference paper (Refereed)
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 with verifying contextual equivalences for message-passing process calculi is the infinite branching on process input. In this paper, we propose a general symbolic semantics for the spi calculus, where an input prefix gives rise to only one transition. To avoid infinite quantification over contexts, non-contextual concrete bisimulations approximating barbed equivalence have been defined. We propose a symbolic bisimulation that is sound with respect to barbed equivalence, and brings us closer to automated bisimulation checks.
Place, publisher, year, edition, pages
Berlin Heidelberg: Springer Berlin/Heidelberg, 2004. Vol. 3170, 161-176 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 3170
IdentifiersURN: urn:nbn:se:uu:diva-161485DOI: 10.1007/978-3-540-28644-8_11ISBN: 3-540-22940-XOAI: oai:DiVA.org:uu-161485DiVA: diva2:456278
International Conference on Concurrency Theory (CONCUR), 15th international conference, August 31 - September 3, 2004, London, UK