（非定时）AODV 路由协议无环性的机械化证明
网络与互联网体系结构
2015-05-22 v1 计算机科学中的逻辑
摘要
Ad hoc 按需距离向量（AODV）路由协议允许移动自组织网络（MANET）或无线网状网络（WMN）中的节点知道在何处转发数据包。如果此类协议永远不会导致将数据包循环转发的路由决策，则它是“无环的”。本文描述了在交互式定理证明器 Isabelle/HOL 中对已有的 AODV 无环性的笔纸证明进行机械化的过程。该机械化依赖于一种新颖的组合方法，用于将不变量提升到节点网络。我们利用该机械化分析了 AODV 的若干改进，并表明 Isabelle/HOL 能够自动重新建立大多数证明义务，并准确识别出不再有效的步骤。
引用
@article{arxiv.1505.05646,
title = {A mechanized proof of loop freedom of the (untimed) AODV routing protocol},
author = {Timothy Bourke and Robert J. van Glabbeek and Peter Höfner},
journal= {arXiv preprint arXiv:1505.05646},
year = {2015}
}
备注
The Isabelle/HOL source files, and a full proof document, are available in the Archive of Formal Proofs, at http://afp.sourceforge.net/entries/AODV.shtml