Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions

1

Verification of K - and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions

arXiv:2609.01192v1 [cs.FL] 1 Sep 2026

Jiahui Zhang, Kuize Zhang, Senior Member, IEEE, Xiaoguang Han, Member, IEEE, and Zhiwu Li, Fellow, IEEE

Abstract— Anonymity is an information flow property that provides privacy protection in the sense of nonuniqueness of system information at certain moments with respect to observations. The notion of K -step anonymity in the context of discrete-event systems characterizes the scenario that the state estimates cannot be a singleton within at most K observational steps prior to the current instant, while infinite-step anonymity is the same as K -step anonymity without considering the limit on K. In this paper, we lucubrate K - and infinite-step anonymity for partially-observed discrete-event systems modeled by non-deterministic finite-state automata. First, we define two strong types and two weak types of K - and infinitestep anonymity that are fundamentally different from the existing notions of K - and infinite-step anonymity due to the consideration of strong and weak anonymous projections. Then, we develop a new methodology by exploiting the concurrent-composition technique to verify these four types of anonymity. Based on the constructed concurrent compositions, verifiable necessary and sufficient conditions for the four types of anonymity are provided, along with their complexity analysis. Finally, the upper bounds on K for K -step strong anonymity and weak anonymity are computed. Index Terms— Discrete-event system, security, privacy, K -step anonymity, infinite-step anonymity, concurrent composition.

I. I NTRODUCTION ECURITY and privacy of cyber-physical systems (CPSs) have increasingly received attention. As an information flow property, anonymity characterizes the non-uniqueness of the intruder’s estimate of a system’s state. Anonymity can be used in a wide range of practical scenarios such as anonymous voting, donations, and transactions [1]. In recent decades, much work has been done on anonymity analysis and verification, see, e.g., [2]–[5]. In [2], the authors introduce a system called the Crowds to guarantee the

S

This work is partially supported by the National Natural Science Foundation of China under Grand No. 61903274 and the Science and Technology Fund, FDCT, Macau SAR under Grant No. 0029/2023/RIA1. (Corresponding author: Xiaoguang Han.) Jiahui Zhang and Zhiwu Li are with the Institute of Systems Engineering, Macau University of Science and Technology, Taipa 999078, China (e-mail: 3220006067@student.must.edu.mo; zwli@must.edu.mo). Kuize Zhang is with School of Mathematics and Statistics, Xi’an Jiaotong University, Xi’an 710049, China (e-mail: kuize.zhang@unica.it). Xiaoguang Han is with the College of Electronic Information and Automation, Tianjin University of Science and Technology, Tianjin 300457, China (e-mail: xiaoguanghan@tust.edu.cn).

anonymity of users on the internet. For anonymous Web browsing of the Crowds system, a probabilistic model checker is proposed [3]. The authors in [4] touch upon anonymity and reputation with a focus on anonymous remailers and anonymous publishing, and explain why systems can benefit from reputation. The work in [5] introduces the notions of strong and weak O-anonymity in labeled transition systems to capture different concealment requirements depending on the different observational capabilities of intruders. In recent years, anonymity has been extensively studied in discrete-event systems (DESs). Specifically, the concepts of strong and weak anonymity are proposed in [6] for describing the ability to hide an action among a set of actions, which are quite different from those in [5]. The notions of anonymity defined in [5] and [6] are incomparable. To capture the inability of intruders to determine the accurate current state of a system, current-state anonymity is studied in finite-state automata [7]. Naturally, the notions of K-step anonymity and infinite-step anonymity are investigated, which generalizes the current instant to the last K and arbitrary instants compared with the current-state anonymity [8]. As a stronger version of K-anonymity [9] in the computer science area, a notion of infinite-step Kanonymity is defined in [10]. The underlying observation mechanism is the key to analyzing observational properties of DESs, e.g., anonymity [5]–[10], opacity [11]–[15], detectability [16]–[19], and diagnosability [20]–[23]. To characterize different capabilities for observing a system, the work in [5] first systematically summarizes three types of observation functions: static observation functions, dynamic observation functions [24], and Orwellian-type observation functions [25]. In this paper, we formulate two types of observation functions: strong and weak anonymous projections to define interesting and useful types of anonymity. Specifically, the strong anonymous projection is a static observation function that describes the scenarios in which an intruder’s observation of some specific actions performed by different agents is the same, preventing the intruder from determining the identity of the agents. In contrast, the weak anonymous projection is a dynamic observation function that characterizes the scenarios in which an intruder is able to recognize certain actions performed only by the same agent without knowing the agent’s identity. In this case, the observation of any action depends on its prefix that has happened. Recently, a unified concurrent-composition method has been developed for the verification problem of state/event inference

2

and concealment for DESs modeled by finite-state automata [26]. In addition, standard and strong current-state opacity, initial-state opacity, K-step opacity, and infinite-step opacity can be verified by using a combination of concurrent composition and the classical observer [26]–[28]. The concurrentcomposition technique shows its efficiency in verifying these properties in DESs compared with the existing methods. Inspired by the above work, this paper mainly focuses on the verification of K- and infinite-step anonymity under strong and weak anonymous projections by exploiting the concurrentcomposition technique. Specifically, the main contributions of this research are as follows. • To characterize different inabilities of an intruder to infer whether a system of interest is in an exact state at some certain instants, we formulate four notions of K- and infinite-step anonymity under strong and weak anonymous projections that are essentially different from the existing notions of K- and infinite-step anonymity [8], [10]. • A general methodology for verifying these four types of anonymity is developed by constructing two different information structures Cc(Gm , Obsm (G)) (see Eq. (5)) b w , Obsw (G)) b (see Eq. (9)), both of which are and Cc(G concurrent compositions of a particular automaton and a particular observer, where Cc(Gm , Obsm (G)) (resp., b w , Obsw (G))) b Cc(G is used to verify K- and infinitestep anonymity under the strong (resp., weak) anonymous projection. • Based on the constructed concurrent compositions, verifiable necessary and sufficient conditions are provided to verify these four types of anonymity separately. In addition, we provide an algorithm for computing upper bounds on K for K-step strong anonymity and weak anonymity. Finally, an anonymous questioning process in chemical engineering is shown as a case study to illustrate the proposed notions of anonymity. Structure. The remainder of this paper is structured as follows. The preliminaries used throughout this paper are presented in Section II. Section III formulates four definitions of K- and infinite-step anonymity under strong and weak anonymous projections. Section IV develops a methodology for verifying the proposed four types of anonymity by exploiting the concurrent composition technique. We explore the maximal value of K and calculate the upper bounds on K in Section V regarding the two types of K-step anonymity separately. Section VI provides a case study on an anonymous questioning process. Finally, we conclude this paper in Section VII. II. P RELIMINARIES A. Notation In this paper, let N be the set of non-negative integers. We denote by P , Pstr , and Pw the natural projection, the strong anonymous projection, and the weak anonymous projection, respectively. The set of events is symbolized by Σ. Notation Σ∗ stands for the set of all finite strings over Σ, including the empty string ϵ. Given a string s = σ1 σ2 . . . σn , we

use |s| to denote its length, i.e., |s| = n and |ϵ| = 0. Notation Γ is used to represent the set of anonymous events. Let γ be the unique observation of all anonymous events through the strong anonymous projection Pstr . We denote by Γw = {γ1 , γ2 , . . . , γ|Γ| } the set of distinct observation labels of anonymous events in all strings generated by a system under the weak anonymous projection Pw , where |Γ| is the number of the anonymous events in Γ. Given a state set Q, 2Q and U R(Q) signify the power set of Q and the unobservable reach bG (Pstr , α|αβ) (resp., of Q, respectively. We use notation E b EG (Pw , α|αβ)) to represent the delayed state estimate of system G under the strong (resp., weak) anonymous projection Pstr (resp., Pw ) at the instant that α has just been observed upon observing αβ. In addition, the concurrent composition of automata G1 and G2 is written as Cc(G1 , G2 ). B. System model A non-deterministic finite-state automaton (NFA) is a quadruple G = (X, Σ, δ, X0 ), (1) where • X is a finite set of states, • Σ is a finite set of events, X • δ : X × Σ → 2 is the transition function, which characterizes the dynamics of G: y ∈ δ(x, σ) denotes that there exists a transition labeled by event σ reaching state y from state x, and • X0 ⊆ X is a set of initial states. The transition function can be extended to δ : X × Σ∗ → 2X in the usual manner. L(G, x) is used to denote the language generated by G from the state x, i.e., L(G, x) = {s ∈ Σ∗ |δ(x, s) ̸= ∅}. The set L(G) = {s ∈ Σ∗ |∃x0 ∈ X0 : δ(x0 , s) ̸= ∅} denotes the language generated by G. Note that G is called a deterministic finite-state automaton (DFA) if |X0 | = 1 and |δ(x, σ)| ≤ 1 for all x ∈ X and all σ ∈ Σ. In general, a system modeled by G is partially observable. The event set Σ is divided into two disjoint subsets Σo and ˙ uo , where Σo is the set of observable Σuo , i.e., Σ = Σo ∪Σ events and Σuo is the set of unobservable events. The natural projection P : Σ∗ → Σ∗o is recursively defined by P (ϵ) = ϵ and ( P (s)σ, if σ ∈ Σo , P (sσ) = P (s), otherwise. where s ∈ Σ∗ and σ ∈ Σ. Accordingly, the projection of language generated by G, denoted by P (L(G)), is P (L(G)) = {P (s) | s ∈ L(G)}. We refer the reader to [29] for details. Since system G is partially observed, an intruder needs to estimate the state reached by G based on an observed string, which involves state estimation problems. The following type of state estimate is called the delayed state estimate under the natural projection P [29]. Definition 1: (Delayed state estimate) Let αβ be an observation string generated by a system G = (X, Σ, δ, X0 ) under the natural projection P , i.e., αβ ∈ P (L(G)). The delayed state estimate under the natural projection P for the instant of

3

α upon the fact that αβ is exactly observed is the set of states (at which the system could be in) |β| steps ahead, i.e.,   [∃x0 ∈ X0 , ∃s ∈ L(G, x0 ) :   bG (P, α|αβ) = x ∈ X P (s) = α ∧ x ∈ δ(x0 , s)]∧ . E   [∃t ∈ L(G, x) : P (st) = αβ] ♢ By definition, the delayed state estimate is the collection of possible states that system G may visit prior to some steps bG (P, α|αβ) is of the current observation. The cardinality of E b denoted as |EG (P, α|αβ)|, indicating the number of the states bG (P, α|αβ). In addition, we define the unobservable reach in E of a state subset Q ⊆ X as U R(Q) = {q ′ ∈ X|∃q ∈ Q, ∃s ∈ Σ∗uo : q ′ ∈ δ(q, s)}. III. F OUR TYPES OF K- AND INFINITE - STEP ANONYMITY UNDER THE STRONG / WEAK ANONYMOUS PROJECTION A. K- and infinite-step strong anonymity In this paper, we assume that an action (modeled by an event σ ∈ Σ) is observed (or detected) by an intruder if a sensor is deployed [30]. On the other hand, if no sensor is deployed, an intruder will never observe or detect the occurrence of any action. An action that can (resp., cannot) be observed by an intruder is called an observable (resp., unobservable) event. As mentioned in [1], the persons who perform actions, such as anonymous voting, donations, and transactions, are called agents. In situations where anonymous operations are required, e.g., the aforementioned anonymous transactions, some agents may want to hide their identities. In this paper, an action that can be observed by an intruder and taken by an agent who wants to conceal his/her identity is modeled as an anonymous event. We set a subset of observable events, denoted by Γ ⊆ Σo , as the anonymous event set. When an agent performs the action that is modeled as an anonymous event, he/she does not want to be distinguished from other agents who perform actions in some sense. We assume |Γ| ≥ 2 to make it meaningful to conceal at least two agents’ identities. Suppose that anonymous processors are deployed on the sensors related to the actions modeled by anonymous events, which can help agents hide their identities. In this case, an intruder’s observations of these actions, modeled by different anonymous events and performed by different agents, are identical and indistinguishable. We use a new symbol γ ∈ /Σ to denote the identical observation obtained by the intruder. On this basis, an ideal anonymous processor is modeled as the strong anonymous projection as follows. Definition 2: An ideal anonymous processor, i.e., a processor whose processing results for all anonymous events are the same, and whose processing result for a non-anonymous observable event is still the event itself, is modeled as the strong anonymous projection Pstr : Σ∗ → (Σo ∪ {γ})∗ (a static observation function) defined by Pstr (ϵ) = ϵ and   Pstr (s)γ, if σ ∈ Γ, Pstr (sσ) = Pstr (s)σ, if σ ∈ Σo \Γ,   Pstr (s), otherwise. where s ∈ Σ∗ and σ ∈ Σ.

♢

By definition, an intruder can observe the results after processing different types of events by the ideal anonymous processor (strong anonymous projection) as follows. For an anonymous event, its observation is γ. For an observable event that is not an anonymous event, its observation is itself, since there is no anonymous processor deployed on the sensor related to this event. Obviously, the intruder observes nothing once an unobservable event occurs since the sensors associated with this event are not deployed. bG (P, α|αβ) By changing the natural projection P in E b to the strong anonymous projection Pstr , EG (Pstr , α|αβ) is obtained, representing the delayed state estimate under the strong anonymous projection Pstr at the instant that α has just been exposed upon observing αβ. Next, we use the notations introduced above to describe the scenario that an ideal anonymous processor is employed, i.e., an intruder cannot distinguish between any two anonymous events. In this situation, the observations processed by the ideal anonymous processor are obtained by the intruder. The intruder is expected not be able to determine for sure whether the system is in only one state K observational steps before the current time instant. As a result, the notion of K-step strong anonymity is formulated. Definition 3: (K-step strong anonymity) Given a system G = (X, Σ, δ, X0 ), a non-negative integer K ∈ N, and the strong anonymous projection Pstr w.r.t. a set of anonymous events Γ and a set of observable events Σo with Γ ⊆ Σo , G is said to be K-step strongly anonymous w.r.t. Σo , Γ, and Pstr if for all st ∈ L(G) with Pstr (s) = α, Pstr (st) = αβ, and |β| ≤ K, it holds bG (Pstr , α|αβ)| > 1. |E ♢ In plain words, K-step strong anonymity means that at any instant, an intruder cannot infer which state a system is exactly in at most K observational steps before the current instant. When a system satisfies K-step strong anonymity for any K, we say that the system satisfies infinite-step strong anonymity, as defined below. Definition 4: (Infinite-step strong anonymity) Given a system G = (X, Σ, δ, X0 ) and the strong anonymous projection Pstr w.r.t. a set of anonymous events Γ and a set of observable events Σo with Γ ⊆ Σo , G is said to be infinite-step strongly anonymous w.r.t. Σo , Γ, and Pstr if for all st ∈ L(G) with Pstr (s) = α and Pstr (st) = αβ, it holds bG (Pstr , α|αβ)| > 1. |E ♢ Intuitively, infinite-step strong anonymity requires that after observing αβ, the cardinality of the set of state estimates of system G after α has just been observed inferred by an intruder are greater than 1, so that the intruder cannot determine which state system G is exactly in at any instant. Example 1: Consider the system G shown in Fig. 1 and assume K = 1. To verify whether the system satisfies 1-step strong anonymity, we need to check whether the cardinality bG (Pstr , α|αβ) is greater than of the delayed state estimate E 1 for all αβ ∈ Pstr (L(G)) with |β| = 0 and |β| = 1. When |β| = 0, taking the strings whose strong anonymous projections are γ and γc for example respectively, one has bG (Pstr , γ|γ) = {2, 3} and E bG (Pstr , γc|γc) = {4, 5, 6}. E

state

}

}

6}

4

It means that the number of states in the 0 delayed state estimates is greater than 1 when an intruder observes γ and bG (Pstr , ϵ|γ) = {0, 1} and γc. When |β| = 1, one has E b EG (Pstr , γ|γc) = {2, 3}. The number of possible states the system G could be in 1 observational step ago is greater than 1 when observing γ and γc. Moreover, one finds that bG (Pstr , α|αβ)| > 1 holds for all αβ ∈ Pstr (L(G)) with |E |β| ≤ 1. By Definition 3, the system G is 1-step strongly anonymous w.r.t. Σo , Γ, and Pstr . bG (Pstr , α|αβ)| > 1 always holds Further, we find that |E regardless of the value of K, suggesting that the system G also satisfies infinite-step strong anonymity. It means that an intruder cannot accurately infer whether the system G is in a singleton state at any instant. □

strong 0

2

4

1

3

5

6

Fig. 1. System G with Σo = {a, b, c} and Γ = {a, b}.

{0,1}

{2,3}

{4,5,6}

B. K- and infinite-step weak anonymity Ideally, as stated in Definition 2, anonymous processors process different anonymous events performed by different agents with a fixed observational result γ. However, anonymous processors may become less adjoint powerful (i.e., non-ideal) state state set sometimes. The non-ideal anonymous processor produces the {1} same result for specific 0actions only performed by the same agent. In other words, an1 intruder only knows when the same {0} agent performs the specific actions without knowing which 2 {3} agent. Some notations are introduced before formulating the non3 {2} ideal anonymous processor. Let Γw = {γ1 , γ2 , . . . , γ|Γ| } be a 4 labels of the anonymous {5,6} set of distinct observation events of all strings s ∈ L(G) under the weak anonymous projection. In 5 {4,6} other words, set Γw represents all possible labels for the first 6 {4,5,6} in string s. We appearance of the anonymous events contained assume Γw is disjoint with Σo , i.e., Γw ∩Σo = ∅ to distinguish anonymous events with the other observable events. With a slight abuse of notation, write σ ∈ s to denote that an event σ ∈ Σ appears in string s ∈ Σ∗ . The set of anonymous events appearing in string s is denoted by EΓ (s) = Γ ∩ E(s), where E(s) = {σ ∈ Σ|σ ∈ s}. For any string s = µσv ∈ Σ∗ with σ ∈ Γ, µ ∈ (Σ\{σ})∗ , and v ∈ Σ∗ , let R(s, σ) = |EΓ (µ)| + 1 be the location index of the first occurrence of event σ ∈ Γ in string s. A non-ideal anonymous processor is formally characterized by the weak anonymous projection as follows. Definition 5: A non-ideal anonymous processor, i.e., a processor whose processing result for an anonymous event in a string depends on the order of its first appearance in this string, and whose processing result for an observable event that is not anonymous event is still the event itself, is modeled as the weak anonymous projection Pw : Σ∗ → (Σo ∪ Γw )∗ (a

dynamic observation function) formulated by Pw (ϵ) = ϵ and   Pw (s)γR(sσ,σ) , if σ ∈ Γ, Pw (sσ) = Pw (s)σ, if σ ∈ Σo \Γ,   Pw (s), otherwise. where s ∈ Σ∗ and σ ∈ Σ. ♢ In plain words, for Pw , the observation of an anonymous event depends on the order of its first appearance in a string, but for Pstr , the observation of an anonymous event has nothing to do with the order of its first appearance. As shown in Table I, to demonstrate the difference between Pstr and Pw more intuitively, we list string s ∈ L(G), Pstr (s), and Pw (s) in the first, second, and third columns, respectively, where system G is shown in 0 Fig. 1. From Table 2 4 I, one 6 sees that the strong anonymous projection of event a/b is always fixed γ due to its static property. However, the weak anonymous 1 characterization. 3 5 For example, the projection has a dynamic weak anonymous projection of the anonymous event a in string ab is γ1 , while in ba is γ2 . The reason is that the order in which event a first appears in string ab (resp., ba) is 1 (resp., 2) if we only focus on the order in which anonymous events first appear in string ab (resp., ba).{2,3} Additionally, we finds that {1} {4,5,6} the strong anonymous projection of strings ab and bb (resp., strings abc and bbc) are the same but their weak anonymous {0} {2} {4,6} projections are different. The technical details of calculating the weak anonymous projection for a string s ∈ L(G) are presented in Example {3} 2. {5} {5,6} TABLE I I LLUSTRATIVE EXAMPLE

string s ∈ L(G) a/b ab/ba bb (1,{0}) abc bbc abbc (2,{2}) · · ·

(0,{1})

Pstr (s)

γ (2,{2,3}) γγ γγ (3,{2})γγc γγc γγγc (4,{4,6}) ···

Pw (s) γ1 (4,{4,5,6}) γ1 γ2 γ1 γ1 (5,{4,6}) γ1 γ2 c γ1 γ1 c γ1 γ2 γ2 c (6,{4,6}) ···

(6,{4,5,6})

Example 2: Consider again the system G(6,{5}) in Fig. 1 with Γ = (2,{3}) (4,{5}) {a, b}. For string s = b, one has E(s) = {b}, EΓ (ϵ) = Γ ∩ E(ϵ) = ∅, and R(b, b) = |EΓ (ϵ)|+1 = 1. Then, one concludes (4,{5,6}) (6,{5,6}) Pw (b) = γR(b,b) = γ1 due to b ∈ Γ. For string t = ba, E(t) = {a, b}, EΓ (s) = EΓ (b) = {b}, and R(ba, a) = |EΓ (b)|+1 = 2 can be obtained. The weak anonymous projection of string ba is Pw (ba) = Pw (b)γR(ba,a) = γ1 γ2 . Similarly, for string s′ = a, Pw (s′ ) = γR(a,a) = γ1 is derived owing to a ∈ Γ and R(a, a) = |EΓ (ϵ)| + 1 = 1. The weak anonymous projection of string t′ = ab is Pw (ab) = Pw (s′ )γR(ab,b) = γ1 γ2 due to b ∈ Γ and R(ab, b) = |EΓ (a)| + 1 = 2. As shown above, we have Pw (ab) = Pw (ba) = γ1 γ2 , which shows that Pw fundamentally differs from Pstr , due to Pstr (ab) = Pstr (ba) = γγ. □ bG (P, α|αβ) By changing the natural projection P in E bG (Pw , α|αβ) is to the weak anonymous projection Pw , E obtained, representing the delayed state estimate under the

5

weak anonymous projection Pw . Consider the scenario that the processing capability of the anonymous processor is nonideal. It means that an intruder can only partially distinguish between anonymous events to a limited extent weakly. In this case, the intruder obtains observations processed by a nonideal anonymous processor. We still expect that the intruder’s estimate of the system state over the past K observational steps is not a singleton state. With the previously defined notations in mind, K-step weak anonymity is formally defined for a system G as follows. Definition 6: (K-step weak anonymity) Given a system G = (X, Σ, δ, X0 ), a non-negative integer K ∈ N, and the weak anonymous projection Pw w.r.t. a set of anonymous events Γ and a set of observable events Σo with Γ ⊆ Σo , G is said to be K-step weakly anonymous w.r.t. Σo , Γ, and Pw if for all st ∈ L(G) with Pw (s) = α, Pw (st) = αβ, and |β| ≤ K, it holds bG (Pw , α|αβ)| > 1. |E ♢ By definition, K-step weak anonymity under weak anonymous projection Pω indicates that an intruder is not able to infer with certainty which state a system is in at most K observational steps before the current instant, even if the intruder has weak discrimination on anonymous events. Similarly, infinite-step weak anonymity can be obtained by removing the restriction on the length of the observational string β in K-step weak anonymity. Definition 7: (Infinite-step weak anonymity) Given a system G = (X, Σ, δ, X0 ) and the weak anonymous projection Pw w.r.t. a set of anonymous events Γ and a set of observable events Σo with Γ ⊆ Σo , G is said to be infinite-step weakly anonymous w.r.t. Σo , Γ, and Pw if for all st ∈ L(G) with Pw (s) = α and Pw (st) = αβ, it holds bG (Pw , α|αβ)| > 1. |E ♢ Similar to Definition 4, the infinite-step weak anonymity also characterizes that the number of state estimates at any past instant inferred by an intruder are greater than 1. Compared with the strong anonymity projection Pstr , the weak anonymity projection Pw provides a more detailed description of anonymous events in a string, which may lead to the situation that strong anonymous projections of two strings are the same, but their weak anonymous projections are different. This also makes the verification of K- and infinite-step weak anonymity more complex. The following example illustrates the difference between strong anonymity and weak anonymity. Example 3: Reconsider the system G shown in Fig. 1. Suppose K = 0. For the purpose of verifying 0-step weak bG (Pw , αβ|αβ)| > 1 anonymity, we need to check whether |E holds for all αβ ∈ Pw (L(G)). Take string s = bb for bG (Pw , γ1 γ1 |γ1 γ1 )| = example. One has Pw (s) = γ1 γ1 and |E |{2}| = 1. It means that an intruder is sure that the system is in state 2 currently (i.e., 0 step ago) when observation γ1 γ1 is obtained. Obviously, system G is not 0-step weakly anonymous w.r.t. Σo , Γ, and Pw . Hence, G does not satisfy K-step weak anonymity for any K, suggesting that G is not infinite-step weakly anonymous. Compared that G is 1-step strongly anonymous w.r.t. Σo , Γ, and Pstr , one sees the huge difference between strong anonymity and weak anonymity. □

Similar to the proposed four types of anonymity, state-based opacity is also an information flow property based on state estimates. In general, when state-based opacity is concerned, the states of a system are typically divided into secret states and non-secret states. Opacity requires that an intruder can never be certain that a system is in secret states. It permits the intruder to determine that the system is in a specific non-secret state. However, the proposed anonymity captures a different scenario compared to opacity. It requires that the state estimates inferred by an intruder always contain at least two states. In other words, the essence of the proposed anonymity lies in preventing any form of state determination so as to the maintenance of state uncertainty. Moreover, in this paper, we consider this security and privacy requirement for the past K- and infinite observational steps under both ideal and nonideal anonymous processors, respectively. In summary, opacity and the proposed anonymity are two types of information flow properties that are used to characterize different security and privacy requirements. Specifically, opacity focuses on the ambiguity of the secret states of a system, while the proposed anonymity emphasizes the non-uniqueness of all states of a system. Based on their respective characteristics, opacity applies to the scenarios requiring “selective confidentiality”, while the proposed anonymity applies to those requiring “universal confidentiality” or “identity protection”. Remark 1: Here, we discuss the distinction and relationship among different anonymity notions. When Γ ̸= ∅, the proposed four notions of anonymity are different from those of [7] and [8] since it depends on how Γ is defined. If Γ = ∅, i.e., the strong and weak anonymous projections reduce to the natural projection P , then the notions of K-step (resp., infinite-step) strong anonymity and weak anonymity reduce to K-step (resp., infinite-step) anonymity defined in [8]. In this case, to verify whether a system satisfies K-step anonymity (resp., infinite-step) anonymity, we only need to check whether bG (P, α|αβ)| > 1 holds or not, where |β| ≤ K (resp., |E |β| has no restriction). For instance, consider the system G shown in Fig. 1 with Γ = ∅. After observing abc, an intruder certainly infers that the system is in state 2 after ab occurs, bG (P, ab|abc)| = |{2}| = 1. Thus, system G does i.e., |E not satisfy 1-step anonymity, suggesting that G also does not satisfy infinite-step anonymity. Further, if Γ = ∅ and K = 0, both K-step strong anonymity and weak anonymity in Definitions 3 and 6 reduce to currentstate anonymity defined in [7] and [8]. The requirement of current-state anonymity is that the set of possible current states of the system is never a singleton set. For example, reconsider the system G shown in Fig. 1 with Γ = ∅. An intruder determines that the system is in state 3 after observing ba, bG (P, ba|ba)| = |{3}| = 1, which violates current-state i.e., |E anonymity. Overall, the proposed four types of anonymity are more generalized versions of those of existing anonymity. In other words, the existing current-state anonymity, K-step anonymity, and infinite-step anonymity can be viewed as their special cases. In addition, by definitions, the relationship between K-step (resp., infinite-step) strong anonymity and weak anonymity is that G is K-step (resp., infinite-step) strongly

6

anonymous if it is K-step (resp., infinite-step) weakly anonymous, but not vice versa. □ Proposition 1: Given a system G = (X, Σ, δ, X0 ), a nonnegative integer K ∈ N, a set of observable events Σo , a set of anonymous events Γ with Γ ⊆ Σo , and the strong and weak anonymous projection Pstr and Pw , the following statements hold: e 1) system G is K-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ) if G is K-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ), e < K; and 0 ≤ K 2) it is K-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ) for any K ∈ N if G is infinite-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ). Proof: By Definitions 3, 4, 6, and 7, statements 1) and 2) are trivially true. IV. V ERIFICATION OF ANONYMITY USING CONCURRENT COMPOSITIONS

A. Verification of K- and infinite-step strong anonymity In this subsection, we focus on the verification of K- and infinite-step strong anonymity. According to the definition of strong anonymous projection, the observer of system G is constructed as a DFA, denoted by Obs(G) = (Xobs , Σobs , δobs , X0,obs ),

(2)

where X • Xobs = 2 is a finite set of states1 , • Σobs = (Σo \Γ) ∪ {γ} is a finite set of observable events, • δobs : Xobs × Σobs → Xobs is the transition function defined by: for any xobs ∈ Xobs and σobs ∈ Σobs , one has δobs (xobs , σobs ) = U R({x′ ∈ X|∃x ∈ xobs , ∃σ ∈ Γ : Pstr (σ) = γ ∧ x′ ∈ δ(x, σ)}) if σobs = γ, δobs (xobs , σobs ) = U R({x′ ∈ X|∃x ∈ xobs : x′ ∈ δ(x, σobs )}) otherwise, and • X0,obs = U R(X0 ) is the set of initial states. In observer Obs(G), the adjoint state set of state x in terms of state xobs is defined by ( U R(xobs \{x}), if x ∈ xobs , As(x, xobs ) = undefined, otherwise. We can tabulate all adjoint states of each state in all xobs ∈ Xobs . Note that there may be more than one adjoint state set for state x since x may be contained in different states of Xobs . Then, we construct a new observer of system G called a modified observer, defined by Obsm (G) = (Xm , Σm , δm , X0,m ),

(3)

where X • Xm = 2 is a finite set of states, 1 For the ease of showing anonymity verification algorithms, the set X obs includes all states that are reachable and unreachable (from X0,obs ). When depicting an automaton, we usually only draw its reachable part or its part related to verification of the corresponding definition of anonymity. In the sequel, we will define Obsm (G) from the reachable states in Xobs .

Σm = Σobs is a finite set of observable events, δm : Xm × Σm → Xm is the transition function defined by: for any xm ∈ Xm and σm ∈ Σm , δm (xm , σm ) = U R({x′ ∈ X|∃x ∈ xm , ∃σ ∈ Γ : Pstr (σ) = γ ∧ x′ ∈ δ(x, σ)}) if σm = γ, δm (xm , σm ) = U R({x′ ∈ X|∃x ∈ xm : x′ ∈Sδ(x, σm )}) otherwise, and x∈xobs • X0,m = {As(x, xobs )} is the set of initial • •

∅̸=xobs ∈X̄obs

states, where X̄obs is the set of reachable states in Obs(G) (note that ∅ ∈ X̄obs may hold.). Clearly, the only difference between Obs(G) and Obsm (G) is the set of initial states. Notation Obsm (G) characterizes the evolution of all non-empty adjoint state sets during all observational steps, which is critical for the subsequent decision on the existence of adjoint states within K observational steps. A variant of system G, denoted by Gm , is realized by letting all the states in G be initial states. Next, we introduce the main tool–concurrent composition. Definition 8: (Concurrent composition) Consider two automata Gi = (Xi , Σi , δi , X0,i ), i = 1, 2, where G1 and G2 are NFAs. Let ℓ : Σ1 → Σ2 ∪ {ϵ} be a projection mapping, where all events in Σ2 are observable. The concurrent composition of G1 and G2 is Cc(G1 , G2 ) = (X c , Σc , δ c , X 0,c ),

(4)

where2 c • X = X1 × X2 , c o,c • Σ =Σ ∪Σuo,c , where Σo,c = {(σ, σ ′ )|σ ∈ Σ1o ∧σ ′ ∈ Σ2 ∧ ℓ(σ) = σ ′ }, Σuo,c = {(σ, ϵ)|σ ∈ Σ1uo }, and Σ1o (resp., Σ1uo ) is the set of observable (resp., unobservable) events of Σ1 , ′ c o,c uo,c • for all (x1 , x2 ) ∈ X , (σ, σ ) ∈ Σ , and (σ, ϵ) ∈ Σ , ′ ′ ′ c 1) (x1 , x2 ) ∈ δ ((x1 , x2 ), (σ, σ )) if and only if x′1 ∈ δ1 (x1 , σ) and x′2 = δ2 (x2 , σ ′ ), 2) (x′1 , x′2 ) ∈ δ c ((x1 , x2 ), (σ, ϵ)) if and only if x′1 ∈ δ1 (x1 , σ) and x′2 = x2 , 0,c • X ⊆ X0,1 × X0,2 is the set of initial states and will be specified when defining (5) and (9). ♢ To verify K- and infinite-step strong anonymity, we construct the concurrent composition of Gm and Obsm (G) by considering projection mapping ℓ as the strong anonymous projection Pstr . The constructed concurrent composition is accordingly denoted by Cc(Gm , Obsm (G)) = (Xc , Σc , δc , X0,c ),

(5)

where Gm is the variant automaton for G by letting all the states in G be initial states, Obsm (G) is the modified observer as defined in (3) (Note that Obsm (G) is not an observer of Gm .), and the set of initial states X0,c = S x∈xobs {(x, As(x, xobs ))}, where X̄obs is the set of ∅̸=xobs ∈X̄obs

reachable states in Obs(G). A state xc in Cc(Gm , Obsm (G)) takes the form of xc = (x, q), where the left component x stands for the actual state of the system G, while the right component q represents the corresponding adjoint state set of the left component x. For any string sc ∈ 2 “Cc” is the abbreviation of “concurrent composition”.

7

L(Cc(Gm , Obsm (G))), the left and right components of sc are denoted as L(sc ) and R(sc ), respectively. By the construction of Cc(Gm , Obsm (G)), we find Pstr (L(sc )) = R(sc ). Next, we illustrate the construction of Cc(Gm , Obsm (G)) for system G. Example 4: Consider again the system G in Fig. 1. The observer Obs(G) is shown in Fig. 2. From the constructed Obs(G), we obtain the states and their corresponding adjoint state sets as shown in Table II. Further, the modified observer Obsm (G) and the variant automaton Gm are shown in Figs. 3 and 4, respectively. The concurrent composition Cc(Gm , Obsm (G)) is constructed as shown in Fig. 5. □ {0,1}

{2,3}

(0,{1})

(2,{2,3})

(4,{4,5,6})

(1,{0})

(3,{2})

(5,{4,6})

(2,{2})

(4,{4,6})

(6,{4,6})

(2,{3})

(4,{5})

(6,{5})

(4,{5,6})

(6,{5,6})

(6,{4,5,6})

Fig. 5. Part of the concurrent composition Cc(Gm , Obsm (G)).

{4,5,6}

Fig. 2. Part of the observer Obs(G) for G.

TABLE II S TATES AND THE CORRESPONDING ADJOINT STATE SETS

xobs

state

adjoint state set

{0,1}

0 1

{1} {0}

{2,3}

2 3

{3} {2}

{4,5,6}

4 5 6

{5,6} {4,6} {4,5,6}

{1}

{2,3}

{4,5,6}

{0}

{2}

{4,6}

{3}

{5}

{5,6}

Fig. 3. Part of the modified observer Obsm (G).

0

2

4

1

3

5

6

Fig. 4. The variant automaton Gm for G.

Now we present the main results of verifying K- and infinite-step strong anonymity using the proposed concurrent composition Cc(Gm , Obsm (G)).

Theorem 1: Given a system G = (X, Σ, δ, X0 ), let Cc(Gm , Obsm (G)) = (Xc , Σc , δc , X0,c ) be the corresponding concurrent composition. G is infinite-step (resp., K-step) strongly anonymous w.r.t. Σo , Γ, and Pstr if and only if there exists no state of the form (·, ∅) in Cc(Gm , Obsm (G)) that is reachable from X0,c (resp., within K observational steps). Proof: First, we show the case of K-step strong anonymity in Theorem 1. (if) By contrapositive, suppose that system G is not Kstep strongly anonymous w.r.t. Σo , Γ, and Pstr . By Definition 3, there exists a string st ∈ L(G) such that bG (Pstr , α|αβ)| > 1 does not hold, where Pstr (s) = α, |E bG (Pstr , α|αβ)| = 1. Pstr (st) = αβ, and |β| ≤ K. Then |E b Denote EG (Pstr , α|αβ) = {xc }. By the construction of Obs(G), xc ∈ xobs where xobs = δobs (X0,obs , α). By the construction of Obsm (G), δm (As(xc , xobs ), β) = ∅. By the construction of Cc(Gm , Obsm (G)), there exists a string sc ∈ L(Cc(Gm , Obsm (G))) with R(sc ) = β such that (xc,k , ∅) ∈ δc ((xc , As(xc , xobs )), sc ), where xc,k ∈ δ(xc , L(sc )). One concludes that (xc,k , ∅) is reachable from X0,c within K observational steps due to |Pstr (L(sc ))| = |R(sc )| ≤ K. (only if) Still by contrapositive, suppose that there exists a state of the form (·, ∅) in Cc(Gm , Obsm (G)) that is reachable from X0,c within K observational steps. By the construction of Cc(Gm , Obsm (G)), there exists a state (xc,k , ∅) ∈ Xc reached from some initial state (xc , As(xc , xobs )) ∈ X0,c and a string sc ∈ L(Cc(Gm , Obsm (G))) such that |R(sc )| ≤ K, xc ∈ xobs , xc,k ∈ δ(xc , L(sc )), and (xc,k , ∅) ∈ δc ((xc , As(xc , xobs )), sc ). By the construction of Obsm (G), δm (As(xc , xobs ), R(sc )) = ∅. Further, δ(x′c , t) = ∅ holds for all x′c ∈ As(xc , xobs ) and all t ∈ Σ∗ with Pstr (t) = R(sc ). Then, by the construction of Obs(G), one concludes that there exists an initial state x0 ∈ X0 and a string s ∈ L(G, x0 ) such that xc ∈ δ(x0 , s) and δobs (X0,obs , Pstr (s)) = xobs owing to xc ∈ xobs . Let Pstr (s) = α and Pstr (t) = β. bG (Pstr , α|αβ), i.e., Accordingly, xc is the unique state in E b |EG (Pstr , α|αβ)| = 1. By Definition 3, system G does not satisfy K-step strong anonymity w.r.t. Σo , Γ, and Pstr . The proof for the case of infinite-step strong anonymity is very similar to the mentioned case, we omit the details here. By Theorem 1, we summarize the verification procedures for K- and infinite-step strong anonymity as shown

8

in Algorithm 1. In Algorithm 1, the time costs of computing Obs(G), Obsm (G), Gm , and Cc(Gm , Obsm (G)) are O(|Σo ||Σuo ||X|2 2|X| ), O(|Σo ||Σuo ||X|2 2|X| ), O(|Σ||X|2 ), and O(|Σ||X|2 2|X| ), respectively. Hence, the overall time complexity for verifying K- and infinite-step strong anonymity using Algorithm 1 is O((|Σo ||Σuo | + |Σ|)|X|2 2|X| ). Note that the two-way observer method proposed in [12] can also verify K- and infinite-step strong anonymity by making slight modifications, but its complexity is higher than ours. Algorithm 1: Verification of Infinite-Step (resp., KStep) Strong Anonymity Input: System G = (X, Σ, δ, X0 ), Σo , Σuo , Γ ⊆ Σo , and K ∈ N. Output: “YES” if G satisfies infinite-step (resp., K-step) strong anonymity w.r.t. Σo , Γ, and Pstr , “NO” otherwise. 1 Construct the observer Obs(G) for G; 2 if there exists a reachable state xobs ∈ Xobs such that |xobs | = 1, then 3 return “No”; 4 stop; 5 else 6 Construct modified observer Obsm (G) for G; 7 Construct Gm as a variant of G; 8 Construct Cc(Gm , Obsm (G)) as the concurrent composition of Gm and Obsm (G); 9 Use the “Breadth-First Search Algorithm” in [31] to decide whether there exists a state of the form (·, ∅) in Cc(Gm , Obsm (G)) that is reachable from X0,c (resp., within K observational steps); 10 if there exists such a state (·, ∅) in Cc(Gm , Obsm (G)) that is reachable from X0,c (resp., within K observational steps), then 11 return “No”; 12 stop; 13 else 14 return “Yes”; 15 stop.

Example 5: Reconsider the system G in Fig. 1. The corresponding concurrent composition Cc(Gm , Obsm (G)) is shown in Fig. 5 in which there exists no reachable state of the form (·, ∅), concluding that G satisfies infinite-step strong anonymity. It also satisfies K-step strong anonymity for any value of K. The verification results are consistent with the conclusions in Example 1. □ B. Verification of K- and infinite-step weak anonymity As the weak anonymous projection Pw is a class of dynamic observation functions, the verification for K- and infinitestep anonymity under the weak anonymous projection Pw is more complicated than their verification under the strong anonymous projection Pstr . In other words, the previous Cc(Gm , Obsm (G)) cannot be used to verify K- and infinitestep weak anonymity. To this end, we need an augmented au-

tomaton to express historical information about the occurrence of anonymous events along with their corresponding location indices. Some symbols are introduced before constructing the augmented automaton of the system G. For theS anonymous b= event set Γ, we define its augmented set as Γ σ∈Γ {σi |i = b = {a1 , a2 , b1 , b2 } if 1, . . . , |Γ|}. For example, one has Γ Γ = {a, b}. For system G, its augmented system is defined by bX b = (X, b Σ, b δ, b0 ), G

(6)

where b = (X × {ϵ}) ∪ S|Γ| (X × {{(σ 1 )1 , . . . (σ i )i }|σ 1 , . . . , • X i=1 σ i ∈ Γ are distinct}) is a finite set of states, b =Γ b ∪ (Σo \Γ) ∪ Σuo is a finite set of events, where • Σ b b b uo , Σ bo = Γ b ∪ (Σo \Γ), and Σ b uo = Σuo , Σ = Σo ∪˙ Σ b X b: X b ×Σ b → 2 is defined by: • δ b e ∈ (Σo \Γ) ∪ Σuo , let (1) for any state (x, p) ∈ X, b δ((x, p), e) = {(x′ , p)|x′ ∈ δ(x, e)}, (2) for all 1 ≤ i ≤ |Γ|, 1 ≤ j ≤ i, b (σ j )j ∈ for all (x, {(σ 1 )1 , . . . , (σ i )i }) ∈ X, b b Γ, let δ((x, {(σ 1 )1 , . . . , (σ i )i }), (σ j )j ) = {(x′ , {(σ 1 )1 , . . . , (σ i )i })|x′ ∈ δ(x, σ j )}, (3) for all 0 ≤ i ≤ |Γ|, for all (x, {(σ 1 )1 , . . . , (σ i )i }) ∈ b (σ i+1 )i+1 b with σ 1 , . . . , σ i+1 being X, ∈ Γ 1 b distinct, let δ((x, {(σ )1 , . . . , (σ i )i }), (σ i+1 )i+1 ) = {(x′ , {(σ 1 )1 , . . . , (σ i )i , (σ i+1 )i+1 })|x′ ∈ δ(x, σ i+1 )}, b × Σ, b and (4) δb is not defined at any other pair in X b • X0 = X0 × {ϵ} is a finite set of initial states. b → Γw as We define a projection mapping P m : Γ m b P (σi ) = γi for all σi ∈ Γ with 1 ≤ i ≤ |Γ| to b by γi , where γi ∈ Γw and Γw = replace an event σi in Γ {γ1 , γ2 , . . . , γ|Γ| }. To describe the language generated by augb under the weak anonymous projection mented automaton G b ∗ → (Γw ∪ (Σo \Γ))∗ Pw , define a projection mapping P n : Σ as P n (ϵ) = ϵ and  n m b  P (s)P (σ), if σ ∈ Γ, P n (sσ) = P n (s)σ, if σ ∈ (Σo \Γ),   n P (s), otherwise. b ∗ and σ ∈ Σ. b Trivially, P n (L(G)) b = Pw (L(G)) where s ∈ Σ b the unobservable reach of holds. In augmented automaton G, b is defined as a state set Q ⊆ X b s)}. b U Rw (Q) = {q ′ ∈ X|∃q ∈ Q, ∃s ∈ Σ∗uo : q ′ ∈ δ(q, b is constructed as a DFA, denoted by Then, the observer for G d G) b = (X bobs , Σ b obs , δbobs , X b0,obs ), Obs(

(7)

where bobs = 2Xb is a finite set of states, • X b obs = Γw ∪ (Σo \Γ) is a finite set of observable events, • Σ bobs : X bobs × Σ b obs → X bobs is the transition function • δ bobs and σ b obs , one defined by: for any x bobs ∈ X b ∈ Σ b x ∈ x has δbobs (b xobs , σ b) = U Rw ({b x′ ∈ X|∃b bobs : x b′ ∈ b x, σ δ(b b)}) if σ b ∈ (Σo \Γ); δbobs (b xobs , σ b) = U Rw ({b x′ ∈ ′ ′ ′ m ′ b x, σ b x∈x b :x X|∃b bobs , ∃b σ ∈Γ b ∈ δ(b b ) ∧ P (b σ)=σ b}) otherwise, and b0,obs = U Rw (X b0 ) is the set of initial states. • X

9

In order to describe the state x ∈ X involved in x bobs ∈ bobs , let m(b X xobs ) = {x ∈ X|(x, ·) ∈ x bobs }. For any state x b= (x, ·) ∈ x bobs , we use its left part to denote its corresponding original state x, denoted by l(b x) = x. Write n(b x, x bobs ) = {(x, ·) ∈ x bobs |x = l(b x)} as the set of states in x bobs that corresponding to the same original state x. The adjoint state d G) b is set of state x b in terms of state x bobs in observer Obs( defined as   U Rw (b xobs \n(b x, x bobs )), if x b∈x bobs ∧      |m(b xobs )| > 1,  ASw (b x, x bobs ) = ∅, if x b∈x bobs ∧    |m(b xobs )| = 1,    undefined, otherwise. d G) b is derived by changing the set of Also, a variant of Obs( initial states, defined by b = (Xw , Σw , δw , X0,w ), Obsw (G)

b for G. Fig. 6. The augmented automaton G

(8)

where b X • Xw = 2 is a finite set of states, b • Σw = Σobs is a finite set of observable events, • δw : Xw ×Σw → Xw is the transition function defined by: for any xw ∈ Xw and σw ∈ Σw , one has δw (xw , σw ) = b x, σw )}) if σw ∈ b x ∈ xw : x U Rw ({b x′ ∈ X|∃b b′ ∈ δ(b ′ b x ∈ xw , ∃b (Σo \Γ); δw (xw , σw ) = U Rw ({b x ∈ X|∃b σ′ ∈ ′ ′ m ′ b x, σ b:x Γ b ∈S δ(b b ) ∧ P (b σ ) = σw }) otherwise, and • X0,w = {ASw (b x, x bobs )} is the initial state x̂∈x̂obs f ∅̸=x̂obs ∈X obs

d G). eobs is the set of reachable states in Obs( b sets, where X b be initial states, which enables us Let all the states in G b w . Now, the concurrent composition of to get a new NFA G b w and Obsw (G) b is constructed by considering projection G mapping ℓ as the projection mapping P n . The constructed concurrent composition is represented by w w b w , Obsw (G)) b = (Xcw , Σw Cc(G c , δc , X0,c ),

d G), b the table of states and their By the constructed Obs( corresponding adjoint state sets are shown in Table III. The b and variant automaton G b w are variant observer Obsw (G) depicted in Figs. 8 and 9, respectively. Then, the concurrent b w , Obsw (G)) b is constructed in Fig. 10. □ composition Cc(G

(9)

b w is the variant automaton for G b by letting all where G b be the initial states of G b w , Obsw (G) b is the states in G d G) b as defined in (8) (Obsw (G) b is variant observer of Obs( b w ), and the set of initial states X w = not an observer of G 0,c S eobs is the set of {(b x, ASw (b x, x bobs ))}, where X x̂∈x̂obs f ∅̸=x̂obs ∈X obs

w d G). b For any state xw reachable states in Obs( c ∈ Xc , the left w b component of xc tracks the states in G while the right component of xw c reflects the evolution of corresponding adjoint b w , Obsw (G))), b state set. For any string sc ∈ L(Cc(G L(sc ) and R(sc ) are used to denote the left and right components of sc , respectively. Thus, we have P n (L(sc )) = R(sc ). Now, we use an example to show the construction of the concurrent b w , Obsw (G)). b composition Cc(G b and Example 6: Consider again the system G in Fig. 1. G d b its observer Obs(G) are shown in Figs. 6 and 7, respectively3 . 3 Note that we denote the state (x, σ b by xe e) ∈ X σ for the sake of S|Γ| convenience, where σ e ∈ {ϵ} ∪ i=1 {{(σ 1 )1 , . . . , (σ i )i }|σ 1 , . . . , σ i ∈ Γ are distinct}. For example, states (0, ϵ) and (2, a1 ) are denoted by 0ϵ and 2a1 , respectively.

b for G. b [ G) Fig. 7. Part of the observer Obs(

TABLE III S TATES AND THE CORRESPONDING ADJOINT STATE SETS xobs

state

adjoint state set

{0ϵ, 1ϵ}

0ϵ 1ϵ

{1ϵ} {0ϵ}

{2a1 , 2b1 , 3b1 }

2a1 2b1 3b1

{3b1 } {3b1 } {2a1 , 2b1 }

{2b1 }

2b1

∅

{4b1 , 6b1 }

4b1 6b1

{6b1 } {4b1 , 6b1 }

{2a1 b2 , 3b1 a2 }

2a1 b2 3b1 a2

{3b1 a2 } {2a1 b2 }

{4a1 b2 , 6a1 b2 , 5b1 a2 }

4a1 b2 6a1 b2 5b1 a2

{6a1 b2 , 5b1 a2 } {4a1 b2 , 6a1 b2 , 5b1 a2 } {4a1 b2 , 6a1 b2 }

{4a1 , 6a1 , 4b1 , 6b1 , 5b1 }

4a1 6a1 4b1 6b1 5b1

{6a1 , 6b1 , 5b1 } {4a1 , 6a1 , 4b1 , 6b1 , 5b1 } {6a1 , 6b1 , 5b1 } {4a1 , 6a1 , 4b1 , 6b1 , 5b1 } {4a1 , 6a1 , 4b1 , 6b1 }

We present the main results of verifying K- and infinite-step weak anonymity using the proposed concurrent composition b w , Obsw (G)). b Cc(G Theorem 2: Given a system G = (X, Σ, δ, X0 ), let d G) b = (X bobs , Σ b obs , δbobs , X b0,obs ) be the observer and Obs( b w , Obsw (G)) b = (X w , Σw , δ w , X w ) be the correspondCc(G c c c 0,c ing concurrent composition. G is infinite-step (resp., K-step) weakly anonymous w.r.t. Σo , Γ, and Pw if and only if there

10

b Fig. 8. Part of the variant observer Obsw (G).

b w for G. b Fig. 9. The variant automaton G

b w , Obsw (G)) b that is exists no state of the form (·, ∅) in Cc(G w reachable from X0,c (resp., within K observational steps). Proof: We first prove the K-step weak anonymity. (if) By contrapositive, assume that system G does not satisfy K-step weak anonymity w.r.t. Σo , Γ, and Pw . By Definition 6, there exists a string s′ t′ ∈ L(G) such that bG (Pw , α|αβ)| > 1 does not hold, where Pw (s′ ) = α, |E bG (Pw , α|αβ)| = Pw (s′ t′ ) = αβ, and |β| ≤ K. This implies |E b 1. In this case, assume EG (Pw , α|αβ) = {xw }. By d G), b (xw , ·) ∈ x the construction of Obs( bobs can be obb b0,obs , α). By the constructained, where x bobs = δobs (X b one sees δw (ASw ((xw , ·), x tion of Obsw (G), bobs ), β) = b w , Obsw (G)), b ∅. By the construction of Cc(G there exb w , Obsw (G))) b ists a string sc ∈ L(Cc(G such that (xw,k , ∅) ∈ δcw (((xw , ·), ASw ((xw , ·), x bobs )), sc ), where b w , ·), L(sc )). Due to |P n (L(sc ))| = |R(sc )| ≤ K, xw,k ∈ δ((x b w , Obsw (G)) b that there exists a state of the form (·, ∅) in Cc(G w is reachable from X0,c within K observational steps. (only if) Still by contrapositive, suppose that there exists b w , Obsw (G)) b that is a state of the form (·, ∅) in Cc(G w reachable from X0,c within K observational steps. By the b w , Obsw (G)), b one concludes that there construction of Cc(G exists a state (xw,k , ∅) ∈ Xcw reached from some iniw tial state ((xw , ·), ASw ((xw , ·), x bobs )) ∈ X0,c and a string b w , Obsw (G)), b ((xw , ·), ASw ((xw , ·), x sc ∈ L(Cc(G bobs ))) with |R(sc )| ≤ K, where (xw , ·) ∈ x bobs , xw,k ∈ b w , ·), L(sc )), and (xw,k , ∅) ∈ δ w (((xw , ·), ASw ((xw , ·), δ((x c

b w , Obsw (G)). b Fig. 10. Part of the concurrent composition Cc(G

b we infer that x bobs )), sc ). By the construction of Obsw (G), b ′ , t) = ∅ δw (ASw ((xw , ·), x bobs ), R(sc )) = ∅. Further, δ(x w ′ b ∗ with holds for all xw ∈ ASw ((xw , ·), x bobs ) and all t ∈ Σ d G), b there P n (t) = R(sc ). Then, by the construction of Obs( b0 and a string s ∈ L(G, b x exists an initial state x b0 ∈ X b0 ) such n b b b that (xw , ·) ∈ δ(b x0 , s) and δobs (X0,obs , P (s)) = x bobs due to (xw , ·) ∈ x bobs . Let P n (s) = α and P n (t) = β. Based on the bG (Pw , α|αβ), i.e., above analysis, xw is the unique state in E b |EG (Pw , α|αβ)| = 1, where |β| ≤ K. System G does not satisfy K-step weak anonymity w.r.t. Σo , Γ, and Pw . The proof of the case of infinite-step weak anonymity can be obtained similarly. We propose an algorithm for verifying K- and infinitestep weak anonymity, as shown in Algorithm 2. As seen, d G), b Obs( b Obsw (G), b the time complexity of computing G, b w , and Cc(G b w , Obsw (G)) b G are O((|Γ|2 + |Σo \Γ| + b b 2 ), O(|Γ| + |Σo \Γ|)|Σuo ||X| b 2 2|X| |Σuo |)|X| ), O(|Γ| + b b 2 2|X| b 2 ), and |Σo \Γ|)|Σuo ||X| ), O((|Γ|2 + |Σo \Γ| + |Σuo |)|X| b 2 2 | X| b 2 ), respectively, where |X| b = O((|Γ| +|Σo \Γ|+|Σuo |)|X| P|Γ| |X| k=0 |Γ|! . The overall time complexity of verifying Kk!

11

and infinite-step weak anonymity is O((2|Σuo |(|Γ|+|Σo \Γ|)+ b b 2 2|X| (|Γ|2 + |Σo \Γ| + |Σuo |))|X| ). Algorithm 2: Verification of Infinite-Step (resp., Kstep) Weak Anonymity Input: System G = (X, Σ, δ, X0 ), Σo , Σuo , Γ ⊆ Σo , and K ∈ N. Output: “YES” if G satisfies infinite-step (resp., K-step) weak anonymity w.r.t. Σo , Γ, and Pw , “NO” otherwise. b for G; 1 Construct the augmented automaton G d G) b for G; b 2 Construct the observer Obs( b 3 if there exists a state x bobs ∈ Xobs such that |m(b xobs )| = 1, then 4 return “No”; 5 stop; 6 else b for G; b 7 Construct modified observer Obsw (G) b w as a variant of G; b 8 Construct G b b 9 Construct Cc(Gw , Obsw (G)) as the concurrent b w and Obsw (G); b composition of G 10 Use the “Breadth-First Search Algorithm” to decide whether there exists a state of the form b w , Obsw (G)) b that is reachable from (·, ∅) in Cc(G w X0,c (resp., within K observational steps); 11 if there exists such a state (·, ∅) in b w , Obsw (G)) b that is reachable from X0,c Cc(G (resp., within K observational steps), then 12 return “No”; 13 stop; 14 else 15 return “Yes”; 16 stop.

Example 7: Reconsider Example 3. The corresponding conb w , Obsw (G)) b is shown in Fig. 10, current composition Cc(G where there exists an initial state (2b1 , ∅). By Theorem 2, we conclude that G is not K-step weakly anonymous w.r.t. to Pw and Γ for any K. Therefore, G is also not infinite-step weakly anonymous w.r.t. to Pw and Γ. The results are consistent with Example 3. □ Finally, we discuss both the proposed verification method and the existing ones for verifying anonymity and opacity properties. Two comparison tables of methods for verifying different types of anonymity and opacity with complexities are presented in Tables IV and V, respectively. From the tables, one sees that our concurrent composition plus the observer method currently provides the most efficient algorithms for verifying all kinds of anonymity and opacity properties. Furthermore, we find that the complexities of methods for verifying K- and infinite-step opacity and anonymity (i.e., initialstate estimator, two-way observer, and non-secret specification plus the observer) all depend on the value of K. In contrast, the idea of the concurrent-composition technique is to construct a K-free information structure. It means that once a system is

given, a concurrent composition information structure can be constructed to verify K-step strong (resp., weak) anonymity for any K ∈ N. This contrasts with the two-way observer approach, where the construction depends explicitly on K (i.e., for each different K, a new two-way observer must be constructed). To sum up, the use of concurrent-composition techniques results in lower complexity and enables the constructed information structure to be independent of K. Note that the proposed method for verifying K- and infinitestep strong anonymity can also be used to verify K- and infinite-step anonymity in [8]. In addition, the methods listed in Table V for verifying K- and infinite-step opacity can also be used to verify K- and infinite-step anonymity (resp., Kand infinite-step strong anonymity with slight modifications). When Γ = ∅, K-step (resp., infinite-step) strong anonymity and weak anonymity reduce to K-step (resp., infinite-step) anonymity. In this case, all methods for verifying K- and infinite-step opacity can be used for their verification. V. M AXIMAL K AND UPPER BOUNDS ON K FOR K- STEP STRONG / WEAK ANONYMITY A. Maximal K for K-step strong/weak anonymity In this subsection, we aim to obtain the maximal value of K that makes system G satisfy K-step strong (resp., weak) anonymity. To this end, we first define the minimum length of the strong (resp., weak) exposure distance ks (resp., kw ) which is the minimum value of K that violates K-step strong (resp., weak) anonymity. Definition 9: (Minimum length of the strong and weak exposure distance) Given a system G, its corresponding two concurrent compositions are Cc(Gm , Obsm (G)) = w b w , Obsw (G)) b = (Xcw , Σw (Xc , Σc , δc , X0,c ) and Cc(G c , δc , w X0,c ), respectively. (1) A non-negative integer ks ∈ N is said to be the minimum length of the strong exposure distance if (∄x0,c ∈ X0,c )(∄t ∈ L(Cc(Gm , Obsm (G)), x0,c ))(∄Z ∈ N) [(·, ∅) ∈ δc (x0,c , t) ∧ |R(t)| = Z ∧ Z < ks ]. (2) A non-negative integer kw ∈ N is said to be the minimum length of the weak exposure distance if w ′ w ′ b b (∄xw 0,c ∈ X0,c )(∄t ∈ L(Cc(Gw , Obsw (G)), x0,c ))(∄Z ∈ N) ′ ′ ′ ′ [(·, ∅) ∈ δcw (xw 0,c , t ) ∧ |R(t )| = Z ∧ Z < kw ]. ♢ Now, we design an algorithm to compute the maximal K for K-step strong/weak anonymity, as shown in Algorithm 3. b w , Obsw (G))), b In Cc(Gm , Obsm (G)) (resp., Cc(G we check whether there exists a state taking the form (·, ∅) reached from w an initial state in X0,c (resp., X0,c ). If the answer is “no”, Algorithm 3 outputs “∞”, which means that system G satisfies infinite-step strong (resp., weak) anonymity. If the answer is “yes”, we need to find the minimum length of the strong (resp., weak) exposure distance ks (resp., kw ). Algorithm 3 outputs “NA” if ks = 0 (resp., kw = 0), indicating that the maximal K does not exist. Algorithm 3 outputs “ks − 1” (resp., “kw − 1”) if ks > 0 (resp., kw > 0), suggesting that the maximal K for K-step strong (resp., weak) anonymity is ks − 1.

12

TABLE IV M ETHODS FOR VERIFYING DIFFERENT TYPES OF ANONYMITY WITH COMPLEXITIES method

current-state anonymity

observer

O(|Σo ||Σ||X|2 2|X| ) ([7])

two-way observer

concurrent composition + observer

O(|Σo ||Σ||X|2 2|X| ) ([26] with slight modification)

K/infinite-step anonymity

K/infinite-step strong anonymity

O(|Σo ||Σ||X|2 2|X|+1 + min{2|X| , |Σo |K }|Σo |2|X| )/ O(|Σo ||Σ||X|2 2|X|+1 + |Σo |4|X| ) ([8], [12])

O(|Σo ||Σ||X|2 2|X|+1 + min{2|X| , |Σo |K }|Σo |2|X| )/ O(|Σo ||Σ||X|2 2|X|+1 + |Σo |4|X| ) ([8], [12])

O(|X|2 2|X| (|Σo ||Σuo |+ |Σ|)) (Theorem 1 with slight modification)

O(|X|2 2|X| (|Σo ||Σuo |+ |Σ|)) (Theorem 1)

K/infinite-step weak anonymity

b 2 2|X| (2|Σo |(|Γ|+ O(|X| |Σo \Γ|) + (|Γ|2 + |Σo \Γ| + |Σuo |)) (Theorem 2) b

TABLE V M ETHODS FOR VERIFYING DIFFERENT TYPES OF STATE - BASED OPACITY WITH COMPLEXITIES method

current-state opacity

observer

O(|Σo ||Σ||X|2 2|X| ) ([11])

initial-state opacity

reverse observer

O(|Σo ||Σ||X|2 2|X| ) ([32])

initial-state estimator

O(|Σo |2|X| ) ([32])

2

two-way observer

K-step opacity

infinite-step opacity

O(|Σo |2|X| (|Σo |+ |X|2 −1 ) ) ([33]) 1)min(K,2

O(|Σo |2|X|+|X| ) ([13])

O(|Σo ||Σ||X|2 2|X|+1 + min{2|X| , |Σo |K }|Σo |2|X| ) ([12])

O(|Σo ||Σ||X|2 2|X|+1 + |Σo |4|X| ) ([12])

2

non-secret specification automaton + observer

O(|Σo ||Σ||X|2 22|X|+3 ) ([34])

O(3|Σo ||Σ||X|2 23|X|+2 ) ([34])

O(|Σo ||Σ||X|2 (K+ 3)2(K+3)|X|+2 ) ([34])

O(|Σo ||Σ||X|2 (2|X| +

concurrent composition + observer

O(|Σo ||Σ||X|2 2|X| ) ([26])

O(|Σo ||Σ||X|2 2|X| ) ([26])

O(|Σo ||Σ||X|2 2|X| ) ([14], called product automaton)

O(|Σo ||Σ||X|2 2|X| ) ([35], called product automaton)

Algorithm 3: Computing the Maximal K for K-Step Strong (resp., Weak) Anonymity Input: System G = (X, Σ, δ, X0 ), Σo , Σuo , and Γ ⊆ Σo . 1 Construct the corresponding concurrent composition b w , Obsw (G))); b Cc(Gm , Obsm (G)) (resp., Cc(G 2 if there exists no state of the form (·, ∅) in b w , Obsw (G))) b Cc(Gm , Obsm (G)) (resp., Cc(G then 3 Output “∞” and exit; 4 else 5 Use the “Breadth-First Search” to find the minimum length of the strong (resp., weak) exposure distance ks (resp., kw ); 6 if ks = 0 (resp., kw = 0) then 7 Output “NA” and exit; 8 else 9 Output “ks − 1” (resp., “kw − 1”) and exit;

|X|

3)2(2

+3)|X|+2 ) ([34])

B. Upper bounds on K in K-step strong anonymity and weak anonymity In this subsection, we will give two upper bounds on K for K-step strong anonymity and weak anonymity, respectively. Proposition 2: Given a system G = (X, Σ, δ, X0 ), for any b b > K ≥ |X| · 2|X| (resp., |X| b · 2|X| K ), G is K-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ) b if and only if G is K-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ). Proof: We show it holds for the case of K-step strong anonymity first. By Proposition 1, the “if” part holds. We focus on the “only if” part, which requires us to prove that b if G satisfies K-step strong anonymity, then G satisfies Kstep strong anonymity. Without loss of generality, we assume b = K +1, which can be naturally generalized to K b > K +1. K For brevity, let e = (|X| · 2|X| ) + 1. Then, we only prove that G is e-step strongly anonymous if G is (e − 1)-step strongly anonymous. By contrapositive, suppose that system G does not satisfy e-step strong anonymity. It means that there exists a string st ∈ L(G) with Pstr (s) = α, Pstr (t) = β, and bG (Pstr , α|αβ)| > 1 does not hold. By |β| ≤ e such that |E the construction of Cc(Gm , Obsm (G)), there exists a state xn,c = (·, ∅) reached by a string sc ∈ L(Cc(Gm , Obsm (G))) from an initial state x0,c within e observational steps, i.e.,

13

xn,c ∈ δc (x0,c , sc ) and |Pstr (L(sc ))| = |R(sc )| ≤ e. Consider (σ1 ,η1 )

(σ2 ,η2 )

(σn ,ηn )

the complete run x0,c −−−−→ x1,c −−−−→ · · · −−−−−→ xn,c = (·, ∅). Let the actual number of observational steps in sc be k, i.e., k = |R(sc )| = |η1 η2 · · · ηn |, where k ≤ e. Now, identify the positions where new observational steps occur. Let 0 = m0 < m1 < m2 < · · · < mk = n be the indices where ηmi ̸= ϵ. Define the immediate state after the i-th observational step as yi,c = xmi ,c . One has yk,c = xmk ,c = xn,c = (·, ∅) since the right component ∅ of xn,c is derived from the last updated observational step at the end of the string sc . The state space of Cc(Gm , Obsm (G)) has at most N = |X| · 2|X| states. Now, we need to consider two cases: Case 1: k ≤ N . In this case state yk,c = (·, ∅) is reached within k ≤ N ≤ e − 1 observational steps, which contradicts the (e − 1)-step strong anonymity. Case 2: k = N + 1 = e. In this case there are e + 1 states: y0,c , y1,c , . . . , and ye,c , where ye,c = (·, ∅). By the pigeonhole principle, there exist indices i and j with 0 ≤ i < j ≤ e such that yi,c = yj,c . Let sc be the prefix of sc that ends at state yi,c (after i-th observational steps). State yi,c = (·, ∅) is reached through the string sc within i ≤ e−1 observational steps, contradicting the (e − 1)-step strong anonymity. Both cases show that system G does not satisfy (e − 1)-step strong anonymity and thus completes the proof. The proof of the upper bounds for K-step weak anonymity is very similar to that of K-step strong anonymity. We omit it here due to the limited space. Theoretically, the meaning of the upper bound K̄ on K in K-step strong or weak anonymity is the “maximum depth” that the corresponding concurrent composition b w , Obsw (G)) b needs to be examCc(Gm , Obsm (G)) or Cc(G ined. In other words, after undergoing the corresponding K̄ observational steps, concurrent composition Cc(Gm , Obsm (G)) b w , Obsw (G)) b no longer generates any new state or Cc(G that does not appear in paths of length less than or equal to K̄. Moreover, for all values L greater than K̄, L-step strong/weak anonymity property holds naturally. That is, if a system satisfies (or does not satisfy) K-step strong/weak anonymity when K reaches its upper bound K̄, then for any value L greater than K̄, the system still satisfies (or does not satisfy) L-step strong/weak anonymity. Practically, the upper bound K̄ on K may be significant for dynamic security strategies. For instance, cloud service providers aim to protect customers’ virtual machines from side-channel attacks. The cloud platform defense system could consider utilizing K̄ to implement a dynamic security strategy. Specifically, a virtual machine is migrated to a potentially insecure host machine. During K̄ observational steps, a highintensity and high-overhead active defense mechanism is employed, such as real-time monitoring and/or obfuscation techniques. This ensures the state non-uniqueness of the virtual machine, such that the cloud platform defense system satisfies K-step strong/weak anonymity. Based on the above theoretical analysis, the virtual machine is stable on its current host and maintains K-step strong/weak anonymity when the number of observational steps exceeds K̄, which drives the system to switch to a low-cost maintenance mode. In a word, a high-

cost mode will stop until K̄ is reached, at which point a lowcost maintenance mode is activated. This strategy minimizes performance degradation caused by defensive measures such as migration and monitoring while ensuring security. Notably, an optimal balance between safety and efficiency is achieved. Corollary 1: Given a system G = (X, Σ, δ, X0 ), a strong (resp., weak) anonymous projection Pstr (resp., Pw ) w.r.t. a set of anonymous events Γ and a set of observable events Σo with Γ ⊆ Σo , G is infinite-step strongly (resp., weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ) if and only if G b b · 2|X| is (|X| · 2|X| )-step strongly (resp., (|X| )-step weakly) anonymous w.r.t. Σo , Γ, and Pstr (resp., Pw ). Proof: The results are obtained directly from Propositions 1 and 2. VI. A CASE STUDY ON A SIMPLE ANONYMOUS QUESTIONING PROCESS

In this section, we apply the developed notions of Kand infinite-step strong anonymity and weak anonymity to an anonymous questioning process to demonstrate the proposed methods. We adapt the example from [5] and add more details. A chemical development company R asks company Q to prepare a feasibility study on developing a new chemical. When this procedure is completed, company R is informed of the result of this study. Then, company R decides to commission a chemical safety report from a specialized agency. The specialized agency will choose some professional consultants. The relevant law allows the chosen professional consultants to question company Q on aspects of the feasibility study. To ensure the integrity and impartiality of the answer of company Q, the identity of any exact consultant involved cannot be inferred by company Q. In other words, from the viewpoint of company Q, the observable actions cannot expose any exact consultant. We model a simple anonymous questioning process for company Q, as shown in Fig. 11. The whole process should start with an initial review stage before moving on to the questioning stage. The green part of Fig. 11 represents that there are two consultants M and N who are responsible for the initial review process, whereas the blue part of Fig. 11 denotes the questioning process between consultants A–G and company Q. The questioning of consultants is sequential since the latter’s questioning is based on the former’s questioning. For instance, consultant A is only allowed to initiate questioning after the initial review of consultant M while consultant B is not. The events a−g represent that “consultants A–G initiate questioning to company Q”, respectively. It is a fact that only the questioning process with the associated sensors can be observed. In the general cases, not all questioning devices are equipped with sensors due to the consideration of the cost savings. This results in the situation that only part of the questioning process can be observed. Assume that the actions “consultants A, B, C, D, and F initiate questioning to company Q” can be observed by company Q since company Q can detect the sensor signals from the questioning devices of consultants A, B, C, D, and F, i.e., Σo = {a, b, c, d, f }. The occurrence of actions “consultants E and G initiate questioning to company

ompany B questions

3: Company 3 interacts with Company B

ompany B questions

4: Company 4 interacts with Company B

14 ompany B questions

5: Company 4 interacts with Company B

ompany B questions

6: Company 6 interacts with Company B

}

int } } } } 6} 6} ,6} } 8}

7: Company 7 interacts withby Company B Q” cannot be captured company Q since there are no Company 8 interacts with Company B sensors8:deployed on the questioning devices of consultants E and G and company Q cannot detect the sensor signals, i.e., Σuo = {e, g}. To maximize the concealment of the identity of all consultants, consultants A, B, C, D, and F add anonymous {2,3} {4,5,6} {7,8} processors to their questioning devices, i.e., Γ = Σo . States M and N represent that consultants M and N are initially reviewing company Q, respectively. States A–G represent that company Q answers consultants A–G, respectively.

M

A

C E

N

B

F

G

D

Initial review

Questioning stage

Fig. 11. System G∗ : The model of a simple anonymous questioning process for company Q. question

question

qu e

A by C b stion the processing power We needMto by consider E A two cases C yfor of anonymous processors. stOne is that the processing power on i e E question F question G of anonymous processorsqu bisy C ideal, which means that actions by F by G ion t s e and B D E representingN “consultants A, B, C, D, F initiate questioning u q by question question by B by D to company Initial Q” can be observed as γ by company Q. The Questioning stage other isreview that the processing power of anonymous processors is less powerful such that the same result can be obtained for specific actions only performed by the same agent. For instance, company Q can observe γ1 γ2 when action string ac or bd happens. Specifically,

The first case corresponds to the strong anonymous projection. The concurrent composition Cc(G∗m , Obsm (G∗ )) for the modeled system G∗ can be constructed to verify K-step strong anonymity, which is omitted here to save space. We conclude that the system is K-step strongly anonymous for any value of K, suggesting that the modeled system is infinite-step strongly anonymous. For instance, assume K = 1. Consider action strings s = ce and t = f g. Then, Pstr (s) = γ and Pstr (st) = γγ can be obtained. The delayed state estimate at the instant that the first γ has just been observed upon observing γγ bG (Pstr , γ|γγ) = can be inferred as {A, B, C, E}, i.e., E {A, B, C, E}. It means that company Q cannot determine the identity of any precise consultant when the first γ is captured even according to 1 observational step future information if the processing power of anonymous processors is ideal such that company Q cannot distinguish questions from different consultants. • The second case corresponds to the weak anonymous projection. Similarly, we verify K-step weak anonymity by constructing the concurrent composition b ∗w , Obsw (G b ∗ )) of the modeled system G∗ , which Cc(G is also omitted here. By computation, it is found that the modeled system G∗ satisfies infinite-step weakly anonymity. It means that company Q cannot infer the identity of any accurate consultant at any instant even though it knows future information when the processing power of anonymous processors is less powerful such that •

company Q can only distinct the actions performed by the same consultant. VII. C ONCLUDING R EMARKS Anonymity and opacity are both information flow properties based on state estimates. The four K- and infinite-step anonymity concepts proposed in this paper are essentially different from the existing K- and infinite-step anonymity [8], [10] and opacity [12]–[14] since we take the strong and weak anonymous projections into account. Particularly, when the anonymous events are not considered, i.e., Γ = ∅, the strong and weak anonymous projections reduce to the natural projection. Note that the strong anonymous projection Pstr can be viewed as a natural extension of the natural projection, but the weak anonymous projection Pw is more complicated, i.e., the weak anonymous projection of a string contains more information than its strong anonymous projection. For instance, assume Γ = {a, b} ⊆ Σo . The strong anonymous projection of strings aab and abb are Pstr (aab) = Pstr (abb) = γγγ, whereas the weak anonymous projection of strings aab and abb are Pw (aab) = γ1 γ1 γ2 and Pw (abb) = γ1 γ2 γ2 . That is, the weak anonymous projection of an anonymous event depends on when it first appears in a string. As a result, the verification of K- and infinite-step anonymity under the weak anonymous projection is much more difficult. The classical observer cannot capture this scenario accurately. Therefore, no existing methods for verifying K- and infinite-step opacity can be used to verify K- and infinite-step anonymity under the weak anonymous projection. Using the designed concurrent-composition-based verification method, one accurately captures the state information to verify the K- and infinite-step anonymity under the weak anonymous projection. Upper bounds on K for K-step strong anonymity and weak anonymity are also obtained. Furthermore, the proposed methodology is sufficiently general, as it can also be used to verify the K- and infinite-step opacity/anonymity under the natural projection efficiently. A case study on an anonymous questioning process is provided for practical applications. It is a fact that verifying K/infinite-step opacity in discreteevent systems is PSPACE-hard, as established in the literature [11], [13]. K/infinite-step anonymity [8] and K/infinite-step opacity are closely related information-flow properties. Their verification structures are essentially the same. This means that verifying K/infinite-step anonymity [8] in discrete-event systems is also PSPACE-hard. As discussed in Remark 1, the proposed four anonymity notions reduce to the existing K-step and infinite-step anonymity [8] when Γ = ∅. As a result, the verification of the four notions of anonymity proposed in this technical note is also PSPACE-hard. It seems highly unlikely that there exist polynomial-time algorithms to verify the four types of anonymity considered in this paper unless P=PSPACE. This means that when handling large-scale practical systems, the proposed algorithms will face challenges such as state space explosion problem (i.e., the state spaces of the constructed verifiers are all exponential) and memory consumption (i.e., the memory usage grows exponentially since

15

the “Breadth-First Search” traversal requires storing all visited states). To overcome such limitations, in the future, we will consider employing approximate methods, such as abstractionrefinement [36] and machine learning [37]. The former constructs a series of progressively precise approximate models to approach the verification problems of complex systems in a controllable manner, thereby achieving computational feasibility while ensuring correctness. The latter provides probabilistic predictions whose accuracy depends on the quality of training data and model capabilities. Both methods align with the regular structure of the constructed concurrent composition. In addition, the idea of over-approximation state estimation proposed in [38] will also be considered. To move forward, we will focus on enforcing these four types of anonymity based on the proposed verification method in the future. R EFERENCES

[1] S. Schneider and A. Sidiropoulos, “CSP and anonymity,” in Proc. 4th Eur. Symp. Res. Comput. Secur., 1996, pp. 198–218. [2] M. K. Reiter and A. D. Rubin, “Crowds: anonymity for Web transactions,” ACM Trans. Inf. Syst. Secur., vol. 1, no. 1, pp. 66–92, 1998. [3] V. Shmatikov, “Probabilistic model checking of an anonymity system,” J. Comput. Secur., vol. 12, no. 3–4, pp. 355–377, 2004. [4] R. Dingledine, N. Mathewson, and P. Syverson, “Reputation in P2P anonymity systems,” in Workshop Econ. Peer-to-Peer Syst., 2003, vol. 92, pp. 1–5. [5] J. W. Bryans, M. Koutny, L. Mazaré, and P. Ryan, “Opacity generalised to transition systems,” Int. J. Inf. Secur., vol. 7, no. 6, pp. 421–435, 2008. [6] F. Lin, “Opacity of discrete event systems and its applications,” Automatica, vol. 47, no. 3, pp. 496–503, 2011. [7] Y. Wu, K. A. Sankararaman, and S. Lafortune, “Ensuring privacy in location-based services: an approach based on opacity enforcement,” in Proc. 12th IFAC/IEEE Workshop Discrete Event Syst., 2014, vol. 47, no. 2, pp. 33–38. [8] J. C. Basilio, C. N. Hadjicostis, and R. Su, “Analysis and control for resilience of discrete event systems: fault diagnosis, opacity and cyber security,” Found. Trends Syst. Control, vol. 8, no. 4, pp. 285–443, 2021. [9] L. Sweeney, “K-anonymity: A model for protecting privacy,” Int. J. Uncertainty Fuzziness Knowl.-Based Syst., vol. 10, no. 5, pp. 557–570, 2002. [10] X. Yin and S. Li, “Synthesis of dynamic masks for infinite-step opacity,” IEEE Trans. Autom. Control, vol. 65, no. 4, pp. 1429–1441, 2020. [11] A. Saboori and C. N. Hadjicostis, “Notions of security and opacity in discrete event systems,” in Proc. IEEE 46th Conf. Decis. Control, 2007, pp. 5056–5061. [12] X. Yin and S. Lafortune, “A new approach for the verification of infinitestep and K-step opacity using two-way observers,” Automatica, vol. 80, pp. 162–171, 2017. [13] A. Saboori and C. N. Hadjicostis, “Verification of infinite-step opacity and complexity considerations,” IEEE Trans. Autom. Control, vol. 57, no. 5, pp. 1265–1269, 2012. [14] J. Balun and T. Masopust, “Verifying weak and strong k-step opacity in discrete-event systems,” Automatica, vol. 155, 111153, 2023. [15] S. Yang and X. Yin, “Secure your intention: on notions of pre-opacity in discrete-event systems,” IEEE Trans. Autom. Control, vol. 68, no. 8, pp. 4754–4766, 2023. [16] S. Shu, F. Lin, and H. Ying, “Detectability of discrete event systems,” IEEE Trans. Autom. Control, vol. 52, no. 12, pp. 2356–2359, 2007. [17] S. Shu and F. Lin, “Delayed detectability of discrete event systems,” IEEE Trans. Autom. Control, vol. 58, no. 4, pp. 862–875, 2012. [18] M. V. S. Alves and J. C. Basilio, “State estimation and detectability of networked discrete event systems with multi-channel communication networks,” IEEE Trans. Autom. Sci. Eng., vol. 21, no. 3, pp. 2622–2637, 2024. [19] L. Zhou, S. Shu, and F. Lin, “Detectability of discrete-event systems under nondeterministic observations,” IEEE Trans. Autom. Sci. Eng., vol. 18, no. 3, pp. 1315–1327, 2020.

[20] S. Lafortune, F. Lin, and C. N. Hadjicostis, “On the history of diagnosability and opacity in discrete event systems,” Annu. Rev. Control, vol. 45, pp. 257–266, 2018. [21] S. Takai, “A general framework for diagnosis of discrete event systems subject to sensor failures,” Automatica, vol. 29, 109669, 2021. [22] J. W. Wang, S. Baldi, W. W. Yu, and X. Yin, “Distributed fault diagnosis in discrete event systems with transmission delay impairments,” IEEE Trans. Autom. Control, vol. 69, no. 8, pp. 5508–5515, 2024. [23] Z. Ma, Y. Tong, and C. Seatzu, “Verification of pattern-pattern diagnosability in partially observed discrete event systems,” IEEE Trans. Autom. Control, vol. 69, no. 3, pp. 2044–2051, 2023. [24] B. Zhang, S. Shu, and F. Lin, “Maximum information release while ensuring opacity in discrete event systems,” IEEE Trans. Autom. Sci. Eng., vol. 12, no. 3, pp. 1067–1079, 2015. [25] J. Hou, X. Yin, and S. Li, “A framework for current-state opacity under dynamic information release mechanism,” Automatica, vol. 140, 110238, 2022. [26] K. Zhang, “A unified concurrent-composition method to state/event inference and concealment in labeled finite-state automata as discreteevent systems,” Annu. Rev. Control, vol. 56, 100902, 2023. [27] X. Han, K. Zhang, J. Zhang, Z. Li, and Z. Chen, “Strong current-state and initial-state opacity of discrete-event systems,” Automatica, vol. 148, 110756, 2023. [28] X. Han, K. Zhang, and Z. Li, “Verification of strong K-step opacity for discrete-event systems,” in Proc. IEEE 61st Conf. Decis. Control, 2022, pp. 4250–4255. [29] C. G. Cassandras and S. Lafortune, Introduction to Discrete Event Systems. 3rd ed., Cham, Switzerland: Springer, 2021. [30] C. N. Hadjicostis, Estimation and Inference in Discrete Event Systems. Cham, Switzerland: Springer, 2020. [31] T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms. 4th ed., MIT Press, 2022. [32] Y. Wu and S. Lafortune, “Comparative analysis of related notions of opacity in centralized and coordinated architectures,” Discret. Event Dyn. Syst.-Theory Appl., vol. 23, no. 3, pp. 307–339. 2013. [33] A. Saboori and C. N. Hadjicostis, “Verification of K-step opacity and analysis of its complexity,” IEEE Trans. Autom. Sci. Eng., vol. 8, no. 3, pp. 549–559, 2011. [34] A. Wintenberg, M. Blischke, S. Lafortune, and N. Ozay, “A general language-based framework for specifying and verifying notions of opacity,” Discret. Event Dyn. Syst.-Theory Appl., vol. 32, no. 2, pp. 253–289, 2022. [35] J. Balun and T. Masopust, “Comparing the notions of opacity for discrete-event systems,” Discret. Event Dyn. Syst.-Theory Appl., vol. 31, no.4, pp. 553–582, 2021. [36] J. Wang, J. Sun, S. Qin, and C. Jegourel, “Automatically ‘verifying’ discrete-time complex systems through learning, abstraction and refinement,” IEEE Trans. Softw. Eng., vol. 47, no. 1, pp. 189–203, 2021. [37] S. Ding, G. Liu, L. Yin, J. Wang, and Z. Li, “Detection of cyber-attacks in a discrete event system based on deep learning,” Mathematics, vol. 12, no. 17, 2635, 2024. [38] Z. Xiang, Y. Chen, N. Wu, and Z. Li, “Over-approximation state estimation for networked timed discrete event systems with communication delays and losses,” IEEE Trans. Syst. Man Cybern. -Syst., vol. 55, no. 2, pp. 1215–1229, 2025.

Related documents

• Copy-Protection with Correlated Challenges: Point Functions and More via Decisional Coset Monogamy#467076
• Concurrent composition for differentially private continual mechanisms#405944
• Stable Matching with Deviators and Conformists#670470
• Stable Matching with Deviators and Conformists#668405
• A Trusted Approach for Decentralised and Privacy-Preserving Identity Management#679029