Attack Trees in Isabelle
This work addresses the need for rigorous verification of security models in systems, though it is incremental as it builds on existing attack tree and formal logic methods.
The paper tackles the problem of formally verifying attack trees by developing a proof theory in Isabelle with a state-based semantics using Kripke structures and CTL, resulting in a framework that enables mechanical logic analysis and application to case studies like healthcare IoT and GDPR compliance.
In this paper, we present a proof theory for attack trees. Attack trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we succeed in developing a generic theory of attack trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of attack trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of attack tree validity and CTL. The application is illustrated on the example of a healthcare IoT system and GDPR compliance verification.