A Method for Proving Observational Equivalence

13 years 11 months ago
A Method for Proving Observational Equivalence
—Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy (expressed as a reachability property) or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require the notion of observational equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography. In this paper, we consider the applied pi calculus and we show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. Then, for simple processes without replication nor else branch, we reduce the decidability of trace equivalence to deciding an equivalence relation i...
Véronique Cortier, Stéphanie Delaune
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where CSFW
Authors Véronique Cortier, Stéphanie Delaune
Comments (0)