{"id":94723,"date":"2009-02-07T00:00:00","date_gmt":"2009-02-07T00:00:00","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/formal-methods-for-the-analysis-of-security-protocols\/"},"modified":"2009-02-07T00:00:00","modified_gmt":"2009-02-07T00:00:00","slug":"formal-methods-for-the-analysis-of-security-protocols","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/ciencia-de-los-ordenadores\/formal-methods-for-the-analysis-of-security-protocols\/","title":{"rendered":"Formal methods for the analysis of security protocols"},"content":{"rendered":"<h2>Tesis doctoral de <strong> Mar\u00eda  De Los Llanos Tobarra Abad <\/strong><\/h2>\n<p>Los sistemas inform\u00e1ticos que aparecen en la actualidad se encuentran orientados al desarrollo de entornos colaborativos y distribuidos. Estas tendencias han convertido a las redes, y especialmente a internet, en elementos clave en el proceso del dise\u00f1o de un sistema. La aparici\u00f3n de nuevos tipos de aplicaciones sobre internet que implican el intercambio de datos privados han otorgado suma importacia al estudio de los protocolos de seguridad. Las soluciones tradicionales en este campo no son adecuadas para los nuevos requisitos en seguridad. Actualmente, la criptograf\u00eda debe, ademas de proporcionar confidencialidad, garantizar intergridad, no-repudio, autenticaci\u00f3n, autorizaci\u00f3n, . . . . Adem\u00e1s es necesario el desarrollo de nuevos esquemas criptogr\u00e1ficos que den cobertura a las nuevas necesidades. los protocolos de seguridad son programas distribuidos que se ejecutan bajo un entorno inseguro. Debido a su naturaleza distribuida son complejos de dise\u00f1ar, junco con que el anlisis de su correctitud es una tarea crucial. La mayoria de los m\u00e9todos formales omiten el tiempo para incrementar su rendimiento. Sin embargo, en sistemas de seguridad, como programas distribuidos que son, el tiempo tiene gran influencia en su ejecuci\u00f3n. Los aspectos temporales de un protocolo de seguridad se pueden dividir en dos categorias. Primero, las marcas temporales e informaci\u00f3n temporal (tiempo de vida para los tokens, las sesiones, las claves, . . . ) Que son incluidos en los mensajes. Segundo, el flujo temporal de los protocolos (tiempos de caducidad, retransmisiones,. . . ) Que pueden ser explotados por un intruso para llevar a cabo un ataque. De forma que no solo estamos interesados en modelar elementos temporales pero tambien en representar el flujo temporal en nuestro modelos. Los automatas temporizados extendidos que presentamos en esta tesis doctoral nos ayudan en ambos casos. los modelos basados en la propuesta de dolev-yao consideran un medio de comunicaci\u00f3n hostil en una red cableada. Debido al desarrollo de las redes inalmbricas y la aparici\u00f3n de nuevas tecnolog\u00edas, como los servicios web o las redes inal\u00e1mbricas de sensores, este modelo no es apropiado. Necesitamos representar diferentes medios de comunicaci\u00f3n con diferentes propiedades que pueden afectar a la seguridad del sistema. Otra raz\u00f3n para introducir nuestra extensi\u00f3n para automatas temporizados. La verificaci\u00f3n de protocolos de seguridad es una tarea crucial en la mayoria de los procesos de desarrollo de sistemas de comunicacin. Pero el an\u00e1lisis de los protocolos de seguridad no se puede realizar de forma aislada. Debe integrarse en los procesos de desarrollo de software. Como consequencia, no solo necesitamos un mecanismo para analizar protocolos de seguridad, sino que tambi\u00e9n es necesario una metodologa bien definida para aplicar el mecanismo de an\u00e1lisis. despu\u00e9s de todo esto, en esta tesis doctoral, se presenta como contribuci\u00f3n principal una metodolog\u00eda para el dise\u00f1o y an\u00e1lisis de protocolos de seguridad mediante uppaal asi como un nuevo tipo de automata temporizados de comportamiento extendido. La metodolog\u00eda se encarga de definir un conjunto de pasos bien establecidos para permitir que dise\u00f1adores desarrollen analicen un protocolo de seguridad siguiendo un estilo incremental. Adem\u00e1s, introducimos los automatas de comportamiento extendido como herramienta para facilitar la tarea de modelado del sistema.<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Formal methods for the analysis of security protocols<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Formal methods for the analysis of security protocols <\/li>\n<li><strong>Autor:<\/strong>\u00a0 Mar\u00eda  De Los Llanos Tobarra Abad <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 Castilla-la mancha<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 02\/07\/2009<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li>Fernando Cuartero Gomez<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: valentin Valero ruiz <\/li>\n<li>Francisco Javier Oliver villarroya (vocal)<\/li>\n<li>pedro Merino gomez (vocal)<\/li>\n<li>karim Djemame (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Mar\u00eda De Los Llanos Tobarra Abad Los sistemas inform\u00e1ticos que aparecen en la actualidad se encuentran orientados [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[18451,1890,4149,13880,8967],"tags":[5510,195133,192679,195132,32622,54644],"class_list":["post-94723","post","type-post","status-publish","format-standard","hentry","category-castilla-la-mancha","category-ciencia-de-los-ordenadores","category-diseno-y-componentes-de-sistemas-de-informacion","category-informatica","category-sistemas-en-tiempo-real","tag-fernando-cuartero-gomez","tag-francisco-javier-oliver-villarroya","tag-karim-djemame","tag-maria-de-los-llanos-tobarra-abad","tag-pedro-merino-gomez","tag-valentin-valero-ruiz"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/94723","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=94723"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/94723\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=94723"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=94723"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=94723"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}