University of Sussex
Browse

File(s) not publicly available

The Security Picalculus and Non-interference

journal contribution
posted on 2023-06-08, 07:54 authored by Matthew Hennessy
The security p-calculus is a typed version of the asynchronous p-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 p-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.

History

Publication status

  • Published

Journal

Journal of Logic and Algebraic Programming

ISSN

15678326

Publisher

Elsevier

Issue

1

Volume

63

Page range

3-34

Pages

32.0

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2012-02-06

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC