Verificación automática de protocolos criptográficos de seguridad

Abstract

[ES] En el presente proyecto se estudiarán, explicarán y aplicarán las nuevas posibilidades que nos proporciona la introducción de mejoras en la herramienta de verificación de protocolos MaudeNPA. Estas mejoras nos permitirán analizar y verificar la seguridad de protocolos de comunicación, utilizando ataques que exploten estas nuevas mejoras. En concreto nos centraremos en la asociatividad, siendo ésta una nueva característica, y en cómo añadiendo esta característica existen protocolos que siendo seguros pierden esta propiedad. Para ello utilizaremos Maude-NPA, una herramienta de verificación de protocolos de comunicación con propiedades criptográficas, desarrollada por el profesor Santiago Escobar (Universitat Politècnica de València), en colaboración con el profesor José Meseguer (University of Illinois at Urbana-Champaign, USA) y la profesora Catherine Meadows (Naval Research Laboratory, USA). Esta herramienta gracias a su capacidad para verificar protocolos complejos de forma automática, nos permitirá analizar cómo se desarrollan estos ataques y en qué puntos se producen las vulnerabilidades, y así también poder comprobar la efectividad de la herramienta en cuestión al ser los ataques conocidos.

[EN] In this project will be studied , explain and apply the new possibilitiesIt provides improvements in protocol verification toolMaude -NPA .These improvements will allow us to analyze and verify security protocols communication , using attacks that exploit these new enhancements . Specifically we focus on associativity , and this is a new feature and how adding thisthere are protocols that feature remain safe lose this property. We will use Maude -NPA , a verification tool protocols communication with cryptographic properties, developed by Professor Santiago Escobar ( Polytechnic University of Valencia ) , in collaboration with Professor José Meseguer( University of Illinois at Urbana- Champaign , USA ) and Professor Catherine Meadows ( Naval Research Laboratory, USA) . This tool thanks to its ability to verify complex protocols so automatic , allow us to analyze how these attacks take place and at what points produce vulnerabilities , and thus also to check the effectiveness of the tool in question to be known attacks .