密码协议的SPIN建模和验证

• 作者: 熊焰 胡香冬 蒋凡 邵晨曦
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 模型检测 BAN-Yahalom协议 SPIN
• 年，卷（期）: 2002,（z1）
• 所属期刊栏目: 科研通信
• 页码范围: 2099-2101
• 页数: 3页
• 分类号: TP311.133.1
• 字数: 2618字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2002.z1.044

摘要

为了将模型检测这种强有力的系统验证技术应用于网络协议的安全分析,形式化建模仍然是目前的关键问题和难点所在.本文提出了一种基于高级过程描述语言的建模方法.根据入侵者角色和攻击目标的不同,从入侵者的角度分析协议的运行模式,为每个主体建立过程模型,用模型检测工具进行分析验证.对BAN-Yahalom协议的SPIN分析验证了这种方法的可行性.该方法具有一定的通用性,对其它网络协议的分析有很好的参考价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	蒋凡	中国科学技术大学计算机科学技术系	97	867	16.0	25.0
2	邵晨曦	中国科学技术大学计算机科学技术系	40	445	12.0	19.0
3	熊焰	中国科学技术大学计算机科学技术系	82	648	12.0	21.0
4	胡香冬	中国科学技术大学计算机科学技术系	3	42	3.0	3.0