Abstract
We present an epistemic logic equipped with time-stamps in atoms and epistemic operators, which enables reasoning about the moments at which events happen and knowledge is acquired or deduced. Our logic includes both an epistemic operator K and a belief operator B, to capture the disclosure of inaccurate information. Our main motivation is to describe rich privacy policies in online social networks (OSNs). Most of today’s privacy policy mechanisms in existing OSNs allow only static policies. In our logic it is possible to express rich dynamic policies in terms of the knowledge available to the different users and the precise time of actions and deductions. Our framework can be instantiated for different OSNs by specifying the effect of the actions in the evolution of the social network and in the knowledge disclosed to each user. We present an algorithm for deducing knowledge and propagating beliefs, which can also be instantiated with different variants of how the epistemic information is preserved through time. Policies are modelled as formulae in the logic, which are interpreted over timed traces. Finally, we show that the model checking problem for this logic, and in consequence policy conformance, is decidable.
This research has been partially supported by: the Swedish funding agency SSF under the grant Data Driven Secure Business Intelligence, the Swedish Research Council (Vetenskapsrådet) under grant Nr. 2015-04154 (PolUser: Rich User-Controlled Privacy Policies), the EU H2020 project Elastest (num. 731535), by the Spanish MINECO Project “RISCO (TIN2015-71819-P)” and by the EU ICT COST Action IC1402 ARVI (Runtime Verification beyond Monitoring).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
We can assume that the predecessor of the initial time-stamp is the intial state itself, and similarly the next of the end of the trace returns the equal to itself.
- 2.
For readability we omit \( occurred ^{15}(\mathsf {enter}(B^{15}_{ Alice } loc ^{15}( Bob , work )))\) in Fig. 1 which is included in \( EKB ^{\sigma [15]}_{ Alice }\).
References
Lenhart, A., Purcell, K., Smith, A., Zickuhr, K.: Social media & mobile internet use among teens and young adults. Millennials. Pew Internet & American Life Project (2010)
Madejski, M., Johnson, M., Bellovin, S.: A study of privacy settings errors in an online social network. In: PERCOM Workshops 2012, pp. 340–345. IEEE (2012)
Johnson, M., Egelman, S., Bellovin, S.M.: Facebook and privacy: it’s complicated. In: SOUPS 2012, pp. 9:1–9:15. ACM (2012)
Liu, Y., Gummadi, K.P., Krishnamurthy, B., Mislove, A.: Analyzing facebook privacy settings: user expectations vs. reality. In: IMC 2011, pp. 61–70. ACM (2011)
Madejski, M., Johnson, M.L., Bellovin, S.M.: The failure of online social network privacy settings. Technical report, Columbia University (2011)
Pardo, R., Kellyérová, I., Sánchez, C., Schneider, G.: Specification of evolving privacy policies for online social networks. In: TIME 2016, pp. 70–79. IEEE (2016)
The Guardian: As fake news takes over Facebook feeds, many are taking satire as fact. www.theguardian.com/media/2016/nov/17/facebook-fake-news-satire. Accessed 20 Oct 2017
The Guardian: How to solve Facebook’s fake news problem: experts pitch their ideas. www.theguardian.com/technology/2016/nov/29/facebook-fake-news-problem-experts-pitch-ideas-algorithms. Accessed 20 Oct 2017
The Guardian: Obama is worried about fake news on social media-and we should be too. www.theguardian.com/media/2016/nov/20/barack-obama-facebook-fake-news-problem. Accessed 20 Oct 2017
van Zee, M., Doder, D., Dastani, M., van der Torre, L.W.N.: AGM revision of beliefs about action and time. In: IJCAI 2015, pp. 3250–3256. AAAI Press (2015)
Xiong, Z., Ågotnes, T., Seligman, J., Zhu, R.: Towards a logic of tweeting. In: Baltag, A., Seligman, J., Yamada, T. (eds.) LORI 2017. LNCS, vol. 10455, pp. 49–64. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-55665-8_4
Halpern, J.Y., Samet, D., Segev, E.: Defining knowledge in terms of belief: the modal logic perspective. Rev. Symbolic Logic 2, 469–487 (2009)
Fong, P.W.: Relationship-based access control: Protection model and policy language. In: CODASPY 2011, pp. 191–202. ACM (2011)
Bruns, G., Fong, P.W., Siahaan, I., Huth, M.: Relationship-based access control: its expression and enforcement through hybrid logic. In: CODASPY 2012, pp. 117–124. ACM (2012)
Pardo, R., Balliu, M., Schneider, G.: Formalising privacy policies in social networks. J. Logical Algebraic Methods Program. 90, 125–157 (2017)
Snodgrass, R., Ahn, I.: Temporal databases. Computer 19(9), 35–42 (1986)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge, vol. 4. MIT press Cambridge, Cambridge (2003)
Erciyes, K.: Complex Networks: An Algorithmic Perspective, 1st edn. CRC Press Inc., Boca Raton (2014)
FlockDB: A distributed fault-tolerant graph database. github.com/twitter/flockdb. Accessed 20 Oct 2017
Bronson, N., Amsden, Z., Cabrera, G., Chakka, P., Dimov, P., Ding, H., Ferris, J., Giardullo, A., Kulkarni, S., Li, H., Marchukov, M., Petrov, D., Puzar, L., Song, Y.J., Venkataramani, V.: Tao: Facebook’s distributed data store for the social graph. In: ATC 2013, pp. 49–60 (2013)
Neo4j decreases development time-to-market for LinkedIn’s Chitu App. neo4j.com/case-studies/linkedin-china/. Accessed 20 Oct 2017
Pardo, R., Sánchez, C., Schneider, G.: Timed Epistemic Knowledge Bases for Social Networks (Extended Version). ArXiv e-prints (2017)
Ben-Zvi, I., Moses, Y.: Agent-time epistemics and coordination. In: Lodaya, K. (ed.) ICLA 2013. LNCS, vol. 7750, pp. 97–108. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36039-8_9
Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 378–392. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10431-7_30
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Pardo, R., Sánchez, C., Schneider, G. (2018). Timed Epistemic Knowledge Bases for Social Networks. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-95582-7_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-95581-0
Online ISBN: 978-3-319-95582-7
eBook Packages: Computer ScienceComputer Science (R0)