=Paper=
{{Paper
|id=Vol-2240/paper12
|storemode=property
|title=Hidden States in Reaction Systems
|pdfUrl=https://ceur-ws.org/Vol-2240/paper12.pdf
|volume=Vol-2240
|authors=Roberta Gori,Damas Gruska,Paolo Milazzo
|dblpUrl=https://dblp.org/rec/conf/csp/GoriGM18
}}
==Hidden States in Reaction Systems==
https://ceur-ws.org/Vol-2240/paper12.pdf
Hidden States in Reaction Systems ?
Roberta Gori1 , Damas Gruska2 , and Paolo Milazzo1
1
Dipartimento di Informatica, Università di Pisa, Italy
2
Department of Applied Informatics, Faculty of Mathematics, Physics and Informatics,
Comenius University in Bratislava, Slovak Republic
Abstract. Pushing forward a previous investigation on security of reaction
systems, we introduce new state based security properties. Assume there are
some states of a reaction system that are in some sense critical, and that
we want to hide whether the system reaches them. We define new security
properties that guarantee that an external observer who has only a partial
knowledge on the objects provided by the environment cannot infer whether
a secret state is reached by the system. We also propose an effective method
for verifying such properties. The verification method is based on a newly
defined extension of the concept of formula based predictor to set of states.
1 Introduction
Reaction systems is a qualitative modeling formalism introduced by Ehrenfeucht
and Rozenberg to model biological systems [1, 2]. It is based on the two opposite
mechanisms of facilitation and inhibition. Facilitation means that a reaction can
occur only if all its reactants are present, while inhibition means that the reaction
cannot occur if any of its inhibitors is present. A reaction system is essentially a
set of rewrite rules (reactions) having the form (R, I, P ), where R, I and P are sets
of objects representing reactants, inhibitors and products, respectively. The state
of a reaction system is a finite set of objects, describing the biological entities that
are present in the modeled system. The presence of an object in the state means
that the corresponding biological entity is present in a number of copies as high as
needed. This is the threshold supply assumption and characterizes reaction systems.
A reaction system evolves by means of the application of its reactions.The thresh-
old supply assumption ensures that all the applicable reactions in a step are always
applied, since they do not compete for thier reactants. The application of a set of
reactions results in the introduction of all of their products in the next state of
the system. The behaviour of a reaction system is driven by the (set of) contextual
elements which are provided by the external environment at each step. Such ele-
ments join the current state of the system and can enable or disable reactions. The
computation of the next state of a reaction system is a deterministic procedure.
Consequently, if the contextual elements provided to the system at each step are
know, then the whole execution of the system is determined. On the other hand, if
they are not known, the overall system dynamics becomes non deterministic.
?
Work supported by the grant VEGA 1/0778/18 and by the project “Metodologie infor-
matiche avanzate per l’analisi di dati biomedici” (University of Pisa, PRA 2017 44).
In previous papers [3, 4] we investigated the concept of opacity in reaction sys-
tems. Assume we have a real biochemical system described by a reaction system,
and an observer having a partial information about the objects provided by the en-
vironment because of the cost of obtaining such informaton. We can distinguish two
types of objects: visible low level (L) objects, and invisible high level (H) objects.
We studied the detectability of H-objects, namely how much information on the
presence of H-objects can be obtained by just observing the presence of L-objects in
context sequences. This problem, called information flow [5], was extensively stud-
ied in security by introducing the concept of opacity [6, 7]. We reformulated opacity
for reaction systems and proposed dynamic causality relatioships (formula based
predictors) as an effective method to verify opacity properties in reaction systems.
In this paper we push forward our approach by considering sets of secret states.
Let Sec be a set of states and assume we want to hide to an external observer
whether a reaction system reaches one of such states. So, Sec is a set of secret
states. As before, the observer can only see L-objects in context sequences. In order
to prevent the observer to infer whether the system reaches a secret state, we have
to ensure that for every context sequence leading to one of such states there exists
another context sequence leading to a non-secret state that is indistinguishable from
the previous one from the (limited) point of view of the observer. In other words, the
two context sequences must make the same use of L-objects, which are the only ones
that can be observed. We will formalize this idea in terms of two security properties
called Current State Opacity and n-p Window Current state Opacity, and we will
provide effective methods for verifying them based on dynamic causalities.
Dynamic causalities deal with the ways entities dynamically influence each other.
Brijder, Ehrenfeucht and Rozenberg initiated an investigation on causalities in reac-
tion systems [8], by introducing the idea of predictor. Assume that one is interested
in knowing whether a particular object s ∈ S will be present after n steps of ex-
ecution of the reaction system. Since the only source of non-determinism are the
contextual elements received at each step, knowing which objects will be received
allows the production of s after n steps to be predicted. In [9–12] the new notion of
formula based predictor was introduced. A formula based predictor is a propositional
logic formula to be satisfied by the sequence of (sets of) elements provided by the
environment. Satisfaction of the logic formula precisely discriminates the cases in
which s will be produced after n steps from those in which it will not. In the style of
[13, 14], here the notion of formula-based predictor is first naturally extended to sets
of objects (states), and then it is extended to sets of states. The result is a formula
based predictor that can be used to precisely characterize all context sequences that
lead to one secret state in a set Sec. We apply this extended predictor for secret
states in Sec to prove whether the reaction system is opaque for an observer that
can only see L-objects of the context sequence provided by the environment.
2 Reaction Systems
In this section we briefly introduce reaction systems [1, 2]. Given S, a finite set of
symbols, called objects, a reaction is a triple (R, I, P ) with R, I, P ⊆ S, composed
of reactants R, inhibitors I, and products P . Reactants and inhibitors are disjoint
(R ∩ I = ∅) otherwise the reaction would never be applicable. The set of all possible
reactions over a set S is denoted by rac(S). Finally, a reaction system is a pair
A = (S, A), with S a finite background set, and A ⊆ rac(S) a set of reactions.
The state of a reaction system is a set of objects. Let a = (Ra , Ia , Pa ) be a
reaction and T be a set of objects. The result resa (T ) of the application of a to T is
either Pa , if T separates Ra from Ia (i.e. Ra ⊆ T and Ia ∩ T = ∅), or the empty set
∅ otherwise. The application of multiple reactions at the same time occurs without
any competition for the used reactants (threshold supply assumption). Therefore,
each reaction for which no inhibitor is present in the current state is applied, and
the result of application of multiple reactions is cumulative. Given a reaction system
A = (S, A), S the result of the application of A to a set T ⊆ S is defined as resA (T ) =
resA (T ) = a∈A resa (T ). An important characteristic of reaction systems is the
assumption about the non-permanency of objects: the objects carried over to the
next step are only those produced by reactions. All the other objects vanish.
The dynamics of a reaction system A = (S, A) is driven by the contextual ob-
jects, namely the objects which are supplied to the system by the external envi-
ronment at each step. The dynamics is defined as an interactive process π = (γ, δ),
with γ and δ being finite sequences of sets of objects called the context sequence and
the result sequence, respectively. The sequences are of the form γ = C0 , C1 , . . . , Cn
and δ = D0 , D1 , . . . , Dn for some n ≥ 1, with Ci , Di ⊆ S, and D0 = ∅. Each set
Di , for i ≥ 1, in the result sequence is obtained from the application of reactions A
to a state composed of both the results of the previous step Di−1 and the objects
Ci−1 from the context; formally Di = resA (Ci−1 ∪ Di−1 ) for all 1 ≤ i ≤ n. Finally,
the state sequence of π is the sequence W0 , W1 , . . . , Wn , where Wi = Ci ∪ Di for all
1 ≤ i ≤ n. In the following we call γ = C0 , C1 , . . . , Cn a n-step context sequence.
3 Preliminaries on Predicate Logic
The aim of formula based predictors is to characterize all context sequences that
lead to the production of a specific object in a given number of steps. In order to
describe conditions on the presence or absence of objects in context sequences, we
use objects of reaction systems as propositional symbols. Formally, we define the set
FS of propositional formulas on S in the standard way: S ∪ {true, f alse} ⊆ FS and
¬f1 , f1 ∨ f2 , f1 ∧ f2 ∈ FS if f1 , f2 ∈ FS . Propositional formulas FS are interpreted
with respect to subsets of S. Intuitively, a subset C ⊆ S is used to describe the
objects that are present in (an element of) a context sequence, and this implies
the truth of the corresponding propositional symbol. The formal definition of the
satisfaction relation is as follows.
Definition 1. Let C ⊆ S for a set of objects S. Given a propositional formula
f ∈ FS , the satisfaction relation C |= f is inductively defined as follows:
C |= s iff s ∈ C, C |= true,
C |= ¬f 0 iff C 6|= f 0 , C |= f1 ∨ f2 iff either C |= f1 or C |= f2 ,
C |= f1 ∧ f2 iff C |= f1 and C |= f2 .
In the following ≡l stands for the logical equivalence on propositional formulas FS .
Moreover, given a formula f ∈ FS we use atom(f ) to denote the set of propositional
symbols that appear in f . The simplified version of a formula is obtained by applying
the standard formula simplification procedure of propositional logic converting a
formula to Disjunctive Normal Form, DN F(f ). We recall that for any formula
f ∈ FS the simplified formula DN F(f ) is equivalent to f , it is minimal with
respect to the number of propositional symbols and unique up to commutativity
and associativity. Thus, we have f ≡l DN F(f ) and atom(DN F(f )) ⊆ atom(f )
and there exists no formula f 0 such that f 0 ≡l f and atom(f 0 ) ⊂ atom(DN F(f )).
The causes of an object in a reaction system are defined by a propositional
formula on the set of objects S. First of all we define the applicability predicate of
a reaction a as a formula describing the requirements for applicability of a, namely
that all reactants have to be present and inhibitors have to be absent. This is
represented by the conjunction of all atomic formulas representing reactants and the
negations of all atomic formulas representing inhibitors of the considered reaction.
Definition 2. Let a = (R, I, P ) be a reaction with R, I, P ⊆ S for a set of objects
S.
VThe applicability
V predicate
of a, denoted by ap(a), is defined as follows: ap(a) =
s
sr ∈R r ∧ si ∈I ¬si .
The causal predicate of a given object s is a propositional formula on S representing
the conditions for the production of s in one step, namely that at least one reaction
having s as a product has to be applicable.
Definition 3. Let gA = (S, A) be a r.s. and s ∈ S. The causal predicate of s in A,
denoted by cause(s, A) (orWcause(s), when A is clear from the context), is defined
as follows3 : cause(s, A) = {(R,I,P )∈A|s∈P } ap ((R, I, P )) .
We introduce a simple reaction system as running example.
Example 1. Let A1 = ({A, . . . , G}, {a1 , a2 , a3 }) be a reaction system with
a1 = ({A}, {}, {B}) a2 = ({C, D}, {}, {E, F }) a3 = ({G}, {B}, {E}) .
The applicability predicates of the reactions are ap(a1 ) = A, ap(a2 ) = C ∧ D and
ap(a3 ) = G ∧ ¬B. Thus, the causal predicates of the objects are
cause(A) = cause(C) = cause(D) = cause(G) = f alse,
cause(B) = A, cause(F ) = C ∧ D, cause(E) = (G ∧ ¬B) ∨ (C ∧ D).
Note that cause(A) = f alse given that A cannot be produced by any reaction. An
analogous reasoning holds for objects C, D and G.
4 Formula Based Predictors
In the first part of this section we introduce the notion of formula based predictor
as it was originally presented in [9]. Then, we extend the notion of predictors to
3
We assume that cause(s) = f alse if there is no (R, I, P ) ∈ A such that s ∈ P .
states (see Corollary 1) and to sets of states (see Corollary 2) in order to address
causal dependences of the secret states set Sec that we want to hide.
A formula based predictor for an object s at step n+1 is a propositional formula
satisfied exactly by the context sequences leading to the production of s at step n+1.
Minimal formula based predictors can be calculated in an effective way.
Given a set of objects S, we consider a corresponding set of labelled objects
S × IN. For theSsake of legibility, we denote (s, i) ∈ S × IN simply as si and we
n
introduce S n = i=0 Si where Si = {si | s ∈ S}. Propositional formulas on labelled
n
objects S describe properties of n-step context sequences. The set of propositional
formulas on S n , denoted by FS n , is defined analogously to the set FS (presented in
Sect. 3) by replacing S with S n . Similarly, the set FSi can be defined by replacing
S with Si . Given a formula f ∈ FS , a corresponding formula labelled(f, i) ∈ FSi
can be obtained by replacing each s ∈ S in f with si ∈ Si .
A labelled object si represents the presence (or the absence, if negated) of object
s in the i-th element Ci of the n-step context sequence γ = C0 , C1 , . . . Cn . This in-
terpretation leads to the following definition of satisfaction relation for propositional
formulas on context sequences.
Definition 4. Let γ = C0 , C1 , . . . Cn be a n-step context sequence and f ∈ FS n a
propositional formula. The satisfaction relation γ |= f is defined as
{si | s ∈ Ci , 0 ≤ i ≤ n} |= f .
As an example, let us consider the context sequence γ = C0 , C1 where C0 = {A, C}
and C1 = {B}. We have that γ satisfies the formula A0 ∧ B1 (i.e. γ |= A0 ∧ B1 )
while γ does not satisfy the formula A0 ∧ (¬B1 ∨ C1 ) (i.e. γ 6|= A0 ∧ (¬B1 ∨ C1 )).
The latter notion of satisfaction allows us to define formula based predictor.
Definition 5 (Formula based Predictor). Let A = (S, A) be a reaction system,
s ∈ S and f ∈ FS n a propositional formula. We say that f f-predicts s in n + 1
steps if for any n-step context sequence γ = C0 , . . . , Cn
γ |= f ⇔ s ∈ Dn+1
where δ = D0 , . . . , Dn is the result sequence corresponding to γ and Dn+1 =
resA (Cn ∪ Dn ).
Note that if formula f f-predicts s in n + 1 steps and if f 0 ≡l f then also f 0 f-
predicts s in n + 1. More specifically, we are interested in the formulas that f-predict
s in n + 1 and contain the minimal numbers of propositional symbols, so that their
satisfiability can easily be verified. This is formalised by the following approximation
order on FS n .
Definition 6 (Approximation Order). Given f1 , f2 ∈ FS n we say that f1 vf f2
if and only if f1 ≡l f2 and atom(f1 ) ⊆ atom(f2 ).
In [9] it is shown that there exists a unique equivalence class of formula based
predictors for s in n + 1 steps that is minimal with respect to the order vf .
We now define an operator fbp that allows formula based predictors to be ef-
fectively computed.
Definition 7. Let A = (S, A) be a r.s. and s ∈ S. We define a function fbp :
S × IN → FS n as follows: fbp(s, n) = fbs(cause(s), n), where the auxiliary function
fbs : FS × IN → FS n is recursively defined as follows:
fbs(s, 0) = s0 fbs(s, i) = si ∨ fbs(cause(s), i − 1) if i > 0
fbs((f 0 ), i) = (fbs(f 0 , i)) fbs(f1 ∨ f2 , i) = fbs(f1 , i) ∨ fbs(f2 , i)
fbs(¬f 0 , i) = ¬fbs(f 0 , i) fbs(f1 ∧ f2 , i) = fbs(f1 , i) ∧ fbs(f2 , i)
fbs(true, i) = true fbs(f alse, i) = f alse
The function fbp gives a formula based predictor that, in general, may not be min-
imal with respect to the approximation order vf . Therefore, the calculation of a
minimal formula based predictor requires the application of the standard simplifica-
tion procedure that simplifies the obtained logic formula and puts it in disjunctive
normal form, here called simply DN F(.).
Theorem 1. Let A = (S, A) be a r.s.. For any object s ∈ S,
– fbp(s, n) f-predicts s in n + 1 steps;
– DN F(fbp(s, n)) f-predicts s in n + 1 steps and is minimal w.r.t. vf .
Example 2. Let us consider again the reaction system A1 of Ex. 1. We are interested
in the production of E after 4 steps. Hence, we calculate the logic formula that f-
predicts E in 4 steps applying the function fbp:
fbp(E, 3) = fbs (G ∧ ¬B) ∨ (C ∧ D), 3
= fbs(G, 3) ∧ ¬fbs(B, 3) ∨ fbs(C, 3) ∧ fbs(D, 3)
= (G3 ) ∧ ¬(B3 ∨ fbs(A,
2))) ∨ (C3 ∧ D3 )
= G3 ∧ ¬B3 ∧ ¬A2 ∨ (C3 ∧ D3 )
A context sequence satisfies fbp(E, 3) iff the execution of the reaction system leads
to the production of object E after 4 steps. Furthermore, in this case the obtained
formula is also minimal w.r.t. vf . This is because DN F(fbp(E, 3)) = fbp(E, 3).
Indeed, the formula fbp(E, 3) cannot be further simplified and any literal cannot
be canceled without obtaining a non equivalent formula.
The result of Theorem 1 can be easily extended to states. Indeed, we can char-
acterize all the context sequences that lead to the production of the set of objects
of the state. To this aim, we need to consider the context sequences that satisfy all
conditions for the production of each single object of the set. Assume sec to be a
state, that is, a set of objects in S then we can characterize all the context sequence
leading to states in the following way.
Corollary 1. Let A = (S, A) be a r.s.. Consider sec a set of objects in S,
V
– s∈sec fbp(s, n) f-predicts
sec in n + 1 steps;
V
– DN F s∈sec fbp(s, n) f-predicts s in n + 1 steps and is minimal w.r.t. vf .
Moreover, the previous results can be extended to finite sets of states. Assume
Sec to be a set of states {sec1 , sec2 , ...., secm }, for some m. We need to characterize
all the context sequences that lead to some state in Sec.
Corollary 2. Let A = (S, A) be a r.s.. Let Sec be a set of states {sec1 , sec2 , ...., secm },
for some m,
W V
– seci ∈Sec s∈sec i
fbp(s, n) f-predicts
the set Sec in n + 1 steps;
W V
– DN F seci ∈Sec s∈seci fbp(s, n) f-predicts Sec in n + 1 steps and is mini-
mal w.r.t. vf .
Example 3. Let us consider again the reaction system A1 of Examples 1 and 2.
Assume we are interested in reaching the state {E, F } after 4 steps. In Example 2
we calculated the logic formula that f-predicts E in
4 steps applying
the function
fbp. This resulted in the formula G3 ∧ ¬B3 ∧ ¬A2 ∨ (C3 ∧ D3 ) . Analogously, we
can calculate the logic formula that f-predicts F in 4 steps applying the function
fbp. This resulted in the formula (C3 ∧ D3 ). Now, in order to obtain the minimal
formula characterising the context sequences that lead to the state where both E
and F are present, according to Corollary 1, we need to compute
DN F(fbp(E,
4) ∧ fbp(F, 4)) =
DN F (G3 ∧ ¬B3 ∧ ¬A2 ) ∨ (C3 ∧ D3 ) ∧ (C3 ∧ D3 ) = C3 ∧ D3 .
A context sequence satisfies C3 ∧ D3 iff the execution of the reaction system leads
to the production of both object E and F after 4 steps.
Assume now we are interested in characterising the context sequences that
either lead to state {E, F } or to state {B} after 4 steps. Hence, in this case
Sec = {{E, F }, {B}}.
According to Corollary 2 the minimal formula can be obtained by computing
DN F ((fbp(E, 4) ∧ fbp(F, 4)) ∨ fbp(B, 4)) =
DN F((C3 ∧ D3 ) ∨ A3 ) = (C3 ∧ D3 ) ∨ A3 .
Note that any sequence satisfying the formula (C3 ∧ D3 ) ∨ A3 leads to a state
in Sec. Moreover, such sequences are the only ones that can lead to the production
of a state in Sec.
5 Information flow
As in [3, 4], we now consider a reaction system A = (S, A) where we assume an ex-
ternal observer can only detect or see some kinds of objects in the context sequence.
To formally describe this situation, borrowing techniques developed for reasoning
about flow based security (see [5]), we divide objects from S into two groups, namely
public (low level) objects L and private (high level) objects H. It is assumed that
L ∪ H = S and L ∩ H = ∅. We assume that an observer can see only L-objects, i.e.
objects from L. Moreover, we introduce an equivalence on sets of objects and on
contexts sequences. Two sets of objects A, B are equivalent with respect to the set
M if they contain the same objects apart from those in M . Formally, A ≡M B iff
A\M = B \M . This can be applied to reaction system contexts: we write γ1 ≡M γ2
if γ1 = C01 , ....Cn1 , ... and γ2 = C02 , ....Cn2 , ... and ∀i, Ci1 ≡M Ci2 . To formalize infor-
mation flow between L-objects and H-objects we exploit a concept known as current
state opacity (see [15] for an overview paper).
5.1 Current State Opacity
Let us assume a set of states Sec with Sec ⊂ 2S . We assume an external observer of
the system who can detect or see only L objects in the context sequence, but who
wants to discover whether the current state Wi is a secret state belonging to Sec.
In this context a reaction system is i-current state opaque if whenever there exists
a context sequence leading to a secret state of Sec, there exists an equivalent (with
respect to the L object) context sequence that does not lead to a secret state in Sec.
This will assure us that just observing the context sequence an external observer
cannot decide whether the system will go to a secret state.
Definition 8. (i-Step Current State Opacity) The reaction system A = (S, A) is
i-current state opaque with respect to L and Sec iff whenever there exists an i-step
context sequence γ leading to a secret state in Sec, that is, Di+1 ∈ Sec, there also
exists an i-step context sequence γ 0 not leading to a state in Sec, that is, Di+1
0
6∈ Sec,
0
such that γ ≡L γ .
Note that differently from our previous work [3, 4], here the attacker observes
properties of context sequences to detect properties of the system states.
Since formula based predictors express all causal dependences of an object from
all the objects of the context sequences, we can use this concept to verify if a reaction
system is i-step current state opaque.
Theorem 2. A r.s. A is i-current state opaque with respect to L and Sec iff
W V
DN F sec∈Sec s∈sec fbp(s, i) = c1 ∨ c2 ∨ ... ∨ cn and
∀m ∈ {1, ..., n}, {A | Aj ∈ atom(cm ), with 0 ≤ j < i} ∩ (S \ L) 6= ∅.
Proof. We start by proving the right hand implication. Assume by contradiction
that the reaction system A is i-current state opaque with respect to L and Sec but
that there exists a cm such that {A | Aj ∈ atom(cm ), with 0 ≤ j < i} ∩ (S \ L) = ∅.
Choose a minimal context sequence γ such that γ |= cm . γ has to be minimal in
the sense that it just provides the positive literals in the conjunction cm . Note that
by hypothesis, γ provides only Wlow levelVL-objects. Note that γ |= cm implies that
γ |= c1 ∨ c2 ∨ ... ∨ cn = DN F sec∈Sec s∈sec fbp(s, i) . By applying Corollary 2
we have that the context sequence γ leads to the production of one state in Sec after
i steps. However, since γ contains just low level objects L, any context sequence
γ 0 such that γ 0 ≡L γ will satisfy cm , since cm contains only L-objects. Then, by
Corollary 2 any γ 0 will lead to the production of a state in Sec after i steps. Therefore
A is not i-current state opaque. This gives a contradiction.
For proving the left hand implication, assume, by contradiction that every ci
contain at least an H object but that the reaction system A is not i-current state
opaque with respect to a set of low level objects L and Sec. This implies that there
do not exist two context sequence γ and γ 0 with γ ≡L γ 0 such that one lead to a
secret state in Sec and the other does not.
Choose a γ leading to the production of a state in Sec such that it satisfy only
one particular conjunction ci in the disjunction c1 ∨ c2 ∨ ... ∨ cn . By Corollary 2 such
γ exists and we can choose γ as the minimal context sequence satisfying a ci . Since
by hypothesis ci is a conjunction containing at least one object in S \ L consider γ 0
as the context sequence satisfying the conjunction of low level objects in ci but that
does not satisfy the S \ L literals in ci . Now, by construction γ ≡L γ 0 . However,
γ 0 6|= ci . Moreover, since we have chosen γ to be the minimal context sequence
satisfying just ci and ci ∈ c1 ∨ c2 ∨ ... ∨ cn then it is simplified, we can be sure that
γ 0 6|= c1 ∨ c2 ∨ ... ∨ cn . Then, by Corollary 2, we have that the context sequence γ 0
does not lead to the production of a state in Sec. Hence, we found γ and γ 0 such
that γ ≡L γ 0 and context sequence γ leads to a secret state in Sec while context
sequence γ 0 does not. This gives a contradiction. t
u
This gives us an easy method to verify if a reaction system is i-current state opaque
with respect to a set of low level objects L and a secret set of states Sec. While
computing c1 ∨ c2 ∨ ... ∨ cn gives us a way to represent all different context sequences
that lead to the production of a secret state in Sec (see Corollary 2), the condition
that each conjunction in c1 ∨ c2 ∨ ... ∨ cn has to contain at least one non low level
object, gives us a way to automatically construct an L-equivalent context sequence
that does not lead to a state in Sec. We will illustrate this construction in the next
example. As a consequence of Theorem 2, we can state the following proposition.
Proposition 1. The property of a reaction system A to be i-current state opaque
with respect to a set of low level objects L and a secret set of states Sec is decidable.
Example 4. Let A2 = ({A, . . . , F }, {a1 , a2 , a3 , a4 }) be a reaction system with
a1 = ({A}, {B}, {C}) a2 = ({A}, {D}, {C})
a3 = ({D}, {}, {B}) a4 = ({F }, {}, {E})
and consider L = {A, B, E, F }, Sec = {{C, E}}. Note that A2 is 3-current state
opaque even if E is caused just by a low level object F . Roughly speaking, A2 is i-
current state opaque for each i ≥ 2 because in that case C is always caused by an H
level object. This can formally be proved by considering DN F(fbp(C, 3)∧fbp(E, 3))
DN F(fbp(C, 3) ∧ fbp(E, 3)) = DN F fbs (A ∧ ¬B) ∨ (A ∧ ¬D), 3 ∧ fbs(F, 3)
= DN F ((fbs(A, 3) ∧ ¬fbs(B, 3))
∨ (fbs(A, 3) ∧ ¬fbs(D, 3))) ∧ fbs(F, 3)
= DN F ((A3 ∧ ¬B3 ∧ D2 ) ∨ (A3 ∧ ¬D3 )) ∧ F3
= (A3 ∧ ¬B3 ∧ D2 ∧ F3 ) ∨ (A3 ∧ ¬D3 ∧ F3 )
Since both conjunctions A3 ∧ ¬B3 ∧ D2 ∧ F3 and A3 ∧ ¬D3 ∧ F3 contain at least
a high level object D then by Theorem 2 we are sure that A2 is 3-current state
opaque.
It is worth noting that using the formula based predictor for each γ leading to
the production of a secret state in Sec we can actually construct γ 0 with γ ≡L γ 0
such that γ 0 does not lead to a secret state in Sec. Indeed, let γ = C1 , C2 , C3
where C2 and C3 are such that D ∈ C2 , F, A ∈ C3 and B 6∈ C3 . Consider then
γ 0 = C1 , C2 \ {D}, C3 , by Corollary 2, we have that γ lead to a state in Sec while
γ 0 does not lead to the state in Sec.
The following example shows that the conditions for a system to be i-current
state opaque cannot be checked on isolation. Let A3 = ({A, . . . , D}, {a1 , a2 }) be
the following reaction system with rules
a1 = ({A}, {D}, {B}) a2 = ({A, D}, {}, {C})
and consider L = {A, B, C}, Sec = {{C}{B}}. Note that both rules depend on one
H-object D. However, the system is not i-current state opaque for any i ≥ 1. Let
us verify if a system is 3-current state opaque,
DN F(fbp(B, 3) ∨ fbp(C, 3)) = DN F fbs (A ∧ ¬D), 3 ∨ fbs (A ∧ D), 3
= DN F (fbs(A, 3) ∧ ¬fbs(D, 3)
∨ (fbs(A, 3) ∧ fbs(D, 3))
= DN F (A3 ∧ ¬D3 ) ∨ (A3 ∧ D3 ) = A3
In this case, the conjunction A3 does not satisfy the claim of Theorem 2 since
it does not have at least one hight level H-object. Indeed, consider any context
sequence γ = C1 , C2 , C3 where A ∈ C3 . Note that any context sequence γ 0 ≡L γ
will provide A at the third step. Then, by Corollary 2, any γ 0 ≡L γ will lead to the
state in Sec. Hence, A3 is not 3-state opaque.
5.2 n-p Window State Opacity
We now introduce a stronger notion of opacity. Assume now that an observer can
observe all objects in the context sequence except for a “blurry window” on which
it can observe just L-objects. Once again he wants to discover whether the state at
some given step belongs to the set of secret states Sec.
We first define the concept of observational window of a context sequence. Let
γ = C0 , ....Cn , ..., Cp , ..., Ci , by γn,p , for 0 ≤ n ≤ p we denote the subsequence
Cn , ..., Cp .
Definition 9. (n-p Window i-State Opacity) Let n and p such that 0 ≤ n ≤ p ≤ i.
Reaction system A = (S, A) is n-p window i-state opaque with respect to L and
Sec, iff whenever there exists a γ such that Di+1 belongs to Sec, i.e. Di+1 ∈ Sec,
there exists γ 0 such that state Di+1
0
does not belong to Sec i.e. Di0 +1 6∈ Sec and
0 0 0
γ0,n−1 ≡S γ0,n−1 , γn,p ≡L γn,p and γp+1,i ≡S γp+1,i .
Once again, formula based predictors can be used to verify if a reaction system
is n-p window i-state opaque.
Theorem 3. A reaction system A is n-p window i-state opaque with respect to L
and Sec iff for every
W V
DN F sec∈Sec s∈sec fbp(s, i) = c1 ∨ c2 ∨ ... ∨ cn and
∀m ∈ {1, ..., n}, {A | Aj ∈ atom(cm ), with n ≤ j ≤ p} ∩ (S \ L) 6= ∅.
As before, to verify if a reaction system is n-p window i-state opaque with respect to
a set of low level objects L and a secret set of states Sec, we can check c1 ∨c2 ∨...∨cn .
Proof. The proof is similar to the proof of Theorem 2, therefore it is only sketched.
For the right hand implication assume by contradiction that the reaction system
A is n-p window i-state opaque with respect to L and Sec but the second part of
the claim is false for at lest one cm . Choose a minimal (in the sense of the proof
of Theorem 2) context sequence γ such that γ |= cm . By hypothesis, γ does not
provide S \ L objects at any step included between n and p. Note that any context
sequence γ 0 such that γ0,n−1 ≡S γ0,n−10
, γn,p ≡L γn,p0
and γp+1,i ≡S γp+1,i 0
will
0
satisfy cm . Then, by Corollary 2 any γ will lead to the production of a state in Sec
after i steps. This gives a contradiction.
For proving the left hand implication, assume, by contradiction that every ci
contain at least one S \ L object at some step included between n and p but A
is not n-p window i-state opaque. This means that there do not exist two context
sequence γ and γ 0 with γ0,n−1 ≡S γ0,n−1 0 0
, γn,p ≡L γn,p and γp+1,i ≡S γp+1,i 0
such
that one lead to a secret state in Sec and the other does not.
Choose a γ = C0 , ..., Ci leading to the production of a state in Sec such that it
satisfies only one particular conjunction ci in the disjunction c1 ∨ c2 ∨ ... ∨ cn . By
Corollary 2 such γ exists. Consider γ 0 = C0 , ..., Cn−1 , Cn0 , ..., Cp0 , Cp+1 , ..., Ci as the
context sequence such that Cn0 , ..., Cp0 , satisfy the conjunction of low level objects
only included between n and p of ci but that does not satisfy the S \ L literals
0 0 0
of ci . Now, by construction γ0,n−1 ≡S γ0,n−1 , γn,p ≡L γn,p and γp+1,i ≡S γp+1,i .
0
However, γ 6|= ci . Following the reasoning of proof of Theorem 2, we can conclude
that we have found γ and γ 0 such that one leads to a secret state in Sec while the
other does not. This gives a contradiction. t
u
Therefore we can state the following.
Proposition 2. The property of a reaction system A to be n-p window i-state
opaque with respect to a set of low level objects L and a secret sets of state Sec
is decidable.
If a system is 0-i window i-state opaque then it is i-current state opaque.
Example 5. Consider again the reaction system A2 , L and Sec as in Example 4.
A2 was 3-current state opaque. However, A2 it is not 3-3 window i-state opaque.
Recall that
DN F(fbp(C, 3) ∧ fbp(E, 3)) = (A3 ∧ ¬B3 ∧ D2 ∧ F3 ) ∨ (A3 ∧ ¬D3 ∧ F3 ).
Then, {A | Aj ∈ atom((A3 ∧¬B3 ∧D2 ∧F3 )), with 3 ≤ j ≤ 3}∩(S\L) = ∅ and Theo-
rem 3 is not satisfied. Consider, for example, we can choose γ = {}, {}, {D}, {A, B, F },
then any γ 0 such that γ0,2 ≡S γ0,20 0
, γ3,3 ≡L γ3,3 must be γ 0 = {}, {}, {D}, C30 with
0 0
C3 ⊇ {A, B, F }, therefore also γ will lead to a secret state in Sec.
Finally, note that A2 is n-3 window i-state opaque for any 0 ≤ n ≤ 2.
6 Conclusions and further work
In this paper we have defined two state based security properties, that are, Current
State Opacity and n-p Window State Opacity for reaction systems. We proposed ef-
fectively computable methods for verifying such properties based on the new notion
of formula based predictor for set of secret states sets, newly defined in Section 4.
As further work we plan to elaborate other notions of opacity for reaction sys-
tems. The first one is in a sense a complement notion to n-p Window i-State Opacity.
We consider an observer who can see only a small “window” of computation. If af-
ter that computation a secret state has been reached we expect that there exists
seemingly the same window which leads to non-secret states. Also we plan to study
the notion Initial State Opacity. In this case an observer tries to learn properties of
an initial state of the computation. We believe that these concepts, borrowed by the
security theory, can be also studied in the context of reaction systems. Moreover, it
would be interesting to study variants of reaction systems with a limited threshold
assumption and with timed properties (for a process algebra example, see [16]).
References
1. A. Ehrenfeucht, G. Rozenberg, Reaction Systems, Fundam. Inform. 75 (1-4) (2007)
263–280.
2. R. Brijder, A. Ehrenfeucht, M. G. Main, G. Rozenberg, A Tour of reaction Systems,
Int. J. Found. Comput. Sci. 22 (7) (2011) 1499–1517.
3. D. Gruska, R. Gori, P. Milazzo, Studying opacity of reaction systems through formula
based predictors, in: Proc. of the 26th Int. Workshop on Concurrency, Specification
and Programming, CS&P, 2017.
4. D. Gruska, R. Gori, P. Milazzo, Studying opacity of reaction systems through formula
based predictors, Fundamenta Informaticae To appear.
5. J. A. Goguen, J. Meseguer, Security policies and security models, Proc. of IEEE Sym-
posium on Security and Privacy.
6. J. Bryans, M. Koutny, P. Ryan, Modelling non-deducibility using petri nets, in: 2nd
Workshop on Security Issues with Petri Nets and other Computational Models, 2004.
7. J. W. Bryans, M. Koutny, L. Mazaré, P. Y. Ryan, Opacity generalised to transition
systems, International Journal of Information Security 7 (6) (2008) 421–435.
8. R. Brijder, A. Ehrenfeucht, G. Rozenberg, A Note on Causalities in Reaction Systems,
ECEASST 30.
9. R. Barbuti, R. Gori, F. Levi, P. Milazzo, Investigating dynamic causalities in reaction
systems, Theoretical Computer Science 623 (2016) 114–145.
10. R. Barbuti, R. Gori, F. Levi, P. Milazzo, Specialized predictor for reaction systems with
context properties, in: Proc. of the 24th Int. Workshop on Concurrency, Specification
and Programming, CS&P 2015, 2015, pp. 31–43.
11. R. Barbuti, R. Gori, F. Levi, P. Milazzo, Specialized predictor for reaction systems
with context properties, Fundamenta Informaticae 147 (2-3) (2016) 173–191.
12. R. Barbuti, R. Gori, F. Levi, P. Milazzo, Generalized contexts for reaction systems:
definition and study of dynamic causalities, Acta Inf. 55 (3) (2018) 227–267.
13. R. Barbuti, R. Gori, P. Milazzo, Multiset patterns and their application to dynamic
causalities in membrane systems, in: Membrane Computing - 18th Int. Conference,
CMC 2017, 2017, pp. 54–73.
14. R. Barbuti, R. Gori, P. Milazzo, Predictors for flat membrane systems, Theor. Comput.
Sci. 736 (2018) 79–102.
15. R. Jacob, J. Lesage, J. Faure, Overview of discrete event systems opacity: Models,
validation, and quantification, Annual Reviews in Control 41 (2016) 135–146.
16. M. C. Ruiz, D. Cazorla, F. Cuartero, J. J. Pardo, H. Macia, A bounded true concur-
rency process algebra for performance evaluation, in: FORTE Workshops 2004, 2007,
pp. 143–155.