论文部分内容阅读
基于串空间模型的研究是当前安全协议领域的一个研究热点。Song对串空间模型进行了扩展，将模型检验和定理证明结合起来，提出了一种取名为Athena的安全协议分析方法，并基于该方法开发了自动证明工具APV，Song的工作被认为是串空间理论发展的一个重要事件。本文对Athena进行了系统的分析，介绍了Athena的假设条件，给出了Athena的语法和语义，分析了该逻辑的优点和局限性，在此基础上，分析了Athena的核心算法，讨论了Athena算法自动高效的原因，以及该算法如何避免状态空间爆炸的技术，指出了该算法