=Paper=
{{Paper
|id=Vol-1698/CS&P2016_20_Gruska_Process-Environment-Opacity
|storemode=property
|title=Process Environment Opacity
|pdfUrl=https://ceur-ws.org/Vol-1698/CS&P2016_20_Gruska_Process-Environment-Opacity.pdf
|volume=Vol-1698
|authors=Damas Gruska
|dblpUrl=https://dblp.org/rec/conf/csp/Gruska16
}}
==Process Environment Opacity==
https://ceur-ws.org/Vol-1698/CS&P2016_20_Gruska_Process-Environment-Opacity.pdf
Process Environment Opacity
Damas P. GRUSKA
Institute of Informatics, Comenius University,
Mlynska dolina, 842 48 Bratislava, Slovakia,
gruska@fmph.uniba.sk.
Abstract. A security property called process environment opacity is for-
malized 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 for-
mulated in various ways. The resulting security properties are compared.
Keywords: security, opacity, process algebras, information flow
1 Introduction
Information flow based security properties (see [GM82]) assume an ab-
sence of any information flow between private and public systems ac-
tivities. This means, that systems are considered to be secure if from
observations of their public activities no information about private activ-
ities 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 pred-
icate holds has been performed or not. In [Gru15] opacity is modified (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 as-
sume 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 satisfied some given (classified) predicate. It turns out that
in this way we could capture some new security flaws. Both opacity and
process opacity are based on fixed (static) security policy which is not
changed during system computation. In [Gru16] process opacity for dy-
namic security policies is formalized. All of these properties are defined 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 defined 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 envi-
ronments 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 flow security based on opacity
and in the next section process environment opacity is defined, studied
and compared to other security properties. Section 5 contains discussion
and plans for future work.
2 Timed Process Algebra
In this section we define 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
simplification 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 spec-
ification). 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 differs 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.
To define the language TPA, we first assume a set of atomic action
symbols A not containing symbols τ and t, and such that for every a ∈ A
there exists a ∈ A and a = a. We define Act = A ∪ {τ }, At = A ∪
{t}, Actt = Act ∪ {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∈{0,1,2} Σn , where
Σ0 = {N il}
Σ1 = {x. | x ∈ A ∪ {t}} ∪ {[S] | S is a relabeling function}
∪{\M | M ⊆ A}
Σ2 = {|, +}
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 : Actt → Actt are such that S(a) = S(ā)
for a ∈ A, S(τ ) = τ and S(t) = t.
The set of TPA terms over the signature Σ is defined 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 TPA
terms, µX− is the binding construct, op ∈ Σ.
The set of CCS terms consists of TPA terms without t action. We will
use an usual definition 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 finitely
many non timed actions can be performed) are called TPA processes.
We give a structural operational semantics of terms by means of la-
beled transition systems. The set of terms represents a set of states,
labels are actions from Actt. The transition relation → is a subset of
x
TPA × Actt × TPA. We write P → P 0 instead of (P, x, P 0 ) ∈ → and
x x
P →6 if there is no P 0 such that P → P 0 . The meaning of the expression
x
P → P 0 is that the term P can evolve to P 0 by performing action x, by
x x
P → we will denote that there exists a term P 0 such that P → P 0 . We
define the transition relation as the least relation satisfying the inference
rules for CCS plus the following inference rules:
t
A1 t
A2
N il → N il u.P → u.P
t t τ t t
P → P 0 , Q → Q0 , P | Q →
6 P → P 0 , Q → Q0
t
Pa t
S
P | Q → P 0 | Q0 P + Q → P 0 + Q0
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 definition 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 defined system. We avoid
these dangers by making derivations of τ independent of derivations of t.
For an explanation and details see [Gro90].
s x x xn
For s = x1 .x2 . . . . .xn , xi ∈ Actt we write P → instead of P →1 →2 . . . →
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 ) =
s
{P 0 |P → P 0 , s ∈ Actt∗ }. If set Succ(P ) is finite we say that P is finite
x
state process. We define modified transitions ⇒M which ”hide” actions
x s1 x s2
from M . Formally, we will write P ⇒M P 0 for M ⊆ Actt iff P → →→ P 0
s x x x
for s1 , s2 ∈ M ? and P ⇒M instead of P ⇒M ⇒M . . . ⇒M . We will write
1 2 n
x x x
P ⇒M if there exists P 0 such that P ⇒M P 0 . We will write P ⇒M P 0
b
x
instead of P ⇒M P 0 if x ∈ M . Note that ⇒M is defined for arbitrary
action but in definitions of security properties we will use it for actions
(or sequence of actions) not belonging to M . We can the extend the
s
definition 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 defined as T rw (P ) = {s ∈
s
(A ∪ {t})? |∃P 0 .P ⇒{τ } P 0 }. Two process P and Q are weakly timed trace
equivalent (P 'w Q) iff T rw (P ) = T rw (Q). We conclude this section with
definitions M-bisimulation and weak timed trace equivalence.
Definition 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 satisfies the following condition: if (P, Q) ∈ < and P → P 0 , x ∈
x
Actt then there exists a process Q0 such that Q ⇒M Q0 and (P 0 , Q0 ) ∈ <.
b
Two processes P, Q are M-bisimilar, abbreviated P ≈M Q, if there exists
a M-bisimulation relating P and Q.
3 Information flow and opacity
In this section we will present motivations for new security concepts which
will be introduced in the next section. First we define an absence-of-
information-flow 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 ∈ SN N I) if P \ H behaves like P for which all high level
actions are hidden (by action τ ) for an observer. To express this hiding
a
we introduce hiding operator P/M, M ⊆ A, for which it holds if P → P 0
a τ
then P/M → P 0 /M whenever a 6∈ M ∪ M̄ and P/M → P 0 /M whenever
a ∈ M ∪ M̄ . Formally, we say that P has SNNI property, and we write
P ∈ SN N I iff P \ 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. defined
for every sequence of actions). 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 a predi-
cate φ over sequences. We would like to know whether an observer can
deduce the validity of the property φ just by observing sequences of ac-
tions from Actt? performed by system of interest. The observer cannot
deduce the validity of φ if there are two sequences w, w0 ∈ 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.
Definition 2 (Opacity). Given process P , a predicate φ over Actt? is
opaque w.r.t. the observation function O if for every sequence w, w ∈
T r(P ) such that φ(w) holds and O(w) 6= , there exists a sequence w0 , w0 ∈
T r(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).
w
P =⇒
O(w) = O(w0 ) and φ(w), ¬φ(w0 )
w0
P =⇒
Fig. 1. Opacity
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 definition follows.
Definition 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 (≈{τ } ) or any other suitable equivalence. A special class of
such predicates are such ones (denoted as φQ = ) which are defined by a
∼
∼
given process Q and equivalence relation = i.e. φQ ∼
= (P ) holds iff P = Q.
∼
We suppose that the intruder can observe only some activities per-
formed 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 pri-
s
vate) actions. To model observations we exploit the relation ⇒M . The
formal definition of process opacity (see [Gru15]) is the following.
Definition 4 (Process Opacity). Given process P , a predicate φ over
s
processes is process opaque w.r.t. the set M if whenever P ⇒M P 0 for
s
s ∈ (Actt \ M )∗ and φ(P 0 ) holds then there exists P 00 such that P ⇒M 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 ∈ P P Op(φ, M ) ⇔ P 0 ∈ P Op(φ, M )
whenever φ is consistent with respect to ∼
= and ∼= is such that it a subset
s s
of the trace equivalence (defined as 'w but instead of ⇒{τ } we use ⇒∅ ).
s
P =⇒M φ(P 0 )
s
P =⇒M ¬φ(P 00 )
Fig. 2. Process opacity
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 classified, 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 modification of the the property formulated for programming lan-
guages 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 def-
inition of predicates over environments to sets of environments K, K ⊆ E
in the following way. φ(K) holds iff φ(E) holds for every E ∈ K. More-
over, we assume two equivalence relations over processes, ∼ =1 , ∼
=2 , which
express capability of an intruder to distinguish among processes.
Definition 5 (Process Environment Opacity). Given process P and
set of environments E, a predicate φ over processes is environment opaque
s
w.r.t. the set M and ∼ =1 , ∼
=2 if whenever (P |E) \ M ⇒ R for s ∈ (Actt \
s
M )+ and φ(E) holds then there exists E 0 such that (P |E 0 ) \ M ⇒ R0 ,
E ∼=1 E 0 , ¬φ(E 0 ) 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.
s
(P |E) \ M =⇒ R, and φ(E) E
∼
=2 ∼
=1
s
(P |E 0 ) \ M =⇒ R0 and ¬φ(E 0 ) E0
Fig. 3. Process environment opacity
4.1 Properties of process environment opacity
In this subsection we will formulate some properties of process environ-
ment opacity.
Proposition 1. Let φ1 ⇒ φ2 . Then
P EOp(φ2 , E, M, ∼
=1 , ∼
=2 ) ⊆ P EOp(φ1 , E, M, ∼
=1 , ∼
=2 ).
s
Proof. Let P ∈ P EOp(φ2 , E, M, ∼ =1 , ∼
=2 ) and (P |E) \ M ⇒ R for s ∈
(Actt \ M )+ and φ1 (P 0 ) holds. Then also φ2 (P 0 ) holds since φ1 ⇒ φ2 .
s
We know that there exists E 0 such that (P |E 0 ) \ M ⇒ R0 , E ∼ =1 E 0 and
¬φ2 (E ) holds and R ∼
0
= R . Since ¬φ2 ⇒ ¬φ1 we have that also ¬φ1 (E 0 )
2 0
holds and hence P ∈ P EOp(φ1 , E, M, ∼ =1 , ∼
=2 ). t
u
Proposition 2. Let E1 ⊆ E2 and ¬φ(E2 \ E1 ). Then
P EOp(φ, E1 , M, ∼
=1 , ∼
=2 ) ⊆ P EOp(φ, E2 , M, ∼
=1 , ∼
=2 ).
s
Proof. Sketch. Let P ∈ P EOp(φ, E1 , M, ∼ =1 , ∼
=2 ) and (P |E) \ M ⇒ R
for s ∈ (Actt \ M )+ and φ(E) holds for E ∈ E1 . Since ¬φ(E2 \ E1 ) all
environments for which φ holds are from E1 . We know that there exists
s
E 0 ∈ E1 , E ∼=1 E 0 , such that (P |E 0 ) \ M ⇒ R0 and ¬φ(E 0 ) holds and
R∼ =2 R0 . Since E1 ⊆E2 we have that also P ∈P EOp(φ, E2 , M, ∼ =1 , ∼
=2 ). t
u
0
Proposition 3. Let ∼
=1 ⊆∼
=1 . Then
0
P EOp(φ, E, M, ∼
=1 , ∼
=2 ) ⊆ P EOp(φ, E, M, ∼
=1 , ∼
=2 ).
s
Proof. Let P ∈ P EOp(φ, E, M, ∼ =1 , ∼
=2 ) and (P |E) \ M ⇒ R for s ∈
(Actt \ M )+ and φ(E) holds for E ∈ E . We now that there exists E 0
s
E 0 ∈ E such that (P |E 0 ) \ M ⇒ R0 , E ∼ =1 E 0 and ¬φ(E 0 ) holds and
0 0
R∼ = R . Since ∼
2 0
= ⊆∼
1
= we have that also E ∼
1
=1 E 0 and hence we have
0
also P ∈ P EOp(φ, E, M, ∼=1 , ∼=2 ). t
u
0
Proposition 4. Let ∼
=2 ⊆∼
=2 . Then
0
P EOp(φ, E, M, ∼
=1 , ∼
=2 ) ⊆ P EOp(φ, E, M, ∼
=1 , ∼
=2 ).
s
Proof. Let P ∈ P EOp(φ, E, M, ∼ =1 , ∼
=2 ) and (P |E) \ M ⇒ R for s ∈
(Actt \ M )+ and φ(E) holds for E ∈ E . We now that there exists E 0
s
E 0 ∈ E such that (P |E 0 ) \ M ⇒ R0 , E ∼ =1 E 0 and ¬φ(E 0 ) holds and
0 0
R∼ =2 R0 . Since ∼
=2 ⊆∼
=2 we have that also R ∼ =2 R0 and hence we have
0
also P ∈ P EOp(φ, E, M, ∼=1 , ∼
=2 ). t
u
As regards compositionality properties of process environment opac-
ity, only a few of them hold. In general, process environment opacity is not
compositional even for the prefix operator. Let P ∈ P EOp(φ, E, M, ∼ =1
x̄
,∼
=2 ) for φ such that φ(A) holds iff A → and x ∈ M . Clearly, (x.P |A0 )\M
cannot perform any action for A0 such that ¬φ(A0 ), i.e.
x.P 6∈ P EOp(φ, E, M, ∼ =1 , ∼
=2 ). A bit more sophisticated argument leads
to the same result also for x 6∈ 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 ∈ P EOp(φ, E, M, ∼
=1 , ∼
=2 ). Then
P + Q ∈ P EOp(φ, E, M, ∼
=1 , ∼
=2 ).
s
Proof. Let (P +Q|E)\M ⇒M R for s ∈ (Actt\M )+ and φ(E) holds. Then
s
without loss of generality we can assume that (P |E) \ M ⇒M R. Since
s
P ∈ P EOp(φ, E, M, ∼=1 , ∼
=2 ) there exists E 0 such that (P |E 0 ) \ M ⇒M R0 ,
s
E∼= E and ¬φ(E ) holds and R ∼
1 0 0
= R . Hence also (P +Q|E )\M ⇒M R0
2 0 0
what implies P + Q ∈ P EOp(φ, E, M, ∼ =1 , ∼
=2 ).
t
u
As regards the rest of TPA operators, the situation is similar as for
the prefix operator.
4.2 Process environment opacity and Non-Deducibility
In this subsection we will compare process environment opacity with Non-
Deducibility 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 modified (in terms of trace
equivalence) by the presence of A. The idea of NDC can be formulated
as follows.
Definition 6. (NDC) P ∈ N DC iff for every A, Sort(A) ⊆ H ∪ {τ, t}
(P |A) \ H 'w P \ 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 ∈ N DC iff P ∈ P EOp(φ, E, H, ∼ =1 , ∼
=2 ) for E = {E ∈
T P A|Sort(A) ⊆ H}, ∼ =2 = T P A × T P A and for every φ such that every
∼ 1
kernel of = contains with every process E from E for which φ(E) holds
also process E 0 for which ¬φ(E 0 ) holds.
Proof. Sketch. Let P ∈ N DC that means that (P |E) \ H 'w (P |E 0 ) \ H
for every two E, E 0 such that Sort(E) ⊆ H, Sort(E 0 ) ⊆ H. But by the
assumption we know that for every φ such that for every E for which
φ(E) holds there exists E 0 for which ¬φ(E 0 ) holds and E ∼
=1 E 0 , and this
implies that P ∈ P EOp(φ, E, H, ∼ =1 , ∼
=2 ).
Now suppose that P 6∈ N DC i.e. there exist E, E 0 such that (P |E) \
H 6'w (P |E 0 ) \ H. Without loss of generality we can assume that (P |E) \
s s
H ⇒ but (P |E 0 ) \ H ⇒.
6 Hence we can choose predicate φ such that φ(E)
holds and only environment for which φ does not hold is equal to E 0 .
Hence P 6∈ P EOp(φ, E, H, ∼ =1 , ∼
=2 ). t
u
4.3 Variants of process environment opacity
In this subsection we will formulate several variants of process environ-
ment opacity. We will start with its persistent variant.
Definition 7 (Persistent Process Environment Opacity). Given
process P and set of environments E, a predicate φ over processes is envi-
ronment persistently opaque w.r.t. the set M and ∼ =1 , ∼
=2 if whenever for
every P 0 , P 0 ∈ Succ(P ) we have P 0 ∈ 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 persis-
tent variant is formulated in by the following Proposition.
Proposition 7. P P EOp(φ, E, M, ∼
=1 , ∼
=2 ) ⊆ P EOp(φ, E, M, ∼
=1 , ∼
=2 )
Proof. The proof follows directly from Definitions 5 and 7. In general, we
cannot guarantee that this inclusion is proper. t
u
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
define a stronger variant of process environment opacity.
Definition 8 (Strong Process Environment Opacity). Given pro-
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 ∈ P EOp(φ, E, M, ∼ =1 , ∼
=2 ) and P ∈ P EOp(¬φ, E, M, ∼ =1 , ∼
=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 ) ⊆ P EOp(φ, E, M, ∼
=1 , ∼
=2 )
Proof. Again the proof follows directly from Definitions 5 and 8. and we
cannot guarantee that the inclusion is proper as well. t
u
The most of properties stated for process environment opacity can be
formulated also for its strong variant, some with a slight modification.
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 definition of process environment opac-
ity. Suppose that all process in E are finite and moreover, the last action
√
performed before reaching (sub)state N il is a new auxiliary action .
That means that for every environment E every occurrence of N il is
√ √
preceded by i.e. every N il is always a subterm of a term .N il. For
√ √
example, E = a.b.c. .N il + b.a. .N il is such a process. We indicate
corresponding environments by E√ .
Definition 9 (Termination Process Environment Opacity). Given
process P and set of environments E√ , a predicate φ over processes is
√
environment opaque w.r.t. the set M and ∼1 , ∼2 if whenever (P |E)\M s.
⇒
= =
R for s ∈ (Actt √
\ M )+ and φ(E) holds then there exists E 0 such that
s.
(P |E 0 ) \ M ⇒ R0 , E = ∼1 E 0 and ¬φ(E 0 ) 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(φ, E√ , M, ∼
=1 , ∼
=2 ).
As regards decidability of proposed security properties, in general they
are undecidable. To obtain properties which are decidable, we need re-
strictions on predicates which should be decidable, limitation to finite 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 different 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.
References
[BKR04] Bryans J., M. Koutny and P. Ryan: Modelling non-deducibility using Petri
Nets. Proc. of the 2nd International Workshop on Security Issues with Petri
Nets and other Computational Models, 2004.
[BKMR06] Bryans J., M. Koutny, L. Mazare and P. Ryan: Opacity Generalised to
Transition Systems. In Proceedings of the Formal Aspects in Security and
Trust, LNCS 3866, Springer, Berlin, 2006.
[DHS15] van Delft B., S. Hunt, D. Sands: Very Static Enforcement of Dynamic Poli-
cies. In Principles of Security and Trust, LMCS 9036, 2015.
[FGM03] Focardi R., R. Gorrieri and F. Martinelli: Real-Time information flow anal-
ysis. IEEE Journal on Selected Areas in Communications 21 (2003).
[FGM00] Focardi, R., R. Gorrieri, and F. Martinelli: Information flow analysis in
a discrete-time process algebra. Proc. 13th Computer Security Foundation
Workshop, IEEE Computer Society Press, 2000.
[GM04] Gorrieri R. and F. Martinelli: A simple framework for real-time crypto-
graphic protocol analysis with compositional proof rules. Science of Com-
puter Programming, Volume 50, Issues 13, 2004.
[GM82] Goguen J.A. and J. Meseguer: Security Policies and Security Models. Proc.
of IEEE Symposium on Security and Privacy, 1982.
[GM04] Gorrieri R. and F. Martinelli: A simple framework for real-time crypto-
graphic protocol analysis with compositional proof rules. Science of Com-
puter Programming, Volume 50, Issues 13, 2004.
[Gro90] Groote, J. F.: Transition Systems Specification with Negative Premises.
Proc. of CONCUR’90, Springer Verlag, Berlin, LNCS 458, 1990.
[Gru15] Gruska D.P.: Process Opacity for Timed Process Algebra. In Perspectives
of System Informatics, LNCS 8974, 2015.
[Gru16] Gruska D.P.: Dynamic Security Policies and Process Opacity, In Proc of
Perspectives of System Informatics, to appeare in LNCS, 2016.
[Gru10] Gruska D.P.: Process Algebra Contexts and Security Properties. Funda-
menta Informaticae, vol. 102, Number 1, 2010.
[Gru07] Gruska D.P.: Observation Based System Security. Fundamenta Informati-
cae, vol. 79, Numbers 3-4, 2007.
[KS83] Kanellakis, P. C. and S.A. Smolka: CCS expressions, finite state processes,
and three problems of equivalence. Proc. of The second annual ACM sym-
posium on Principles of distributed computing, ACM, 1983.
[SS15] Schoepe D. and A. Sabelfeld: Understanding and Enforcing Opacity. Proc.
of IEEE 28th Computer Security Foundations Symposium, 2015.