Abstract
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.
Supplemental Material
- M. Abadi and A. Gordon. A calculus for cryptographic protocols: the spi calculus, 1997.Google Scholar
- C. Baier and M. Kwiatkowska. Domain equations for probabilistic processes. Mathematical Structure in Computer Science, 1999. Google ScholarDigital Library
- C. H. Bennett and S. J. Wiesner. Communication via one-and twoparticle operators on einstein-podolsky-rosen states. Physical Review Letters, 69(20):2881--2884, 1992.Google ScholarCross Ref
- C. H. Bennett, G. Brassard, C. Crepeau, R. Jozsa, A. Peres, and W.Wootters. Teleporting an unknown quantum state via dual classical and epr channels. Physical Review Letters, 70:1895--1899, 1993.Google ScholarCross Ref
- Y. Feng, R. Duan, Z. Ji, and M. Ying. Probabilistic bisimulations for quantum processes. Information and Computation, 205(11):1608--1639, 2007. Google ScholarDigital Library
- S. J. Gay and R. Nagarajan. Communicating quantum processes. In J. Palsberg and M. Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 145--157, 2005. Google ScholarDigital Library
- L. K. Grover. Quantum mechanics helps in searching for a needle in a haystack. Physical Review Letters, 78(2):325, 1997.Google ScholarCross Ref
- M. Hennessy. A proof system for communicating processes with value-passing. Formal Aspects of Computer Science, 3:346--366, 1991.Google ScholarDigital Library
- M. Hennessy and A. Ingólfsdóttir. A theory of communicating processes value-passing. Information and Computation, 107(2):202--236, 1993. Google ScholarDigital Library
- P. Jorrand and M. Lalire. Toward a quantum process algebra. In P. Selinger, editor, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, page 111, 2004. Google ScholarDigital Library
- K. Kraus. States, Effects and Operations: Fundamental Notions of Quantum Theory. Springer, Berlin, 1983.Google Scholar
- M. Lalire. Relations among quantum processes: Bisimilarity and congruence. Mathematical Structures in Computer Science, 16(3): 407--428, 2006. Google ScholarDigital Library
- R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts i and ii. Information and Computation, 100:1--77, 1992.Google ScholarDigital Library
- M. Nielsen and I. Chuang. Quantum computation and quantum information. Cambridge university press, 2000. Google ScholarDigital Library
- P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527--586, 2004. Google ScholarDigital Library
- P. W. Shor. Algorithms for quantum computation: discrete log and factoring. In Proceedings of the 35th IEEE FOCS, pages 124--134, 1994. Google ScholarDigital Library
- J. von Neumann. Mathematical Foundations of Quantum Mechanics. Princeton University Press, Princeton, NJ, 1955.Google Scholar
- M. Ying, Y. Feng, R. Duan, and Z. Ji. An algebra of quantum processes. ACM Transactions on Computational Logic (TOCL), 10 :1--36, 2009. Google ScholarDigital Library
Index Terms
- Bisimulation for quantum processes
Recommendations
Communicating quantum processes
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and ...
Bisimulation for Quantum Processes
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 ...
An algebra of quantum processes
We introduce an algebra qCCS of pure quantum processes in which communications by moving quantum states physically are allowed and computations are modeled by super-operators, but no classical data is explicitly involved. An operational semantics of ...
Comments