Skip to Main content Skip to Navigation
Theses

Résolution de problèmes d'accessiblité pour la compilation et la validation de protocoles cryptographiques

Abstract : Commercial transactions and services over insecure networks have lead to the use of security protocols. These protocols ought to provide both data confidentiality and participants authentication, but many of those proposed up to date have turned out to be flawed. Their economical importance has motivated the introduction of formal verification. In this dissertation, we investigate the problems raised by the automatic analysis of such protocols. We give an operationnal semantics to high-level protocol specifications, extend the standard Dolev-Yao framework to algebraic operators and finally consider the problem of protocol verification. We reduce these problems to reachability problems. This reduction is a first steptoward the implementation of an automatic analysis tool.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2003_0181_CHEVALIER.pdf
Complete list of metadata

https://hal.univ-lorraine.fr/tel-01746836
Contributor : Thèses Ul Connect in order to contact the contributor
Submitted on : Thursday, March 29, 2018 - 10:45:49 AM
Last modification on : Saturday, October 16, 2021 - 11:26:08 AM

Identifiers

  • HAL Id : tel-01746836, version 1

Collections

Citation

Yannick Chevalier. Résolution de problèmes d'accessiblité pour la compilation et la validation de protocoles cryptographiques. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2003. Français. ⟨NNT : 2003NAN10181⟩. ⟨tel-01746836⟩

Share

Metrics

Record views

24