Automatically Verified Mechanized Proof of One-Encryption Key Exchange

Abstract : We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a non-trivial protocol, and thus mechanizing its proof provides additional confidence that it is correct. This case study was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. We have indeed extended CryptoVerif to support the computational Diffie-Hellman assumption. We have also added support for proofs that rely on Shoup's lemma and additional game transformations. In particular, it is now possible to insert case distinctions manually and to merge cases that no longer need to be distinguished. Eventually, some improvements have been added on the computation of the probability bounds for attacks, providing better reductions. In particular, we improve over the standard computation of probabilities when Shoup's lemma is used, which allows us to improve the bound given in a previous manual proof of OEKE, and to show that the adversary can test at most one password per session of the protocol. In this paper, we present these extensions, with their application to the proof of OEKE. All steps of the proof, both automatic and manually guided, are verified by CryptoVerif.
Type de document :
Communication dans un congrès
25th IEEE Computer Security Foundations Symposium (CSF'12), 2012, Cambridge, United States. pp.325--339, 2012
Liste complète des métadonnées

Littérature citée [59 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00863386
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:48
Dernière modification le : mercredi 22 novembre 2017 - 01:13:37
Document(s) archivé(s) le : vendredi 20 décembre 2013 - 15:03:33

Fichier

BlanchetCSF12.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00863386, version 1

Collections

Citation

Bruno Blanchet. Automatically Verified Mechanized Proof of One-Encryption Key Exchange. 25th IEEE Computer Security Foundations Symposium (CSF'12), 2012, Cambridge, United States. pp.325--339, 2012. 〈hal-00863386〉

Partager

Métriques

Consultations de la notice

90

Téléchargements de fichiers

72