Cryptology ePrint Archive: Report 2015/074

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

Gilles Barthe and Juan Manuel Crespo and 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+.

Category / Keywords: cryptographic protocols / Provable Security; Security Protocols; EasyCrypt; Key Exchange; Interactive Theorem Proving

Original Publication (in the same form): IACR-EUROCRYPT-2015

Date: received 2 Feb 2015

Contact author: benedikt schmidt at imdea org

Available format(s): PDF | BibTeX Citation

Version: 20150210:203443 (All versions of this report)

Short URL: ia.cr/2015/074

Discussion forum: Show discussion | Start new discussion