Con el crecimiento de aplicaciones desarrolladas en base al uso de nombres de dominio, la autenticidad en los datos dentro de DNS (Domain Name System) se ha tornado crítica, haciendo que informaci on falsa dentro del sistema pueda llevar a problemas inesperados y potencialmente peligrosos. Para proveer extensiones de seguridad al protocolo DNS, la IETF (Internet Engineer Task Force) desarroll o DNSSEC (DNS SECurity Extensions). El presente trabajo provee una especificación formal de DNSSEC, utilizando el Cálculo de Construcciones Inductivas (CCI) y COQ como asistente de pruebas. El enfoque propuesto aborda principalmente el análisis de integridad de la cadena de confianza que se genera a lo largo del árbol DNSSEC, así como tambi en la posibilidad de que se produzca algún tipo de contaminaci on de caché por suplantación de datos. La formalización en el CCI permiti o realizar un análisis riguroso de la especificación propuesta. Se logró demostrar que la semantica de los comandos que se ejecutan dentro del sistema conservan invariante la validez del estado, lo cual garantiza que el sistema no puede transicionar a un estado que no represente un posible estado DNSSEC. Sin embargo, tambi en pudo detectarse una inconsistencia en los datos dentro de la cadena de confianza al ejecutarse el rollover de una llave de zona, ya que puede suceder el caso en que los datos almacenados en el cach e de un servidor discrepen de los datos verdaderamente publicados.