Thibaud Antignac
email: thibaud.antignac@inria.fr

Daniel Le Métayer
email: daniel.le-metayer@inria.fr

Privacy Architectures: Reasoning About Data Minimisation and Integrity ⋆

Privacy by design will become a legal obligation in the European Community if the Data Protection Regulation eventually gets adopted. However, taking into account privacy requirements in the design of a system is a challenging task. We propose an approach based on the specification of privacy architectures and focus on a key aspect of privacy, data minimisation, and its tension with integrity requirements. We illustrate our formal framework through a smart metering case study.

Introduction

The philosophy of privacy by design is that privacy should not be treated as an afterthought but as a first-class requirement in the design of IT systems. Privacy by design will become a legal obligation in the European Community if the Data Protection Regulation [11] eventually gets adopted. However, from a technical standpoint privacy by design is a challenging endeavour: first, privacy is a multifaceted notion stemming from a variety of principles1 which are generally not defined very precisely; in addition, these requirements may be (or may seem to be) in tension with other requirements such as functional requirements, ease of use or performances. To implement these requirements, a wide array of privacy enhancing technologies (PETs) are available 2 . Each of these techniques provides different guarantees based on different assumptions and therefore is suitable in different contexts. As a result, it is quite complex for a software engineer to make informed choices among all these possibilities and to find the most appropriate combination of techniques to solve his own requirements. Solutions have been proposed in different application domains such as smart metering [START_REF] Garcia | Privacy-friendly energy-metering via homomorphic encryption[END_REF][START_REF] Rial | Privacy-Preserving smart metering[END_REF], payas-you-drive [START_REF] Balasch | PrETP: Privacy-Preserving electronic toll pricing[END_REF][START_REF] De Jonge | Privacy-Friendly electronic traffic pricing via commits[END_REF], or location-based systems [START_REF] Krumm | A survey of computational location privacy[END_REF] but the next challenge in this area is to go beyond individual cases and to establish sound foundations and methodologies for privacy by design [START_REF] Diaz | Privacy preserving electronic petitions[END_REF][START_REF] Tschantz | Formal methods for privacy[END_REF]. In this paper, we advocate the idea that privacy by design should be addressed at the architectural level, because it makes it possible to abstract away unnecessary details, and should be supported by a formal model. The fact that not all aspects of privacy are susceptible to formalisation is not a daunting obstacle to the use of formal methods for privacy by design: the key issue is to be able to build appropriate models for the aspects of privacy that are prone to formalisation and involve complex reasoning. Data minimisation, which is one of the key principles of most privacy guidelines and regulations, is precisely one of these aspects. Data minimisation stipulates that the collection and processing of personal data should always be done with respect to a particular purpose and the amount of data strictly limited to what is really necessary to achieve the purpose [11].

In this paper, data minimisation requirements are expressed as properties defining for each stakeholder the information that he is (or is not) allowed to know. Data minimisation would not be so difficult to achieve if other, sometimes conflicting, requirements did not have to be met simultaneously. Another common requirement, which we call "integrity" in the sequel, is the fact that some stakeholders may require guarantees about the correctness of the result of a computation. In fact, the tension between data minimisation and integrity is one of the delicate issues to be solved in many systems involving personal data.

In Section 2 we propose a language to define privacy architectures. In Section 3, we introduce a logic for reasoning about architectures and show the correctness and completeness of its axiomatisation. This axiomatisation is used in Section 4 to prove that an example of smart metering architecture meets the expected privacy and minimisation requirements. Section 5 discusses related work and Section 6 outlines directions for further research.

Privacy Architectures

Many definitions of architectures have been proposed in the literature. In this paper, we adopt a definition inspired by [START_REF] Bass | Software Architecture in Practice[END_REF] 3 : The architecture of a system is the set of structures needed to reason about the system, which comprise software and hardware elements, relations among them and properties of both. The atomic components of an architecture are coarse-grain entities such as modules, components or connectors. In the context of privacy, the components are typically the PETs themselves and the purpose of the architecture is their combination to achieve the requirements of the system.

The meaning of the requirements considered here (minimisation and integrity) depends on the purpose of the data collection, which is equated to the expected functionality of the system here. In the sequel, we assume that this functionality is expressed as the computation of a set of equations4 Ω such that Ω = X = T with terms T defined as shown in Table 1. X represents (potentially indexed) variables and X simple variables (X ∈ Var), k index variables (k ∈ Index), Cx constants (Cx ∈ Const), Ck index constants (Ck ∈ N5 ), F functions (F ∈ F un) and ⊙F (X) is the iterative application of function F to the elements of the array denoted by X (e.g. sum of the elements of X if F is equal to +). We assume that each array variable X represents an array of fixed size Range(X).

T ::= X | Cx | F (T1, . . . , Tn) | ⊙F (X) X ::= X | XK K ::= k | Ck Table 1. Term Language.
In the following subsections, we introduce our privacy architecture language (Subsection 2.1) and its semantics (Subsection 2.2).

Privacy Architecture Language

We define an architecture as a set of components C i , i ∈ [1, . . . , n] associated with relations describing their capabilities. These capabilities depend on the set of available PETs. For the purpose of this paper, we consider the architecture language described in Table 2. Subscripts i and j are component indexes and the notation {Z} is used to define a set of terms of category Z. Has i ( X) expresses the fact that variable X is an input variable located at component C i (e.g. sensor or meter) and Receive i,j ({S}, { X}) specifies that component C i can receive from component C j messages consisting of a set of statements {S} and a set of variables { X}. A statement can be either a proof of a set of properties P (denoted by Proof i ({P })) or an attestation (denoted by Attest i ({Eq})), that is to say a simple declaration by a component C i that properties Eq are true. A component can also compute a variable defined by an equation X = T (denoted by Compute i ( X = T )), check that a set of properties Eq holds (denoted by Check i ({Eq})), verify a proof of a property Pro received from another component (denoted by Verif P roof i (Pro)), verify the origin of an attestation (denoted by Verif Attest i (Att)), or perform a spotcheck. A spotcheck, which is denoted by Spotcheck i,j (X k , Eq), is the request from a component C j of a value X k taken from array X and the verification that this value satisfies property Eq. Primitive properties Eq are simple equations on terms T . Last but not least, trust assumptions are expressed using Trust i,j (meaning that component C i trusts component C j ). In the sequel, we use Γ to denote the set of architectures following the syntax of Table 2. Architectures can also be defined using graphical representations. As an illustration, Figure 1 displays a simple architecture involving a meter M and the central server of a provider P . The meter plays both the role of a sensor providing the input consumption values (Has M (Cons t )) and the role of a secure element computing the fee. Because the provider trusts the meter (Trust P,M ), it merely checks the certificate Attest M ({Fee = ⊙ + (y) , y t = F (x t ) , x t = S (Cons t )}) sent by the meter. Strictly speaking, we should introduce a notion of actor and a relationship between actors and the components that are under their control but, for the sake of brevity (and without loss of generality6 ), we do not distinguish between components and actors here.

A ::= {R} R ::= Hasi X | Receivei,j {S}, { X} | Compute i X = T | Checki ({Eq}) | Verif Proof i (Pro) | Verif Attest i (Att) | Spotcheck i,j (X k , Eq) | Trusti,
Has M (Cons) Compute M (Fee = § +(y)) Compute M (y t = F (x t )) Compute M (x t = S (Cons t )) Meter M Verif P Q a Attest M Q a Y ] [ Fee = § +(y) , y t = F (x t ) , x t = S (Cons t ) Z \R b R b Central Server of the Provider P Receive P,M Q a Y ] [ Attest M Q a Y ] [ Fee = § +(y) , y t = F (x t ) , x t = S (Cons t ) Z \R b Z \ , {Fee} R b Trust P,M
Architectures provide an abstract, high-level view of a system: for example, we do not express at this level the particular method (for example, a zeroknowledge proof protocol) used by a component to build a proof (Proof i ({P })) or to verify it, or to check that another component has actually certified (attested) a property (Verif Attest i (Att)). Another main departure from protocol specification languages is that we do not have any specific ordering or notion of sequentiality here, even though functional dependencies introduce implicit constraints in the events of the system, as discussed below. The objective is to express and reason about the main design choices rather than to cover all the development steps.

Privacy Architectures Semantics

The definition of the semantics of an architecture is based on its set of compatible traces. A trace is a sequence of high-level events occurring in the system as presented in Table 3. Events can be seen as instantiated relations of the architecture. For example, a Receive i,j {S}, { X : V } event specifies the values V of the variables X received by C i . Similarly, Spotcheck i,j (X Ck : V, {Eq}) specifies the specific index Ck (member of N) chosen by C i for the spotcheck and the value V of X Ck . All variable indexes occurring in events, except for variables occurring in the properties of Receive i,j , Verif Proof i , Verif Attest i , and Spotcheck i,j , must belong to N.

θ ::= Seq(ǫ) ǫ ::= Hasi X : V | Receivei,j {S}, { X : V } | Compute i X = T | Checki ({Eq}) | Verif Proof i (Pro) | Verif Attest i (Att) | Spotcheck i,j (X Ck : V, {Eq})
Table 3. Events and traces.

In the following, we consider only consistent architectures and consistent traces. An architecture is said to be consistent if each variable can be computed (or can be initially possessed, as expressed by Has i ) by a single component, a component cannot receive a variable from different sources, a component computing a variable or checking a property can receive or compute all the necessary input variables (variables occuring in T for Compute i ( X = T ), in Eq for Check i (Eq)), a component can only verify properties that it can receive from another component, etc. The same kind of consistency assumptions apply to traces, in addition to ordering consistency properties (variables and properties are not used before being received or computed).

We use Event to denote the set of events ǫ and Trace to denote the set of consistent traces θ.

Definition 1 (Compatibility). A trace θ of length θ is compatible with an architecture A if and only if:

∀a ∈ [1, θ], if θ a = Compute i X = T then ∃α ∈ A, C(θ a , α) and if θ a = Spotcheck i,j (X Ck : V, {Eq}) then ∀b ∈ [1, θ], b = a ⇒ ∀k ′ , V ′ , Eq ′ , θ b = Spotcheck i,j X k ′ : V ′ , {Eq ′ }

where C(ǫ, α) holds if and only if ǫ can be obtained from α by adding specific values V for variables and instantiating index variables to integer values.

The first condition in the definition of compatibility states that, except for compute events, only events which are instantiations of components of the architecture A can appear in the trace θ. The rationale for excepting compute events is the need to express the potential actions of a curious agent trying to derive the value of a variable X from the values of variables that he already has. As a result, compatible traces may include computations that are not contemplated by the architecture, provided that the component possesses all the variables necessary to perform this computation (consistency assumption). The adversary model considered here includes computation of new variables, erroneous computations, and communication of incorrect values, which corresponds to Dolev-Yao attacks for internal stakeholders (except they cannot break the protocol). The second condition expresses the fact that spotchecks can be performed only once. This condition could be relaxed through the introduction of an additional threshold parameter t to express the fact that up to t spotchecks are possible. We denote by T (A) the set of compatible traces of an architecture A.

In order to define the semantics of events, we introduce first the notion of state of a component:

State = (State V × State P × State P ) ∪ {Error} State V = (Var → Val ⊥ ) State P = {{Eq} ∪ {Trust i,j }}
The state of a component is either the error state Error or a triple made of a variable state assigning a value (or the undefined value ⊥ 7 ) to each variable and two property states: the first one defines the set of properties known by the component and the second one the set of properties believed by the component (after a spotcheck). In the sequel, we use σ to denote the global state (state of the components C 1 , . . . , C n ) defined on State n . The initial state for an architecture A is denoted by

Init A = Init A 1 , . . . , Init A n with: ∀i ∈ [1, n], Init A i = (Empty, {Trust i,j |Trust i,j ∈ A}, ∅)
where Empty denotes the empty variable state (∀X ∈ Var, Empty(X) = ⊥). The only information contained in the initial state is the trust properties specified by the architecture.

The semantics function S T is defined in Table 4. It specifies the impact of a trace on the state of each component C i . It is defined as an iteration through the trace with function S E defining the impact of each type of event on the states of the components.

The notation ǫ.θ is used to denote a trace whose first element is ǫ and the rest of the trace is θ. Each event modifies only the state of the component C i . 7 Please note that ⊥ is used to denote undefined values, that is to say values which have not been set, as opposed to error values (e.g. division by zero or type errors). We do not consider computation error values here.

ST : Trace × State n → State n SE : Event × State n → State n ST ( , σ) = σ ST (ǫ.θ, σ) = ST (θ, SE(ǫ, σ)) SE Hasi X : V , σ = σ[σi/(σ v i [ X/V ], σ pk i , σ pb i )] SE Receivei,j {S}, { X : V } , σ = σ[σi/(σ v i [{ X/V }], σ pk i , σ pb i )] SE Compute i X = T , σ = σ[σi/(σ v i [ X/ε(T, σ v i )], σ pk i ∪ { X = T }, σ pb i )] SE (Checki (E) , σ) = σ[σi/(σ v i , σ pk i ∪ E, σ pb i )] if ∀Eq ∈ E, ε(Eq, σ v i ) = True = σ[σi/Error] otherwise SE Verif Proof i Proof j (E) , σ = σ[σi/(σ v i , σ pk i ∪ {Eq|Eq ∈ E or (Attest j ′ (E ′ ) ∈ E and
Eq ∈ E ′ and

Trust i,j ′ ∈ σ pk i )}, σ pb i )] if Verif Proof ((E) , σ v i ) = True = σ[σi/Error] otherwise SE Verif Attest i (Attestj(E)) , σ = σ[σi/(σ v i , σ pk i ∪ {Eq|Eq ∈ E and Trusti,j ∈ σ pk i }, σ pb i )] if Verif Attest ((E) , σ v i ) = True = σ[σi/Error] otherwise SE Spotcheck i,j (X Ck : V, E) , σ = σ[σi/(σ v i [X Ck /V ], σ pk i , σ pb i ∪ E)] if ∀Eq ∈ E, ε(Eq[k/Ck], σ v i [X Ck /V ]) = True = σ[σi/Error] otherwise Table 4. Semantics of traces of events.
This modification is expressed as σ[σ i /(v, pk, pb)] (or σ[σ i /Error] in the case of the error state) that replaces the variable and property components of the state of C i by v, pk, and pb respectively. We assume that no event θ a ′ with a ′ > a involves component C i if its state σ i is equal to Error after the occurrence of θ a (in other words, any error in the execution of a component causes this component to stop).

The effect of Has i and Receive i,j on the variable state of component C i is the replacement of the values of the variables X by new values V ∈ Val, which is denoted by

σ v i [ X/V ].
The effect of Compute i ( X = T ) is to set the variable X to the evaluation of the value of T in the current variable state σ v i of C i , which is defined by ε(T, σ v i ). Spotcheck i (X Ck : V, E) sets the value of X Ck to V . The other events do not have any effect on the variable state of C i . The value of a variable replaced after the occurrence of an event must be ⊥ before its occurrence 8 . We assume that it is different from ⊥ and does not involve any ⊥) after the event 9 .

Most events also have an effect on the property states. This effect is the addition to the property states of the new knowledge or belief provided by the event. For Compute i X = T , this new knowledge is the equality X = T ; for the Check i , Verif i , and Spotcheck i,j events, the new knowledge is the properties checked or verified. In all cases except for Spotcheck i,j these properties are added to the pk property state because they are known to be true by component C i ; in the case of Spotcheck i,j the properties are added to the pb property state because they are believed by C i : they have been checked on a sample value X Ck but might still be false for some other X k . The only guarantee provided to C i by Spotcheck i,j is that C i has always the possibility to detect an error (but he has to choose an appropriate index, that is to say an index that will reveal the error).

Functions Verif

Proof and Verif Attest define the semantics of the corresponding verification operations. As discussed above, we do not enter into the internals of the proof and attestation verifications here and just assume that only true properties are accepted by Verif Proof and only attestations provided by the authentic sender are accepted by Verif Attest . The distinctive feature of Verif Attest i events is that they generate new knowledge only if the author of the attestation can be trusted (hence the Trust i,j ∈ A condition).

Let us note also that Receive i,j events do not add any new knowledge by themselves because the received properties have to be verified before they can be added to the property states.

We can now define the semantics of an architecture A as the set of the possible states produced by compatible traces.

Definition 2 (Semantics of architectures.). The semantics of an architecture A is defined as:

S(A) = {σ ∈ State n | ∃θ ∈ T (A), S T (θ, Init A ) = σ}.
In the following, we use S i (A) to denote the subset of S(A) containing only states which are well defined for component

C i : S i (A) = {σ ∈ S(A) | σ i = Error}.
The prefix ordering on traces gives rise to the following ordering on states:

∀σ ∈ S i (A), ∀σ ′ ∈ S i (A), σ ≥ i σ ′ ⇔ ∃θ ∈ T (A), ∃θ ′ ∈ T (A), σ = S T (θ, Init A ), σ ′ = S T (θ ′ , Init A )
, and θ ′ is a prefix of θ.

Privacy Logic

Because privacy is closely connected with the notion of knowledge, epistemic logics form an ideal basis to reason about privacy properties. Epistemic logics [START_REF] Fagin | Reasoning About Knowledge[END_REF] are a family of modal logics using a knowledge modality usually denoted by K i (ψ) to denote the fact that agent i knows the property ψ. However standard epistemic logics based on possible worlds semantics suffer from a weakness which makes them unsuitable in the context of privacy: this problem is often referred to as "logical omniscience" [START_REF] Halpern | Dealing with logical omniscience[END_REF]. It stems from the fact that agents know all the logical consequences of their knowledge (because these consequences hold in all possible worlds). An undesirable outcome of logical omniscience would be that, for example, an agent knowing the hash H (v) of a value v would also know v. This is obviously not the intent in a formal model of privacy where hashes are precisely used to hide the original values to the recipients. This issue is related to the fact that standard epistemic logics do not account for limitations of computational power.

Therefore it is necessary to define dedicated epistemic logics to deal with different aspects of privacy and to model the variety of notions at hand (e.g. knowledge, zero-knowledge proof, trust, etc.). In this paper, we follow the "deductive algorithmic knowledge" approach [START_REF] Fagin | Reasoning About Knowledge[END_REF][START_REF] Pucella | Deductive algorithmic knowledge[END_REF] in which the explicit knowledge of a component C i is defined as the knowledge that this component can actually compute using his own deductive system ⊲ i . The deductive relation ⊲ i is defined here as a relation between a set of Eq and Eq properties: {Eq 1 , . . . , Eq n } ⊲ i Eq 0 . Typically, ⊲ i can be used to capture properties of the functions of the specification. For example {h 1 = H (x 1 ) , h 2 = H (x 2 ) , h 1 = h 2 }⊲ i (x 1 = x 2 ) expresses the injectivity property of a hash function H. Another relation, Dep i , is introduced to express that a variable can be derived from other variables. Dep i X, X1 , . . . Xn means that a value for X can be obtained by C i (∃F, X = F ( X1 , . . . , Xn )). The absence of a relation such as Dep i (x k , {y k }) prevents component C i from deriving the value of x k from the value of y k , capturing the hiding property of the hash application y k = H (x k ).

φ ::= Has all i X | Has none i X | Has one i X | Ki (Eq) | Bi (Eq) | φ1 ∧ φ2 Eq ::= T1 Rel T2 | Eq1 ∧ Eq2 Table 5. Architecture logic.
This logic involves two modalities, denoted by K i and B i , which represent respectively knowledge and belief properties of a component C i . Please note that the Eq notation (already used in the language of architectures) is overloaded, without ambiguity: it is used to denote conjunctions (rather than sets) of primitive relations in the logic. The logic can be used to express useful properties of architectures: for example Has all i ( X) expresses the fact that component C i can obtain or derive (using its deductive system ⊲ i ) the value of Xk for all k in Range(X). Has one i ( X) expresses the fact that component C i can obtain or derive the value of X k for at most one k in Range(X). Finally, Has none i ( X) is the privacy property stating that C i does not know any X k value. It should be noted that Has i properties only inform on the fact that C i can get or derive some values for the variables but they do not bring any guarantee about the correctness of these values. Such guarantees can only be ensured through integrity requirements, expressed using the K i (Eq) and B i (Eq) properties. K i (Eq) means that component C i can establish the truthfulness of Eq while B i (Eq) expresses the fact that C i may test this truthfulness, and therefore detect its falsehood or believe that the property is true otherwise.

We can now define the semantics of a property φ.

Definition 3 (Semantics of properties). The semantics S(φ) of a property

φ is defined in Table 6 as the set of architectures meeting φ. An architecture satisfies the Has all i ( X) property if and only if C i may obtain the full value of X in at least one compatible execution trace whereas Has none i ( X) holds if and only if no execution trace can lead to a state in which C i gets a value of X (or of any part of its content if X is an array variable). Has one i ( X) is true if and only if no execution trace can lead to a state in which C i knows more than one of the values of the array X. The validity of K i (Eq) and B i (Eq) properties is defined with respect to correct execution traces (with respect to C i ) since an incorrect trace leads to a state in which an error has been detected by the component 10 . The condition σ ≥ σ ′ is used to discard states corresponding to incomplete traces in which the property Eq has not yet been established. As discussed above, the capacity for a component C i to derive new knowledge or beliefs is defined by its deductive system ⊲ i .

A ∈ S Has all i X ⇔ ∃σ ∈ S(A), σ v i ( X) does not contain any ⊥ A ∈ S Has none i X ⇔ ∀σ ∈ S(A), σ v i ( X) = ⊥ A ∈ S Has one i X ⇔ ∀σ ∈ S(A), σ v i ( X) = ⊥ ∨ (σ v i ( X) = < v1, . . . , v k > ∧ ∄(u, u ′ ), u = u ′ ∧ vu = ⊥ ∧ v u ′ = ⊥) A ∈ S (Ki (Eq)) ⇔ ∀σ ′ ∈ Si(A), ∃σ ∈ Si(A), ∃Eq ′ , (σ ≥i σ ′ ) ∧ (σ pk i ⊲i Eq ′ ) ∧ (Eq ′ ⇒ Eq) A ∈ S (Bi (Eq)) ⇔ ∀σ ′ ∈ Si(A), ∃σ ∈ Si(A), ∃Eq ′ 1 , ∃Eq ′ 2 , (σ ≥i σ ′ )∧ (σ pb i ⊲i Eq ′ 1 ) ∧ (σ pk i ⊲i Eq ′ 2 ) ∧ Eq ′ 1 ∧ Eq ′ 2 ⇒ Eq A ∈ S (φ1 ∧ φ2) ⇔ A ∈ S(φ1) ∧ A ∈ S(φ2)
In order to reason about architectures and the knowledge of the components, we introduce in Table 7 an axiomatisation of the logic presented in the previous section. The fact that an architecture A satisfies a property φ is denoted by A ⊢ φ. Axioms (H1-8) and (HNO) are related to properties Has i while axioms (K1-5) and (K∧) are related to the knowledge of the components. Axioms (B), (KB), and (B∧) handle the belief case. Finally, the remaining axioms are structural axioms dealing with the conjunctive operator.

H1

Hasi

X ∈ A A ⊢ Has all i X H2 Receivei,j (S, E) ∈ A X ∈ {E} A ⊢ Has all i X H3 Compute i X = T ∈ A A ⊢ Has all i X H4 Spotcheck i,j (X k , E) ∈ A A ⊢ Has one i (X) H5 Dep i X, X1 , . . . Xn for all l ∈ [1, n], A ⊢ Has all i Xl A ⊢ Has all i X

H6

None of the pre-conditions of H1, H2, H3, H4, or H5 holds for X or any

X k A ⊢ Has none i X H7 A ⊢ Has all i X A ⊢ Has all i (X k ) for all k ∈ Range(X) HNO A ⊢ Has none i X A ⊢ Has one i X H8 A ⊢ Has none i X A ⊢ Has none i (X k ) for all k ∈ Range(X) K1 Compute i X = T ∈ A A ⊢ Ki( X = T ) K3 Verif Proof i Proof j (E) ∈ A Eq ∈ E A ⊢ Ki(Eq) K2 Checki (E) ∈ A Eq ∈ E A ⊢ Ki(Eq) K4 Verif Proof i Proof j (E) ∈ A Attest k (E ′ ) ∈ E Trust i,k ∈ A Eq ∈ E ′ A ⊢ Ki(Eq) K5 Verif Attest i (Attestj(E)) ∈ A Trusti,j ∈ A Eq ∈ E A ⊢ Ki(Eq) KB A ⊢ Ki(Eq) A ⊢ Bi(Eq) K∧ A ⊢ Ki(Eq 1 ) A ⊢ Ki(Eq 2 ) A ⊢ Ki(Eq 1 ∧ Eq 2 ) B Spotcheck i,j (X k , E) ∈ A Eq ∈ E A ⊢ Bi(Eq) K⊲ E ⊲i Eq 0 for all Eq ∈ E, A ⊢ Ki(Eq) A ⊢ Ki(Eq 0 ) I∧ A ⊢ φ1 A ⊢ φ2 A ⊢ φ1 ∧ φ2 B∧ A ⊢ Bi(Eq 1 ) A ⊢ Bi(Eq 2 ) A ⊢ Bi(Eq 1 ∧ Eq 2 ) B⊲ E ⊲i Eq 0 for all Eq ∈ E, A ⊢ Bi(Eq) A ⊢ Bi(Eq 0 ) Table 7. Axiomatics.
The axiomatics meets the following soundness, completeness, and decidability properties.

Property 1 (Soundness). For all

A in Γ, if A ⊢ φ then A ∈ S (φ).
The soundness property can be proved by considering each rule in Table 7 in turn and showing that the traces specified in Table 6 have the expected properties (or that appropriate traces can be found in the case of Has all i ).

Property 2 (Completeness). For all

A in Γ, if A ∈ S (φ) then A ⊢ φ.
Completeness can be proved by systematic inspection of the different cases in Table 4 that can make a property φ true in the trace semantics.

Property 3 (Decidability). If the deductive systems ⊲ i are decidable, then the axiomatics is decidable.

The intuition is that proofs can be stratified into proofs of Has all i , Has none i , Has one i , K i , and B i successively, with proofs of properties not involving the deductive systems of the components first and those involving the deductive systems of the components as the last step.

Smart Meter Case Study

One of the services provided by smart metering systems is the periodic billing of an amount Fee based on the customers consumption Cons t for periods of time t. The service Fee = t (F (S (Cons t ))) (where F and S stand for pricing and metering) is expressed as Ω = {Fee = ⊙ + (y), y t = F (x t ), x t = S(Cons t )}. We provide the details for the provider only here but a similar approach could be used for customers or other parties.

Architecture Goals. The architecture should enable the provider P to get access to the global fee: A ⊢ Has all P (Fee). However, he should not be able to get access to the individual consumptions Cons t or to the intermediate variables x and y since they are the results of easily inversible functions (typically F is a mapping and S the identity): A ⊢ Has none P (Cons) ∧ Has none P (x) ∧ Has none P (y). Moreover, he should be convinced that the value provided for Fee is actually correct: A ⊢ K P (Fee = ⊙ + (y) ∧ y t = F (x t ) ∧ x t = S(Cons t )).

Architecture Design. The design of an architecture meeting the above goals is described Figure 1. A strong constraint concerning the metering has to be taken into account from the start: regulators generally require the data to be metered by officially certified and tamper-resistant metrological devices M : Has M (Cons), Compute M (x t = S (Cons t )), and Attest M (x t = S (Cons t )).

One option for the computation of the fee is to have it performed by the meter: Compute M (Fee = ⊙ + (y)) and Compute M (y t = F (x t )). The result of this computation can then be sent to the provider along with the corresponding attestation and the metering attestation through a Receive P,M ({Att} , {Fee}) primitive. Another architectural primitive Verif Attest P (Att) should be added to convince the provider of the correctness of the computation (considering that the provider trusts the meter Trust P,M ).

Finally, the dependance relations have to be defined to model the computational power of the components P and M (they both have the same here for the sake of simplicity, noted Dep i for i ∈ {P, M }). The relations are such that (Fee, {y t }) ∈ Dep i , (y t , {x t }) ∈ Dep i , (x t , {y t }) ∈ Dep i , (x t , {Cons t }) ∈ Dep i , and (Cons t , {x t }) ∈ Dep i (only the summation is not inversible here and we have (y t , {Fee}) / ∈ Dep i ).

Application of the Axiomatics. Rules (H2) and (H6) allow us to prove respectively that the provider gets a value for the global fee since it receives it from the meter and that the consumption and the values of the intermediate variables x and y are not disclosed. Applications of rules (K5) and (K∧) prove that the correctness of the global fee is ensured thanks to the attestations and the trust relation between the provider and the meter. As expected, (H2) and (H3) prove that the meter has an access to the consumption data.

The solution chosen here for the sake of conciseness describes heavy meters performing the billing computations (which is generally not the case). Moreover, there is a direct link between the meter and the provider: the customer has to trust the meter not to disclose too much data to the provider. This issue could be solved by adding a proxy under the control of the customer which would filter the communications between the provider and the meter. Other options for smart metering such as [START_REF] Rial | Privacy-Preserving smart metering[END_REF] can be expressed in the same framework but space considerations prevent us from presenting them here.

Related Work

This paper stands at the crossroads of three different areas: engineering privacy by design, software architectures and protocols, and epistemic logics.

Several authors [START_REF] Gürses | Engineering Privacy by Design[END_REF][START_REF] Kerschbaum | Privacy-preserving computation[END_REF][START_REF] Métayer | Privacy by design: A formal framework for the analysis of architectural choices[END_REF][START_REF] Mulligan | Bridging the gap between privacy and design[END_REF][START_REF] Spiekermann | Engineering privacy[END_REF] have already pointed out the complexity of "privacy engineering" as well as the "richness of the data space" [START_REF] Gürses | Engineering Privacy by Design[END_REF] calling for the development of more general and systematic methodologies for privacy by design. As far as privacy mechanisms are concerned, [START_REF] Kerschbaum | Privacy-preserving computation[END_REF][START_REF] Maffei | Security and privacy by declarative design[END_REF] points out the complexity of their implementation and the large number of options that designers have to face. To address this issue and favor the adoption of these tools, [START_REF] Kerschbaum | Privacy-preserving computation[END_REF] proposes a number of guidelines for the design of compilers for secure computation and zeroknowledge proofs whereas [START_REF] Fournet | Zql: A compiler for privacypreserving data processing[END_REF] provides a language and a compiler to perform computations on private data by synthesising zero-knowledge protocols. In a different context (designing information systems for the cloud), [START_REF] Manousakis | Privacy in the cloud: Bridging the gap between design and implementation[END_REF] also proposes implementation techniques to make it easier for developers to take into account privacy and security requirements.

Software architectures have been an active research topic for several decades [START_REF] Shaw | The golden age of software architecture[END_REF] but they are usually defined using purely graphical, informal means or within semi-formal frameworks. Dedicated languages have been proposed to specify privacy properties [START_REF] Barth | Privacy and contextual integrity: framework and applications[END_REF][START_REF] Becker | A Practical Generic Privacy Language[END_REF][START_REF] Métayer | A Formal Privacy Management Framework[END_REF][START_REF] Yu | A formal semantics for P3P[END_REF] but the policies expressed in these languages are usu-ally more fine-grained than the properties considered here because they are not intended to be used at the architectural level. Similarly, process calculi such as the applied π-calculus [START_REF] Ryan | Formal Models and Techniques for Analyzing Security Protocols[END_REF] have been applied to define privacy protocols [START_REF] Delaune | Verifying privacy-type properties of electronic voting protocols: A taster[END_REF]. Because process calculi are general frameworks to model concurrent systems, they are more powerful than dedicated frameworks. The downside is that protocols in these languages are expressed at a lower level and the tasks of specifying a protocol and its expected properties are more complex [START_REF] Meadows | Formal methods for cryptographic protocol analysis: emerging issues and trends[END_REF][START_REF] Paulson | The inductive approach to verifying cryptographic protocols[END_REF][START_REF] Burrows | A logic of authentication[END_REF]. Again, the main departure of the approach advocated in this paper with respect to this trend of work is that we reason at the level of architectures, providing ways to express properties without entering into the details of specific protocols that we assume perfect. The work presented here is a follow-up of [START_REF] Antignac | Privacy by design: From technologies to architectures[END_REF] which advocates an approach based on formal models of privacy architectures. The framework introduced in [START_REF] Métayer | Privacy by design: A formal framework for the analysis of architectural choices[END_REF] includes an inference system to reason about the implementation of a "detectability property" similar to the integrity property considered here. This framework makes it possible to prove that, in a given architecture, an actor "A" can detect potential errors (or frauds) in the computation of a variable "X". The logical framework presented here can be seen as a generalisation of [START_REF] Métayer | Privacy by design: A formal framework for the analysis of architectural choices[END_REF] which does not include a logic for defining privacy and integrity properties.

Epistemic logics have been extensively studied [START_REF] Fagin | Reasoning About Knowledge[END_REF]. A difficulty in this kind of framework in a context where hiding functions are used is the problem known as "logical omniscience". Several ways to solve this difficulty have been proposed [START_REF] Pucella | Deductive algorithmic knowledge[END_REF][START_REF] Halpern | Dealing with logical omniscience[END_REF][START_REF] Cohen | A complete axiomatization of knowledge and cryptography[END_REF]. Other works such as [START_REF] Glasgow | A logic for reasoning about security[END_REF] also rely on deontic logics and focus on the expression of policies and how they relate to database security or distributed systems.

Directions for Further Work

The framework presented in this paper can be used to express in a formal way the main architectural choices in the design of a system and to reason about them. It also makes it possible to compare different options, based on the properties that they comply with, which is of prime importance when privacy requirements have to be reconciled with other, apparently conflicting requirements.

As stated above, the framework described here does not cover the full development cycle: ongoing work addresses the mapping from the architecture level to the protocol level to ensure that a given implementation, abstracted as an applied π-calculus protocol [START_REF] Ryan | Formal Models and Techniques for Analyzing Security Protocols[END_REF], is consistent with an architecture. Work is also ongoing to integrate this formal framework into a more user-friendly, graphical, design environment integrating a pre-defined design strategy. This strategy, which is implemented as a succession of question-answer iterations, allows the designer to find his way among all possible design options based on key decision factors such as the trust assumptions between entities. The resulting architectures can then be checked using the formal framework described here.

In this paper, we have focused on data minimisation and it should be clear that the framework presented here does not address other privacy requirements such as the purpose limitation or the deletion obligation. Indeed, privacy is a multi-faceted notion that cannot be entirely captured within a single formal framework. Another limitation of the approach is that it must be possible to define the service (or "purpose") as the result of a functional expression (e.g. the computation of a fee in electronic toll pricing or smart metering). Thus the approach does not help in situations such as social networks where the service is just the display of the data (and its access based on a given privacy policy). Last but not least, in this paper, follow a "logical" (or qualitative) approach, as opposed to a quantitative approach to privacy and we do not consider the use of auxiliary information. An avenue for further research in this area would be to study the integration of quantitative measures of privacy (such as differential privacy [START_REF] Dwork | Differential privacy[END_REF]) into the framework.

  j S ::= Pro | Att Att ::= Attesti ({Eq}) Pro ::= Proof i ({P}) Eq ::= T1 Rel T2 P ::= Att | Eq Rel ::= = | < | > | ≤ | ≥

Fig. 1 .

 1 Fig. 1. Example of smart metering architecture.

Table 2 .

 2 Privacy Architecture Language.

Table 6 .

 6 Semantics of properties.

These principles include collection limitation, data quality, purpose specification, use limitation, security, openness, individual participation, accountability, etc.

For example homomorphic encryption, zero-knowledge proof, secure multi-party computation, private information retrieval, anonymous credentials, anonymous communication channels, etc.

This definition is a generalisation (to system architectures) of the definition of software architectures proposed in[START_REF] Bass | Software Architecture in Practice[END_REF].

[START_REF] Bass | Software Architecture in Practice[END_REF] Which is typically the case for systems involving integrity requirements.

Set of natural numbers.

The fact that an actor controls several components can be expressed through a trust relationship.

Because we consider only consistent traces. A value different from ⊥ would mean that the variable is computed or set more than once.

In other words, input values and results of computations are fully defined.

This is a usual implicit assumption in protocol verification.

Acknowledgement. This work was partially funded by the European project PRIPARE/FP7-ICT-2013-1.5, the ANR project BIOPRIV, and the Inria Project Lab CAPPRIS.