Michele Boreale, Rocco De Nicola, Rosario Pugliese

Dipartimento di Sistemi e Informatica, Università di Firenze

Abstract

Contextual equivalences for cryptographic process calculi, like the
spi-calculus, can be used to reason about correctness of protocols,
but their definition suffers from quantification over all possible
contexts. Here, we focus on two such equivalences, namely may-testing
and barbed equivalence, and investigate tractable proof methods for them.
To this aim, we design an enriched labelled transition system, where
transitions are constrained by the knowledge the environment has of
names and keys. The new transition system is then used to define a
trace equivalence and a weak bisimulation equivalence, that avoid
quantification over contexts. Our main results are soundness and
completeness of trace and weak bisimulation equivalence with respect
to may-testing and barbed equivalence, respectively. They lead to more
direct proof methods for equivalence checking. The use of these methods
is illustrated with a few examples, concerning implementation of secure
channels and verification of protocol correctness.