Modelling and Analysing Overlay Networks by Ambients with Wormholes

Process calculi are a powerful mechanism to formally model distributed systems, and are especially useful for assessing trust, security, and privacy issues in mobile and ubiquitous computing and networking. However, they often only support a single modelling approach and semantics, whereas distributed systems and networks often are a conglomeration of different technologies and functionalities. In this paper we propose a novel approach to model these systems and make them amenable to formal analysis. We enhance the ambient calculus with “wormholes” as a convenient way for ambients to travel between “worlds” representing the different technologies and functionalities by means of different semantic layers. Our approach enables easy and natural modelling and analysis of multi-layer systems for ubiquitous computing and networking.