CFP last date
20 December 2024
Call for Paper
January Edition
IJCA solicits high quality original research papers for the upcoming January edition of the journal. The last date of research paper submission is 20 December 2024

Submit your paper
Know more
The week's pick
Responsive image
Improved Shuffled Frog Leaping Algorithm with Self-Adaptive Shuffling for Fuzzy Logic PD+G Controller Optimization in Robotic Manipulators

Duc Hoang Nguyen
Random Articles
Reseach Article

Formal Verification of Authenticated AODV Protocol using AVISPA

by Kinchit Vishesh, Amandeep Verma
journal cover thumbnail

International Journal of Computer Applications
Foundation of Computer Science (FCS), NY, USA
Volume 50 - Number 19
Year of Publication: 2012
Authors: Kinchit Vishesh, Amandeep Verma
10.5120/7914-1179

Kinchit Vishesh, Amandeep Verma . Formal Verification of Authenticated AODV Protocol using AVISPA. International Journal of Computer Applications. 50, 19 ( July 2012), 38-43. DOI=10.5120/7914-1179

@article{ 10.5120/7914-1179,
author = { Kinchit Vishesh, Amandeep Verma },
title = { Formal Verification of Authenticated AODV Protocol using AVISPA },
journal = { International Journal of Computer Applications },
issue_date = { July 2012 },
volume = { 50 },
number = { 19 },
month = { July },
year = { 2012 },
issn = { 0975-8887 },
pages = { 38-43 },
numpages = {9},
url = { https://ijcaonline.org/archives/volume50/number19/7914-1179/ },
doi = { 10.5120/7914-1179 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2024-02-06T20:48:46.451331+05:30
%A Kinchit Vishesh
%A Amandeep Verma
%T Formal Verification of Authenticated AODV Protocol using AVISPA
%J International Journal of Computer Applications
%@ 0975-8887
%V 50
%N 19
%P 38-43
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

Due to the advancement in the communication technologies, people can communicate with each other anywhere on the move. The concept of ad hoc networks comes into existence in such scenarios. These networks require secure routing protocols; as such networks are vulnerable to various attacks, because of their open and dynamic infrastructure. In this paper we analyze ad hoc on-demand distance vector routing protocol (AODV) using formal verification technique. The verification has been carried out with the help of an automated tool, AVISPA. The result reveals poor authentication between the nodes of the routing protocol. To overcome the weak authentication problem found, we incorporate a secure authentication technique in AODV specification and prove it to be secure by formally verifying the results.

References
  1. A. Sobeih, M. Vishwanathan, D. Marinov, and J. C. Hou, "J-Sim: An integrated environment for simulation and model checking of network protocols", IEEE International conference on Parallel and Distributed Processing Symposium, pp. 1-6, March 2007.
  2. C. Perkins, E. Belding-Royer, S. Das, "Ad hoc On-Demand Distance Vector (AODV) Routing", RFC 3561, July 2003.
  3. C. Xiong, T. Murata, and J. Leigh, "An approach for verifying routing protocols in mobile ad hoc networks using Petri Nets",Proceedings of 6th IEEE Circuits and Systems Symposium on Emerging Technologies: Frontiers of Mobile and Wireless Communication, vol. 2, pp. 537-540, May-June 2004.
  4. D. Camara, A. A. F. Loureiro and F. Filali, "Methodology for formal verification of routing protocols for ad hoc wireless networks", IEEE conference on Global Communications, pp. 705-709, November 2007.
  5. D. Benetti, M. Merro and L. Vigano, "Model checking ad hoc network routing protocols: ARAN vs. endairA", 8th IEEE International Conference on Software Engineering and Formal Methods, pp. 191-202, September 2010.
  6. E. M. Royer and C. K. Toh, "A review of current routing protocols for ad hoc mobile wireless networks", IEEE Personal Communications, vol. 6, no. 2, pp. 46-55, April 1999.
  7. K. Bhargavan, D. Obradovic, and C. A. Gunter, "Formal verification of standards for Distance Vector Routing Protocols", Journal of ACM, vol. 49, no. 4, July 2002.
  8. L. Abusalah, A. Khokhar, and M. Guizani, "A survey of secure mobile ad hoc routing protocols", IEEE Communications Surveys and Tutorials, vol. 10, no. 4, pp. 78-93, 2008.
  9. L. Zhou and Z. J. Haas, "Securing ad hoc networks", IEEE Network Journal, November-December 1999, 13(6), pp. 24-30.
  10. M. L. Pura, V. V. Patriciu and I. Bica, "Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study",Proceedings of 4th European Computing Conference, 2010.
  11. R. de Renesse and A. H. Aghvami, "Formal verification of ad-hoc routing protocols using SPIN model checker", 12th IEEE Mediterranean Electrotechnical Conference, vol. 3, pp. 1177-1182, May 2004.
  12. R. Bhaskar, J. Herranz and F. Laguillaumie, "Efficient authentication for reactive routing protocols", 20th International Conference on Advanced Information Networking and Applications, vol. 2, pp. 57-61, April 2006.
  13. S. Georgoulas, K. Moessner, B. Mcaleer, and R. Tafazolli, "Using formal verification methods and tools for protocol profiling and performance assessment in mobile and wireless environments", 21st Annual IEEE International Symposium on Personal, Indoor and Mobile Radio Communications, pp. 2471-2476, September 2010.
  14. The AVISPA team, "AVISPA v1. 1 User Manual", June 2006.
  15. The AVISPA team, "HLPSL Tutorial", June 2006.
Index Terms

Computer Science
Information Sciences

Keywords

AVISPA HLPSL AODV

Powered by PhDFocusTM