Diseño, modelado y verificación de un protocolo nuevo de autenticación usando Maude

Abstract

[ES] El objetivo de este trabajo fin de máster consiste en diseñar un nuevo protocolo de autenticación en colaboración con una empresa de la comunidad valenciana y realizar el modelado y verificación de propiedades de fiabilidad y seguridad usando el lenguaje de programación y modelado Maude. El modelo, además, integra partes desarrolladas en Python, por lo que requiere cierta interacción entre los dos lenguajes, Maude y Python. Se sigue una metodología ágil con la empresa donde se diseñan distintas iteraciones del protocolo, del modelo en Maude y se verifican propiedades de forma incremental involucrando a la empresa desde el principio del proceso.

[EN] The objective of this master's final project consists of designing a new authentication protocol, in collaboration with a company in Comunitat Valenciana and make the modelling and verification of reliability and security properties using the Maude programming language, The model, in addition, integrates Python-developed blocks, so it is required some interaction between both languages, Maude and Python. An agile methodology is followed with the company, where different protocol iterations are designed, from the Maude model, and some properties are verified incrementally involving the company members since the beginning of the process.