Maude-NRL 协议分析器中的状态空间约简
密码学与安全
2011-05-30 v1 计算机科学中的逻辑
摘要
Maude-NRL 协议分析器（Maude-NPA）是一个用于推理密码协议安全性的工具和推理系统，其中密码系统满足不同的等式性质。它既扩展了原始的 NRL 协议分析器，又为其提供了形式化框架，而原始分析器对等式推理的支持较为有限。Maude-NPA 支持多种代数性质，包括许多感兴趣的密码系统，例如一次性密码本和 Diffie-Hellman。与原始 NPA 一样，Maude-NPA 通过从不安全的攻击状态向后搜索来寻找攻击，并假设会话数量无界。由于会话数量无界且支持不同的等式理论，因此必须开发减少搜索空间和避免无限搜索路径的方法。为了使这些技术证明有用，它们不仅需要加速搜索，而且不应破坏完备性，从而使得未能发现攻击仍能保证安全性。在本文中，我们描述了在 Maude-NPA 中实现的一些状态空间约简技术。我们还提供了完备性证明，以及它们对 Maude-NPA 性能影响的实验评估。
引用
@article{arxiv.1105.5282,
title = {State Space Reduction in the Maude-NRL Protocol Analyzer},
author = {Santiago Escobar and Catherine Meadows and Jose Meseguer},
journal= {arXiv preprint arXiv:1105.5282},
year = {2011}
}