A quantification of process's security by differential privacy is defined and studied in the framework of probabilistic process algebras. The resulting (quantitative) security properties are studied and compared with other (qualitative) security notions. Several formulations of system security can be found in the literature. Many of them are based on a non-interference (see [GM82]) which assumes an absence of any information flow between private and public systems activities. More precisely, systems are considered to be secure if from observations of their public activities no information about private activities can be deduced. This approach has found many reformulations for different formalisms, computational models and nature or “quality” of observations. For many applications such properties could be criticized for being either too restrictive or too benevolent. They are too restrictive in the case that there exists some information flow between public and private activities (or data) but this flow is reasonable small. For example, usually access control processes exhibit some information flow (mostly) showing which password is not correct but they are still considered to be secure under reasonable password policy: it is not meaningful to consider such systems insecure in the case that a number of possible passwords is sufficiently large. On the other side, qualitative security properties could be too benevolent. For example, if an intruder cannot learn the whole secrete (password, private key, etc) they could consider a system to be safe despite the fact, that the intruder could still learn almost all the secrete (for example, signicfiant number of bits of private key). Hence there is a need to quantify an amount of information flow which can be gained from the observations of public system activities. An amount of possibly leaked information could be expressed by means of Shannon's information theory as it was done, for example, in [CHM07,CMS09] for simple imperative languages and in [Gru08] for process algebras. Another possibility is to exploit probabilistic theory as it was used for process algebras in
? Work supported by the grant VEGA 1/1333/12. [Gru09]. Resulting techniques lead to quantifications of how many bits of private information can leak or how probable is that an intruder can learn some secrete property on processes. In [L02] an information oflw is studied in the framework of process algebras. Particularly, it is investigated how much information i.e. a number of bits can be transmitted by observing some timed system activities. In [Gru11] it is investigated which private actions can gained or excluded by observations of public actions.
The aim of this paper is to quantify an amount of information flow by differential privacy (see [D08]) in the framework of probabilistic process algebras. The concept of differential privacy was originally developed to ”provide means to maximize the accuracy of queries from statistical databases while minimizing the chances of identifying its records”. Later on it was used also for other applications. In [X14] differential privacy is studied for probabilistic automata and in [X12] it has been exploited in the framework of probabilistic process algebra by comparing probabilities of a given output produced by inputs which differ in one position. Here we extend and further develop this approach and we propose several other security properties based on -differential privacy for a (different) probabilistic process algebra. We show how these properties are related as well as how they are related to some traditional qualitative security properties (namely, Non-Deducibility on Composition [FGM03] and opacity [BKR04,BKMR06]). Moreover, we show some of their compositionality properties as well as undecidability and decidability results.
The paper is organized as follows. In Section 2 we describe our working formalism - probabilistic process algebra. In Sections 3 we recall some (qualitative) security properties based on an absence of information oflw which will serve as a motivation for our work. Section 4 is devoted to differential privacy. Here we denfie and investigate various security properties based on -differential privacy. 2
In this section we define the Probabilistic Process Algebra, pCCS for short, which is based on Milner’s CCS (see [Mil89]). First we assume a set of atomic action symbols A not containing symbol τ and such that for every a ∈ A there exists a ∈ A and a = a. We define Act = A ∪ {τ }. We assume that a, b, . . . range over A and u, v, . . . range over Act.
To add probabilities to CCS calculus we will follow alternating model (the approach presented in [HJ90]) which is neither reactive nor generative nor stratiefid (see [LN04]). Probabilistic transitions are not associated with actions but they are labeled with probabilities. In so called probabilistic states a next transition is chosen according to probabilistic distribution. For example, process a.(0.3.b.N il ⊕ 0.7.(a.N il + b.N il)) can perform action a and after that it reaches the probabilistic state and from this state it can reach with probability 0.3 the state where only action b can be performed or with probability 0.7 it can reach the state where it can perform either a or b .
Formally, we introduce a new operator L (0, 1] such that Pi∈I qi = 1. Processes whichi∈Icaqni.Ppie,rqfiorbmeinags rtehael nfirsutmabcetriosnin probabilistic transition will be called probabilistic processes or states (to stress that P is non-probabilistic process we will sometimes write PN if necessary). Hence we assume the signature Σ = Sn∈N Σ n, where Σ 0 = {N il} Σ 1 = {x. | x ∈ Act} ∪ {[S] | S is a relabeling function} ∪{\M | M ⊆
A} Σ 2 = {|} Σ n = {M qi, |I| = n}
i∈I with the agreement to write unary action operators in prexfi form, the unary operators [S], \M in postxfi form, and the rest of operators in infix form. Relabeling functions, S : Act → Act are such that S(a) = S(a¯) for a ∈ A and S(τ ) = τ .
The set of pCCS terms over the signature Σ is denfied by the following BNF notation:
P ::= X | op(P1, P2, . . . Pn) | μXP where X ∈ V ar, V ar is a set of process variables, P, P1, . . . Pn are pCCS terms, Xμ − is the binding construct, op ∈ Σ . We require that all Pi processes in Li∈I qi.Pi are non-probabilistic ones. By pCCS we will denote the set of all probabilistic and non-probabilistic processes and all definitions and notations for CCS processes (see [Mil89]) are extended for pCCS ones. Structural operational semantics is given by labeled transition systems. The transition relation → is a subset of pCCS × Act ∪ (0, 1] × pCCS. We just mention the new transition rules for probabilitis.
PN →1 PN q P → P 0, Q →r Q0
q.r P | Q → P 0 | Q0
A1 P a
Li∈I qi.Pi →qi Pi
A2
For probabilistic choice we have the rule A2 and for a probabilistic transition of two processes running in parallel we have the rule P a. The technical rule A1 enables parallel run of probabilistic and non-probabilistic processes by allowing to non-probabilistic processes to perform →1 transition and hence the rule P a could be applied.
We will use an usual denfiition of opened and closed terms where μX is the only binding operator. Closed terms which are guarded (each occurrence of X is within some subexpression u.A are called pCCS processes. Note that N il will be often omitted from processes descriptions and hence, for example, instead of a.b.N il we will write just a.b. We write P →x P 0 instead of (P, x, P 0) ∈ → and P 6→x if there is no P 0 such that P →x P 0. The meaning of the expression P →x P 0
To express what an observer can see from system behaviour we will denfie will write P ⇒x P 0 iff ⇒Px →ws1h→xic→hs2 hPid0efotrhes1a,cst2io∈n(τ {τ a}n∪d (p0r,o1b])a?bialnitdiePs. F⇒sorimnsatlelya,dwoef modified transitions P ⇒x1 ⇒x2 . . . ⇒xn. We will write P ⇒x if there exists P 0 such that P ⇒x P 0. By we will denote the empty sequence of actions and by s v s0, s, s0 ∈ (Act ∪ (0, 1])? we will denote that s is a prefix of s0. By Sort(P ) we will denote the set of actions from A which can be performed by P i.e. Sort(P ) = {x|P →−s.x for some s ∈ (Act ∪ (0, 1])? and x ∈ A}.
As regards behaviorial semantics, we will work with the weak trace equivalence.
Definition 1. The set of weak traces of process P is defined as T rw(P ) = {s ∈ A?|∃P 0.P ⇒s P 0}. Two processes P and Q are weakly trace (P ≈ w Q) iff T rw(P ) = T rw(Q).
We conclude this section with a definition of probabilities of traces for a given process. Let P be a pCCS process and let P →x1 P1 →x2 P2 →x3 . . . → xn Pn, where xi ∈ Act ∪ (0, 1] for every i, 1 ≤ i ≤ n. The sequence P.x1.P1.x2 . . . xn.Pn will be called a nfiite computational path of P (path, for short), its label is a subsequence of x1. . . . .xn consisting of those elements which belong to Act i.e. label(P.x1.P1.x2 . . . xn.Pn) = x1. . . . .xn|Act and its probability is denfied as a multiplication of all probabilities contained in it, i.e. P rob(P.x1.P1.x2 . . . xn.Pn) = 1 × q1 × . . . × qk where x1. . . . .xn|(0,1] = q1 . . . gk. The multiset of nfiite paths of P will be denoted by P ath(P ). For example, the path (0.5.a.N il ⊕ 0.5.a.N il). 0.5.(a.N il).a.(N il) is contained in P ath(0.5.a.N il ⊕ 0.5.a.N il) two times. There exist a few techniques how to define this multiset. For example, in [SL95] a technique of schedulers are used to resolve the nondeterminism and in [GSS95] all transitions are indexed and hence paths can be distinguished by different indexes. In the former case, every scheduler denfies (schedules) a particular computation path and hence two different schedulers determine different paths, in the later case, the index records which transition was chosen in the case of several possibilities. The set of indexes for process P consists of sequences i1 . . . ik where ij ∈ {0, . . . , n}∪{0, . . . , n}×{ 0, . . . , n} where n is the maximal cardinality of I for subterms of P of the form Li∈I qi.Pi. An index records how a computation path of P could be derived, i.e. it records which process was chosen in case of several nondeterministic possibilities. If there is only one possible successor transitions are indexed by 1 (i.e. corresponding il = 1). If transition Pi →x P 0 is indexed by k then transition Li∈I qi.Pi →x P 0 is indexed by k.i, and if transitions P →x P 0 x and Q → Q0 are indexed by k and l, respectively, then transitions of P |Q have indexes from {(k, 0), (0, l), (k, l)} depending on which transition rule for parallel composition was applied. Every index defines at most one path and the set of all indexes defines the multisets of paths P ath(P ). Let C, C ⊆ P ath(P ) be a finite multiset. We define P r(C) = Pc∈C P rob(c) if C 6= ∅ and P r(∅) = 0. For s ∈ T rw(P ) we will denote by P r(s) the probability of performing s (i.e. it is the sum of probabilities of all paths c ∈ P ath(P ) such that label(c) = s). 3
In this section we recall two (qualitative) security properties for CCS (i.e. nonprobabilistic process algebra). The rfist inspiration for our work is the security property Non-Deducibility on Composition (NDC for short, see in [FGM03]). Suppose that all actions are divided in two groups, namely public (low level) actions L and private (high level) actions H i.e. A = L ∪ H, L ∩ H = ∅. Then process P has property NDC if for every high level user A, the low level view of the behaviour of P is not modiefid (in terms of weak trace equivalence) by the presence of A. The idea of NDC can be formulated as follows.
A, Sort(A) ⊆
H ∪ {τ } (P |A) \ H ≈ w P \ H.
Now we introduce another information flow notion, which is based on a more general concept of observation and opacity. This concept was exploited in [BKR04] and [BKMR06] in a framework of Petri Nets and transition systems, respectively. First we assume an observation function O : Act? → Act?.
Now suppose that we have some security property. This might be an execution of one or more classified actions, an execution of actions in a particular classiefid order which should be kept hidden, etc. Suppose that this property is expressed by predicate φ over process’s traces. Contrary to the original denfiition we do not require that the predicate is total. We would like to know whether an observer can deduce the validity of the property φ just by observing sequences of actions from Act? performed by given process. The observer cannot deduce the validity of φ if there are two traces w, w0 ∈ Act? such that φ (w), ¬φ (w0) and the traces cannot be distinguished by the observer i.e. O(w) = O(w0). We formalize this concept by opacity.
Definition 3 (Opacity). Given process P , a predicate φ over Act? is opaque w.r.t. the observation function O if for every sequence w, w ∈ T rw(P ) such that φ (w) holds and O(w) 6= , there exists a sequence w0, w0 ∈ T rw(P ) such that ¬φ (w0) holds and O(w) = O(w0). The set of processes for which the predicate φ is opaque with respect to O will be denoted by Opφ .
O
Now we are prepared to denfie several quantitative security properties based on differential privacy. Actually, as we will see later, two of them are really quantitative counterparts of the above mentioned qualitative properties. 4
Differential privacy was originally developed for privacy protection of statistical databases (see [D08]). In the original definition, a query mechanism A is differentially private if for any two databases D1 and D2 which differ only for one individual (one raw, for example, data of one person), and any property S, the probability distributions of A(D1), A(D1) differ on S at most by e , namely,
Pr(A(D1) ∈ S) ≤ e × Pr(A(D2) ∈ S).
Now we will reformulate -differential privacy for our process algebra framework. Every sequence of high level actions s (i.e. s ∈ H∗ ) represents a secrete input. The public output o is a sequence of low level actions (i.e. o ∈ L∗ ). First we start with formulation of -differential privacy for the given secrete input and public output. Note that this definition is similar to the one which appeared in [X12]. We will write for a given process P conditional probability P r(o|s) as probability P r(o) for process (P |s.N il) \ H.
P ∈ DF (o, s) iff o ∈ T rw((P |s.N il) \ H) and for every s0 ∈ H∗ which differs from s in one position.
Note that in the previous definition we assume that if s = x1 . . . xn s0 = x01 . . . x0n then there exists j such that xj 6= x0j and xi = x0i for i 6= j. The property DF (o, s) says that by observing the public output o an intruder cannot be pretty sure (expressed by ) whether the secrete input was s or s0. Note that for = 0 the inputs s and s0 do not lead to different probabilities for the corresponding output. Now we will formulate several properties of differential privacy. First, differential privacy is not sensitive to a length of the observation (public output) i.e. a longer observation can leak less as well as more on private inputs as it is stated by the following proposition.
L∗ such that o1 v o2 and o3 v o4 and such that P ∈ DF (o1, s), P 6∈ DF (o2, s) and P ∈ DF (o4, s), P 0 6∈ DF (o3, s).
Proof. Let P = (1− )/2.(h1.l1.(p.l2.N il⊕ (1− p).l3.N il))⊕ ((1+ )/2.h1.l1.l2.N il), s = h1 and o1 = l1, o2 = l1.l2. By appropriate choice of p we get P ∈ DF (o1, s), P 6∈ DF (o2, s). The second case is similar.
Differential privacy is neither sensitive to a length of secrete as it is stated by the following proposition, its proof is similar to the proof of previous proposition.
H∗ such that s1 v s2 and s3 v s4 and such that P ∈ DF (o, s1), P 6∈ DF (o, s2) and P ∈ DF (o, s4), P 0 6∈ DF (o, s3).
Now we will formulate and prove some compositional properties of DF (o, s) property.
Proposition 3. P ∈ DF (o, s) then l.P ∈ DF (l.o, s) and h.P ∈ DF (o, h.s). Proof. Clearly, every observation of the process l.P has to start with l and probabilities of all traces with the proper prexfi l do not change. Similarly for the process h.P .
P ∈ DFln(p0/p)(o, s).
Proposition 4. Let us assume processes Pi and let p = min(q1.P r(o|s)1, . . . qn.P r(o|s)n) and let us suppose that p = qi.P r(o|s)i, and p0 = max(q1.P r(o|s)1, . . . qn.P r(o|s)n) and let us suppose that p0 = qj .P r(o|s)j , where P r(o|s)i is the corresponding probability for the process Pi. Let P = Li∈{1,...,n} qi.Pi then Proof. The main idea. The process P can output o with the input s by performing Pi and can output o with the input s0 by performing Pj . The rest of the proof could be done by computing the corresponding probability.
P [S] ∈ DF (S((o), S(s)) and P \ M ∈ DF (o, s).
Proof. The rfist part follows directly from the denfiition of relabeling. The second part follows from the fact that the restriction either has no inuflence on performing o and hence the corresponding probabilities are not changed or M ∪ Sort(o.N il) 6= ∅ and in this case probabilities are equal to 0.
As regards the recursion we need an auxiliary definition.
Definition 5. Process variable X is sequential in P if every subterm of P containing X (except X itself ) is of a form y.P 0 or P Pi. Let M ⊆ Act. Process variable X is M -guarded in P if it is contained in a subterm of P of the form u.P 0, u ∈ M .
Proposition 6. Let P ∈ DF (o, s) and P r(o|s) 6= 0 for P and P is sequential and process variable X is M -guarded in P for some nonempty M such that Sort(o.N il) ∩ M = ∅ . Then μX.P ∈ DF (o, s).
Proof. Sketch. We have to eliminate the case when o could be produced by application of the recursion what is satisefid by proposition’s requirements. The rest follows directly from the definitions of DF (o, s) and recursion.
Now we can define the property expressing security of the input s with respect to -differential privacy. Process has this property if there is no observation (output) which could distinguish between the input s and input s0 (which differs from s in one element). The formal denfiition is the following.
The property DF (s) is rather strong but in general it is undecidable as it is stated by the following proposition.
Proposition 7. Property DF (s) is undecidable.
Proof. The main idea. We exploit Turing power of pCCS and hence we reduce the property to the halting problem. Let R be an arbitrary process and let T = μX. Py∈Act y.X. By deciding (P |((R|T ) \ Act)) ∈ DF (s) we could decide halting problem for R.
We could put some restrictions on processes in such a way that the property DF (s) is decidable for them.
Proposition 8. Property DF (s) is decidable for finite processes and for processes which are sequential and H-guarded.
Proof. Sketch. Only the case of innfiite processes is interesting. If a process is sequential and H-guarded this process can produce public outputs only by reading secrete inputs and hence we can limit length of possible outputs o i.e. there are only finitely many cases to be checked.
Now we denfie which observations could leak something about the secrete s with respect to -differential privacy.
DF (P, , s) = {o|P r(o|s) > e × P r(o|s0) and o ∈ T rw((P |s.N il)\ Clearly, P ∈ DF (s) iff DF (P, , s) = ∅. On the other side, if DF (P, , s) 6= ∅ we can ask what is the minimal length of o, o ∈ DF (P, , s). Usually, longer o (a higher value of |o|) means that the secrete s could be considered safer.
Similarly to the previous definition, we can specify which secretes could by leak (with respect to -differential privacy) by the given observation o.
DF (P, , o) = {s|P r(o|s) > e × P r(o|s0) and o ∈ T rw((P |s.N il)\
H)}.
H)}.
There is a simple relation between sets from Definition 7 and 8, namely, o ∈ (P, , s) iff s ∈ (P, , o). Another generalization of above mentioned concepts is overall security of processes with respect to -differential privacy which requires that processes are secure with respect to every secrete input and public output. The formal definition follows.
DF ( ) = {P |P ∈ DF (o, s) for every o ∈ L∗ , s ∈ H∗ }.
Note that for P ∈ DF ( ) it holds that DF (P, , o) = DF (P, , s) = ∅ i.e. for such the process there is no secret which could leak by any observation.
Naturally, all above mentioned sets depend on value of as corresponding ”security” level. So it is meaningful to denfie ”highest” security as the minimal such that by observing o an intruder cannot be sure (in terms of differential privacy) about the value of s.
P DF (P, o, s) = min{ |P ∈ DF (o, s)}.
Clearly, for 1 < 2 it holds DF (P, 1, s) ⊆ DF (P, 2, s) and DF (P, 1, o) ⊆ DF (P, 2, o). Hence for P DF (P, o, s) we obtain the smallest sets DF (P, , o), DF (P, , s) and DF ( ). As regards ”length” of observations and secrets we have the following proposition.
and o3 ⊂ o4 such that P DF (P, o1, s) < P DF (P, o2, s) and P DF (P, o4, s) < P DF (P, o3, s).
Proof. The proof follows from Proposition 1.
Till now we have investigated an impact of probability distributions for two secret inputs which differ only in one position. This approach could be too restrictive in many cases so we extend it now. We assume a metric ρ on the set of secretes, i.e. sequences of high level actions. Hence we can relate probabilities of the output o produced by arbitrary secretes s, s0 not only those ones which differ only in one position.
P ∈ DF ,ρ (o, s) iff o ∈ T rw((P |s.N il) \ H) and
P r(o|s) ≤ e × ρ (s,s0) × P r(o|s0)
Similarly to Definition 9 we can define the set of secure properties with respect to metrics ρ and -differential privacy.
DF ( , ρ ) = {P |P ∈ DF (o, s) for every o ∈ L∗ , s ∈ H∗ }.
Now we can relate qualitative security property NDC to quantitative one, namely -differential privacy.
Proposition 10. Let P be a process and ρ be a metric on sequences of H actions. Then if P ∈ N DC then for every o ∈ L∗ , s ∈ H∗ there exists such that P ∈ DF ,ρ (o, s). Moreover, if P ∈ DF ( , ρ ) for some and ρ is such that ρ (x, y) 6= 0 whenever x 6= y, then P ∈ N DC.
Proof. Let P ∈ N DC, i.e. (P |A) \ H ≈ w P \ H for every A such that Sort(A) ⊆ H ∪{τ }. This means that also (P |s.N il)\H ≈ w (P |s0.N il)\H and so P r(o|s) = 0 iff P r(o|s0) = 0 for every o i.e. it cannot happen that one of these probabilities is non-zero and another one is equal to zero, hence there exists such that P ∈ DF ,ρ (o, s).
Now suppose that for every o ∈ L∗ , s ∈ H∗ there exists such that P ∈ DF ,ρ (o, s). This means that for any two secretes if one could output o then also another one can do the same and hence P ∈ N DC.
As regards the metric, there are several meaningful choices how to measure a distance between two secrets. First we consider a variant of Hamming distance. Definition 13. Let s, s0 ∈ Act∗ and s = x1.x2. . . . .xn, s0 = x01.x02. . . . .x0m. We define metrics ρ 0 as a number of positions where s and s0 differ, i.e. ρ 0(s, s0) = |m − n| + Pim=in1,(xni,6=mx)0i 1.
For the metric ρ 0 we have the following result which relates DF (o, s) and DF (o, s) properties.
Proof. Suppose that ρ 0(s, s0) = n, then there exist s1, . . . , sn− 1 such that si, si+1 differ by one element as well as s, s1 and sn− 1, s0. Since we have P ∈ DF (o, s), P ∈ DF (o, si) for all i, 1 ≤ n − 1 we have P r(o|s) ≤ e × n × P r(o|s0).
The metric ρ 0 does not take into account the length of inputs. If we have two completely different inputs of length 2 and inputs which differ in two positions but both of length 128, in both cases the metric is 2 what does not express an amount of secrecy which could leak or is protected. In the first case the whole secrete is protected and in the second case only a fraction of secrecy could be protected if P ∈ DF ,ρ 0 (o, s). Hence we could consider more elaborated metrics, for example ρ min(s, s0) = (ρ o + min |s|, |s0|)/ min(|s|, |s0|), ρ max(s, s0) = (ρ o + max |s|, |s0|)/ max(|s|, |s0|), ρ sum(s, s0) = (ρ o + |s| + |s0|)/(|s| + |s0|) etc.
Now we can reformulate Denfiition 7 and 8 taking into account a given metric. We illustrate this by generalization of the set DF (P, , o).
Definition 14. DF (P, , ρ, ,δ o ) = {s|P r(o|s) o ∈ T rw((P |s.N il) \ H) and ρ (s, s0) = δ }. > e × δ ×
P r(o|s0) and
The sets of secretes DF (P, , ρ, ,δ o ) represents those secrets which could (at least partially) leak under the observation o. The amount of leakage is given by ρ and δ . It is easy to check that DF (P, , ρ 0, 1, o) = DF (P, , o). Similarly, we could generalize the set DF (P, , s).
Now we have taken into account a more appropriate distance between two secrets but we have omitted a length of observations. It makes a difference if a secrete could leak by short observation or it could leak only by very long observations. For example, if s1 ∈ DF (P, , ρ, ,δ o ) and |o| is small but s2 ∈ DF (P, , ρ, ,δ o 0) only for a very big |o0| then s2 should be considered safer. This leads us to further generalization of -differential privacy. We consider function f which could take into account a distance between secrete inputs, their length, as well as length of outputs. Moreover, it can incorporate also a cost of observations (it could be different from it length) and other relations.
P ∈ DF ,f (o, s) iff o ∈ T rw((P |s.N il) \ H) and
P r(o|s) ≤ e × f(s,s0,o) × P r(o|s0).
We believe that by appropriate choice of the function f we obtain more realistic security properties based on -differential privacy but we leave this for the further research. But now we turn to another generalization of -differential privacy which is inspired by opacity (see Denfiition 3).
Definition 16. Suppose that we have the predicate φ over secrets. Then we define P ∈ oDF ,φ (o, s) if for o ∈ T rw((P |s.N il) \ H) where s is such that φ (s) holds we have for some s0 ∈ H∗ such that ¬φ (s0).
There is a clear relationship between qualitative property ”opacity” Opφ and its quantitative variant based on -differential privacy. O
that P ∈ oDF ,φ (o, s). Then P ∈ OpφO for O which maps high level actions, probabilities as well as τ action to empty sequence, and vice versa. Proof. The main idea. Let us assume that P ∈ oDF ,φ (o, s). This means that for every secrete s for which φ holds there exists s0 for which φ does not hold. Since we consider the observation function O which ”does not see” high level actions and τ , we have P ∈ Opφ . The proof of the opposite implication is similar.
O
We can relate oDF ,φ (o, s) also to the property oDF (o, s).
where φ s(s0) holds if s = s0 and does not hold if s and s0 differ in one position. Proof. The main idea. Let us assume that P ∈ oDF (o, s). This means that probability of the output o with the secrete input s0 which differs form s in one position (i.e. φ s(s), ¬φ s(s0) hold) is non zero and hence P ∈ oDF ,φ s (o, s).
Note that it is easy to prove that the most of the above mentioned properties (sets) are undecidable in general (it follows from undecidable result stated by Proposition 7). We leave for further work to specify conditions for which they are decidable. 5
We have presented several (quantitative) security concepts based on -differential privacy. They could be seen as quantifications of some qualitative properties, namely non-deducibility on composition [FGM03] and opacity [BKR04,BKMR06]). They express how secure is the secrete input s with respect to the public output o, which secrete could leak by observing the public output o, which output could leak the secrete s or which processes are completely safe i.e. there is no secrete and output which could leak it. Even very basic of these properties are undecidable in general but we have shown under which conditions they become decidable. But since also in this case complexity remains very high we propose some compositional properties to manage it at least somehow. We propose also some metrics on inputs which could be exploited to obtain more realistic security properties. As it was mentioned, one should consider also length of inputs and relate it to the length of public outputs. Without this we could obtain too restrictive security notions. The price of leakage - as a relation between amount of leaked secrecy with respect to the length of observation is a crucial security characterization. Otherwise no access control process based on passwords would be considered safe (if a number of attempts to guess the password is not limited).
As regards the future work, besides already mentioned plans, we also plan to exploit information theory to express how much information on secrete inputs could leak with a given probability. This is particularly interesting if secrete inputs have qualities which cannot be simply captured. Then we will use differences between entropy of inputs as a metric. Moreover, we plan to concentrate on efficient techniques for checking of above proposed security properties.