Formal Security Analysis for Ad-Hoc Networks

In ad-hoc networks, autonomous wireless nodes can communicate by forwarding messages for each other. For routing protocols in this setting, it is known that a malicious node can perform a variety of attacks just by not behaving according to the specification. Whilst secure versions of routing protocols are under development, little effort has been made to formalise the scenario similarly to developments in the realm of traditional security protocols for secrecy and authentication. We present a broadcast process calculus suitable to describe the behaviour of protocols which require a local memory component for every node. By adding annotations for the origin of messages, we are able to formalise a vital security property in this context, called store authorisation. Furthermore, we describe a static analysis for the detection of violations of this property. For a model of the AODV protocol in our calculus, we are then able to deduce that an attacker may introduce a routing loop in certain networks.