论文部分内容阅读
将SAODV（secure Ad—hocon—demand distance vector routing）协议的正确性性质划分为安全性性质和活动性性质。前者是指SAODV发现的路由具有某些期望的性质，如无环路等；后者是指节点一定能够找到合适的路由，并利用其成功传送数据。很多移动自组网路由协议的形式化验证工作关注安全性性质，而活动性性质却被忽略了。利用Paulson归纳法来描述SAODV协议并验证其安全性性质，扩展Paulson归纳法描述和验证SAODV的活动性性质。所有定义和推理都是在机器辅助定理证明工