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

dc.contributor.advisorLuna, Carlos D.
dc.contributor.authorBazán, Ezequiel
dc.date.accessioned2013-09-13T13:43:41Z
dc.date.available2013-09-13T13:43:41Z
dc.date.issued2011-09-29
dc.description.abstractCon 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.es
dc.description.affiliationFil: Bazán, Ezequiel. Tesista del Departamento de Ciencias de la Computación. Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario; Argentina.
dc.description.peerreviewedPeer reviewedes
dc.identifier.urihttp://hdl.handle.net/2133/2663
dc.language.isospaes
dc.publisherFacultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosarioes
dc.relation.publisherversionhttp://www.fceia.unr.edu.ar/lcc/t523/tesina.php?campo1=40es
dc.rightsopenAccesses
dc.subjectDNSes
dc.subjectDNSSECes
dc.subjectCOQes
dc.subjectMétodos Formaleses
dc.titleEspecificación Formal del Modelo DNSSEC en el Cálculo de Construcciones Inductivas
dc.typebachelorThesis
dc.typetesis de grado
dc.typepublishedVersion

Archivos

Bloque original
Mostrando 1 - 1 de 1
Cargando...
Miniatura
Nombre:
bazan.2011.pdf
Tamaño:
1.57 MB
Formato:
Adobe Portable Document Format
Bloque de licencias
Mostrando 1 - 1 de 1
Nombre:
license.txt
Tamaño:
2.95 KB
Formato:
Item-specific license agreed upon to submission
Descripción: