Université de Rennes 1 Formal verification of the Internet Key Exchange (IKEv2) security protocol Vérification formelle du protocole d'échange de clé IKEv2 Protocole cryptographiqueVérification formelleIKEv2Déni de service Cryptographic protocolFormal verificationIKEv2Denial-of-Service Cryptographie Systèmes informatiques -- Mesures de sûreté Dans cette thèse, nous analysons le protocole IKEv2 à l'aide de trois outils de vérification formelle : Spin, ProVerif et Tamarin. Pour effectuer l'analyse avec Spin, nous étendons une méthode existante de modélisation. En particulier, nous proposons un modèle de la signature numérique, du MAC et de l'exponentiation modulaire, nous simplifions le modèle d'adversaire pour le rendre applicable à des protocoles complexes, et nous proposons des modèles de propriétés d'authentification. Nos analyses montrent que l'attaque par réflexion, une attaque trouvée par une précédente analyse, n'existe pas. De plus, nos analyses avec ProVerif et Tamarin produisent de nouvelles preuves concernant les garanties d'accord non injectif et d'accord injectif pour IKEv2 dans le modèle non borné. Nous montrons ensuite que la faille de pénultième authentification, une vulnérabilité considérée comme bénigne par les analyses précédentes, permet en fait d'effectuer un nouveau type d'attaque par déni de service auquel IKEv2 est vulnérable : l'Attaque par Déviation. Cette attaque est plus difficile à détecter que les attaques par déni de service classiques mais est également plus difficile à réaliser. Afin de démontrer concrètement sa faisabilité, nous attaquons avec succès une implémentation open-source populaire de IKEv2. Les contre-mesures classiques aux attaques DoS ne permettent pas d'éviter cette attaque. Nous proposons alors deux modifications simples du protocole, et prouvons formellement que chacune d'entre elles empêche l'Attaque par Déviation. In this thesis, we analyze the IKEv2 protocol specification using three formal verification tools: Spin, ProVerif and Tamarin. To perform the analysis with Spin, we extend and improve an existing modeling method with a simpler adversary model and a model for common cryptographic primitives and Lowe's authentication properties. As a result we show that the reflection attack, an attack found by a previous analysis, is actually not applicable. Moreover, our analysis using ProVerif and Tamarin provides new results regarding non-injective agreement and injective agreement guaranties of IKEv2 in the unbounded model. We then show that the penultimate authentication flaw, a vulnerability that was considered harmless by previous analyses, actually allows for a new type of Denial-of-Service attack, which works against IKEv2: the Deviation Attack. The Deviation Attack is harder to detect than existing DoS attacks, but is also harder to perform. To concretely demonstrate the attack, we successfully implement it against a popular open-source implementation of IKEv2. Finally, we study the use of existing DoS countermeasures and existing configuration options to defeat the attack, but we only find mitigations or incomplete workarounds. We therefore tackle the problem at a higher level: we propose two possible inexpensive modifications of the protocol, and formally prove that they both prevent the attack. Electronic Thesis or DissertationText en application/pdf1 : 1358 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/f29befcd-d429-42a5-9216-1257e76ded8b Ninet Tristan 1992-10-21 FR 245239189 ninettristan@gmail.com 2020REN1S002 http://www.theses.fr/2020REN1S002 2020-03-09 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiDelauneStéphanieintervenant_1109561384ZendraOlivierintervenant_2133979555 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 DelauneStéphanieZendraOlivierUniversite 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 1390180