On Compositional Reasoning in the Spi-Calculus

Michele Boreale and Daniele Gorla

Paper appeared in 5th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS '02), Grenoble (France), April 6-14, 2002.

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

@InProceedings{BG:FoSSaCs02,
  author    =   {M. Boreale and D. Gorla},
  title     =   {On Compositional Reasoning in the Spi-Calculus},
  editor    =   {M. Nielsen and U. Engberg},
  booktitle =   {Proc. of 5th Intern.Conf. on Foundations of Software Science and Computation Structures (FoSSaCS'02)},
  series    =   {LNCS},
  volume    =  	{2303},
  pages     = 	{67--81},
  year      =  	{2002},
  publisher =   {Springer},
}

Home page / Publications