基于TLA的NS安全协议分析及检测

• 作者: 万良 李祥 黄贻望
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 安全协议 模型检测 TLA TLA+ TLC
• 年，卷（期）: 2010,（7）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 38-41
• 分类号: TP309
• 字数: 3442字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.07.011

摘要

行为时序逻辑是一种组合了时序逻辑与行为逻辑来对并发系统进行描述与验证的逻辑,在描述并发转移系统中,行为时序逻辑通过引入行动和行为的概念,使得系统和属性可用同一种行为时序逻辑来表示.本文首先介绍行为时序逻辑的语法、语义及简单推理规则;然后以典型的NS公开密钥协议为例,对其进行形式化分析,建立了入侵者参加的简化模型.通过对模型进行FSM建模,转化为TLA+描述的规约系统,然后对其进行TLC检测,发现其存在中间人的重放攻击.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李祥	贵州大学计算机软件与理论研究所	91	551	13.0	19.0
2	万良	贵州大学计算机软件与理论研究所	37	125	6.0	8.0
3	黄贻望	贵州大学计算机软件与理论研究所	10	18	2.0	4.0