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 de ne 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 e ective method for verifying such properties. The veri cation method is based on a newly de ned extension of the concept of formula based predictor to set of states.
? Work supported by the grant VEGA 1/0778/18 and by the project \Metodologie informatiche avanzate per l'analisi di dati biomedici" (University of Pisa, PRA 2017 44).
In previous papers [
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 e ective methods for verifying them based on dynamic causalities.
Dynamic causalities deal with the ways entities dynamically in uence each other.
Brijder, Ehrenfeucht and Rozenberg initiated an investigation on causalities in
reaction systems [
In this section we brie y introduce reaction systems [
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), the result of the application of A to a set T S is de ned as resA(T ) = resA(T ) = Sa2A 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 objects, namely the objects which are supplied to the system by the external environment at each step. The dynamics is de ned as an interactive process = ( ; ), with and being nite 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
The aim of formula based predictors is to characterize all context sequences that lead to the production of a speci c 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 de ne the set FS of propositional formulas on S in the standard way: S [ ftrue; f alseg FS and :f1; f1 _ f2; f1 ^ f2 2 FS if f1; f2 2 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 de nition of the satisfaction relation is as follows.
De nition 1. Let C S for a set of objects S. Given a propositional formula f 2 FS , the satisfaction relation C j= f is inductively de ned as follows: C j= s i s 2 C; C j= :f 0 i C 6j= f 0; C j= f1 ^ f2 i C j= f1 and C j= f2:
C j= true;
C j= f1 _ f2 i either C j= f1 or C j= f2; In the following l stands for the logical equivalence on propositional formulas FS . Moreover, given a formula f 2 FS we use atom(f ) to denote the set of propositional symbols that appear in f . The simpli ed version of a formula is obtained by applying the standard formula simpli cation procedure of propositional logic converting a formula to Disjunctive Normal Form, DN F (f ). We recall that for any formula f 2 FS the simpli ed 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 de ned by a propositional formula on the set of objects S. First of all we de ne 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. De nition 2. Let a = (R; I; P ) be a reaction with R; I; P S for a set of objects S. The applicability predicate of a, denoted by ap(a), is de ned as follows: ap(a) = Vsr2R sr ^ Vsi2I :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.
De nition 3. Let gA = (S; A) be a r.s. and s 2 S. The causal predicate of s in A, denoted by cause(s; A) (or cause(s), when A is clear from the context), is de ned as follows3: cause(s; A) = Wf(R;I;P )2Ajs2P g ap ((R; I; P )) :
Example 1. Let A1 = (fA; : : : ; Gg; fa1; a2; a3g) be a reaction system with a1 = (fAg; fg; fBg) a2 = (fC; Dg; fg; fE; F g) a3 = (fGg; fBg; fEg) : 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
In the rst part of this section we introduce the notion of formula based predictor
as it was originally presented in [
A formula based predictor for an object s at step n + 1 is a propositional formula satis ed exactly by the context sequences leading to the production of s at step n+1. Minimal formula based predictors can be calculated in an e ective way.
Given a set of objects S, we consider a corresponding set of labelled objects S IN. For the sake of legibility, we denote (s; i) 2 S IN simply as si and we introduce Sn = Sin=0 Si where Si = fsi j s 2 Sg. Propositional formulas on labelled objects Sn describe properties of n-step context sequences. The set of propositional formulas on Sn, denoted by FSn , is de ned analogously to the set FS (presented in Sect. 3) by replacing S with Sn. Similarly, the set FSi can be de ned by replacing S with Si. Given a formula f 2 FS , a corresponding formula labelled(f; i) 2 FSi can be obtained by replacing each s 2 S in f with si 2 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 interpretation leads to the following de nition of satisfaction relation for propositional formulas on context sequences.
De nition 4. Let = C0; C1; : : : Cn be a n-step context sequence and f 2 FSn a propositional formula. The satisfaction relation j= f is de ned as fsi j s 2 Ci; 0 i ng j= f : As an example, let us consider the context sequence = C0; C1 where C0 = fA; Cg and C1 = fBg. We have that satis es the formula A0 ^ B1 (i.e. j= A0 ^ B1) while does not satisfy the formula A0 ^ (:B1 _ C1) (i.e. 6j= A0 ^ (:B1 _ C1)).
The latter notion of satisfaction allows us to de ne formula based predictor. De nition 5 (Formula based Predictor). Let A = (S; A) be a reaction system, s 2 S and f 2 FSn a propositional formula. We say that f f-predicts s in n + 1 steps if for any n-step context sequence = C0; : : : ; Cn
j= f , s 2 Dn+1 where = D0; : : : ; Dn is the result sequence corresponding to resA(Cn [ Dn). and Dn+1 = Note that if formula f f-predicts s in n + 1 steps and if f 0 l f then also f 0 fpredicts s in n + 1. More speci cally, we are interested in the formulas that f-predict s in n + 1 and contain the minimal numbers of propositional symbols, so that their satis ability can easily be veri ed. This is formalised by the following approximation order on FSn .
De nition 6 (Approximation Order). Given f1; f2 2 FSn we say that f1 vf f2 if and only if f1 l f2 and atom(f1) atom(f2).
In [
We now de ne an operator fbp that allows formula based predictors to be effectively computed.
De nition 7. Let A = (S; A) be a r.s. and s 2 S. We de ne a function fbp : S IN ! FSn as follows: fbp(s; n) = fbs(cause(s); n), where the auxiliary function fbs : FS IN ! FSn is recursively de ned as follows: fbs(s; 0) = s0 fbs((f 0); i) = (fbs(f 0; i)) fbs(:f 0; i) = :fbs(f 0; i) fbs(true; i) = true fbs(s; i) = si _ fbs(cause(s); i 1) if i > 0 fbs(f1 _ f2; i) = fbs(f1; i) _ fbs(f2; i) fbs(f1 ^ f2; i) = fbs(f1; i) ^ fbs(f2; i) fbs(f alse; i) = f alse The function fbp gives a formula based predictor that, in general, may not be minimal with respect to the approximation order vf . Therefore, the calculation of a minimal formula based predictor requires the application of the standard simpli cation procedure that simpli es 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 2 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 fpredicts 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 satis es fbp(E; 3) i 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 simpli ed 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 characterize 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, { Vs2sec fbp(s; n) f-predicts sec in n + 1 steps; { DN F Vs2sec 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 nite sets of states. Assume Sec to be a set of states fsec1; sec2; ::::; secmg, 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 fsec1; sec2; ::::; secmg, for some m, { Wseci2Sec { DN F Wseci2Sec mal w.r.t. vf .
Vs2seci fbp(s; n) f-predicts the set Sec in n + 1 steps;
Vs2seci fbp(s; n) f-predicts Sec in n + 1 steps and is miniExample 3. Let us consider again the reaction system A1 of Examples 1 and 2. Assume we are interested in reaching the state fE; F g 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 satis es C3 ^ D3 i 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 fE; F g or to state fBg after 4 steps. Hence, in this case Sec = ffE; F g; fBgg.
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
As in [
De nition 8. (i-Step Current State Opacity) The reaction system A = (S; A) is i-current state opaque with respect to L and Sec i whenever there exists an i-step context sequence leading to a secret state in Sec, that is, Di+1 2 Sec, there also exists an i-step context sequence 0 not leading to a state in Sec, that is, Di0+1 62 Sec, such that L 0.
Note that di erently from our previous work [
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 i
8m 2 f1; :::; ng; fA j Aj 2 atom(cm); with 0 = c1 _ c2 _ ::: _ cn and j < ig \ (S n 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 fA j Aj 2 atom(cm); with 0 j < ig \ (S n L) = ;. Choose a minimal context sequence such that j= 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 low level L-objects. Note that j= cm implies that j= c1 _ c2 _ ::: _ cn = DN F Wsec2Sec Vs2sec 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 n L consider 0 as the context sequence satisfying the conjunction of low level objects in ci but that does not satisfy the S n L literals in ci. Now, by construction L 0. However, 0 6j= ci. Moreover, since we have chosen to be the minimal context sequence satisfying just ci and ci 2 c1 _ c2 _ ::: _ cn then it is simpli ed, we can be sure that 0 6j= 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. tu 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 di erent 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 = (fA; : : : ; F g; fa1; a2; a3; a4g) be a reaction system with a1 = (fAg; fBg; fCg) a3 = (fDg; fg; fBg) a2 = (fAg; fDg; fCg) a4 = (fF g; fg; fEg) and consider L = fA; B; E; F g; Sec = ffC; Egg. Note that A2 is 3-current state opaque even if E is caused just by a low level object F . Roughly speaking, A2 is icurrent 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 2 C2, F; A 2 C3 and B 62 C3. Consider then 0 = C1; C2 n fDg; 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 = (fA; : : : ; Dg; fa1; a2g) be the following reaction system with rules a1 = (fAg; fDg; fBg) a2 = (fA; Dg; fg; fCg) and consider L = fA; B; Cg; Sec = ffCgfBgg. 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 2 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 rst de ne 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.
0;n 1 S 00;n 1, n;p
L n0;p and p+1;i S p0+1;i.
De nition 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, i whenever there exists a such that Di+1 belongs to Sec, i.e. Di+1 2 Sec, there exists 0 such that state Di0+1 does not belong to Sec i.e. Di0+1 62 Sec and
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 i for every
8m 2 f1; :::; ng; fA j Aj 2 atom(cm); with n = c1 _ c2 _ ::: _ cn and j pg \ (S n 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 j= cm. By hypothesis, does not provide S n L objects at any step included between n and p. Note that any context sequence 0 such that 0;n 1 S 00;n 1, n;p L n0;p and p+1;i S p0+1;i will satisfy cm. Then, by Corollary 2 any 0 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 n 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 00;n 1, n;p L n0;p and p+1;i S p0+1;i 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 satis es 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 n L literals of ci. Now, by construction 0;n 1 S 00;n 1, n;p L n0;p and p+1;i S p0+1;i. However, 0 6j= 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. tu
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, fA j Aj 2 atom((A3^:B3^D2^F3)); with 3 j 3g\(SnL) = ; and Theorem 3 is not satis ed. Consider, for example, we can choose = fg; fg; fDg; fA; B; F g, then any 0 such that 0;2 S 00;2, 3;3 L 30;3 must be 0 = fg; fg; fDg; C30 with C30 fA; B; F g, therefore also 0 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
In this paper we have de ned two state based security properties, that are, Current State Opacity and n-p Window State Opacity for reaction systems. We proposed effectively computable methods for verifying such properties based on the new notion of formula based predictor for set of secret states sets, newly de ned in Section 4.
As further work we plan to elaborate other notions of opacity for reaction
systems. The rst 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
after 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 [