2018/03/17 by Florian Kammüller, Kammüller, Florian · 1 citation
Computer Science · #Advanced Malware Detection Techniques #Cryptography and Security (cs.CR) #FOS: Computer and information sciences #Information and Cyber Security #Logic in Computer Science (cs.LO) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.1803.06494
openalex publication_date 2018/03/17 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.