Why wasn't the KRACK exploit discovered sooner?
The 802.11 specification that describes WPA2 (802.11i) is behind a paywall, and was designed by a few key individuals at the IEEE. The standard was reviewed by engineers, not by cryptographers. The details of the functionality (e.g. retransmission) were not widely known about or studied by security professionals.
Cryptographer Matthew D Green wrote a blog post about this subject, and I think this section sums it up quite nicely:
One of the problems with IEEE is that the standards are highly complex and get made via a closed-door process of private meetings. More importantly, even after the fact, they’re hard for ordinary security researchers to access. Go ahead and google for the IETF TLS or IPSec specifications — you’ll find detailed protocol documentation at the top of your Google results. Now go try to Google for the 802.11i standards. I wish you luck.
The IEEE has been making a few small steps to ease this problem, but they’re hyper-timid incrementalist bullshit. There’s an IEEE program called GET that allows researchers to access certain standards (including 802.11) for free, but only after they’ve been public for six months — coincidentally, about the same time it takes for vendors to bake them irrevocably into their hardware and software.
In some sense, it feels like this should have been obvious.
Remember Heartbleed, Shellshock, POODLE, TLS Triple Handshake attack, "goto fail", ... ?
In hindsight, most of these problems seem to be obvious and could have been prevented if the right people just had a closer look at the right time at the right place. But, there is only a limited amount of people with the right technical expertise and these usually have lots of other things to do too. Please don't expect them to be perfect.
Instead of having illusions about standards being perfectly designed, software being bug free and systems being 100% secure one should accept that this is impossible to achieve in practice for today's complex systems. To mitigate this one should care more about resilience and robustness, i.e. staying safe and secure even if some parts break by layering security, not fully trusting anything and having plans if something breaks.
The paper describing KRACK discusses this very issue in section 6.6.
A couple of points: There were ambiguities in the specification. Also formal proofs of specification are based on a model of the specification, and there are times when that model does not match the actual specification, much less matching the implementations based on that specification.