Formalization of quantum protocols using Coq. (English) Zbl 1477.68528
Heunen, Chris (ed.) et al., Proceedings of the 12th international workshop on quantum physics and logic, QPL’15, Oxford, UK, July 15–17, 2015. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 195, 71-83 (2015).
Summary: Quantum Information Processing, which is an exciting area of research at the intersection of physics and computer science, has great potential for influencing the future development of information processing systems. The building of practical, general purpose Quantum Computers may be some years into the future. However, Quantum Communication and Quantum Cryptography are well developed. Commercial Quantum Key Distribution systems are easily available and several QKD networks have been built in various parts of the world. The security of the protocols used in these implementations rely on information-theoretic proofs, which may or may not reflect actual system behaviour. Moreover, testing of implementations cannot guarantee the absence of bugs and errors. This paper presents a novel framework for modelling and verifying quantum protocols and their implementations using the proof assistant Coq. We provide a Coq library for quantum bits (qubits), quantum gates, and quantum measurement. As a step towards verifying practical quantum communication and security protocols such as Quantum Key Distribution, we support multiple qubits, communication and entanglement. We illustrate these concepts by modelling the Quantum Teleportation Protocol, which communicates the state of an unknown quantum bit using only a classical channel.
For the entire collection see [Zbl 1434.03015].
For the entire collection see [Zbl 1434.03015].
MSC:
| 68V20 | Formalization of mathematics in connection with theorem provers |
| 68Q12 | Quantum algorithms and complexity in the theory of computing |
| 81P68 | Quantum computation |
References:
| [1] | Ebrahim Ardeshir-Larijani, Simon J. Gay & Rajagopal Nagarajan (2013): Equivalence Checking of Quan-tum Protocols. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’13), Springer LNCS 7795, pp. 478-492. Available at http://dx.doi.org/10.1007/978-3-642-36742-7_33. · Zbl 1381.68144 · doi:10.1007/978-3-642-36742-7_33 |
| [2] | Ebrahim Ardeshir-Larijani, Simon J. Gay & Rajagopal Nagarajan (2014): Verification of Concurrent Quan-tum Protocols by Equivalence Checking. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’14), Springer LNCS 8413, pp. 500-514. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_42. · doi:10.1007/978-3-642-54862-8_42 |
| [3] | C. H. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres & W K Wootters (1993): Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70(13), doi:10.1103/PhysRevLett.70.1895. · Zbl 1051.81505 · doi:10.1103/PhysRevLett.70.1895 |
| [4] | Charles H. Bennett & Gilles Brassard (1984): An Update on Quantum Cryptography. In G. R. Blakley & David Chaum, editors: CRYPTO, Lecture Notes in Computer Science 196, Springer, pp. 475-480. Available at http://dx.doi.org/10.1007/3-540-39568-7_39. · Zbl 1359.81102 · doi:10.1007/3-540-39568-7_39 |
| [5] | Y. Bertot & P. Castéran (2004): Interactive Theorem Proving and Program Development Coq’Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science, Springer, doi:10.1007/978-3-662-07964-5. · Zbl 1069.68095 · doi:10.1007/978-3-662-07964-5 |
| [6] | Cerberis: Layer 2 Link Encryprion with Quantum Key Distribution. Available at http://www.idquantique.com/wordpress/wp-content/uploads/Cerberis-Datasheet.pdf. Retrieved 27.9.2015. |
| [7] | Adam Chlipala (2011): Certified Programming with Dependent Types. MIT Press. Available at http://adam.chlipala.net/cpdt/. http://adam.chlipala.net/cpdt/. · Zbl 1288.68001 |
| [8] | Jacek Chrzaszcz (2003): Implementing Modules in the Coq System. In David A. Basin & Burkhart Wolff, editors: TPHOLs, Lecture Notes in Computer Science 2758, Springer, pp. 270-286. Available at http://dx.doi.org/10.1007/10930755_18. · doi:10.1007/10930755_18 |
| [9] | Th. Coquand & C. Paulin-Mohring (1990): Inductively defined types. In P. Martin-Löf & G. Mints, ed-itors: Proceedings of Colog’88, Lecture Notes in Computer Science 417, Springer-Verlag. Available at http://dx.doi.org/10.1007/3-540-52335-9_47. · Zbl 0722.03006 · doi:10.1007/3-540-52335-9_47 |
| [10] | Luís Cruz-Filipe, Herman Geuvers & Freek Wiedijk (2004): C-CoRN, the Constructive Coq Repository at Nijmegen. In Andrea Asperti, Grzegorz Bancerek & Andrzej Trybulec, edi-tors: MKM, Lecture Notes in Computer Science 3119, Springer, pp. 88-103. Available at http://dx.doi.org/10.1007/978-3-540-27818-4_7. · Zbl 1108.68586 · doi:10.1007/978-3-540-27818-4_7 |
| [11] | Timothy A. S. Davidson (2011): Formal Verification Techniques using Quantum Process Calculus. Ph.D. thesis, University of Warwick. |
| [12] | Yuan Feng, Runyao Duan & Mingsheng Ying (2011): Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages (POPL 2011), ACM, doi:10.1145/1926385.1926446. · Zbl 1284.68425 · doi:10.1145/1926385.1926446 |
| [13] | Yuan Feng, Nengkun Yu & Mingsheng Ying (2012): Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph]. · Zbl 1311.68086 |
| [14] | S. J. Gay & R. Nagarajan (2005): Communicating Quantum Processes. In: POPL’05, ACM, doi:10.1145/1040305.1040318. · Zbl 1369.68207 · doi:10.1145/1040305.1040318 |
| [15] | Simon J. Gay & Rajagopal Nagarajan (2006): Types and typechecking for Communicating Quantum Pro-cesses. Mathematical Structures in Computer Science 16(3), pp. 375-406, doi:10.1017/S0960129506005263. · Zbl 1122.68059 · doi:10.1017/S0960129506005263 |
| [16] | Simon J. Gay, Nikolaos Papanikolaou & Rajagopal Nagarajan (2008): QMC: a model-checker for quantum systems. In: Proceedings of the 20th International Conference on Com-puter Aided Verification (CAV 2008), Springer LNCS 5123, pp. 543-547. Available at http://dx.doi.org/10.1007/978-3-540-70545-1_51. · doi:10.1007/978-3-540-70545-1_51 |
| [17] | Simon J. Gay, Nikolaos Papanikolaou & Rajagopal Nagarajan (2010): Specification and verification of quan-tum protocols. In: Semantic Techniques in Quantum Computation, Cambridge University Press. · Zbl 1196.68135 |
| [18] | Georges Gonthier (2008): Formal proof -the four color theorem. Notices of the American Mathematical Society 55(11), pp. 1382-1393. Available at http://dx.doi.org/10.1007/978-3-540-87827-8_28. · Zbl 1166.68346 · doi:10.1007/978-3-540-87827-8_28 |
| [19] | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013): A Machine-Checked Proof of the Odd Order Theorem. In Sandrine Blazy, Christine Paulin-Mohring & David Pichardie, editors: ITP, Lecture Notes in Computer Science 7998, Springer, pp. 163-179. Available at http://dx.doi.org/10.1007/978-3-642-39634-2. · Zbl 1268.68006 · doi:10.1007/978-3-642-39634-2 |
| [20] | William Howard (1980): The formulae-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 479-490. |
| [21] | INRIA (2013): The Coq Proof Assistant. Available at http://coq.inria.fr/. Accessed on 8.5.2013. |
| [22] | Philippe Jorrand & Marie Lalire (2004): Toward a Quantum Process Algebra. In: 1st ACM Conference on Computing Frontiers, doi:10.1145/977091.977108. · doi:10.1145/977091.977108 |
| [23] | Marie Lalire (2006): Relations among quantum processes: bisimilarity and congruence. Mathematical Struc-tures in Computer Science 16(3), pp. 407-428, doi:10.1017/S096012950600524X. · Zbl 1122.68060 · doi:10.1017/S096012950600524X |
| [24] | Xavier Leroy (2009): Formal verification of a realistic compiler. Communica-tions of the ACM 52(7), pp. 107-115, doi:10.1145/1538788.1538814. Available at http://gallium.inria.fr/ xleroy/publi/compcert-CACM.pdf. · doi:10.1145/1538788.1538814 |
| [25] | MagiQ: Quantum Key Distribution System (Q-Box). Available at http://www.magiqtech.com/Products.html. Retrieved 27.9.2015. |
| [26] | D. Mayers (2001): Unconditional Security in Quantum Cryptography. Journal of the ACM 48(3), pp. 351-406, doi:10.1145/382780.382781. · Zbl 1323.94128 · doi:10.1145/382780.382781 |
| [27] | Robin Milner, Joachim Parrow & David Walker (1992): A Calculus of Mobile Processes, I. Inf. Comput. 100(1), pp. 1-40, doi:10.1016/0890-5401(92)90009-5. · Zbl 0752.68037 · doi:10.1016/0890-5401(92)90009-5 |
| [28] | Michael A. Nielsen & Isaac L. Chuang (2000): Quantum Computation and Quantum Information. Cambridge University Press. · Zbl 1049.81015 |
| [29] | M.E. Peck (2007): Geneva Vote Will Use Quantum Cryptography. IEEE Spectrum. Available at http://spectrum.ieee.org/computing/networks/geneva-vote-will-use-quantum-cryptography. |
| [30] | Quantum-Coq (2014): Coq sources for quantum protocol proofs. Available at https://www.dropbox.com/sh/fhldyg1mfnxdmcl/AAC0T7tWxDrOnt4SZGshOKeua. Shared Dropbox folder, read only -work in progress. |
| [31] | H. de Riedmatten, I. Marcikic, W. Tittel, H. Zbinden, D. Collins & N. Gisin (2004): Long distance quantum teleportation in a quantum relay configuration. Physical Review Letters 92(4), p. 047904, doi:10.1103/PhysRevLett.92.047904. · Zbl 1068.81527 · doi:10.1103/PhysRevLett.92.047904 |
| [32] | Eleanor G. Rieffel & Wolfgang Polak (2000): An introduction to quantum computing for non-physicists. ACM Comput. Surv. 32(3), pp. 300-335. Available at http://doi.acm.org/10.1145/367701.367709. · doi:10.1145/367701.367709 |
| [33] | Mingsheng Ying, Yuan Feng, Runyao Duan & Zhengfeng Ji (2009): An algebra of quantum processes. ACM Transactions on Computational Logic 10(3), p. 19, doi:10.1145/1507244.1507249. · Zbl 1351.68187 · doi:10.1145/1507244.1507249 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
