Higher Order Model Checking in Isabelle for Human Centric Infrastructure Security

TL;DR

The paper addresses executing model checking for attack trees inside Isabelle/HOL, despite the general undecidability of HOL-based verification. It introduces an efficient, executable realization using a computable state-transition representation, a mapping EsetI, and a st_e evaluator, enabling CTL-guided attack-tree verification via $EF$-style semantics. Correctness and completeness are established through the $AT\_EF$ theorem and related Completeness results, linking attack-tree validity to CTL properties and supporting automated code generation. An IoT healthcare case study demonstrates practical detection of privacy attacks and illustrates integration with the Refinement-Risk cycle for human-centric security analysis.

Abstract

In this paper we present an efficient approach to implementing model checking in the Higher Order Logic (HOL) of Isabelle. This is a non-trivial task since model checking is restricted to finite state sets. By restricting our scope to considering security attacks, we achieve an efficient executable specification of a model checking algorithm for attack trees. We provide the existing background, the necessary theory and illustrate its application. Theory and application are fully formalized in Isabelle thus providing an executable model checking algorithm.