Implementación de una interfaz gráfica para Maude-NPA

Abstract

[ES] Maude-NPA es una herramienta de verificación de protocolos criptográficos desarrollada por la University of Illinois at Urbana- Champaign (EE.UU.), el Navy Research Laboratory en Washington D.C. (EE.UU.) y la Universitat Politècnica de València. Maude-NPA es un poderoso analizador, es flexible ya que puedes crear tu propia notación y permite una larga variedad de propiedades criptográficas como homomorfismo o or-exclusivo. Sin embargo, la interfaz existente para modelar protocolos y luego verificar propiedades de seguridad de éstos es compleja y difícil de entender, por lo que hace a la herramienta Maude-NPA poca atractiva. Andrew Russel Cholewa, estudiante de máster en la University of Illinois at Urbana-Champaign propuso un nuevo lenguaje de modelado de protocolos y de verificación de sus propiedades de seguridad, denominado Maude-NPA Protocol Specification Language (Maude- PSL). Maude-PSL utiliza la notación Alice y Bob estándar para definir protocolos de forma directa: la interpretación de cada uno de los mensajes enviados o recibidos por cada participante (rol) utilizando tanto la información asumida al comienzo de la ejecución del protocolo como la información de los participantes al final de la ejecución. En este proyecto de fin der grado durante una estancia en la University of Illinois at Urbana-Champaign de cinco meses, me he centrado en modelar y verificar la mayor cantidad de protocolos criptográficos descritos en Maude-PSL, incluyendo protocolos con homomorfismo, y conseguir que tengan el mismo resultado que con Maude-NPA original y, en el caso de no ser así, modificar los protocolos.