Université de Rennes 1 Assisted design and analysis of attack trees Assistance à la conception et l’analyse d’arbres d’attaque Arbres d’attaqueVérification de modèlesMéthodes formellesÉvaluation du risque Attack treesFormal methodsModel checkingRisk assessment Vérification de modèles (informatique)Thèses et écrits académiques Méthodes formelles (informatique)Thèses et écrits académiques En analyse de risques, les arbres d’attaque sont utilisés pour évaluer les menaces sur un système. Les méthodes formelles permettent leur analyse quantitative et leur synthèse, mais les propriétés exprimant la qualité des arbres d’attaque par rapport au système n’ont pas été formalisées. Dans ce document, nous définissons un nouveau cadre formel pour les arbres d’attaque prenant en compte un modèle opérationnel du système, et dotant les arbres d’une sémantique de chemins. Nous définissons les propriétés de correction des raffinements, et étudions leurs complexités. A partir d’une attaque optimale dans un modèle de système quantitatif, nous guidons la conception d’un arbre d’attaque, en indiquant ses feuilles qui contribuent à l’attaque optimale considérée. In risk analysis, attack trees are used to assess threats to a system. Formal methods allow for their quantitative analysis and synthesis, but the properties expressing the quality of the attack trees with respect to the system have not been formalized. In this document, we define a new formal framework for attack trees that takes an operational model of the system into account, and provides the trees with a path semantics. We define the correctness properties of refinements, and study their computational complexity. Given an optimal attack in a quantitative system model, we guide the design of a attack tree, indicating its leaves that contribute to considered the optimal attack. Electronic Thesis or DissertationText en application/pdf1 : 1386 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/e8de042b-7b43-4871-ae35-bb1ed014abce Audinot Maxime 1992-05-31 FR 235455539 maxime.audinot@gmail.com 2018REN1S082 http://www.theses.fr/2018REN1S082 2018-12-17 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiPinchinatSophieintervenant_1097578754 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 PinchinatSophieUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) IRISA ASCII PDF 1418796