zbMATH — the first resource for mathematics

On compositional reasoning in the spi-calculus. (English) Zbl 1077.68713
Nielsen, Mogens (ed.) et al., Foundations of software science and computation structures. 5th international conference, FOSSACS 2002, held as part of the joint European conferences on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43366-X). Lect. Notes Comput. Sci. 2303, 67-81 (2002).
Summary: Observational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in $$\pi$$-calculus, these equivalences do not enjoy a simple formulation in spi-calculus. The present paper aims at enriching the set of tools for reasoning on processes by providing a few equational laws for a sensible notion of spi-bisimilarity. We discuss the difficulties underlying compositional reasoning in spi-calculus and show that, in some cases and with some care, the proposed laws can be used to build compositional proofs. A selection of these laws forms the basis of a proof system that we show to be sound and complete for the strong version of bisimilarity.
For the entire collection see [Zbl 0989.00051].

MSC:
 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: