摘要： 基于串空间模型的研究是当前安全协议领域的一个研究热点。Song对串空间模型进行了扩展，将模型检验和定理证明结合起来，提出了一种取名为Athena的安全协议分析方法，并基于该方法开发了自动证明工具APV，Song的工作被认为是串空间理论发展的一个重要事件。本文对Athena进行了系统的分析，介绍了Athena的假设条件，给出了Athena的语法和语义，分析了该逻辑的优点和局限性，在此基础上，分析了Athena的核心算法，讨论了Athena算法自动高效的原因，以及该算法如何避免状态空间爆炸的技术，指出了该算法
吴光伟 董荣胜. 基于串空间的Athena分析技术研究[J]. 计算机科学, 2006, 33(8): 9-13. https://doi.org/
WU Guang-Wei, DONG Rong-Sheng （Department of Computer, Guilin University of Electronic Technology, Guilin 541004）. [J]. Computer Science, 2006, 33(8): 9-13. https://doi.org/
首页