Modeling and Verifying the Ariadne Protocol Using Process Algebra

Xi Wu1, Huibiao Zhu1, Yongxin Zhao2, Zheng Wang3 and Si Liu4

  1. Shanghai Key Laboratory of Trustworthy Computing, Software Engineering Institute, East China Normal University
    3663 Zhongshan Road (North), Shanghai, China, 200062
    {xiwu,hbzhu}@sei.ecnu.edu.cn
  2. School of Computing, National University of Singapore
    Singapore
    zhaoyx@comp.nus.edu.sg
  3. Beijing Institute of Control Engineering
    China
    wangzheng@sei.ecnu.edu.cn
  4. Department of Computer Science, University of Illinois at Urbana-Champaign
    siliu3@illinois.edu

Abstract

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.

Key words

Formal Verification, CSP, Mobile Ad Hoc Networks, Ariadne

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS120601009W

Publication information

Volume 10, Issue 1 (Januar 2013)
Year of Publication: 2013
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Wu, X., Zhu, H., Zhao, Y., Wang, Z., Liu, S.: Modeling and Verifying the Ariadne Protocol Using Process Algebra. Computer Science and Information Systems, Vol. 10, No. 1, 393-421. (2013), https://doi.org/10.2298/CSIS120601009W