Attack Trees in Isabelle 
Florian Kammueller 

In this talk, 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.