Dawson, JeremyTiu, Alwen2015-12-079783642033582http://hdl.handle.net/1885/20863We 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 automation of open bisimulation checking for the spi-calculus, and highlight some novelty in our Isabelle/HOL formalisations of decidability proofs.Keywords: Bisimulation checking; Bisimulations; Deductive systems; Environment-sensitive; Formalisation; Isabelle/HOl; Observer theory; Process calculi; Security protocols; Spi calculus; Symbolic analysis; Symbolic techniques; Biomineralization; Calculations; Commu200910.1007/978-3-642-03359-9_142016-02-24