Paper 2026/991

DDYF: Differential Dolev-Yao Fuzzing of Cryptographic Protocols

Abstract

Symbolic formal verification of cryptographic protocols based on the Dolev-Yao (DY) attacker model—an active attacker with full network control and perfect cryptography—is well-established for finding design-level logical flaws in cryptographic protocols. Building on this, Dolev-Yao Fuzzing (DYF) enriches fuzzing with this attacker model to uncover logical bugs at the implementation level. In contrast to bit-level fuzzers (e.g., AFL), DYF leverages a formal model of messages and cryptography to generate structured, adversarial executions, such as replaying and re-signing a modified payload. However, a significant limitation of DYF is the requirement to precisely model properties to check at runtime (e.g., session parameter agreement). Defining these properties is labor-intensive and inherently non-exhaustive, often necessitating complex instrumentation of the Programs Under Test. Consequently, typically only a subset of logical attacks is detected. We address this limitation by introducing Differential Dolev-Yao Fuzzing (DDYF) based on a differential oracle to compare executions across different protocol implementations. By interpreting discrepancies through the DY model, it identifies semantic differences indicative of bugs or vulnerabilities, effectively minimizing false positives. We propose a generic design for DDYF, implement it within the PUFFIN DY fuzzer, and evaluate it on four major TLS implementations and two SSH implementations. Our results demonstrate that DDYF can detect vulnerabilities that evade state-of-the-art fuzzers, specifically those requiring DY attacker capabilities (missed by bit-level differential fuzzers) or complex objective oracles (missed by DYF). DDYF also uncovered numerous new RFC violations in OpenSSL, BoringSSL, wolfSSL, LibreSSL, libssh, and wolfSSH, which are by-design hardly detectable with non-differential oracles.