Dowling and Paterson just wrote one. But it seems to require changes to the protocol. https://eprint.iacr.org/2018/080
-
-
Replying to @matthew_d_green @BenLaurie
That change (extra msg): is it a proof convenience only, or is it also necessary for achieving the desired properties?
1 reply 0 retweets 1 like -
Replying to @tobycmurray @BenLaurie
Who knows? My experience is that a broken proof often implies an attack.
2 replies 0 retweets 5 likes -
Ok, looking more closely I’d bet there’s a hack that would get you a proof of the original protocol. Maybe. But who knows.
1 reply 1 retweet 3 likes -
Replying to @matthew_d_green @BenLaurie
Thanks. Paul van Oorschot & I have been talking about this “who knows” issue. The theorem itself doesn’t help to figure it out, although the internal arguments of the proof might shed light. Hard for outsiders to weigh proof’s value when these changes are made
1 reply 0 retweets 0 likes -
Replying to @tobycmurray @BenLaurie
The general idea is that you want to analyze the key exchange and record protocol separately. But when protocols (like TLS and WireGuard) use record session keys in the key exchange, it screws all that up. Makes analysis that much harder.
2 replies 0 retweets 3 likes -
You can probably still do an ACCE proof of the whole thing but it’s annoying. An interesting problem would be to design a protocol that’s “secure” in one model but somehow interestingly broken in the other. Don’t know if that’s possible.
2 replies 0 retweets 2 likes -
ACCE, or even another model that supersedes that; ACCE was mostly made for TLS 1.2 and some work has to be done to wrestle it free from that context. Treat this all as impetus for the methods and techniques to catch up.
1 reply 0 retweets 0 likes -
The reason the methods and techniques keep having to “catch up” is that people keep writing protocols without writing a reduction proof. So we keep having to make new custom definitions that fit to the idiosyncrasies of the protocol rather than the other way around.
2 replies 0 retweets 4 likes -
Replying to @matthew_d_green @EdgeSecurity and
Writing a definition fit to TLS 1.2 is bad but at least understandable because TLS predates a lot of the formal analysis and is widespread. WireGuard was a green field.
1 reply 0 retweets 0 likes
Which is why we pushed things forward by providing a protocol that is possible to implement in an easily secure manner. Defense in depth matters. Now it's time for the methods to come around to modern protocol development. There's progress to be made in several fields at once.
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.