# Compositional BD Security

 Title: Compositional BD Security Authors: Thomas Bauereiss (thomas /at/ bauereiss /dot/ name) and Andrei Popescu Submission date: 2021-08-16 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). BibTeX: @article{BD_Security_Compositional-AFP, author = {Thomas Bauereiss and Andrei Popescu}, title = {Compositional BD Security}, journal = {Archive of Formal Proofs}, month = aug, year = 2021, note = {\url{https://isa-afp.org/entries/BD_Security_Compositional.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Bounded_Deducibility_Security Used by: CoSMeDis Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.