### 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

- Computer science/Security

### Session CoSMeDis

- Prelim
- System_Specification
- API_Network
- Automation_Setup
- Safety_Properties
- Post_Intro
- Post_Observation_Setup_ISSUER
- Post_Unwinding_Helper_ISSUER
- Post_Value_Setup_ISSUER
- Post_ISSUER
- Post_Observation_Setup_RECEIVER
- Post_Unwinding_Helper_RECEIVER
- Post_Value_Setup_RECEIVER
- Post_RECEIVER
- Post_COMPOSE2
- Post_Network
- DYNAMIC_Post_Value_Setup_ISSUER
- DYNAMIC_Post_ISSUER
- DYNAMIC_Post_COMPOSE2
- DYNAMIC_Post_Network
- Independent_Post_Observation_Setup_ISSUER
- Independent_DYNAMIC_Post_Value_Setup_ISSUER
- Independent_DYNAMIC_Post_ISSUER
- Independent_Post_Observation_Setup_RECEIVER
- Independent_Post_Value_Setup_RECEIVER
- Independent_Post_RECEIVER
- Independent_DYNAMIC_Post_Network
- Independent_Posts_Network
- Post_All
- Friend_Intro
- Friend_Observation_Setup
- Friend_State_Indistinguishability
- Friend_Openness
- Friend_Value_Setup
- Friend
- Friend_Network
- Friend_All
- Friend_Request_Intro
- Friend_Request_Value_Setup
- Friend_Request
- Friend_Request_Network
- Friend_Request_All
- Outer_Friend_Intro
- Outer_Friend
- Outer_Friend_Issuer_Observation_Setup
- Outer_Friend_Issuer_State_Indistinguishability
- Outer_Friend_Issuer_Openness
- Outer_Friend_Issuer_Value_Setup
- Outer_Friend_Issuer
- Outer_Friend_Receiver_Observation_Setup
- Outer_Friend_Receiver_State_Indistinguishability
- Outer_Friend_Receiver_Value_Setup
- Outer_Friend_Receiver
- Outer_Friend_Network
- Outer_Friend_All

### Depends on

- Compositional BD Security
- Fresh identifiers

### Auto-related entries

- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part I
- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part II

## Cite

×

CoSMeDis-AFP

    @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:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1