The Security Picalculus and Non-interference.
Citation:
Hennessy, Matthew., The Security Picalculus and Non-interference., Journal of Logic and Algebraic Programming, 63, 1, 2005, 3-34Download Item:
security.pdf (Published (author's copy) - Peer Reviewed) 349.7Kb
Abstract:
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, assuming the observer is constrained by a given
typing environment.
Using these alternative characterisations we prove non-interference results with
respect to may and must testing. These show that information flow between security
levels can be controlled using our typing systems.
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Publisher:
ElsevierType of material:
Journal ArticleSeries/Report no:
Journal of Logic and Algebraic Programming;63;
1;
Availability:
Full text availableLicences: