Mobile Calculi based on Domains

On Compositional Reasoning in the spi-calculus

M. Boreale and D. Gorla


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.

  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 = \{}

About this site. Last modified: Tue Jun 19 17:49:14 CEST 2018