### Abstract

The necessary and sufficient condition for CSP noninterference security stated by the Ipurge Unwinding Theorem is expressed in terms of a pair of event lists varying over the set of process traces. This does not render it suitable for the subsequent application of rule induction in the case of a process defined inductively, since rule induction may rather be applied to a single variable ranging over an inductively defined set.

Starting from the Ipurge Unwinding Theorem, this paper derives a necessary and sufficient condition for CSP noninterference security that involves a single event list varying over the set of process traces, and is thus suitable for rule induction; hence its name, Inductive Unwinding Theorem. Similarly to the Ipurge Unwinding Theorem, the new theorem only requires to consider individual accepted and refused events for each process trace, and applies to the general case of a possibly intransitive noninterference policy. Specific variants of this theorem are additionally proven for deterministic processes and trace set processes.

### License

BSD License

### Topics

- Computer science/Security

### Session Noninterference_Inductive_Unwinding

- InductiveUnwinding

### Depends on

- The Ipurge Unwinding Theorem for CSP Noninterference Security

### Auto-related entries

- The Generic Unwinding Theorem for CSP Noninterference Security
- Noninterference Security in Communicating Sequential Processes
- Conservation of CSP Noninterference Security under Concurrent Composition
- Conservation of CSP Noninterference Security under Sequential Composition

## Cite

×

Noninterference_Inductive_Unwinding-AFP

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