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.

翻译：本文提出了一种在伊莎贝尔的高阶逻辑（HOL）中高效实现模型检测的方法。由于模型检测通常局限于有限状态集，这是一项具有挑战性的任务。通过将研究范围限定于安全攻击场景，我们实现了针对攻击树模型检测算法的高效可执行规范。本文提供了现有研究背景、基础理论，并展示了其应用实例。所有理论与应用均在伊莎贝尔中完成形式化验证，从而生成了可执行的模型检测算法。