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
-
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},
url = {https://eprint.iacr.org/2015/074}
}