论文部分内容阅读
密码协议安全性的分析是网络安全研究领域的一个主要内容,研究人员提出多种形式化方法来分析这个问题。模型检测工具Spin是一个广泛验证并发系统性质的工具,可用来分析密码协议。对Needham-Schroeder(NS)协议认证部分进行了详细的分析,结果表明,Spin可成功检测出NS协议的缺陷,并生成攻击的序列。