| 利用类型推理验证Ad Hoc安全路由协议 |
| |
| 引用本文： | 李 沁,曾庆凯.利用类型推理验证Ad Hoc安全路由协议[J].软件学报,2009,20(10):2822-2833. |
| |
| 作者姓名： | 李 沁 曾庆凯 |
| |
| 作者单位： | 南京大学,计算机软件新技术国家重点实验室,江苏,南京,210093;南京大学,计算机科学与技术系,江苏,南京,210093 |
| |
| 基金项目： | Supported by the National Natural Science Foundation of China under Grant Nos.60773170, 60721002, 90818022 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2006AA01Z432 (国家高技术研究发展计划(863)); the Specialized Research F |
| |
| 摘 要： | 提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.
|
| 关 键 词： | 安全协议验证 ad-hoc网络协议 安全路由协议 类型推理 |
| 收稿时间： | 2007/12/6 0:00:00 |
| 修稿时间： | 6/9/2009 12:00:00 AM |
Verifying Mobile Ad-Hoc Security Routing Protocols with Type Inference |
| |
| LI Qin and ZENG Qing-Kai.Verifying Mobile Ad-Hoc Security Routing Protocols with Type Inference[J].Journal of Software,2009,20(10):2822-2833. |
| |
| Authors: | LI Qin and ZENG Qing-Kai |
| |
| Abstract: | A type-inference-based formal method is proposed for verifying an ad-hoc security routing protocol in this paper. A calculus, called NCCC (neighborhood-constraint communication calculus), is defined to specify the protocol. The security property of the protocol is described with typing rules in a type system. Based on the Dolev-Yao model, an attacker model, called the message set of protocol format, is refined. At last, the simplified version of SAODV (secure ad hoc on-demand routing protocol) is verified with this method. With the type- inference-based formal method, not only is the security of protocols verified, but also the attacke examples are predicted. The complexity of inference is reduced significantly for refining the message set of protocol. |
| |
| Keywords: | verification of security protocol ad-hoc protocol security routing protocol type inference |
| 本文献已被 万方数据 等数据库收录！ |
| 点击此处可从《软件学报》浏览原始摘要信息 |
|
点击此处可从《软件学报》下载全文 |
|
