Formal trace semantics for attack-defence trees

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-defence 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 formal trace semantics over a transition system for attack trees. However, none formal trace semantics have
been considered for Attack-defence trees in the literature. The presentation
will be established over an ongoing work framed by Sophie Pinchinat from
IRISA and Thomas Brihaye from UMONS in which we propose to generalise the formalism of [1] by allowing attack trees to use a new operator
of arity 2, called the counter and represented by C, to try to bring closer
an attack-defence interpretation.
[1] Sophie Pinchinat, Barbara Fila, Florence Wacheux, and Yann ThierryMieg, Attack trees: a notion of missing attacks, International Workshop
on Graphical Models for Security, Springer, 2019, pp. 23–49.
[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.