
doi: 10.1109/csf.2009.9
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 introduced by M. Baudet. Altogether, this yields the first decidability result of observational equivalence for a general class of equational theories.
security protocols, applied pi calculus, observational equivalence, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
security protocols, applied pi calculus, observational equivalence, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 35 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
