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