Significant progress within the area of symbolic verification of cryptographic protocols has made it possible to formally analyze the security of several large-scale internet protocols, such as TLS 1.3, 5G-AKA, EMV, and Apple iMessage. Notably, these verification results can be reproduced and scrutinized by simply downloading the protocol specification and checking it with a fully-automated protocol verification tool, such as Tamarin. By contrast, the symbolic analysis of quantum security protocols remains a challenge even for relative simple quantum protocols like BB84. In this article, we introduce a symbolic model that quantum protocol designers can use to formally verify their protocols with the verification tool Tamarin. We provide symbolic interpretations of various quantum operations, such as entanglement and measurement, and communication protocols, such as teleportation and superdense coding. We illustrate the strengths and limitations of our symbolic model by specifying and formally verifying two prominent quantum protocols.