The director of the INCIBE-UPV Cybersecurity Chair gave an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the symbolic analysis of cryptographic protocols
València, June 23, 2025 .- The director of the INCIBE-UPV Cybersecurity Chair, the result of an agreement between the National Cybersecurity Institute (INCIBE), an entity under the Ministry for Digital Transformation and Public Function, through the Secretary of State for Telecommunications and Digital Infrastructure, and the Universitat Politècnica de Valencia, Santiago Escobar, participated in the Summer School: Formal Methods for Information Security, held from June 18 to 20 in Tarragona.
The INCIBE-UPV Cybersecurity Chair is included in the Cybersecurity Chairs program in Spain, within the framework of the Recovery, Transformation and Resilience Plan, with funding from the Next Generation-EU Funds.
This Summer School, organized by the strategic project HERMES and the Chair in Cybersecurity INCIBE-Universitat Rovira i Virgili, has counted with the lecture under the title “Analysis with Maude-NPA”.
In this conference, which was also attended by the young researchers of the Chair in Cybersecurity INCIBE-UPV, Arturo Hernández and Adrián Sánchez, Escobar has given an overview of the Maude-NRL Protocol Analyzer (Maude-NPA), a tool for the symbolic analysis of cryptographic protocols.
Maude-NPA is able to find an attack, given sufficient resources, or prove the absence of any attack, when the search space is finite, which happens quite often thanks to many optimization techniques.
During his talk he emphasized how with Maude-NPA several properties can be proven: secrecy, authentication and indistinguishability for an active Dolev-Yao intruder model and an unlimited number of sessions. In addition, Maude-NPA takes into account the algebraic properties of the cryptographic systems involved to provide a more complete representation of both the protocol and the attackers’ capabilities. Maude-NPA has recently been extended to handle properties proved by SMT solvers: such as time and space constraints.
Santiago Escobar is Professor at the Universitat Politècnica de València. He is a leading researcher in program verification, cybersecurity and protocol analysis, with more than 100 publications and extensive participation in international conferences. Escobar is a long-time collaborator with the Maude-NPA cryptographic protocol analyzer, developed with collaborators from the U.S. Navy, Catherine Meadows, and the University of Illinois, José Meseguer. He is also part of the Maude programming language team, used by organizations such as NASA and Microsoft for safety-critical verification.
Cybersecurity Chairs Programme in Spain
INCIBE, within the Global Security Innovation Programme, has the particular mission of raising cybersecurity capabilities and resources in the academic, business and technological ecosystems, aimed at boosting the cybersecurity capabilities of society and the economy in general. The aim of this initiative is to have a programme that seeks to promote and generate knowledge and its transfer to the productive sector, especially by establishing synergies between the social and economic spheres of cybersecurity. With the aim of developing this purpose, the public invitation for collaboration in the promotion of cybersecurity chairs in Spain was launched on 1 December 2022.
The initiatives and actions of the Cybersecurity Chairs programme in Spain are included in the Global Security Innovation Programme, included in the Recovery, Transformation and Resilience Plan (PRTR) through Component 15. Investment 7 Cybersecurity: Strengthening the capacities of citizens, SMEs and professionals and boosting the sector. It acts especially in three of the six key aspects of the industry included in milestone 245 of the PRTR: boosting the national cybersecurity industry for the emergence, growth and development of companies in this sector; developing high value-added solutions and services in the field of cybersecurity; and training and developing specialised talent in the field of cybersecurity.
About INCIBE
The National Institute of Cybersecurity is an entity under the Ministry for Digital Transformation and Public Function, through the Secretary of State for Telecommunications and Digital Infrastructure, consolidated as a reference entity for the development of cybersecurity and digital confidence of citizens and businesses. It is also an engine of social transformation and an opportunity for innovation, promoting R&D&I and talent.
About UPV
The Universitat Politècnica de València (UPV) is, according to the Academic Ranking of World Universities (ARWU), known as the Shanghai ranking, the best technological university in Spain. More than 70% of UPV students are already working a year after completing their studies. And this is largely due to paid internships in companies. The UPV has more than a thousand agreements that allow student exchanges with other universities in Europe, Latin America, the United States, Canada, Australia, China and Japan. In its little more than 50 years of history, it has produced more than 145,000 scientific publications. It is a national leader in the number of patents and one of the Spanish academic institutions that obtains most income from its research activity.
Santiago Escobar participa en el curso de verano: Métodos formales para la seguridad de la información
El director de la Cátedra de Ciberseguridad INCIBE-UPV ha dado una visión general del Analizador de Protocolos Maude-NRL (Maude-NPA), una herramienta para el análisis simbólico de protocolos criptográficos
València, 23 de junio de 2025.- El director de la Cátedra de Ciberseguridad INCIBE-UPV, fruto del convenio entre el Instituto Nacional de Ciberseguridad (INCIBE), entidad dependiente del Ministerio para la Transformación Digital y de la Función Pública, a través de la Secretaría de Estado de Telecomunicaciones e Infraestructuras Digitales, y la Universitat Politècnica de Valencia, Santiago Escobar, ha participado en la Escuela de Verano: Formal Methods for Information Security, celebrada del 18 al 20 de junio en Tarragona.
La Cátedra de Ciberseguridad INCIBE-UPV está incluida en el programa de Cátedras de Ciberseguridad en España, en el marco del Plan de Recuperación, Transformación y Resiliencia, con la financiación de los Fondos Next Generation-EU.
Esta Escuela de Verano, organizada por el proyecto estratégico HERMES y la Cátedra en Ciberseguridad INCIBE-Universitat Rovira i Virgili, ha contado con la ponencia bajo el título “Análisis con Maude-NPA”.
En esta conferencia, a la que también han asistido los jóvenes investigadores de la Cátedra de Ciberseguridad INCIBE-UPV, Arturo Hernández y Adrián Sánchez, Escobar ha dado una visión general del Analizador de Protocolos Maude-NRL (Maude-NPA), una herramienta para el análisis simbólico de protocolos criptográficos.
Maude-NPA es capaz de encontrar un ataque, dados los recursos suficientes, o demostrar la ausencia de cualquier ataque, cuando el espacio de búsqueda es finito, lo que ocurre con bastante frecuencia gracias a muchas técnicas de optimización.
Durante su intervención ha subrayado como con Maude-NPA se pueden comprobar varias propiedades: secreto, autenticación e indistinguibilidad para un modelo de intruso Dolev-Yao activo y un número ilimitado de sesiones. Además, Maude-NPA tiene en cuenta las propiedades algebraicas de los sistemas criptográficos implicados para ofrecer una representación más completa, tanto del protocolo como de las capacidades de los atacantes. Maude-NPA se ha ampliado recientemente para manejar propiedades comprobadas mediante solucionadores SMT: como las restricciones de tiempo y espacio.
Santiago Escobar es Catedrático de la Universitat Politècnica de València. Es un destacado investigador en verificación de programas, ciberseguridad y análisis de protocolos, con más de 100 publicaciones y una amplia participación en conferencias internacionales. Escobar colabora desde hace tiempo con el analizador de protocolos criptográficos Maude-NPA, desarrollado con los colaboradores de la Marina estadounidense, Catherine Meadows, y la Universidad de Illinois, José Meseguer. También forma parte del equipo del lenguaje de programación Maude, utilizado por organizaciones como la NASA y Microsoft para la verificación de seguridad crítica.
Programa de Cátedras de Ciberseguridad en España
INCIBE, dentro del Programa Global de Innovación en Seguridad, tiene como misión particular la elevación de las capacidades y recursos en ciberseguridad, en los ecosistemas académico, empresarial y tecnológico, dirigidos a impulsar las capacidades en ciberseguridad de la sociedad y la economía en general. Esta iniciativa tiene el propósito de disponer de un programa que persiga la promoción y generación del conocimiento y la transferencia del mismo al sector productivo, especialmente estableciendo sinergias entre los ámbitos sociales y económicos de la ciberseguridad. Con el objetivo de desarrollar este propósito se lanzó el pasado 1 de diciembre de 2022 la invitación pública para la colaboración en la promoción de cátedras de ciberseguridad en España.
Las iniciativas y actuaciones del programa de Cátedras de Ciberseguridad en España se engloban dentro delPrograma Global de Innovación en Seguridad, contemplado en el Plan de Recuperación, Transformación y Resiliencia (PRTR) a través del Componente 15. Inversión 7 Ciberseguridad: Fortalecimiento de las capacidades de ciudadanos, PYMES y profesionales e impulso del sector. Actúa especialmente en tres de los seis aspectos claves de la industria recogidos en el hito 245 del PRTR: impulsar la industria nacional de la ciberseguridad para el surgimiento, crecimiento y desarrollo de empresas en este sector; desarrollar soluciones y servicios de alto valor añadido en el ámbito de la ciberseguridad; y formar y desarrollar talentos especializados en el ámbito de la ciberseguridad.
Sobre INCIBE
El Instituto Nacional de Ciberseguridad es una entidad dependiente del Ministerio para la Transformación Digital y de la Función Pública, a través de la Secretaría de Estado de Telecomunicaciones e Infraestructuras Digitales, consolidado como entidad de referencia para el desarrollo de la ciberseguridad y de la confianza digital de los ciudadanos y las empresas. Además, es un motor de transformación social y oportunidad para la innovación, fomentando la I+D+i y el talento.
Sobre UPV
La Universitat Politècnica de València (UPV) es, según el Academic Ranking of World Universities (ARWU), conocido como ranking de Shanghai, la mejor universidad tecnológica de España. Más del 70% del alumnado de la UPV ya trabaja al año de haber finalizado sus estudios. Y ello se debe en buena medida a las prácticas en empresa que son remuneradas. La UPV mantiene más de mil convenios que permiten el intercambio de estudiantes con otras universidades europeas, de América Latina, Estados Unidos, Canadá, Australia, China y Japón. En sus poco más de 50 años de historia, ha producido más de 145.000 publicaciones científicas. Es líder nacional en número de patentes y una de las instituciones académicas españolas que más ingresos obtiene gracias a su actividad investigadora.