Mobile Calculi based on Domains


On Compositional Reasoning in the spi-calculus

M. Boreale and D. Gorla

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