安全协议的SPIN建模与分析

• 来源期刊: 南京航空航天大学学报
• 学科: 工学
• 关键词: 安全协议 Helsinki协议 Promela语言 建模
• 年，卷（期）: 2009,（5）
• 页码范围: 672-676
• 页数: 5页
• 分类号: TP393.08
• 字数: 4860字
• 语种: 中文

摘要

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