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 metadatas

https://hal.univ-lorraine.fr/tel-01746836
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:45:49 AM
Last modification on : Thursday, December 17, 2020 - 1:52:03 PM

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

17