Call for Paper - March 2020 Edition
IJCA solicits original research papers for the March 2020 Edition. Last date of manuscript submission is February 20, 2020. Read More

A Survey on Formal Modelling for Secure Routing in Mobile Ad hoc Networks

IJCA Proceedings on International Conference on Distributed Computing and Internet Technology
© 2015 by IJCA Journal
ICDCIT 2015 - Number 1
Year of Publication: 2015
Parul Yadav
Manish Gaur

Parul Yadav and Manish Gaur. Article: A Survey on Formal Modelling for Secure Routing in Mobile Ad hoc Networks. IJCA Proceedings on International Conference on Distributed Computing and Internet Technology ICDCIT 2015(1):18-23, January 2015. Full text available. BibTeX

	author = {Parul Yadav and Manish Gaur},
	title = {Article: A Survey on Formal Modelling for Secure Routing in Mobile Ad hoc Networks},
	journal = {IJCA Proceedings on International Conference on Distributed Computing and Internet Technology},
	year = {2015},
	volume = {ICDCIT 2015},
	number = {1},
	pages = {18-23},
	month = {January},
	note = {Full text available}


Mobile ad hoc network is an autonomous collection of mobile or stationary nodes communicating with each other via radio transceivers that has limited radio transmission range. In ad hoc networking, nodes are connected without any fixed infrastructure. Applications for mobile ad hoc network range from personal networks to emergency services. Major challenges to these innovative networks are due to highly dynamic topology and limitation of resources like battery power & bandwidth. Security of routing protocols is one of the crucial and emerging issues in mobile ad hoc networks. A lot of secure versions of routing protocols in mobile ad hoc networks are already been proposed by eminent researchers. But most of them are tested by means of simulation. Simulation techniques have its limitations as it can only find presence of error rather than absence of error. To overcome this situation, formal methods are used that can verify systems using theorem proving or automated model checking techniques. This paper presents a survey on research done, so far, in line of formal modelling for secure routing in mobile ad hoc networks. The novelty of this paper is to highlight key features of proposed models for MANETs and open an area for future research.


  • Thomas Plagemann, Vera Goebel, Carsten Griwodz, and Pål Halvorsen, Towards Middleware Services for Mobile Ad-hoc Network Applications, IEEE Workshop on Future Trends of Distributed Computing Systems, pp. 249-255, 2003
  • Changling Liu and Jörg Kaiser, A Survey of Mobile Ad Hoc network Routing Protocols, Tech. Report Series, Nr. 2003-08, University of Magdeburg, pp. 1-37, 2005
  • Hao Yang, Haiyun Luo, Fan Ye, Songwu Lu, and Lixia Zhang, Security In Mobile Ad Hoc Networks: Challenges And Solutions IEEE Wireless Communications, vol. 11, issue 1, pp. 38-47, 2004
  • D. Djenouri, L. Khelladi, and N. Badache, " A survey of security issues in mobile ad hoc and sensor networks, IEEE Commun. Surveys Tutorials, vol. 7, pp. 2-28, 2005
  • Henrik Lundgren, Implementation and Real-world Evaluation of Routing Protocols for Wireless Ad hoc Networks , Licentiate thesis, Uppsala University, 2002.
  • W. Liu and Y. Fang, SPREAD: Enhancing Data Confidentiality in Mobile Ad Hoc Networks, Proc. IEEE INFOCOM, vol. 4, pp. 2404-2413, 2004
  • Y. Hu, A. Perrig, and D. B. Johnson, Packet Leashes: A defense against Wormhole Attacks in Wireless Ad Hoc Networks, Proc. IEEE INFOCOM 2003, vol. 3, pp. 1976-86, 2003
  • S. Buchegger and J. L. Boudec, Performance Analysis of the CONFIDANT Protocol (Cooperation Of Nodes-Fairness In Dynamic Ad-hoc Networks), Proc. IEEE/ACM Symp. Mobile Ad Hoc Networking and Computing (MobiHOC), pp. 226-236, 2002
  • Y. Wang, G. Attebury, and B. Ramamurthy, A Survey of Security Issues in Wireless Sensor Networks, IEEE Commun. Surveys & Tutorials, vol. 8, no. 2, pp. 2-23, 2006
  • Y. Hu and A. Perrig, A Survey of Secure Wireless Ad Hoc Routing, IEEE Comp. Society, vol. 2, issue 3, pp. 28-39, 2004
  • Y. Hu and D. B. Johonson, Securing Quality-of-Service Route Discovery in On-Demand Routing for Ad Hoc Networks, Proc. ACM SASN '04, pp. 106-117, 2004
  • Massimo Merro, An Observational Theory for Mobile Ad Hoc Networks (full version), Information and Computation, vol. 207, issue 2, pp. 194-208, 2009
  • Lucia Gallina, Sabina Rossi, A Model for Broadcast, Unicast and Multicast Communications of Mobile Ad Hoc Networks available http://www. dsi. unive. it/ srossi/Papers/icmsc10. pdf
  • Fatemeh Ghassemi, Wan Fokkink, Ali Movaghar Restricted Broadcast Process Theory, Proc. IEEE SEFM 08, pp. 345-354, 2008
  • Fatemeh Ghassemi, Ali Movaghar, Formal Modeling Routing Protocols in Mobile Adhoc Networks, The CSI Journal on Comp. Sci. And Engg. , Vol. 5, No. 2& 4(b), p 46-55, 2007
  • Anu Singh, C. R. Ramakrishnan, Scott A. Smolka, A Process Calculus for Mobile Adhoc Networks, Sci. Comput. Program. , vol. 75, issue 6, pp. 440-469, 2010
  • Sebastian Nanz, Chris Hankin, A Framework for Security Analysis of Mobile Ad Hoc Networks, Electronic Notes in Theor. Comp. Sci. , vol. 367, issue 1, pp. 203-227,2006
  • Lucia Gallina, Sabina Rossi, A Process Calculus for Energy-Aware Multicast Communications of Mobile Adhoc Networks , Wireless Communications and Mobile Computing, pp. 1-16, 2012
  • Hans Huttel, Willard Thor Rafnsson, Secrecy in Mobile Adhoc Networks available http://www. cse. chalmers. se/ rafnsson/article. pdf
  • Martin Abadi, Bruno Blanchet, Analyzing Security Protocols with Secrecy Types and Logic Program, Journal of the ACM 52,pp. 102-146, 2005
  • Oskar Wibling,Joachim Parrow, Arnold Pears, Automatized Verification of Adhoc Rouitng Protocols
  • Qiuna Niu, Formal Analysis of Secure Routing Protocol for Ad hoc Networks , Proc. IEEE WCSP 09, pp. 1-4, 2009
  • Mihai-Lica Pura, Victor-Valeriu Patriciu, Ion Bica, Modeling and formal verification of implicit ondemand secure ad hoc routing protocols in HLPSL and AVISPA, International Journal of Computers and Communications, Issue 2, Volume 3, pp. 25-32, 2009
  • Remy Chretien, Stephanie Delaune, Formal analysis of privacy for routing protocols in mobile ad hoc networks,Proc. ACM POST'13, pp. 1-20, 2013
  • M. Abadi, C. Fournet, Mobile values, new names, and secure communication, In Proc. 28th Symposium on Principles of Programming Languages (POPL'01), pp 104-115. ACM Press, 2001
  • M. Arnaud, V. Cortier, S. Delaune Modeling and verifying ad hoc routing protocols, In Proc. 23rd IEEE Comp. Security Foundations Symposium (CSF'10), pp 59-74, IEEE Comp. Society Press,2010
  • V. Cortier, J. Degrieck, S. Delaune Analysing routing protocols: four nodes topologies are sufficient, In Proc. of the 1st International Conference on Principles of Security and Trust (POST'12), LNCS, pp 30-50. Springer, 2012.
  • J. Kong, X. Hong, ANODR: anonymous on demand routing with untraceable routes for mobile ad-hoc networks, In Proc. 4th ACM Interational Symposium on Mobile Ad Hoc Networking and Computing, (MobiHoc'03), ACM, 2003
  • Xu Donghong1, Jiang Shujuan,Qi Yong, Security Properties Analysis of Routing Protocol for MANET ,Second International Conference on Networks Security, Wireless Communications and Trusted Computing, pp 405-408, IEEE Comp. Society Press, 2010
  • Matthew Hennessy, A fully abstract denotational semantics for the pi calculus , Theoretical Comp. Sci. , 278(1–2),pp. 53–89, 2002
  • V. Cortier,H. Comon,et al, Deciding Security properties for cryptographic protocols, Application to key cycles, ACM Transactions on Computational Logic, pp. 1-39, 2009
  • R. de Renesse, A. H. Aghvami, Formal verification ad hoc routing protocols using SPIN model checker, IEEE MELECON 2004, pp. 1177-1182, 2004
  • G. J. Holzmann, The model checker SPIN , IEEE Transactions on Software Engineering, vol. 23, No. 5, pp. 279-295, 1997
  • Avinash Shenoi, Yelena Yesha, Yaacov Yesha and Anupam Joshi, A Framework For Specification And Performance Evaluation Of Service Discovery Protocols In Mobile Ad-Hoc Networks , Ad Hoc Networks, Volume 4 Issue 1, pp. 1-23, 2006
  • Wissam Mallouli, Bachar Wehbi, Ana Cavalli and Stéphane Maag, Formal Supervision of Mobile Ad hoc Networks for Security Flaws Detection , Book chapter in Security Engineering Techniques and Solutions for Information Systems: Management and Implementation, Information Science Reference - IGI Global. ISBN: 9781615208036, 2011
  • Kathrin Hoffmann, Formal Modeling and Analysis of Mobile Ad Hoc Networks and Communication Based Systems using Graph and Net Technologies , Bulletin of The EATCS no 101, pp 148-160, 2010
  • H. Ehrig, K. Hoffmann, J. Padberg, C. Ermel, U. Prange, E. Biermann, and T. Modica. Petri net transformations, In Petri Net Theory and Applications, pp. 1-16, I-Tech Education and Publication, 2008
  • H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer, Fundamentals of Algebraic Graph Transformation, EATCS Monographs in Theoretical Comp. Sci. , Springer Verlag, 2006
  • A. Urpi, M. Bonuccelli, S. Giordano, Modelling cooperation in mobile ad hoc networks: a formal description of selfishness, available ftp://ftp-sop. inria. fr/maestro/WiOpt03PDFfiles/urpi10. pdf
  • Muhammad Saleem, Syed Ali Khayam, Muddassar Farooq, Formal Modeling of BeeAdHoc: a Bio-inspired Mobile Ad Hoc Network Routing Protocol, In: ANTS conference, LNCS 5217, pp 315-322, Springer-Verlag Berlin Heidelberg, 2008
  • Shrirang Ambaji Kulkarni1, Dr. G Raghavendra Rao, Formal Modeling of Reinforcement Learning Algorithms Applied for Mobile Ad Hoc Network,International Journal of Recent Trends in Engineering, Vol 2, No. 3, pp 43-47, 2009