DDYF: Differential Dolev-Yao Fuzzing of Cryptographic Protocols

본문 미리보기

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