Formalising Observer Theory for Environment-Sensitive Bisimulation
Date
2009
Authors
Dawson, Jeremy
Tiu, Alwen
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
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 automation of open bisimulation checking for the spi-calculus, and highlight some novelty in our Isabelle/HOL formalisations of decidability proofs.
Description
Keywords
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; Commu
Citation
Collections
Source
Type
Book chapter
Book Title
Theorem Proving in Higher Order Logics (TPHOLs)
Entity type
Access Statement
License Rights
Restricted until
2037-12-31
Downloads
File
Description