So wait, NDSS accepted and published an entire new VPN protocol with no security analysis?
-
-
Replying to @matthew_d_green
There are arguments in the original paper, the Tamarin analysis and it's based on existing protocols, . Or are you saying Tamarin proof doesn't count, or that the other NDSS protocol analyses without eCK-equivalent models are also bad?
2 replies 1 retweet 2 likes -
Replying to @lvh
I’m saying Tamarin analyses are not the same as a formal proof.
2 replies 0 retweets 0 likes -
Replying to @matthew_d_green @lvh
They're both formal. Dowling and Paterson did a computational proof. Tamarin provides symbolic proofs. You evidently don't like symbolic proofs. Many beg to differ.
2 replies 0 retweets 0 likes -
Replying to @EdgeSecurity @lvh
There is a real difference between the two concepts. You understand that just because something includes the word “proof” it doesn’t imply the same thing. Right?
2 replies 0 retweets 1 like -
Symbolic provers argue that there’s no combination of allowed manipulations that yields an attack. It does not prove that those allowed manipulations are the only ones.
1 reply 0 retweets 2 likes -
Replying to @matthew_d_green @lvh
Yes, I'm well aware of the differences between symbolic and computational proofs. Like you said earlier, the debate about their respective roles would make an interesting panel discussion, as clearly academia possesses a wide variety of opinions on the matter.
1 reply 0 retweets 0 likes
Either way, I do certainly look forward to additional proofs -- both computational and symbolic -- of WireGuard and of Noise. I know that folks are looking into that.
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.