From: blipp@mailbox.org
To: wireguard@lists.zx2c4.com
Subject: Mechanised cryptographic proof of the WireGuard protocol
Date: Tue, 16 Apr 2019 18:25:50 +0200 (CEST) [thread overview]
Message-ID: <1676414122.33317.1555431950456@office.mailbox.org> (raw)
Dear all,
With Bruno Blanchet and Karthik Bhargavan from the Prosecco research group at Inria Paris, we continued working on our mechanised cryptographic proof of the WireGuard protocol since my master's thesis was finished last year.
I am happy to say that a paper we wrote about our work was accepted at this year's EuroS&P conference [1]. A long version of the paper is as of now available at https://hal.inria.fr/hal-02100345, and the code and the models at https://cryptoverif.inria.fr/WireGuard.
Differences to my master's thesis that is linked at the moment on WireGuard's formal verification page https://www.wireguard.com/formal-verification/ under the headline “Computational Proof of Protocol in ACCE Model” include:
- We now use a precise model of the elliptic curve group Curve25519. This removes the gap between our previous proof and what WireGuard actually does, and thus increases confidence in the proof. This is, to the best of our knowledge, the first work that analyses WireGuard with such a precise model.
- We analyse the identity hiding property of WireGuard.
- We analyse the DoS protection provided by the MACs and the cookie message.
- We provide a comparison with 5 other works that analysed WireGuard or the underlying Noise IKpsk2 protocol. This includes symbolic analyses using ProVerif and Tamarin, and a manual cryptographic proof.
If you have questions regarding our work, please reach out, I am happy to explain more details.
Best regards,
Benjamin
[1] https://www.ieee-security.org/TC/EuroSP2019/
--
Research group: https://prosecco.gforge.inria.fr/
Personal website: https://benjaminlipp.de/
_______________________________________________
WireGuard mailing list
WireGuard@lists.zx2c4.com
https://lists.zx2c4.com/mailman/listinfo/wireguard
reply other threads:[~2019-04-16 16:26 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=1676414122.33317.1555431950456@office.mailbox.org \
--to=blipp@mailbox.org \
--cc=wireguard@lists.zx2c4.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).