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

Available format(s)
Category
Cryptographic protocols
Publication info
Keywords
Provable SecuritySecurity ProtocolsEasyCryptKey ExchangeInteractive Theorem Proving
Contact author(s)
benedikt schmidt @ imdea org
History
Short URL
https://ia.cr/2015/074

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.