### Abstract

An extension of classical noninterference security for deterministic state machines, as introduced by Goguen and Meseguer and elegantly formalized by Rushby, to nondeterministic systems should satisfy two fundamental requirements: it should be based on a mathematically precise theory of nondeterminism, and should be equivalent to (or at least not weaker than) the classical notion in the degenerate deterministic case.

This paper proposes a definition of noninterference security applying to Hoare's Communicating Sequential Processes (CSP) in the general case of a possibly intransitive noninterference policy, and proves the equivalence of this security property to classical noninterference security for processes representing deterministic state machines.

Furthermore, McCullough's generalized noninterference security is shown to be weaker than both the proposed notion of CSP noninterference security for a generic process, and classical noninterference security for processes representing deterministic state machines. This renders CSP noninterference security preferable as an extension of classical noninterference security to nondeterministic systems.

### License

BSD License

### Topics

- Computer science/Security

### Session Noninterference_CSP

- CSPNoninterference
- ClassicalNoninterference
- GeneralizedNoninterference

### Used by

- The Ipurge Unwinding Theorem for CSP Noninterference Security

## Cite

×

Noninterference_CSP-AFP

    @article{Noninterference_CSP-AFP,
      author  = {Pasquale Noce},
      title   = {Noninterference Security in Communicating Sequential Processes},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Noninterference_CSP.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- Jun 13, 2015 : Isabelle2015
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- May 24, 2014 : Isabelle2013-2