Current-State Opacity in Safe Partially Observed Quantum Petri Nets: True-Concurrency Semantics and Exact Symbolic Verification

TL;DR

This paper introduces a formal framework for current-state opacity in quantum Petri nets, combining true-concurrency semantics with symbolic verification to improve security analysis in hybrid quantum-classical systems.

Contribution

It formalizes current-state opacity in quantum Petri nets using true-concurrency semantics and develops an exact symbolic verification algorithm with computational efficiency.

Findings

The proposed method accurately evaluates quantum leakage in a case study.

The verification algorithm significantly reduces computational complexity.

The framework preserves classical opacity definitions within quantum contexts.

Abstract

Classical opacity theory for discrete-event systems relies strictly on observable event sequences, fundamentally failing to capture security breaches in hybrid architectures where an attacker exploits both classical traces and localized quantum correlations. To address this gap, we formalize current-state opacity within the framework of safe partially observed quantum Petri nets by introducing a true-concurrency semantics that represents classical observations as partially ordered multisets via unfolding configurations. Building upon this, we define quantitative posterior-state leakage as the trace distance between the attacker's localized quantum states, evaluated conditionally on whether the underlying system has reached a secret or non-secret marking. This formulation strictly preserves classical opacity definitions. To achieve computational tractability, we apply the stabilizer formalism and develop an exact symbolic verification algorithm. By combining targeted unfolding exploration, state aggregation exclusively at maximal unobservable reach, and stabilizer-tableau propagation, this procedure circumvents both concurrent interleaving explosions and exponential density-matrix overhead. Finally, an entanglement-swapping case study validates the exact leakage evaluation, demonstrates substantial computational gains, and establishes a rigorous interface for counterexample-guided leakage enforcement.