The Security Picalculus and Non-interference

Hennessy, Matthew (2004) The Security Picalculus and Non-interference. Journal of Logic and Algebraic Programming, 63 (1). pp. 3-34. ISSN 15678326

Full text not available from this repository.


The security π-calculus is a typed version of the asynchronous π-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.

We define typed versions of may and must equivalences for the security π-calculus, where the tests are parameterised relative to a security level. We provide alternative characterisations of these equivalences in terms of actions in context; these describe the actions a process may perform in a given typing environment, assuming the observer is constrained by a related, but possibly different, environment.

The paper also contains non-interference results with respect to may and must testing. These show that certain form of non-interference can be enforced using our typing systems.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Depositing User: Matthew Hennessy
Date Deposited: 06 Feb 2012 20:48
Last Modified: 13 Jun 2012 14:13
📧 Request an update