A Formal Specification of the {DNSSEC} Model

The Domain Name System Security Extensions ({DNSSEC)} is a suite of specifications that provide origin authentication and integrity assurance services for {DNS} data. In particular, {DNSSEC} was designed to protect resolvers from forged {DNS} data, such as the one generated by {DNS} cache poisoning. This article presents a minimalistic specification of a {DNSSEC} model which provides the grounds needed to formally state and verify security properties concerning the chain of trust of the {DNSSEC} tree. The model, which has been formalized and verified using the Coq proof assistant, specifies an abstract formulation of the behavior of the protocol and the corresponding security-related events, where security goals, such as the prevention of cache poisoning attacks, can be given a formal treatment.