We will report on work-in-progress on developing a model-checking tool for quantum communication protocols and quantum cryptographic protocols. Our early experiments with probabilistic model checking will be reviewed; then the general model-checking problem for quantum protocols will be formalised and its complexity discussed. This will naturally lead to the question of which protocols can be efficiently simulated on a classical computer. An overview of the stabilizer formalism will be given, followed by a summary of the Aaronson-Gottesman algorithm for simulation of stabilizer circuits. We will present QMC, a tool for automatically verifying properties of such circuits; properties of protocols are expressed using a subset of EQPL, a logic developed by Mateus and Sernadas. This is joint work with Rajagopal Nagarajan (University of Warwick) and Simon Gay (University of Glasgow)