Automated formal analysis of real-world privacy-friendly systems


Companies and other organisations collect and process increasing amounts of data about us. At the same time, data leaks of personal data are reported on a regular -almost daily- basis. These leaks can lead to, for example, identity theft, causing considerable personal stress and/or damages. Under the upcoming European General Data Protection Regulation (GDPR) these leaks can lead to hefty fines. The GDPR also introduces the requirement of applying the privacy by design paradigm. This all shows the need for privacy-friendly systems, which appear more and more. It is important to rigorously verify the privacy claims of these systems and, most critically, the protocols they use. Security protocols in general, which might not even take privacy into account yet, have already proven to be very error prone, both in design and implementation. A well-established research direction to verify the correctness of security protocols is that of automated protocol verification. For the analysis of privacy-friendly systems, however, this area is less mature.

The goal of this project is to develop techniques and tools to provide guarantees about real-world privacy-friendly systems. This is done by developing a framework to perform automated formal verification of privacy properties of the protocols used for realistic parameters. Until now, this has only been done for limited systems and parameters. The development will be guided based on two categories of privacy-friendly systems: attribute-based credential systems and homomorphic encryption-based systems. First, it will be defined what it means to provide privacy in these real-world applications. There are many definitions of privacy, and it is not always immediately clear what is meant exactly and how this should be verified. Next, techniques will be developed to verify the defined properties for realistic parameters, and, finally, they are applied to real-world scenarios to verify their privacy and anonymity claims.





Dr. ir. J.E.J. de Ruiter

Verbonden aan

Radboud Universiteit Nijmegen, Faculteit der Natuurwetenschappen, Wiskunde en Informatica, Institute for Computing and Information Science (ICIS)


Dr. ir. J.E.J. de Ruiter


01/01/2018 tot 31/12/2020