research-article

Sequence numbers do not guarantee loop freedom: AODV can yield routing loops

Authors:

Rob van Glabbeek,

Marius PortmannAuthors Info & Claims

MSWiM '13: Proceedings of the 16th ACM international conference on Modeling, analysis & simulation of wireless and mobile systems

Pages 91 - 100

https://doi.org/10.1145/2507924.2507943

Published: 03 November 2013 Publication History

Abstract

In the area of mobile ad-hoc networks and wireless mesh networks, sequence numbers are often used in routing protocols to avoid routing loops. It is commonly stated in protocol specifications that sequence numbers are sufficient to guarantee loop freedom if they are monotonically increased over time. A classical example for the use of sequence numbers is the popular Ad hoc On-Demand Distance Vector (AODV) routing protocol. The loop freedom of AODV is not only a common belief, it has been claimed in the abstract of its RFC and at least two proofs have been proposed. AODV-based protocols such as AODVv2 (DYMO) and HWMP also claim loop freedom due to the same use of sequence numbers.

In this paper we show that AODV is not a priori loop free; by this we counter the proposed proofs in the literature. In fact, loop freedom hinges on non-evident assumptions to be made when resolving ambiguities occurring in the RFC. Thus, monotonically increasing sequence numbers, by themselves, do not guarantee loop freedom.

References

[1]

Kernel AODV (ver. 2.2.2), NIST. http://www.antd.nist.gov/wctg/aodv_kernel/ (September 27, 2013).

[2]

AODV-UU: An implementation of the AODV routing protocol (IETF RFC 3561). http://sourceforge.net/projects/aodvuu/ (September 27, 2013).

[3]

K. Bhargavan, D. Obradovic, and C. Gunter. Formal verification of standards for distance vector routing protocols. J. ACM, 49(4):538--576, 2002.

Digital Library

[4]

I. Chakeres and E. Belding-Royer. AODV routing protocol implementation design. In 24th International Conference on Distributed Computing Systems Workshops (WWAN'04), pages 698--703. IEEE Press, 2004.

Digital Library

[5]

S. Chiyangwa and M. Kwiatkowska. A timing analysis of AODV. In Formal Methods for Open Object-based Distributed Systems (FMOODS'05), volume 3535 of LNCS, pages 306--322. Springer, 2005.

Digital Library

[6]

A. Fehnker, R. J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W. L. Tan. Automated analysis of AODV using UPPAAL. In C. Flanagan and B. König, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214 of LNCS, pages 173--187. Springer, 2012.

Digital Library

[7]

A. Fehnker, R. J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W. L. Tan. A process algebra for wireless mesh networks. In H. Seidl, editor, European Symposium on Programming (ESOP'12), volume 7211 of LNCS, pages 295--315. Springer, 2012.

Digital Library

[8]

A. Fehnker, R. J. van Glabbeek, P. Höfner, A. McIver, M. Portmann, and W. L. Tan. A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical Report 5513, NICTA, 2013. http://www.nicta.com.au/pub?doc=5513.

[9]

J. J. Garcia-Luna-Aceves. A unified approach to loop-free routing using distance vectors or link states. In Symposium Proceedings on Communications, Architectures & Protocols (SIGCOMM '89), volume 19(4) of ACM SIGCOMM Computer Communication Review, pages 212--223. ACM Press, 1989.

Digital Library

[10]

J. J. Garcia-Luna-Aceves and H. Rangarajan. A new framework for loop-free on-demand routing using destination sequence numbers. In IEEE International Conference on Mobile Ad-hoc and Sensor Systems (MASS), pages 426--435, 2004.

[11]

T. Griffin and J. Sobrinho. Metarouting. In Proceedings of the 2005 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (SIGCOMM '05), volume 35(4) of ACM SIGCOMM Computer Communication Review, pages 1--12. ACM Press, 2005.

Digital Library

[12]

P. Höfner, R. J. van Glabbeek, W. L. Tan, M. Portmann, A. McIver, and A. Fehnker. A rigorous analysis of AODV and its variants. In Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWIM'12). ACM Press, 2012.

Digital Library

[13]

C. Huitema, J. Postel, and S. Crocker. Not all RFCs are standards. RFC 1768 (Informational), 1995.

[14]

IEEE P802.11s. IEEE draft standard for information technology - telecommunications and information exchange between systems - local and metropolitan area networks - specific requirements - part 11: Wireless LAN Medium Access Control (MAC) and physical layer (PHY) specifications-amendment 10: Mesh networking, July 2010.

[15]

V. Kawadia, Y. Zhang, and B. Gupta. System services for ad-hoc routing: Architecture, implementation and experiences. In Proceedings of the 1st international conference on Mobile systems, applications and services, MobiSys '03, pages 99--112. ACM, 2003.

Digital Library

[16]

P. M. Merlin and A. Segall. A failsafe distributed routing protocol. IEEE Transactions on Communications, com-27(9), 1979.

[17]

M. Musuvathi, D. Y. W. Park, A. Chou, D. R. Engler, and D. L. Dill. CMC: a pragmatic approach to model checking real code. In Operating Systems Design and Implementation (OSDI'02), 2002.

Digital Library

[18]

T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL sx- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

Digital Library

[19]

C. Perkins, E. Belding-Royer, and S. Das. Ad hoc on-demand distance vector (AODV) routing. RFC 3561 (Experimental), 2003. http://www.ietf.org/rfc/rfc3561.txt.

Digital Library

[20]

C. Perkins and P. Bhagwat. Highly dynamic destination-sequenced distance-vector routing (DSDV) for mobile computers. In Conference on Communications, Architectures, Protocols & Applications (SIGCOMM '94), volume 24(4) of ACM SIGCOMM Computer Communication Review, pages 234--244. ACM Press, 1994.

Digital Library

[21]

C. Perkins and I. Chakeres. Dynamic MANET on-demand (AODVv2) routing. Internet Draft (Standards Track), 2013. http://tools.ietf.org/html/draft-ietf-manet-dymo-26.

[22]

C. Perkins and E. Royer. Ad-hoc On-Demand Distance Vector Routing. In 2nd IEEE Workshop on Mobile Computing Systems and Applications, pages 90--100, 1999.

Digital Library

[23]

H. Rangarajan and J. J. Garcia-Luna-Aceves. Making on-demand routing protocols based on destination sequence numbers robust. In IEEE International Conference on Communications (ICC), volume 5, pages 3068--3072, 2005.

[24]

P. Zave. Using lightweight modeling to understand CHORD. SIGCOMM Comput. Commun. Rev., 42(2):49--57, 2012.

Digital Library

[25]

P. Zave, E. Cheung, G. W. Bond, and T. M. Smith. Abstractions for programming SIP back-to-back user agents. In International Conference on Principles, Systems and Applications of IP Telecommunications, IPTComm '09, pages 11:1--11:12. ACM Press, 2009.

Digital Library

[26]

M. Zhou, H. Yang, X. Zhang, and J. Wang. The proof of AODV loop freedom. In Wireless Communications & Signal Processing (WCSP09), pages 1--5. IEEE Press, 2009.

Cited By

Darville CHöfner PIvankovic FPam A(2022)Advanced Models for the OSPF Routing ProtocolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.355.2355(13-26)Online publication date: 21-Mar-2022
https://doi.org/10.4204/EPTCS.355.2
Garcia-Luna-Aceves J(2022)THORP: Choosing Ordered Neighbors To Attain Efficient Loop-Free Minimum-Hop Routing2022 IEEE International Symposium on Local and Metropolitan Area Networks (LANMAN)10.1109/LANMAN54755.2022.9820398(1-7)Online publication date: 11-Jul-2022
https://doi.org/10.1109/LANMAN54755.2022.9820398
Garcia-Luna-Aceves JSmith BSamson J(2022)QoS Routing Using Dominant-Distance Vectors2022 IEEE/ACM 30th International Symposium on Quality of Service (IWQoS)10.1109/IWQoS54832.2022.9812900(1-10)Online publication date: 10-Jun-2022
https://doi.org/10.1109/IWQoS54832.2022.9812900
Show More Cited By

Index Terms

Sequence numbers do not guarantee loop freedom: AODV can yield routing loops
1. Networks
  1. Network protocols
    1. Network layer protocols
      1. Routing protocols
    2. Protocol correctness
      1. Protocol testing and verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Invariants

Recommendations

A rigorous analysis of AODV and its variants
MSWiM '12: Proceedings of the 15th ACM international conference on Modeling, analysis and simulation of wireless and mobile systems

In this paper we present a rigorous analysis of the Ad hoc On-Demand Distance Vector (AODV) routing protocol using a formal specification in AWN (Algebra for Wireless Networks), a process algebra which has been specifically tailored for the modelling of ...
Modelling and verifying the AODV routing protocol

This paper presents a formal specification of the Ad hoc On-demand Distance Vector (AODV) routing protocol using AWN (Algebra for Wireless Networks), a recent process algebra which has been tailored for the modelling of mobile ad hoc networks and ...
MANET Routing Protocols Comparison for Composite Traffic Network
IMCCC '13: Proceedings of the 2013 Third International Conference on Instrumentation, Measurement, Computer, Communication and Control

The choice of routing protocols is an important issue in the establishment and design of Ad hoc networks. However, existing routing protocols are based on single traffic source or simple traffic models used in conventional networks like HTTP and video ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

MSWiM '13: Proceedings of the 16th ACM international conference on Modeling, analysis & simulation of wireless and mobile systems

November 2013

468 pages

ISBN:9781450323536

DOI:10.1145/2507924

General Chairs:
Bjorn Landfeldt
Lund University, Sweden
,
Mónica Aguilar Igartua
Universitat Politàcnica de Catalunya, Spain
,
Program Chairs:
Ravi Prakash
University of Texas at Dallas, USA
,
Cheng Li
Memorial University of Newfoundland, Canada

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSIM: ACM Special Interest Group on Simulation and Modeling

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 November 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

MSWiM '13

Sponsor:

SIGSIM

MSWiM '13: 16th ACM International Conference on Modeling, Analysis and Simulation of Wireless and Mobile Systems

November 3 - 8, 2013

Barcelona, Spain

Acceptance Rates

MSWiM '13 Paper Acceptance Rate 42 of 184 submissions, 23%;

Overall Acceptance Rate 398 of 1,577 submissions, 25%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
152
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 06 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Darville CHöfner PIvankovic FPam A(2022)Advanced Models for the OSPF Routing ProtocolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.355.2355(13-26)Online publication date: 21-Mar-2022
https://doi.org/10.4204/EPTCS.355.2
Garcia-Luna-Aceves J(2022)THORP: Choosing Ordered Neighbors To Attain Efficient Loop-Free Minimum-Hop Routing2022 IEEE International Symposium on Local and Metropolitan Area Networks (LANMAN)10.1109/LANMAN54755.2022.9820398(1-7)Online publication date: 11-Jul-2022
https://doi.org/10.1109/LANMAN54755.2022.9820398
Garcia-Luna-Aceves JSmith BSamson J(2022)QoS Routing Using Dominant-Distance Vectors2022 IEEE/ACM 30th International Symposium on Quality of Service (IWQoS)10.1109/IWQoS54832.2022.9812900(1-10)Online publication date: 10-Jun-2022
https://doi.org/10.1109/IWQoS54832.2022.9812900
Drury JHöfner PWang W(2020)Formal Models of the OSPF Routing ProtocolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.316.4316(72-120)Online publication date: 26-Apr-2020
https://doi.org/10.4204/EPTCS.316.4
Barry Rvan Glabbeek RHöfner P(2020)Formalising the Optimised Link State Routing ProtocolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.316.3316(40-71)Online publication date: 26-Apr-2020
https://doi.org/10.4204/EPTCS.316.3
Chaudhary KFehnker AMehta V(2017)Modelling, Verification, and Comparative Performance Analysis of the B.A.T.M.A.N. ProtocolElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.244.3244(53-65)Online publication date: 15-Mar-2017
https://doi.org/10.4204/EPTCS.244.3
Kamali MMerro MDal Corso A(2017)AODVv2: Performance vs. Loop FreedomSOFSEM 2018: Theory and Practice of Computer Science10.1007/978-3-319-73117-9_24(337-350)Online publication date: 22-Dec-2017
https://doi.org/10.1007/978-3-319-73117-9_24
Bres EGlabbeek RHöfner P(2016)A Timed Process Algebra for Wireless Networks with an Application in RoutingProceedings of the 25th European Symposium on Programming Languages and Systems - Volume 963210.5555/3089528.3089533(95-122)Online publication date: 2-Apr-2016
https://dl.acm.org/doi/10.5555/3089528.3089533
Glabbeek RHöfner PPortmann MTan W(2016)Modelling and verifying the AODV routing protocolDistributed Computing10.1007/s00446-015-0262-729:4(279-315)Online publication date: 1-Aug-2016
https://dl.acm.org/doi/10.1007/s00446-015-0262-7
Höfner P(2016)Using Process Algebra to Design Better ProtocolsThe Role and Importance of Mathematics in Innovation10.1007/978-981-10-0962-4_8(87-101)Online publication date: 10-Aug-2016
https://doi.org/10.1007/978-981-10-0962-4_8
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents