  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.
