Automated security verification of routing protocols

OData support
Ta Vinh Thong
Department of Networked Systems and Services

Wireless ad-hoc networks do not have predefined infrastructure. This is a peer-to-peer network, each node is part of the routing procedure. The nodes use a protocol for the routing. There can be nodes which do not obey this rule system. An irregular behaviour is for example when nodes are not forwarding messages, or forward an incorrect message. These attacker nodes which do not follow the protocol might send fake messages, and can make other nodes to accept non-existent routes. Unfortunately, many protocols which use cryptographic methods for securing the routing procedure are found vulnerable.

My program implements an attack searcher algorithm for source routing protocols. We can define the protocol with a high level specification language. Then the program searches for an attack scenario. If an attack is found, then the exchanged messages during the attack will be displayed, as well as the network topology will be displayed as an image.

Attack finder algorithms already exist for routing protocols. But this new method doesn't need a network topology as an input. When the search procedure executes, the network builds up. This can be achieved with a backward search, we start the search when the source accepts the route. Then the search is stepping back in the path of the attack messages.


Please sign in to download the files of this thesis.