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

摘要：

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

关键词：串空间、Athena、安全协议、定理证明、模型检验

所属期刊栏目：33

分类号：TP3(计算技术、计算机技术)

资助基金：广西自然科学基金0542052

在线出版日期：2006-09-20（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：9-13