Titre de la dissertation: « Foundations of Attack-Defense Trees with dynamics semantics ».

Promoteur: Monsieur Thomas Brihaye et co-promotrice: Mme Sophie Pinchinat (Université de Rennes)

Résumé de la dissertation: 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 trees have since been the subject of many theoretical works addressing different formal approaches. Theoretical works often consider two different generalizations of attack trees, either by adding countermeasures (attack-defense trees) or by considering a dynamic system instead of a static setting.We first present a mathematical setting to tackle the two generalization of attack trees at the same time: we equip attack-defense trees (adts) with (trace) language semantics allowing to have an original dynamic interpretation of countermeasures. Interestingly, the expressiveness of adts coincides with star-free languages, and the nested countermeasures impact the expressiveness of adts. With an adequate notion of countermeasure-depth, we exhibit a strict hierarchy of the star-free languages that does not coincide with the classic one. Additionally, we define ADT-games, a game (similar to Ehrenfeucht-Fraïssé games) able to determine whether a language can be expressed by an adt with a certain number of countermeasures. Additionally, driven by the use of adts in practice, we address the decision problems of trace membership, non-emptiness, and equivalence, and study their computational complexities parameterized by the countermeasure-depth. Moreover, 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 show that a defining canonical inductive semantics in this setting as it is common for attack trees is not easily achievable in this setting. 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 PTIME in the path semantics.