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, significant 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 flow 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 flow which will serve as a motivation for our work. Section 4 is devoted to differential privacy. Here we define and investigate various security properties based on -differential privacy.
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 stratified (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 i∈I q i .P i , q i being real numbers in (0, 1] such that i∈I q i = 1. Processes which can perform as the first action probabilistic transition will be called probabilistic processes or states (to stress that P is non-probabilistic process we will sometimes write P N if necessary). Hence we assume the signature Σ = n∈N Σ n , where
with the agreement to write unary action operators in prefix form, the unary operators [S], \M in postfix form, and the rest of operators in infix form. Relabeling functions, S : Act → Act are such that S(a) = S(ā) for a ∈ A and S(τ ) = τ .
The set of pCCS terms over the signature Σ is defined by the following BNF notation:
where X ∈ V ar, V ar is a set of process variables, P, P 1 , . . . P n are pCCS terms, µX− is the binding construct, op ∈ Σ. We require that all P i processes in i∈I q i .P i 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.
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 definition 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 instead of (P, x, P ) ∈ → and P x → if there is no P such that P x → P . The meaning of the expression P x → P is that the term P can evolve to P by performing action x, by P x → we will denote that there exists a term P such that P x → P .
To express what an observer can see from system behaviour we will define modified transitions
x ⇒ which hide the action τ and probabilities. Formally, we will write P
We will write P x ⇒ if there exists P such that P x ⇒ P . By we will denote the empty sequence of actions and by s s , s, s ∈ (Act ∪ (0, 1]) we will denote that s is a prefix of s . 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 r w (P ) = {s ∈ A |∃P .P s ⇒ P }. Two processes P and Q are weakly trace (P
We conclude this section with a definition of probabilities of traces for a given process. Let P be a pCCS process and let
The sequence P.x 1 .P 1 .x 2 . . . x n .P n will be called a finite computational path of P (path, for short), its label is a subsequence of x 1 . . . . .x n consisting of those elements which belong to Act i.e. label(P.x 1 .P 1 .x 2 . . . x n .P n ) = x 1 . . . . .x n | Act and its probability is defined as a multiplication of all probabilities contained in it, i.e. P rob(P.
The multiset of finite 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 defines (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 i 1 . . . i k where i j ∈ {0, . . . , n}∪{0, . . . , n}×{0, . . . , n} where n is the maximal cardinality of I for subterms of P of the form i∈I q i .P i . 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 i l = 1). If transition P i x → P is indexed by k then transition i∈I q i .P i x → P is indexed by k.i, and if transitions P x → P and Q
x → Q 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) = c∈C P rob(c) if C = ∅ and P r(∅) = 0. For s ∈ T r w (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).
In this section we recall two (qualitative) security properties for CCS (i.e. nonprobabilistic process algebra). The first 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 modified (in terms of weak trace equivalence) by the presence of A. The idea of NDC can be formulated as follows.
Definition 2. (NDC) P ∈ N DC iff for every A, Sort(A) ⊆ 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 classified order which should be kept hidden, etc. Suppose that this property is expressed by predicate φ over process's traces. Contrary to the original definition 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, w ∈ Act such that φ(w), ¬φ(w ) and the traces cannot be distinguished by the observer i.e. O(w) = O(w ). 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 r w (P ) such that φ(w) holds and O(w) = , there exists a sequence w , w ∈ T r w (P ) such that ¬φ(w ) holds and O(w) = O(w ). 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 define 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.
Differential privacy was originally developed for privacy protection of statistical databases (see [D08]). In the original definition, a query mechanism A isdifferentially private if for any two databases D 1 and D 2 which differ only for one individual (one raw, for example, data of one person), and any property S, the probability distributions of A(D 1 ), A(D 1 ) differ on S at most by e , namely, Pr(A(D 1 ) ∈ S) ≤ e × Pr(A(D 2 ) ∈ 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. for every s ∈ H * which differs from s in one position.
Note that in the previous definition we assume that if s = x 1 . . . x n s = x 1 . . . x n then there exists j such that x j = x j and x i = x i for i = 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 s . Note that for = 0 the inputs s and s 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. Proof. Let P = (1− )/2.(h 1 .l 1 .(p.l 2 .N il⊕(1−p).l 3 .N il))⊕((1+ )/2.h 1 .l 1 .l 2 .N il), s = h 1 and o 1 = l 1 , o 2 = l 1 .l 2 . By appropriate choice of p we get P ∈ DF (o 1 , s), P ∈ DF (o 2 , 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.
Proposition 2. For every there exist processes P, P , o ∈ L * and s 1 , s 2 , s 3 , s 4 ∈ H * such that s 1 s 2 and s 3 s 4 and such that P ∈ DF (o, s 1 ), P ∈ DF (o, s 2 ) and P ∈ DF (o, s 4 ), P ∈ DF (o, s 3 ). 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 prefix l do not change. Similarly for the process h.P . Proposition 4. Let us assume processes P i and let p = min(q 1 .P r(o|s) 1 , . . . q n .P r(o|s) n ) and let us suppose that p = q i .P r(o|s) i , and p = max(q 1 .P r(o|s) 1 , . . . q n .P r(o|s) n ) and let us suppose that p = q j .P r(o|s) j , where P r(o|s) i is the corresponding probability for the process P i . Let P = i∈{1,...,n} q i .P i then P ∈ DF ln(p /p) (o, s).
Proof. The main idea. The process P can output o with the input s by performing P i and can output o with the input s by performing P j . The rest of the proof could be done by computing the corresponding probability. Proof. The first part follows directly from the definition of relabeling. The second part follows from the fact that the restriction either has no influence on performing o and hence the corresponding probabilities are not changed or M ∪ Sort(o.N il) = ∅ 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 or P i . 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 , u ∈ M . Proposition 6. Let P ∈ DF (o, s) and P r(o|s) = 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 satisfied 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 s (which differs from s in one element). The formal definition is the following. Definition 6. P ∈ DF (s) if for every o ∈ L * it holds P ∈ DF (o, s).
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. y∈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 infinite 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 define which observations could leak something about the secrete s with respect to -differential privacy. 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.
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 define "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.
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. 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, s not only those ones which differ only in one position.
Definition 11. P ∈ DF ,ρ (o, s) iff o ∈ T r w ((P |s.N il) \ H) and P r(o|s) ≤ e ×ρ(s,s ) × P r(o|s ) Similarly to Definition 9 we can define the set of secure properties with respect to metrics ρ and -differential privacy.
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) = 0 whenever x = 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 |s .N il)\H and so P r(o|s) = 0 iff P r(o|s ) = 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, s ∈ Act * and s = x 1 .x 2 . . . . .x n , s = x 1 .x 2 . . . . .x m . We define metrics ρ 0 as a number of positions where s and s differ, i.e. ρ 0 (s, s
For the metric ρ 0 we have the following result which relates DF (o, s) and DF (o, s) properties.
Proposition 11. Let P ∈ DF (o, s) for every s ∈ H * . Then P ∈ DF ,ρ0 (o, s).
Proof. Suppose that ρ 0 (s, s ) = n, then there exist s 1 , . . . , s n−1 such that s i , s i+1 differ by one element as well as s, s 1 and s n−1 , s . Since we have P ∈ DF (o, s), P ∈ DF (o, s i ) for all i, 1 ≤ n − 1 we have P r(o|s) ≤ e ×n × P r(o|s ).
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 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 s 1 ∈ DF (P, , ρ, δ, o) and |o| is small but s 2 ∈ DF (P, , ρ, δ, o ) only for a very big |o | then s 2 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.
Definition 15. P ∈ DF ,f (o, s) iff o ∈ T r w ((P |s.N il) \ H) and P r(o|s) ≤ e ×f (s,s ,o) × P r(o|s ). 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 Definition 3).
Definition 16. Suppose that we have the predicate φ over secrets. Then we define P ∈ oDF ,φ (o, s) if for o ∈ T r w ((P |s.N il) \ H) where s is such that φ(s) holds we have P r(o|s) ≤ e × P r(o|s ) for some s ∈ H * such that ¬φ(s ).
There is a clear relationship between qualitative property "opacity" Op φ O and its quantitative variant based on -differential privacy.
Proposition 12. Suppose that for every o ∈ L * , s ∈ H * there exists such 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 s for which φ does not hold. Since we consider the observation function O which "does not see" high level actions and τ , we have P ∈ Op φ O . The proof of the opposite implication is similar.
We can relate oDF ,φ (o, s) also to the property oDF (o, s).
Proposition 13. Let us assume that P ∈ oDF (o, s). Then P ∈ oDF ,φs (o, s) where φ s (s ) holds if s = s and does not hold if s and s 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 s which differs form s in one position (i.e. φ s (s), ¬φ s (s ) 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.
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.