Paper 2024/1226

A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols

Guillaume Girol, Université Paris-Saclay, CEA LIST
Lucca Hirschi, Inria Nancy - Grand-Est research centre
Ralf Sasse, ETH Zurich
Dennis Jackson, University of Oxford
Cas Cremers, CISPA Helmholtz Center for Information Security
David Basin, ETH Zurich
Abstract

The Noise specification describes how to systematically construct a large family of Diffie-Hellman based key exchange protocols, including the secure transports used by WhatsApp, Lightning, and WireGuard. As the specification only makes informal security claims, earlier work has explored which formal security properties may be enjoyed by protocols in the Noise framework, yet many important questions remain open. In this work we provide the most comprehensive, systematic analysis of the Noise framework to date. We start from first principles and, using an automated analysis tool, compute the strongest threat model under which a protocol is secure, thus enabling formal comparison between protocols. Our results allow us to objectively and automatically associate each informal security level presented in the Noise specification with a formal security claim. We also provide a fine-grained separation of Noise protocols that were previously described as offering similar security properties, revealing a subclass for which alternative Noise protocols exist that offer strictly better security guarantees. Our analysis also uncovers missing assumptions in the Noise specification and some surprising consequences, e.g. in some situations higher security levels yield strictly worse security.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. USENIX 2020
Keywords
NoiseTamarin ProverDiffie-HellmanX3DHSymbolic analysis
Contact author(s)
lucca hirschi @ inria fr
ralf sasse @ inf ethz ch
research @ dennis-jackson uk
cremers @ cispa de
basin @ inf ethz ch
History
2024-08-02: approved
2024-07-31: received
See all versions
Short URL
https://ia.cr/2024/1226
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2024/1226,
      author = {Guillaume Girol and Lucca Hirschi and Ralf Sasse and Dennis Jackson and Cas Cremers and David Basin},
      title = {A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols},
      howpublished = {Cryptology {ePrint} Archive, Paper 2024/1226},
      year = {2024},
      url = {https://eprint.iacr.org/2024/1226}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.