A Formal Approach to Enforced Privacy

PhD Vacancy in Security

The project

Privacy has been a fundamental property for distributed systems which provide e-services to users. In these systems, users become more and more concerned about their anonymity and how their personal information has been used. For example, in voting systems a voter wants to keep her vote secret. Recently, strong privacy properties in voting such as receipt-freeness and coercion-resistance were proposed and have received considerable attention. These notions seek to prevent vote buying (where a voter chooses to renounce her vote). These strong notions of privacy, which we will call enforced privacy, actually capture the essential idea that privacy must be enforced by a system upon its users, instead of users desiring privacy.

The first aim of this project is to extend enforced privacy from voting to other domains, such as online auctions, anonymous communications, healthcare, and digital rights management, where enforced privacy is a paramount requirement. For example, in healthcare, a patient's health record is private information. However, a patient contracting a serious disease is at risk of discrimination by parties aware of her illness. The inability to unveil (specific parts of) the health record of a patient is a minimal requirement for her privacy.

The second aim of the project is to develop a domain-independent formal framework in which enforced privacy properties in different domains can be captured in a natural, uniform and precise way. Typically, enforced privacy properties will be formalised as equivalence relations on traces, which take into account both the knowledge of the intruder and the users. Within the framework, algorithms can be designed to support analysis of e-service systems which claim to have enforced privacy properties. In the end, the formalisation and techniques will be applied to verify existing real-life systems and to help the design of new systems with enforced privacy properties.


We are looking for candidates with a strong interest in formal verification and privacy. Possible topics include:

Profile for the PhD student position:


The tasks for the PhD student will be to

Appointment and Salary

The PhD student will be employed for a period of 3 years (40 hrs/week), with a possible extension of 1 year. Prof. Dr. Sjouke Mauw will act as supervisor.

The PhD student will be appointed by the University of Luxembourg, and shall start in the first half of 2009.

The remuneration for the PhD position is around 24.000 EUR/year netto. (Note: This figures are meant as an indication and may vary according to personal circumstances.)


For inquiries about the project or the positions, please contact Prof. Dr. Sjouke Mauw (sjouke.mauw@uni.lu, +352 466 644 5480) or Dr. Jun Pang (jun.pang@uni.lu, +352 466 644 5625).


Interested parties are invited to send an application in PDF format to sjouke.mauw@uni.lu and jun.pang@uni.lu. The application should consist of the following documents:

The deadline for application is Feb 20, 2009.

Your application needs to include the relevant job reference number F1R-CSC-AFR-0804 for the PhD student position.