-
Is my attack tree correct? Extended version
Authors:
Maxime Audinot,
Sophie Pinchinat,
Barbara Kordy
Abstract:
Attack trees are a popular way to represent and evaluate potential security threats on systems or infrastructures. The goal of this work is to provide a framework allowing to express and check whether an attack tree is consistent with the analyzed system. We model real systems using transition systems and introduce attack trees with formally specified node labels. We formulate the correctness prop…
▽ More
Attack trees are a popular way to represent and evaluate potential security threats on systems or infrastructures. The goal of this work is to provide a framework allowing to express and check whether an attack tree is consistent with the analyzed system. We model real systems using transition systems and introduce attack trees with formally specified node labels. We formulate the correctness properties of an attack tree with respect to a system and study the complexity of the corresponding decision problems. The proposed framework can be used in practice to assist security experts in manual creation of attack trees and enhance development of tools for automated generation of attack trees.
△ Less
Submitted 9 February, 2018; v1 submitted 26 June, 2017;
originally announced June 2017.
-
Attack Trees with Sequential Conjunction
Authors:
Ravi Jhawar,
Barbara Kordy,
Sjouke Mauw,
Sasa Radomirovic,
Rolando Trujillo-Rasua
Abstract:
We provide the first formal foundation of SAND attack trees which are a popular extension of the well-known attack trees. The SAND attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator SAND. This operator enables the modeling of ordered events.
We give a semantics to SAND attack trees by interpreting them as sets of series-parallel gr…
▽ More
We provide the first formal foundation of SAND attack trees which are a popular extension of the well-known attack trees. The SAND attack tree formalism increases the expressivity of attack trees by introducing the sequential conjunctive operator SAND. This operator enables the modeling of ordered events.
We give a semantics to SAND attack trees by interpreting them as sets of series-parallel graphs and propose a complete axiomatization of this semantics. We define normal forms for SAND attack trees and a term rewriting system which allows identification of semantically equivalent trees. Finally, we formalize how to quantitatively analyze SAND attack trees using attributes.
△ Less
Submitted 8 March, 2015;
originally announced March 2015.
-
Proceedings First International Workshop on Graphical Models for Security
Authors:
Barbara Kordy,
Sjouke Mauw,
Wolter Pieters
Abstract:
The present volume contains the proceedings of the First International Workshop on Graphical Models for Security (GraMSec'14). The workshop was held in Grenoble, France, on April 12, 2014, as one of the satellite events of the European Joint Conferences on Theory and Practice of Software 2014 (ETAPS'14).
Graphical security models provide an intuitive but systematic methodology to analyze securi…
▽ More
The present volume contains the proceedings of the First International Workshop on Graphical Models for Security (GraMSec'14). The workshop was held in Grenoble, France, on April 12, 2014, as one of the satellite events of the European Joint Conferences on Theory and Practice of Software 2014 (ETAPS'14).
Graphical security models provide an intuitive but systematic methodology to analyze security weaknesses of systems and to evaluate potential protection measures. Such models have been subject of academic research and they have also been widely accepted by the industrial sector, as a means to support and facilitate threat analysis and risk management processes.
The objective of GraMSec is to contribute to the development of well-founded graphical security models, efficient algorithms for their analysis, as well as methodologies for their practical usage. The workshop brings together academic researchers and industry practitioners designing and employing visual models for security in order to provide a platform for discussion, knowledge exchange and collaborations.
△ Less
Submitted 6 April, 2014;
originally announced April 2014.
-
ADTool: Security Analysis with Attack-Defense Trees (Extended Version)
Authors:
Barbara Kordy,
Piotr Kordy,
Sjouke Mauw,
Patrick Schweitzer
Abstract:
The ADTool is free, open source software assisting graphical modeling and quantitative analysis of security, using attack-defense trees. The main features of the ADTool are easy creation, efficient editing, and automated bottom-up evaluation of security-relevant measures. The tool also supports the usage of attack trees, protection trees and defense trees, which are all particular instances of att…
▽ More
The ADTool is free, open source software assisting graphical modeling and quantitative analysis of security, using attack-defense trees. The main features of the ADTool are easy creation, efficient editing, and automated bottom-up evaluation of security-relevant measures. The tool also supports the usage of attack trees, protection trees and defense trees, which are all particular instances of attack-defense trees.
△ Less
Submitted 11 June, 2013; v1 submitted 29 May, 2013;
originally announced May 2013.
-
DAG-Based Attack and Defense Modeling: Don't Miss the Forest for the Attack Trees
Authors:
Barbara Kordy,
Ludovic Piètre-Cambacédès,
Patrick Schweitzer
Abstract:
This paper presents the current state of the art on attack and defense modeling approaches that are based on directed acyclic graphs (DAGs). DAGs allow for a hierarchical decomposition of complex scenarios into simple, easily understandable and quantifiable actions. Methods based on threat trees and Bayesian networks are two well-known approaches to security modeling. However there exist more than…
▽ More
This paper presents the current state of the art on attack and defense modeling approaches that are based on directed acyclic graphs (DAGs). DAGs allow for a hierarchical decomposition of complex scenarios into simple, easily understandable and quantifiable actions. Methods based on threat trees and Bayesian networks are two well-known approaches to security modeling. However there exist more than 30 DAG-based methodologies, each having different features and goals. The objective of this survey is to present a complete overview of graphical attack and defense modeling techniques based on DAGs. This consists of summarizing the existing methodologies, comparing their features and proposing a taxonomy of the described formalisms. This article also supports the selection of an adequate modeling technique depending on user requirements.
△ Less
Submitted 29 March, 2013;
originally announced March 2013.
-
Quantitative Questions on Attack-Defense Trees
Authors:
Barbara Kordy,
Sjouke Mauw,
Patrick Schweitzer
Abstract:
Attack-defense trees are a novel methodology for graphical security modeling and assessment. The methodology includes visual, intuitive tree models whose analysis is supported by a rigorous mathematical formalism. Both, the intuitive and the formal components of the approach can be used for quantitative analysis of attack-defense scenarios. In practice, we use intuitive questions to ask about aspe…
▽ More
Attack-defense trees are a novel methodology for graphical security modeling and assessment. The methodology includes visual, intuitive tree models whose analysis is supported by a rigorous mathematical formalism. Both, the intuitive and the formal components of the approach can be used for quantitative analysis of attack-defense scenarios. In practice, we use intuitive questions to ask about aspects of scenarios we are interested in. Formally, a computational procedure, defined with the help of attribute domains and a bottom-up algorithm, is applied to derive the corresponding numerical values.
This paper bridges the gap between the intuitive and the formal way of quantitatively assessing attack-defense scenarios. We discuss how to properly specify a question, so that it can be answered unambiguously. Given a well specified question, we then show how to derive an appropriate attribute domain which constitutes the corresponding formal model. Since any attack tree is in particular an attack-defense tree, our analysis is also an advancement of the attack tree methodology.
△ Less
Submitted 30 October, 2012;
originally announced October 2012.
-
Attack--Defense Trees and Two-Player Binary Zero-Sum Extensive Form Games Are Equivalent - Technical Report with Proofs
Authors:
Barbara Kordy,
Sjouke Mauw,
Matthijs Melissen,
Patrick Schweitzer
Abstract:
Attack--defense trees are used to describe security weaknesses of a system and possible countermeasures. In this paper, the connection between attack--defense trees and game theory is made explicit. We show that attack--defense trees and binary zero-sum two-player extensive form games have equivalent expressive power when considering satisfiability, in the sense that they can be converted into eac…
▽ More
Attack--defense trees are used to describe security weaknesses of a system and possible countermeasures. In this paper, the connection between attack--defense trees and game theory is made explicit. We show that attack--defense trees and binary zero-sum two-player extensive form games have equivalent expressive power when considering satisfiability, in the sense that they can be converted into each other while preserving their outcome and their internal structure.
△ Less
Submitted 4 May, 2011; v1 submitted 14 June, 2010;
originally announced June 2010.