//img.uscri.be/pth/e9ac2457b46a666f73eef03d57b350183f7fa483
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Introduction Assumptions On Shoup's lemma The proof To do Conclusion

De
25 pages
Introduction Assumptions On Shoup's lemma The proof To do Conclusion Automatic, computational proof of EKE using CryptoVerif (Work in progress) Bruno Blanchet Joint work with David Pointcheval CNRS, Ecole Normale Superieure, INRIA, Paris May 2010 Bruno Blanchet (CNRS, ENS, INRIA) EKE in CryptoVerif May 2010 1 / 20

  • eke using

  • precisely evaluated

  • computational diffie-hellman

  • password- based key

  • trivial protocol

  • sku ?


Voir plus Voir moins
IntroductionAssmutpoisnnOhSuopemslThmaroepToofoCodulcnnoislBonurBS,ENS,NR(CetchanreVoaMfi102y2/10RIINEKA)nCEiptry0
´ CNRS, Ecole Normale Superieure, INRIA, Paris ´
Bruno Blanchet blanchet@di.ens.fr Joint work with David Pointcheval
May 2010
Automatic, computational proof of EKE using CryptoVerif (Work in progress)
tcudortnmussAnoiIhTpemeamoTodorfonsOnptiopslShounocnoCisulchan(CetruBBlno02/2y2010
Motivation
EKE (Encrypted Key Exchange): A password-based key exchange protocol. A non-trivial protocol. It took some time before getting a proper computational proof of this protocol. Our goal: Mechanize, and automate as far as possible, its proof using the automatic computational protocol verifierCryptoVerif. This is an opportunity forseveral interesting extensionsof CryptoVerif. This work is still in progress.
tpyrCniEaMfireVoS,ENS,NREKA)RIIN