Model Checking Quantum Protocols