Integrity Analysis and Coercion in Distributed Systems

This thesis presents a new approach to modelling the security and integrity of data in distributed and ad-hoc networks of processes. An annotated type based analysis is introduced which ensures that no contamination will occur between data considered trustworthy and data that may have been corrupted.\ \ A method of performing safe run-time coercion of security properties of data is also presented. This is novel because it enables users to perform run-time coercions of data in a manner that may be statically proven safe.\ \ Both plain networks and dynamic (agent-based) networks are considered. These are modelled as systems of first-order and higher-order pi-calculus, respectively. The higher-order system examined introduces a new notion of trustworthiness dependent on the context in which it is typed or executed. This allows programs with malicious intent to be safely executed when it can be demonstrated that no possibility for interaction with other programs, including the host, is possible. A concept of execution context is introduced to perform this analysis.\ \ In addition, annotated type systems with and without sub-typing are described, and sub ject reduction is shown to hold for all systems considered.\ \ Implementation of the method is demonstrated via type-inference algorithms, and these are shown to be both sound and complete for all systems.