Date : 2006
Type : Livre / Book
Type : Thèse / ThesisLangue / Language : anglais / English
Méthodes formelles (informatique)
Résumé / Abstract : Les protocoles cryptographiques sont utilisés pour assurer des communications securisiées sur des canaux non securisés. Deux approches sont utilisées pour vérifier ces protocoles. L'approche symbolique suppose que la cryptographie est parfaite et a permis le développement d'outils automatiques pour la vérification des protocoles. L'approche computationnelle, au contraire, s'intéresse à la probabilité de "casser" les primitives cryptographiques.Les travaux présentés dans cette thèse permettent de relier le modèle symbolique au modèle computationnel, cela pour des protocoles utilisant les chiffrements asymétrique et symétrique ainsi que la signature numérique. De plus, nous étudions trois extensions possibles de ce résultat : l'ajout d'échanges de clés à la Diffie-Hellman (utilisant une exponentiation modulaire), le cas où l'adversaire est confronté à un nombre non borné de challenges et l'utilisation de propriétés plus complexes par le biais de l'opacité.
Résumé / Abstract : Cryptographie protocols are used to ensure secure communications over insecure channels. Two approaches are used to verify protocols : the symbolic approach, more abstract, but for which many automatic tools exist and the computational approach, more realistic but harder to use. This document links the symbolic and computational views for protocols using asymmetric and symmetric cryptography as weil as digital signature. We also propose three extensions: adding DiffieHellman to handle key exchange protocols using modular exponentiation, considering adversary with access to an unbounded number of challenges and the case of more complex properties defined using opacity.