A security property called process environment opacity is formalized and studied. Properties of process's inputs (environments) are expressed by predicate and it is required that an intruder cannot learn their validity by observing process's behavior. This basic idea can be formulated in various ways. The resulting security properties are compared.
Introduction Information ow based security properties (see [GM82]) assume an absence of any information ow between private and public systems activities. This means, that 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 and among them opacity (see [BKR04,BKMR06]) could be considered as the most general one and many other security properties could be viewed as its special cases (see, for example, [Gru07]). A predicate is opaque if for any trace of a system for which it holds, there exists another trace for which it does not hold and the both traces are indistinguishable for an observer (which is expressed by an observation function). This means that the observer (intruder) cannot be sure whether a trace for which the predicate holds has been performed or not. In [Gru15] opacity is modi ed (the resulting property is called process opacity) in such a way that instead of process's traces we focus on properties of reachable states. Hence we assume an intruder who is not primarily interested whether some sequence of actions performed by a given process has some given property but we consider an intruder who wants to discover whether this process reaches a state which satis ed some given (classi ed) predicate. It turns out that in this way we could capture some new security aws. Both opacity and process opacity are based on xed (static) security policy which is not changed during system computation. In [Gru16] process opacity for dynamic security policies is formalized. All of these properties are de ned in the framework of process algebras, but neither opacity, which represents security of process's traces nor process opacity, which represents security of resulting states, can capture security of process's inputs, similarly as security of inputs is de ned for programming languages.
The aim of this paper is to formalize security of process's inputs. We adopt the approach which appeared in [SS15] for programming languages but we reformulate it for timed process algebras. Inputs will be modeled by processes which we call process's environments. The resulting security property will be called process environment opacity. It assumes that for every process's environment for which a given predicate holds there exists equivalent one, for which it does not hold and the process with these environments leads to equivalent states. This means that an intruder cannot learn validity of the predicate over process's inputs. We will study this security property as well as its variants. Moreover, we compare them with other security properties known in the literature.
The paper is organized as follows. In Section 2 we describe the timed process algebra TPA which will be used as a basic formalism. In Section 3 we present some notion on information ow security based on opacity and in the next section process environment opacity is de ned, studied and compared to other security properties. Section 5 contains discussion and plans for future work. 2
Timed Process Algebra In this section we de ne Timed Process Algebra, TPA for short. TPA is based on Milner's CCS but the special time action t which expresses elapsing of (discrete) time is added. The presented language is a slight simpli cation of Timed Security Process Algebra introduced in [FGM00]. We omit an explicit idling operator used in tSPA and instead of this we allow implicit idling of processes. Hence processes can perform either "enforced idling" by performing t actions which are explicitly expressed in their descriptions or "voluntary idling" (i.e. for example, the process a:N il can perform t action since it is not contained the process speci cation). But in both cases internal communications have priority to action t in the parallel composition. Moreover we do not divide actions into private and public ones as it is in tSPA. TPA di ers also from the tCryptoSPA (see [GM04]). TPA does not use value passing and strictly preserves time determinancy in case of choice operator + what is not the case of tCryptoSPA.
n2f0;1;2g
To de ne the language TPA, we rst assume a set of atomic action symbols A not containing symbols and t, and such that for every a 2 A there exists a 2 A and a = a. We de ne Act = A [ f g; At = A [ ftg; Actt = Act [ f g
t . We assume that a; b; : : : range over A, u; v; : : : range over Act, and x; y : : : range over Actt. Assume the signature = S n, where 0 = fN ilg 1 = fx: j x 2 A [ ftgg [ f[S] j S is a relabeling functiong [fnM j M
Ag 2 = fj; +g with the agreement to write unary action operators in pre x form, the unary operators [S]; nM in post x form, and the rest of operators in in x form. Relabeling functions, S : Actt ! Actt are such that S(a) = S(a) for a 2 A; S( ) = and S(t) = t.
The set of TPA terms over the signature is de ned by the following BNF notation:
P ::= X j op(P1; P2; : : : Pn) j
XP where X 2 V ar, V ar is a set of process variables, P; P1; : : : Pn are TPA terms, X is the binding construct, op 2 .
The set of CCS terms consists of TPA terms without t action. We will use an usual de nition of opened and closed terms where X is the only binding operator. Closed terms which are t-guarded (each occurrence of X is within some subterm t:A i.e. between any two t actions only nitely many non timed actions can be performed) are called TPA processes.
We give a structural operational semantics of terms by means of labeled transition systems. The set of terms represents a set of states, labels are actions from Actt. The transition relation ! is a subset of TPA Actt TPA. We write P !x P 0 instead of (P; x; P 0) 2 ! 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 is that the term P can evolve to P 0 by performing action x, by P !x we will denote that there exists a term P 0 such that P !x P 0. We de ne the transition relation as the least relation satisfying the inference rules for CCS plus the following inference rules:
N il !t N il P !t P 0; Q !t Q0; P j Q 6!
P j Q !t P 0 j Q0
A1 P a
u:P !t u:P P !t P 0; Q !t Q0 P + Q !t P 0 + Q0
A2 S
Here we mention the rules that are new with respect to CCS. Axioms A1; A2 allow arbitrary idling. Concurrent processes can idle only if there is no possibility of an internal communication (P a). A run of time is deterministic (S) i.e. performing of t action does not lead to the choice between summands of +. In the de nition of the labeled transition system we have used negative premises (see P a). In general this may lead to problems, for example with consistency of the de ned system. We avoid these dangers by making derivations of independent of derivations of t. For an explanation and details see [Gro90].
For s = x1:x2: : : : :xn; xi 2 Actt we write P !s instead of P !x1 !x2 : : : !xn and we say that s is a trace of P . The set of all traces of P will be denoted by T r(P ). By we will denote the empty sequence of actions, by Succ(P ) we will denote the set of all successors of P i.e. Succ(P ) = fP 0jP !s P 0; s 2 Actt g. If set Succ(P ) is nite we say that P is nite state process. We de ne modi ed transitions )xM which "hide" actions from M . Formally, we will write P )xM P 0 for M Actt i P !s1 !x !s2 P 0 for s1; s2 2 M ? and P )sM instead of P )x1 M )M : : : )xn M . We will write x2 x x x P )M if there exists P 0 such that P )M P 0. We will write P )b M P 0 instead of P )M P 0 if x 2 M . Note that )x M is de ned for arbitrary action but in de nitions of security properties we will use it for actions (or sequence of actions) not belonging to M . We can the extend the s de nition of )M for sequences of actions similarly to !. By Sort(P ) we will denote the set of actions from A which can be performed by P . The set of weak timed traces of process P is de ned as T rw(P ) = fs 2 (A [ ftg)?j9P 0:P )sf g P 0g. Two process P and Q are weakly timed trace equivalent (P 'w Q) i T rw(P ) = T rw(Q). We conclude this section with de nitions M-bisimulation and weak timed trace equivalence. De nition 1. Let (TPA; Actt; !) be a labelled transition system (LTS). A relation < TPA TPA is called a M-bisimulation if it is symmetric x and it satis es the following condition: if (P; Q) 2 < and P ! P 0; x 2 Actt then there exists a process Q0 such that Q )bx M Q0 and (P 0; Q0) 2 <. Two processes P; Q are M-bisimilar, abbreviated P M Q, if there exists a M-bisimulation relating P and Q. 3
Information
ow and opacity In this section we will present motivations for new security concepts which will be introduced in the next section. First we de ne an absence-ofinformation- ow property called Strong Nondeterministic Non-Interference (SNNI, for short, see [FGM00]). Suppose that all actions are divided into two groups, namely public (low level) actions L and private (high level) actions H. It is assumed that L [ H = A. Process P has SNNI property (we will write P 2 SN N I) if P n H behaves like P for which all high level actions are hidden (by action ) for an observer. To express this hiding we introduce hiding operator P=M; M A, for which it holds if P !a P 0 then P=M !a P 0=M whenever a 62 M [ M and P=M ! P 0=M whenever a 2 M [ M . Formally, we say that P has SNNI property, and we write P 2 SN N I i P n H 'w P=H. SNNI property assumes an intruder who tries to learn whether a private action was performed by a given process while (s)he can observe only public ones. If this cannot be done then the process has SNNI property. A generalization of this concept is given by opacity (this concept was exploited in [BKR04], [BKMR06] and [Gru07] in a framework of Petri Nets, transition systems and process algebras, respectively. Actions are not divided into public and private ones at the system description level, as it is done for example in [GM04], but a more general concept of observations and predicates is exploited. A predicate is opaque if for any trace of a system for which it holds, there exists another trace for which it does not hold and the both traces are indistinguishable for an observer (which is expressed by an observation function). This means that the observer (intruder) cannot say whether a trace for which the predicate holds has been performed or not.
First we assume an observation function i.e. a function O : Actt? ! ?, where is a set of elements called observables (note that we have no other requirements on O except that it has to be total, i.e. de ned for every sequence of actions). Now suppose that we have some security property. This might be an execution of one or more classi ed actions, an execution of actions in a particular classi ed order which should be kept hidden, etc. Suppose that this property is expressed by a predicate over sequences. We would like to know whether an observer can deduce the validity of the property just by observing sequences of actions from Actt? performed by system of interest. The observer cannot deduce the validity of if there are two sequences w; w0 2 Actt? such that (w); : (w0) and the sequences cannot be distinguished by the observer i.e. obs(w) = obs(w0). We formalize this concept by the notion of opacity. De nition 2 (Opacity). Given process P , a predicate over Actt? is opaque w.r.t. the observation function O if for every sequence w, w 2 T r(P ) such that (w) holds and O(w) 6= , there exists a sequence w0; w0 2 T r(P ) such that : (w0) holds and O(w) = O(w0). The set of processes for which the predicate Op( ; O).
is opaque with respect to O will be denoted by
Now let us assume that an intruder tries to discover, instead of a property over process's traces, whether a given process can reach a state with some given property expressed by a (total) predicate. This might be process deadlock, capability to execute only traces s with time length less then n, capability to perform at the same time actions form a given set, incapacity to idle (to perform t action ) etc. Again we do not put any restriction on such predicates but we only assume that they are consistent with some suitable behavioral equivalence. The formal de nition follows. De nition 3. We say that the predicate over processes is consistent with respect to relation = if whenever P = P 0 then (P ) , (P 0).
As consistency relation = we could take bisimulation ( ;), weak bisimulation ( f g) or any other suitable equivalence. A special class of such predicates are such ones (denoted as =Q) which are de ned by a given process Q and equivalence relation = i.e. =Q(P ) holds i P = Q.
We suppose that the intruder can observe only some activities performed by the process. Hence we suppose that there is a set of public actions which can be observed and a set of hidden (not necessarily private) actions. To model observations we exploit the relation )sM . The formal de nition of process opacity (see [Gru15]) is the following. De nition 4 (Process Opacity). Given process P , a predicate over processes is process opaque w.r.t. the set M if whenever P )sM P 0 for s 2 (Actt n M ) and (P 0) holds then there exists P 00 such that P )sM P 00 and : (P 00) holds. The set of processes for which the predicate is process opaque w.r.t. to the M will be denoted by P Op( ; M ).
Note that if P = P 0 then P 2 P P Op( ; M ) , P 0 2 P Op( ; M ) whenever is consistent with respect to = and = is such that it a subset of the trace equivalence (de ned as 'w but instead of )sf g we use )s;).
Properties opacity and process opacity are depicted in Fig. 1 and 2, respectively. In the former case, a set of actions performed by a process is of interest, say classi ed, in the later case, it is a property of reachable states which is protected by process opacity. 4
Process environment opacity Now we will formulate security properties which protect inputs of a given process. We start with property called process environment opacity which is a modi cation of the the property formulated for programming languages which appeared in [SS15]. Process's inputs will be modeled also by processes, called environments, running in parallel with the process. Moreover, we force (by restriction operator) the process to communicate exclusively with its environment by means of channels contained in given set M . Formally, we assume a set of environments E , i.e. processes which represent possible input environments for a given process. We extend definition of predicates over environments to sets of environments K; K E in the following way. (K) holds i (E) holds for every E 2 K. Moreover, we assume two equivalence relations over processes, =1; =2, which express capability of an intruder to distinguish among processes.
set of environments E , a predicate over processes is environment opaque w.r.t. the set M and =1; =2 if whenever (P jE) n M )s R for s 2 (Actt n M )+ and (E) holds then there exists E0 such that (P jE0) n M )s R0, E =1 E0, : (E0) holds and R =2 R0. The set of processes for which the predicate is environment opaque w.r.t. to the M and =1; =2 will be denoted by P EOp( ; E ; M; =1; =2).
Note that process environment opacity says nothing about security of inputs if (E ) or : (E ) holds. As regards choice of relations =1; =2 it depends on capability of possible intruders. For example, it could be bisimulation, trace equivalence or just the relation equal to T P A T P A. Schematically, process environment opacity is depicted in Fig. 3. (P jE) n M =)s (P jE0) n M=)s
R, and (E) =2 =1
R0 and : (E0) E0 In this subsection we will formulate some properties of process environment opacity.
P EOp( 2; E; M; =1; =2)
P EOp( 1; E; M; =1; =2): Proof. Let P 2 P EOp( 2; E; M; =1; =2) and (P jE) n M )s R for s 2 (Actt n M )+ and 1(P 0) holds. Then also 2(P 0) holds since 1 ) 2. We know that there exists E0 such that (P jE0) n M )s R0, E =1 E0 and : 2(E0) holds and R =2 R0. Since : 2 ) : 1 we have that also : 1(E0) holds and hence P 2 P EOp( 1; E; M; =1; =2). tu
E2 and : (E2 n E1). Then P EOp( ; E1; M; =1; =2)
P EOp( ; E2; M; =1; =2): Proof. Sketch. Let P 2 P EOp( ; E1; M; =1; =2) and (P jE) n M )s R for s 2 (Actt n M )+ and (E) holds for E 2 E1. Since : (E2 n E1) all environments for which holds are from E1. We know that there exists E0 2 E1, E =1 E0, such that (P jE0) n M )s R0 and : (E0) holds and R =2 R0. Since E1 E2 we have that also P 2P EOp( ; E2; M; =1; =2). tu Proposition 3. Let =1 =10. Then
P EOp( ; E; M; =1; =2)
P EOp( ; E; M; =10; =2): Proof. Let P 2 P EOp( ; E; M; =1; =2) and (P jE) n M )s R for s 2 (Actt n M )+ and (E) holds for E 2 E . We now that there exists E0 E0 2 E such that (P jE0) n M )s R0, E =1 E0 and : (E0) holds and R =2 R0. Since =1 =10 we have that also E =10 E0 and hence we have also P 2 P EOp( ; E; M; =10; =2). tu Proposition 4. Let =2 =20. Then
P EOp( ; E; M; =1; =2)
P EOp( ; E; M; =1; =20): Proof. Let P 2 P EOp( ; E ; M; =1; =2) and (P jE) n M )s R for s 2 (Actt n M )+ and (E) holds for E 2 E . We now that there exists E0 E0 2 E such that (P jE0) n M )s R0, E =1 E0 and : (E0) holds and R =2 R0. Since =2 =20 we have that also R =20 R0 and hence we have also P 2 P EOp( ; E ; M; =1; =20 ). tu
As regards compositionality properties of process environment opacity, only a few of them hold. In general, process environment opacity is not compositional even for the pre x operator. Let P 2 P EOp( ; E ; M; =1 ; =2) for such that (A) holds i A !x and x 2 M . Clearly, (x:P jA0) n M cannot perform any action for A0 such that : (A0), i.e. x:P 62 P EOp( ; E ; M; =1; =2). A bit more sophisticated argument leads to the same result also for x 62 M . On the other side, process environment opacity is compositional with respect to non-deterministic choice as it is stated by the following Proposition.
Proposition 5. Let P; Q 2 P EOp( ; E ; M; =1; =2). Then
P + Q 2 P EOp( ; E ; M; =1; =2): Proof. Let (P +QjE)nM )sM R for s 2 (ActtnM )+ and (E) holds. Then without loss of generality we can assume that (P jE) n M )sM R. Since s P 2 P EOp( ; E ; M; =1; =2) there exists E0 such that (P jE0) n M )M R0, E =1 E0 and : (E0) holds and R =2 R0. Hence also (P +QjE0)nM )sM R0 what implies P + Q 2 P EOp( ; E ; M; =1; =2). tu
As regards the rest of TPA operators, the situation is similar as for the pre x operator. 4.2
In this subsection we will compare process environment opacity with NonDeducibility on Composition (NDC for short, see in [FGM03]) which is a widely studied security property. It is based on the idea of checking the system against all high level potential interactions, representing every possible high level process. System is NDC if for every high level user A, the low level view of the behaviour of P is not modi ed (in terms of trace equivalence) by the presence of A. The idea of NDC can be formulated as follows.
H [ f ; tg (P jA) n H 'w P n H:
Now we will formulate relationship between NDC and P EOp( ; E ; H; =1 ; =2) properties. Note that this relationship is similar to the one which appeared in [SS15] for programming languages.
Proposition 6. P 2 N DC i P 2 P EOp( ; E ; H; =1; =2) for E = fE 2 T P AjSort(A) Hg, =2= T P A T P A and for every such that every kernel of =1 contains with every process E from E for which (E) holds also process E0 for which : (E0) holds.
Proof. Sketch. Let P 2 N DC that means that (P jE) n H 'w (P jE0) n H for every two E; E0 such that Sort(E) H; Sort(E0) H. But by the assumption we know that for every such that for every E for which (E) holds there exists E0 for which : (E0) holds and E =1 E0, and this implies that P 2 P EOp( ; E ; H; =1; =2).
Now suppose that P 62 N DC i.e. there exist E; E0 such that (P jE) n H 6'w (P jE0) n H: Without loss of generality we can assume that (P jE) n H )s but (P jE0) n H 6 )s. Hence we can choose predicate such that (E) holds and only environment for which does not hold is equal to E0. Hence P 62 P EOp( ; E ; H; =1; =2). tu 4.3
In this subsection we will formulate several variants of process environment opacity. We will start with its persistent variant.
process P and set of environments E , a predicate over processes is environment persistently opaque w.r.t. the set M and =1; =2 if whenever for every P 0; P 0 2 Succ(P ) we have P 0 2 P EOp( ; E ; M; =1; =2).
The set of processes for which the predicate is persistent environment opaque w.r.t. to the M and =1; =2 will be denoted by P P EOp( ; E ; M; =1 ; =2).
The relationship between process environment opacity and its persistent variant is formulated in by the following Proposition.
Proposition 7. P P EOp( ; E ; M; =1; =2) Proof. The proof follows directly from De nitions 5 and 7. In general, we cannot guarantee that this inclusion is proper. tu
Process environment opacity expresses security of inputs for which given predicate holds but does not say anything about those ones for which it does not hold, i.e. says nothing about security of : . So we de ne a stronger variant of process environment opacity.
cess P and set of environments E , a predicate over processes is strongly environment persistently opaque w.r.t. the set M and =1; =2 if whenever P 2 P EOp( ; E ; M; =1; = ) and P 2 P EOp(: ; E ; M; =1; =2).
2
The set of processes for which the predicate is strongly environment opaque w.r.t. to the M and =1; =2 will be denoted by SP EOp( ; E ; M; =1 ; =2).
Proposition 8. SP EOp( ; E ; M; =1; =2) Proof. Again the proof follows directly from De nitions 5 and 8. and we cannot guarantee that the inclusion is proper as well. tu
The most of properties stated for process environment opacity can be formulated also for its strong variant, some with a slight modi cation.
Till now we have not expected that environments are fully "consumed" by processes. For cases when an intruder can see only results of complete computations we have to modify de nition of process environment opacity. Suppose that all process in E are nite and moreover, the last action performed before reaching (sub)state N il is a new auxiliary action p. That means that for every environment E every occurrence of N il is preceded by p i.e. every N il is always a subterm of a term p:N il. For example, E = a:b:c:p:N il + b:a:p:N il is such a process. We indicate corresponding environments by Ep.
process P and set of environments Ep, a predicate over processes is environment opaque w.r.t. the set M and =1; =2 if whenever (P jE)nM s:p ) R for s 2 (Actt n M )+ and (E) holds then there exists E0 such that s:p (P jE0) n M ) R0, E =1 E0 and : (E0) holds and R =2 R0. The set of processes for which the predicate is termination environment opaque w.r.t. to the M and =1; =2 will be denoted by T P EOp( ; Ep; M; =1; =2).
As regards decidability of proposed security properties, in general they are undecidable. To obtain properties which are decidable, we need restrictions on predicates which should be decidable, limitation to nite set of environments and/or restrictions on equivalences =1; = . 2 5
Discussion and further work We have presented the new security concept called process environment opacity and we have formalized it in the timed process algebra framework. It expresses di erent aspects of processes behaviour as opacity or process opacity. Instead of sequences of actions or resulting processes, it focuses on process's inputs and their properties. We have presented some properties of the resulting security property as well as its variants. Since we worked with timed process algebras we can model security with respect to limited time length of an attack, with a limited number of attempts to perform an attack and so on. Besides investigation of decidable variants of the proposed properties we also plan to study variants of process environment opacity which assume intruders which are not only observers but can actively interact with the systems to be attacked.