论文部分内容阅读
研究分析了Athena自动协议形式化分析算法的原理。该算法能够分析协议的各种安全属性，它基于扩展了的串空间模型，利用了消息间的因果关系，并且结合了定理证明和模型检测方法，能有效地分析安全协议的各种安全属性。在此基础上，完整地分析了ISO/IEC DIS 11770-3中提出的Helsinki协议的认证属性，分析得出该协议是有安全缺陷的。