  We establish fundamental and general techniques for formal verification of
quantum protocols. Quantum protocols are novel communication schemes involving
the use of quantum-mechanical phenomena for representation, storage and
transmission of data. As opposed to quantum computers, quantum communication
systems can and have been implemented using present-day technology; therefore,
the ability to model and analyse such systems rigorously is of primary
importance.
  While current analyses of quantum protocols use a traditional mathematical
approach and require considerable understanding of the underlying physics, we
argue that automated verification techniques provide an elegant alternative. We
demonstrate these techniques through the use of PRISM, a probabilistic
model-checking tool. Our approach is conceptually simpler than existing proofs,
and allows us to disambiguate protocol definitions and assess their properties.
It also facilitates detailed analyses of actual implemented systems. We
illustrate our techniques by modelling a selection of quantum protocols (namely
superdense coding, quantum teleportation, and quantum error correction) and
verifying their basic correctness properties. Our results provide a foundation
for further work on modelling and analysing larger systems such as those used
for quantum cryptography, in which basic protocols are used as components.
