基于迹语义的网络安全协议形式化分析

• 作者: 冯珺珺 李光耀 江耘
• 来源期刊: 计算机与现代化
• 学科: 工学
• 关键词: 安全协议 形式化方法 迹语义 模型检测 SPIN/Promela
• 年，卷（期）: 2007,（2）
• 所属期刊栏目: 信息安全技术
• 页码范围: 107-109
• 页数: 3页
• 分类号: TP393.08
• 字数: 2838字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-2475.2007.02.036

摘要

形式化方法是提高软件系统,特别是safety-critical系统的安全性与可靠性的重要手段.本文提出了一种新的简单的迹语义,用于刻画协议部分安全性质,即只针对协议规约的单个主体,此技术支持协议设计者对安全性质进行形式化规约.运用此技术和模型检测器SPIN找到了两种针对TMN协议的攻击,证明了此方法的实用性,可方便地用于其它网络安全协议验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	江耘	南昌大学信息工程学院	21	78	6.0	7.0