So wait, NDSS accepted and published an entire new VPN protocol with no security analysis?
-
-
Replying to @matthew_d_green
Don't be ridiculous. When I asked Kenny and Ben what they meant by "no rigorous analysis has been done to date", they responded that what they meant is no computational proof has been done, but they were certainly aware of the Tamarin symbolic proofs that were done.
1 reply 1 retweet 3 likes -
Replying to @EdgeSecurity @matthew_d_green
There appears to be some kind of rivalry between computational people and symbolic people in the formal analysis community. Anyway, here are two papers prior to this recent one: https://www.wireguard.com/papers/wireguard-formal-verification.pdf … https://www.wireguard.com/papers/wireguard.pdf …
2 replies 0 retweets 1 like -
Replying to @EdgeSecurity
So the Tamarin analysis is something, but it’s not in the NDSS paper. Still seems like a strange accept.
1 reply 0 retweets 3 likes -
Replying to @matthew_d_green
Maybe a strange accept? Probably not a strange accept? There's quite a bit of security analysis threaded throughout the NDSS paper (wireguard.pdf earlier in this thread). And with these new papers, we're receiving additional proofs of the protocol's cryptographic soundness.
1 reply 0 retweets 1 like -
Replying to @EdgeSecurity
There’s no proof in the paper. There are a few arguments. That’s not enough. And the new proof seems to require protocol changes.
2 replies 0 retweets 3 likes -
Replying to @matthew_d_green
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.
2 replies 0 retweets 0 likes -
Replying to @EdgeSecurity @matthew_d_green
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.
1 reply 0 retweets 0 likes -
Replying to @EdgeSecurity
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 reply 0 retweets 0 likes
Except that would destroy important other properties of the protocol. Doing the confirmation on the transport layer is _very important_ - a feature. See here: https://lists.zx2c4.com/pipermail/wireguard/2018-January/002333.html … Computational techniques simply need to catch up to what these modern Noise-based protocols need.
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.