So wait, NDSS accepted and published an entire new VPN protocol with no security analysis?
We did the Tamarin analysis (whose source code is open source, actually) to provide these proofs, which I liked earlier in this thread. Also, as mentioned earlier, the modified protocol is "morally equivalent" to the actual protocol.
-
-
Tamarin “proofs” just rule out certain classes of attack. They don’t prove security based on some reduction to a hard problem. It’s a good start but not sufficient.
-
I'm sure
@CasCremers wouldn't be happy to hear hear symbolic proofs are "not sufficient". But in either case, I agree that having computational proofs is a nice additional verification. Which is why this new paper is useful and important -- - 3 more replies
New conversation -
-
-
The modified protocol is nothing more than a theoretical exercise for the purpose of their proof -- it would not work in the real world with WireGuard's reduced state machine and UDP -- but it is still useful to do eCK proofs on the modified protocol, to then argue similarity.
-
I’d argue it kind of sucks. If WireGuard was one message away from a formal reduction proof, it would have been much better to finalize the protocol with that message.
- 1 more reply
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.