### Abstract

The definition of noninterference security for Communicating Sequential Processes requires to consider any possible future, i.e. any indefinitely long sequence of subsequent events and any indefinitely large set of refused events associated to that sequence, for each process trace. In order to render the verification of the security of a process more straightforward, there is a need of some sufficient condition for security such that just individual accepted and refused events, rather than unbounded sequences and sets of events, have to be considered.

Of course, if such a sufficient condition were necessary as well, it would be even more valuable, since it would permit to prove not only that a process is secure by verifying that the condition holds, but also that a process is not secure by verifying that the condition fails to hold.

This paper provides a necessary and sufficient condition for CSP noninterference security, which indeed requires to just consider individual accepted and refused events and applies to the general case of a possibly intransitive policy. This condition follows Rushby's output consistency for deterministic state machines with outputs, and has to be satisfied by a specific function mapping security domains into equivalence relations over process traces. The definition of this function makes use of an intransitive purge function following Rushby's one; hence the name given to the condition, Ipurge Unwinding Theorem.

Furthermore, in accordance with Hoare's formal definition of deterministic processes, it is shown that a process is deterministic just in case it is a trace set process, i.e. it may be identified by means of a trace set alone, matching the set of its traces, in place of a failures-divergences pair. Then, variants of the Ipurge Unwinding Theorem are proven for deterministic processes and trace set processes.

### License

BSD License

### Topics

- Computer science/Security

### Session Noninterference_Ipurge_Unwinding

- IpurgeUnwinding
- DeterministicProcesses

### Depends on

- Reasoning about Lists via List Interleaving
- Noninterference Security in Communicating Sequential Processes

### Used by

- Conservation of CSP Noninterference Security under Sequential Composition
- The Inductive Unwinding Theorem for CSP Noninterference Security
- The Generic Unwinding Theorem for CSP Noninterference Security

### Auto-related entries

- The Inductive Unwinding Theorem for CSP Noninterference Security
- The Generic Unwinding Theorem for CSP Noninterference Security
- Conservation of CSP Noninterference Security under Concurrent Composition
- Conservation of CSP Noninterference Security under Sequential Composition

## Cite

×

Noninterference_Ipurge_Unwinding-AFP

    @article{Noninterference_Ipurge_Unwinding-AFP,
      author  = {Pasquale Noce},
      title   = {The Ipurge Unwinding Theorem for CSP Noninterference Security},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Noninterference_Ipurge_Unwinding.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