Introduction Assumptions On Shoup's lemma The proof To do Conclusion
25
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
25
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
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 April 2010 Bruno Blanchet (CNRS, ENS, INRIA) EKE in CryptoVerif April 2010 1 / 20
Voir
- eke using
- precisely evaluated
- computational diffie-hellman
- password- based key
- trivial protocol
- sku ?
´ CNRS, Ecole Normale Superieure, INRIA, Paris ´
Bruno Blanchet blanchet@di.ens.fr Joint work with David Pointcheval
April 2010
Automatic, computational proof of EKE using CryptoVerif (Work in progress)
Motivation
EKE (Encrypted Key Exchange): A password-based key exchange protocol. A non-trivial protocol. It took some time before getting a 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.
VotpyrCnirpAfireINS,ENS,EiEKA)RI
