%0 Journal Article
%T manet路由协议的正确性分析
%A 杨华兵
%A 张兴元
%A 王元元
%J 南京邮电大学学报(自然科学版)
%P 15-19
%D 2007
%X 移动自组网(manet)是当前网络研究的一个热点，但是由于安全问题致使其未能广泛应用。在安全问题中，路由协议的正确性尤为重要。采用形式验证方法分析了manet非安全路由协议和安全路由协议的正确性。首先给出了协议正确性的形式描述以及攻击者的形式定义，将协议的正确性分为安全性(safetyproperty)和活性(livenessproperty)，前者指协议所发现的路由具有某些良好的性质，后者指协议能够发现路由而且能够顺利地传输数据；然后提出了两个活性证明规则――响应性证明规则和反应性证明规则，并用所提
%K manet
%K 路由协议
%K 形式验证
%K 正确性
%U http://nyzr.njupt.edu.cn/ch/reader/view_abstract.aspx?file_no=200702004&flag=1