We 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. We define a labelled bisimilarity over 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 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. 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.

A calculus of trustworthy ad hoc networks

MERRO, Massimo;SIBILIO, Eleonora
2013-01-01

Abstract

We 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. We define a labelled bisimilarity over 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 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. 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.
2013
Ad Hoc Network; Trust model; Non-interference; Behavioral semantics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/469993
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 11
  • ???jsp.display-item.citation.isi??? 8
social impact