We suggest a Calculus for Mobile Ad Hoc Networks, CMAN. A node in a network is a processes equipped with a location, it may communicate with other nodes using synchronous local 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 a reduction congruence. We define a labeled transition semantics and prove that the (early) weak contextual bisimulation is a sound and complete co-inductive characterizations of the reduction congruence. Finally, we apply CMAN on a small example of a cryptographic routing protocol.
Jens Chr. Godskesen