Secure Open Networks

We examine and model open networks enforcing the control of safe and authorised communication, i.e. data and resources usage. By an open network we mean an Internet-like global network, where each subject only partially knows and trusts other subjects and their resources. Our goal is to obtain an abstract model that describes faithfully such networks, where computational units communicate one to another exchanging code, and aim at each others resources. Moreover we want to provide a model with efficient abstract mechanisms that enforce correct resource usage, at least for the portion of the open network one is interested in. For the underlying language we choose the π-calculus and its distributed variant the Dπ-calculus. We divide our analysis in phases, hence make it easy to follow the development of the solution. We start with a concurrent model and a simple type system, then enhance types to obtain a faithful model for resources. We close with a distributed model that enforces safe, and lastly authorised resource usage. The thesis is written in a textbook style and may be used as an introduction to the field or a training for modelling in typed languages.