| address at Office |
IRIT office 314 118 route de Narbonne 31062 Toulouse Cedex 04 France |
|
| electronic mail | chevalie@loria.fr | |
| phone number | (+33) 383 593 002 | |
| mon dossier de qualification disponible (ps,pdf). | ||
Ma thèse est désormais disponible en ligne (ps,pdf). Cette version n'est pas définitive, mais aucun changement n'est actuellement prévu dans le corps du texte.
My Phd dissertation, currently only available in french (ps,pdf). This version is the one submitted, and not the final version (though no changes are scheduled in the dissertation).
La généralisation de transactions commerciales et des services
sur des supports non-sécurisés a rendu nécessaire l'utilisation
de protocoles permettant de garantir aux participants la
confidentialité des données aussi bien que l'identification des
correspondants. De nombreux protocoles proposés se sont révélés
incorrects. Leur importance économique a motivé l'introduction
de méthodes formelles pour la détection d'erreurs.
Dans cette thèse, nous nous intéressons aux problèmes liés à
l'analyse automatique de ces protocoles. Nous donnons une
sémantique opérationnelle aux spécifications de haut niveau
habituellement utilisées, étendons le cadre standard de
l'analyse pour prendre en compte les propriétés des opérateurs
algébriques pour la recherche de failles et considérons le
problème de la vérification de protocoles. Nous réduisons ces
problèmes à des problèmes d'accessibilité pour des systèmes de
transitions définis par des règles de réécriture sur des
ensembles. Cette réduction permet de donner la complexité de ces
problèmes, et est une première étape vers une résolution par des
outils entièrement automatiques.
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
step toward the implementation of an automatic analysis tool.
| address at Office |
IRIT office 314 118 route de Narbonne 31062 Toulouse Cedex 04 France |
|
| electronic mail | chevalie@loria.fr | |
| phone number | (+33) 383 593 002 | |
| mon dossier de qualification disponible (ps,pdf). | ||