Adversarial formal semantics of attack trees and related problems

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 [2], 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 (see [3] for an exhaustive list). In [1], the authors introduced a path semantics over a transition system for attack trees. The presentation will be established over an ongoing work framed by Sophie Pinchinat from IRISA and Thomas Brihaye from UMONS in which we generalise the works of [1] by allowing a multi-agent interpretation of the attack-tree formalism. To do it, we replace transition systems by concurrent game arenas and our associated semantics consist of strategies. We then show that our proposed semantics can be recognised by tree automata and we finish by determining bounds to the complexity of the emptiness problem. This problem answers the following question : is there a winning strategy for the the player/coalition trying to achieve the objective described by the attack tree ? References : [1] Maxime Audinot, Sophie Pinchinat, and Barbara Kordy, Is my attack tree correct?, European Symposium on Research in Computer Security, Springer, 2017, pp. 83–102. [2] Bruce Schneier, Attack trees, Dr. Dobbs journal 24 (1999), no. 12, 21–29. [3] Wojciech Wide l, Maxime Audinot, Barbara Fila, and Sophie Pinchinat, Beyond 2014: Formal methods for attack tree–based security modeling, ACM Computing Surveys (CSUR) 52 (2019), no. 4, 1–36.