Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Quantum Bisimulation-Based Acceleration Method for Quantum Cryptographic Protocol Verification

Min Guan, Juan Xu, Lei Jian

Published Jan 1, 2026• 1 citation
Publisher
DOI
10.1007/978-981-95-6206-0_19

Related papers

Automated Symbolic Verification of Quantum Cryptographic Protocols

Rolando Trujillo-Rasúa, Jesse Laeuchli, Reynaldo Gil-Pons

Lecture notes in computer science•Jan 1, 2026•0 citations

Semi-automated verification of security proofs of quantum cryptographic protocols

Takahiro Kubota, Yoshihiko Kakutani, Go Kato +2 more

Journal of Symbolic Computation•Jun 14, 2015•24 citations

Quantum Safety: How Do We Know? Formal Verification of Cryptographic Protocols

Ilias Cherkaoui

•Oct 27, 2026•0 citations

Toward Automatic Verification of Quantum Cryptographic Protocols

Yuan Feng, Mingsheng Ying

Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.

arXiv:1507.05278•Leibniz international proceedings in informatics•Jan 1, 2015•14 citations

Bisimulation for Quantum Processes

Yuan Feng, Runyao Duan, Mingsheng Ying

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit more faults than classical protocol designers since human intuition is poorly adapted to the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. An important issue in quantum process algebra is to discover a quantum generalization of bisimulation preserved by various process constructs, in particular, parallel composition, where one of the major differences between classical and quantum systems, namely quantum entanglement, is present. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communication is involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communication) scheme, where classical communication must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communication is crucial for process algebra approach to verification of quantum cryptographic protocols. In this article we introduce novel notions of strong bisimulation and weak bisimulation for quantum processes, and prove that they are congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communication are present. We also establish some basic algebraic laws for these bisimulations. In particular, we show the uniqueness of the solutions to recursive equations of quantum processes, which proves useful in verifying complex quantum protocols. To capture the idea that a quantum process approximately implements its specification, and provide techniques and tools for approximate reasoning, a quantified version of strong bisimulation, which defines for each pair of quantum processes a bisimulation-based distance characterizing the extent to which they are strongly bisimilar, is also introduced.

ACM Transactions on Programming Languages and Systems•Dec 1, 2012•31 citations

Bisimulation for quantum processes

Yuan Feng, Runyao Duan, Mingsheng Ying

Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit much more faults than classical protocol designers since human intuition is much better adapted to the classical world than the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. One of the most serious issues in quantum process algebra is to discover a quantum generalization of the notion of bisimulation, which lies in a central position in process algebra, preserved by parallel composition in the presence of quantum entanglement, which has no counterpart in classical computation. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communications are involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communications) scheme, where classical communications must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communications is crucial for process algebra approach to verification of quantum cryptographic protocols. In this paper we introduce a novel notion of bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.

ACM SIGPLAN Notices•Jan 24, 2011•23 citations
Several quantum process algebras have been proposed and successfully applied in verification of quantum cryptographic protocols. All of the bisimulations proposed so far for quantum processes in these process algebras are state-based, implying that they only compare individual quantum states, but not a combination of them. This paper remedies this problem by introducing a novel notion of distribution-based bisimulation for quantum processes. We further propose an approximate version of this bisimulation that enables us to prove more sophisticated security properties of quantum protocols which cannot be verified using the previous bisimulations. In particular, we prove that the quantum key distribution protocol BB84 is sound and (asymptotically) secure against the intercept-resend attacks by showing that the BB84 protocol, when executed with such an attacker concurrently, is approximately bisimilar to an ideal protocol, whose soundness and security are obviously guaranteed, with at most an exponentially decreasing gap.
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit more faults than classical protocol designers since human intuition is poorly adapted to the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. An important issue in quantum process algebra is to discover a quantum generalization of bisimulation preserved by various process constructs, in particular, parallel composition, where one of the major differences between classical and quantum systems, namely quantum entanglement, is present. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communication is involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communication) scheme, where classical communication must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communication is crucial for process algebra approach to verification of quantum cryptographic protocols. In this article we introduce novel notions of strong bisimulation and weak bisimulation for quantum processes, and prove that they are congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communication are present. We also establish some basic algebraic laws for these bisimulations. In particular, we show the uniqueness of the solutions to recursive equations of quantum processes, which proves useful in verifying complex quantum protocols. To capture the idea that a quantum process approximately implements its specification, and provide techniques and tools for approximate reasoning, a quantified version of strong bisimulation, which defines for each pair of quantum processes a bisimulation-based distance characterizing the extent to which they are strongly bisimilar, is also introduced.
Quantum cryptographic systems have been commercially available, with a striking advantage over classical systems that their security and ability to detect the presence of eavesdropping are provable based on the principles of quantum mechanics. On the other hand, quantum protocol designers may commit much more faults than classical protocol designers since human intuition is much better adapted to the classical world than the quantum world. To offer formal techniques for modeling and verification of quantum protocols, several quantum extensions of process algebra have been proposed. One of the most serious issues in quantum process algebra is to discover a quantum generalization of the notion of bisimulation, which lies in a central position in process algebra, preserved by parallel composition in the presence of quantum entanglement, which has no counterpart in classical computation. Quite a few versions of bisimulation have been defined for quantum processes in the literature, but in the best case they are only proved to be preserved by parallel composition of purely quantum processes where no classical communications are involved. Many quantum cryptographic protocols, however, employ the LOCC (Local Operations and Classical Communications) scheme, where classical communications must be explicitly specified. So, a notion of bisimulation preserved by parallel composition in the circumstance of both classical and quantum communications is crucial for process algebra approach to verification of quantum cryptographic protocols. In this paper we introduce a novel notion of bisimulation for quantum processes and prove that it is congruent with respect to various process algebra combinators including parallel composition even when both classical and quantum communications are present. We also establish some basic algebraic laws for this bisimulation. In particular, we prove uniqueness of the solutions to recursive equations of quantum processes, which provides a powerful proof technique for verifying complex quantum protocols.