### Abstract

In his outstanding work on Communicating Sequential Processes, Hoare has defined two fundamental binary operations allowing to compose the input processes into another, typically more complex, process: sequential composition and concurrent composition. Particularly, the output of the former operation is a process that initially behaves like the first operand, and then like the second operand once the execution of the first one has terminated successfully, as long as it does.

This paper formalizes Hoare's definition of sequential composition and proves, in the general case of a possibly intransitive policy, that CSP noninterference security is conserved under this operation, provided that successful termination cannot be affected by confidential events and cannot occur as an alternative to other events in the traces of the first operand. Both of these assumptions are shown, by means of counterexamples, to be necessary for the theorem to hold.

### License

BSD License

### Topics

- Computer science/Security
- Computer science/Concurrency/Process calculi

### Session Noninterference_Sequential_Composition

- Propaedeutics
- SequentialComposition
- Counterexamples

### Depends on

- The Ipurge Unwinding Theorem for CSP Noninterference Security

### Used by

- Conservation of CSP Noninterference Security under Concurrent Composition

### Auto-related entries

- Conservation of CSP Noninterference Security under Concurrent Composition
- The Generic Unwinding Theorem for CSP Noninterference Security
- Noninterference Security in Communicating Sequential Processes
- Algebra of Monotonic Boolean Transformers
- The Inductive Unwinding Theorem for CSP Noninterference Security

## Cite

×

Noninterference_Sequential_Composition-AFP

    @article{Noninterference_Sequential_Composition-AFP,
      author  = {Pasquale Noce},
      title   = {Conservation of CSP Noninterference Security under Sequential Composition},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Noninterference_Sequential_Composition.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
- Apr 26, 2016 : Isabelle2016