Deciding the non-emptiness of attack trees

Abstract

We define and study the decision problem of the non-emptiness of an attack tree. This decision problem reflects the natural question of knowing whether some attack scenario described by the tree can be realized in (a given model of) the system to defend. We establish accurate complexity bounds, ranging from -completeness for arbitrary trees down to -completeness for trees with no occurrence of the AND operator. Additionally, if the input system to defend has a succinct description, the non-emptiness problem becomes -complete.