Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap

Operational models of (security) protocols, on one hand, are readable and conveniently match their implementation (at a certain abstraction level). Epistemic models, on the other hand, are appropriate for specifying knowledge-related properties such as anonymity or secrecy. These two approaches to specification and verification have so far developed in parallel and one has either to define ad hoc correctness criteria for the operational model or use complicated epistemic models to specify the operational behavior. We work towards bridging this gap by proposing a combined framework which allows for modeling the behavior of a protocol in a process language with an operational semantics and supports reasoning about properties expressed in a rich logic which combines temporal and epistemic operators.

• Type: Conference
• Year: 2007
• Where: LPAR
• Authors: Francien Dechesne, Mohammad Reza Mousavi, Simona Orzan
• Keywords: Artificial Intelligence, Certain Abstraction Level, Epistemic Models, LPAR 2007, Operational Model