Abstract
The unifying of qACP and classical ACP under the framework of quantum process configuration 〈p, ρ〉 makes verification for quantum protocols possible, not only the pure quantum protocol, but also protocol that mixes quantum information and classical information. In this paper, we verify the KMB09 protocol by use of quantum process algebra qACP.
Similar content being viewed by others
References
Baeten, J.C.M.: A brief history of process algebra. Theor. Comput. Sci. Process. Algebra 335(2–3), 131–146 (2005)
Milner, R.: Communication and concurrency. Prentice Hall (1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Inf. Comput. 1992(100), 1–77 (1992)
Hoare, C.A.R.: Communicating sequential processes. http://www.usingcsp.com/(1985)
Fokkink, W.: Introduction to Process Algebra, 2nd edn. Springer, Berlin (2007)
Feng, Y., Duan, R.Y., Ji, Z.F., Ying, M.S.: Probabilistic bisimulations for quantum processes. Inf. Comput. 2007(205), 1608–1639 (2007)
Gay, S.J., Nagarajan, R.: Communicating quantum processes. In: Proceedings of the 32nd ACM Symposium on Principles of Programming Languages, Long Beach, pp 145–157. ACM Press, California (2005)
Gay, S.J., Nagarajan, R.: Typechecking communicating quantum processes. Math. Struct. Comput. Sci. 2006(16), 375–406 (2006)
Jorrand, P., Lalire, M.: Toward a quantum process algebra. In: Proceedings of the 1st ACM conference on computing frontiers, pp 111–119. ACM Press, Ischia (2005)
Jorrand, P., Lalire, M.: From quantum physics to programming languages: a process algebraic approach. Lect. Notes Comput. Sci 2005(3566), 1–16 (2005)
Lalire, M.: Relations among quantum processes: Bisimilarity and congruence. Math. Struct. Comput. Sci. 2006(16), 407–428 (2006)
Lalire, M., Jorrand, P.: A process algebraic approach to concurrent and distributed quantum computation: operational semantics. In: Proceedings of the 2nd International Workshop on Quantum Programming Languages, TUCS General Publications, pp. 109–126 (2004)
Ying, M., Feng, Y., Duan, R., Ji, Z.: An algebra of quantum processes. ACM Trans. Comput. Log. 10(3), 1–36 (2009)
Feng, Y., Duan, R., Ying, M.: Bisimulations for quantum processes. In: Proceedings of the 38th ACM Symposium on Principles of Programming Languages (POPL 11), pp 523–534, ACM Press (2011)
Deng, Y., Feng, Y.: Open bisimulation for quantum processes. Manuscript, arXiv:1201.0416 (2012)
Feng, Y., Deng, Y., Ying, M.: Symbolic bisimulation for quantum processes. Manuscript, arXiv:1202.3484 (2012)
Wang, Y.: An Axiomatization for Quantum Processes to Unifying Quantum and Classical Computing. Manuscript, arXiv:1311.2960 (2013)
Wang, Y.: Entanglement in Quantum Process Algebra. Manuscript, arXiv:1404.0665 (2014)
Khan, M.M., Murphy, M., Beige, A.: High error-rate quantum key distribution for long-distance communication. arXiv:0901.3909v4 (2009)
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Dai, G. Formal Verification for KMB09 Protocol. Int J Theor Phys 58, 3651–3657 (2019). https://doi.org/10.1007/s10773-019-04232-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10773-019-04232-2