CoSMeDis: A confidentiality-verified distributed social media platform

Thomas Bauereiss 📧 and Andrei Popescu 🌐

August 16, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


This entry contains the confidentiality verification of the (functional kernel of) the CoSMeDis distributed social media platform presented in [1]. CoSMeDis is a multi-node extension the CoSMed prototype social media platform [2, 3, 4]. The confidentiality properties are formalized as instances of BD Security [5, 6]. The lifting of confidentiality properties from single nodes to the entire CoSMeDis network is performed using compositionality and transport theorems for BD Security, which are described in [1] and formalized in a separate AFP entry.


BSD License


Session CoSMeDis