Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas

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ón falsa dentro del sistema pueda llevar a problemas inesperados y potencialmente peligrosos. Para prove...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Bazán, Ezequiel
Otros Autores: Luna, Carlos D.
Formato: bachelorThesis tesis de grado publishedVersion
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2013
Materias:
DNS
DNSSEC
COQ
Métodos Formales
Acceso en línea:http://hdl.handle.net/2133/2663
http://hdl.handle.net/2133/2663
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario
id I15-R121-2133-2663
record_format dspace
institution Universidad Nacional de Rosario
institution_str I-15
repository_str R-121
collection Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR)
language Español
orig_language_str_mv spa
topic DNS
DNSSEC
COQ
Métodos Formales
spellingShingle DNS
DNSSEC
COQ
Métodos Formales
Bazán, Ezequiel
Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
topic_facet DNS
DNSSEC
COQ
Métodos Formales
description 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ón 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én la posibilidad de que se produzca algún tipo de contaminación de caché por suplantación de datos. La formalización en el CCI permitió realizar un análisis riguroso de la especificación propuesta. Se logró demostrar que la semántica 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én 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é de un servidor discrepen de los datos verdaderamente publicados.
author2 Luna, Carlos D.
author_facet Luna, Carlos D.
Bazán, Ezequiel
format bachelorThesis
tesis de grado
publishedVersion
author Bazán, Ezequiel
author_sort Bazán, Ezequiel
title Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
title_short Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
title_full Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
title_fullStr Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
title_full_unstemmed Especificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
title_sort especificación formal del modelo dnssec en el cálculo de construcciones inductivas
publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
publishDate 2013
url http://hdl.handle.net/2133/2663
http://hdl.handle.net/2133/2663
work_keys_str_mv AT bazanezequiel especificacionformaldelmodelodnssecenelcalculodeconstruccionesinductivas
bdutipo_str Repositorios
_version_ 1764820413635887106

Ejemplares similares