基于 Spin/Promela 的 Woo-Lam 协议安全性质高效验证磁
肖美华1
程道雷1
胡磊2
1.华东交通大学 南昌 3300132.南昌瑞道信息技术有限公司 南昌 330046
摘要：形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于 Promela 语言，将 P ．Maggi 和 R ．Sisto 提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型，枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中，提高了协议建模效率，保证了建模准确性。以Woo-Lam 协议为例，运用 Spin 工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。
关键词：形式化方法模型检测Woo-Lam 协议枚举法打表法
分类号：TP393(计算技术、计算机技术)
资助基金：国家自然科学基金(61163005)计算机软件新技术国家重点实验室开放基金(KFKT2012B18)江西省高等学校科技落地计划(KJLD13038)江西省自然科学基金(2010GZS0150)江西省自然科学基金(20132BAB201033)
论文发表日期：2014-10-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：6( 1768-1772,1928 )
英文信息