Formal Modelling of Intrusion Detection System in Mobile Ad hoc Networks

Abstract

Security of routing protocols is one of the crucial and emerging issues newlinein mobile ad-hoc networks. A lot of secure versions of routing protocols in mobile ad-hoc networks have already been proposed by eminent newlineresearchers. But most of them are tested by means of simulation. Simulation techniques have their limitations as they can only find presence newlineof error rather than absence of error. To overcome this situation, formal newlinemethods can aid in verifying systems using theorem proving or automated newlinemodel checking techniques. One of the techniques for formal verification newlineof system is by using process calculus. newlineIn this thesis, we propose a calculus in process algebraic framework newlineto formally model Intrusion Detection System (IDS) for secure routing newlinein mobile ad-hoc networks. The proposed calculus, named as dRi newline, is an newlineadaptation of distributed pi calculus (Dpi). The proposed calculus models newlineunicast, multicast and broadcast communications, node mobility, energy newlineconservation at node as well as detection of malicious node(s) in mobile adhoc networks. The calculus has two syntactic categories: one for describing newlinesystems and another for processes which reside in nodes. We also present newlinetwo views of semantics; one as reduction on configurations whereas another as Labeled Transition Systems (LTSs), behavioural semantics, where newlinereduction on configurations are described on various actions. We justify newlineour calculus using two views. In first view, we justify our model by providing its reduction equivalence, after abstracting away the details of IDS newline(implementation), to its specification calculus for Energy-aware Broadcast, Unicast and Multicast communications of mobile ad-hoc networks newline(E-BUM). We show that proposed calculus conforms to its specification. In newlinesecond view, we define a bisimulation based equivalence between configurations defined over LTSs. Further, we define a touch-stone equivalence newlineon its reduction semantics and prove that bisimulation based equivalence newlinecan be recovered from its touch-stone equivalence and vice-versa. newlineWe