Paper 2015/074

Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols

Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, and Benedikt Schmidt


Using EasyCrypt, we formalize a new modular security proof for one-round authenticated key exchange protocols in the random oracle model. Our proof improves earlier work by Kudla and Paterson (ASIACRYPT 2005) in three significant ways: we consider a stronger adversary model, we provide support tailored to protocols that utilize the Naxos trick, and we support proofs under the Computational DH assumption not relying on Gap oracles. Furthermore, our modular proof can be used to obtain concrete security proofs for protocols with or without adversarial key registration. We use this support to investigate, still using EasyCrypt, the connection between proofs without Gap assumptions and adversarial key registration. For the case of honestly generated keys, we obtain the first proofs of the Naxos and Nets protocols under the Computational DH assumption. For the case of adversarial key registration, we obtain machine-checked and modular variants of the well-known proofs for Naxos, Nets, and Naxos+.

Available format(s)
Cryptographic protocols
Publication info
Published by the IACR in EUROCRYPT 2015
Provable SecuritySecurity ProtocolsEasyCryptKey ExchangeInteractive Theorem Proving
Contact author(s)
benedikt schmidt @ imdea org
2015-02-10: received
Short URL
Creative Commons Attribution


      author = {Gilles Barthe and Juan Manuel Crespo and Yassine Lakhnech and Benedikt Schmidt},
      title = {Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols},
      howpublished = {Cryptology ePrint Archive, Paper 2015/074},
      year = {2015},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.