PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Jiahui Zhang, Kuize Zhang, Xiaoguang Han, Zhiwu Li

arXiv:2609.01192v1cs.FLcs.CR

TL;DR

The paper studies four K- and infinite-step anonymity notions for partially observed discrete-event systems under strong and weak anonymous projections. It uses concurrent compositions to derive verification conditions and computes finite upper bounds on K for strong and weak anonymity.

  • Problem

    Existing K- and infinite-step anonymity notions do not cover the distinct observation capabilities represented by strong and weak anonymous projections.

  • Method

    The paper exploits concurrent compositions to verify the four anonymity types and establish necessary and sufficient verification conditions.

  • Results

    The constructed compositions yield verifiable necessary and sufficient conditions, including a no-reachable-state criterion for weak anonymity and finite upper bounds on K.

  • Takeaways & Limitations

    The framework separately verifies strong and weak anonymity and computes upper bounds connecting infinite-step anonymity with bounded-step verification.

  • Takeaways & Limitations

    Verification faces exponential state-space explosion and memory consumption because the constructed verifiers are exponential and breadth-first search stores visited states.

Abstract

from arXiv · show

Anonymity is an information flow property that provides privacy protection in the sense of non-uniqueness 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 infinite-step 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.

I. INTRODUCTION

The paper studies anonymity as an information-flow property for partially observed discrete-event systems, focusing on four notions defined through strong and weak anonymous projections. It develops concurrent-composition-based verification conditions for these notions.

  • Motivation: Anonymity protects privacy by requiring non-uniqueness in an intruder’s estimate of the system state.The paper relates this property to applications including anonymous voting, donations, and transactions.
  • Observation models: Strong anonymous projections hide the identities behind anonymous actions using a static observation function.Different anonymous events receive the same observation, while other observable events remain distinguishable.
  • Observation models: Weak anonymous projections use dynamic observations that preserve whether anonymous actions were performed by the same agent without revealing that agent’s identity.An action’s observation depends on its prefix.
  • Contributions: The paper introduces four anonymity notions by combining K-step and infinite-step requirements with strong and weak anonymous projections.These notions characterize different limitations on an intruder’s ability to infer system states.
  • Contributions: Verification uses concurrent compositions of automata and observers, with separate constructions for strong and weak anonymous projections.The methodology provides verifiable necessary and sufficient conditions for the four notions and computes upper bounds on K for strong and weak K-step anonymity.
  • System model: The system model is a nondeterministic finite-state automaton with observable and unobservable events, and delayed state estimates track possible earlier states.The event set is partitioned into observable and unobservable events, while delayed estimates quantify states compatible with an observation.

III. FOUR TYPES OF K- AND INFINITE-STEP ANONYMITY UNDER THE STRONG/WEAK ANONYMOUS PROJECTION

Strong anonymity maps all anonymous events to one common observation, whereas K-step and infinite-step requirements constrain singleton state estimates over bounded or unrestricted observational histories. The paper illustrates verification with a system satisfying both strong forms.

  • Strong anonymous projection: An ideal anonymous processor gives every anonymous event the identical observation γ, preventing an intruder from distinguishing those events or their agents.Non-anonymous observable events remain unchanged, and unobservable events produce no observation.
  • Strong anonymity definitions: K-step strong anonymity requires every delayed state estimate up to K observational steps before the current instant to contain more than one state.Infinite-step strong anonymity removes the bound on the observational suffix.
  • Example: For the example system, 0-step delayed estimates after observations γ and γc are {2, 3} and {4, 5, 6}, respectively.Both estimates are nonsingletons.
  • Example: The same system has 1-step delayed estimates {0, 1} after γ and {2, 3} after γc.The example reports that all estimates with |β| ≤ 1 are nonsingletons, establishing 1-step strong anonymity.
  • Example: The example also satisfies infinite-step strong anonymity because every delayed state estimate remains nonsingleton regardless of K.Thus, an intruder cannot determine whether the system is in a singleton state at any instant.

B. K- and infinite-step weak anonymity

Weak anonymity models a non-ideal processor whose anonymous-event labels depend on first-appearance order, making verification more detailed than under strong anonymity. The paper relates weak anonymity to strong anonymity and existing anonymity notions.

  • Weak anonymous projection: A non-ideal anonymous processor labels an anonymous event according to its order of first appearance in the string.Observable non-anonymous events remain unchanged, while unobservable events remain unobserved.
  • Weak anonymity definitions: K-step weak anonymity requires delayed state estimates to contain more than one state for observations no more than K steps before the current instant.Infinite-step weak anonymity removes the bound on the observation suffix.
  • Example: The example system is not 0-step weakly anonymous because Pw(bb) = γ1γ1 yields the singleton delayed estimate {2}.The intruder can therefore determine the current state in that observation case.
  • Relationships: Strong K-step or infinite-step anonymity implies the corresponding weak anonymity, but the converse does not follow from the definitions.When Γ is empty, both proposed projection-based notions reduce to existing anonymity notions, including current-state anonymity at K = 0.

IV. VERIFICATION OF ANONYMITY USING CONCURRENT COMPOSITIONS

The paper verifies K-step and infinite-step strong anonymity by constructing modified observers, variant automata, and concurrent compositions. A necessary-and-sufficient condition reduces verification to checking whether a reachable composition state has an empty adjoint-state component.

  • Observer and automaton construction: The modified observer differs from the standard observer only in its initial states and tracks non-empty adjoint-state evolution across observations.This supports deciding whether adjoint states exist within K observational steps.
  • Concurrent composition: The concurrent composition synchronizes observable events according to the projection and retains unobservable events from the first automaton as composition events.Its transition rules combine synchronized transitions with asynchronous unobservable transitions.
  • Concurrent composition: The verification composition pairs the variant automaton Gm, whose states are all initial, with the modified observer Obsm(G) under the strong anonymous projection Pstr.Composition states encode an actual system state and its corresponding adjoint state set.
  • Verification condition: G is infinite-step, respectively K-step, strongly anonymous if and only if no state of the form (·, ∅) is reachable, respectively reachable within K observational steps.The condition is stated as a necessary and sufficient theorem for the constructed composition.
  • Verification algorithm: The strong-anonymity verification algorithm constructs Obs(G), Obsm(G), Gm, and their concurrent composition before searching for an empty-adjoint-state composition state.The procedure uses breadth-first search to test reachability, including reachability within K observational steps.
  • Complexity: The overall time complexity for verifying K-step and infinite-step strong anonymity is O((|Σo||Σuo| + |Σ|)|X|22|X|).The paper reports that this complexity is lower than that of a modified two-way observer method.

5 else

The verification procedure constructs Gm, Obsm(G), and their concurrent composition, then searches for reachable empty-adjoint-state configurations. In the example, none exists, so infinite-step and every-K K-step strong anonymity hold.

  • 5 else: The procedure constructs the modified observer Obsm(G), the variant automaton Gm, and their concurrent composition Cc(Gm, Obsm(G)).These constructions precede the reachability test.
  • 5 else: Breadth-first search tests whether a state of the form (·, ∅) is reachable, including within K observational steps when required.The search result determines the corresponding anonymity verdict.
  • 5 else: In the example, no reachable state of the form (·, ∅) exists, so G satisfies infinite-step strong anonymity and K-step strong anonymity for every K.The verification result agrees with the conclusion reported for the earlier example.

B. Verification of K- and infinite-step weak anonymity

Weak-anonymity verification augments the system to preserve anonymous-event history, constructs variant observers and automata, and checks a concurrent composition for empty-state reachability. The resulting condition is necessary and sufficient, with an explicit verification complexity.

  • Weak anonymous projections require an augmented automaton that records anonymous-event occurrences together with their location indices.
  • The augmented automaton replaces anonymous events with indexed symbols and preserves their projected language under P_n.
  • The observer for the augmented automaton uses reachable state sets and weak unobservable reach to track possible system states.
  • A variant observer and variant automaton are combined through concurrent composition to verify weak anonymity.
  • Weak anonymity holds exactly when no state of the form (·, ∅) is reachable, either without a step bound or within K observational steps.
  • The proposed algorithm computes the augmented structures and concurrent composition before testing reachability, with the overall complexity given explicitly in the paper.The stated overall time complexity is O((2|Σuo|(|Γ|+|Σo\Γ|)+ (|Γ|2 + |Σo\Γ| + |Σuo|))| b X|22| b X|).

2 Construct the observer d

The observer-construction step determines whether a reachable observer state is a singleton.

  • If a reachable observer state xobs satisfies |xobs| = 1, the construction proceeds to the next verification step.

6 else

The verification algorithm constructs the weak variant structures and uses breadth-first search to test whether an empty adjoint-state component is reachable. Concurrent composition also avoids rebuilding a K-dependent two-way observer.

  • The algorithm constructs the variant automaton and its concurrent composition with the variant observer.
  • Breadth-first search checks whether a state of the form (·, ∅) is reachable from the concurrent composition’s initial states within the relevant observational bound.
  • In the example, an initial state (2b1, ∅) makes the system fail K-step weak anonymity for every K and therefore also infinite-step weak anonymity.
  • The concurrent-composition information structure is independent of K, unlike the two-way observer approach, which requires a new construction for each K.
  • When Γ = ∅, strong and weak K-step or infinite-step anonymity reduce to the corresponding ordinary anonymity notions.

A. Maximal K for K-step strong/weak anonymity

The maximal admissible K is obtained from the shortest exposure distance in the strong or weak concurrent composition. If no empty-state is reachable, the system satisfies infinite-step anonymity; otherwise the maximal K is one less than that distance when positive.

  • The minimum strong or weak exposure distance is the smallest K that violates the corresponding K-step anonymity property.
  • The algorithm searches each corresponding concurrent composition for a reachable state of the form (·, ∅).
  • If no such state is reachable, the algorithm outputs ∞, indicating infinite-step strong or weak anonymity.
  • If the minimum exposure distance is zero, the algorithm outputs NA because no maximal K exists.
  • If the minimum exposure distance is positive, the maximal K is ks −1 for strong anonymity or kw −1 for weak anonymity.

4 else

The paper establishes upper bounds on K for strong and weak K-step anonymity, showing when larger-step verification adds no new behavior. These bounds also support a practical stopping point for concurrent-composition analysis.

  • Verification procedure: The proposed verification procedure uses breadth-first search to examine the constructed concurrent compositions.The proof connects the finite state-space bound to the depth needed for verification.
  • Meaning of the bound: The upper bound K̄ is the maximum depth that the corresponding concurrent composition needs to examine.Beyond K̄, the composition generates no new state absent from paths of length at most K̄.
  • Meaning of the bound: For every L greater than K̄, L-step strong or weak anonymity has the same truth value as anonymity at K̄ steps.Thus, satisfaction or violation at the bound persists for all larger step limits.
  • Practical significance: The bound can guide dynamic security strategies by switching from high-cost active defense to lower-cost maintenance after K̄ observational steps.The paper illustrates this idea with virtual-machine migration and side-channel defense.
  • Upper bounds on K: |X| · 2|X| and |b X| · 2|b X| are upper bounds for strong and weak K-step anonymity, respectively.Infinite-step strong or weak anonymity is equivalent to anonymity checked at these bounded step values.

VI. A CASE STUDY ON A SIMPLE ANONYMOUS QUESTIONING PROCESS

A modeled anonymous questioning process demonstrates the verification method under strong and weak anonymous projections. The system is reported to satisfy infinite-step anonymity under both projection types, despite different observational capabilities.

  • System model: The case study models an anonymous questioning process involving an initial review stage and sequential questioning by consultants.Consultants M and N perform the initial review, while consultants A–G question company Q.
  • Observation model: Company Q cannot distinguish actions performed by different consultants when anonymous processors provide ideal concealment.The example assigns anonymous processors to consultants A, B, C, D, and F, while some questioning devices lack sensors.
  • Strong anonymous projection: The system is K-step strongly anonymous for every K, and therefore infinite-step strongly anonymous under the strong anonymous projection.For K = 1, the delayed estimate after the first observed γ is {A, B, C, E}.
  • Weak anonymous projection: Under the weaker anonymous projection, computation finds that the modeled system satisfies infinite-step weak anonymity.Company Q cannot infer any precise consultant’s identity even with future information under the less powerful processing assumption.

VII. CONCLUDING REMARKS

The paper concludes that concurrent compositions verify the four anonymity notions and provide upper bounds on K, while retaining applicability to natural-projection anonymity and opacity. It also identifies computational limits for large systems.

  • Relation to prior notions: When Γ = ∅, the strong and weak anonymous projections reduce to the natural projection, distinguishing these notions from existing anonymity and opacity concepts when anonymous events are present.The paper states that the four proposed notions are essentially different because they account for strong and weak anonymous projections.
  • Contributions: The concurrent-composition methodology verifies K- and infinite-step anonymity under weak anonymous projections and obtains upper bounds for strong and weak K-step anonymity.The methodology is also described as applicable to K- and infinite-step opacity or anonymity under natural projection.
  • Computational complexity: Verification of the four anonymity notions is PSPACE-hard, making polynomial-time verification unlikely unless P=PSPACE.The paper links this complexity to the close relationship between K/infinite-step anonymity and opacity.
  • Limitations and future work: Exponential verifier state spaces and memory growth from breadth-first search create state-explosion challenges for large-scale practical systems.The paper proposes future work on abstraction-refinement, machine learning, and over-approximation state estimation.
Loading 2609.01192v1…