Lien entre modèles symboliques et computationnels pour les protocoles cryptographiques utilisant des hachages

Les protocoles cryptographiques sont utilisés pour assurer des communications sécurisées sur des canaux non sécurisés. Deux approches sont utilisées pour vérifier ces protocoles. L'approche symbolique suppose que la cryptographie est parfaite. Ainsi, il est impossible de déchiffrer un message sans la clef adéquate. Ce modèle a permis le développement d'outils automatiques pour la vérification des protocoles cryptographiques. L'approche computationnelle, au contraire, s'intéresse à la probabilité de "casser" les primitives cryptographiques. Ce modèle est mal adapté aux me thodes automatiques de part la difficulté des raisonnements sur les probabilités. Récemment, plusieurs travaux ont été entrepris pour relier ces deux approches et ainsi profiter de leurs avantages respectifs: automatisation dans le modèle symbolique et plus grand réalisme du modèle computationnel. Les travaux présentés dans cette thèse permettent de relier le modèle symbolique au modèle computationnel, dans le cas de protocoles utilisant des chiffrements asymétrique et symétrique, des signatures et des hachages. Nous montrons que tout ce qui peut se passer dans le modèle computationnel, avec une probabilité non négligeable, peut également se passer dans le modèle symbolique. Ainsi, les résultats des outils de vérification automatiques dans le modèle symboliques sont également valides dans le modèle computationnel.GRENOBLE1-BU Sciences (384212103) / SudocSudocFranceF