Live data from Hacker News

Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

krackattacks.com

331–340 of 424 posts

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#331

Earlier quoted context omitted.

We're not mind readers. If he says it's ok, we think it's ok. If other vendors have fucked up months long patch cycles, that's their deal, not ours.

What part of this commit description is "not revealing details"? https://ftp.openbsd.org/pub/OpenBSD/patches/6.1/common/027_n...

and this one ? ctrl+f replay https://www.tedunangst.com/flak/post/openbsd-changes-of-note...

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#332

Earlier quoted context omitted.

I have a HTC 10, a flagship device that's barely a year old the fact that I now have to wait a couple a months for a patch to what is clearly a critical vulnerability is just ridiculous. The fact that anyone without a flagship device should now throw that phone away because it will probably never be patched is despicable. I totally agree with your hope that this will kick both the manufacturers and Google in the butt…

To underline your point, even my Nexus 5 (_from Google_), which is a little less than 3 years old, will never receive security updates. And one of the main reasons I chose the Nexus was to be sure to get updates on time. Except for the security vulnerabilities, everything of the device is totally fine. It's such a waste of resources… (In this case I at least have an alternative in the form of Lineage OS, which will o…

Last I checked, LineageOS for the Nexus 5 is still vulnerable to CVE-2017-9417 (Broadpwn). LineageOS might work for keeping the userspace up-to-date, but their kernels are still largely dependent on the upstream vendors. If the problem is in a firmware blob, as is the case with Broadpwn, you are pretty much guaranteed to be SOL without vendor support.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#333
> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?

So, we cannot trust even formal verification?

> it’s a factual statement. In formal analysis, definitions really, really matter!

If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification?

Update:

> We need machine-assisted verification of protocols, preferably tied to the actual source code that implements them.

Haskell, here is your opportunity :-)

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#334

> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure? So, we cannot trust even formal verification? > it’s a factual statement. In formal analysis, definitions really, really matter! If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification? Update: > We need machine-assisted verific…

Formal verification all the way down.

I'm a complete layman in this field, but mustn't it bump against the Incompleteness Theorem at some point? There's no way to prove your definitions.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#335
post #112

Earlier quoted context omitted.

Pray for a vendor patch. The fix landed today in the hostap repository: https://w1.fi/cgit/hostap/commit/?id=a00e946c1c9a1f9cc65c729...

Does this resolve the issue on the AP side of things? Could I theoretically have an AP update that would resolve this with no need to update clients?

Unfortunately no, from what I understand this is primarily an attack against clients.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#336
post #227

Earlier quoted context omitted.

Seems rather prisoner-dilemma-ish[1]. Up until now, there were no indications that this was being exploited publicly. After a flaw like this gets known (whether through a coordinated disclosure or through OpenBSD's early patch) you can be assured people will be exploiting this. Do you both stay silent and take the minor risk of your users being vulnerable for a short time longer whilst patching and disclosure is bein…

And be sure to note the iterated version which is where things get interesting https://en.wikipedia.org/wiki/Prisoner%27s_dilemma#The_itera... You can already see it in this case, where Theo "defecting" leads to less cooperation in future rounds.

For those who missed the FAQ,

> To avoid this problem in the future, OpenBSD will now receive vulnerability notifications closer to the end of an embargo.

i.e., _explicitly signalling_ that this researcher intends to play "defect" with OpenBSD in future rounds, should future rounds occur.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#337

Matthew Green's blog on why it happened and how it escaped detection is a really good read. https://blog.cryptographyengineering.com/2017/10/16/falling-...

> Representation of the 4-way handshake from the paper by He et al. Yes, I know you’re like “what?“. But that’s why people who do formal verification of protocols don’t have many friends. +1 for a good read, really enjoyed his writing style. For those unfamiliar, Matthew Green is a cryptography researcher and professor at Johns Hopkins. Edit: TIL John's' Hopkins ty /u/dEnigma

It's actually "Johns Hopkins". The story behind the name is somewhat interesting:

http://www.hopkinsmedicine.org/about/history/history1.html

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#338

> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure? So, we cannot trust even formal verification? > it’s a factual statement. In formal analysis, definitions really, really matter! If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification? Update: > We need machine-assisted verific…

> So, we cannot trust even formal verification?

it's explained in the article, 2 unit tests, 0 integration tests. The formal verification appears to prove correctness of the 2 pieces independently, but not of the composition.

> Haskell, here is your opportunity :-)

you're just moving the problem to the correctness of the compiler.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#339
post #309

Earlier quoted context omitted.

Because it hasn't been seen before, it's not likely that it has been exploited. Even after knowing about the flaw for a while, the Wi-Fi Alliance says there is no evidence that this was used maliciously before. https://www.wi-fi.org/news-events/newsroom/wi-fi-alliance-se... We can't know absolutely but with all the attention wifi has gotten since the days of war driving, there's a good chance it would have been caugh…

Yeah, without the alliance stating what methods were used to look for attacks, its hard to take that seriously... it's the same line used in just about any security breach. Is this attack likely to generate log evidence on affected APs in their default configuration, or is it so far down the stack that no evidence is generated and nobody could refute this claim?

Nope, definitely further down the stack. This is part of the protocol that deals with retransmission of lost packets. Nobody logs those.

Re: Key Reinstallation Attacks – Breaking WPA2 by Forcing Nonce Reuse

#340

> how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure? So, we cannot trust even formal verification? > it’s a factual statement. In formal analysis, definitions really, really matter! If lack of definition implies flaws in formal verification, does that mean we need an additional formal verification of formal verification? Update: > We need machine-assisted verific…

Formal verification all the way down. I'm a complete layman in this field, but mustn't it bump against the Incompleteness Theorem at some point? There's no way to prove your definitions.

The critical point is specification vs. implementation. Any difference creates a loophole which can be abused.
Post reply on HN