Computer Science and Information Systems 2013 Volume 10, Issue 1, Pages: 393-421
https://doi.org/10.2298/CSIS120601009W
Full text ( 597 KB)
Cited by
Modeling and verifying the Ariadne protocol using process algebra
Wu Xi (Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute, East China Normal University, Shanghai, China)
Zhu Huibiao (Shanghai Key Laboratory of Trustworthy Computing Software Engineering Institute, East China Normal University, Shanghai, China)
Zhao Yongxin (School of Computing, National University of Singapore, Singapore)
Wang Zheng (Beijing Institute of Control Engineering, China)
Si Liu (Department of Computer Science, University of Illinois at Urbana-Champaign)
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.
Keywords: formal verification, CSP, mobile Ad Hoc Networks, Ariadne