Formal Verification of RGR-SEC, a Secured RGR Routing for UAANETs Using AVISPA, Scyther and Tamarin

  • Houssem E. MohamadiEmail author
  • Nadjia Kara
  • Mohand Lagha
Conference paper
Part of the Communications in Computer and Information Science book series (CCIS, volume 878)


Designing an adaptive routing protocol for Unmanned Aeronautical Ad-hoc Networks (UAANETs) is very challenging. UAANET routing protocols are vulnerable to several attacks and threats. Thus applying security mechanisms is crucial to ensure the authentication, data integrity and confidentiality. Moreover, when applying formal verification methods to analyze protocols, it is necessary to define a model that formalizes their semantics and security requirements. In this paper, we focus on a hybrid routing protocol, called the Reactive-Greedy-Reactive (RGR), which combines the mechanisms of reactive routing and Greedy Geographic Forwarding (GGF). Our main contribution is to enhance the reactive mode of RGR protocol by incorporating three security mechanisms: a node-to-node authentication approach, a keyed-hash message authentication code and an aggregate designated verifier signature scheme. The results of our formal analysis are validated via three automated verification tools (AVISPA, Scyther and Tamarin).


UAANETs RGR Security mechanisms Reactive mode Formal verification Automated verification tools 


  1. 1.
    ElKholy, H.M.N., Habib, M.-K.: Dynamic modeling and control of a Quadrotor using linear and nonlinear approaches. M.S. thesis, The American University in Cairo (2014)Google Scholar
  2. 2.
    Li, Y., St-Hilaire, M., Kunz, T.: Enhancing the RGR routing protocol for unmanned aeronautical ad-hoc networks. Technical report SCE-12-01, Systems and Computer Engineering, Carleton University (2012)Google Scholar
  3. 3.
    Maxa, J.-A., Ben Mahmoud, M.-S., Larrieu, N.: Extended verification of secure UAANET routing protocol. In: 35th Digital Avionics Systems Conference, Sacramento, United States (2016)Google Scholar
  4. 4.
    Maxa, J.-A.: Architecture de communication scurise d’une flotte de drones. Rseaux et tlcommunications. Universit Toulouse 3 Paul Sabatier, Français (2017)Google Scholar
  5. 5.
    Maxa, J.-A., Ben Mahmoud, M.-S., Larrieu, N.: Survey on UAANET routing protocols and network security challenges. Ad Hoc Sens. Wirel. Netw. (2017)Google Scholar
  6. 6.
    Câmara, D., Loureiro, A.A., Filali, F.: Formal verification of routing protocols for wireless ad hoc networks. In: Misra, S., Woungang, I., Chandra Misra, S. (eds.) Guide to Wireless Ad Hoc Networks. Computer Communications and Networks. Springer, London (2009). Scholar
  7. 7.
    Sharma, P., Yadav, I.: Improving reactive greedy reactive routing in flying ad hoc networks. Int. J. Sci. Eng. Technol. Res. 5(7), 2276–2281 (2016)Google Scholar
  8. 8.
    Anisha, S.L.: Enhancing RGR routing in unmanned air vehicles networks. Int. J. Sci. Eng. Technol. Res. 5(7), 2338–2343 (2016)Google Scholar
  9. 9.
    Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds.) FPS 2015. LNCS, vol. 9482, pp. 137–155. Springer, Cham (2016). Scholar
  10. 10.
    Xiong, C., Murata, T., Leigh, J.: An approach for verifying routing protocols in mobile ad hoc networks using Petri Nets. In: Proceedings of 6th IEEE Circuits and Systems Symposium on Emerging Technologies: Frontiers of Mobile and Wireless Communication, vol. 2, pp. 537–540 (2004).
  11. 11.
    Bhargavan, K., Obradovic, D., Gunter, C.A.: Formal verification of standards for distance vector routing protocols. J. ACM 49(4), 538–576 (2002). Scholar
  12. 12.
    Gürdag, A.-B., Çaglayan, M.-U.: A formal security analysis of secure AODV (SAODV) using model checking. In: Proceedings of 8th International Symposium on Computer Networks (2008)Google Scholar
  13. 13.
    Ács, G., Buttyán, L., Vajda, I.: Provable security of on-demand distance vector routing in wireless ad hoc networks. In: Molva, R., Tsudik, G., Westhoff, D. (eds.) ESAS 2005. LNCS, vol. 3813, pp. 113–127. Springer, Heidelberg (2005). Scholar
  14. 14.
    Nanz, S., Hankin, C.: A framework for security analysis of mobile wireless networks. Theor. Comput. Sci. 367(1–2), 203–227 (2006). Scholar
  15. 15.
    Perkins, C.-E., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. Internet RFCs, pp. 1–38 (2003)Google Scholar
  16. 16.
    Bekmezci, I., Senturk, E., Turker, T.: Security issues in flying ad-hoc networks (FANETS). J. Aeronaut. Space Technol. 9(2), 13–21 (2016)Google Scholar
  17. 17.
    Liao, L.: Group key agreement for ad hoc networks. Master thesis, Ruhr-University Bochum, Germany (2005)Google Scholar
  18. 18.
    Münch, M.: Integration and verification of a keyed-hash of a message authentication scheme based on broadcast timestamps for NUTS. Master thesis, NTNU, Trondheim (2014)Google Scholar
  19. 19.
    Bhaskar, R., Herranz, J., Laguillaumie, F.: Efficient authentication for reactive routing protocols. In: 20th International Conference on Advanced Information Networking and Applications, vol. 2, pp. 57–61 (2006).
  20. 20.
    Vishesh, K., Verma, A.: Formal verification of authenticated AODV protocol using AVISPA. Int. J. Comput. Appl. 50(19), 38–43 (2012). Scholar
  21. 21.
    Meadows, C.A., Meadows, C.A.: Formal verification of cryptographic protocols: a survey. In: Pieprzyk, J., Safavi-Naini, R. (eds.) ASIACRYPT 1994. LNCS, vol. 917, pp. 133–150. Springer, Heidelberg (1995). Scholar
  22. 22.
    The AVISPA Team: AVISPA v1.1 User Manual (2006)Google Scholar
  23. 23.
    Pfeffer, K.: Formal verification of a LTE security protocol for dual-connectivity. M.S. thesis, KTH Royal Institute of Technology, Stockholm, Sweden (2014)Google Scholar
  24. 24.
    The Tamarin Team: Tamarin-Prover Manual: Security Protocol Analysis in the Symbolic Model (2017)Google Scholar
  25. 25.
    Perrig, A., Johnson, D.-B.: Packet leashes: a defense against wormhole attacks in wireless ad hoc networks. In: IEEE INFOCOM, pp. 1976–1986 (2003).

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Houssem E. Mohamadi
    • 1
    Email author
  • Nadjia Kara
    • 2
  • Mohand Lagha
    • 1
  1. 1.Institute of Aeronautics and Spatial StudiesUniversity of Blida 1BlidaAlgeria
  2. 2.Department of Software Engineering and Information TechnologiesÉcole de Technologie SuperieureMontrealCanada

Personalised recommendations