Contributions à la vérification automatique de protocoles de groupes

Les protocoles cryptographiques sont cruciaux pour securiser les transactions electroniques. La confiance en ces protocoles peut etre augmentee par l'analyse formelle de leurs proprietes de securite. Bien que beaucoup de travaux aient ete dedies pour les protocoles classiques comme le protocole de Needham-Schroeder, tres peu de travaux s'adressent a la classe des protocoles de groupe dont les caracteristiques principales sont : les proprietes de securite specifiques qu'ils doivent satisfaire, et le nombre arbitraire des participants qu'ils impliquent. Cette these comprend deux contributions principales. La premiere traite la premiere caracteristique des protocoles de groupe. Pour cela, nous avons defini un modele appele modele de services que nous avons utilise pour proposer une strategie de recherche d'attaques se basant sur la resolution de contraintes. L'approche proposee a permis de retrouver d'anciennes attaques et d'en decouvrir de nouvelles sur quelques protocoles de groupe. Certaines attaques ont aussi pu etre generalisees pour couvrir le cas de n participants. La deuxieme contribution principale de cette these consiste a definir un modele synchrone qui generalise les modeles standards de protocoles en permettant les listes non bornees a l'interieur des messages. Ceci est assure par l'introduction d'un nouvel operateur appele mpair qui represente une liste construite sur un meme patron. Dans ce modele etendu, nous avons propose une procedure de decision pour une classe particuliere des protocoles de groupe appelee classe de protocoles bien-tagues avec clefs autonomes, en presence d'un intrus actif et avec des clefs composees.