基于串空间的Athena分析技术研究

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

Athena Approach Based on Strand Spaces

Strand space model is an important research field in security protocol analysis scopes. Song extends strand space model, borrows some efficient techniques from both model checking and theorem proving, proposes an efficient automatic checking approach, Athena, for analyzing security protocols, and develops a tool named APV based on this approach. This paper discusses Athena systematically, introduces Athena's assumption, its syntax and semantics, and discusses merit and limitation of this logical. We detailedly describe the core verification algorithm of Athena, analysis what actually makes Athena successful in fast and automatic verification of security protocol. We also point out the defects of this algorithm, discuss the reason and give the way to solve it. Finally, the future direction in this field is discussed.