Formal verification of RGR-SEC, a secured RGR routing for UAANETs using AVISPA, Scyther and Tamarin

Abstract

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).