Avec le développement des réseaux de communications comme Internet, le besoin d'assurer la sécurité des échanges a considérablement augmenté. Les communications " sécurisées " sont réalisées par l'utilisation de petits programmes appelés protocoles cryptographiques qui peuvent être attaqués même en présence d'un chiffrement parfait. De telles failles, qualifiées de " failles logiques ", sont souvent subtiles et difficiles à déceler à la simple vue du texte du protocole. Dans cette thèse, nous poussons les limites de l'analyse des protocoles au delà de cette hypothèse. En particulier, nous proposons des procédures de décision, pour le problème de la recherche d'attaques en présence d'opérateurs satisfaisant des propriétés algébriques.

La conception d'un protocole cryptographique obéit à de nombreux impératifs : algorithmes à utiliser, propriétés à garantir, moyen d'identification, etc. Il apparaît donc régulièrement de nouveaux protocoles qu'il convient de vérifier. Malgré l'apparente simplicité, concevoir un protocole cryptographique est une tâche difficile et sujette à de nombreuses erreurs. Des failles pour certains protocoles ont été découvertes des années après leur conception. La plupart des travaux existants se basent uniformément sur l'intrus de Dolev Yao et ne se généralisent pas automatiquement à un intrus disposant de capacités supplémentaires ou différentes. Dans cette thèse, nous allons présenter un système de déduction prenant le pouvoir de l'intrus comme paramètre. De plus, les règles de protocole seront vues comme une capacité additionnelle pour l'intrus. Le résultat principal est un théorème de normalisation de preuve permettant de réduire l'espace de recherche des attaques.