Vérification des protocoles cryptographiques : comparaison des modèles symboliques avec une application des résultats : étude des protocoles récursifs

Abstract : This thesis deals with formal verification of cryptographic protocols. It is about symbolic modelling of protocols with the objective to prove security properties. The thesis is split in two parts: The first part defines four symbolic models which differ in the syntactic resources that protocol designers may use do model cryptographic primitives. We found that engineers employ coding dodges in order to model missing cryptographic primitives in simpler models. We showed that these codings are correct in that protocol properties that are proven in lean models also hold in more elaborated models. We finish this part with the description of a module implementation for the verification plate-form AVISPA. The module is based on results that allow to automatically translate protocol properties, proven in symbolic models, to computational models. In the second part of this thesis, we develop a symbolic model in order to represent ecursive protocols. This class of protocols is difficult to analyse and, so far, there are only few decidability results. We show that our symbolic model allows us to retrieve an previously known attack against a special security property of an e-commerce protocol. We then modify this protocol and show that the property holds for the modified protocol.
Document type :
Theses
Complete list of metadatas

Cited literature [86 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-01748257
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 11:29:57 AM
Last modification on : Tuesday, April 24, 2018 - 1:53:22 PM
Long-term archiving on : Friday, September 14, 2018 - 8:28:13 AM

File

SCD_T_2007_0083_HORDEGEN.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01748257, version 1

Collections

Citation

Heinrich Hördegen. Vérification des protocoles cryptographiques : comparaison des modèles symboliques avec une application des résultats : étude des protocoles récursifs. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2007. Français. ⟨NNT : 2007NAN10083⟩. ⟨tel-01748257⟩

Share

Metrics

Record views

19

Files downloads

31