# Compositional Bounded Deducibility Security

This is a formalisation of the compositionality results for BD Security
presented in the paper

Thomas Bauereiss, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi.
CoSMeDis: A distributed social media platform with formally verified
confidentiality guarantees. In IEEE Symposium on Security and Privacy, pages
729–748, 2017. [[PDF](https://www.andreipopescu.uk/pdf/cosmedis-oakland.pdf)]

This formalisation imports the entry [Bounded Deducibility
Security](https://www.isa-afp.org/entries/Bounded_Deducibility_Security.html)
in the [Archive of Formal Proofs](https://www.isa-afp.org/).

This formalisation was written by Thomas Bauereiss and Andrei Popescu, and is
distributed under the [2-clause BSD licence](LICENSE).
