Date Added: Sep 2011
The authors propose a process calculus for mobile ad hoc networks which relies on an abstract behaviour-based multilevel trust model. The operational semantics of the calculus is given in terms of a labelled transition system, where actions are executed at a certain security level. They define a labelled bisimilarity over networks parameterised on security levels. Their bisimilarity is congruence and an efficient proof method for an appropriate variant of barbed congruence, standard contextually-defined program equivalence. Communications in the calculus are safe with respect to the security levels of the involved parties. In particular, they ensure safety despite compromise: compromised nodes cannot affect the rest of the network. A non-interference result is also proved in terms of information flow.