### Abstract

This entry contains the confidentiality verification of the (functional kernel of) the CoSMed social media platform. The confidentiality properties are formalized as instances of BD Security [1, 2]. An innovation in the deployment of BD Security compared to previous work is the use of dynamic declassification triggers, incorporated as part of inductive bounds, for providing stronger guarantees that account for the repeated opening and closing of access windows. To further strengthen the confidentiality guarantees, we also prove "traceback" properties about the accessibility decisions affecting the information managed by the system.

### License

BSD License

### Topics

- Computer science/Security

### Session CoSMed

- Prelim
- System_Specification
- Automation_Setup
- Safety_Properties
- Observation_Setup
- Post_Intro
- Post_Value_Setup
- Post
- Friend_Intro
- Friend_Value_Setup
- Friend
- Friend_Request_Intro
- Friend_Request_Value_Setup
- Friend_Request
- Traceback_Intro
- Post_Visibility_Traceback
- Friend_Traceback

### Depends on

- Bounded-Deducibility Security
- Fresh identifiers

## Cite

×

CoSMed-AFP

    @article{CoSMed-AFP,
      author  = {Thomas Bauereiss and Andrei Popescu},
      title   = {CoSMed: A confidentiality-verified social media platform},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/CoSMed.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