manet路由协议的正确性分析

移动自组网(manet)是当前网络研究的一个热点，但是由于安全问题致使其未能广泛应用。在安全问题中，路由协议的正确性尤为重要。采用形式验证方法分析了manet非安全路由协议和安全路由协议的正确性。首先给出了协议正确性的形式描述以及攻击者的形式定义，将协议的正确性分为安全性(safetyproperty)和活性(livenessproperty)，前者指协议所发现的路由具有某些良好的性质，后者指协议能够发现路由而且能够顺利地传输数据；然后提出了两个活性证明规则――响应性证明规则和反应性证明规则，并用所提