A Calculus for Mobile Ad Hoc Networks

We suggest a Calculus for Mobile Ad Hoc Networks, CMAN. A node in a network is a process equipped with a location, it may communicate with other nodes using synchronous spatially oriented broadcast where only the current neighbors receive the message. Nodes may autonomously change their neighbor relationship and thereby change the network topology. We define a natural reduction semantics and strong and weak reduction congruences as well as a labeled transition semantics and prove strong and weak contextual bisimulation respectively to be sound and complete co-inductive characterizations of the corresponding reduction congruences. For the subset of connection closed networks we show a significantly simpler co-inductive characterization. Finally, we apply CMAN on a small example of a cryptographic routing protocol.