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

Abstract

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+.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published by the IACR in EUROCRYPT 2015
Keywords
Provable SecuritySecurity ProtocolsEasyCryptKey ExchangeInteractive Theorem Proving
Contact author(s)
benedikt schmidt @ imdea org
History
2015-02-10: received
Short URL
https://ia.cr/2015/074
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2015/074,
      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{https://eprint.iacr.org/2015/074}},
      url = {https://eprint.iacr.org/2015/074}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.