Abstract FR:

Le but d'un protocole cryptographique est de fonctionner correctement malgre la presence d'agents malveillants. Mais, meme lorsque les participants echangent des messages chiffres avec des fonctions cryptographiques bien concues, la securite du protocole n'est pas garantie. Il faut donc etudier la securite des protocoles cryptographiques independamment des fonctions cryptographiques utilisees. Les proprietes de securite, telles que le secret de l'information transmise ou l'authenticite de l'identite des agents communiquants, peuvent s'enoncer en termes de connaissances. Or la logique epistemique a ete proposee pour etudier formellement des notions comme la connaissance, la croyance et l'ignorance. Pour prouver la securite des protocoles cryptographiques, deux nouvelles logiques epistemiques ont ete definies. La logique de la communication en milieu hostile est une extension de la logique des connaissances qui permet de decrire etats de connaissances et d'ignorance des differents agents d'un protocole durant une execution. Cette logique a rendu possible l'etude de l'authenticite et le secret de l'information transmise pour plusieurs protocoles cryotographiques. La seconde logique est une adaptation de la logique autoepistemique. Elle facilite les preuves de secret car il est possible de decrire implicitement l'etat d'ignorance d'un agent. Finalement, pour permettre la realisation de systemes de preuves automatique de securite, differents systemes de deduction automatique pour les logiques epistemiques ont ete etudies