https://www.mdu.se/

Social network users control the flow of information through their privacy settings. Such privacy settings specify the possibility of interaction or the visibility of each user’s activity to other users. We extend the Rebeca language with 1) annotations for specifying the user’s privacy policies on send and receive message actions, and 2) conditional statement on the knowledge of actors. The annotation of a send message statement identifies possible observers while the annotation of a message server defines the possible senders of that message. Rebecs perceive knowledge by observing messages and they can react accordingly. By integrating epistemic logic into conditional statements, we can model the behaviors influenced by the knowledge of an actor. We define the semantics in terms of labeled transition systems enriched by indistinguishability relations, called Social Network Semantic Model (SNSM). This semantic model addresses both operational and epistemic aspects of social networks which enables us to find scenarios leading to private data disclosure using model checking. We illustrate the applicability of our approach through a simple case study on Instagram.