Mejoras en la interacción con la herramienta Maude-NPA

Abstract

[EN] The security in modern online services is increasingly more and more vulnerable to intruder attacks. Companies like Yubiko works on devices like Yubikey, a USB device that provides strong identification. In this thesis, we have specified and analyzed the cryptographic protocol underneath the Yubikey device using the Maude-NPA tool, a state-of-the-art cryptographic protocol analyzer. During this thesis, we learned how the Yubikey protocol works, we learn how to use the Tamarin proper, another protocol analyzer, and how to specify and analysis this protocol using the Maude-NPA features.

El desarrollo de este proyecto final de carrera tiene como objetivo mejorar los mecanismos de interacción con la herramienta Maude-NPA, ya sea mejorando la interfaz gráfica o el formato de entrada o los comandos asociados. Maude-NPA es una herramienta que permite el análisis de protocolos criptográficos y que ha sido realizada por el profesor Santiago Escobar de la Universidad Politécnica de Valencia en colaboración con el profesor José Meseguer (Universidad de Illinois en Urbana-Champaign, EE.UU.) y la profesora Catherine Meadows (Marina de los Estados Unidos, Washington, D.C, EE.UU.). Existen multitud de nuevas características aún pendientes de ser integradas en la interfaz de entrada de la herramienta, como nuevas propiedades algebraicas de los protocolos (como homomorfismos o ó-exclusivo), el manejo de composición de protocolos de comunicaciones o un lenguaje más rico de especificación de propiedades.