Université de Rennes Foundations of attack-defense trees with dynamic semantics Arbres d'attaque-défense multi-agent pour l'analyse de risque arbres d'attaque-défensesémantique formelleexpressivité attack-defense treesformal semanticsexpressiveness Systèmes informatiques -- Mesures de sûreté Évaluation du risque La sécurité est un sujet de plus en plus important dans notre société actuelle, afin de protéger les ressources critiques contre la divulgation d'informations, le vol ou les dommages. Le modèle informel des arbres d'attaque introduit par Schneier, et largement utilisé dans l'industrie, est recommandé dans le rapport de l'OTAN de 2008 pour gouverner l'évaluation de la menace dans l'analyse des risques. Depuis, les arbres d'attaque ont fait l'objet de nombreux travaux théoriques abordant différentes approches formelles. Ces travaux théoriques considèrent souvent deux généralisations différentes des arbres d'attaque, soit en ajoutant des contre-mesures (arbres d'attaque-défense), soit en considérant un système dynamique au lieu d'un cadre statique. Nous présentons d'abord un cadre mathématique pour traiter simultanément les deux généralisations des arbres d'attaque : nous équipons les arbres d'attaque-défense (ADT) d'une sémantique de langage (de traces), permettant d'avoir une interprétation dynamique originale des contre-mesures. Fait intéressant, l'expressivité des ADT coïncide avec les langages sans étoile, et les contre-mesures imbriquées impactent l'expressivité des ADT. Avec une notion appropriée de "profondeur des contre-mesures", nous exposons une hiérarchie stricte des langages sans étoile qui ne coïncide pas avec les hiérarchies classiques. De plus, nous définissons les ADT-games, des jeux (similaire aux jeux d'Ehrenfeucht-Fraïssé) capables de déterminer si un langage peut être exprimé par un ADT avec un certain nombre de contre-mesures imbriquées. Par ailleurs, motivés par l'utilisation des ADT en pratique, nous abordons les problèmes de décision concernant l'appartenance d'une trace à la sémantique, la non-vacuité et l'équivalence, et étudions leurs complexités computationnelles paramétrées par la profondeur des contre-mesures. De plus, nous proposons une interprétation à deux joueurs du formalisme des arbres d'attaque. Pour ce faire, nous remplaçons les systèmes de transition par des arènes de jeu concurrentes, et notre sémantique associée consiste en des stratégies. Nous montrons qu'une sémantique inductive canonique définissant cet ensemble, comme c'est courant pour les arbres d'attaque, n'est pas facilement réalisable dans ce cadre. Nous montrons ensuite que le problème de vacuité, connu pour être NP-complet dans la sémantique à 1 joueur, est désormais PSPACE-complet. De plus, nous montrons que le problème d'appartenance est coNP-complet pour notre interprétation à deux joueurs, tandis qu'il se réduit à PTIME dans la sémantique à 1 joueur. 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 generalizations of attack trees at the same time: we equip attack-defense trees (adts) with (trace) language semantics allowing us 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 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 with 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. Electronic Thesis or DissertationText en application/pdf1 : 798 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/36f2e681-a283-48a9-907e-9b67206dffb2 Terefenko Alexandre 1998-05-06 BE 293292353 alexandre.terefenko@gmail.com 2025URENS051 http://www.theses.fr/2025URENS051 2025-03-13 Informatique Université de Rennesthesis.degree.grantor_1 26693823X Université de Mons (Belgique)thesis.degree.grantor_2 190187433 Doctorat non ouiPinchinatSophieintervenant_1097578754BrihayeThomasintervenant_2203087011BruyèreVéroniqueintervenant_3197158641BertrandNathalieintervenant_6111647339BoigelotBernardintervenant_4292052944CartonOlivierintervenant_5032992149 MATISSEecoleDoctorale_1 267602553 IRISA partenaireRecherche_1 026386909 ddc:004 PinchinatSophieBrihayeThomasBruyèreVéroniqueBoigelotBernardCartonOlivierBertrandNathalieUniversité de RennesUniversité de Mons (Belgique)MATISSE IRISA ASCII PDF 817612