Les preuves de protocoles cryptographiques revisitées

With the rise of the Internet the use of cryptographic protocols became ubiquitous. Considering the criticality and complexity of these protocols, there is an important need of formal verification.In order to obtain formal proofs of cryptographic protocols, two main attacker models have been developed: the symbolic model and the computational model. The symbolic model defines the attacker capabilities as a fixed set of rules. On the other hand, the computational model describes only the attacker’s limitations by stating that it may break some hard problems. While the former is quite abstract and convenient for automating proofs the later offers much stronger guarantees.There is a gap between the guarantees offered by these two models due to the fact the symbolic model defines what the adversary may do while the computational model describes what it may not do. Since Abadi and Rogaway in 2000 a lot of results aimed at bridging this gap, in order to have symbolic proofs yielding computational guarantees. They however all come at the cost of very strong and often unrealistic hypotheses, due to the fact that attacker capabilities are defined in a fundamentally different way in the two models.In order to overcome this problem, in 2012 Bana and Comon devised a new symbolic model in which the attacker’s limitations are axiomatised. Proving security in this new model amounts to checking – for every trace of the protocol – the unsatisfiability of a set of formulae corresponding to the trace, together with the negation of the security property and some axioms representing the attacker’s limitations. In addition, provided that the (computational semantics) of the axioms follows from the cryptographic hypotheses, proving security in this symbolic model yields security in the computational model.The possibility of automating proofs in this model (and finding axioms general enough to prove a large class of protocols) was left open in the original paper from Bana and Comon. In this thesis we provide with an efficient decision procedure for a general class of axioms. In addition we propose a tool (SCARY) implementing this decision procedure. Experimental results of our tool shows that the axioms we designed for modelling security of encryption are general enough to prove a large class of protocols.Avec la généralisation d’Internet, l’usage des protocoles cryptographiques est devenu omniprésent. Étant donné leur complexité et leur aspect critique, une vérification formelle des protocoles cryptographiques est nécessaire.Deux principaux modèles existent pour prouver les protocoles. Le modèle symbolique définit les capacités de l’attaquant comme un ensemble fixe de règles, tandis que le modèle calculatoire interdit seulement à l’attaquant de résoudre certains problèmes difficiles. Le modèle symbolique est très abstrait et permet généralement d’automatiser les preuves, tandis que le modèle calculatoire fournit des garanties plus fortes.Le fossé entre les garanties offertes par ces deux modèles est dû au fait que le modèle symbolique décrit les capacités de l’adversaire alors que le modèle calculatoire décrit ses limitations. Depuis l’article précurseur d’Abadi et Rogaway en 2000, de nombreux travaux ont tenté de combler ce fossé. Ils supposent tous des hypothèses très fortes et souvent irréalistes sur l’implémentation des protocoles. La nécessité de ces hypothèses s’explique par le fait que les modèles d’attaquant sont fondamentalement différents dans le monde calculatoire et dans le monde symbolique. En effet, dans le modèle calculatoire les capacités de l’attaquant sont un plus grand point fixe alors qu’elles sont un plus petit point fixe dans le monde symbolique. Ainsi tout résultat voulant obtenir des garanties calculatoires à partir de preuves de sécurité symbolique doit s’assurer que ces deux points fixes coïncident.Pour pallier ce problème, en 2012 Bana et Comon ont proposé un nouveau modèle symbolique dans lequel les limitations de l’attaquant (au lieu de ses capacités) sont axiomatisées. En pratique, prouver la sécurité d’un protocole dans ce modèle revient à montrer – pour chaque trace du protocole – que les axiomes limitant l’attaquant ainsi que les formules correspondant à la trace sont inconsistants avec la négation de la propriété de sécurité. Les auteurs montrent que si la sémantique calculatoire des axiomes découle des hypothèses cryptographiques, la sécurité dans ce modèle symbolique fournit des garanties calculatoires.La principale question laissée ouverte par l’article de Bana et Comon est la possibilité d’automatiser les preuves dans ce nouveau modèle (et l’élaboration d’axiomes suffisamment généraux pour prouver un grand nombre de protocoles). Le principal problème à résoudre pour automatiser les preuves dans ce nouveau modèle est la résolution de problèmes de satisfiabilité d’ensembles de formules du premier ordre. Dans cette thèse nous identifions un sous-ensemble de la logique du premier ordre englobant les ensembles de formules et axiomes considérés dansce modèle, et proposons une procédure de décision originale en temps polynomial pour cette classe.Dans un deuxième temps, nous proposons une implémentation de cette procédure de décision dans notre outil (SCARY). Nos résultats expérimentaux nous ont dans un premier temps amené à élargir les axiomes modélisant la sécurité du chiffrement. Nous pensons que les concepts utilisés pour étendre ces axiomes pourront être réutilisés dans l’élaboration d’axiomes pour d’autres primitives. Dans un deuxième temps nous avons montré que nos nouveaux axiomes sont suffisamment généraux pour prouver une large classe de protocoles. Nous avons également retrouvé des attaques connues sur divers protocoles qui ne sont pas détectées par les outils symboliques usuels. Nous avons, enfin, trouvé une attaque originale sur le protocole Andrews Secure RPC