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 / Boreale, M; Gorla, Daniele. - STAMPA. - LNCS 2303:(2002), pp. 67-81. (Intervento presentato al convegno FOSSACS 2002 tenutosi a Grenoble (France)) [10.1007/3-540-45931-6_6].
On Compositional Reasoning in the Spi–Calculus
GORLA, DANIELE
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.