Model Checking the IKEv2 Protocol Using Spin - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Pré-Publication, Document De Travail Année : 2019

Model Checking the IKEv2 Protocol Using Spin

Résumé

Previous analyses of IKEv2 concluded that the protocol was suffering from two authentication vulnerabilities: the penultimate authentication flaw and a vulnerability that leads to a reflection attack. In this paper we analyze the IKEv2 protocol specification using the Spin model checker. To do so we extend and improve an existing modeling method that allows analyzing security protocols using Spin. For completeness we indicate each abstraction we make when writing the model. As a result we show that the reflection attack is actually not applicable. We further discuss two modifications of the protocol that we prove to be effective against the penultimate authentication flaw.
Fichier principal
Vignette du fichier
fortemc.pdf (280.8 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02062292 , version 1 (08-03-2019)
hal-02062292 , version 2 (23-10-2019)

Identifiants

  • HAL Id : hal-02062292 , version 1

Citer

Tristan Ninet, Axel Legay, Romaric Maillard, Louis-Marie Traonouez, Olivier Zendra. Model Checking the IKEv2 Protocol Using Spin. 2019. ⟨hal-02062292v1⟩
206 Consultations
825 Téléchargements

Partager

Gmail Facebook X LinkedIn More