This web-site contains an overview and complementary material related to the paper

It details the following three aspects that were not developed in the paper because of space limitations:

  • EU DPD: the annotated text of the EU Data Protection Directive that allowed us to derive a formalization of the EU DPD used by the our automated compliance checking technique. By sharing this document, we aim to share with the community the choices underlying our formalization. Additionally, we allow people to comment on such choices in the forum section of this web-site by giving the possibility to leave comments and criticisms. Our hope is to improve our formalization through community feedback and build consensus on "our" interpretation of various aspects of the directive;
  • Guidelines: one of the result of our formalization of the EU DPD is a set of guidelines to help security experts to specify a bridge structure, i.e. the relationship between the high-level notions in the EU DPD (e.g., data subject, data controller, mandate) and the concrete notions used in the specification of the IT system under consideration. This is an important part of our approach aiming to simplify the legal compliance checks for security experts who are not usually legal experts;
  • Tool: it is possible to download the tool and the compliance problems used to perform an experimental evaluation that confirms the scalability and practical viability of the proposed approach (and allow for reproducing our experiments and results).

Our methodology for legal compliance checking is illustrated in the following diagram.

We start by considering the L-shaped (dashed) box at the top-left corner of the picture where legal and IT security experts collaborate to identify the parts of the regulation (in our case the EU DPD) that are amenable to formalization, elicit any simplifying assumptions restricting the scope of applicability of the rules, use a declarative approach to derive a mathematical model, and compile a set of guidelines (in natural language) that should help IT system designers to bridge the gap between the technical and legal levels. This process is time consuming, requires a lot of ingenuity and interdisciplinary skills but it is done once for each regulation of interest.

The rest of the diagram shows what an IT security expert (possibly complementing the designs of an IT system architect) should do in order to come up with a privacy-friendly IT system design. First of all, she produces a(decorated version) of the MSCs (Message Sequence Chart) describing the main processes in the system and associates each one of them with a purpose. Second, she designs the (concrete) access control policies that the various entities in the MSC should respect in order to send or receive messages. Third, by using the guidelines made available by the group of experts that produced the formal model of the regulation, she specifies the bridge structure in order to instantiate the (formal) model to the system under consideration. Afterwards, she can use the automated tool for security analysis and compliance checking to answer several questions about the system design: is this authorization query permitted or denied? Do the (concrete) access control policy enable the execution of the scenarios described by the MSCs in the design? And, most importantly for our work, is the (concrete) access control policy compliant with the (formalization of the) regulation? The results returned by tool can be used by the IT system expert to revise the system design or the bridge structure when security or compliance issues are detected.