利用类型推理验证Ad Hoc安全路由协议

• 作者: 曾庆凯 李沁
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 安全协议验证 ad-hoc网络协议 安全路由协议 类型推理
• 年，卷（期）: 2009,（10）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 2822-2833
• 页数: 12页
• 分类号: TP393
• 字数: 9720字
• 语种: 中文
• DOI: 10.3724/SP.J.1001.2009.03504

摘要

提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	曾庆凯	南京大学计算机软件新技术国家重点实验室	58	555	13.0	21.0
5	李沁	南京大学计算机软件新技术国家重点实验室	4	16	2.0	4.0