Proved Implementations of Cryptographic Protocols in the Computational Model
Implémentations de protocoles cryptographiques prouvées dans le modèle calculatoire
Résumé
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 protocoles
cryptographiques prouvées dans le modèle calculatoire. Nous avons
implémenté un compilateur qui prend une spécification d'un protocole
dans le langage d'entrée du vérificateur de protocoles CryptoVerif et
compile celle-ci en une implémentation en OCaml. Nous avons prouvé le
secret des clés échangées et l'authentification du serveur de l'échange
de clés du protocole SSH (Secure SHell), puis nous avons utilisé notre
compilateur sur celui-ci.
Nous avons prouvé que ce compilateur est correct : si un adversaire est
capable de casser une propriété de sécurité dans le code généré avec
probabilité p, alors il existe un adversaire capable de casser cette
propriété sur la spécification avec la même probabilité p. Si une
spécification est prouvée sûre dans le modèle calculatoire par
CryptoVerif, alors l'implémentation générée est aussi sûre.
Loading...