The intrinsic complexity of DNS poses unique challenges for ensuring its security and reliability. Despite continuous advances in DNS testing, monitoring, and verification, protocol-level defects still give rise to numerous bugs and attacks. In this paper, we establish the first sound and complete decision procedure for the DNS verification problem. Additionally, we establish the upper bound of $\mathsf{2ExpTime}$ on the complexity of this problem, which was previously unknown. We further apply our framework to two of the most prominent attack vectors on DNS, namely amplification attacks and rewrite blackholing.