Call for Paper - November 2022 Edition
IJCA solicits original research papers for the November 2022 Edition. Last date of manuscript submission is October 20, 2022. Read More

Formal Verification of Authenticated AODV Protocol using AVISPA

Print
PDF
International Journal of Computer Applications
© 2012 by IJCA Journal
Volume 50 - Number 19
Year of Publication: 2012
Authors:
Kinchit Vishesh
Amandeep Verma
10.5120/7914-1179

Kinchit Vishesh and Amandeep Verma. Article: Formal Verification of Authenticated AODV Protocol using AVISPA. International Journal of Computer Applications 50(19):38-43, July 2012. Full text available. BibTeX

@article{key:article,
	author = {Kinchit Vishesh and Amandeep Verma},
	title = {Article: Formal Verification of Authenticated AODV Protocol using AVISPA},
	journal = {International Journal of Computer Applications},
	year = {2012},
	volume = {50},
	number = {19},
	pages = {38-43},
	month = {July},
	note = {Full text available}
}

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

  • 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.
  • C. Perkins, E. Belding-Royer, S. Das, "Ad hoc On-Demand Distance Vector (AODV) Routing", RFC 3561, July 2003.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • L. Zhou and Z. J. Haas, "Securing ad hoc networks", IEEE Network Journal, November-December 1999, 13(6), pp. 24-30.
  • 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.
  • 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.
  • 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.
  • 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.
  • The AVISPA team, "AVISPA v1. 1 User Manual", June 2006.
  • The AVISPA team, "HLPSL Tutorial", June 2006.