基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁

• 作者: 程道雷 肖美华 胡磊
• 来源期刊: 计算机与数字工程
• 学科: 工学
• 关键词: 形式化方法 模型检测 Woo-Lam 协议 枚举法 打表法
• 年，卷（期）: 2014,（10）
• 所属期刊栏目: 专栏
• 页码范围: 1768-1772,1928
• 页数: 6页
• 分类号: TP393
• 字数: 4265字
• 语种: 中文
• DOI: 10.3969/j.issn1672-9722.2014.10.005

摘要

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言，将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型，枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中，提高了协议建模效率，保证了建模准确性。以Woo-Lam 协议为例，运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	肖美华		18	92	6.0	9.0
2	程道雷		4	22	3.0	4.0
3	胡磊		2	2	1.0	1.0