Adversarial Formal Semantics of Attack Trees and Related Problems

TL;DR

This paper introduces a two-player game semantics for attack trees, analyzing their computational complexity and showing that certain problems are harder under this new interpretation compared to previous path semantics.

Contribution

It proposes a novel two-player game semantics for attack trees using concurrent game arenas, extending formal analysis and complexity results.

Findings

Emptiness problem is PSPACE-complete under the new semantics.

Membership problem is coNP-complete in the two-player interpretation.

Complexity of problems increases compared to path semantics.

Abstract

Security is a subject of increasing attention in our actual society in order to protect critical resources from information disclosure, theft or damage. The informal model of attack trees introduced by Schneier, and widespread in the industry, is advocated in the 2008 NATO report to govern the evaluation of the threat in risk analysis. Attack-defense trees have since been the subject of many theoretical works addressing different formal approaches. In 2017, M. Audinot et al. introduced a path semantics over a transition system for attack trees. Inspired by the later, we propose a two-player interpretation of the attack-tree formalism. To do so, we replace transition systems by concurrent game arenas and our associated semantics consist of strategies. We then show that the emptiness problem, known to be NP-complete for the path semantics, is now PSPACE-complete. Additionally, we show that the membership problem is coNP-complete for our two-player interpretation while it collapses to P in the path semantics.