Researchers from Japan successfully parallelized both the backward narrowing and transition subsumption steps in the powerful analyzer Maude-NPA for cryptographic protocol analysis
Internet security is a major concern, but cryptographic protocol analysis tools often require a long time due to their computational complexity. Professor Kazuhiro Ogata and Assistant Professor Canh Minh Do of the Department of Computing Science at Japan Advanced Institute of Science and Technology (JAIST) successfully parallelized two key steps—backward narrowing and transition subsumption—in Maude-NPA, resulting in what they call Par-Maude-NPA. Par-Maude-NPA improves the runtime performance of Maude-NPA by about 52% on average for complex cases, significantly reducing analysis time and enhancing the ability to analyze large and complex cryptographic protocols efficiently. This research is the result of an international collaboration with Professor Santiago Escobar of Polytechnic University of Valencia and Associate Professor Adrián Riesco of Complutense University of Madrid in Spain. It was published in the leading academic journal in the field of dependable and secure computing, IEEE Transactions on Dependable and Secure Computing, on July 16, 2025.
We are in an era where the Internet has become an indispensable part of daily life—from online shopping to banking, making internet security a critical concern. Ensuring the safety of internet communications requires verification of design flaws and security vulnerabilities in cryptographic protocols, such as Transport Layer Security (TLS), which protects personal information like credit card numbers from unauthorized access during online transactions. To support the formal verification of these protocols, various tools and techniques have been developed. In addition to Maude-NPA, several other formal analyzers have been introduced, including ProVerif, Tamarin, and Scyther. However, until recently, there had been no successful parallelization of formal analyzers for cryptographic protocols.
Maude-NPA begins from an attack state and uses backward narrowing reachability analysis to find security flaws in cryptographic protocols. If the initial state can be reached from the attack state, the possible attack is shown. Conversely, if no such path exists, it can be concluded that the attack is infeasible. However, this technique suffers from a rapid increase in the number of states that must be analyzed—a problem known as state explosion. To address this, Maude-NPA introduces transition subsumption, which eliminates unnecessary states that can be subsumed by other previously explored states in the search space. In this research, the research team parallelizes both the backward narrowing and the transition subsumption to make the best use of high-performance computing resources.
“Maude-NPA uses a breadth-first search strategy to traverse the reachable state space. Starting from a set of states at layer l (representing depth l from the attack state, which is at layer 0), it performs one backward narrowing step on each state to generate their successor states at layer l+1. This operation is referred to as step (1),” Dr. Canh Minh Do explains. This backward narrowing search from any given state can be performed independently, which opens an opportunity for parallelization to improve the performance of Maude-NPA.
“In addition, as soon as the successor states at each layer are obtained from step (1), Maude-NPA conducts the transition subsumption to discard unnecessary states that can be subsumed by previously explored states. This process is referred to as step (2).” Dr. Canh Minh Do adds. Although transition subsumption plays a critical role in reducing the state space, it is computationally expensive. Instead of checking the subsumption of each state one by one, many states can be considered simultaneously to improve the runtime performance of Maude-NPA.
The research team successfully parallelized both the backward narrowing in step (1) and the transition subsumption in step (2) and tested across a variety of complex cryptographic protocols. Dr. Canh Minh Do comments on the results,
“We present experimental results across diverse cryptographic protocols demonstrating that Par-Maude-NPA improves the runtime performance of Maude-NPA by an average of 52% for complex case studies with a large number of states at each layer.” The case studies have also shown that Par-Maude-NPA can effectively perform formal analysis of not only conventional cryptographic protocols such as TLS, but also of quantum-resistant TLS, which will enable safe, secure, and sustainable use of the Internet even when large-scale quantum computers become available.
###
Reference
| Title of original paper: |
Parallel Maude-NPA for Cryptographic Protocol Analysis |
| Authors: |
Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata |
| Journal: |
IEEE Transactions on Dependable and Secure Computing |
| DOI: |
10.1109/TDSC.2025.3589584 |
|
About Japan Advanced Institute of Science and Technology, Japan
Founded in 1990 in Ishikawa prefecture, the Japan Advanced Institute of Science and Technology (JAIST) was the first independent national graduate school in Japan. Now, after 30 years of steady progress, JAIST has become one of Japan’s top-ranking universities. JAIST strives to foster capable leaders with a state-of-the-art education system where diversity is key; about 40% of its alumni are international students. The university has a unique style of graduate education based on a carefully designed coursework-oriented curriculum to ensure its students have a solid foundation on which to carry out cutting-edge research. JAIST also works closely with both local and overseas communities by promoting industry–academia collaborative research.
About Assistant Professor Canh Minh Do from Japan Advanced Institute of Science and Technology, Japan
Dr. Canh Minh Do received his M.S. and Ph.D. degrees in Information Science from Japan Advanced Institute of Science and Technology (JAIST) in 2019 and 2022, respectively. He is currently an Assistant Professor at JAIST. His research focuses on formal specification and verification of concurrent and distributed systems for both classical and quantum technologies.
Funding information
This work was partially supported by JST SICORP Grant Number JPMJSC20C2, Japan, by JSPS KAKENHI Grant Numbers JP23K28060, JP23K19959, JP24K20757, JP24KK0185, by ProCode10 (PID2023-149943OB-I00) funded by MICIN, by the grant PID2021-122830OB-C42 funded by MCIN/AEI/10.13039/501100011033 and ERDF A way of making Europe, by the grant CIPROM/2022/6 funded by Generalitat Valenciana, and by INCIBE’s Chair funded by the EU-NextGenerationEU through the Spanish government’s Plan de Recuperación, Transformación y Resiliencia.