Non-interference via Typing in the Security Pi-calculus

Matthew Hennessy

University of Sussex

Abstract:
The security pi-calculus is a typed version of the asynchronous pi-calculus in which the types, in addition to constraining the input/output behaviour of processes, have security levels associated with them. This enables us to introduce a range of typing disciplines which allow input or output behaviour, or both, to be bounded above or below by a given security level. This in turn allows us to formalise the notions of ``high-level'' and ``low-level'' users.

Within this framework we discuss the formalisation of ``non-interference'' which dictates, intuitively, that the behaviour of low-level processes should be independent of that of high-level processes. We demonstrate that this is very dependent on the precise formulation of the notion of ``behaviour''. We show that our type system automatically enforces non-interference relative to may testing equivalence; a restricted set of types is required for must testing equivalence.

Reference: The Security Pi-calculus and Non-interference, Sussex Technical Report 2000:05.

Back to schedule.


Marieke Huisman
Last modified: Thu Nov 9 16:01:28 MET 2000