CoSMeDis: A confidentiality-verified distributed social media platform

 

Title: CoSMeDis: A confidentiality-verified distributed social media platform
Authors: Thomas Bauereiss (thomas /at/ bauereiss /dot/ name) and Andrei Popescu
Submission date: 2021-08-16
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.
BibTeX:
@article{CoSMeDis-AFP,
  author  = {Thomas Bauereiss and Andrei Popescu},
  title   = {CoSMeDis: A confidentiality-verified distributed social media platform},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2021,
  note    = {\url{https://isa-afp.org/entries/CoSMeDis.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: BD_Security_Compositional, Fresh_Identifiers