Opacity-enforcing for Process Algebras ? Damas P. Gruska1 and M. Carmen Ruiz2 1 Comenius University, Slovakia 2 Universidad de Castilla-La Mancha, Spain Abstract. Supervisory control as a way how to guarantee security of processes is discussed and studied. We work with a security property called processes opacity and we investigate how it can be enforced. Su- pervisors can restrict behaviour of the original systems by enabling or disabling some actions to guarantee its security. We study maximal su- pervisors as the least restricting supervisory control processes. Moreover, we study also enhanced supervisory control which can add idling between system’s action to prevent timing attacks. Keywords: security, opacity, process algebras, information flow, super- visory control 1 Introduction The great revolution brought about by the internet of things involves the emer- gence of new devices, new protocols and, of course, new security needs to fulfill the new requirements. New protocols come into operation before they have been evaluated in depth. This leads to the appearance of new versions of the pro- tocol that is not always compatible with its predecessors and that companies will not always incorporate in their devices with sufficient speed. In addition, these solutions usually require downloading a new code and this itself is open to security attacks. This lack of security has been detected even in our own works. For example in [Gar16] we present an architecture for Wireless Sensor and Ac- tuator Networks (WSAN) using the Bluetooth Low Energy (BLE) and TCP/IP protocols in conjunction, which make necessary to include bridges that lack ba- sic security requirements. Another example can be found in [Hor17] where we propose a new packet format and a new BLE mesh topology, with two different configurations: Individual Mesh and Collaborative Mesh. All these represent our motivation to study applicability of formal models and formal methods to define and enforce system’s security. As regards formalism, we will work with timed process algebra. Then we exploit information flow based security properties (see [GM82]) which assume an absence of any information flow 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 ac- tivities or states can be deduced. This approach has found many reformulations and among them opacity (see [BKR04,BKMR06]) could be considered as the ? Work supported by the grant VEGA 1/0778/18. most general one and many other security properties could be viewed as its spe- cial cases (see, for example, [Gru15,Gru12,Gru11,Gru10,Gru08,Gru07]). Opacity properties could be divided into two types: language based opacity, expressing security (privacy) of system’s actions or traces of actions and state based one, concentrating on system’s states (see an overview paper [JLF16]). The former one is much more studied for process algebra’s formalism. But also for the later one there is some research already done. In [Gru15] we consider an intruder who wants to discover whether a process reaches a confident state. Resulting security property is called process opacity. It turned out that in this way some new security flaws could be expressed. If a process is not secure with respect to process opacity we can either re-design its behavior, what might be costly, difficult or even impossible, in the case that it is already part of a hardware solution, proprietary firmware and so on or we can use supervisory control (see [RW89]) to restrict system’s behaviour in such a way that the system becomes secure. A supervisor can see (some) system’s actions and can control (disable or enable) some set of system’s action. In this way it restricts system’s behaviour to guarantee its security. This is a trade-off between security and functionality. But in many cases it is not a fatal problem. Suppose that a communication protocol can reach (with a low probability) a state which is not secure. In that case the transmission of a packet is interrupted and it should start from the begging. Sometimes this restriction has even smaller impact on system’s behavior. Sup- pose that the system can perform action a and b in an arbitrary order but only a sequence b.a could leak some classified information about intermediate states. Restricting this sequence make system secure but could not have influence on overall system’s functionality. In this paper we do not assume any relation among a set of actions visible for an intruder, a set of actions visible for a controller and a set of controllable actions, i.e. sets EI , ES , EC , respectively, similarly to [TLSG18]. Note that in [DDM10] it is assumed that EI ⊆ ES (or ES ⊆ EI ) and EC ⊆ ES . In [YL10] EI ⊆ ES is assumed and in [TLSG16] EC ⊆ ES is assumed. As regards the related work, besides already mentioned works there is a large body of work on controller synthesis in temporal model checking. From the rest we mention just two papers. In [RS01] the idea of controller to enforce secure information flow is discussed for language based security in process al- gebra setting. Opacity-enforcing (called strategic noninterference) was proposed and investigated for transition systems in [JT15]. Timing attacks, as side channel attacks, represent serious threat for many systems. They allow intruders “break” “unbreakable” systems, algorithms, pro- tocols, etc. Even relatively recently discovered possible attacks on most of cur- rently used processors (Meltdown and Spectre) also belong to timing attacks. To protect systems against some type of timing attacks we propose to enhance ca- pabilities of the supervisory control. Such controller can add some idling between actions to enforce process’s security. 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 supervisory control. The next section contains some basic definition on informa- tion flow security and process opacity. Sections 5 and 6 deals with supervisory and enhanced supervisory control for process opacity, respectively. 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 specification). 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, S u, v, . . . range over Act, and x, y . . . range over Actt. Assume the signature Σ = 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. Rela- beling 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 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 x x x P → P 0 instead of (P, x, P 0 ) ∈ → and P → 6 if there is no P 0 such that P → P 0 . x The meaning of the expression P → P is that the term P can evolve to P 0 by 0 x performing action x, by P → we will denote that there exists a term P 0 such x 0 that P → P . 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. per- forming 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 s denote the set of all successors of P i.e. Succ(P ) = {P 0 |P → P 0 , s ∈ Actt∗ }. If the set Succ(P ) is finite we say that P is a finite state process. We define x modified transitions ⇒M which ”hide” actions from M . Formally, we will write x s1 x s2 s P ⇒M P 0 for M ⊆ Actt iff P → →→ P 0 for s1 , s2 ∈ M ? and P ⇒M instead of x1 x2 xn x x P ⇒M ⇒M . . . ⇒M . We will write P ⇒M if there exists P 0 such that P ⇒M P 0 . x  x We will write P ⇒M P 0 instead of P ⇒M P 0 if x ∈ M . Note that ⇒M is b defined for arbitrary action x but in definitions of security properties we will use it for actions (or sequence of actions) not belonging to M . We can extend s the definition of ⇒M for sequences of actions similarly to →. Let s ∈ Actt? . By |s| we will denote the length of s i.e. a number of action contained in s. By s|B we will denote the sequence obtained from s by removing all actions not belonging to B. For example, |s|{t} | denote a number of occurrences of t in s, i.e. time length of s. By Sort(P ) we will denote the set of actions from A which can be performed by P . The set of traces of process P is defined as s L(P ) = {s ∈ Actt? |∃P 0 .P ⇒ P 0 }. The set of weak timed traces of process P is s defined as Lw (P ) = {s ∈ (A∪{t})? |∃P 0 .P ⇒{τ } P 0 }. Two processes P and Q are weakly timed trace equivalent (P 'w Q) iff Lw (P ) = Lw (Q). We conclude this section with definitions of M-bisimulation and weak timed trace equivalence. Definition 1. Let (TPA, Actt, →) be a labelled transition system (LTS). A re- lation < ⊆ TPA × TPA is called a M-bisimulation if it is symmetric and it x satisfies the following condition: if (P, Q) ∈ < and P → P 0 , x ∈ Actt then there x exists a process Q0 such that Q ⇒M Q0 and (P 0 , Q0 ) ∈ <. Two processes P, Q b are M-bisimilar, abbreviated P ≈M Q, if there exists a M-bisimulation relating P and Q. 3 Supervisory control In this section we introduce some basic concepts of supervisory control the- ory. For more details see [RW89]. Let us assume deterministic finite automaton (DFA) G = (X, E, δ, x0 ), where X is the finite set of states, E is the set of events, δ : X × E → X is the (partial) transition function, x0 ∈ X is the initial state. The transition function can be naturally extended to strings of events. The generated language of G = (X, E, δ, x0 ) is defined as L(G) = {s, s ∈ E ∗ such that δ(x0 , s) is defined}. The goal of supervisory control is to design a control agent (called supervisor) that restricts the behavior of the system within a specification language K ⊆ L(G). The supervisor observes a set of observable events ES ⊆ E and is able to control a set of controllable events EC ⊆ E. The supervisor enables or disables controllable events. When an event is enabled (resp., disabled) by the supervisor, all transitions labeled by the event are allowed to occur (resp., prevented from occurring). After the supervisor observes a string generated by the system it tells the system the set of events that are enabled next to ensure that the system will not violate the specification. A supervisor can be represented by Sup = (Y, ES , δs , y0 , Ψ ), where (Y, ES , δs , y0 ) is an automaton and Ψ : Y → {E 0 ⊆ E|EU C ⊆ E 0 } where EU C = E \ EC specifies the set of events enabled by the supervisor in each state. System G under the control of a suitable supervisor Sup is denoted as Sup/G, and it satisfies L(Sup/G) ⊆ K. Definition 2 (Controllability). Given a DF AG, a set of controllable events EC , and a language K ⊆ L(G), K is said to be controllable (wrt L(G) and EC ) if K̄EU C ∩ L(G) ⊂ K̄ where K̄ is the prefix closer of K. The controllability of K requires that for any prefix s, s ∈ K, if s followed by an uncontrollable event e ∈ EU C is in L(G), then it must also be a prefix of a string in K. Definition 3 (Observability). Given a DF AG, a set of controllable events EC , a set of observable events ES , and a language K ⊆ L(G), K is said to be observable (wrt L(G), ES and EC ) if for all s, s0 ∈ K̄ and all e ∈ EC such that se ∈ L(G), s =S s0 (s =S s0 is means that strings are equal with respect to the set ES ), s.e ∈ K̄. Observability requires that supervisors observation of the system (i.e., the projection of s on ES ) provides sufficient information to decide after the occur- rence of a controllable event whether the resultant string is still in K̄ . Proposition 1. Let K ⊆ L(G) be a prefix-closed nonempty language, EC the set of controllable events and ES the set of observable events. There exists a supervisor Sup such that L(Sup/G) = K if and only if K is controllable and observable. 4 Information flow In this section we will present our working security concept. First we define the absence-of-information-flow property - 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. 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. Namely, 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 (namely, replaced by action τ ) for an observer. To express this hiding we introduce the hiding op- a a erator P/M, M ⊆ A, for which it holds that if P → P 0 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. 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 but a more general concept of observations and predicates are 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. Now let us assume a different scenario, namely that an intruder is not interested in traces and their properties but he or she tries to discover whether a given process always reaches a state with some given property which is expressed by a (total) predicate. This property might be process deadlock, capability to execute only traces with time length less then n time unites, capability to perform at the same time actions form a given set, incapacity to idle (to perform t action ) etc. 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 4. We say that the predicate φ over processes is consistent with respect to relation ∼ = if whenever P ∼ = P 0 then φ(P ) ⇔ φ(P 0 ). As the consistency relation ∼ = we could take bisimulation (≈∅ ), weak bisimu- lation (≈{τ } ) 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 equiv- ∼ ∼ alence relation = i.e. φ∼Q ∼ = (P ) holds iff 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 such s observations we exploit the relation ⇒M where actions from M are those ones which could not be seen by the observer. The formal definition of process opacity (see [Gru15]) is the following. Definition 5 (Process Opacity). Given process P , a predicate φ over pro- s cesses 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 OpM ⇔ P 0 ∈ P OpM whenever φ is consistent = and ∼ with respect to ∼ = is such that it is a subset of the trace equivalence (defined s s as 'w but instead of ⇒{τ } we use ⇒∅ ). s P =⇒M φ(P 0 ) s P =⇒M ¬φ(P 00 ) Fig. 1. Process opacity 5 Supervisory Control of Process Opacity In this section we will concentrate on enforcing process opacity, namely, how to guarantee that there is no leakage of information on validity of φ in a current state, i.e. security with respect to process opacity. Let M ⊆ Actt by M̄ we will denote the complement of M i.e. M̄ = Actt \ M . Let s ∈ Actt∗ , by sM̄ we denote the string obtained form s by removing all elements belonging to M . Formally, M̄ = , s.xM̄ = s.x iff x 6∈ M and s.xM̄ = s iff x ∈ M . We can extend this definition to a set of strings. Let T ⊆ Actt∗ then TM̄ = {sM̄ |s ∈ T }. Now let as suppose that process P is not secure with respect to process opacity P OpφM i.e. P 6∈ P OpφM . That means that there exists s ∈ L(P )M̄ such s s that P ⇒M P 0 and φ(P 0 ) holds then there does not exist P 00 such that P ⇒M 00 00 P and ¬φ(P ) holds. Hence, by observing s, an intruder knows that a state satisfying φ has been reached. For security reasons we want to prohibit such computations what will be the role for the supervisory control. Formally, let s K, K ⊆ L(P )M̄ is a set of safe observations, i.e. for every s ∈ K, P ⇒M P 0 and s φ(P ) does not hold or if it holds then there exists P such that P ⇒M P 00 and 0 00 ¬φ(P 00 ) holds. Clearly, if P ∈ P OpφM then K = L(P )M̄ , otherwise K ⊂ L(P )M̄ but K 6= L(P )M̄ . The aim of the control is to design a supervisor Sup which will restrict behaviour of the original process P in such a way that for the resulting process Sup/P we have L(Sup/P ) ⊆ K. Note that we do not assume any relations among set of actions visible for an intruder, a set of actions visible for a controller and a set of controllable actions, i.e. sets EI (EI = M̄ ), ES , EC , respectively, similarly to [TLSG18]. Note that in [DDM10] it is assumed that EI ⊆ ES (or ES ⊆ EI ) and EC ⊆ ES . In [YL10] EI ⊆ ES is assumed and in [TLSG16] EC ⊆ ES is assumed. Example 1. Let P = c.(a.b.N il+b.(a.N il+d.N il)), M = {c, d} and predicate φ is d defined as follows: φ(Q) holds iff Q →. Then it is easy to check that P 6∈ P OpφM . The execution of c.b (visible as b) at the beginning leads to the state satisfying φ but no execution visible as b can lead to a state not satisfying φ. Now we will model supervisory control by means a special process Sup. Pro- cess Sup runs in parallel with P , communicates with environment via actions Sort(P ) and internally with P by actions renamed by function f which maps every action a from Sort(P ) to a new ”ghost” action a0 (see Fig. 2). The formal definition of process supervisor is the following. f   - P Sup - P Fig. 2. Supervisory Control Definition 6 (Process Supervisor). Given process P , a process Sup is called supervisor if Lw (Sup/P ) ⊆ Lw (P ) where Sup/P = (P [f ]|Sup) \ f (Sort(P )) where f : Sort(P ) → Sort(P )0 where Sort(P )0 = {x0 |x ∈ Sort(P ), x 6= τ }. We will use a process supervisor to restrict behaviour of the original process in such a way that the resulting process becomes secure with respect to process opacity. Definition 7 (Process Supervisor for Process Opacity). Given process P , process Sup is called supervisor for opacity property P OpφM iff P 6∈ P OpφM but Sup/P ∈ P OpφM . By Sup(P, P OpφM ) we will denote the set of all supervisors for opacity property P OpφM for a given process P . Example 2. Let us continue with the Example 1. Let Sup1 = c0 .c.N il Sup2 = c0 .c.a0 .aN il and Sup3 = c0 .c.a0 .a.b0 .b.N il then it is easy to check that all processes Supi are process supervisors for P and opacity property P OpφM . Actually these process supervisors restrict the execution of action b immediately after c. Clearly, Sup(P, P OpφM ) 6= ∅ since N il ∈ Sup(P, P OpφM ). Note that supervi- sor N il restricts all behaviour of P which consequently becomes trivially secure. We can formulate some properties of the set Sup(P, P OpφM ). Proposition 2. Let Sup1 , Sup2 ∈ Sup(P, P OpφM ). Then Sup1 + Sup2 ∈ Sup(P, P OpφM ). Proof. The main idea. The first actions which is performed by (Sup1 + Sup2 )/P is performed either by Sup1 or by Sup2 . Proposition 3. Let Sup1 ∈ Sup(P, P OpφM ) and Sup1 ≈∅ Sup2 . Then Sup2 ∈ Sup(P, P OpφM ). Proof. Sketch. The proof follows from the the fact that trace equivalence is con- gruence i.e. for Sup1 ≈∅ Sup2 we have (P [f ]|Sup1 )\f (Sort(P )) ≈∅ (P [f ]|Sup1 )\ f (Sort(P )) and so L((P [f ]|Sup1 ) \ f (Sort(P ))) = L((P [f ]|Sup2 ) \ f (Sort(P ))) i.e.L(Sup1 /P ) = L(Sup2 /P ). To guarantee a minimal restriction of process behaviour our aim is to find a maximal process supervisor in a sense that it minimally restricts behavior of the original process. The formal definition is the following. Definition 8 (Maximal Process Supervisor for Process Opacity). Pro- cess Sup ∈ Sup(P, P OpφM ) is called maximal process supervisor for process opac- ity P OpφM iff for every Sup0 ∈ Sup(P, P OpφM ) L(Sup0 /P ) ⊆ L(Sup/P ). Example 3. Let us continue with the Examples 1 and 2. It is easy to check that process Sup3 is a maximal process supervisor for P and opacity property P OpφM . Processes Sup1 and Sup2 are not maximal process supervisors for P and opacity property P OpφM . Unfortunately it is undecidable to verify whether a process Sup is a process supervisors for P and opacity property P OpφM as it is stated by the following proposition. Proposition 4. The property that Sup is a process supervisor for process opac- ity for process P is undecidable in general. Proof. The proof is based on an idea that already process opacity is undecidable (see Proposition 2. in [Gru15]). Suppose that the property is decidable. Let Sup = µX. x∈Actt x0 .x.X i.e Sup does not restrict anything. We have that Sup P is a process supervisor for process opacity for process P iff P ∈ P OpφM . Hence we would be able to decide process opacity what contradicts its undecidability. Corollary. The property that Sup is a maximal process supervisor for process opacity for process P is undecidable in general. To obtain a decidable variant of the previous property we put some restric- tion on process predicates. First we model predicates by special processes called tests. For now we assume that action τ is not visible for√an intruder, i.e. τ ∈ M . The tests communicate with processes and produce action if correspond- ing predicates hold for the processes. In the subsequent proposition we show how to exploit this idea to express process opacity by means of appropriate M-bisimulation. Definition 9. We say that the √ process Tφ√is the test representing predicate φ if φ(P ) holds iff (P |Tφ )\At ≈t .N il where is a new action indicating a passing of the test. If Tφ is the finite state process we say that φ is the finitely definable predicate. Suppose that both φ and ¬φ are the finitely definable predicates. Then we can reduce checking whether Sup is a process supervisor for process opacity to checking bisimulation (see Proposition 4. in [Gru15]). Since we can reduce the problem of decidability to finite automata (see [TLSG18]) we obtain the following result. Proposition 5. Let φ and ¬φ are finitely definable predicates. The property that Sup is a process supervisor for process opacity for finite state process P is decidable. Moreover, we can always find a maximal supervisor for process opacity. 6 Enhanced Supervisory Control Time attacks belong to powerful tools for attackers who can observe or interfere with systems in real time. By the presented formalism we can distinguish timing attacks. Suppose that P 6∈ P OpφM but P ∈ P OpφM ∪{t} . This means that an attack is possible only for an observer who can see elapsing of time, i.e. there is a possibility of timing attacks. To prevent them, we can use process supervisor which restricts process behaviour with respect to actions from A or we introduce a new type of process supervisor, called enhanced process supervisor which can add some idling between actions to ensure that the resulting process becomes secure with respect to timing attacks. In this case the restriction with respect to atomic actions from A could be smaller as in the case of original supervisory control. Definition 10 (Enhanced Process Supervisor). Given process P , a process s ESup is called enhanced supervisor if whenever s ∈ Lw (P ) then ESup/P ⇒t,τ where ESup/P = (P [f ]|ESup) \ f (Sort(P )) where f : Sort(P ) → Sort(P )0 where Sort(P )0 = {x0 |x ∈ Sort(P ), x 6= τ }. Definition 11 (Enhanced Process Supervisor for Process Opacity). Given process P , P ∈ P OpφM ∪{t} , a process ESup is called enhanced supervisor for opacity property P OpφM iff P 6∈ P OpφM , but ESup/P ∈ P OpφM . By ESup(P, P OpφM ) we will denote the set of all supervisors for opacity property EP OpφM for a given process P . Now we can formulate a condition which guarantees existence of an enhanced supervisory control. Proposition 6. Let P 6∈ P OpφM and there exists P 0 , P ≈τ,t P 0 such that P 0 ∈ P OpφM . Then there exists nontrivial (not equivalent to N il with respect to ≈τ ) enhanced supervisory control for P . Proof. The main idea. According to the assumption processes P and P 0 behave essentially in the same way but the later performs more idling between actions from Act. The enhanced supervisory control adds this idling to behaviour of P in such a way that the resulting process is process opaque. Moreover, the previous proposition has the following consequence which guar- anties that the maximal enhanced supervisory control does not restrict action from A. Corollary. Let P ∈ P OpφM ∪{t} and P 6∈ P OpφM . For the maximal enhanced supervisory control for P we have L(ESup/P )Ā = KĀ . 7 Conclusions We have presented the new concepts called supervisory and enhanced super- visory controller for process algebra which enforce the security property called process opacity. Particularly, we have investigated finite state systems and time sensitive observations. A supervisor can see (some) system’s actions and can control (disable or enable) some set of system’s action. In this way it restricts system’s behaviour to guarantee its security. Sometimes either we simply cannot redesign original insecure system which could have, for example, hardware im- plementation or some small restriction of system’s behaviour is not essential for overall system functionality. In the case of enhanced supervisory controller it can only add some idling between actions which would have no influence on system non-timing properties. The presented approach allows us to exploit also process algebras enriched by operators expressing other ”parameters” (space, distribu- tion, networking architecture, processor or power consumption and so on). In this way also other types of attacks, which exploit information flow through various covert channels, can be described and enforced. Hence we could obtain security properties which have not only theoretical but also practical value, since many protocols, particularly low level protocols for IoT, could be described by means of some process algebra formalism. 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. [DDM10] Dubreil J., P. Darondeau and H. Marchand: Supervisory control for opacity. IEEE Trans Autom Control 55(5), 2010. [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. [Gar16] Garrido C., V. Lopez, T. Olivares and M. C. Ruiz: Architecture Proposal for Heterogeneous, BLE-Based Sensor and Actuator Networks for Easy Man- agement of Smart Homes. 15th ACMIEEE International Conference on In- formation Processing in Sensor Networks (IPSN), 2016. [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. [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. [Gru12] Gruska D.P.: Informational analysis of security and integrity. Fundamenta Informaticae, vol. 120, Numbers 3-4, 2012. [Gru11] Gruska D.P.: Gained and Excluded Private Actions by Process Observa- tions. Fundamenta Informaticae, Vol. 109, No. 3, 2011. [Gru10] Gruska D.P.: Process Algebra Contexts and Security Properties. Funda- menta Informaticae, vol. 102, Number 1, 2010. [Gru08] Gruska D.P.: Probabilistic Information Flow Security. Fundamenta Infor- maticae, vol. 85, Numbers 1-4, 2008. [Gru07] Gruska D.P.: Observation Based System Security. Fundamenta Informati- cae, vol. 79, Numbers 3-4, 2007. [Hor17] Hortelano, D., T Olivares, M.C. Ruiz, M. Carmen, C. Garrido-Hidalgo and V. López: From Sensor Networks to Internet of Things. Bluetooth Low Energy, a Standard for This Evolution. Sensors, vol 17, 2017. [JLF16] Jacob, R., J.-J.Lesage and J.-M. Faure: Overview of discrete event systems opacity: Models, validation, and quantification, Annual Reviews in Control Volume 41, 2016. [JT15] Jamroga W. and M. Tabatabaei: Strategic Noninterference. ICT Systems Security and Privacy Protection, SEC 2015. [RW89] Ramadge P.J.G, Wonham W.M.: The control of discrete event systems. Proc IEEE 77(1):8198, 1989. [RS01] Ryan P. Y. A. and S. A. Schneider: Process Algebra and Non-Interference. Journal of Computer Security 9(1/2), 2001. [TLSG18] Tong, Y, Z. Li, Zhiwu, C. Seatzu and A. Giua: Current-state opacity en- forcement in discrete event systems under incomparable observations. Dis- crete Event Dynamic Systems, vol. 28, 2018. [TLSG16] Tong, Y, Z. Li, Zhiwu, C. Seatzu and A. Giua: Supervisory enforcement of current-state opacity with uncomparable observations. In: Proceedings of the 13th International workshop on discrete event systems, 2016. [YL10] Yin X. and S. Lafortune: A new approach for synthesizing opacity-enforcing supervisors for partially-observed discrete-event systems. In: Proceedings of the 2015 American control conference. IEEE, Chicago, 2015.