基于Spin/Promela的Woo-Lam协议安全性质高效验证
形式化方法是分析验证安全协议的重要技术之一.模型检测是用在形式化方法中实现形式化自动验证的重要手段.基于Promela语言,将P.Maggi和R.Sisto提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性.以Woo-Lam协议为例,运用Spin工具成功发现一个已知著名攻击.此通用方法适用于类似复杂协议形式化分析与验证.
计算机网络 Woo-Lam协议 形式化方法 模型检测 Promela语言 Spin工具 安全性质
肖美华 程道雷 胡磊
华东交通大学 南昌 330013 南昌瑞道信息技术有限公司 南昌 330046
国内会议
济南
中文
1-7
2014-10-16(万方平台首次上网日期,不代表论文的发表时间)