Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems
Other
Kammueller, F. 2020. Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems.
Title | Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems |
---|---|
Authors | Kammueller, F. |
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 succeed in developing a generic theory of Attack Trees with a state-based semantics based on Kripke structures and CTL (see [2] for more details). 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. A more detailed account of the Attack Tree formalisation is given in [3] and the case study is described in detail in [4]. |
ISSN | 2150-914X |
Journal or Publication | Archive of Formal Proof |
Publication dates | |
Online | 27 Apr 2020 |
Publication process dates | |
Deposited | 11 Sep 2020 |
Accepted | 27 Apr 2020 |
Output status | Published |
Web address (URL) | https://www.isa-afp.org/entries/Attack_Trees.html |
Language | English |
Publisher's version | File Access Level Restricted |
https://repository.mdx.ac.uk/item/89104
65
total views2
total downloads0
views this month0
downloads this month