%0 Journal Article
%T 利用类型推理验证adhoc安全路由协议
%A 李沁？
%A 曾庆凯？
%J 软件学报
%P 2822-2833
%D 2009
%X 提出一种基于类型推理的移动ad-hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算nccc(neighborhood-constrainedcommunicationcalculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动ad-hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简dolev-yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.
%K 安全协议验证
%K ad-hoc网络协议
%K 安全路由协议
%K 类型推理
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=3504&flag=1