A calculus of trustworthy ad hoc networks
Massimo Merro, Eleonora Sibilio · Formal Aspects of Computing · 2011
Abstract We propose aprocess calculusformobile ad hoc networkswhich relies on an abstract behaviour-based multileveltrust 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. We define alabelled bisimilarityover networks 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 in the calculus are safe with respect to the security levels of the involved parties. In particular, we ensuresafety despite compromise: compromised nodes cannot affect the rest of the network. Anon-interferenceresult is also proved in terms of information flow. Finally, we use our calculus to provide formal descriptions of trust-based versions of both a routing protocol and a leader election protocol for ad hoc networks.