Paper 2023/057

DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing

Max Ammann, Independent Researcher, Trail of Bits
Lucca Hirschi, Inria Nancy Grand-Est, Université de Lorraine, France, LORIA
Steve Kremer, Inria Nancy Grand-Est, Université de Lorraine, France, LORIA

Critical and widely used cryptographic protocols have repeatedly been found to contain flaws in their design and their implementation. A prominent class of such vulnerabilities is logical attacks, e.g. attacks that exploit flawed protocol logic. Automated formal verification methods, based on the Dolev-Yao (DY) attacker, formally define and excel at finding such flaws, but operate only on abstract specification models. Fully automated verification of existing protocol implementations is today still out of reach. This leaves open whether such implementations are secure. Unfortunately, this blind spot hides numerous attacks, such as recent logical attacks on widely used TLS implementations introduced by implementation bugs. We answer by proposing a novel and effective technique that we call DY model-guided fuzzing, which precludes logical attacks against protocol implementations. The main idea is to consider as possible test cases the set of abstract DY executions of the DY attacker, and use a novel mutation-based fuzzer to explore this set. The DY fuzzer concretizes each abstract execution to test it on the program under test. This approach enables reasoning at a more structural and security-related level of messages represented as formal terms (e.g. decrypt a message and re-encrypt it with a different key) as opposed to random bit-level modifications that are much less likely to produce relevant logical adversarial behaviors. We implement a full-fledged and modular DY protocol fuzzer. We demonstrate its effectiveness by fuzzing three popular TLS implementations, resulting in the discovery of four novel vulnerabilities.

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. Minor revision. IEEE Security & Privacy 2024
security protocolsfuzzingformal methodsTLSsymbolic verification
Contact author(s)
max @ maxammann org
lucca hirschi @ inria fr
steve kremer @ inria fr
2023-12-01: last of 2 revisions
2023-01-18: received
See all versions
Short URL
Creative Commons Attribution


      author = {Max Ammann and Lucca Hirschi and Steve Kremer},
      title = {{DY} Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing},
      howpublished = {Cryptology ePrint Archive, Paper 2023/057},
      year = {2023},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.