Geodesic
Modeling and Verifying the Ariadne Protocol Using Process Algebra
Computer Science and Information Systems, Tome 10 (2013) no. 1.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

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 
@article{CSIS_2013_10_1_a19,
     author = {Xi Wu and Huibiao Zhu and Yongxin Zhao and Zheng Wang and Si Liu},
     title = {Modeling and {Verifying} the {Ariadne} {Protocol} {Using} {Process} {Algebra}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {10},
     number = {1},
     year = {2013},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2013_10_1_a19/}
}
TY  - JOUR
AU  - Xi Wu
AU  - Huibiao Zhu
AU  - Yongxin Zhao
AU  - Zheng Wang
AU  - Si Liu
TI  - Modeling and Verifying the Ariadne Protocol Using Process Algebra
JO  - Computer Science and Information Systems
PY  - 2013
VL  - 10
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2013_10_1_a19/
ID  - CSIS_2013_10_1_a19
ER  - 
%0 Journal Article
%A Xi Wu
%A Huibiao Zhu
%A Yongxin Zhao
%A Zheng Wang
%A Si Liu
%T Modeling and Verifying the Ariadne Protocol Using Process Algebra
%J Computer Science and Information Systems
%D 2013
%V 10
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2013_10_1_a19/
%F CSIS_2013_10_1_a19
Xi Wu; Huibiao Zhu; Yongxin Zhao; Zheng Wang; Si Liu. Modeling and Verifying the Ariadne Protocol Using Process Algebra. Computer Science and Information Systems, Tome 10 (2013) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2013_10_1_a19/