Description
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
asreceipt-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.
Team members
The following members are involved in the project:
Journals
Conference and Workshop Proceedings
-
Enforcing privacy in the presence of others: Notions, formalisations and relations.
Naipeng Dong, Hugo Jonker, andJun Pang.
In Proc. 18th European Symposium on Research in Computer Security - ESORICS'13,
Lecture Notes in Computer Science 8134, pp. 499-516.
Springer-Verlag, 2013.
-
Formal analysis of privacy in an eHealth protocol.
Naipeng Dong, Hugo Jonker, and Jun Pang.
In Proc. 17th European Symposium on Research in Computer Security - ESORICS'12,
Lecture Notes in Computer Science 7459, pp. 325-342.
Springer-Verlag, 2012.
-
Challenges in eHealth: from enabling to enforcing privacy.
Naipeng Dong, Hugo Jonker, and Jun Pang.
In Proc. 1st Symposium on Foundations of Health Information Engineering and Systems - FHIES'11,
Lecture Notes in Computer Science 7151, pp. 195-206. Springer-Verlag, 2012.
-
Analysis of a receipt-free auction protocol in the applied pi calculus.
Naipeng Dong, Hugo Jonker, and Jun Pang.
In Proc. 7th Workshop on Formal Aspects in Security and Trust - FAST'10,
Lecture Notes in Computer Science 6561, pp. 223-238. Springer-Verlag, 2011.
-
Bulletin boards in voting systems: Modelling and measuring privacy.
Hugo Jonker and Jun Pang.
In Proc. 6th Conference on Availability, Reliability and Security - ARES'11,
pp. 294-300. IEEE Computer Society, 2011.
-
Measuring voter-controlled privacy.
Hugo Jonker, Sjouke Mauw, and Jun Pang.
In Proc. 4th Conference on Availability, Reliability and Security - ARES'09,
pp. 289-298. IEEE Computer Society, 2009.
Technical reports
-
Formal analysis of a receipt-free auction protocol in applied pi.
Naipeng Dong, Hugo Jonker, and Jun Pang.
Technical report, University of Luxembourg, 2015.
[Original ProVerif model] [Revised ProVerif model]
-
Formal Analysis of an eHealth Protocol.
Naipeng Dong, Hugo Jonker, and Jun Pang.
Technical report, University of Luxembourg, 2012.
[ProVerif model]
-
Enforcing Privacy in the Presence of Others: Notions, Formalisations and Relations.
Naipeng Dong, Hugo Jonker, and Jun Pang.
Technical report, University of Luxembourg, 2013.
Financial support
The project is supported by the University of Luxembourg and the
National Research Fund Luxembourg.