=Paper=
{{Paper
|id=Vol-2373/paper-5
|storemode=property
|title=A Richer Policy Language for GDPR Compliance
|pdfUrl=https://ceur-ws.org/Vol-2373/paper-5.pdf
|volume=Vol-2373
|authors=Piero A. Bonatti,Iliana M. Petrova,Luigi Sauro
|dblpUrl=https://dblp.org/rec/conf/dlog/BonattiPS19
}}
==A Richer Policy Language for GDPR Compliance==
https://ceur-ws.org/Vol-2373/paper-5.pdf
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.