Automated generation of attack trees with optimal shape and labelling

The problem this article addresses is, given a formal specification of a system, how to produce an attack tree that correctly and clearly describes the ways the system can be attacked. Correctness means that the attacks displayed by the attack tree are indeed attacks in the system; clarity means that the tree is efficient in communicating the attack scenario. To pursue clarity, we introduce an attack-tree generation algorithm that minimises the tree size and the information length of its labels without sacrificing correctness. We achieve this by establishing a connection between the problem of factorising algebraic expressions and the problem of minimising the tree size. Notably, our generation algorithm can handle complex attacks that execute actions in parallel and sequentially. For completeness, we introduce a system model that integrates well with our generation approach, and validate the resulting framework via a running example.