Observational equivalences can be used to reason about the
correctness of protocols described in the spi-calculus, but they
do not enjoy the same pleasant properties they enjoy in CCS
or in pi-calculus. The present paper aims at enriching the
set of tools for reasoning on spi-processes by providing a
few equational laws for a sensible notion of spi-calculus
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.
