Mémoires de Fin d’Etudes
Etablissement
Université d’Oran1 - Ahmed Ben Bella
Affiliation
Département d’Informatique
Auteur
ARIBI, Noureddine
Directeur de thèse
LEBBAH Yahia (Maitre de conférence)
Filière
Système d’Information
Diplôme
Magister
Titre
Vérification des Protocoles Cryptographiques avec la Programmation Par Contraintes
Mots clés
Protocoles cryptographiques; Vérification formelle; Vérification automatique; Planification; SAT.
Résumé
Cette thèse propose des voies pour améliorer la vérification automatique des protocoles cryptographiques. En premier, nous introduisons un état de l’art de l’ensemble des techniques de vérification organisés en deux classe : celles basées sur la recherche de preuve mathématique et celles basées sur la recherche d’attaque. Au niveau preuve mathématique, nous avons adopté l’interprétation abstraite qui a l’avantage de faire la preuve automatique, contrairement aux autres approches qui font appel aux prouveurs semi automatiques. Nous avons prouvé le protocole de Needham-Schroeder à clé privée en s’inspirant à la fois des travaux de Goubault sur l’utilisation de la logique d’ordre un pour les besoins de la vérification des protocoles, et des travaux de Blanchet sur l’interprétation abstraite.
Date de soutenance
2008
Cote
TH2640
Pagination
124F.
Format
30 cm
Notes
RESUME ET MOTS CLES EN FRANCAIS ET EN ANGLAIS.
Statut
Soutenue