References

  1. J. Ahrenholz, C. Danilov, T. Henderson & J. Kim (2008): CORE: A Real-Time Network Emulator. In: IEEE Military Communications Conference, MILCOM'08, doi:10.1109/MILCOM.2008.4753614.
  2. G. Behrmann, A. David & K. G. Larsen (2004): A Tutorial on Uppaal. In: Marco Bernardo & Flavio Corradini: Formal Methods for the Design of Real-Time Systems, Lecture Notes in Computer Science 3185. Springer, pp. 200–236, doi:10.1007/978-3-540-30080-9_7.
  3. Karthikeyan Bhargavan, Davor Obradovic & Carl A. Gunter (2002): Formal Verification of Standards for Distance Vector Routing Protocols. J. ACM 49(4), pp. 538–576, doi:10.1145/581771.581775.
  4. B. Blanchet (2016): Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security 1(1-2), pp. 1–135, doi:10.1561/3300000004.
  5. E. Bres, R. van Glabbeek & P. Höfner (2016): A Timed Process Algebra for Wireless Networks with an Application in Routing (Extended Abstract). In: P. Thiemann: Programming Languages and Systems (ESOP'16), Lecture Notes in Computer Science 9632. Springer, pp. 95–122, doi:10.1007/978-3-662-49498-1_5.
  6. E. Clarke, D. Kroening & F. Lerda (2004): A Tool for Checking ANSI-C Programs. In: K. Jensen & A. Podelski: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), Lecture Notes in Computer Science 2988. Springer, pp. 168–176, doi:10.1007/978-3-540-24730-2_15.
  7. R. Coltun, D. Ferguson, J. Moy & A. Lindem (2008): OSPF for IPv6. RFC 5340, Network Working Group. Available at http://www.ietf.org/rfc/rfc5340.txt.
  8. L. De Moura & N. Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & J. Rehof: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), Lecture Notes in Computer Science 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  9. E. W. Dijkstra (1959): A Note on Two Problems in Connexion with Graphs. Numerische Mathematik 1(1), pp. 269–271, doi:10.1007/BF01386390.
  10. J. Drury, P. Höfner & W. Wang (2020): Formal Models of the OSPF Routing Protocol. In: A. Fehnker & H. Garavel: Models for Formal Analysis of Real Systems (MARS'20), Electronic Proceedings in Theoretical Computer Science 316. Open Publishing Association, pp. 72–120, doi:10.4204/EPTCS.316.4.
  11. E. A. Emerson (1990): Temporal and Modal Logic. In: Handbook of Theoretical Computer Science (vol. B): Formal Models and Semantics. MIT Press, pp. 995–1072, doi:10.1016/B978-0-444-88074-1.50021-4.
  12. A. Fehnker, R. J. van Glabbeek, P Höfner, A. K. McIver, M. Portmann & W. L. Tan (2012): Automated Analysis of AODV using UPPAAL. In: C. Flanagan & B. König: Tools and Algorithms for the Construction and Analysis of Systems (TACAS '12), Lecture Notes in Computer Science 7214. Springer, pp. 173–187, doi:10.1007/978-3-642-28756-5_13.
  13. A. Fehnker, L. van Hoesel & A. Mader (2007): Modelling and Verification of the LMAC Protocol for Wireless Sensor Networks. In: Integrated Formal Methods, IFM'07, Lecture Notes in Computer Science 4591. Springer, pp. 253–272, doi:10.1007/978-3-540-73210-5_14.
  14. R. J. van Glabbeek, P. Höfner, W. L. Tan & M. Portmann (2013): Sequence Numbers Do Not Guarantee Loop Freedom —AODV Can Yield Routing Loops—. In: Modeling, Analysis and Simulation of Wireless and Mobile Systems (MSWiM '13). ACM, pp. 91–100, doi:10.1145/2507924.2507943.
  15. K. Havelund, K. G. Larsen & A. Skou (1999): Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. In: J.-P. Katoen: Formal Methods for Real-Time and Probabilistic Systems (ARTS'99), Lecture Notes in Computer Science 1601. Springer, pp. 277–298, doi:10.1007/3-540-48778-6_17.
  16. ISO/IEC/IEEE 8802-11 (2018): 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. Available at https://www.iso.org/standard/73367.html.
  17. E. Jones & O. Le Moigne (2006): OSPF Security Vulnerabilities Analysis. Routing Protocol Security. Available at https://tools.ietf.org/id/draft-ietf-rpsec-ospf-vuln-02.txt.
  18. K. G. Larsen, P. Pettersson & Wang Yi (1997): UPPAAL in a Nutshell. International Journal of Software Tools for Technology Transfer 1(1-2), pp. 134–152, doi:10.1007/s100090050010.
  19. S.U.R Malik, S. K. Srinivasan & S. U. Khan (2012): A Methodology for OSPF Routing Protocol Verification.
  20. S. Meier, B. Schmidt, C. Cremers & D. Basin (2013): The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: N. Sharygina & H. Veith: Computer Aided Verification (CAV'13), Lecture Notes in Computer Science 8044. Springer, pp. 696–701, doi:10.1007/978-3-642-39799-8_48.
  21. S. Miskovic & E. W. Knightly (2010): Routing Primitives for Wireless Mesh Networks: Design, Analysis and Experiments. In: INFOCOM'10. IEEE, pp. 2793–2801, doi:10.1109/INFCOM.2010.5462111.
  22. J. Moy (1998): OSPF Version 2. RFC 2328, Network Working Group. Available at http://www.ietf.org/rfc/rfc2328.txt.
  23. G. Nakibly, D. Gonikman, A. Kirshon & D. Boneh (2012): Persistent OSPF Attacks.
  24. G. Nakibly, A. Sosnovich, E. Menahem, A. Waizel & Y. Elovici (2014): OSPF Vulnerability to Persistent Poisoning Attacks: A Systematic Analysis. In: Computer Security Applications Conference, ACSAC '14. ACM, pp. 336–345, doi:10.1145/2664243.2664278.
  25. R. de Renesse & A.H. Aghvami (2004): Formal Verification of Ad Hoc Routing Protocols Using SPIN Model Checker. In: IEEE MELECON'04. IEEE, pp. 1177 – 1182, doi:10.1109/MELCON.2004.1348275.
  26. O. Wibling, J. Parrow & A. N. Pears (2004): Automatized Verification of Ad Hoc Routing Protocols. In: Formal Techniques for Networked and Distributed Systems, FORTE'04, Lecture Notes in Computer Science 3235. Springer, pp. 343–358, doi:10.1007/978-3-540-30232-2_22.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org