A richer policy language for GDPR compliance Piero A. Bonatti1 , Iliana M. Petrova2 , and Luigi Sauro1 1 Università degli studi di Napoli Federico II 2 CeRICT Abstract. We illustrate an OWL2 fragment properly tailored for the specifica- tion of both companies’ data protection policies and data subjects’ consent to data processing. Assessing a company’s policy for compliance with data subjects’ consent is then reduced to a subsumption checking. We provide a complete sub- sumption algorithm which combines tableaux-based and structural-subsumption techniques and show that, under some conditions, it performs in polynomial time. 1 Introduction The European General Data Protection Regulation3 (GDPR) places tight restrictions on the processing of personal data and establishes substantial administrative fines to discourage infringements. Since collecting and processing personal data is a paramount source of innovation and revenue, data controllers (i.e. the personal and legal entities that process personal data) are interested in maximizing personal data usage within the limits posed by the GDPR. The European H2020 project SPECIAL4 is aimed at supporting controllers with methodological and technological means to comply with the GDPR requirements ef- ficiently and safely. Compliance checking plays a crucial role in this picture: first, the data usage policies of the industrial partners must be compared with a (partial) formal- ization of the GDPR itself. Second, in the absence of a legitimate legal basis5 , personal data cannot be stored or processed, even temporarily, without the explicit consent of the data subjects. As the number of data subjects (and their policies) can be as large as the number of customers of a major communication service provider, some of the project’s use cases consist in checking storage permissions against a stream of incom- ing data points, at the rate of hundreds of thousands per minute. Thus, a crucial tasks is the development of scalable reasoning procedures for compliance checking. Here, we focus on PL, that is, the SPECIAL’s approach to the representation of data usage activities, consent to data processing, and selected parts of the GDPR. PL is a DL 3 http://data.consilium.europa.eu/doc/document/ ST-5419-2016-INIT/en/pdf 4 https://www.specialprivacy.eu/ 5 Such legal bases include public interest, the vital interests of the data subject, signed contracts, and the legitimate interests of the data controller, just to name a few (cf. GDPR Art. 6). How- ever, the regulation constrains the applicability of these legal bases with a number of provisos and caveats as the data minimization principle introduced in Art. 5, and the limitations to the legitimate interests of the controller rooted in Art. 6.1(f). 2 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro fragment specifically designed to balance expressiveness requirements to encode data usage policies and scalability of reasoning. A first formalization has been presented in [5]. In this paper, we describe an extention, PL+ , that overcomes some limitations of expressiveness that arose from a further in-depth analysis of the GDPR on one side, and the policy specifications of the industrial partners involved in the project on the other. More precisely, PL+ enhances PL in the following aspects: – it extends PL by including role domains in the ontology language and role chain agreements (R1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm ) in the query language; – it relies on a new subsumption checking algorithm that combines tableaux-based and structural subsumption reasoning techniques. This algorithm is notably simpler than the one presented in [5] and hence we expect it to perform faster. Thereafter, we focus on the technical aspects of PL+ referring to [5] for further moti- vations and examples. 2 Preliminaries PL+ is tailored to formalize policies regulating the usage of personal data. It can ex- press (i) the policies of data controllers (i.e. the organizations that collect and process personal data), (ii) the selective consent to data usage issued by data subjects, and (iii) parts of the GDPR related to consent management, user rights, and data transfer. The aspects of data usage that have legal relevance are clearly indicated in several articles of the GDPR. In particular, the main properties of a usage policy that need to be encoded and archived include: – reasons for data processing (purpose); – which data categories are involved; – what kind of processing is applied to the data; – which third parties data are distributed to (recipients); – countries in which the data will be stored (location); – time limits for data erasure (duration). Here we focus only on the technical aspects needed in this work and refer the reader to [3] for further details. The PL+ language is built from countably infinite and mutually disjoint sets of concept names (NC ), role names (NR ) and concrete feature names (NF ). An interpretation I is a structure I = (∆I , ·I ) where ∆I is a nonempty set, and the interpretation function ·I , defined over the signature Σ = NC ∪ NR ∪ NF , is s.t. (i) AI ⊆ ∆I if A ∈ NC ; (ii) RI ⊆ ∆I × ∆I if R ∈ NR ; (iii) f I ⊆ ∆I × N if f ∈ NF , where N is the set of natural numbers. A pointed interpretation is a pair I, d where I is an interpretation and d is an element of the domain ∆I . A PL+ knowledge base KB is a finite set of axioms of the form func(f ), func(R), dom(R, A), ran(R, A), disj(A, B), and A v B, where A and B are concept names, R is a role name, and f denotes a concrete feature. An interpretation I satisfies an axiom α if I satisfies the corresponding semantic condition in Figure 1. Figure 2 shows the syntax and semantics of PL+ operators which allow to de- fine query concepts. We say that a concept is simple if no disjunction occurs in it. By applying the logical equivalences C1 u (C2 t C3 ) ≡ (C1 u C2 ) t (C1 u C3 ) and A richer policy language for GDPR compliance 3 Name Syntax Semantics GCI AvB AI ⊆ B I disj disj(A, B) AI ∩ B I = ∅ role functionality func(R) RI is a partial function concr. feature functionality func(f ) f I is a partial function domain dom(R, A) RI ⊆ AI × ∆I range ran(R, A) RI ⊆ ∆I × AI Fig. 1. Syntax and semantics of PL+ axioms. ∃R.(C1 t C2 ) ≡ ∃R.C1 t ∃R.C2 any concept C can be reduced in a normal form C1 t · · · t Cn where each Ci is simple (clearly, the normal form can be exponentially longer than C). A pointed interpretation satisfies a concept C, formally I, d |= C, iff d ∈ C I . Then, I satisfies C in case I, d |= C for some d ∈ ∆I . As usual, KB |= C v D means that C I ⊆ DI , for all models I of KB . Example 1. A company – call it BeFit – sells a wearable fitness appliance and wants to process biometric data (stored in the EU) for sending health-related advice to a cus- tomer. Furthermore, BeFit wants to share the customer’s location data with a group of enterprises (located in the USA) engaged in a joint economic activity. According to Art. 47 of the GDPR, the transfer of personal data outside of EU is allowed towards recipients that enforce, so-called, binding corporate rules. Location data are kept for a minimum of one year but no longer than 5; biometric data are kept for an unspecified amount of time. In order to do all this legally, BeFit needs consent from its customers. The consent BeFit acquires from a customer may look as follows: (∃purpose.F itnessRecommendation u ∃data.BiometricData u ∃processing.Analytics u ∃recipient.BeF it u ∃store.∃location.EU ) t (∃purpose.M onetize u ∃data.LocationData u ∃processing.T ransf er u ∃recipient.U SEnterpriseGroup u ∃store.(∃location.U SA u duration : [1, 5]) u (controller ◦ applyBindingCorporateRulesT o = recipient) u ∃controller.BeF it) , where integers represent years. Moreover, KB can include the following axioms: HeartRate v BiometricData ComputeAvg v Analytics f unc(recipient) Given the knowledge base, the first disjunct of the above consent allows BeFit to compute the average heart rate of the data subject in order to send her fitness rec- ommendations. The purpose could be further detailed by saying how the data sub- ject is contacted, e.g. “recommendation via SMS”. Then, in the customer’s consent 4 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro Name Syntax Semantics bottom ⊥ ⊥I = ∅ conjunction C uD (C u D)I = C I ∩ DI disjunction C tD (C t D)I = C I ∪ DI existential ∃R.C {d ∈ ∆I | ∃(d, e) ∈ RI : e ∈ C I } restriction concrete f : [l, u] {d ∈∆I | ∃w ∈ N s.t. (d, w) ∈ f I and l ≤ constraint w ≤ u) existential chain (R1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm ) {d ∈ ∆I | ∃d¯ s.t. (d, d) ¯ ∈ (R1 ◦ · · · ◦ restriction Rn ) ∩ (S1 ◦ · · · ◦ Sm )I } I Fig. 2. Syntax and semantics of PL+ (query) concepts. ∃purpose.F itnessRecommendation should be replaced with something like ∃purpose.(F itnessRecommendation u ∃contact.SMS) . Note also that, since recipient is a functional role, the chain agreement in the second disjunct imposes to the recipient the application of the controller’s binding corporate rules. t u An Abox A is a finite set of assertions of the form C(x) and R(x, y), where R is a role name, C is a simple query concept, and x and y belong to a countably infinite set of variable names VR. In particular, we assume that VR contains a distinguished variable x0 . An assignment π : VR → ∆I interprets all variables in VR as elements of an interpretation I. Let VRA ⊆ VR be the set of variable names occurring in A, we say that π and π 0 agree in A if π(x) = π 0 (x), for all x ∈ VRA . Then, a pair I, π satisfies an Abox A (formally, I, π |= A) iff (i) π(x) ∈ C I , for all C(x) ∈ A, and (ii) (π(x), π(y)) ∈ RI , for all R(x, y) ∈ A. A pointed interpretation I, d satisfies A (formally, I, d |= A) if I, π |= A for some assignment π with π(x0 ) = d. We write KB , A |= C(x) meaning that I, π |= A implies I, π |= C(x), for all models I |= KB and assignments π. Finally, we say that C (resp. A) and D are interval safe iff for all constraints f : [l, u] occurring in C (resp. for all f : [l, u] s.t. f : [l, u](x) ∈ A, for some variable x) and f : [l0 , u0 ] occurring in D, either [l, u] ⊆ [l0 , u0 ], or [l, u] ∩ [l0 , u0 ] = ∅. 3 The subsumption algorithm Checking whether KB |= C v D is performed in three phases. The first phase pre- processes the concept C. First of all, for each f : [l, u] in C, let x1 < x2 < · · · < xr be the integers that occur as interval endpoints in sub-concept f : [l0 , u0 ] of D and belong to [l, u]. Let x0 = ` and xr+1 = u and replace f [l, u] with the equivalent concept r G  f : [xi , xi ] t f : [xi + 1, xi+1 − 1] t f : [xr+1 , xr+1 ]. (1) i=0 Doing so, we ensure that C and D are interval safe. Then, C is translated in the corre- sponding normal form C1 t · · · t Cn . As a consequence, a knowledge base KB entails A richer policy language for GDPR compliance 5 Rule →u if 1. C1 u C2 (x) ∈ A and 2. {C1 (x), C2 (x)} 6⊆ A, then set A0 ← A ∪ {C1 (x), C2 (x)} Rule →v if 1. A(x) ∈ A and 2. A v B ∈ KB , and 3. B(x) 6∈ A then set A0 ← A ∪ {B(x)} Rule →∃ if 1. ∃R.C(x) ∈ A and 2. for no y {R(x, y), C(y)} ⊆ A then create a new variable ynew and set A0 ← A ∪ {R(x, ynew ), C(ynew )} Rule →dom if 1. R(x, y) ∈ A and 2. dom(R, A) ∈ KB , and 3. A(x) 6∈ A, then set A0 ← A ∪ {A(x)} Rule →ran if 1. R(x, y) ∈ A and 2. ran(R, A) ∈ KB , and 3. A(y) 6∈ A then set A0 ← A ∪ {A(y)} Rule →func(R) if 1. {R(x, y), R(x, z)} ⊆ A and 2. func(R) ∈ KB then set A0 ← A[y/z] Rule →func(f ) if 1. {f : [l, u](x), f : [v, w](x)} ⊆ A and 2. func(f ) ∈ KB then set A0 ← A ∪ {f : [max(l, v), min(u, w)]} Rule →= if 1. (R1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm )(x) ∈ A, and 2. there does not exist y1 , . . . , yn−1 , z1 , . . . , zm−1 , ȳ s.t. {R1 (x, y1 ), S1 (x, z1 )} ⊆ A, Ri (yi−1 , yi ) ∈ A, for i = 1, . . . , n − 1, Sj (zj−1 , zj ) ∈ A, for j = 1, . . . , m − 1, {Rn (yn−1 , ȳ), Sm (zm−1 , ȳ} ⊆ A then create new variables y1new , . . . , yn−1 new , z1new , . . . , zm−1 new , ȳ new and 0 new new new set A ← A ∪ {R1 (x, y1 ), . . . , Rn (yn−1 , ȳ )} ∪ {S1 (x, z1new ), . . . , Sm (zm−1 new , ȳ new )} Rule →disj if 1. {A(x), B(x)} ⊆ A and 2. disj(A, B) ∈ KB then set A0 ← A ∪ {⊥(x)} Rule →f⊥ if 1. f : [l, u](x) ∈ A and 2. u < l then set A0 ← A ∪ {⊥(x)} Fig. 3. PL+ tableaux rules C v D iff KB |= Ci v D, for all i = 1, . . . , n6 . After the preprocessing phase, the subsumption problem is reduced to checking whether each simple concept Ci is subsumed by D. For a simple concept Ci , during the second phase, an Abox A0 is first initialised with a Ci (x0 ) and then expanded by exhaustively applying the tableaux rules in Figure 3. The subsumption vacuously holds if the resulting Abox A contains assertions of the form ⊥(x) for some x. In contrary case, the third phase checks whether x0 ∈ hhDiiA , where hhDiiA is the set of variable names contained in VRA inductively defined as follows: 6 Note that, differently from the subsumption algorithm presented in [5], D is not normalized. This may significantly impact on performance since the normalization process might exponen- tially inflate D. 6 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro hhAiiA={x ∈ VRA | A(x) ∈ A} hhD1 u D2 iiA={x ∈ VRA | x ∈ hhD1 iiA ∩ hhD2 iiA } hhD1 t D2 iiA={x ∈ VRA | x ∈ hhD1 iiA ∪ hhD2 iiA } hh∃R.DiiA={x ∈ VRA | ∃y ∈ VRA s.t. R(x, y) ∈ A and y ∈ hhDiiA } hhR1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm iiA={x ∈ VRA | ∃(y, z) ∈ VR2A s.t. (y, z) ∈ hhRn , Sm iiA and x ∈ hhR1 ◦ · · · ◦ Rn−1 , yiiA and x ∈ hhS1 ◦ · · · ◦ Sm−1 , ziiA } hhR, SiiA={(y, z) ∈ VR2A | ∃w ∈ VRA s.t. R(y, w) ∈ A and S(z, w) ∈ A} hh·, yiiA={y} hhR̂1 ◦ · · · ◦ R̂k , yiiA={x ∈ VRA | ∃w ∈ VRA s.t. R̂1 (x, w) ∈ A and w ∈ hhR̂2 ◦ · · · ◦ R̂k , yiiA } hhf : [a, b]iiA={x ∈ VRA | ∃a0 , b0 ∈ N s.t. f : [a0 , b0 ](x) ∈ A and a ≤ a0 ≤ b0 ≤ b} Note that hhR, SiiA , hhR̂1 ◦ · · · ◦ R̂k , yiiA , and hh·, yiiA are only used to support the computation of the set hhR1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm iiA of variable names in VRA that satisfies a role chain agreement. Intuitively, hhRn , Sm iiA computes the set of pairs (y, z) that are connected to a single variable through the role names Rn and Sm . Then, hhR1 ◦ · · · ◦ Rn−1 , yiiA (resp. hhS1 ◦ · · · ◦ Sm−1 , ziiA ) recursively computes the set of vari- ables connected to y (resp. to z) through a role chain R1 ◦· · ·◦Rn−1 (resp. S1 ◦· · ·◦Sm−1 ). Thereafter, A → A0 means that A0 results from the application of a rule in Figure ∗ 3 to A. As usual → denotes the reflexive and transitive closure of the → relation. A is complete (w.r.t. KB ) if no rule is applicable and is clash-free if it does not contain assertions of the form ⊥(x). Then, let C be a simple concept and KB a PL+ knowledge ∗ base, we say that A is the tableaux of C w.r.t. KB if A is complete and {C(x0 )} → A. Lemma 1. Let A and A0 be two Aboxes over VR s.t. A → A0 . For all models I of KB and d ∈ ∆I , we have that I, d |= A iff I, d |= A0 . Proof. First, consider A →func(R) A0 and assume that I, d |= A. This means that for some assignment π, with π(x0 ) = d, I, π |= A. Since the rule →func(R) is applicable to A, it must be the case that I, π |= R(x, y1 ) and I, π |= R(x, y2 ), for some x, y1 , y2 ∈ VRA and a role R s.t. func(R) ∈ K. Futhermore, I |= KB by hypothesis, so π(y1 ) = π(y2 ) and hence I, π |= A0 . Vice versa, assume that I, d |= A0 and let π be the corresponding assignment. Since y2 does not occur in A0 , π is free to map y2 arbitrarily. Then, in order to satisfy A, it is sufficient to assign π(y1 ) to y2 . Since in both directions the assignment of x0 has not changed, we have that I, d |= A iff I, d |= A0 . Regarding the other rules, note that A ⊆ A0 and hence I, d |= A0 implies I, d |= A by monotonicity. For the opposite direction, assume that I, π |= A, where π(x0 ) = d. Case A →u A0 . Since →u is applicable to A, (C1 u C2 )(x) must occur in A, for some simple concepts C1 , C2 and a variable x ∈ VRA . I, π |= C1 (x) and I, π |= C2 (x) A richer policy language for GDPR compliance 7 directly follow from the assumption I, π |= A. Consequently, I, π |= A0 . Case A →v A0 . Since →v is applicable to A, for some atomic concepts A, B and a variable x ∈ VRA , A(x) ∈ A and A v B ∈ KB . Then, from I, π |= A and I |= KB , it follows that I, π |= B(x) and hence I, π |= A0 . Case A →∃ A0 . From the precondition of the rule →∃ , we have that ∃R.C(x) occurs in A. Moreover, from the assumption I, d |= A, it holds dx ∈ (∃R.C)I , with π(x) = dx , which means that there exists an individual d0 s.t. d0 ∈ C I and (dx , d0 ) ∈ RI . Since y new does not occur in A, we can assign π(y new ) = d0 and obtain I, π |= A0 . Case A →dom A0 . From the precondition of →dom , R(x, y) ∈ A and dom(R, A) ∈ KB . So, any I, π satisfying A and KB must also satisfy A(x) and hence A0 . Case A →ran A0 . Similar to the previous case. Case A →func(f ) A0 . From the precondition of the →func(f ) rule, we have that I, π satisfy f : [l, u](x) and f : [v, w](x) where, according to KB , f is a function from ∆I to N. Then, given dx = π(x), both l ≤ f I (dx ) ≤ u and v ≤ f I (dx ) ≤ w hold which clearly means that max(l, v) ≤ f I (dx ) ≤ min(u, w). Consequently, I, π |= A0 . Case A →= A0 . By assumption I, π |= A and (R1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm )(x) ∈ A. Let dx be the individual associated to the variable x by π. There ex- ist two paths dx , d01 , . . . , d0n−1 , d¯ and dx , d001 , . . . , d00m−1 , d¯ s.t. (i) (dx , d01 ) ∈ R1I and (dx , d001 ) ∈ S1I ; (ii) (d0i−1 , d0i ) ∈ RiI , with i = 2, . . . , n − 1; (iii) (d00j−1 , d00j ) ∈ SjI , with j = 2, . . . , m − 1; (iv) (d0n−1 , d) ¯ ∈ RI and (d00 , d) ¯ ∈ S I . Since the variables n m−1 m new new new new new y1 , . . . , yn−1 , z1 , . . . , zm−1 , ȳ are fresh, we can extend π by mapping them to ¯ respectively. I, π |= A0 follows by construction. d01 , . . . , d0n−1 , d001 , . . . , d00m−1 , d, 0 Case A →disj A . According to the precondition of →disj , {A(x), B(x)} ⊆ A and disj(A, B) ∈ KB . Then, this case is vacuously satisfied since there does not exist a model I of KB and an assignment π that satisfy A. Case A →f⊥ A0 .Vacuously satisfied, otherwise we have l ≤ f I (d) ≤ u and u < l. Finally, note that in all of the previous cases π has been extended by mapping only fresh variables. The assignment of x0 therefore never changes, hence I, d |= A0 . t u Let A be a complete and clash-free Abox, a canonical model of A is an interpreta- tion JA = (∆JA , · JA ) satisfying the following conditions: 1. ∆JA = VRA ; 2. AJA = {x ∈ VRA | A(x) ∈ A}; 3. RJA = {(x, y) ∈ VRA × VRA | R(x, y) ∈ A}; 4. if f is non-functional (i.e. func(f ) 6∈ KB ), then (a) f JA ⊆ {(x, h) ∈ VRA × N | ∃l, u ∈ N s.t. f : [l, u](x) ∈ A and l ≤ h ≤ u}; (b) for each f : [l, u](x) ∈ A, there exists at least one l ≤ h ≤ u s.t. (x, h) ∈ f JA ; 5. if f is functional, then (x, h) ∈ f JA iff (a) h = max{l | f : [l, u](x) ∈ A} or h = min{u | f : [l, u](x) ∈ A}; (b) for each h0 6= h, (x, h0 ) 6∈ f JA . Note that all canonical models share the same domain as well as the same interpretation of atomic concepts and roles. Concrete features involve multiple canonical models, in particular condition 4 requires a canonical model to satisfy all assertions f : [l, u](x) for a not functional f occurring in A. Condition 5 associates to a variable x the maximum lower (resp. minimum upper) bound of the intervals relative to x and a functional f . 8 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro Lemmas 2 and 3 show that a canonical model JA of A satisfies both A and KB . Lemma 2. Let A be a complete and clash-free Abox, JA a canonical model of A and π the identity assignment s.t. π(x) = x, for all x occurring in A. Then, JA , π |= A. Proof. Clearly, JA and π satisfy all assertions A(x) and R(x, y) occurring in A by construction. Moreover, given f : [l, u](x) ∈ A corresponding to non-functional fea- J ture, by construction there exists a value l ≤ h ≤ u s.t. (x, h) ∈ fA (see condition 4). As a consequence, also f : [l, u](x) ∈ A is satisfied. Let f be a functional concrete feature and assume by contradiction that JA , π 6|= f : J [l, u](x), with f : [l, u](x) ∈ A. By construction, fA associates to x a single value h which is either max{l | f : [l, u](x) ∈ A} or min{u | f : [l, u](x) ∈ A}. Consider the first case and let f : [ˆl, û](x) be an assertion in A s.t. ˆl = max{l | f : [l, u](x) ∈ A}. From JA 6|= f : [l, u](x) and the fact that l ≤ ˆl it follows that ˆl > u. Moreover, since A is complete, by applying →func(f ) to f : [l, u](x) and f : [ˆl, û](x) we obtain that f : [max(l, ˆl), min(u, û)](x) is also in A. Then, we have that max(l, ˆl) = ˆl and min(u, û) ≤ u < ˆl. Consequently, by application of rule →f⊥ we would have that ⊥(x) occurs in A against the hypothesis that A is clash-free. Symmetrically, the assumption J that fA associates to x the minimum upper bound once again results in ⊥(x) ∈ A. t u Lemma 3. Let A be clash-free and complete w.r.t. KB , then a canonical model JA of A is also a model of KB . Proof. The proof is by reduction ad absurdum. Assume JA does not satisfy A v B ∈ KB . Then by construction, for some variable x ∈ VRA , A(x) ∈ A and B(x) 6∈ A. However, in this case →v would be applicable to A. Analogously, the assumptions that JA does not satisfy dom(R) v A ∈ KB , ran(R) v A ∈ KB and func(R) ∈ KB all lead to a contradiction of the hypothesis that A is complete. Finally, for each f s.t. J func(f ) ∈ KB , fA is functional by construction. t u The following lemmas prove that, under the interval safety assumption, the semantic consequences of a knowledge base and a complete Abox can be computed by hh·iiA . Lemma 4. Let A be clash-free and complete w.r.t. KB and D a concept s.t. D and A are interval safe. Then, KB , A |= D(x) iff JA , x |= D, for all canonical models JA . Proof. For the the left-to-right direction, we already know that each canonical model JA satisfies KB and JA , π |= A, where π is the identity assignment. Then, KB , A |= D(x) in particular implies JA , π |= D(x) and, since π(x) = x, we have that JA , x |= D. The right-to-left direction can be proved by induction on the structure of D. Case D = A. By definition, JA , x |= A iff x ∈ AJA iff A(x) ∈ A. Moreover, given a model I of KB and an assignment π, the facts that I, π |= A and A(x) ∈ A imply by definition that I, π |= A(x). Hence, KB , A |= A(x). Case D = f : [l, u], where f is not functional. We show that if JA , x |= f : [l, u], for all canonical models JA , then A contains an assertion f : [l0 , u0 ](x) with l0 ≥ l and u0 ≤ u. This clearly ensures that KB , A |= f : [l, u](x). Let f : [l1 , u1 ](x), . . . , f : [ln , un ](x) be the assertions in A relative to f and x, and assume by contradiction that A richer policy language for GDPR compliance 9 for all i = 1, . . . , n [li , ui ] 6⊆ [l, u]. Since D and A are interval safe, we have that [li , ui ] ∩ [l, u] = ∅. Then, by condition 4a, it follows that JA that does not satisfies f : [l, u], a contradiction. Case D = f : [l, u], where f is functional. By construction, that all canoni- cal models of A satisfy f : [l, u] means that both ˆl = maxf :[l,u](x)∈A l and û = minf :[l,u](x)∈A u lie in the interval [l, u]. Then, on the one hand, being A clash-free ensures that ˆl ≤ û and hence [ˆl, û] is an interval contained in [l, u]. On the other hand, since A is complete, f : [ˆl, û](x) occurs in A and hence KB , A |= f : [l, u](x). Cases D = D1 u D2 , D = D1 t D2 , D = ∃R.D0 and D = (R1 ◦ · · · ◦ Rn = S1 ◦ · · · ◦ Sm ) follow directly from the definitions and the induction hypothesis. t u Lemma 5. Let A be clash-free and complete w.r.t. KB and D a concept s.t. D and A are interval safe. Then, x ∈ hhDiiA iff JA , x |= D, for all canonical models JA . Proof. The proof is by induction on the structure of D. Case D = A. In this case hhDiiA = AJ A , for all canonical models JA . Case D = D1 uD2 . We have that JA , x |= D1 uD2 , for all JA iff JA , x |= D1 , for all JA , and JA , x |= D2 , for all JA . By induction, this holds iff x ∈ hhD1 iiA ∩ hhD2 iiA and hence x ∈ hhD1 u D2 iiA . Analogously, the cases when D = D1 tD2 , D = ∃R.D0 and D = (R1 ◦· · ·◦Rn = S1 ◦ · · · ◦ Sm ) follow directly from the definitions applying the induction hypothesis. Case D = f : [l, u]. For the left-to-right direction, x ∈ hhf : [l, u]iiA means that there exists some l0 , u0 s.t. l ≤ l0 ≤ u0 ≤ u and f : [l0 , u0 ](x) ∈ A. However, this ensures that KB , A |= f : [l, u](x) and by Lemma 4 it follows that JA , x |= f : [l, u], for all canonical models of A. For the opposite direction, assume that all canonical models satisfy f : [l, u] in x. As we know from Lemma 4, whether f is functional or not, this ensures that there exists an assertion f : [l0 , u0 ](x) in A with [l0 , u0 ] ⊆ [l, u]. By construction follows that x ∈ hhf : [l, u]iiA . t u The following theorem shows that the combined subsumption checking algorithm is correct and complete. Theorem 1. Let KB be a PL+ knowledge base, C a simple concept and D a concept s.t. C and D are interval safe. Then, KB |= C v D iff the tableaux A of C contains a clash or x0 ∈ hhDiiA . Proof. For the left-to-right direction, assume by contraposition that A is clash-free and x0 6∈ hhDiiA . By Lemma 5, we have that JA , x0 6|= D. Then, by Lemmas 3 and 1, JA is a model of KB and JA , x0 |= C. It follows that KB 6|= C v D. For the opposite direction, if A contains a clash, by Lemma 1 no model of KB satisfies C. Hence, KB |= C v D vacuously holds. Finally, assume that A is clash- free and x0 ∈ hhDiiA . By Lemmas 5 and 3 we have KB , A |= D. Let I be a model of KB s.t. I, d |= C. Clearly, by assigning x0 to d, I, d |= C(x0 ) holds and hence I, d |= A (Lemma 1). Then, I is a model of KB and, since I, d |= A, there exists an assignment π s.t. I, π |= A. Since KB , A |= D it follows that I, d |= D t u Finally, we show that tableaux-based expansion in the second phase together with the structural subsumption in the third phase can be performed in polynomial time. 10 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro Theorem 2. Let KB be a PL+ knowledge base, C a simple concept and D a concept s.t. C and D are interval safe. Subsumption checking KB |= C v D is PTIME. Proof. With respect to the tableaux construction, we show that the resulting Abox A is polynomial in the size of KB and C. First of all, the number of variable names occurring in A depends on the application of →∃ and →= rules. Since rule →∃ generates a single variable name, rule →= generates n + m − 1 variables at a time and the total number of their applications is bounded by |C|, it follows that VRA is proportional to |C|. Being VRA ∝ |C|, it is straightforward to see that rule →u can be applied at most |C| times whereas the number of possible applications of rules →v , →dom , →ran , →func(R) , and →disj is bounded by |C| · |KB |. Finally, the applications of →func(f ) and →f⊥ are at most |C|3 · |KB |. Then, the size of the resulting tableaux is polynomial in the size of KB and C and hence the second phase of the subsumption algorithm is performed in polynomial time. Then, checking x0 ∈ hhDii incrementally updates the extension of the subconcepts of D over A. Consequently, the third phase can be performed in O(|A| · |D|). t u As said above, in case C is not simple, the preprocessing reduces it in a normal form C1 t · · · t Cn that can be exponentially longer than C. This in particular may occur if C and D are not interval safe, due to introduction of disjunctions in the interval normalization (1), thus making the subsumption checking (see also Theorem 7 in [5]). However, the subsumption algorithm can be optimized in several ways in order to improve performance. A first optimization concerns the interval normalization. Clearly, the number of resulting interval splits depend on the set of distinct end-points occurring in D. We can reduce this set by using the following syntactic replacements in D: f [l1 , u1 ] t f [l2 , u2 ] f [min{l1 , l2 }, max{u1 , u2 }] if [l1 , u1 ] ∪ [l2 , u2 ] is an interval (2) f [l1 , u1 ] u f [l2 , u2 ] f [¯ l, ū] if ¯ l ≤ ū and f is functional . (3) where ¯l = max{l1 , l2 } and ū = min{u1 , u2 }. Standard optimizations can also be used to speed up the tablaux expansion. For instance, rules →∃ and →func(R) can be merged as follows: given ∃R.C(x), if R is not functional or x has no R-successor, then →∃ is applied as usual. Otherwise, C is added to the (single) R-successor of x. The rule →func(f ) can as well be optimized. Let f : [l1 , u1 ], . . . , f : [ln , un ] be the interval constrains occuring in C that are assigned to a variable x, ¯l the maximum lower bound of {l1 , . . . , ln } and ū the minimum upper bound of {u1 , . . . , un }. It is easy to see that either ū < ¯l, that is C is inconsistent w.r.t. KB , or [¯l, ū] is an interval that by construction is contained in all [li , ui ]. Therefore, we can replace f : [l1 , u1 ](x), . . . , f : [ln , un ](x) in A with a single assertion f : [¯l, ū](x). 4 Discussion We have introduced the description logic PL+ which allows to formalize the data usage policies adopted by controllers as well as the consent to data processing granted by data subjects. Checking whether the controllers’ policies comply with the available consent boils down to subsumption checking between PL+ concepts. A richer policy language for GDPR compliance 11 The frequency of compliance checks can be high, so PL+ has been designed to ad- dress scalability requirements by making the language as simple as possible. As a con- sequence, the ontology and the query languages are notably different from each other. In particular, the ontology language largely intersects some fragments of the EL and DL-lite families of DLs [2, 4, 1]. Conversely, the query language supports disjunctions, role chain agreements, and non-convex interval constraints in order to model limitations on data storage duration. These features place PL+ outside the space of Horn DLs [10, 11] – and in particular the tractable profiles of OWL2. We also presented a subsumption algorithm which, in broad terms, reminds the structural subsumption algorithm for the description logic underlying CLASSIC [9]. However, CLASSIC supports neither concept unions (t) nor qualified existential re- strictions (∃R.C). On the other hand, CLASSIC additionally supports number restric- tions and qualified universal restrictions (that strictly generalize the range restrictions of PL+ ), which make it incomparable to PL+ . To the best of our knowledge all previous encodings of policies in KR languages [14, 12, 6], focus on trust management and access control, rather than data usage con- trol. As a consequence, those languages lack the terms for expressing privacy-related and usage-related concepts. A crucial drawback is that the main reasoning task in those frameworks is permission checking; policy comparison (which is central to our work) is not considered. Both Rei and Protune [12, 6] support logic program rules. However, if rules are recursive the policy comparison results undecidable, otherwise, it is NP-hard. Similar considerations apply to KAoS [14], a framework based on a DL that, in general, is not tractable, and supports role-value maps that in general make reasoning undecid- able (see [3], Ch. 5). The authors do not discuss how to avoid this issue. In comparison, checking compliance between PL+ policies is tractable if there is a constant bound on the number of disjuncts occurring in a normalized concept. As future work, we are planning to implement the presented algorithm and to as- sess its scalability experimentally against real data usage policies provided by SPE- CIAL’s industrial partners. Moreover, we are planning to study three further extensions of PL motivated by SPECIAL’s use cases. Two of them are needed by a novel, dy- namic method for collecting consent. This method is based on fine-grained authoriza- tions, where the data categories involved consist of single data points (e.g. a specific location). This can be achieved by introducing nominals in PL. Moreover, the data subject should be able to deny consent for some of such specific authorizations, which amounts to introducing some form of negation in the policy language. The third exten- sion is needed to support so-called sticky policies [13], that constitute a sort of a license that applies to the data released to third parties. The recipient is allowed to use the data according to the sticky policy. In order to apply the same sticky policy transitively to arbitrary sequences of data transfers, a construct similar to fixpoints is needed (see [8, 7] for an extension of description logics with fixpoints). Acknowledgments This research is funded by the European Unions Horizon 2020 research and innovation programme under grant agreement N. 731601. 12 Piero A. Bonatti, Iliana M. Petrova, Luigi Sauro References 1. A. Artale, D. Calvanese, R. Kontchakov, and M. Zakharyaschev. The dl-lite family and relations. J. Artif. Intell. Res., 36:1–69, 2009. 2. F. Baader, S. Brandt, and C. Lutz. Pushing the EL envelope. In IJCAI-05, pages 364–369. Professional Book Center, 2005. 3. F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003. 4. F. Baader, C. Lutz, and S. Brandt. Pushing the EL envelope further. In K. Clark and P. F. Patel-Schneider, editors, Proceedings of the Fourth OWLED Workshop on OWL: Experiences and Directions, Washington, DC, USA, 1-2 April 2008., volume 496 of CEUR Workshop Proceedings. CEUR-WS.org, 2008. 5. P. A. Bonatti. Fast compliance checking in an OWL2 fragment. In J. Lang, editor, Proceed- ings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden., pages 1746–1752. ijcai.org, 2018. 6. P. A. Bonatti, J. L. D. Coi, D. Olmedilla, and L. Sauro. A rule-based trust negotiation system. IEEE Trans. Knowl. Data Eng., 22(11):1507–1520, 2010. 7. P. A. Bonatti, C. Lutz, A. Murano, and M. Y. Vardi. The complexity of enriched mu-calculi. Logical Methods in Computer Science, 4(3), 2008. 8. P. A. Bonatti and A. Peron. On the undecidability of logics with converse, nominals, recur- sion and counting. Artif. Intell., 158(1):75–96, 2004. 9. A. Borgida and P. F. Patel-Schneider. A semantics and complete algorithm for subsumption in the CLASSIC description logic. J. Artif. Intell. Res., 1:277–308, 1994. 10. D. Carral, C. Feier, B. C. Grau, P. Hitzler, and I. Horrocks. EL-ifying ontologies. In S. Demri, D. Kapur, and C. Weidenbach, editors, Automated Reasoning - 7th International Joint Con- ference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Aus- tria, July 19-22, 2014. Proceedings, volume 8562 of Lecture Notes in Computer Science, pages 464–479. Springer, 2014. 11. D. Carral, C. Feier, B. C. Grau, P. Hitzler, and I. Horrocks. Pushing the boundaries of tractable ontology reasoning. In P. Mika, T. Tudorache, A. Bernstein, C. Welty, C. A. Knoblock, D. Vrandecic, P. T. Groth, N. F. Noy, K. Janowicz, and C. A. Goble, editors, The Semantic Web - ISWC 2014 - 13th International Semantic Web Conference, Riva del Garda, Italy, October 19-23, 2014. Proceedings, Part II, volume 8797 of Lecture Notes in Computer Science, pages 148–163. Springer, 2014. 12. L. Kagal, T. W. Finin, and A. Joshi. A policy language for a pervasive computing environ- ment. In 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY), pages 63–, Lake Como, Italy, June 2003. IEEE Computer Society. 13. S. Pearson and M. C. Mont. Sticky policies: An approach for managing privacy across multiple parties. IEEE Computer, 44(9):60–68, 2011. 14. A. Uszok, J. M. Bradshaw, R. Jeffers, N. Suri, P. J. Hayes, M. R. Breedy, L. Bunch, M. John- son, S. Kulkarni, and J. Lott. KAoS policy and domain services: Towards a description-logic approach to policy representation, deconfliction, and enforcement. In 4th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY), pages 93–96, Lake Como, Italy, June 2003. IEEE Computer Society.