### Abstract

Building on a previous AFP entry that formalizes the Bounded-Deducibility Security (BD Security) framework [1], we formalize compositionality and transport theorems for information flow security. These results allow lifting BD Security properties from individual components specified as transition systems, to a composition of systems specified as communicating products of transition systems. The underlying ideas of these results are presented in the papers [1] and [2]. The latter paper also describes a major case study where these results have been used: on verifying the CoSMeDis distributed social media platform (itself formalized as an AFP entry that builds on this entry).

### License

BSD License

### Topics

- Computer science/Security

### Session BD_Security_Compositional

- Composing_Security
- Trivial_Security
- Transporting_Security
- Composing_Security_Network
- Independent_Secrets

### Depends on

- Bounded-Deducibility Security

### Used by

- CoSMeDis: A confidentiality-verified distributed social media platform

### Auto-related entries

- A Verified Efficient Implementation of the Weighted Path Order
- Formalization of CommCSL: A Relational Concurrent Separation Logic for Proving Information Flow Security in Concurrent Programs
- The Hales–Jewett Theorem
- Irrational numbers from THE BOOK
- The Safely Composable DOM

## Cite

×

BD_Security_Compositional-AFP

    @article{BD_Security_Compositional-AFP,
      author  = {Thomas Bauereiss and Andrei Popescu},
      title   = {Compositional BD Security},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/BD_Security_Compositional.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