these

TH¨SEprØsentØe à l’ cole Normale SupØrieure de Cachanpour obtenir le grade deDOCTEUR DE L’ COLE NORMALE SUP RIEURE DE CACHANpar : Muriel RogerSpØcialitØ : InformatiqueRa nemen ts de la rØsolution et vØri cationde protocoles cryptographiquesSoutenue le 24 octobre 2003Composition du Jury : Guy Cousineau rapporteur Didier Galmiche rapp Jean Goubault-Larrecq directeur de thŁse Francis Klay examinateur Yassine Lakhnech prØsident du jury Denis Lugiez Michaºl Rusinowitch examinateur2Table des matiŁresIntroduction 7I tat de l’art 111 Techniques de dØmonstration automatique 131.1 Quelques dØ nitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131.2 La rØsolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141.3 La rØsolution ordonnØe avec sØlection : un ra nemen t de la rØsolution . . . . . . . 161.4 StratØgies d’Ølimination de clauses . . . . . . . . . . . . . . . . . . . . . . . . . . . 171.4.1 limination de tautologies . . . . . . . . . . . . . . . . . . . . . . . . . . . . 171.4.2 de clauses subsumØes . . . . . . . . . . . . . . . . . . . . . . . . 171.4.3 limination des pures . . . . . . . . . . . . . . . . . . . . . . . . . . 181.5 Splitting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181.5.1 Splitting et tableaux . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181.5.2 sans splitting . . . . . . . . . . . . . . . . . . . . . ...