Automation of Timed Processes in Maude-NPA using Maude

Abstract

[ES] El desarrollo de este trabajo fin de grado tiene como objetivo automatizar el modelado de un protocolo con tiempo real en Maude-NPA. Se define una sintaxis nueva para procesos con tiempo junto con transformaciones implementadas en el lenguaje de alto rendimiento Maude. El resultado final es un fichero de sintaxis análoga a la usada por la herramienta Maude-NPA. Entre todas las herramientas para analizar protocolos criptográficos hemos elegido Maude-NPA, creado por el profesor Santiago Escobar (Universitat Politècnica de València, España), la profesora Catherine Meadows (Marina de los Estados Unidos, Washington, DC, EE. UU.) y el profesor José Meseguer (Universidad de Illinois en Urbana Champaign, EE.UU). Para desarrollar nuestra herramienta, hemos utilizado el lenguaje de programación y modelado de alto rendimiento. Maude, desarrollado por José Meseguer (Universidad de Illinois en Urbana Champaign, EE. UU.), Carolyn Talcott y Steven Eker (SRI International, Palo Alto, CA, EE. UU.), Narciso Martí-Oliet y Rubén Rubio (Universidad Complutense de Madrid), Francisco Durán (Universidad de Málaga) y Santiago Escobar (Universitat Politècnica de València).

[EN] The main objective of this final degree project is to automate the modelling of a real time protocol in Maude-NPA. A new syntax is defined for timed processes along with transformations implemented in the high performance language, Maude. The final result is a syntax file analogous to the one used by the Maude-NPA tool. Among all the tools to analyse cryptographic protocols we have chosen Maude-NPA, created by Santiago Escobar (Polytechnic University of Valencia, Spain), Catherine Meadows (United States Navy, Washington, DC, USA) and José Meseguer (University of Illinois at Urbana Champaign, USA). To develop our tool, we have used the high performance programming and modelling language. Maude, developed by José Meseguer (University of Illinois at Urbana Champaign, USA), Carolyn Talcott and Steven Eker (SRI International, Palo Alto, CA, USA), Narciso Martí-Oliet and Rubén Rubio (Universidad Complutense de Madrid), Francisco Durán (Universidad de Málaga) and Santiago Escobar (Universitat Politècnica de València).

[CA] El desenvolupament d'aquest treball fi de grau té com a objectiu automatitzar el modelatge d'un protocol amb temps real en Maude-NPA. Es defineix una sintaxi nova per a processos amb temps juntament amb transformacions implementades en el llenguatge d'alt rendiment Maude. El resultat final és un fitxer de sintaxi anàloga a la usada per l'eina Maude-NPA. Entre totes les eines per a analitzar protocols criptogràfics hem triat Maude-NPA, creat pel professor Santiago Escobar (Universitat Politècnica de València, Espanya), la professora Catherine Meadows (Marina dels Estats Units, Washington, DC, els EUA) i el professor José Meseguer (Universitat d'Illinois en Urbana Champaign, els EUA). Per a desenvolupar la nostra eina, hem utilitzat el llenguatge de programació i modelatge d'alt rendiment, Maude, desenvolupat per José Meseguer (Universitat d'Illinois en Urbana Champaign, els EUA), Carolyn Talcott i Steven Eker (SRI International, Palo Alto, CA, USA), Narcís Martí-Oliet i Ruben Rubio (Universidad Complutense de Madrid), Francisco Durán (Universidad de Málaga) i Santiago Escobar (Universitat Politècnica de València).