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

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 ?