Observational equivalences can be used to reason about the correctness of security protocols described in the spi-calculus. Unlike in CCS or in π-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.

On Compositional Reasoning in the Spi-calculus / M. BOREALE; D. GORLA. - STAMPA. - (2002), pp. 67-81. [10.1007/3-540-45931-6_6]

On Compositional Reasoning in the Spi-calculus

BOREALE, MICHELE;
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 π-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.
2002
9783540433668
5th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2002
67
81
M. BOREALE; D. GORLA
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificatore per citare o creare un link a questa risorsa: https://hdl.handle.net/2158/236452
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 8
social impact