Preuves de protocoles cryptographiques : méthodes symboliques et attaquants puissants

The use of communication protocols has become pervasive at all levels of our society. Yet, their uses come with risks, either about the security of the system or the privacy of the user. To mitigate those risks, we must provide the protocols with strong security guarantees: we need formal, extensive, modular and machine-checked proofs. However, such proofs are very difficult to obtain in practice. In this Thesis, we strive to ease this process in the case of cryptographic protocols and powerful attackers. The four main contributions of this Thesis, all based on symbolic methods, are 1) a methodology for extensive analyses via a case study of multi-factor authentication; 2) composition results to allow modular proofs of complex protocols in the computational model; 3) symbolic methods for deciding basic proof steps in computational proofs, formulated as problems on probabilistic programs; 4) a prototype of a mechanized prover in the Computationally Complete Symbolic Attacker model.L'utilisation des protocoles de communication est omniprésente dans notre société, mais leur utilisation comporte des risques de sécurité ou d'atteinte à la vie privée. Pour réduire ces risques, il faut exiger de solides garanties, i.e. des preuves formelles, approfondies, modulaires et vérifiées par ordinateur. Toutefois, de telles preuves sont très difficiles à obtenir. Nous essayons dans cette thèse de faciliter ce processus dans le cas des protocoles cryptographiques et d'attaquants puissants. Nos contributions principales sont 1) une méthodologie d'analyse approfondies dans le cas de l'authentification multi-facteurs; 2) des résultats de composition permettant des preuves modulaires de protocoles complexes dans le modèle calculatoire; 3) l'automatisation d'étapes élémentaires de preuves calculatoires via des méthodes symboliques appliquées à des programmes probabilistes; 4) un prototype d'assistant de preuve dans le modèle de l'attaquant symbolique calculatoirement complet