Quantum cryptography represents a novel cryptographic paradigm aimed at resisting attacks posed by quantum computing. Prior to the practical deployment of quantum cryptographic protocols, rigorous security verification is essential. However, existing verification approaches have not effectively addressed the state space explosion problem under eavesdropping scenarios. In response, this paper proposes two key innovations. First, we extend classical bisimulation theory to the quantum domain. In this extension, atomic propositions evolve from classical logical descriptors of state properties to quantum state assertions based on density operators. Additionally, we introduce a classification mechanism for the density operators associated with the state nodes of quantum Markov chains. Second, we construct a quantum Markov chain model that explicitly incorporates eavesdropping behaviors. In this model, the traditional binary termination states are replaced with quantum measurement outcomes, enabling a more effective partitioning of bisimulation equivalence classes. As a result, our method achieves efficient compression of the state space under eavesdropping conditions. This approach is applicable to protocols that can be modeled as quantum Markov chains. For simplicity, we validate the proposed method on the BB84 protocol. Experimental results demonstrate that, in the case of BB84 verification, the number of states and transitions is reduced by 17% and 18%, respectively. During the model checking phase, evaluation across multiple logical formulas shows that analysis time is reduced by at least 17%, and memory consumption is decreased by no less than 11%.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Quantum Bisimulation-Based Acceleration Method for Quantum Cryptographic Protocol Verification

  • Min Guan,
  • Juan Xu,
  • Jian Lei

摘要

Quantum cryptography represents a novel cryptographic paradigm aimed at resisting attacks posed by quantum computing. Prior to the practical deployment of quantum cryptographic protocols, rigorous security verification is essential. However, existing verification approaches have not effectively addressed the state space explosion problem under eavesdropping scenarios. In response, this paper proposes two key innovations. First, we extend classical bisimulation theory to the quantum domain. In this extension, atomic propositions evolve from classical logical descriptors of state properties to quantum state assertions based on density operators. Additionally, we introduce a classification mechanism for the density operators associated with the state nodes of quantum Markov chains. Second, we construct a quantum Markov chain model that explicitly incorporates eavesdropping behaviors. In this model, the traditional binary termination states are replaced with quantum measurement outcomes, enabling a more effective partitioning of bisimulation equivalence classes. As a result, our method achieves efficient compression of the state space under eavesdropping conditions. This approach is applicable to protocols that can be modeled as quantum Markov chains. For simplicity, we validate the proposed method on the BB84 protocol. Experimental results demonstrate that, in the case of BB84 verification, the number of states and transitions is reduced by 17% and 18%, respectively. During the model checking phase, evaluation across multiple logical formulas shows that analysis time is reduced by at least 17%, and memory consumption is decreased by no less than 11%.