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