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: Fri Apr 19 21:54:11 CEST 2024