On Compositional Reasoning in the spi-calculus

Abstract

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. 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 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.

@InProceedings\{boreale.gorla:compositional-reasoning-spi-calculus, author = \{M. Boreale and D. Gorla}, title = \{On Compositional Reasoning in the spi-calculus}, booktitle = \{Proceedings of Foundations of Software Technology and Computation Structures 2002}, year = \{2002}, volume = \{2303}, series = \{Lecturer notes in computer science}, publisher = \{Springer Verlag}, url = \{http://mikado.di.fc.ul.pt/repository/boreale.gorla_compositional-reasoning-spi-calculus.pdf} }

About this site. Last modified: Wed Sep 20 22:02:13 CEST 2017