Mobile ad-hoc networks consist of mobile wireless devices which autonomously organise their communication infrastructure. Because of the simple network deployment this networking paradigm offers much convenience, but security turns out to be an important concern when considering the threats implied in using the wireless medium. In order to eliminate such concerns, formal specification and analysis techniques have to be used so that the employed communication protocols can be proved secure or their vulnerabilities exposed. While many such frameworks have been proposed for the analysis of classical security protocols, the challenges of the new setting prevent these from being applied directly. The main complication stems from the fact that the actions of intermediate nodes and their connectivity can no longer be abstracted into a single unstructured adversarial environment as they form an inherent part of the system's security.

In this talk we present a framework for modelling and reasoning about mobile ad-hoc networks and their security needs. Communication protocols are specified using a broadcast process calculus which makes a clear distinction between the protocol processes and the network's connectivity graph, which may change independently from protocol actions. This modelling formalism is complemented by a control flow analysis which yields an overapproximation of the possible behaviour of a network specified with the calculus. The results obtained from the analysis can be used to establish a behavioural equivalence for networks which in turn is used to specify security requirements. We have analysed two real-world routing protocols for mobile ad-hoc networks using a prototype implementation of this framework and present some of the exposed attacks.