On the Automated Correction of Faulty Security Protocols

Hdl Handle:
http://hdl.handle.net/11285/572492
Title:
On the Automated Correction of Faulty Security Protocols
Authors:
López Pimentel, Juan C.
Issue Date:
01/04/2008
Abstract:
Un Protocolo de Seguridad se usa para establecer una comunicacio ?n segura entre dos o más agentes a pesar de condiciones adversas. Cr ??menes tales como la usurpacio ?n de identidades o accesos no autorizados a la informacio ?n han provocado incontables pérdidas econo ?micas especialmente cuando se realizan transacciones electro ?nicas. Por ese motivo, la comunidad de los métodos for- males ha puesto un interés especial en la verificacio ?n de protocolos de seguridad, produciendose en los u ?ltimos an ?os una gran cantidad de técnicas y herramientas. Otros autores han tomado un enfoque diferente, proponiendo principios de disen ?o para ayudar al desarrollo de mejores protocolos. Esta iniciativa se origina porque ellos han observado que los ataques de protocolos de seguridad son un resultado de malas prácticas de disen ?o. Algunos de los más importantes principos de disen ?o han sido publicados por Abadi y Needham. A pesar de ésto, el disen ?o de protocolos de seguridad es particularmente dif ??cil y propenso a errores. En esta tesis presentamos SHRIMP (a Smart metHod for Repairing IMperfect security Pro- tocols). SHRIMP tiene como objetivo acelerar el ciclo de desarrollo de protocolos de seguri- dad, uniendo la brecha que hay entre disen ?o y análisis por medio de una tarea de diagno ?stico y reparacio ?n. SHRIMP trabaja con herramientas de verificacio ?n existentes para el proceso de bu ?squeda de ataques en el protocolo (en particular hemos usado AVISPA ya que es considerado el estado del arte). SHRIMP primero analiza un protocolo y, si el protocolo tiene fallas, busca una o más corridas del protocolo que violan un requirimiento de seguridad, llamado ataque. As ??, SHRIMP analiza el protocolo y el ataque para indicar qué pasos fallan en el protocolo y de esta forma sintetizar cambios apropiados para corregirlos. SHRIMP produce una versio ?n mejorada del protocolo, el cuál es analizado y parchado nuevamente hasta que no sean detectados más errores. Para organizar la aplicacio ?n de diagno ?stico y reparacio ?n, hemos adoptado la metodolog ??a proof planning de Bundy. As ??, SHRIMP es un conjunto de métodos de parche, cada uno de ellos es capaz de parchar una clase general de fallas. Para arreglar una falla, en cada método de parche hemos traducido algunos de los principios de Abadi y Needham en requirimientos formales, la cual llamamos precondiciones. Estas precondiciones son una coleccio ?n de reglas que identifican la clase de ataque que el protocolo sufre y a partir de las cuales se propone un parche. En esta tesis nos hemos enfocado en parchar protocolos vulnerables a los ataques de tipo replay. SHRIMP toma cuidado de este tipo de ataques cuando el mensaje siendo re-enviado es un texto cifrado. Si éste es el caso, SHRIMP incluye tres principles métodos de parche para enfrentar este tipo de ataques: message encoding, agent naming y session binding. Hasta ahora hemos probado SHRIMP en 36 protocolos, 21 de ellos fueron obtenidos de la librer ??a Clark-Jacob, obteniendo una tasa de reparacio ?n del 90%.
Keywords:
Correciones; Potocolos; Seguridad
Degree Program:
Programa de Graduados en Informática y Computación
Advisors:
Dr. RaÚl Monroy Borja
Committee Member / Sinodal:
Dr. Dieter Hutter; Dr. Guillermo Morales Lune; Dr. Luis Angel Trejo Rodríguez; Dr. Alberto Oliart Ros
Degree Level:
Doctor en Ciencias Computacionales
School:
Escuela de Graduados en Informática y Computación
Campus Program:
Campus Monterrey
Discipline:
Ingeniería y Ciencias Aplicadas / Engineering & Applied Sciences
Appears in Collections:
Ciencias Exactas

Full metadata record

DC FieldValue Language
dc.contributor.advisorDr. RaÚl Monroy Borjaes
dc.contributor.authorLópez Pimentel, Juan C.es
dc.date.accessioned2015-08-17T11:33:37Zen
dc.date.available2015-08-17T11:33:37Zen
dc.date.issued01/04/2008-
dc.identifier.urihttp://hdl.handle.net/11285/572492en
dc.description.abstractUn Protocolo de Seguridad se usa para establecer una comunicacio ?n segura entre dos o más agentes a pesar de condiciones adversas. Cr ??menes tales como la usurpacio ?n de identidades o accesos no autorizados a la informacio ?n han provocado incontables pérdidas econo ?micas especialmente cuando se realizan transacciones electro ?nicas. Por ese motivo, la comunidad de los métodos for- males ha puesto un interés especial en la verificacio ?n de protocolos de seguridad, produciendose en los u ?ltimos an ?os una gran cantidad de técnicas y herramientas. Otros autores han tomado un enfoque diferente, proponiendo principios de disen ?o para ayudar al desarrollo de mejores protocolos. Esta iniciativa se origina porque ellos han observado que los ataques de protocolos de seguridad son un resultado de malas prácticas de disen ?o. Algunos de los más importantes principos de disen ?o han sido publicados por Abadi y Needham. A pesar de ésto, el disen ?o de protocolos de seguridad es particularmente dif ??cil y propenso a errores. En esta tesis presentamos SHRIMP (a Smart metHod for Repairing IMperfect security Pro- tocols). SHRIMP tiene como objetivo acelerar el ciclo de desarrollo de protocolos de seguri- dad, uniendo la brecha que hay entre disen ?o y análisis por medio de una tarea de diagno ?stico y reparacio ?n. SHRIMP trabaja con herramientas de verificacio ?n existentes para el proceso de bu ?squeda de ataques en el protocolo (en particular hemos usado AVISPA ya que es considerado el estado del arte). SHRIMP primero analiza un protocolo y, si el protocolo tiene fallas, busca una o más corridas del protocolo que violan un requirimiento de seguridad, llamado ataque. As ??, SHRIMP analiza el protocolo y el ataque para indicar qué pasos fallan en el protocolo y de esta forma sintetizar cambios apropiados para corregirlos. SHRIMP produce una versio ?n mejorada del protocolo, el cuál es analizado y parchado nuevamente hasta que no sean detectados más errores. Para organizar la aplicacio ?n de diagno ?stico y reparacio ?n, hemos adoptado la metodolog ??a proof planning de Bundy. As ??, SHRIMP es un conjunto de métodos de parche, cada uno de ellos es capaz de parchar una clase general de fallas. Para arreglar una falla, en cada método de parche hemos traducido algunos de los principios de Abadi y Needham en requirimientos formales, la cual llamamos precondiciones. Estas precondiciones son una coleccio ?n de reglas que identifican la clase de ataque que el protocolo sufre y a partir de las cuales se propone un parche. En esta tesis nos hemos enfocado en parchar protocolos vulnerables a los ataques de tipo replay. SHRIMP toma cuidado de este tipo de ataques cuando el mensaje siendo re-enviado es un texto cifrado. Si éste es el caso, SHRIMP incluye tres principles métodos de parche para enfrentar este tipo de ataques: message encoding, agent naming y session binding. Hasta ahora hemos probado SHRIMP en 36 protocolos, 21 de ellos fueron obtenidos de la librer ??a Clark-Jacob, obteniendo una tasa de reparacio ?n del 90%.es
dc.language.isoenen
dc.rightsOpen Accessen
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.titleOn the Automated Correction of Faulty Security Protocolsen
dc.typeTesis de Doctoradoes
thesis.degree.grantorInstituto Tecnológico y de Estudios Superiores de Monterreyes
thesis.degree.levelDoctor en Ciencias Computacionaleses
dc.contributor.committeememberDr. Dieter Hutteres
dc.contributor.committeememberDr. Guillermo Morales Lunees
dc.contributor.committeememberDr. Luis Angel Trejo Rodríguezes
dc.contributor.committeememberDr. Alberto Oliart Roses
thesis.degree.disciplineEscuela de Graduados en Informática y Computaciónes
thesis.degree.namePrograma de Graduados en Informática y Computaciónes
dc.subject.keywordCorrecioneses
dc.subject.keywordPotocoloses
dc.subject.keywordSeguridades
thesis.degree.programCampus Monterreyes
dc.subject.disciplineIngeniería y Ciencias Aplicadas / Engineering & Applied Scienceses
All Items in REPOSITORIO DEL TECNOLOGICO DE MONTERREY are protected by copyright, with all rights reserved, unless otherwise indicated.