  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.
