Towards a Behavioural Theory of Access and Mobility Control in Distributed Systems.

Abstract

We de ne a typed bisimulation equivalence for the language Dpi, a dis- tributed version of the -calculus in which processes may migrate between dynamically created locations. It takes into account resource access policies, which can be imple- mented in Dpi using a novel form of dynamic capability types. The equivalence, based on typed actions between con gurations, is justi ed by showing that it is fully-abstract with respect to a natural distributed version of a contextual equivalence. In the second part of the paper we study the e ect of controlling the migration of processes. This a ects the ability to perform observations at speci c locations, as the observer may be denied access. We show how the typed actions can be modi ed to take this into account, and generalise the full-abstraction result to this more delicate scenario.