Arbres d'attaque-défense multi-agent pour l'analyse de 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.