Communicating Quantum Processes (CQP) is a quantum process calculus that applies
techniques from classical computer science to concurrent and communicating systems that combine quantum and classical computation. By employing the theory of
between processes, it is possible to verify the correctness of a system in CQP. The
of CQP helps us to analyse quantum systems by reducing the need to explicitly construct
relations. We add three new equational axioms to the existing equational theory of CQP, which helps us to analyse various quantum protocols by proving that the implementation and specification are equivalent. We summarise the necessary theory and demonstrate its application in the analysis of quantum secret sharing. Also, we illustrate the approach by verifying other interesting and important practical quantum protocols such as superdense coding, quantum error correction and remote CNOT.