LogoLogo

Kourjieh, Mounira. Analyse logique et vérification des protocoles cryptographiques

Kourjieh, Mounira (2009) Analyse logique et vérification des protocoles cryptographiques.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1221Kb

Résumé en francais

Cette thèse est développée dans le cadre de l'analyse symbolique des protocoles cryptographiques. Les contributions de cette thèse peuvent être divisées en trois parties principales : 1- Nous analysons les trois classes des protocoles cryptographiques qui utilisent respectivement des fonctions de hachage vulnérables à la collision, des schémas de signature vulnérables à la substitution des clés, et des primitives cryptographiques représentées par des théories équationnelles convergentes ayant la propriété de variante finie. a- Nous conjecturons que le problème de vérification de la première classe des protocoles peut être réduit au problème de vérification de la classe des protocoles cryptographiques qui utilisent un symbole associatif de la concaténation, et nous montrons la décidabilité du problème de vérification de la dernière classe. b- Nous montrons la décidabilité du problème de vérification des deux dernières classes des protocoles. 2- Nous montrons la décidabilité du problème de déduction clos pour un nouveau fragment de la logique du premier ordre, et nous montrons l'application de ce résultat sur le problème de vérification des protocoles cryptographiques. 3- Nous analysons les protocoles de vote électronique, et nous donnons une définition formelle pour la propriété de vérifiabilité de vote. Nous montrons également que certains protocoles de vote électronique satisfont cette propriété.

Sous la direction du :
Directeur de thèse
Balbiani, Philippe
Chevalier, Yannick
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Protocoles cryptographiques - Protocoles de vote électronique - Procédures de décision - Primitives algébriques - Systèmes de constraintes - Clauses de premier ordre - Résolution - Saturation - Pi calcul appliqué
Sujets :Informatique
Déposé le :05 Jul 2010 17:24