Formal Verification of Secure Ad-Hoc Network Routing Protocols Using Deductive Model-Checking
Ad-hoc networks do not rely on a pre-installed infrastructure, but they are formed by end-user devices in a self-organized manner. A consequence of this principle is that end-user devices must also perform routing functions. However, end-user devices can easily be compromised, and they may not follow the routing protocol faithfully. Such compromised and misbehaving nodes can disrupt routing, and hence, disable the operation of the network. In order to cope with this problem, several secured routing protocols have been proposed for Ad-Hoc networks. However, many of them have design flaws that still make them vulnerable to attacks mounted by compromised nodes.