Vérification formelle de protocoles basés sur de courtes chaines authentifiées

Modern security protocols may involve humans in order to compare or copy short strings betweendifferent devices. Multi-factor authentication protocols, such as Google 2-factor or 3D-Secure are typical examplesof such protocols. However, such short strings may be subject to brute force attacks. In this thesis we propose asymbolic model which includes attacker capabilities for both guessing short strings, and producing collisions whenshort strings result from an application of weak hash functions. We propose a new decision procedure for analyzing(a bounded number of sessions of) protocols that rely on short strings. The procedure has been integrated in theAKISS tool and tested protocols from the ISO/IEC 9798-6:2010 standardLes protocoles de sécurité modernes peuvent impliquer un participant humain de façon à ce qu'il compare ou copie de courtes chaines de caractères faisant le pont entre différents appareils. C'est par exemple le cas des protocoles basés sur une authentification à facteur multiples comme les protocoles Google 2 factor ou 3D-Secure.Cependant, de telles chaines de caractères peuvent être sujettes à des attaques par force brute. Dans cette thèse nous proposons un modèle symbolique qui inclut les capacités de l'attaquant à deviner des secrets faibles et à produire des collisions avec des fonctions de hachage dont de l'application résulte une courte chaine de caractères. Nous proposons une nouvelle procédure de décision pour analyser un protocole (restreint à un nombre borné de sessions) qui se base sur de courtes chaines de caractères. Cette procédure a été intégré dans l'outil AKISS et testé sur les protocoles du standard ISO/IEC 9798-6:201