Modeling and Verifying the Ariadne Protocol Using Process Algebra

Mobile Ad Hoc Networks (MANETs) are formed dynamically by mobile nodes without the support of prior stationary infrastructures. In such networks, routing protocols, particularly secure ones are always the essential parts. Ariadne, an efficient and well-known on-demand secure protocol of MANETs, mainly concerns about how to prevent a malicious node from compromising the route. In this paper, we apply the method of process algebra Communicating Sequential Processes (CSP) to model and reason about the Ariadne protocol, focusing on the process of its route discovery. In our framework, we consider the communication entities as CSP processes, including the initiator, the intermediate nodes and the target. Moreover, we also propose an intruder model allowing the intruder to learn and deduce much information from the protocol and the environment. Note that the modeling approach is also applicable to other protocols, which are based on the on-demand routing protocols and have the route discovery process. Finally, we use PAT, a model checker for CSP, to verify whether the model caters for the specification and the non-trivial secure properties, e. g. nonexistence of fake path. Three case studies are given and the verification results naturally demonstrate that the fake routing attacks may be present in the Ariadne protocol.