Attack trees in Isabelle

DOI10.1007/978-3-030-01950-1_36zbMATH Open1497.68548arXiv1803.06494OpenAlexW2804520164MaRDI QIDQ2218979FDOQ2218979

Authors: Florian Kammüller 

Publication date: 18 January 2021

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/1803.06494

Recommendations

• Information Security and Cryptology - ICISC 2005
• Attack-defense trees
• Is my attack tree correct?
• Model Checking Exact Cost for Attack Scenarios
• Semantics for specialising attack trees based on linear logic

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Formalization of mathematics in connection with theorem provers (68V20)

Cited In (4)

• Semantics for specialising attack trees based on linear logic
• Attack-defense trees
• Theory of disjunctive attacks, Part I
• Simple infeasibility certificates for attack trees

This page was built for publication: Attack trees in Isabelle

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2218979)