Strong current-state and initial-state opacity of
discrete-event systems

A DES of interest is modeled as a nondeterministic finite-state automaton (NFA) $G=(X,\Sigma,\delta,X_{0})$, where $X$ is the finite set of states, $\Sigma$ is the finite set of events, $X_{0}\subseteq X$ is the set of initial states, $\delta:X\times\Sigma\rightarrow 2^{X}$ is the transition function, which depicts the system dynamics: given states $x,y\in X$ and an event $\sigma\in\Sigma$, $y\in\delta(x,\sigma)$ implies that there exists a transition labeled by $\sigma$ from $x$ to $y$. Note that for $x\in X$ and $\sigma\in\Sigma$, if there exists no $y\in X$ such that $y\in\delta(x,\sigma)$, then $\delta(x,\sigma)=\emptyset$. We can extend the transition function to $\delta:X\times\Sigma^{\ast}\rightarrow 2^{X}$ in the usual manner, where $\Sigma^{\ast}$ denotes the Kleene closure of $\Sigma$, consisting of all finite sequences composed of the events in $\Sigma$ (including the empty sequence $\epsilon$), see, e.g., [38] for more details on DESs. We use $\mathcal{L}(G,x)$ to denote the language generated by $G$ from state $x$, i.e., $\mathcal{L}(G,x)=\{s\in\Sigma^{\ast}:\delta(x,s)\neq\emptyset\}$. Therefore, the language generated by $G$ is $\mathcal{L}(G)=\cup_{x_{0}\in X_{0}}\mathcal{L}(G,x_{0})$. For a sequence $s\in\mathcal{L}(G)$, we denote its prefix closure by $Pr(s)$, i.e., $Pr(s)=\{w\in\mathcal{L}(G):(\exists w^{\prime}\in\Sigma^{\ast})[ww^{\prime}=s]\}$. Further, for a prefix $w\in Pr(s)$, we use the notation $s/w$ to denote the suffix of $s$ after its prefix $w$. We without loss of generality assume that $G$ is accessible, i.e., all its states are reachable from $X_{0}$.

As usual, we assume that the intruder can only see partially the system’s behavior. To this end, $\Sigma$ is partitioned into the set $\Sigma_{o}$ of observable events and the set $\Sigma_{uo}$ of unobservable events, i.e., $\Sigma_{o}\cup\Sigma_{uo}=\Sigma$ and $\Sigma_{o}\cap\Sigma_{uo}=\emptyset$. The natural projection $P:\Sigma^{\ast}\rightarrow\Sigma_{o}^{\ast}$ is defined recursively by ($i$) $P(\epsilon)=\epsilon$, ($ii$) $P(s\sigma)=P(s)\sigma,\mbox{ if }\sigma\in\Sigma_{o}$, ($iii$) $P(s\sigma)=P(s),\mbox{ if }\sigma\in\Sigma_{uo}$, where $s\in\Sigma^{\ast}$. We extend the natural projection $P$ to $\mathcal{L}(G)$ by $P(\mathcal{L}(G))=\{P(s)\in\Sigma_{o}^{\ast}:s\in\mathcal{L}(G)\}$. We denote the inverse projection by a mapping $P^{-1}:\Sigma_{o}^{\ast}\rightarrow 2^{\Sigma^{\ast}}$, i.e., for any $\alpha\in\Sigma_{o}^{\ast}$, we have $P^{-1}(\alpha)=\{s\in\Sigma^{\ast}:P(s)=\alpha\}$.

To study opacity of $G=(X,\Sigma,\delta,X_{0})$, we assume that $G$ has a set of secret states, denoted by $X_{S}\subset X$. We use $X_{NS}$ to denote the set of non-secret initial states. Let $s=s_{1}s_{2}\ldots s_{n}\in\Sigma^{\ast}$ and $x_{0}\in X_{0},x_{i}\in X$, $i=1,2,\ldots,n$. If $x_{k+1}\in\delta(x_{k},s_{k+1})$, $0\leq k\leq n-1$, we call $x_{0}\stackrel{{\scriptstyle s_{1}}}{{\rightarrow}}x_{1}\stackrel{{\scriptstyle s_{2}}}{{\rightarrow}}x_{2}\stackrel{{\scriptstyle s_{3}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle s_{n}}}{{\rightarrow}}x_{n}$ a run generated by $G$ from $x_{0}$ to $x_{n}$ under $s$. We write $x_{0}\stackrel{{\scriptstyle s}}{{\rightarrow}}x_{n}$ (resp., $x_{0}\stackrel{{\scriptstyle s}}{{\rightarrow}}$) when $x_{1},x_{2},\ldots,x_{n-1}$ (resp., $x_{1},x_{2},\ldots,x_{n}$) are not specified. Note that there may be more than one run under a sequence $s\in\mathcal{L}(G,x_{0})$ based on nondeterminism of $G$. In other words, $x_{0}\stackrel{{\scriptstyle s}}{{\rightarrow}}x_{n}$ may denote some runs. $x_{0}\stackrel{{\scriptstyle s_{1}}}{{\rightarrow}}x_{1}\stackrel{{\scriptstyle s_{2}}}{{\rightarrow}}x_{2}\stackrel{{\scriptstyle s_{3}}}{{\rightarrow}}\cdots\stackrel{{\scriptstyle s_{n}}}{{\rightarrow}}x_{n}$ is called a non-secret run if $x_{i}\in X\backslash X_{S}$, $i=0,1,2,\cdots,n$.

In this subsection, we first recall the formal definitions of standard CSO and ISO in [6] and [7, 11], respectively. And then, we discuss their limitations for characterizing information security.

Note that, in [6] the notion of standard CSO was defined for deterministic finite-state automata. Obviously, this property can be readily extended to the nondeterministic setting as in Definition 2.1.

The phenomena in Examples 2.1 and 2.2 indicate that the standard versions of CSO and ISO have some limitations to some extent for characterizing high-level information security of a system. In order to overcome the aforementioned limitations, in this paper we propose two strong versions of opacity, called strong current-state opacity (SCSO) and strong initial-state opacity (SISO). Note that these two stronger notions of opacity provide high-level confidentiality.

Note that if $G$ is a deterministic finite-state automaton, SCSO in Definition 3.1 can be rephrased as follows: $G$ is said to be SCSO (w.r.t. $\Sigma_{o}$ and $X_{S}$) if

Now we give a physical interpretation of Definition 3.1. The notion of SCSO captures that if a sequence $s\in\mathcal{L}(G)$ is generated and a secret state is reached, then there exists a sequence $t\in\mathcal{L}(G)$ that has the same projection as $s$ and its execution generates a run that never passes through a secret state. SCSO has a higher-level confidentiality than standard CSO. In other words, SCSO implies standard CSO, but the converse implication does not hold. For instance, the system $G$ in Example 2.1 is standard CSO, but not SCSO since after observing the sequence $aa$ an intruder certainly concludes that $G$ has passed secret state $x_{4}$ or $x_{5}$. This results in the following proposition for SCSO and CSO whose straightforward proof is omitted.

In the following Subsection 3.2, we study the verification of SCSO based on a novel verification approach, which has time complexity $O(|X|^{4}|\Sigma_{o}||\Sigma_{uo}||\Sigma|2^{|X|})$.

In this subsection, we focus on the verification of SCSO in Definition 3.1. In order to obtain the main result, we need to introduce three notions of non-secret subautomaton, observer and concurrent composition for a given system.

Given a system $G=(X,\Sigma,\delta,X_{0})$ and a set $X_{S}\subset X$ of secret states, we construct a non-secret subautomaton by deleting all its secret states from $G$, which is denoted by $G_{dss}$, where “$dss$” stands for the acronym of “deleting secret states”. Note that when we delete a secret state $x_{s}\in X_{S}$, all transitions attached to $x_{s}$ are also deleted. Formally,

where

• •

  $X_{dss}=\{x\in X\backslash X_{S}:\mbox{ there is a non-secret run }x_{0}\stackrel{{\scriptstyle s}}{{\rightarrow}}x\mbox{ for some }x_{0}\in X_{NS}\mbox{ and }s\in\Sigma^{\ast}\}$ stands for the set of states;

• •

  $\Sigma_{dss}=\{\sigma\in\Sigma:\exists x,x^{\prime}\in X_{dss}\mbox{ s.t. }x^{\prime}\in\delta(x,\sigma)\}$ stands for the set of events;

• •

  $\delta_{dss}:X_{dss}\times\Sigma_{dss}\rightarrow 2^{X_{dss}}$ stands for the transition function, i.e., for all $x,x^{\prime}\in X_{dss}\mbox{ and }\sigma\in\Sigma_{dss},x^{\prime}\in\delta_{dss}(x,\sigma)\mbox{ if }x^{\prime}\in\delta(x,\sigma)$;

• •

  $X_{dss,0}=X_{NS}$ stands for the set of initial states.

Next, we recall the observer of $G_{dss}$ that is defined by

where $X^{obs}_{dss}\subseteq 2^{X_{dss}}\backslash\emptyset$ stands for the set of states; $\Sigma^{obs}_{dss}$ stands for the observable event set $\Sigma_{dss,o}$ of $\Sigma_{dss}$; $\delta^{obs}_{dss}:X^{obs}_{dss}\times\Sigma^{obs}_{dss}\rightarrow X^{obs}_{dss}$ stands for the (partial) deterministic transition function defined as follows: for any $q\in X^{obs}_{dss}$ and $\sigma\in\Sigma^{obs}_{dss}$, we have $\delta^{obs}_{dss}(q,\sigma)=\{x^{\prime}\in X_{dss}:\exists x\in q,\exists w\in\Sigma_{dss,uo}^{\ast}\mbox{ s.t. }x^{\prime}\in\delta_{dss}(x,\sigma w)\}$ if it is nonempty, where $\Sigma_{dss,uo}=\Sigma_{dss}\backslash\Sigma_{dss,o}$; $X^{obs}_{dss,0}=\{x\in X_{dss}:\exists x_{0}\in X_{dss,0},\exists w\in\Sigma_{dss,uo}^{\ast}\mbox{ s.t. }x\in\delta_{dss}(x_{0},w)\}$ stands for the (unique) initial state. For brevity, we only consider the accessible part of observer $Obs(G_{dss})$.

Note that the widely-used observer $Obs(G_{dss})$ is an important information structure that can track all possible states of $G_{dss}$ consistent with the current observation. Specifically, $Obs(G_{dss})$ captures the observable behavior of $G_{dss}$, that is, $\mathcal{L}(Obs(G_{dss}))=P(\mathcal{L}(G_{dss}))$. The time complexity of computing observer $Obs(G_{dss})$ for $G_{dss}$ is $O(|X|^{2}|\Sigma_{o}||\Sigma_{uo}|2^{|X|})$. We refer the reader to [38, 39] for more details on the notion of observer.

Now we are ready to introduce a novel information structure called the concurrent composition of system $G$ and observer $Obs(G_{dss})$, which will be used to verify SCSO in Definition 3.1.

For a sequence $e\in\mathcal{L}(Cc(G,Obs(G_{dss})))$, we utilize the notations $e(L)$ and $e(R)$ to denote its left and right components, respectively. A similar notation is employed to the language $\mathcal{L}(Cc(G,Obs(G_{dss})))$. Further, we use $P(e)$ to denote $P(e(L))$ or $P(e(R))$ since $P(e(L))=P(e(R))$ for any $e\in\mathcal{L}(Cc(G,Obs(G_{dss})))$, which depends on the context. Intuitively, $Cc(G,Obs(G_{dss}))$ characterizes the following two properties: (i) $\mathcal{L}(Cc(G,$ $Obs(G_{dss})))(L)=\mathcal{L}(G)$; and (ii) it tracks a sequence $s\in\mathcal{L}(G)$ from $X_{0}$ and an observation $\alpha\in\mathcal{L}(Obs(G_{dss}))$ from $X^{obs}_{dss,0}$ (if exists) such that $P(s)=\alpha$.

In order to present the first main result of this paper, we classify the states whose first components belong to $X_{S}$ in $Cc(G,Obs(G_{dss}))$ defined in (5) into two types:

• •

  leaking secret states: $(x,q)\in X_{cc}$ with $x\in X_{S}\wedge q=\emptyset$;

• •

  non-leaking secret states: $(x,q)\in X_{cc}$ with $x\in X_{S}\wedge q\neq\emptyset$;

The leaking and non-leaking secret states are interpreted physically as follows. If $(x,q)\in X_{cc}$ is a leaking secret state, then, by Definition 3.2, in $G$ there exists $x_{0}\in X_{0}$ and $s\in\mathcal{L}(G,x_{0})$ such that $x\in\delta(x_{0},s)$, and there exists no observation $\alpha\in\mathcal{L}(Obs(G_{dss}))$ such that $P(s)=\alpha$. This means that an intruder certainly concludes that $G$ has reached/passed through at least one secret state by observing $P(s)$. If $(x,q)\in X_{cc}$ is a non-leaking secret state, then there exist $x_{0},x^{\prime}_{0}\in X_{0}$, $s\in\mathcal{L}(G,x_{0})$, and $t\in\mathcal{L}(G,x^{\prime}_{0})$ such that: (i) $x\in\delta(x_{0},s)$; (ii) $s$ and $t$ have the same projection, i.e., $P(s)=P(t)$; (iii) there exists a non-secret run $x^{\prime}_{0}\stackrel{{\scriptstyle t}}{{\rightarrow}}x^{\prime}$ generated by $G$ from $x^{\prime}_{0}$ to $x^{\prime}$ under $t$.

Based on the above preparation, now we are ready to introduce the main result on verification of SCSO for a system. It reveals that a system is SCSO if and only if its concurrent-composition structure does not contain any leaking secret state.

$(\Leftarrow)$ Also by contrapositive, assume that $G$ is not SCSO w.r.t. $\Sigma_{o}$ and $X_{S}$. By Definition 3.1, there exists a run $x_{0}\stackrel{{\scriptstyle s}}{{\rightarrow}}x_{s}$, where $x_{0}\in X_{0}$ and $x_{s}\in X_{S}$, and there exist no $x^{\prime}_{0}\in X_{NS}$ and $t\in\mathcal{L}(G,x^{\prime}_{0})$ such that $P(t)=P(s)$ and $G$ generates a non-secret run starting from $x^{\prime}_{0}$ under $t$. The former means $x_{s}\in\delta(x_{0},s)$. By the construction of $G_{dss}$, the latter means $\delta_{dss}(x^{\prime\prime}_{0},t)=\emptyset$ for all $x^{\prime\prime}_{0}\in X_{NS}$ and for all $t\in\mathcal{L}(G,x^{\prime\prime}_{0})$ with $P(t)=P(s)$. This further means that $\delta^{obs}_{dss}(X_{dss,0}^{obs},P(t))$ is not well-defined. By the construction of $Cc(G,Obs(G_{dss}))$, we conclude that there is $e\in\mathcal{L}(Cc(G,Obs(G_{dss})))$ with $e(L)=s$ and $e(R)=P(t)$ such that $(x_{s},\emptyset)\in\delta_{cc}((x_{0},X^{obs}_{dss,0}),e)$. Therefore, $(x_{s},\emptyset)$ a leaking secret state in $Cc(G,Obs(G_{dss}))$.       

We end this section by analyzing the time complexity of using Theorem 3.1 to verify SCSO. Since $G$ has the complexity of $O(|X|^{2}|\Sigma|)$ and computing $Obs(G_{dss})$ costs time $O(|X|^{2}|\Sigma_{o}||\Sigma_{uo}|2^{|X|})$, the time complexity of constructing $Cc(G,Obs(G_{dss}))$ is $O(|X|^{4}|\Sigma_{o}||\Sigma_{uo}||\Sigma|2^{|X|})$. Consequently, the (worst-case) time complexity of using Theorem 3.1 to verify SCSO is $O(|X|^{4}|\Sigma_{o}||\Sigma_{uo}||\Sigma|2^{|X|})$.

Intuitively, SISO in Definition 4.1 captures that for each sequence $s\in\mathcal{L}(G)$ starting from any $x_{0}\in X_{0}\cap X_{S}$, there exists a sequence $t\in\mathcal{L}(G)$ starting from some $x^{\prime}_{0}\in X_{NS}$ such that $P(t)=P(s)$ and $G$ generates a non-secret run starting from $x^{\prime}_{0}$ under $t$. Note that, SISO, compared with standard ISO in Definition 2.2, has a higher-level confidentiality obviously. In other words, SISO implies standard ISO, but the converse is not true. Taking the system $G$ shown in Fig. 2 for example, by Definitions 2.2 and 4.1, we conclude readily that $G$ is standard ISO, but not SISO.

Next, we illustrate these two strong versions of opacity in Definitions 3.1 and 4.1 are incomparable. In other words, SCSO does not imply SISO, and vice versa. For instance, by Definitions 3.1 and 4.1, the system $G$ depicted in Fig. 2 is SCSO, but not SISO. On the other hand, let us consider the system $G$ shown in Fig. 8. We know that $G$ is SISO, but not SCSO.

Inspired by the verification of SCSO in Section 3, we, in this subsection, use a minor variant of the concurrent composition approach to verify SISO of a system.

Consider a system $G=(X,\Sigma,\delta,X_{0})$ in which the set of secret states is denoted by $X_{S}\subset X$. $G_{dss}$ stands for the non-secret subautomaton obtained by deleting all secret states in $G$, which is defined in Eq. (4). $Obs(G_{dss})$ defined in Eq. (5) stands for the observer of $G_{dss}$. To check SISO in Definition 4.1, we construct an initial-secret subautomaton from $G$, denoted by $\hat{G}$, as follows:

where

• •

  $\hat{X}=\{x\in X:\exists x_{0}\in{X_{0}}\cap{X_{S}},\exists s\in\Sigma^{\ast}\mbox{ s.t. }x\in\delta(x_{0},s)\}$ stands for the set of states;

• •

  $\hat{\Sigma}=\{\sigma\in\Sigma:\exists x,x^{\prime}\in\hat{X}\mbox{ s.t. }x^{\prime}\in\delta(x,\sigma)\}$ stands for the set of events;

• •

  $\hat{\delta}:\hat{X}\times\hat{\Sigma}\rightarrow 2^{\hat{X}}$ stands for the transition function, i.e., for all $x,x^{\prime}\in\hat{X}$ and $\sigma\in\hat{\Sigma}$, $x^{\prime}\in\hat{\delta}(x,\sigma)$ if $x^{\prime}\in\delta(x,\sigma)$;

• •

  $\hat{X}_{0}={X_{0}}\cap{X_{S}}$ stands for the set of secret initial states.