Motivated by limitations in DNSSEC, ss2DNS has been recently proposed as an alternative scheme that augments recursive resolver and nameserver interactions with stronger real-time security and privacy properties. In this paper, using a symbolic model of ss2DNS in the Tamarin protocol verifier, and the assumption that none of the relevant cryptographic keys are compromised, we formally verify the security and privacy properties of the DNS resolution process with the root zone when using ss2DNS. The validity of these proofs is then extended to the other subordinate zones. We also explore the impact of key and entity compromises on ss2DNS security and privacy properties.