Verificación automática del protocolo TLS 1.3 usando Maude-NPA

Abstract

[ES] La importancia de la confidencialidad y seguridad en las tecnologías de la información es un tema en el que poco a poco más entidades tanto públicas como privadas aúnan esfuerzos con el fin de conseguir entornos más seguros y robustos frente a los atacantes. El protocolo TLS tiene un papel fundamental en el establecimiento de conexiones seguras sobre medios no seguros como es Internet. Es ampliamente utilizado hoy en día en todos los navegadores y en informática en general por lo que la razón de este trabajo se fundamenta en el estudio de las propiedades de seguridad de este protocolo criptográfico mediante el uso de Maude-NPA, herramienta de verificación de protocolos criptográficos de comunicación utilizada para dicho análisis. A lo largo de este trabajo se profundizará en la herramienta Maude-NPA, el protocolo TLS, el estado del arte en el análisis de este protocolo con herramienta similares como Tamarin y una comparativa de resultados obtenidos con Maude-NPA frente a los ya extraídos con Tamarin.