Mobile ad hoc networks (MANETs) are self-configuring networks of mobile devices connected via wireless links. Every device in MANETs is also a router because it is required to forward traffic unrelated to its own use. These kinds of networks are exposed more than traditional networks to security threats due to their mobility and open architecture aspects. In addition, any attack can severely affect the network as all nodes participate in the routing task. For these mentioned reasons, it is important to check the validity of ad hoc protocols, and verify whether their running implementation is in accordance with their security goals in order to detect potential security flaws in the network. In this chapter, we propose a formal methodology based on passive testing techniques to collect and analyze ad hoc network traffic trace and detect potential attacks (distributed or not). Observers running on a set of nodes collect local traces and send them later to a global observer. An adapted time synchronization mechanism allows the global observer to correlate the received traces obtaining thus a global trace. The latter is then analyzed to study the security aspects of the running routing protocol. This analysis is performed using dedicated algorithms that allow checking the collected trace against a set of functional and security properties specified in a well adapted formal language called Nomad.
