Application of formal modeling to detect black hole attacks in wireless sensor network routing protocols

Black hole attack has long been a problem in wireless in data routing. Although numerous solutions have been proposed, they all have drawbacks. The main reason is that formal modeling techniques have not been employed to confirm whether the solutions are immune from black hole attacks. We have earlier shown how formal modeling can be utilized efficiently to detect the vulnerabilities of existing routing protocols against black hole attacks. In this paper we propose a new protocol, RAEED (Robust formally Analyzed protocol for wirEless sEnsor networks Deployment), which is able to address the problem of black hole attacks. Using formal modeling we prove that RAEED avoids this type of attack. Finally computer simulations were carried out to support our findings.