Matthew Hennessy - Information flow vs. resource access in the asynchronous pi-calculus

We propose an extension of the asynchronous picalculus in which a variety of security properties may be captured using types. These are an extension of the Input/Output types for the picalculus in which I/O capabilities are assigned specific security levels. We define a typing system which ensures that processes running at security level sigm cannot access resources with a security level higher than sigma. The notion of access control guaranteed by this system is formalized in terms of a Type Safety theorem. We then show that, for a certain class of processes, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behaviour can not be influenced by changes to high-level behaviour. This is formalized as a Non-Interference Theorem with respect to may testing.