Context-Sensitive Equivalences for Non-interference Based Protocol Analysis

We develop new proof techniques, based on non-interference, for the analysis of safety and liveness properties of cryptographic protocols expressed as terms of the process algebra CryptoSPA. Our approach draws on new notions of behavioral equivalence, built on top of a context-sensitive labelled transition system, that allow us to characterize the behavior of a process in the presence of any attacker with a given initial knowledge. We demonstrate the effectiveness of the approach with an example of a protocol of fair exchange.

• Type: Conference
• Year: 2003
• Where: FCT
• Authors: Michele Bugliesi, Ambra Ceccato, Sabina Rossi
• Keywords: Context-sensitive Labelled Transition, Cryptographic Protocols, FCT 2003, Process Algebra Cryptospa