摘要
将SAODV(secure Ad-hoc on-demand distance vector routing)协议的正确性性质划分为安全性性质和活动性性质。前者是指SAODV发现的路由具有某些期望的性质,如无环路等;后者是指节点一定能够找到合适的路由,并利用其成功传送数据。很多移动自组网路由协议的形式化验证工作关注安全性性质,而活动性性质却被忽略了。利用Paulson归纳法来描述SAODV协议并验证其安全性性质,扩展Paulson归纳法描述和验证SAODV的活动性性质。所有定义和推理都是在机器辅助定理证明工具Isabelle/HOL/Isar中进行的。
The correctness properties of the SAODV（secure Ad-hoc on-demand distance vector routing） protocol was classified into safety properties and liveness properties. The former states that routes discovered by SAODV have some desired properties, such as loop-freedom etc. The later states that once a node wants to send a message to a destination, it can eventually find a route, through which data can be transmitted successfully. Many safety properties for routing protocols were verified, whereas the reasoning of liveness properties was neglected. SAODV with Paulson＇s inductive approach was deseribed, both safety properties and liveness properties of SAODV were verified. All formalizations and proofs were carried out with Isabelle/HOL/Isar.
出处
《解放军理工大学学报（自然科学版）》
EI
2008年第5期450-454,共5页
Journal of PLA University of Science and Technology(Natural Science Edition)
基金
国家自然科学基金资助项目(60373068)
