  This paper discusses the use of computer-aided verification as a practical
means for analysing quantum information systems; specifically, the BB84
protocol for quantum key distribution is examined using this method. This
protocol has been shown to be unconditionally secure against all attacks in an
information-theoretic setting, but the relevant security proof requires a
thorough understanding of the formalism of quantum mechanics and is not easily
adaptable to practical scenarios. Our approach is based on probabilistic
model-checking; we have used the PRISM model-checker to show that, as the
number of qubits transmitted in BB84 is increased, the equivocation of the
eavesdropper with respect to the channel decreases exponentially. We have also
shown that the probability of detecting the presence of an eavesdropper
increases exponentially with the number of qubits. The results presented here
are a testament to the effectiveness of the model-checking approach for systems
where analytical solutions may not be possible or plausible.
