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={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},}