In this talk, we present a unified formal model of the WireGuard protocol in the symbolic model. Using the automatic cryptographic protocol verifiers SAPIC+, PROVERIF and TAMARIN, we conduct a thorough security assessment of the protocol with regard to an adversary that can read or set static, ephemeral or pre-shared keys, read or set ecdh pre-computations and control key distribution. We consider a complete protocol execution, including cookie messages used for resistance against denial of service attacks. Our analysis determines the minimal security guarantees required for each security property to be held. We present our results in a unified and interpretable way that allows comparisons with previous analyses. We also confirm a flaw in the anonymity of the communications and highlight an implementation choice that considerably weakens the protocol’s security. Lastly, we propose remediation with provably secure fixes for the weaknesses we found.