Mémoires de Fin d’Etudes
Etablissement
Université d’Oran1 - Ahmed Ben Bella
Affiliation
Département d’Informatique
Auteur
KEMMAR, Amina
Directeur de thèse
LEBBAH Yahia (Professeur)
Co-directeur
KADDOUR Mejdi (Maitre de conférence)
Filière
Informatique
Diplôme
Magister
Titre
Programmation par Contraintes pour la vérification des protocoles cryptographiques munis d’opérateurs algébriques
Mots clés
Cryptographie; Protocoles cryptographiques; Véri_cation formelle;Courbes elliptiques; Programmation par contraintes; Plani_cation.
Résumé
Dans ce projet de magistère, nous proposons des approches pour améliorer la vérification formelle des protocoles cryptographiques avec la programmation par contraintes. En particulier, nous avons contribué dans la vérification du protocole de Schnorr basé sur les courbes elliptiques et le protocole de porte-monnaie électronique (approche asymétrique). Ces deux protocoles font appel à une primitive algébrique qui est l’exponentielle modulaire. Cet opérateur n’est pas encore pris en charge par les outils de vérification actuels. Nous essayons au long de ce mémoire de trouver des solutions pour traiter ce type d’opérateur. Le protocole de Schnorr basé sur les courbes elliptiques repose sur la difficulté de résolution du logarithme discret, pour lequel, jusqu’à ce jour, il n’y a pas d’algorithmes en temps polynomial pour le résoudre. La première approche que nous avons préconisée consiste à représenter le protocole avec un système d’équations non linéaires en nombre entier exprimé dans le langage AMPL; cette approche AMPL a rapidement montré ses limitations en raison de l’indisponibilité d’un certain nombre d’opérateurs incontournables dans la modélisation du protocole. Après, nous avons proposé un modèle de ce dernier sous forme d’un ensemble de contraintes sous Gecode, où nous avons réussi à modéliser tout le protocole, ouvrant la perspective de sa vérification. Nous avons réussi à le casser pour des longueurs de clé inférieures à 24 bits.
Date de soutenance
2010
Cote
TH3205
Pagination
119F.
Format
30 cm
Notes
RESUME ET MOTS CLES EN FRANCAIS ET EN ANGLAIS.ANNEXES 101-111F.BIBLIOG.112-119F.
Statut
Soutenue