SAODV协议在Isabelle/HOL中的正确性验证

摘要：

将SAODV(secure Ad-hoc on-demand distance vector routing)协议的正确性性质划分为安全性性质和活动性性质.前者是指SAODV发现的路由具有某些期望的性质,如无环路等;后者是指节点一定能够找到合适的路由,并利用其成功传送数据.很多移动自组网路由协议的形式化验证工作关注安全性性质,而活动性性质却被忽略了.利用Paulson归纳法来描述SAODV协议并验证其安全性性质,扩展Paulson归纳法描述和验证SAODV的活动性性质.所有定义和推理都是在机器辅助定理证明工具Isabelle/HOL/Isar中进行的.

关键词： 移动自组网 路由协议 形式化验证 活动性 安全性

作者: 王金双 杨华兵 张兴元 王元元 张毓森

作者单位: 南京大学,软件新技术国家重点实验室,江苏,南京,210093;解放军理工大学,指挥自动化学院,江苏,南京,210007 解放军理工大学,指挥自动化学院,江苏,南京,210007

会议类型: 国内会议

会议名称: 第十六届全国网络与数据通信学术会议(NDCC2008)

会议地点: 南京

会议语种:中文

页码: 450-454

在线出版日期: 2008-11-10（万方平台首次上网日期，不代表论文的发表时间）