RT Journal Article
T1 Parallel Maude-NPA for Cryptographic Protocol Analysis
A1 Canh Minh Do, 
A1 Riesco Rodríguez, Adrián
A1 Santiago Escobar, 
A1 Kazuhiro Ogata, 
AB 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.
PB IEEE
YR 2025
FD 2025-07-10
LK https://hdl.handle.net/20.500.14352/122624
UL https://hdl.handle.net/20.500.14352/122624
LA eng
DS Docta Complutense
RD 20 jul 2025