### 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 latter operation is a process in which any event not shared by both operands can occur whenever the operand that admits the event can engage in it, whereas any event shared by both operands can occur just in case both can engage in it.

This paper formalizes Hoare's definition of concurrent composition and proves, in the general case of a possibly intransitive policy, that CSP noninterference security is conserved under this operation. This result, along with the previous analogous one concerning sequential composition, enables the construction of more and more complex processes enforcing noninterference security by composing, sequentially or concurrently, simpler secure processes, whose security can in turn be proven using either the definition of security, or unwinding theorems.

### License

BSD License

### Topics

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

### Session Noninterference_Concurrent_Composition

- ConcurrentComposition

### Depends on

- Conservation of CSP Noninterference Security under Sequential Composition

### Auto-related entries

- 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
- Reasoning about Lists via List Interleaving

## Cite

×

Noninterference_Concurrent_Composition-AFP

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