Formalising privacy policies in social networks

Abstract

Social Network Services (SNS) have changed the way people communicate, bringing many benefits but also new concerns. Privacy is one of them. We present a framework to write privacy policies for SNSs and to reason about such policies in the presence of events making the network evolve. The framework includes a model of SNSs, a logic to specify properties and to reason about the knowledge of the users (agents) of the SNS, and a formal language to write privacy policies. Agents are enhanced with a reasoning engine allowing the inference of knowledge from previously acquired knowledge. To describe the way SNSs may evolve, we provide operational semantics rules which are classified into four categories: epistemic, topological, policy, and hybrid, depending on whether the events under consideration change the knowledge of the SNS' users, the structure of the social graph, the privacy policies, or a combination of the above, respectively. We provide specific rules for describing Twitter's behaviour, and prove that it is privacy-preserving (i.e., that privacy is preserved under every possible event of the system). We also show how Twitter and Facebook are not privacy-preserving in the presence of additional natural privacy policies.