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