A calculus of trustworthy ad hoc networks

We propose a process calculus for mobile ad hoc networks which embodies a behaviour-based multilevel decentralised trust model. Our trust model supports both direct trust, by monitoring nodes behaviour, and indirect trust, by collecting recommendations and spreading reputations. The operational semantics of the calculus is given in terms of a labelled transition system, where actions are executed at a certain security level. We define a labelled bisimilarity parameterised on security levels. Our bisimilarity is a congruence and an efficient proof method for an appropriate variant of barbed congruence, a standard contextually-defined program equivalence. Communications are proved safe with respect to the security levels of the involved parties. In particular, we ensure safety despite compromise: compromised nodes cannot affect the rest of the network. A non interference result expressed in terms of information flow is also proved.