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.
-
-
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
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.
1 reply 0 retweets 0 likes -
Replying to @matthew_d_green
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 --1 reply 0 retweets 0 likes -
-- it provides the first computational confirmations, as well as pointing to the need to improve the computational proof toolkit to handle new Noise-based protocols. Hopefully it will be motivation for people to further develop ACCE model into something nicer and more complete.
1 reply 0 retweets 0 likes -
Replying to @EdgeSecurity @CasCremers
I’d be happy to hash that out with
@CasCremers. Would be a good panel topic! I think symbolic proofs aren’t sufficient. But to actually back this up I’m curious if there are any examples (even contrived ones) where a broken protocol survives one analysis but not the other.1 reply 0 retweets 0 likes
Symbolic models may have advanced considerably since you last looked at what kind of reasoning they're capable of. Either way, this "symbolic vs computational" battle seems to be one of those hot and contested issues. I'd enjoy listening to that panel discussion.
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.