| 基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁 |
| |
| 引用本文： | 肖美华,程道雷,胡磊.基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁[J].计算机与数字工程,2014(10). |
| |
| 作者姓名： | 肖美华 程道雷 胡磊 |
| |
| 作者单位： | 1. 华东交通大学 南昌 330013
2. 南昌瑞道信息技术有限公司 南昌 330046 |
| |
| 基金项目： | 国家自然科学基金(编号61163005)；计算机软件新技术国家重点实验室开放课题(编号KFKT2012B18)；江西省高校科技落地计划项目(编号KJLD13038)；江西省自然科学基金(编号2010GZS0150，20132BAB201033)资助。 |
| |
| 摘 要： | 形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言，将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型，枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中，提高了协议建模效率，保证了建模准确性。以Woo-Lam 协议为例，运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。
|
| 关 键 词： | 形式化方法 模型检测 Woo-Lam 协议 枚举法 打表法 |
Efficiently Verify Security Properties of Woo-Lam Protocol with Spin/Promela |
| |
| XIAO Meihua,CHENG Daolei,HU Lei.Efficiently Verify Security Properties of Woo-Lam Protocol with Spin/Promela[J].Computer and Digital Engineering,2014(10). |
| |
| Authors: | XIAO Meihua CHENG Daolei HU Lei |
| |
| Abstract: | |
| |
| Keywords: | formal method model checking Woo-Lam protocol enumeration method tabulation method |
| 本文献已被 万方数据 等数据库收录！ |
