Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Attack Trees


view this post on Zulip Email Gateway (Aug 23 2022 at 08:49):

From: Lawrence Paulson <lp15@cam.ac.uk>
We’ve been deluged by submissions lately and I’m happy to announce

Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems, by Florian Kammüller:

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.

You’ll find it at https://www.isa-afp.org/entries/Attack_Trees.html

Larry


Last updated: Mar 29 2024 at 12:28 UTC