Formalization of Quantum Protocols using Coq

Jaap Boender
(Middlesex University)
Florian Kammüller
(Middlesex University)
Rajagopal Nagarajan
(Middlesex University)

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.

In Chris Heunen, Peter Selinger and Jamie Vicary: Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015), Oxford, U.K., July 15-17, 2015, Electronic Proceedings in Theoretical Computer Science 195, pp. 71–83.
Published: 4th November 2015.

ArXived at: https://dx.doi.org/10.4204/EPTCS.195.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org