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

• URL: http://arxiv.org/abs/2512.11431v1
• Date: Fri, 12 Dec 2025 10:12:06 GMT
• Title: Proving DNSSEC Correctness: A Formal Approach to Secure Domain Name Resolution
• Authors: Qifan Zhang, Zilin Shen, Imtiaz Karim, Elisa Bertino, Zhou Li,
• Abstract summary: This paper introduces DNSSECVerif, the first framework for comprehensive, automated formal security analysis of the DNSSEC protocol suite.<n>We formally prove four of DNSSEC's core security guarantees and uncover critical ambiguities in the standards.<n>Our work provides crucial, evidence-based recommendations for hardening DNSSEC specifications and implementations.
• Score: 12.033681333491685
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• ReliabilityRAG: Effective and Provably Robust Defense for RAG-based Web-Search [69.60882125603133]
  We present ReliabilityRAG, a framework for adversarial robustness that explicitly leverages reliability information of retrieved documents.<n>Our work is a significant step towards more effective, provably robust defenses against retrieved corpus corruption in RAG.
  arXiv  Detail & Related papers  (2025-09-27T22:36:42Z)
• A Survey and Evaluation Framework for Secure DNS Resolution [0.749377967268953]
  We survey DNS resolution process attacks and threats and develop a comprehensive threat model and attack taxonomy for their systematic categorization.<n>This analysis results in the formulation of 14 desirable security, privacy, and availability properties to mitigate the identified threats.<n>Our evaluation reveals that no single scheme provides ideal protection across the entire resolution path.
  arXiv  Detail & Related papers  (2025-09-17T08:07:20Z)
• Overcoming DNSSEC Islands of Security: A TLS and IP-Based Certificate Solution [0.03262230127283452]
  We propose a decentralized approach to addressing gaps in DNSSEC's chain of trust.<n>We leverage TLS and IP-based certificates to enable end-to-end authentication between hierarchical levels.
  arXiv  Detail & Related papers  (2025-09-10T08:02:07Z)
• Collusion Resistant DNS With Private Information Retrieval [42.34183823376613]
  We propose PDNS, a DNS extension leveraging single-server Private Information Retrieval to strengthen privacy guarantees.<n>PDNS achieves acceptable performance (2x faster than DoH over Tor with similar privacy guarantees) and strong privacy guarantees today.
  arXiv  Detail & Related papers  (2025-07-28T13:17:25Z)
• Implementing and Evaluating Post-Quantum DNSSEC in CoreDNS [0.4374837991804085]
  This paper presents the integration of post-quantum cryptographic (PQC) algorithms into CoreDNS.<n>We have developed a plugin that extends CoreDNS with support for five PQC signature algorithm families.<n>Our implementation maintains compatibility with existing DNS resolution flows while providing on-the-fly signing using quantum-resistant signatures.
  arXiv  Detail & Related papers  (2025-07-12T14:34:17Z)
• Quantum-Resistant Domain Name System: A Comprehensive System-Level Study [0.9365037811026767]
  We present a comprehensive system-level study of post-quantum DNS security across three widely deployed mechanisms.<n>We propose Post-Quantum Cryptographic (PQC)-DNS, a unified framework for benchmarking DNS security under legacy, post-quantum, and hybrid cryptographic configurations.
  arXiv  Detail & Related papers  (2025-06-24T18:35:24Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  We introduce a benchmark to assess the ability of Large Language Models to autonomously identify vulnerabilities in new cryptographic protocols. We created a dataset of novel, flawed, communication protocols and designed a method to automatically verify the vulnerabilities found by the AI agents.
  arXiv  Detail & Related papers  (2024-11-20T14:16:55Z)
• ss2DNS: A Secure DNS Scheme in Stage 2 [1.8379423176822356]
  We introduce ss2DNS, a novel DNS scheme designed to mitigate the security and privacy vulnerabilities in the resolution process between resolvers and authoritative nameservers.<n>We show that for server-side processing latency, resolution time, and CPU usage, ss2DNS is comparable to less-secure schemes but significantly outperforms DNS-over-TLS.
  arXiv  Detail & Related papers  (2024-08-02T01:25:14Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  The Controller Area Network (CAN) bus leaves in-vehicle communications inherently non-secure. This paper reviews and compares the 15 most prominent authentication protocols for the CAN bus. We evaluate protocols based on essential operational criteria that contribute to ease of implementation.
  arXiv  Detail & Related papers  (2024-01-19T14:52:04Z)
• Securing Graph Neural Networks in MLaaS: A Comprehensive Realization of Query-based Integrity Verification [68.86863899919358]
  We introduce a groundbreaking approach to protect GNN models in Machine Learning from model-centric attacks. Our approach includes a comprehensive verification schema for GNN's integrity, taking into account both transductive and inductive GNNs. We propose a query-based verification technique, fortified with innovative node fingerprint generation algorithms.
  arXiv  Detail & Related papers  (2023-12-13T03:17:05Z)
• An Efficient and Multi-private Key Secure Aggregation for Federated Learning [41.29971745967693]
  We propose an efficient and multi-private key secure aggregation scheme for federated learning. Specifically, we skillfully modify the variant ElGamal encryption technique to achieve homomorphic addition operation. For the high dimensional deep model parameter, we introduce a super-increasing sequence to compress multi-dimensional data into 1-D.
  arXiv  Detail & Related papers  (2023-06-15T09:05:36Z)
• Scalable Quantitative Verification For Deep Neural Networks [44.570783946111334]
  We propose a test-driven verification framework for deep neural networks (DNNs) Our technique performs enough tests until soundness of a formal probabilistic property can be proven. Our work paves the way for verifying properties of distributions captured by real-world deep neural networks, with provable guarantees.
  arXiv  Detail & Related papers  (2020-02-17T09:53:50Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.