DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing
Max Ammann, Lucca Hirschi, Steve Kremer
IEEE Symposium on Security and Privacy 2024 · Day 1 · Continental Ballroom 6
Cryptographic protocols are the bedrock of secure digital communication, yet their complex design and implementation often harbor subtle, dangerous vulnerabilities. The talk "DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing" introduces a novel approach to uncover these critical flaws by synergistically combining the rigorous analytical power of **Dolev-Yao (DY) formal models** with the practical effectiveness of **fuzz testing**. Presented by Max Ammann, Lucca Hirschi, and Steve Kremer, this work addresses significant blind spots in existing security testing methodologies, particularly for protocol-level vulnerabilities that don't manifest as typical memory safety issues.
AI review
This is a critical advancement in cryptographic protocol security, successfully bridging the long-standing gap between formal verification and fuzz testing. The DY Fuzzing approach, demonstrated by TLS Puffin, effectively uncovers protocol-level implementation flaws that traditional methods miss, proven by five new vulnerabilities in major TLS libraries. This work defines a new standard for robust protocol security testing.