Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems

Title:	Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
Author:	Florian Kammueller
Submission date:	2020-04-27
Abstract:	In this article, 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 develop 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.
BibTeX:	@article{Attack_Trees-AFP, author = {Florian Kammueller}, title = {Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems}, journal = {Archive of Formal Proofs}, month = apr, year = 2020, note = {\url{http://isa-afp.org/entries/Attack_Trees.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.