We analyse the entire WireGuard protocol as it is, including transport data messages, in an ACCE-style model. We contribute proofs for correctness, message secrecy, forward secrecy, mutual authentication, session uniqueness, and resistance against key compromise impersonation, identity mis-binding, and replay attacks. We also discuss the strength of the identity hiding provided by WireGuard.
Our work also provides novel theoretical contributions that are reusable beyond WireGuard. First, we extend CryptoVerif to account for the absence of public key validation in popular Diffie-Hellman groups like Curve25519, which is used in many modern protocols including WireGuard. To our knowledge, this is the first mechanised cryptographic proof for any protocol employing such a precise model. Second, we prove several indifferentiability lemmas that are useful to simplify the proofs for sequences of key derivations.
@INPROCEEDINGS{LippBlanchetBhargavanEuroSP19, AUTHOR = {Benjamin Lipp and Bruno Blanchet and Karthikeyan Bhargavan}, TITLE = {A Mechanised Cryptographic Proof of the {W}ire{G}uard Virtual Private Network Protocol}, BOOKTITLE = {IEEE European Symposium on Security and Privacy (EuroS\&P'19)}, YEAR = 2019, PAGES = {231--246}, MONTH = JUN, ADDRESS = {Stockholm, Sweden}, PUBLISHER = {IEEE Computer Society} }