Dynamic Quantum Logic (DQL) has been used as a logical framework for manually proving the correctness of quantum programs. This paper presents an automated approach to quantum program verification at the cost of simplifying DQL to Basic Dynamic Quantum Logic (BDQL). We first formalize quantum states, quantum gates, and projections in bra-ket notation and use a set of laws from quantum mechanics and matrix operations to reason on quantum computation. We then formalize the semantics of BQDL and specify the behavior and desired properties of quantum programs in the scope of BDQL. Formal verification of whether a quantum program satisfies desired properties is conducted automatically through an equational simplification process. We use Maude, a rewriting logic-based specification/programming language, to implement our approach. To demonstrate the effectiveness of our automated approach, we successfully verified the correctness of five quantum protocols: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, and Quantum Gate Teleportation, using our support tool.