Implémentations de protocoles cryptographiques prouvées dans le modèle calculatoire

The goal of this work is to obtain implementations of security protocols proved in the computational model. We implemented a compiler that takes as input a specification of a protocol in the input language of the protocol verifier CryptoVerif and compiles it into an implementation in OCaml. We proved the secrecy of exchanged keys and authentication of the server in the SSH (Secure SHell) key exchange protocol, and used our compiler on this protocol. We proved that this compiler is correct: if an adversary can break a security property on the generated code with a probability p, then there exists an adversary that can break this property on the specification with the same probability p. Hence, if a specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.Le but de ce travail est d'obtenir des implémentations de protocolescryptographiques prouvées dans le modèle calculatoire. Nous avonsimplémenté un compilateur qui prend une spécification d'un protocoledans le langage d'entrée du vérificateur de protocoles CryptoVerif etcompile celle-ci en une implémentation en OCaml. Nous avons prouvé lesecret des clés échangées et l'authentification du serveur de l'échangede clés du protocole SSH (Secure SHell), puis nous avons utilisé notrecompilateur sur celui-ci.Nous avons prouvé que ce compilateur est correct : si un adversaire estcapable de casser une propriété de sécurité dans le code généré avecprobabilité p, alors il existe un adversaire capable de casser cettepropriété sur la spécification avec la même probabilité p. Si unespécification est prouvée sûre dans le modèle calculatoire parCryptoVerif, alors l'implémentation générée est aussi sûre