Authors
Michele Boreale, Rocco De Nicola, Rosario Pugliese
Publication date
2001
Journal
SIAM Journal on Computing
Volume
31
Issue
3
Pages
947-986
Publisher
Society for Industrial and Applied Mathematics
Description
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 …
Total citations
Scholar articles
M Boreale, R De Nicola, R Pugliese - SIAM Journal on Computing, 2001