ADTLANG: A Programming Language Approach to Attack Defense Trees

The Attack Defense Tree framework was developed to facilitate abstract reasoning about security issues of complex systems. As such, a zoo of techniques and extensions have emerged in an attempt to extend the simple Boolean logic of Attack Defense Trees with behavioral properties and quantities. In this paper we expand the modeling power of Attack Defense Trees by introducing a notion of temporal dependencies between attacks, forcing specific ordering of event in successful attacks. Importantly, we introduce a notion of policy for the defender, facilitating a pseudo-active defender, mechanically reacting to the choices of an attacker. To easen the use of Attack Defense Trees we introduce a domain specific language (DSL) and an accompanying tool. The introduction of the DSL facilitates reuse, modularity, collaborative tree construction and separation of logical properties and quantitative/behavioral elements. The usefulness of our framework is exhibited on a small running example, utilizing the policy-notion to implement a reactive Break The Glass policy. We note that all the implemented analysis techniques use well established tools from the formal methods community to produce the given results, relying on non-trivial and automatic translation to and from the target formalisms. Lastly we present our Open Source prototype-tool, capable of conducting various analysis and visualizing the results.