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.
2002
FOSSACS 2002
sei calculus, inference system, bisimulation
04 Pubblicazione in atti di convegno::04b Atto di convegno in volume
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].
File allegati a questo prodotto
Non ci sono file associati a questo prodotto.

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

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11573/56000
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 8
social impact