论文部分内容阅读
总结了利用模型检测工具SPIN对安全协议进行建模的方法。以Helsinki协议和Helsinki改进协议作为分析实例,用Promela语言建模并使用SPIN对模型进行行为模拟和属性校验,发现了Helsinki存在的Horng-Hsu攻击漏洞以及Helsinki改进协议存在的DoS攻击隐患。该方法具有较好的通用性,容易推广到有多个主体参与的安全协议的分析。