Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909957756026880 |
|---|---|
| author | Zhang, Qifan Shen, Zilin Karim, Imtiaz Bertino, Elisa Li, Zhou |
| author_facet | Zhang, Qifan Shen, Zilin Karim, Imtiaz Bertino, Elisa Li, Zhou |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_11431 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution Zhang, Qifan Shen, Zilin Karim, Imtiaz Bertino, Elisa Li, Zhou Cryptography and Security Formal Languages and Automata Theory Networking and Internet Architecture 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. |
| title | Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution |
| topic | Cryptography and Security Formal Languages and Automata Theory Networking and Internet Architecture |
| url | https://arxiv.org/abs/2512.11431 |