Reasoning about Cryptographic Protocols in Observational Theories
Imen Zaabar, Narjes Berregeb · 2007
A lot of models have been applied to the analysis of cryptographic protocols. Some of them formalize security properties as reachability and some others express them as observational equivalences. In this paper, our intent is to present the main ideas for reasoning about cryptographic protocols in the framework of observational theories. We model protocols by term rewriting systems and express secrecy and authentication properties by observational equivalences, in a way close to spi-calculus (Abadi and Gordon, 1999)