E Ernst
email: emil.ernst@univ-amu.fr

The image of a closed convex set under a Fredholm operator

Keywords: Fredholm operator, image of a closed convex set, countable union of closed convex sets, F σ set 2000 MSC: 52A20, 52A41, 52B99

The purpose of this article is two-fold. In the first place, we prove that a set is the image of a non empty closed convex subset of a real Banach space under an onto Fredholm operator of positive index if and only if it can be written as the union of {D n : n ∈ N}, a non-decreasing family of non empty, closed, convex and bounded sets such that

The second part of this article proves that in every infinite dimensional real Banach space there is a convex set which can be expressed as the union of countably many closed sets, but not as the union of countably many closed and convex sets. Accordingly, every infinite dimensional real Banach space contains a convex F σ set which is not the image of a closed convex set under a Fredholm operator.

Introduction

This article deals with one of the most ubiquitous concepts in convex analysis and optimization: the image of a closed and convex set under a Fredholm operator. The case of an operator acting between two finite dimensional Banach spaces is well understood. With virtually no modifications, the technique used by Klee to prove [START_REF] Klee | Some characterizations of convex polyhedra[END_REF]Theorem 6.1] (a different method may be retrieved from the proof given by Sang and Tam to [START_REF] Sung | On the cone of a finite dimensional compact convex set at a point[END_REF]Proposition 2.2]), provides us with the following result.

Theorem [Klee]: Let X and Y be euclidean spaces, and Π : Y → X be an onto Fredholm operator of positive index. Then the set C is the image of a non empty closed and convex subset of Y under Π if and only if it is a non empty convex F σ subset of X.

Our first result (Theorem 2.3, Section 2) is a generalization of the previous Theorem to the setting of possibly infinite dimensional real Banach spaces.

Theorem A: Let X and Y be real Banach spaces, and Π : Y → X be an onto Fredholm operator of positive index. Then the set C is the image of a non empty closed and convex subset of Y under Π if and only if it is the union of {D n : n ∈ N}, a non-decreasing family of non empty, closed, convex and bounded sets, with the additional property that

D n + D n+2 ⊆ 2 D n+1 ∀n ∈ N. (1)
The rather technical assumption of Theorem A may be justified by arguing that, on one hand, any non empty closed and convex subset of a Banach space may easily be expressed as the union a a non-decreasing family composed of countably many non empty bounded closed and convex sets fulfilling relation [START_REF] Albiac | Topics in Banach space theory[END_REF], and on the other, that the image under a Fredholm operator of such a family is again a nondecreasing sequence of bounded closed and convex sets satisfying relation [START_REF] Albiac | Topics in Banach space theory[END_REF]. However, when X is a finite dimensional Banach space, by combining the two above-mentioned theorems, we deduce that a set is the union of a non-decreasing family of non empty, closed, convex and bounded sets fulfilling relation [START_REF] Albiac | Topics in Banach space theory[END_REF] if and only if it is a non empty convex F σ set.

Our second result (Theorem 4.3, Section 4) addresses the interplay between the hypothesis of Theorem A, on one hand, and of the previously mentioned Theorem by Klee, on the other, in the case of an infinite dimensional real Banach space.

Theorem B: Every infinite dimensional real Banach space contains a convex set which can be expressed as the union of countably many closed sets, but not as the union of countable many closed and convex sets.

In other words, the appropriate notion to describe the image of a closed convex set under a Fredholm operator is indeed the union of an increasing family of non empty closed, convex and bounded sets satisfying the property (1), as stated by Theorem A.

As a first step in achieving Theorem B, we are concerned with the convex hull of the extreme points of the unit ball in ∞ . Indeed, as stated by Albiac and Kalton at page 29 of their textbook, [START_REF] Albiac | Topics in Banach space theory[END_REF], "[the] structure [of ∞ ] has been well understood for many years. However, there can still be surprises, and there remain intriguing open questions". Our "surprise" is related to the notion of (infinite dimensional) convex polytope, as introduced by Klee ( [START_REF] Klee | Polyhedral sections of convex bodies[END_REF]): Proposition 3.2 proves that the convex hull of the extreme points of the unit ball in ∞ is a polytope, which, by virtue of Proposition 3.6, does not contain any infinite dimensional closed and convex set.

This unusual polytope is an example of a convex F σ set which cannot be written as a countable union of closed and convex sets, and settles in this way Theorem B when X = ∞ ; on this ground, Theorem 4.3 addresses the case of a general real Banach space X by using a standard compact embedding result.

The last section of this work addresses a question which, at the best of our knowledge, is open: characterize all the real normed spaces containing a convex F σ set which cannot be written as a countable union of closed and convex sets.

Theorem A

Let us consider X a real Banach space, and {D n : n ∈ N} a nondecreasing (meaning that D n ⊆ D n+1 for every n ∈ N) sequence of non empty, closed, convex and bounded subsets of X fulfilling the property [START_REF] Albiac | Topics in Banach space theory[END_REF]. The first part of this section is devoted to the proof of the following result.

Proposition 2.1. Let m be a positive integer, and λ i , i = 1, m, be nonnegative scalars whose sum amounts to 1. Then

m i=1 λ i D i ⊂ D p , (2)
provided that p ≥ m i=1 i λ i . (3)
This results plays a special role in achieving Theorem A, as the index p on the right side of the relation (2) depends only upon the coefficients λ i , i = 1, m, and not upon the sets from the sequence (D n ).

Proof of Proposition 2.1.

As a first step in establishing the desired result, let us address the following property of non-decreasing sequences of real numbers. Lemma 2.2. Let (x n ) n∈N be a non-decreasing sequence of reals such that

x n + x n+2 ≤ 2 x n+1 ∀n ∈ N. (4)
Let m be a positive integer, and λ i , i = 1, m, be non-negative scalars whose sum amounts to 1. Then

m i=1 λ i x i ≤ x p , (5)
provided that relation (3) holds true.

Proof of Lemma 2.2. As the case m = 1 is clear, we assume that m ≥ 2. The proof will be done in three steps.

Step 1: We claim that

x n + x n+k+1 ≤ x n+1 + x x+k ∀n, k ∈ N. (6)
Let us prove relation [START_REF] Klee | Some characterizations of convex polyhedra[END_REF] by induction after k. The case k = 1 is nothing but property (4), so we may assume that k > 1 and that property (6) holds for k -1:

x n + x n+k ≤ x n+1 + x n+k-1 ∀n ∈ N. (7)
By combining relation (4), and relation [START_REF] Klee | Polyhedral sections of convex bodies[END_REF] written for n + 1, we get that

x n + x x+2 + x n+k+1 ≤ 2x n+1 + x n+k+1 (8) = x n+1 + x n+1 + x n+k+1 ≤ x n+1 + x n+2 + x n+k .
The desired relation [START_REF] Klee | Some characterizations of convex polyhedra[END_REF] obviously follows from relation [START_REF] Sung | On the cone of a finite dimensional compact convex set at a point[END_REF].

Step 2: Let us consider q, k ∈ N, and α i ≥ 0, i = q, q + k + 1. We claim that there exists either γ i ≥ 0, i = q + 1, q + k + 1, with the property that

q+k+1 i=q+1 γ i = q+k+1 i=q α i , q+k+1 i=q+1 i γ i = q+k+1 i=q i α i , (9)
such that

q+k+1 i=q α i x i ≤ q+k+1 i=q+1 γ i x i , (10)
or µ i ≥ 0, i = q, q + k, satisfying the relation

q+k i=q µ i = q+k+1 i=q α i , q+k i=q i µ i = q+k+1 i=q i α i , (11)
such that

q+k+1 i=q α i x i ≤ q+k i=q µ i x i . (12)
Indeed, if α q ≤ α q+k+1 , then

q+k+1 i=q α i x i = α q (x q + x q+k+1 ) + q+k i=q+1 α i x i + (α q+k+1 -α q )x q+k+1 ,
and, as from the first step of Lemma 2.2 it follows that α q (x q + x q+k+1 ) ≤ α q (x q+1 + x q+k ), we deduce that

q+k+1 i=q α i x i ≤ α q (x q+1 + x q+k ) (13)
+ q+k i=q+1 α i x i + (α q+k+1 -α q )x q+k+1 .
It is easy to see that both the sum of the coefficients, and the sum of the products between the coefficients and their indices is the same on the right and on the left sides of formula (13):

α q + α q + q+k i=q+1 α i + (α q+k+1 -α q ) = α q + q+k+1 i=q α i -α q (14) = q+k+1 i=q α i , and
((q + 1) + (q + k))α q + q+k i=q+1 i α i + (q + k + 1)(α q+k+1 -α q ) = (15) (1 + (q + k))α q + q+k+1 i=q i α i -(q + k + 1)α q = q+k+1 i=q i α i .
We have thus established that, in the case α q ≤ α q+k+1 , the coefficients of the right side of relation (13) provide us with a system γ i , i = q + 1, q + k + 1 of non-negative scalars which fulfills the properties (9) and (10). Obviously, when α q ≥ α q+k+1 , a similar line of reasoning proves that there are µ i ≥ 0, i = q, q + k, satisfying relations (11) and (12).

Step 3: Let us finally consider the coefficients λ i ≥ 0, i = 1, m, whose sum equals to 1, and an index p fulfilling relation [START_REF] Bessaga | On bases and unconditional convergence of series in Banach spaces[END_REF]. In order to prove that relation [START_REF] Fonf | Some results on infinite-dimensional convexity[END_REF] holds true, let us repeatedly apply the procedure given by Step 2, with the the coefficients λ i , i = 1, m, as a starting point. It yields that there is a positive integer s = 1, m -1, and ζ s , ζ s+1 , two non-negative scalars, such that

ζ s + ζ s+1 = m i=1 λ i , sζ s + (s + 1)ζ s+1 = m i=1 i λ i , (16)
and

m i=1 λ i x i ≤ ζ s x s + ζ s+1 x s+1 .
From relations (3) and ( 14) it results that

p ≥ m i=1 i λ i = sζ s + (s + 1)ζ s+1 . (17)
Let us consider two cases:

ζ s+1 = 0, and ζ s+1 > 0. When ζ s = 0, then ζ s = 1, so relation (17) becomes p ≥ s. As the sequence (x n ) is non-decreasing, it follows that x s ≤ x p , whence m i=1 λ i x i ≤ ζ s x s + ζ s+1 x s+1 = x s ≤ x p . (18)
In the case ζ s+1 > 0, then sζ s + (s + 1)ζ s+1 > s, so from relation (17) it yields that

p ≥ m i=1 i λ i = sζ s + (s + 1)ζ s+1 > s, that is p ≥ s + 1. Then x s ≤ x s+1 ≤ x p , so m i=1 λ i x i ≤ ζ s x s + ζ s+1 x s+1 ≤ ζ s x p + ζ s+1 x p = x p . ( 19
)
The desired relation 5 may be deduced from statements ( 18) and ( 19).

We are now in a position to address the main technical result of this section.

Proof of Proposition 2.1. Let us pick a continuous linear function f : X → R (in other words f is an element of X * , the topological dual of X), and let us set x n := sup Dn f , n ∈ N, (obviously x n is a real number, since D n is a bounded set, and f is linear and continuous). The sequence (x n ) is nondecreasing, as the same holds for the sequence (D n ). Moreover, as f is linear, it holds that

x n + x n+2 = sup Dn f + sup D n+2 f = sup Dn+D n+2 f, (20)
and that 2 x n+1 = 2 sup

D n+1 f = sup 2 D n+1 f ; (21) but D n + D n+2 ⊆ 2 D n+1 , so sup Dn+D n+2 f ≤ sup 2 D n+1 f. (22)
From relations (20-22) it results that the sequence (x n ) satisfies the property (4), so, by virtue of Lemma 2.2, we deduce that

m i=1 λ i sup D i f ≤ sup Dp f. ( 23
)
Again as a consequence of the fact that f is linear, we observe that

m i=1 λ i sup D i f = sup m i=1 λ i D i f ; (24)
from relations (23) and ( 24) it yields that sup

m i=1 λ i D i f ≤ sup Dp f ∀f ∈ X * . ( 25
)
Being closed and convex, the set D p is the intersection of all the closed half-spaces containing it; relation (2) follows thus from relation (25).

The proof of Theorem A

This subsection characterizes the image of a closed convex set under a Fredholm operator.

Theorem 2.3. Let X and Y be real Banach spaces, and Π : Y → X be an onto Fredholm operator of positive index. The following statements are equivalent: i) the set C is the union of the non-decreasing family of non empty closed and convex sets fulfilling the property (1), ii) the set C is the image of a non empty closed convex subset of Y under Π.

Proof of Theorem 2.3. ii) ⇒ i) Let us consider K, a non empty closed convex subset of Y . Pick x 0 ∈ K, and set K n := K ∩ (x 0 + n B Y ), where B Y is the closed unit ball of Y . It is an easy task to verify that K n , n ∈ N, is a nondecreasing sequence of non empty bounded closed and convex subsets of Y fulfilling relation [START_REF] Albiac | Topics in Banach space theory[END_REF]. As the image under a Fredholm operator of a bounded closed convex set is always a bounded closed convex set, and as the image under a linear mapping of a non-decreasing sequence satisfying relation ( 1) is again a non-decreasing sequence satisfying relation [START_REF] Albiac | Topics in Banach space theory[END_REF], it follows that Π(K) is the union of an non-decreasing family of non empty closed and convex sets fulfilling the property (1). i) ⇒ ii) We consider D n , n ∈ N, a non-decreasing sequence of non empty bounded convex and closed subsets of X which satisfies relation [START_REF] Albiac | Topics in Banach space theory[END_REF]. Let V be the kernel of the Fredholm operator Π. As any finite dimensional subspace of a Banach space is complemented, there exists W , a closed subspace of Y disjoint from V , such that W + V = Y .

The restriction on W of Π, Π W : W → X, is a bijective continuous linear operator, so the sets E n := (Π W ) -1 (D n ) form a non-decreasing sequence of non empty bounded closed and convex subsets of W , and thus of Y ; moreover, the elements of this sequence satisfy formula [START_REF] Albiac | Topics in Banach space theory[END_REF].

Let us pick a non null vector v ∈ V (such a vector always exists since the index of Π, and thus the dimension of V , is a positive integer). We define the sets

A := ∪ i∈N (E i + i v) , and
B := ∪ i∈N (E i + {s v : s ≤ i}) ,
and claim that

A ⊆ co (A) ⊆ B. (26)
The sets

H p := W +{s v : s < p}, p ∈ N, are open half-spaces of W +R v, which is itself a closed subspace of Y . As A is a subset of W + R v, and as H p is open in W + R v, it results that co(A) ∩ H p ⊆ co(A) ∩ H p . ( 27
)
Let us pick x ∈ co(A) ∩ H p . As x ∈ co(A), there are some non-negative scalars λ i , i = 1, m, of sum equal to 1, and some elements

x i ∈ E i , i = 1, m such that x = m i=1 λ i x i + m i=1 i λ i w.
But x ∈ H p , so m i=1 i λ i < p; we may thus apply Proposition 2.1 to the sequence (E n ), and deduce that m i=1 λ i x i ⊂ E p . In other words,

co(A) ∩ H p ⊆ E p + {s v : s < p}. (28)
Finally, by combining relations ( 27) and (28) with the obvious fact that the closure of E p + {s v : s < p} amounts to

E p + {s v : s ≤ p}, it yields that co(A) ∩ H p ⊆ E p + {s v : s ≤ p} ∀p ∈ N,
fact which clearly implies relation (26). Taking into account that

Π(A) = Π(B) = ∪ i∈N Π(E i ) = ∪ i∈N D i , the proof of implication i) ⇒ ii) is complete.
3. The convex hull of the extreme points of the unit ball of ∞ : Theorem B in the case X = ∞

The aim of this section is to prove that the convex hull of the set gathering all the extreme points of the unit ball from the Banach space ∞ is a convex F σ set which cannot be expressed as the union of countably many closed and convex sets, proving in this way Theorem B in the case when X = ∞ .

To avoid some complicated notation, we will write a typical element of

∞ as x := (x(n)) ∞
n=1 , and we will call x n the n-th coefficient of x. Given S ⊂ N, let us denote be y S the element of ∞ defined by the formula

y S (n) := 1 n ∈ S -1 n / ∈ S .
Obviously, every point of form y S is an extreme point of B ∞ , the unit ball of ∞ , and every extreme point of B ∞ is of the form y S : ext B ∞ = {y S : S ⊆ N}.

Basic properties of co (ext B ∞ )

Let us denote by

P (x) := {x(n) : n ∈ N}, x ∈ ∞ ,
the set containing all the coefficients of some vector x from ∞ . For every S ⊂ N, it is clear that P (y S ) is a subset of {-1, 1}. More generally, the following easy to prove statement provides a characterization of elements x from the convex hull of ext B ∞ in terms of P (x).

Lemma 3.1. A vector x ∈ X belongs to the convex hull of ext B ∞ if and

only if P (x) is a finite subset of the closed interval [-1, 1].
Proof of Lemma 3.1. As the "only if" part is obvious, let us address the "if" part, and consider x ∈ X such that P (x) is a finite subset of [-1, 1]. Let α k , k = 0, p, be the elements of the set P (x) ∪ {-1, 1} written in increasing order; in particular, α 0 = -1, and α p = 1. For every k = 1, p we define

λ k := α k -α k-1 2 and S k := {n ∈ N : x(n) ≥ α k }. (29)
Obviously, all the numbers λ k , k = 1, p are positive, and their sum amounts to αp-α 0 2 = 1. We claim that

x = p k=1 λ k y S k . (30)
In order to prove our claim, let us pick n ∈ N; then x(n) = α s for some s = 0, p. We shall distinguish two cases: s = 0 and s ≥ 1.

Case s = 0: Since x(n) = α 0 = -1, it results that n does not belong to any of the sets S k , k = 1, p. Accordingly,

{k = 1, p : y S k (n) = 1} = ∅, so {k=1,p: y S k (n)=1} λ k = 0 = α 0 -α 0 2 . ( 31
)
Case s ≥ 1: With k = 1, p, the following line of equivalent relations is easily seen:

k = 1, s ⇔ α k ≤ α s ⇔ α k ≤ x(n) ⇔ n ∈ S k ⇔ y S k (n) = 1. ( 32
)
Relation (32) proves that {k = 1, p : y S k (n) = 1} = {1, . . . , s}, hence {k=1,p:

y S k (n)=1} λ k = s k=1 λ k = α s -α 0 2 . ( 33
)
By putting together relations (31) and (33), we infer that

[x(n) = α s ] ⇒   {k=1,p: y S k (n)=1} λ k = α s -α 0 2   ,
fact which allows us to compute the value of ( p k=1 λ k y S k ) (n):

p k=1 λ k y S k (n) = p k=1 λ k (y S k (n)) = {k=1,p: y S k (n)=1} λ k - {k=1,p: y S k (n)=-1} λ k = 2   {k=1,p: y S k (n)=1} λ k   -1 = 2 α s -α 0 2 -1 = α s = x(n) ∀n ∈ N.
We have thus proved our claim, together with the "if" part of Lemma 3.1.

We are now in a position to prove that co (ext B ∞ ) is a F σ polytope in the sense of Klee: each and every one of its affine finite-dimensional sections is the convex hull of a finite set of points. Proposition 3.2. The following two statements hold true. i) the convex hull of the extreme points of the unit ball of ∞ is a F σ set, ii) co (ext B ∞ ) ∩ L is the convex hull of a finite set, provided that L ⊂ ∞ is a linear manifold of finite dimension.

Proof of Proposition 3.2. i) Pick p ∈ N, and let T p be the set of all the vectors x from ∞ for which the set P (x) is a subset of [-1, 1] containing at most p elements.

Let us also consider a vector y such that y / ∈ S p . There are two possibilities:

|y(n)| > 1 for some n ∈ N, or P (y) ∩ [-1, 1] contains at least p + 1 different scalars, say {µ k : k = 1, p + 1}.
When it holds that |y(n)| > 1, let us set

ε := |y(n)| -1 2 ,
and remark that |z(n)| > 1 for every z ∈ y + ε B ∞ , so

(y + ε B ∞ ) ∩ T p = ∅.
When P (y) ∩ [-1, 1] contains the scalars {µ k : k = 1, k + 1}, we set

ε := min |µ i -µ j | 3 : i = j, i, j = 1, p + 1 .
Clearly, the set P (z) ∩ [-1, 1] contains at least p + 1 elements, for every z ∈ y + ε B ∞ , so again

(y + ε B ∞ ) ∩ T p = ∅.
Consequently, the set T p is closed for any p ∈ N; moreover, an obvious consequence of Lemma 3.1 reads that co (ext B ∞ ) = ∪ k∈N T k , so the convex hull of the extreme points of the unit ball of ∞ is a F σ set.

ii) Given L ⊂ ∞ , a linear manifold of finite dimension, we denote by p the dimension of the set

C := co (ext B ∞ ) ∩ L; then C contains p + 1 vectors, say x k , k = 0, p, such that C = co (ext B ∞ ) ∩ L , where L := x 0 + p k=1 γ k (x k -x 0 ) : (γ k ) k=1,p ∈ R p
is the linear manifold spanned by the set {x k : k = 0, p}.

By virtue of Lemma 3.1, it holds that C may be seen as the set of all the elements x from L such that P (x) is a finite subset of [-1, 1]. But the set P (x) is finite for any x ∈ L . Indeed, given n ∈ N, we define the following vector from R p :

w n := (x k (n) -x 0 (n)) k∈1,p ;
as for every k = 0, p, P (x k ) is a finite subset of [-1, 1], it easily yields that the set

W := {w n : n ∈ N} is a finite subset of the p-dimensional cube [-2, 2] p . Given x ∈ L , there exists γ := (γ k ) k∈1,p ∈ R p such that x = x 0 + p k=1 γ k (x k -x 0 ); thus x(n) = x 0 (n) + p k=1 γ k (x k (n) -x 0 (n)) = x 0 (n) + γ, w n
where •, • : R p × R p → R is the standard dot product in R p . As the vector x 0 has only a finite number of different coefficients, and since w n , n ∈ N, runs through the finite set W , it results that the vector x has also a finite number of different coefficients.

Consequently, the set C = co (ext B ∞ ) ∩ L may be seen as the set of all the elements x from L such that P (x) ⊂ [-1, 1]:

C = x 0 + p k=1 γ k (x k -x 0 ) : γ ∈ M , where M := {γ ∈ R p : -1 ≤ x 0 (n) + γ, w n ≤ 1 ∀n ∈ N}.
As already observed, both the sets W and P (x 0 ) are finite, so the set M is the intersection of finitely many closed half-spaces of R p . Hence C, a bounded subset of L , is the intersection of finitely many closed half-spaces of L , and an application of Weyl-Minkowsky's theorem concludes the proof of point ii).

Remark 3.3. It worth noticing that the polytope co (ext B ∞ ) has two unusual properties. First, when the finite dimensional linear manifold L runs through the class of all the linear manifolds of a given dimension, the number of vertices of the bounded convex polytope co (ext B ∞ ) ∩ L is not bounded from above. More precisely, given n ∈ N, it is easy to find a two-dimensional linear manifold L such that the convex polygon co (ext B ∞ ) ∩ L has at least n vertices.

Secondly, its closure, that is the unit ball in ∞ , is not a polytope.

Infinite dimensional subsets of co (ext B ∞ )

A key step in achieving the main result of this section is to characterize the infinite dimensional subsets of the convex hull of ext B ∞ . To this purpose, we denote by

R(µ, x) := {n ∈ N : x(n) = µ} x ∈ ∞ , µ ∈ P (x),
the set of all indices n ∈ N at which the n-th coefficient of x takes the value µ, and, given A ⊂ ∞ , we set

R(A) := {R(µ, x) : x ∈ A, µ ∈ P (x)}.
Proposition 3.4. Let A be a subset of the convex hull of ext B ∞ . The following sentences are equivalent: i) the dimension of A is infinite, ii) the set R(A) is infinite, iii) it exists a sequence (x n ) n∈N ⊂ A, and, for any n ∈ N, a scalar µ n ∈ P (x n ), such that the sets

K n := ∩ n i=1 R(µ i , x i ) ( 34
)
form a decreasing sequence.

Proof of Proposition 3.4. As obviously iii) ⇒ ii), all what we have to show

is that i) ⇒ ii), ii) ⇒ i), and that ii) ⇒ iii). i) ⇒ ii): Let us consider A ⊂ co (ext B ∞ ) such that R(A)
is a finite set. Thus, R, the ring of sets spanned by {∅} ∪ R(A) (we use here the notion of ring of sets in Birkhoff's sense, meaning a family of sets closed under the operations of set unions and set intersections) is itself finite. We set Y A := {y S : S ∈ R}, and we claim that A ⊂ co (Y A ).

Indeed, let us pick x ∈ A; as already seen (relations (29) and (30)), x lies within the convex hull of the set y S k : k = 1, p , where p + 1 is the number of elements from the set P (x) ∪ {-1, 1}, the scalars α k , k = 0, p, are the elements of P (x) ∪ {-1, 1} written in increasing order, and

S k = {n ∈ N : x(n) ≥ α k }.
It remains to prove that the sets S k , k = 1, p are elements of the ring R. Of course, α k ∈ P (x) for every k = 1, p -1, so

S k = ∪ p-1 i=k R(α k , x) ∪ S p , ∀k = 1, p -1.
As moreover

S p = ∅ 1 / ∈ P (x) R(1, x) 1 ∈ P (x) ∀p ∈ N,
we may conclude that, for any k = 1, p, the set S k is either the empty set, or the union of finitely many sets of form R(µ, x), with µ ∈ P (x); in both cases, S k ∈ R. Accordingly, y S k : k = 1, p ⊂ Y A , fact which proves our claim, and consequently the fact that the set A is finite, provided that R(A) is a finite set. The i) ⇒ ii) part of Proposition 3.4 is established.

ii) ⇒ i): Let us pick A, a finite dimensional subset of co (ext B ∞ ). By virtue of Proposition 3.2, it follows that A is contained in the convex hull of a finite subset of co (ext B ∞ ): in other words, there exists a positive integer p ∈ N, and

{x k : k = 1, p} ⊂ co (ext B ∞ ) such that A ⊂ co {x k : k = 1, p}.
Clearly, both the set R {x k : k = 1, p} , and R, the ring of sets spanned by R {x k : k = 1, p} , are finite. Let us pick

µ := (µ k ) k∈1,p ∈ Π p k=1 P (x k ); the set B µ := ∩ p k=1 R(µ k , x k
), besides providing an obvious example of an element of R, has the following property:

x k (n) = x k (m) ∀k = 1, p, ∀n, m ∈ B µ . (35)
As every element x from A may be expressed as a convex combination of the vectors x k , k = 1, p, from relation (35) it yields that

x(n) = x(m) ∀x ∈ A, ∀ n, m ∈ B µ ;
consequently, every set of form R(µ, x) with x ∈ A and µ ∈ P (x) is necessarily the union of a family of sets of form B µ , with µ ∈ Π p k=1 P (x k ). We have thus proved that R(µ, x) ∈ R ∀x ∈ A, ∀µ ∈ P (x), relation which entails that R(A) is a subset of R, hence a finite set, for every finite dimensional set A.

ii) ⇒ iii): To the purpose of establishing this implication, we will repeatedly use the following result, whose obvious proof will be omitted. Lemma 3.5. Let J be an infinite subset of N, and L ⊂ 2 J be an infinite set of subsets of J. Given J = ∪ p i=1 J i a finite partition of J, there is at least one index k = 1, p such that the set {D ∩ J k : D ∈ L} is an infinite set of subsets of J k .

Let us consider A, a subset of co (ext B ∞ ) such that the set R(A) is infinite. We will inductively define a sequence (x n ) n∈N of vectors from A, and, for every n ∈ N, a scalar µ n ∈ P (x n ), such that the two following relations hold true: α): the sets K i , i = 1, n, given by formula (34), are all different, β) the set {D ∩ K n : D ∈ R(A)} is infinite.

Case n = 1: Let us pick x 1 ∈ A. As relation α) obviously holds true when n = 1, we only need to define µ 1 ∈ P (x 1 ) such that the set {D ∩ K 1 : D ∈ R(A)} is finite.

To this respect, we apply Lemma 3.5 for J := N, L := R(A), and the finite partition N = ∪ µ∈P (x 1 ) R(µ, x 1 ) of N, and we deduce that it is always possible to pick µ 1 ∈ P (x 1 ) such that the set

{D ∩ R(µ 1 , x 1 ) : D ∈ R(A)} = {D ∩ K 1 : D ∈ R(A)} is infinite.
Case n > 1: Having defined x i and µ i , i = 1, n -1, let us remark that all what it is needed in order to fulfill relation α), is to pick the vector x n ∈ A in such a way that the set {K n-1 ∩ R(µ, x n ) : µ ∈ P (x n )} possesses at least two elements. Or, it is always possible to pick such a vector x n from A; indeed, by assuming, to the end of achieving a contradiction, that for every x ∈ A it holds that K n-1 ⊂ R(µ, x) for some µ ∈ P (x), then it results that

{D ∩ K n-1 : D ∈ R(A)} = {K n-1 }.
But relation β) is valid for n -1, so the set {D ∩ K n-1 : D ∈ R(A)} is infinite, and cannot contain only one element; our assumption is accordingly false.

It remains to chose the scalar µ n ∈ P (x n ) such that relation β) is satisfied; to this respect, let us apply once again Lemma 3.5, this time for J := K n-1 , L := {D ∩ K n-1 : D ∈ R(A)} and for the finite partition

K n-1 = ∪ µ∈P (xn) (K n-1 ∩ R(µ, x n )) .
It follows that there is an element, say µ n , in P (x n ) such that the set

{D ∩ (K n-1 ∩ R(µ n , x n )) : D ∈ L} = {D ∩ K n : D ∈ R(A)}
is infinite, and the second case is completed. Sequences (x n ) and (µ n ) obviously prove implication ii) ⇒ iii).

On the ground of Proposition 3.4, we establish the following result, providing a key property of the convex hull of ext(B ∞ ).

Proposition 3.6. The convex hull of the extreme points of the unit ball of ∞ does not contain any infinite dimensional closed convex set. Proof of Proposition 3.6. Let us consider A, an infinite dimensional subset of co (ext B ∞ ). By virtue of implication i) ⇒ iii) from Proposition 3.4, there is (x n ), a sequence of elements from A, and (µ n ), µ n ∈ P (x n ), a sequence of scalars, such that (K n ), the sequence defined by formula (34), is decreasing. Our objective is to define a sequence of positive real numbers λ n , n ∈ N, of sum equal to 1, such that the vector x := n∈N λ n x n possesses infinite many different coefficients.

As the sequence (K n ) is decreasing, it is always possible to pick, for every n ∈ N, an index a n which lies in K n , but outside K n+1 ; accordingly,

x n (a k ) = x n (a p ) ∀n, k, p ∈ N with n ≤ k < p, (36)
and

x n+1 (a n ) = x n+1 (a k ) ∀n, k ∈ N with n < k. (37)
It is an easy task to recursively construct the sequence of positive scalars τ n , n ∈ N, such that τ 1 := 1, τ 2 := 1, and that

τ n ≤ τ q+1 2 n |x q+1 (a q ) -x q+1 (a q+1 )|, ∀q, n ∈ N with q + 1 < n. (38)
Indeed, let n ≥ 3 be a positive integer, and assume that the numbers τ i > 0, i = 1, n -1 have already been chosen. As a consequence of relation (37) we deduce that

τ q+1 2 n |x q+1 (a q ) -x q+1 (a q+1 )| > 0, ∀q ∈ 1, n -2;
it is thus always possible to pick a positive scalar τ n fulfilling all the n -2 inequalities implied by relation (38).

All the coefficients of all the elements x n , n ∈ N, lay between -1 and 1; in particular, |x 2 (a 1 ) -x 2 (a 2 )| ≤ 2. By applying relation (38) for q = 1, n ≥ 3, one deduces that

τ n ≤ τ 2 2 n |x 2 (a 1 ) -x 2 (a 2 )| ≤ 1 2 n-1 ∀n ∈ N, n ≥ 3,
so the series n∈N τ n is convergent. We define λ n := τn n∈N τn , a sequence of positive real numbers whose sum is equal to 1. The following well-known and easy to prove fact is provided here without a proof. Lemma 3.7. Let X be a real Banach space, (x n ) n∈N ⊂ X be a bounded sequence, and (λ n ) n∈N ⊂ R + be a sequence of non-negative real numbers whose sum is equal to 1. Then the series +∞ k=1 λ k x k is convergent, and its sum belongs to the closed convex hull of the set {x n : n ∈ N}.

The series

n∈N λ n x n is thus convergent; let x denote its sum. We claim that the coefficients x(a n ), n ∈ N, are all different.

To prove our claim, let us consider two positive integers q and k such that q < k. By denoting the sum of the series i∈N τ i by s, we have s x(a q ) = n∈N τ i x i (a q ) (39) = q n=1 τ i x i (a q ) + τ q+1 x q+1 (a q ) + ∞ n=q+2 τ i x i (a q ), and

s x(a k ) = n∈N τ i x i (a k ) (40) = q n=1 τ i x i (a k ) + τ q+1 x q+1 (a k ) + ∞ n=q+2 τ i x i (a k ).
From relation (36) it results that q n=1 τ i x i (a q ) = q n=1 τ i x i (a k ), (41) and that x q+1 (a k ) = x q+1 (a q+1 ).

Putting together relations (39-42) we obtain that s (x(a q ) -x(a k )) = τ q+1 (x q+1 (a q ) -x q+1 (a q+1 )) (43)

+ ∞ n=q+2 τ i x i (a q ) - ∞ n=q+2 τ i x i (a k ),
so, by taking the absolute value in relation (43) we infer that |s (x(a q ) -x(a k ))| ≥ |τ q+1 (x q+1 (a q ) -x q+1 (a q+1 ))| (44)

- ∞ n=q+2 τ i x i (a q ) - ∞ n=q+2 τ i x i (a k ) .
polytope, and visibly does not lay in any closed hyperplane in ∞ , behaves in a strikingly different manner. Indeed, not only the norm interior of this set is empty, but co (ext B ∞ ) does not contain any infinite dimensional closed and convex set; in particular, the norm interior of every one of its infinitedimensional sections is empty.

Theorem B for the case x = ∞

The conclusions of Proposition 3.6 allow us to prove that Theorem B holds true in ∞ .

Theorem 3.9. The convex hull of the extreme points of the unit ball of ∞ cannot be expressed as a countable union of closed and convex sets.

Proof of Theorem 3.9. To the end of achieving a contradiction, let us assume that co (ext

B ∞ ) = ∪ n∈N C n ,
where C n , n ∈ N are closed and convex subsets of ∞ . The set {y S : S ⊆ N} of all the extreme points of the unit ball of ∞ is infinite and uncountable; accordingly, there is at least one of the sets C n , n ∈ N, say C n 0 , which contains infinitely many vectors of form y S , S ⊆ N.

Consequently, the set R(C n 0 ) is infinite, and implication ii) ⇒ i) from Proposition 3.4 proves that the set C n 0 is infinite dimensional. We have thus found a closed and convex subset of co (ext B ∞ ) whose dimension is infinite, fact which contradicts the conclusions of Proposition 3.6, proving in this way that our initial assumption is false.

Theorem B

This section addresses Theorem B in the general setting of real Banach spaces. In order to construct, in any given real Banach space X, a convex F σ set which cannot be written as the union of countably many closed and convex sets, we use the well-known theorem by Mazur1 which says that any infinite dimensional Banach space contains a basic sequence.

Originally stated by Banach without any proof at page

of his foundational treatise[START_REF] Banach | Théorie des opérations linéaires[END_REF], this result was proved in [3, Corollary 3, page 157]; the reader may found a complete account of this topic in the chapter V of the textbook[START_REF] Diestel | Sequences and series in a Banach space[END_REF]

Let us estimate the two absolute values from the right side of relation (44). As the coefficients of the vectors x n are contained between -1 and 1, and since the numbers λ n are positive, we may conclude that

on the other hand, by summing up after n ≥ q + 2 relation (38), one gets

Taking into account relations (45) and ( 46), it yields that

< |τ q+1 (x q+1 (a q ) -x q+1 (a q+1 ))| ;

finally, relations (44) and (47) combine to prove our claim.

The vector x has accordingly an infinite number of different coefficients. Lemma 3.1 proves that x does not belong to the convex hull of the extreme points of the unit ball of ∞ , while Lemma 3.7 shows that x is an element of the closed convex hull of the set A: consequently, the convex hull of the extreme points of B ∞ does not contain any infinite dimensional closed convex set.

Remark 3.8. A different light may be thrown on the previous result by recalling the well-known theorem by Fonf and Lindenstrauss ([5, Theorem 3.3]) which proves that the norm interior of any symmetric closed polytope is non empty, provided that the polytope does not lay in any closed hyperplane in X.

Or Proposition 3.6 proves that the convex hull of the extreme points of the unit ball in ∞ , a set which, by virtue of Proposition 3.2, is a symmetric The proofs of the following two easy exercises will be omitted. Lemma 4.1. Let X be an infinite dimensional real Banach space, and x n , n ∈ N, be a basic sequence in X. The operator K : ∞ → X defined by the formula:

is one-to-one an compact.

Lemma 4.2. Let Y and X be two real Banach spaces, and K : Y → X be a one-to-one compact operator. If A ⊂ Y is a convex F σ set which cannot be expressed as the union of countably many closed and convex sets, then the same holds true for K(A) ⊂ X.

Theorem 4.3. In any infinite dimensional real Banach space, there is a convex F σ set which cannot be expressed as a countable union of closed and convex sets.

Proof of Theorem 4.3. The desired conclusion easily follows by combining the conclusions of Lemmata 4.1 and 4.2, and of Theorem 3.9.

Concluding remarks

Theorems A and B provide us with a good understanding of the properties of the image of a closed convex subset of a real Banach space under a Fredholm operator. These results may accordingly be seen as a generalization of the analysis done by Klee in [6, Theorem 6.1] for the Euclidean case.

The study of Theorem B naturally rises the following question: does any infinite dimensional real normed space contains a convex F σ set which cannot be expressed as the union of countably many closed and convex sets? The answer, as proved by the following result, is negative. Proposition 5.1. Let X be a real normed space, and assume that X = ∪ n∈N X n , where X n are finite dimensional subspaces of X. Then every convex F σ set may be expressed as the union of countably many closed and convex sets.

Proof of Proposition 5.1. Let C ⊆ X be a convex set such that C = ∪ n∈N F n , where F n , n ∈ N, are closed sets, and let us pick x 0 ∈ C.

Let us set

; each of the sets D n is a no empty finite dimensional compact set, so its convex hull is closed. As moreover C = ∪ n∈N D n and C is convex, it follows that C = ∪ n∈N co D n .

We are thus lead to address the following question, which, at the best of our knowledge is open: which are the real normed spaces containing a convex F σ set which cannot be expressed as the union of countably many closed and convex sets? In view of Theorem B and Proposition 5.1, the answer must include the infinite dimensional Banach spaces, but must exclude the normed spaces which can be written as the union of countably many of their finite dimensional subspaces.


Koen Decroix
email: koen.decroix@cs.kuleuven.be

Denis Butin
email: denis.butin@inria.fr

Joachim Jansen
email: joachim.jansen@cs.kuleuven.be

Vincent Naessens
email: vincent.naessens@cs.kuleuven.be

Inferring Accountability from Trust Perceptions

Keywords: Accountability, IDP, Trust, Privacy, Surveillance

Opaque communications between groups of data processors leave individuals out of touch with the circulation and use of their personal information. Empowering individuals in this regard requires supplying them -or auditors on their behalf -with clear data handling guarantees. We introduce an inference model providing individuals with global (organization-wide) accountability guarantees which take into account user expectations and varying levels of usage evidence, such as data handling logs. Our model is implemented in the IDP knowledge base system and demonstrated with the scenario of a surveillance infrastructure used by a railroad company. We show that it is flexible enough to be adapted to any use case involving communicating stakeholders for which a trust hierarchy is defined. Via auditors acting for them, individuals can obtain global accountability guarantees, providing them with a trust-dependent synthesis of declared and proven data handling practices for an entire organization.

Context and Motivation

Contemporary situations involving the exchange of personal data for services often leave individuals oblivious as to the actual processing of their data. While privacy policies are widely used by organizations across the world, they often constitute mere declarations of intent. Individuals generally cannot check whether actual processing is in line with such ex ante statements. Furthermore, privacy policies often remain purposely vague while users demand concrete promises about the retention of their data, the purposes for which it is used, obligations in terms of third party forwarding and so on.

The rise of individuals' expectations about data handling transparency, combined with the growing imbalance of power between them and data processing organizations, has made the principle of accountability a key component of the discourse over privacy protection. While the concept of accountability was already mentioned in this context in the eighties [START_REF]and Development: OECD Guidelines on the Protection of Privacy and Transborder Flows of Personal Data[END_REF], it appears more prominently these days. In particular, the upcoming European General Data Protection Regulation [12] cites accountability explicitly. Organizations will therefore increasingly be legally required to be accountable for their data handling practices to data subjects.

A downside of this concept's popularity is that its meaning has been diluted due to frequent use in different contexts. Lawyers often focus on procedural aspects of accountability [START_REF] De Hert | Accountability and System Responsibility: New Concepts in Data Protection Law and Human Rights Law[END_REF][START_REF] Raab | The Meaning of 'Accountability' in the Information Privacy Context[END_REF]. Computer scientists often tackle specific security properties -such as non-repudiation [START_REF] Bella | Accountability Protocols: Formalized and Verified[END_REF] -or specific technical contexts like cloud environments [START_REF] Haeberlen | A Case for the Accountable Cloud[END_REF]. Because of these varied interpretations, no universal definition of accountability can be given. However, it normally refers to the necessity of surpassing mere compliance to achieve demonstration of compliance. By putting the burden of proof of good behavior on the data controller, accountability measures increase pressure on organizations to be transparent and fair in their data handling practices.

In real-world situations, data shared by an individual does often not remain within the realm of a single entity but it disseminated among communicating subsystems that may even be geographically distant. Since subcontractors may belong to different corporations than the organization that collected personal data in the first place, different data handling policies may apply. The initial data controller may fulfill its promises as long as data remains in its initial location, but offer no guarantees about processing by other stakeholders. Such situations leave individuals blind to the whereabouts of their data.

Even if all involved entities publish clear data handling policies, the end result is opaque to individuals. Technical privacy policies may be very detailed and the number of entities may be large. It is useful for individuals to understand the resulting global (organization-or system-wide) guarantees that apply to their personal data. If individuals have defined personal privacy preferences for themselves once and for all, they would also like to know whether the overall processing of their data by an organization and its subcontractors is in conflict with those preferences.

This paper introduces a model capable of inferring global accountability guarantees from the point of view of a trusted auditor. This auditor acts on behalf of the user and represents his interests. In practice, the auditor could be a member of a Data Protection Authority or a third-party, accredited auditing organization. The framework allows the hierarchical representation of entities in an organization, thereby modeling trust relationships: an individual may only trust a given component in an organization, or may trust an entity higher in the hierarchy, thereby trusting all components operating by that entity. These trust assumptions (i.e. user expectations) influence the computation of the global accountability guarantees. We distinguish between three levels of users: a naive user, a regular one and a privacy-aware one. The level of privacy-awareness of a user influences the kind of evidence this user assumes to be trustworthy.

In addition to these different types of users, data handling statements carry different levels of evidence. Each entity subcontracting for an organization has its own data handling statements. At the lowest level, statements are merely declarations of intent with no additional evidence. This level of evidence is akin to a detailed, technical privacy policy. Other statements are provided together with system traces of data handling operations, i.e. logs. These logs are assumed to be trustworthy, but they have not been inspected. Therefore, it may not be obvious at first glance that a data processor has misbehaved, even though a trace of misbehavior is assumed to exist in the logs. The situation where logs cannot be checked easily is realistic because logs are not standardized in general, many organizations use very specific formats and because semantics are often unavailable. The highest level of evidence features statements that are accompanied by logs that have been verified and found to be compliant. Here, it is again assumed that the logs are trustworthy, i.e. reflect actual system execution, and that the log analysis software is sound and accurate.

The three levels of user privacy-awareness and three levels of statement evidence are combined to compute fine-grained global accountability guarantees. The auditor, on behalf of the user, can both inspect those global guarantees or detect potential conflicts by providing the privacy preferences of the individual.

Our framework is implemented in IDP, a knowledge base system [START_REF] Denecker | A Knowledge Base System Project for FO(•)[END_REF]. We demonstrate it through the scenario of a surveillance infrastructure managed by a railroad company and involving a third-party security service company, operators such as a surveillance guard and an image processor, and components used by these operators. This kind of scenario demonstrates the typical situation where an individual shares his data with only one entity initially, after which the entity processes and disseminates the data among several subcontractors. Assuming individuals are monitored via cameras, one can distinguish between several categories of personal data which can be collected, processed and distributed. Depending on image quality and on pan-tilt-zoom functionality, cameras may record full body pictures with insufficient quality to distinguish faces, full body pictures with blurred faces, faces only or even record behavior patterns while discarding body images.

As mentioned above, we assume logs (when they exist) to be trustworthy: they are accurate and cannot be forged by entities. In practice, this requires techniques such as forward integrity [START_REF] Bellare | Forward Integrity for Secure Audit Logs[END_REF] to guarantee the security of logs, and partial formal modeling or trusted computing to ensure unforgeability. While these criteria are important, they are outside of the scope of this work: here, we suppose that logs reflect actual system execution and therefore embody meaningful evidence. Furthermore, we presume that personal data is categorized in a standardized way, so that individuals and organizations use the same terminology for categories of personal data.

We continue with some technical background on the IDP system, a knowledge base system based on an extension of typed first-order logic ( §2). The approach is illustrated by the running example of a railroad surveillance infrastructure, presented informally at first ( §3). We then introduce the building blocks of the accountability inference framework and apply it to this scenario ( §4). After evaluating the results of this implementation of the model ( §5), we discuss related work on formalizations of accountability and privacy ( §6), including ex-isting models for privacy reasoning realized with IDP. The paper concludes with a discussion of the potential, limitations and future of the framework ( §7).

IDP

IDP [START_REF]The IDP system[END_REF][START_REF] Wittocx | The IDP system: A model expansion system for an extension of classical logic[END_REF] is a state-of-the-art knowledge base system [START_REF] De Pooter | A Prototype of a Knowledge-based Programming Environment[END_REF] developed by the Knowledge Representation and Reasoning (KRR) group at KU Leuven. We briefly introduce IDP and how it can be used as a tool to manage an accountability framework, focusing on the parts of the system relevant for this paper. More interested readers can find IDP documentation and source code here [START_REF]The IDP system[END_REF], and some examples here [START_REF]KRR Software[END_REF]. In this text we use IDP to refer to IDP 3 , the current version of the IDP system. One of the main focuses of IDP is knowledge representation: allowing users to formulate their knowledge in a intuitive manner. To this end the FO(•) language framework, an extension of First Order Logic (FO), was developed. Using this language, users can model their data (in this case, which organizations or data categories to analyze), as well their knowledge (here, accountability across organizations) in a formal way using logical formulas (constraints) and definitions. This model can be used to solve problems by applying one of the many inferences IDP provides. For this paper we will need (optimal) model expansion: given a partial assignment for data, find a complete (optimal) assignment such that all expressed constraints and definitions hold. The initial, partial assignment corresponds to the setting of our framework: a hierarchical network of organizations and the accountability guarantees they offer. The outcome of the model expansion inference then corresponds to a complete assignment: a listing of which information is used in what places and what kinds of accountability guarantees it offers. This will later be called the Global Accountability Profile (GAP).

There exists a variety of declarative modeling systems, such as Alloy [START_REF] Jackson | Alloy: A Lightweight Object Modelling Notation[END_REF][START_REF] Jackson | alloy: a language & tool for relational models[END_REF] or ASP solvers [START_REF] Gebser | Conflict-Driven Answer Set Solving: From Theory to Practice[END_REF][START_REF] Leone | The DLV system for knowledge representation and reasoning[END_REF]. We chose to use IDP as our modeling tool for two reasons. First, the language it uses is expressive and intuitive: it supports extended first order constraints as well as definitions under well-founded semantics [START_REF] Van Gelder | The Well-Founded Semantics for General Logic Programs[END_REF]. Second, it is implemented as an extension in Lua [START_REF] Ierusalimschy | Lua -an extensible extension language[END_REF], which means there is support for procedural integration. This allows us to determine the way in which we want to use our declarative model in a flexible way.

A Railway Station Surveillance Scenario

To illustrate the model, we consider the scenario of video camera surveillance in a railway station. Since individuals are filmed by cameras, the collected categories of personal data are related to images (we assume the cameras do not record sound). Several categories of personal data can be inferred from camera recordings, such as identification through face detection [START_REF] Viola | Robust Real-Time Face Detection[END_REF], gait recognition [START_REF] Lee | Gait Analysis for Recognition and Classification[END_REF], behavioral tracking [START_REF] Mecocci | Automatic detection of anomalous behavioural events for advanced real-time video surveillance[END_REF] The trusted auditor (acting on behalf of a filmed individual) is external to the model and we focus on data handling statements from the entities collecting personal data, listed in Tab. 1.

Components of the Accountability Inference Model

Having set the stage for both our model and the tool that will be used to evaluate it, we now describe the framework's building blocks (depicted in Fig. 1) in detail. Entities, all related to a core organization, provide individual statements about their data handling practices. These statements can be provided together with unverified logs, verified logs, or exist on their own without companion evidence. Different categories of personal data can be modeled. As a consequence, statements are fine-grained enough to express different guarantees about various types of personal data. The data subject is represented by a trusted auditor. This auditor takes into account the subject's trust perceptions. Global accountability guarantees are automatically computed using the computation rules in the System Independent Part of the framework. These guarantees are represented by the Global Accountability Profile (GAP) that is automatically inferred, using a Knowledge Base System (IDP), from the System Model and the User Model, both part of the framework's Input Model. The former models the individual statements, the relations between the entities expressing the statements, and the level of evidence characterizing the statements. The latter includes the level of trust of the user. As a consequence, the global accountability guarantees take into account both factual evidence and subjective appreciations of privacy risks. This combination reflects the fact that different data subjects demand different levels of proof to be satisfied. The model provides data subjects with an overview of the accountability guarantees resulting from a set of interacting entities. In addition, it allows them (or the auditor, on their behalf) to check whether their personal privacy preferences are compatible with this global accountability panorama. The remainder of this section further details the framework's elements.

Personal Data

Organizations collect personal data of data subjects that interact with systems owned by these organizations. Being accountable to data subjects involves clarifying which types of their personal data are harvested and used. These categories are represented by the DataCategory type. All categories of collected personal data involved in a given scenario must be spelled out in the input model as the contents of DataCategory.

One can define hierarchies of personal data categories. This models the fact that categories of personal data can be subsets of other categories, e.g. the age of an individual gives strictly more information than a predicate on whether the individual is over 18. The data category hierarchy is represented using Data-CategoryOf(DataCategory,DataCategory), which deduces hierarchical knowledge from the initial specifications. Listing 1 depicts the IDP input model for the personal data and their hierarchy of the camera surveillance scenario.

Entities

Data subjects and the auditors that act on their behalf are not explicitly modeled since their point of view is external. An arbitrary number of active entities can be modeled in the framework's system model. Active entities are those that handle personal data of the subjects and provide some degree of accountability, IDP Listing 2: Partial system model representing the entities and their relationships in the video surveillance scenario.

Statements and Local Accountability Statements

All entities involved in data handling relevant to a given data subject are assumed to exhibit some level of accountability of practice, i.e. they publish precise declarations about their intended personal data handling practices. In general, each entity publishes a different data handling statement. A one-to-one mapping between entities and data handling statements is assumed, and is modeled using function StatementFrom(Statement) : Entity. Listing 3 shows the part of the system model that defines a subset of the statements of the railway company listed in Tab. 1 4 . Those statements include the following aspects:

-Purposes of use, i.e. the list of finalities for which the collected personal data may be used (for instance statistics or direct marketing) -this is modeled using StatementPurpose(Statement, Purpose). Multiple purposes can be defined for a statement. -The category of personal data that is used, i.e. the collection of personal identifiable information. Possibly, multiple subject data categories exist for a statement -this is modeled using predicate StatementSubject(Statement, DataCategory). -Global retention limits, i.e. the period of time after which the personal data will be deleted by the entity (e.g. Obligations are flexible and can be used to express a variety of constraints. Conditions are events that trigger a reaction, e.g. the personal data is accessed or the data subject has requested an update. Actions are the resulting events, for instance the update of his personal data or its forwarding.

Statements guaranteeing the sending of a notification (to a user) when a specific event occurs (e.g. when a specific category of personal data is accessed by the entity) are expressed using StatementNotificationGuarantee (Statement).

Accountability occurs at different levels. Some entities may merely declare their intended practices, without providing any companion evidence. Other entities provide data handling logs. In the model this is denoted using function StatementProof(Statement) : StatementEvidence. It may not always be possible to check the compliance of data handling logs with obligations. Logs can be in a format which is not standardized, or semantics may not be provided by the entity. We therefore distinguish between three levels of assurance (StatementEvidence) for data handling statements:

1. A statement is (purely) Declarative if data handling logs relevant to the statement are not made available by the entity publishing the statement. 2. If data handling logs are provided together with the statement but cannot be checked straight away, the statement obtains the status LoggedUnverified. 3. If a statement is provided together with logs that have been checked for compliance (e.g. through a trusted log analysis software), the statement is said to be LoggedVerified. This is the highest level of accountability for a data handling statement, since actual behavior has both been recorded and shown to be compliant with the statement.

Trust Perception and Global Accountability Inference

While organizations may feature complex hierarchies with heterogeneous data handling practices, individuals care about what happens to their personal data globally. A panoramic overview of the worst-case scenario in terms of data processing (i.e. what are the weakest global guarantees?) is relevant to individuals, since they must often decide whether to interact with an entire organization. Most of the time, they cannot cherry-pick with which subcontractors to share their data with. Global accountability inference is a central feature of this framework that builds such a synthetic statement for data subjects. It deduces global guarantees from the local accountability statements of all entities involved in the system. These (subjective) guarantees depend on trust perceptions of data subjects.

Individuals display different levels of trust in the entities that handle their personal data. The framework's user model reflects this socio-technical aspect by modeling three levels of trust, corresponding to three typical types of individuals:

-Naive individuals always trust data handling statements, even if statements are purely declarative (i.e. no evidence in the form of a log is provided); -Regular individuals only trust statements co-occurring with relevant data handling logs; -Privacy-aware individuals are most skeptical and trust only statements for which verified logs have been provided by issuing entities.

Furthermore, the user model includes UserTrust(Organization), the user's high-level trust perception towards organizations. It represents his trust in declared data handling practices of related organizations. This also implies that all operators they employ and components they own are trusted by him. The modeled video surveillance scenario features the aforementioned three user models: naive (U1 ), regular (U2 ) and privacy-aware (U3 ). It also assumes that no organization is trusted, i.e. UserTrust(Organization) is the empty set. This impact of these user trust models on the perception of global accountability guarantees is shown in Tab. 2. For instance, a naive user considers he is guaranteed that merely declared statements of an entity E, owned or employed by organization O, correspond with actual data handling practices. By contrast, a regular user only considers merely declared statements to be guaranteed if he trusts O (i.e. UserTrust(O)), and assumes statements provided together with logs to be guaranteed, whether these logs are checked for compliance or not.

G G G Regular user F (E) : {G, U } ⋆ G G Privacy-aware user F (E) : {G, U } ⋆ F (E) : {G, U } ⋆ G ⋆ F (E) = ′ G ′ ⇔ UserTrust(O) ∧ (ComponentOf (E) = O ∨ EmployeeOf (E) = O) ⋆ F (E) = ′ U ′ ⇔ ¬UserTrust(O) ∧ (ComponentOf (E) = O ∨ EmployeeOf (E) = O)
Global statement computations are performed differently for duties (i.e. statements featuring Always) and for prohibitions (i.e. statements featuring Never). Beside these categories, models also include statements expressing notification guarantees and global retention limits. Comparable with duties, these also feature Always. Nevertheless, these are treated differently in computations.

Global statements are expressed in terms of global data categories (i.e. users are concerned what happens to their personal data). Let S be an individual statement of entity E, CanCollect(E,DC) a data category DC that can be collected by an entity E, and Sub(S,DC) representing that data category DC is a subject of S. Tab. 3 summarizes the worst-case deduction rules that depend on the global statement evidence for the computation of GlobalDataCategory(S,DC), the global data categories derived from S.

Duties. Global statements using Always are built as follows:

-The global purposes of use for a global data category are constructed from the union of all purposes of (individual) duties S, with GlobalDataCategory(S,DC). These represent worst-case global purposes which are conjunctive. For instance, personal data is collected for commercial and statistical reasons. If no purpose is explicitly specified, then all purposes are assumed to be permitted globally. -The global conditions of use for a data category are constructed from the disjunction of all conditions of duties S, with GlobalDataCategory(S,DC). If

Global statement evidence of S:

Uncertain Guaranteed

Duty(S) CanCollect(E, DC ) ψ(S, E, DC ) ⋆ Prohibition(S) ψ(S, E, DC ) ⋆ Sub(S, DC ) NotificationGuarantee(S) Sub(S, DC ) ψ(S, E, DC ) ⋆ RetentionLimit(S) Sub(S, DC ) ψ(S, E, DC ) ⋆ ⋆ ψ(S, E, DC ) ≡ CanCollect(E, DC ) ∧ Sub(S, DC)
at least one unconditional statement exists, no conditional statement is generated. -The global actions for a data category are built from the union of all actions of individual duties S, with GlobalDataCategory(S,DC). -The global level of assurance (i.e. global evidence) for a data category is Uncertain if at least one uncertain statement (in the sense of Tab. 3) exists for this data category. Else, the global statement is considered Guaranteed. -The global notification guarantee for events relative to a data category is built from the conjunction of all individual notification guarantees S relative to that data category, with GlobalDataCategory(S,DC). -The global retention limit for a data category is the maximum of all retention limts S existing for the data category, with GlobalDataCategory(S,DC).

Prohibitions. Global statements using Never are built as follows:

-The global purposes of use for a global data category are constructed from the union of all purposes of individual prohibitions S, with GlobalDataCategory(S,DC). These represent worst-case global purposes which are disjunctive. For instance, personal data is never collected for commercial or statistical reasons. Individual prohibitions without explicit purpose are omitted during the deduction of global purposes (i.e. worst-case). -The global conditions of use for a data category are constructed from the conjunction of all conditions of prohibitions S, with GlobalDataCategory(S,DC).

Unconditional statements are omitted. -The global actions for a data category is computed as for duties, mutatis mutandis. -The global level of assurance for a data category is computed as for duties, mutatis mutandis.

In global statements, trust is expressed in a binary way (i.e. GAPEvidence): statements are, from the point of view of the data subject, either Uncertain or Guaranteed. Both global notification guarantees and global retention limits, part of the GAP, are expressed as duties. Global statements present guarantees as a function of categories of personal data. Once global statements have been computed, they are represented as in Listing 4. They are categorized as follows:

-Global duties about collecting personal data -declaring actions about the use, collection, or storage of personal data. -Global duties about distributing personal data -declaring actions that forward data to external organizations. -Global prohibitions for collecting personal data -expressing that the use, collection, or storage of personal data is forbidden. -Global prohibitions for distributing personal data -forbidding the forwarding of personal data to an organization. -Global notification guarantees -declaring the sending of a notification upon the occurrence of a specific event.

-Global retention limits -expressing the time limit after which all categories of personal data must be deleted.

Computation and Evaluation

We illustrate a possible use of the framework with an IDP realization1 . Our realization infers the GAPs of the user models U1 , U2 , and U3 described earlier, representing individuals under video surveillance in a railway station. The model was generated in less than a second on a personal computer. We first compare the resulting profiles for naive, regular, and privacy-aware data subjects. Next, we discuss how the statements of entities and users are modeled.

Trust-Dependent GAP Inference

First, given the type of user and his trust perception toward organizations, we deduce for each entity the user's global statement evidence using the rules of Tab. 2. For instance, U2 (i.e. regular user) is sufficiently guaranteed that data practices comply with declared ones if they are merely logged. Instead, U3 is satisfied when statements are logged and verified by an auditor or just logged in case organizations are trusted by him. This global evidence is then used for the deduction of the GAP using the rules of Tab. 3. The inferred GAPs are summarized in Tab. 4. None of these contain global prohibitions. However, individual statements of entities include two prohibitions (i.e. R.3 and I.3 ). The reason for this is that worst-case computation rules give priority to global duties containing data categories that are subject of both duties and prohibitions. Semantically, this corresponds to a user who is more concerned about the categories of data used rather than about the unused ones.

IDP Listing 4:

Modeling concepts representing the GAP.

Global duties for collecting data are perceived differently by U1 , U2 , and U3 . Since U1 is satisfied with statements that are purely declarative, he believes that data collection duties are respected by the organizations. Having the same guarantees U2 is only partially convinced, since he requires at least data handling logs while the security company's duty S.1 is purely declarative. Therefore, Time and Location, subjects of S.1, are considered as global duty data categories that are uncertain. U3 needs the strongest guarantees. He is not convinced for any of the data categories part of the GAP. He expects for all data collection duties that logs exist and that they are verified by an auditor. For instance, because duty R.1 is logged-unverified, the duty subjects, such as Face and BlurredFace, are not sufficiently guaranteed for U3 . Furthermore, due to R.1 an additional data category PictureIncident is deduced in U3 's GAP. This fol-lows from the computation rule in Tab. 3 for duties with global evidence that is uncertain for U3 , and the given railway station's camera capability Component-CanCollect(Camera,PictureIncident). Also, comparing the GAP of U3 with the others, more purposes for collecting data are deduced. In particular, besides that BlurredFace and are collected for incident detection (i.e. DetectIncident), these are used as Evidence of incidents as well.

Global data forward duties are computed from the declarative duty R.2 and the merely logged duty S.2. Both duties declare to forward data to other stakeholders in the system. The results show that U1 is satisfied with the guarantees provided that the system respects data forwarding declarations. The same guarantees are too weak to convince U2 and U3 . Both doubt that actual data practices correspond with declared ones. At first glance, one could expect that U2 assumes that Time and Location, part of the GAP, are used as declared by S.2. However, S.2 is redundant with the purely declared duty R.2 because Time and Location are subjects of R.2 as well. This can be deduced using the computation rules of Tab. 3 and from the railway company's image database capabilities, namely ComponentCanCollect(ImageDB,Time) and ComponentCan-Collect(ImageDB,Location).

Global retention limits are computed from R.4, I.4, and D.3. Results show that retention limits are conditional (i.e. NoLegalInvestigation) for all data categories in the GAP of U1 and U2 . The GAP of U3 shows an additional unconditional retention limit for data category PersData (i.e. personal data). This is deduced from R.4, which provided evidence not fulfilling U3 's expectations. Indeed, R.4 is just logged, and not verified. Furthermore, U2 only has partial guarantees for Time and Location since evidence of R.3 sufficiently guarantees him. In case of U3 , R.3 provides insufficient evidence. Hence, usage of Time and Location are not sufficiently guaranteed according to U3 's GAP.

Statements Modeling and User Models

The statements presented in the scenario are atomic declarations, i.e. they consist of single actions on subject data categories. Concepts in the framework were defined for modeling atomic statements. However, statements may contain multiple declarations. The concepts defined lack expressiveness for modeling these. These statements must be represented by the atomic parts from which they are composed. For instance, the image database is associated with a declarative statement announcing the storage of personal data of categories blurred face and gait for a maximum of 30 days and for the purpose of statistics and marketing. This is modeled as (a) a duty declaring that data categories blurred face and gait are stored, and (b) a retention limit specifying that data is kept for a maximum of 30 days. In the model, these items correspond to separate elements of the Statement domain. Though both statements have the same purposes, these must be expressed separately. In particular, StatementPurpose(Statement,Purpose) relates the purposes statistics and marketing to the duty and retention limit with 2 statements × 2 purposes relations. Decomposing combined statements may imply that statement relations grow combinatorially. Similarly, each Statement Detecting conflicts. The user model could be extended with user privacy preferences containing prohibitions. This aspect could be used by auditors wanting to verify e.g. whether a system, run by a commercial organization, is not collecting sensitive health information. The individual statements of system entities are another flexible facet. Typically, these statements form a large set of opaque and potentially inconsistent declarations. Automated verification can be added to the system-independent part of the framework for easy conflict detection.

Related Work

A privacy evaluation framework based on trust assumptions is introduced in [START_REF] Decroix | A Formal Approach for Inspecting Privacy and Trust in Advanced Electronic Services[END_REF]. Like our model, it involves multiple stakeholders. This framework was later implemented in IDP [START_REF] Decroix | A Framework for Formal Reasoning about Privacy Properties Based on Trust Relationships in Complex Electronic Services[END_REF]. A distinction is made between storage-trusted and distribution-trusted organizations. The privacy analysis focuses on which data is needed for access to services, and how personal data is distributed between interacting services. By contrast, this paper's model targets interactions between organizations, not services, and investigates how statements about personal data handling, backed with varying levels of evidence, combine with trust perceptions to yield assumptions about the processing of personal data. The approach of using standardized privacy policies to enable accountability by clarifying obligations is widespread. In particular, the idea of combining privacy policies with data handling logs to automatically check compliance ex post appears in [START_REF] Weitzner | Information accountability[END_REF]. The question of the gap between system event logs and logs at the level of abstraction of privacy policies is addressed in [START_REF] Butin | Log Analysis for Data Protection Accountability[END_REF]. The consequences of log design choices for log analysis and accountability are addressed in [START_REF] Butin | Log Design for Accountability[END_REF]. Adequate log design for compliance checking is tricky because of the numerous possible semantic ambiguities. Both papers presume a single data controller rather than the setting of this paper -a constellation of interacting data processors with different, potentially incompatible privacy policies.

Beyond computer science, the scope of application of accountability is a vividly debated issue in the privacy regulation debate [START_REF] Guagnin | Managing Privacy Through Accountability[END_REF]. A key question related to our work is how far data controllers should be required to go to demonstrate compliance. Distinctions are sometimes [START_REF] Bennett | Implementing Privacy Codes of Practice[END_REF] made between different levels of accountability, ranging from public declarations of intent to full technical transparency, such as the one that we advocate here. The adequacy of procedures, i.e. organizational measures, is often discussed. Privacy Impact Assessments are often advocated [START_REF] Wright | Introduction to Privacy Impact Assessment[END_REF] and can be seen as a bridge between accountability of procedures and accountability of practice if the assessment is conducted in sufficient detail. The question of privacy-preserving surveillance infrastructures is addressed in particular in the PARIS project [START_REF]PrivAcy pReserving Infrastructure for Surveillance[END_REF], with an interdisciplinary angle.

We described an accountability inference model and its realization in the IDP knowledge base system. Trust perceptions are taken into account to compute global accountability statements from the individual statements made by interacting entities. We distinguish between different levels of proof for the individual statements, again influencing the resulting global accountability statements. Our approach is illustrated with a scenario involving stakeholders in a railway surveillance infrastructure. The framework is not tied to any particular scenario and can be extended easily. Our representation of data handling evidence is only implicit, and therefore coarse-grained. A more refined approach would model the semantics of log compliance explicitly. This level of detail seems difficult to implement within a first-order logic-based framework. In the current version of the framework, the auditor acting on behalf of an individual is not notified of privacy policy conflicts automatically. Including this aspect would remove the need for manual compatibility checking.

(

  R)ailway Company, (C)amera, (M)onitor, (I)mage Database Statements Stat R.1 (L) Full body pictures with blurred or clear faces, gaits, heights, and behavior are recorded for incident detection. Stat R.2 (D) Collected pictures containing evidence of incidents can be forwarded to legal authorities upon their request. Stat R.3 (L) Pictures are never collected for commercial purposes. Stat R.4 (L) The maximal retention time for any category of collected personal data is 60 days. Stat C.1 (L) Cameras in the station record full body pictures with blurred or clear faces, gaits, heights, and behaviors of travelers for incident detection purposes. Stat M.1 (L) Guards monitor in real-time full body pictures with blurred faces, gaits, heights, and behaviors of travelers in the station for incident detection purposes. Stat I.1 (L) Full body pictures with clear faces are stored as evidence of possible incidents. Stat I.2 (V) Access to stored full body pictures with clear faces is only granted to the image processor upon request of the legal authorities. Stat I.3 (V) Full body pictures with clear faces, gaits, heights, and behavior are never processed for the purpose of identification. Stat I.4 (D) Stored images are deleted after 30 days, unless they are being used as evidence in legal cases. (S)ecurity Company, M(O)bile Device, Status (D)atabase Statements Stat S.1 (D) Time and location of incidents are collected as evidence. Stat S.2 (L) Time and location of incidents are only forwarded to legal authorities upon request. Stat O.1 (V) Surveillance guards collect time and location as evidence in case of incidents. Stat D.1 (V) Time and location of incidents are collected as evidence. Stat D.2 (V) Access to stored time and location of incidents is granted to status processors for gathering evidence. Stat D.3 (V) The time and location of incidents are deleted after 90 days unless they are being used as legal evidence.

Fig. 1 .

 1 Fig. 1. Structure of the global accountability inference model.

typeIDP Listing 1 :

 1 DataCategory = { PersData; Face; BlurredFace; Gait; Height; Behavior ; Location; Time, PictureIncident } DataCategoryOf (DataCategory, DataCategory) = { Face, PictureIncident; BlurredFace, PictureIncident; Gait, PictureIncident; Height, PictureIncident; Behavior , PictureIncident } Partial user model representing personal data categories and hierarchies in the video surveillance scenario.

typeIDP Listing 3 :

 3 Statement = { StatR1 ; StatR2 ; StatR3 ; StatR4 ; . . . } type Purpose = { Evidence; DetectIncident ; Commerce; Identification } type Condition = { RequestLegalAuthority ; NoLegalInvestigation } type Action = { Collecting; Monitoring; Storing; Forwarding; Accessing } type Duration isa int = { 30; 60; 90 } type Permission constructed from { Always; Never } type StatementEvidence constructed from { Declarative; LoggedUnverified ; LoggedVerified } StatementFrom(Statement) : Entity = { StatR1 → RailwayCompany; StatR2 → RailwayCompany; StatR3 → RailwayCompany; StatR4 → RailwayCompany; . . . } StatementSubject(Statement, DataCategory) = { StatR1 , Face; StatR1 , BlurredFace; StatR1 , Gait; StatR1 , Height; StatR1 , Behavior ; StatR2 , PictureIncident; StatR3 , PictureIncident; StatR4 , PersData; . . . } StatementPurpose(Statement, Purpose) = { StatR1 , DetectIncident; StatR2 , Evidence; StatR3 , Commerce; . . . } partial StatementCondtion(Statement) : Condition = { StatR2 → RequestLegalAuthority ; . . . } StatementPermission(Statement) : Permission = { StatR1 → Always; StatR2 → Always; StatR3 → Never ; StatR4 → Always; . . . } partial StatementAction(Statement) : Action = { StatR1 → Collecting; StatR2 → Forwarding; StatR3 → Collecting; . . . } StatementDestination(Statement, Organization) = { StatR2 , LegalAuthority; . . . } partial StatementRetentionLimit(Statement) : Duration = { StatR4 → 60; . . . } StatementNotificationGuarantee(Statement) = { } StatementProof (Statement) : StatementEvidence = { StatR1 → LoggedUnverified ; StatR2 → Declarative; StatR3 → LoggedUnverified ; StatR4 → LoggedUnverified ; . . . } Partial system model representing the statements of the entities involved in the video surveillance scenario.

  and many others. Signs inform passersby that the Railway Company installed Cameras for video surveillance. The cameras provide the railway's Monitors in the control room with real-time video feeds containing Blurred Faces and Gaits of travelers. Furthermore, detailed images of individuals' Full Body and Gait are stored in the railway's Image Database serving as Evidence in legal investigations. Only authorized Image Processors employed by the railway company have access to it. Additionally, surveillance Guards employed by a third-party Security Company patrol in the station. They are authorized to view real-time images on the monitors, and carry a Mobile Device for registering Contextual Data (e.g. time and location) in case of incidents. These devices are connected with the Status Database, property of the security company. It is only accessible for the security company's Status Processors upon request of legal institutions for collecting Evidence.

Table 1 .

 1 Camera surveillance data handling statements. Entity statements are (D)eclarative, (L)ogged-unverified or Logged-and-(V)erified.

  i.e. declarations (with or without proof) about the data processing they perform. A distinction is made between Stakeholders and Components. A stakeholder is either an Organization, or an Operator acting on behalf of exactly one organization. An organization can employ more than one operator. Components are constituents of data processing systems. A component belongs to exactly one organization, but can be used by multiple operators.Components process personal data under the responsibility of the organizations that own them. Organizations or authorities may restrict access to the data categories that a given component is capable of collecting. Authorized categories for a given component are specified using ComponentCanCollect(Component, DataCategory). Listing 2 depicts the IDP specification of the entities involved in the camera surveillance scenario.

	ImageDB, PictureIncident; ImageDB, Gait; ImageDB, Height;
	ImageDB, Behavior ; ImageDB, Time; ImageDB, Location; StatusDB,
	Time; StatusDB, Location; MobileDevice, Time; MobileDevice,
	Location }

type Entity = { RailwayCompany; SecurityCompany; LegalAuthority; Camera; Monitor ; MobileDevice; SurveilanceGuard ; ImageProcessor ; StatusProcessor ; ImageDB; StatusDB } type Stakeholder isa Entity = { RailwayCompany; SecurityCompany; LegalAuthority; SurveilanceGuard ; ImageProcessor ; StatusProcessor } type Component isa Entity = { Camera; Monitor; MobileDevice; ImageDB; StatusDB } type Organization isa Stakeholder = { RailwayCompany; SecurityCompany; LegalAuthority } type Operator isa Stakeholder = { SurveilanceGuard ; ImageProcessor ; StatusProcessor } ComponentOf (Component) : Organization = { Camera → RailwayCompany; Monitor → RailwayCompany; ImageDB → RailwayCompany; StatusDB → SecurityCompany; MobileDevice → SecurityCompany EmployeeOf(Operator) : Organization = { SurveilanceGuard → SecurityCompany; StatusProcessor → SecurityCompany; ImageProcessor → RailwayCompany } OperatorOf (Operator, Component) = { SurveilanceGuard , Monitor ; SurveilanceGuard , MobileDevice; ImageProcessor , ImageDB; StatusProcessor , StatusDB } ComponentCanCollect(Component, DataCategory) = { Camera, Face; Camera, BlurredFace; Camera, PictureIncident; Camera, Gait; Camera, Height; Camera, Behavior ; Monitor, Face; Monitor , BlurredFace; Monitor , PictureIncident; Monitor , Gait; Monitor , Height; Monitor , Behavior ; ImageDB, Face; ImageDB, BlurredFace;

Table 2 .

 2 Global statement evidence deduction rules -the global evidence for the statement S by the entity E owned by the organization O is (U)ncertain or (G)uaranteed for the modeled user.

	StatementProof(S)=	Declared	Logged-unverified	Logged-and-verified
	Naive user

Table 3 .

 3 Worst-case computation rules for deducing GlobalDataCategory(S,DC), the global data categories DC deduced from the individual statement S of entity E, with Sub(S,DC) the subject DC of statement S, and CanCollect(E, DC ) the data categories collectable by E.

Table 4 .

 4 Inferred GAP synthesizing global accountability in the camera surveillance system for user models U1 (1), U2 (2), and U3 (3). The numbers in the table indicate the user models for which the statements in the left column, represented relatively to the different data categories, are valid.

	PictureIncident Face BlurredFace Gait Behavior Time Location PersData
	Global Collection duties
	Actions
	Collecting	3	1,2,3	1,2,3	1,2,3 1,2,3	1,2,3 1,2,3 1,2,3
	Accessing		1,2,3					1,2,3 1,2,3
	Storing	3	1,2,3	3	3	3	3	1,2,3 1,2,3
	Monitoring	3	3	1,2,3	1,2,3 1,2,3	1,2,3	3	3
	Purposes
	All		1,2,3
	DetectIncident	3		1,2,3	1,2,3 1,2,3	1,2,3	3	3
	Evidence	3		3	3	3	3	1,2,3 1,2,3
	Conditions
	Unconditional	3	1,2,3	1,2,3	1,2,3 1,2,3	1,2,3 1,2,3 1,2,3
	Guaranteed		1,2	1,2	1,2	1,2	1,2	1	1
	Global Forward duties
	Actions
	Forwarding
	to LegalAuthority	1,2,3

  The coarse-grained user categorization we use facilitates user modeling since modelers only need to specify user types via a single constant, for instance TypeOfUser = NaiveUser . The model's user types intuitively represent typical real-world users, determining how data subjects appreciate statements and evidence from organizations. They reflect the fact that skeptical users are more difficult to convince of the compliance of actual data handling with declared practices. The user model also addresses the high-level trust perception of users. Namely, UserTrust(O) expresses that a user trusts the organization O.

	nario) is unaffected when new types of users are introduced. Similarly, if an
	auditor collects different samples of statement evidence, only changes to the
	evidence in the statement model are required.
				1	1	1	1	1	1
	Global Retention Limits
	Duration (days)
	60 days	1,2,3	1,2,3	1,2,3	1,2,3 1,2,3	1,2,3		3
	90 days							1,2	1,2
	Conditions
	UnConditional								3
	NoLegalInvestigation	1,2,3	1,2,3	1,2,3	1,2,3 1,2,3	1,2,3 1,2,3 1,2,3
	Guaranteed	1	1	1	1	1	1	1,2	1,2
	Reusing framework components. The framework consists of modular compo-
	nents, making possible isolated changes to one part while leaving the others
	intact. A given system model (e.g. the railway station camera surveillance sce-

element must be related to the Entity "ImageDatabase", the Permission "Always", and to the StatementEvidence "Declarative". Furthermore, each duty is related to the Action "Store". Users model.

For the complete model of the statements, see https://code.google.com/p/ inferring-accountability/.

A detailed IDP realization -together with the output containing the GAPs for the three user models -can be found at https://code.google.com/p/ inferring-accountability/.

Acknowledgement This work was funded by the Flemish agency for Innovation by Science and Technology (IWT), the European project PARIS / FP7-SEC-2012-1 and the Inria Project Lab CAPPRIS.