%0 Conference Proceedings
%T Loop Freedom in AODVv2
%+ Alcatel-Lucent Bell Labs
%+ University of Waterloo [Waterloo]
%A Namjoshi, Kedar, S.
%A Trefler, Richard, J.
%Z Part 2: Formal Models of Concurrent and Distributed Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 98-112
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_7
%K Target Node
%K Actual Protocol
%K Mobile Router
%K Route Entry
%K Route Table
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X The AODV protocol is used to establish routes in a mobile, ad-hoc network (MANET). The protocol must operate in an adversarial environment where network connections and nodes can be added or removed at any point. While the ability to establish routes is best-effort under these conditions, the protocol is required to ensure that no routing loops are ever formed. AODVv2 is currently under development at the IETF, we focus attention on version 04. We detail two scenarios that show how routing loops may form in AODVv2 routing tables. The second scenario demonstrates a problem with the route table update performed on a Broken route entry. Our solution to this problem has been incorporated by the protocol designers into AODVv2, version 05. With the fix in place, we present an inductive and compositional proof showing that the corrected core protocol is loop-free for all valid configurations.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767329/document
%2 https://inria.hal.science/hal-01767329/file/978-3-319-19195-9_7_Chapter.pdf
%L hal-01767329
%U https://inria.hal.science/hal-01767329
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039