Par-Maude-NPA

2025

1. IEEE TDSC

   Parallel Maude-NPA for Cryptographic Protocol Analysis

   Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata

   IEEE Transactions on Dependable and Secure Computing, Jul 2025

   Abstract DOI Bib

   Maude-NPA is a formal verification tool for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic primitives. It starts from an attack state to find counterexamples or conclude that the attack concerned cannot be conducted by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with complex protocols whose state space is huge. This paper describes a parallel version of Maude-NPA in which the backward narrowing and the transition subsumption at each layer in Maude-NPA are conducted in parallel. A tool supporting the parallel version has been implemented in Maude with a master-worker model using meta-interpreters. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 52% on average for complex case studies in which the number of states located at each layer is considerably large.

   @article{CanhTDSC25,
     author = {Do, Canh Minh and Riesco, Adrián and Escobar, Santiago and Ogata, Kazuhiro},
     journal = {IEEE Transactions on Dependable and Secure Computing},
     title = {Parallel Maude-NPA for Cryptographic Protocol Analysis},
     publisher = {IEEE},
     year = {2025},
     volume = {},
     number = {},
     pages = {1-18},
   }

2022

1. WRLA

   Parallel Maude-NPA for Cryptographic Protocol Analysis

   Canh Minh Do, Adrián Riesco, Santiago Escobar, and Kazuhiro Ogata

   In The 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022, Jul 2022

   Abstract DOI Bib

   Maude-NPA is a symbolic model checker for analyzing cryptographic protocols in the Dolev-Yao strand space model modulo an equational theory defining the cryptographic operations, which starts from an attack state to find counterexamples by performing a backward narrowing reachability analysis. Although Maude-NPA is a powerful analyzer, its running performance can be improved by taking advantage of parallel and/or distributed computing when dealing with non-trivial protocols in which the state space is huge. This paper describes a parallel version of Maude-NPA and a tool that supports it. We report on some experiments of various kinds of protocols that demonstrate that the tool can increase the running performance of Maude-NPA by 30% on average for most non-trivial case studies in which the number of states located at each layer is considerably large.

   @inproceedings{CanhWrla22,
     author = {Minh Do, Canh and Riesco, Adri{\'a}n and Escobar, Santiago and Ogata, Kazuhiro},
     editor = {Bae, Kyungmin},
     title = {Parallel Maude-NPA for Cryptographic Protocol Analysis},
     booktitle = {The 14th International Workshop on Rewriting Logic and its Applications, WRLA 2022},
     year = {2022},
     publisher = {Springer International Publishing},
     address = {Cham},
     pages = {253--273},
     isbn = {978-3-031-12441-9},
   }