We present a framework for specification and security analysis of communication
protocols for mobile wireless networks. This setting introduces new challenges which
are not being addressed by classical protocol analysis techniques. 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 order to model this scenario
faithfully, we present a broadcast calculus which makes a clear distinction between
the protocol processes and the network’s connectivity graph, which may change independently
from protocol actions. We identify a property characterising an important
aspect of security in this setting and express it using behavioural equivalences of the
calculus. We complement this approach with a control flow analysis which enables us
to automatically check this property on a given network and attacker specification.