A Formal Logic Framework for the Automation of the Right to Be Forgotten

  • Abhishek TiwariEmail author
  • Fabian Bendun
  • Christian Hammer
Conference paper
Part of the Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering book series (LNICST, volume 254)


The right to be forgotten results from a ruling of the European Court of Justice. It empowers individuals to control the display of their personal data indexed by a search engine. Specifically, it requires Internet search engine operators to deploy a process for individuals to file requests concerning the removal of their personal data from search indices.

To support the right to be forgotten, search engine operators such as Google, Microsoft and Yahoo currently provide a web form where users submit all relevant information. A subsequent manual process by the search engine operators assesses whether the author of the request is eligible to exercise the right to be forgotten and if the request itself is lawful. However, manual verification is inefficient, unscalable, and prone to subjective judgment. A framework for automated reasoning about case law (“PriCL”) could in principle tell whether some precedents lead to the conclusion that some action is legal or illegal. However, PriCL leverages first order logic, and hence, is insufficient to determine similarity of cases. In this paper, we design a framework that extends PriCL’s logic with similarity measures in order to automate the enforcement of the right to be forgotten. Our implementation of this logic leverages the Z3 theorem prover. We evaluate the framework by performing 10 case studies on the right to be forgotten. Each case was decided correctly in less than 1 s.


Formal language definitions Verification and validation Privacy protections 


  1. 1.
    Basin, D., Klaedtke, F., Samuel, M.: Monitoring security policies with metric first-order temporal logic. In: Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, pp. 23–34. No. 12 in SACMAT 2010. ACM, New York (2010)Google Scholar
  2. 2.
    Giblin, C., Liu, A.Y, Müller, S., Pfitzmann, B., Zhou, X.: Regulations expressed as logical models (REALM). In: 18th Annual Conference on Legal Knowledge and Information Systems (JURIX), pp. 37–48. IOS Press, Amsterdam (2005)Google Scholar
  3. 3.
    Garg, D., Jia, L., Datta, A.: A logical method for policy enforcement over evolving audit logs*. Technical report, CMU-CyLab-11-002 (2011)Google Scholar
  4. 4.
    Agirre, E., Cer, D., Diab, M., Gonzalez Agirre, A., Guo, W.: Semantic textual similarity, including a pilot on typed similarity. In: The Second Joint Conference on Lexical and Computational Semantics (2013)Google Scholar
  5. 5.
    Baader, F., Bauer, A., Lippmann, M.: Runtime verification using a temporal description logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 149–164. Springer, Heidelberg (2009). Scholar
  6. 6.
    Google: European privacy requests for search removals, January 2015.
  7. 7.
  8. 8.
  9. 9.
    DeYoung, H., Garg, D., Jia, L., Kaynar, D., Datta, A.: Experiences in the logical specification of the HIPAA and GLBA privacy laws. In: Proceedings of the 9th Annual ACM Workshop on Privacy in the Electronic Society (WPES), Chicago, Illinois, USA, pp. 12–20. ACM (2010)Google Scholar
  10. 10.
  11. 11.
    Finkel, J.R., Grenager, T., Manning, C.: Incorporating non-local information into information extraction systems by Gibbs sampling. In: Proceedings of the 43rd Annual Meeting of the Association for Computational Linguistics (ACL 2005), pp. 363–370. Association for Computational Linguistics, Stroudsburg (2005)Google Scholar
  12. 12.
    Argonne National Laboratory: Otter, August 2004.
  13. 13.
    Han, L., Kashyap, A., Finin, T., Mayfield, J., Weese, J.: UMBC EBIQUITY-CORE: semantic textual similarity systems. Technical report. University of Maryland (12)Google Scholar
  14. 14.
    Metzler, D., Dumais, S., Meek, C.: Similarity measures for short segments of text. In: Amati, G., Carpineto, C., Romano, G. (eds.) ECIR 2007. LNCS, vol. 4425, pp. 16–27. Springer, Heidelberg (2007). Scholar
  15. 15.
    Backes, M., Bendun, F., Hoffmann, J., Marnau, N.: PriCL: creating a precedent, a framework for reasoning about privacy case law. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 344–363. Springer, Heidelberg (2015). Scholar
  16. 16.
    Microsoft: Z3 prover, January 2017.
  17. 17.
    Simeonovski, M., Bendun, F., Asghar, M.R., Backes, M., Marnau, N., Druschel, P.: Oblivion: mitigating privacy leaks by controlling the discoverability of online information. CoRR abs/1506.06033, 01 July 2015Google Scholar
  18. 18.
    Schulz, S.: E theorem prover, July 2017.
  19. 19.
    Takale, S.A., Nandgaonkar, S.S.: Measuring semantic similarity between words using web search engines. In: Proceedings of the 16th International Conference on World Wide Web, pp. 757–766. ACM, New York (2007)Google Scholar
  20. 20.
    Dao, T.N, Simpson, T.: Wordnet-based semantic similarity measurement (2005). (1 Oct 2011)
  21. 21.
    Voronkov, A.: Vampire, July 2017.

Copyright information

© ICST Institute for Computer Sciences, Social Informatics and Telecommunications Engineering 2018

Authors and Affiliations

  • Abhishek Tiwari
    • 1
    Email author
  • Fabian Bendun
    • 2
  • Christian Hammer
    • 1
  1. 1.University of PotsdamPotsdamGermany
  2. 2.Saarland UniversitySaarlandGermany

Personalised recommendations