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.

Abstract

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.

License

BSD License

Topics

Session CoSMeDis

Depends on

Cite

× 
@article{CoSMeDis-AFP,
  author  = {Thomas Bauereiss and Andrei Popescu},
  title   = {CoSMeDis: A confidentiality-verified distributed social media platform},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/CoSMeDis.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: