论文部分内容阅读
介绍了Gastin.P最小反例的算法思想,然后结合著名的Needham-Schroeder公钥身份认证协议进行了非形式化分析,实例分析的结果表明,算法用于分析网络安全协议的有效性。针对Gastin.P算法中存在对已遍历的状态重复遍历的缺点,结合语法重定序策略提出了一种新的算法框架,有效地解决了这个问题。因此,新的算法框架用于网络安全协议的分析具有高效性。