Formalising Observer Theory for Environment-Sensitive Bisimulation

Abstract. We consider a formalisation of a notion of observer (or intruder) theories, commonly used in symbolic analysis of security protocols. An observer theory describes the knowledge and capabilities of an observer, and can be given a formal account using deductive systems, such as those used in various “environment-sensitive” bisimulation for process calculi, e.g., the spi-calculus. Two notions are critical to the correctness of such formalisations and the effectiveness of symbolic techniques based on them: decidability of message deduction by the observer and consistency of a given observer theory. We consider a formalisation, in Isabelle/HOL, of both notions based on an encoding of observer theories as pairs of symbolic traces. This encoding has recently been used in a theory of open bisimulation for the spi-calculus. We machine-checked some important properties, including decidability of observer deduction and consistency, and some key steps which are crucial to the automa...

• Type: Conference
• Year: 2009
• Where: TPHOL
• Authors: Jeremy E. Dawson, Alwen Tiu
• Keywords: Artificial Intelligence, Observer Theories, Observer Theory, Open Bisimulation, TPHOL 2009