Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution

TL;DR

This paper presents DNSSECVerif, a formal verification framework that rigorously analyzes DNSSEC's security, uncovers ambiguities and vulnerabilities, and validates findings through real-world testing and large-scale measurements.

Contribution

It introduces DNSSECVerif, the first automated formal analysis tool for DNSSEC, proving core security guarantees and identifying critical protocol ambiguities and weaknesses.

Findings

Proved four core security guarantees of DNSSEC.

Discovered critical ambiguities, including insecure coexistence of NSEC and NSEC3.

Validated vulnerabilities through testing and large-scale resolver measurements.

Abstract

The Domain Name System Security Extensions (DNSSEC) are critical for preventing DNS spoofing, yet its specifications contain ambiguities and vulnerabilities that elude traditional "break-and-fix" approaches. A holistic, foundational security analysis of the protocol has thus remained an open problem. This paper introduces DNSSECVerif, the first framework for comprehensive, automated formal security analysis of the DNSSEC protocol suite. Built on the SAPIC+ symbolic verifier, our high-fidelity model captures protocol-level interactions, including cryptographic operations and stateful caching with fine-grained concurrency control. Using DNSSECVerif, we formally prove four of DNSSEC's core security guarantees and uncover critical ambiguities in the standards--notably, the insecure coexistence of NSEC and NSEC3. Our model also automatically rediscovers three classes of known attacks, demonstrating fundamental weaknesses in the protocol design. To bridge the model-to-reality gap, we validate our findings through targeted testing of mainstream DNS software and a large-scale measurement study of over 2.2 million open resolvers, confirming the real-world impact of these flaws. Our work provides crucial, evidence-based recommendations for hardening DNSSEC specifications and implementations.