针对协议组合问题的Athena方法扩展

针对安全协议形式化分析领域的五个公开问题之一的协议的组合性问题,选用并扩展了Athena分析方法,以求对组合协议进行自动分析。通过扩展了串、丛的概念以及逻辑和状态表示法,以描述多个协议的运行。考虑到从协议对主协议的影响,引入了串空间中理想的概念,给出了其自动生成算法,并扩展了后继状态函数。最后运用扩展后的Athena方法对Neuman Stubblebine协议进行了分析,发现协议部分对协议部分存在有攻击,相应给出了攻击路径。