Falling through the KRACKs
blog.cryptographyengineering.com
blog.cryptographyengineering.com
This, to me, is one of the biggest problems facing our industry. In first year undergraduate in engineering we learn how to design a state machine. We learn to design one before we learned OOP and circuits and assembly. Yet, how many APIs or Protocols have you come across or has your organization developed where there isn't a state machine described somewhere. It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it. We programmers sometimes spend far too much time juggling stuff in our heads and communicating with coworkers in a wonderful game of workplace telephone. If the state machine has become too complex, then we have lost all hope to fully manage it and must accept the risks. Some things just shouldn't be risked!
Additionally, in my years of working as a contractor, I can tell you that nearly 1 in 1,000 companies (+ or - 1) care about security. Management simply does not value it, and everyone already thinks your product "should have been done yesterday." The entire world runs on insecure products. From banks, to healthcare, to universities. I can list every one of those who has put admin credentials in a publicly, internet accessible text file. (But they'll do silly things like insanely unmemorizable passwords like 23ix2n5 that get written down as postit notes and as files on desktops, and disable RDP copy-and-paste but leave RDP hard drive support.)
We're going to continue seeing these blunders day after day until people start going to jail for losing data.
I guess this is fine for throwaway acquihire SaaS stuff, but it's becoming a serious problem for stuff that's meant to be widely used.
I'll wait.
I think one of the causes is that a lot of CS is taught top-down and not bottom-up, so things like flowcharts, state diagrams, and other similar visual aids are completely skipped in preference to more abstract thinking. I wonder if at least some of this aversion is directly related to the "gotophobia" that started with Dijkstra's famous paper.
It may seem difficult and tedious, but this is how you engineer something rather than merely 'develop' it.
As someone who learned the "old school" way of planning out your code --- yes, even drawing flowcharts and state diagrams --- before writing a single line of it, I can assuredly say that it should be a natural and completely pleasant process; what's "difficult and tedious" is trying to debug and coerce something you (or someone else) wrote without planning into working correctly.
Over the years coworkers have been puzzled at why I spend "so much time" flowcharting and just thinking before writing even a single line of code --- only to try adopting the same method once they realise how much time it saves in total, since all the cases have already been accounted for and the only thing left to do is test out any of the few remaining and often trivial bugs introduced during the design->code process.
For some people (like me) thinking through problems with pen and paper is a tool.
For others I guess it is annoying: look at him, now he's doing this wannabe software architect stuff again.
Same might go the other way: here he goes again, trying to prove his programming super skills by jumping into it without even the smalles amount of planning.
For me it is not very visual when I code. It is more a gut feeling: this goes here, that goes there. This is good, bad, weird but works etc.
This is nice for me but I know I have to work on how to explain it to others.
Bad example but I guess this is somewhat closer to what I want to be able to explain: "it currently works but it is a bad idea because it means you'll have to remember to patch seemingly unrelated functions x, y and z whenever you update this.
Also, in this case it is even worse as in the worst case you won't see the errors until the quarterly reporting run and that code is well known for having bad test coverage."
Edit: as usual I'm curious as to why parent was downvoted?
Seemed relevant to point out that at least for me it’s not.
I enjoy both diagramming and early exploratory coding.
I have real problems when one of my (really smart) colleagues wants to discuss some code we have neither written nor diagrammed yet.
For her however that seems to be the natural way of doing it and when we started working together I had to point out that just didn't work for me.
It seems to me that knowing and being aware and accepting of the different learning styles can solve a number of problems in teams.
This problem goes away once you gain some experience - both in writing specs and in programming.
Think of it this way: do engineers build bridges without design documents and diagrams? No. So why are you writing software without them? If you aren't familiar with the problem domain, fine, do it the agile way. But once you gain experience there is no excuse to not thinking problems through in advance before trying to solve them.
Documents are cheaper to create and easier to change than bridges. Code is just another kind of document.
I've a sneaking suspicion that bridge building would look more like software if we could drive over AutoCAD models. (Or that software would look more like bridge building if we were still compiling by hand).
EDIT: I should add that I certainly do write and communicate documents about "what business problem does this even solve" and "what does it do" and "what are the major components and what are they responsible for" and "did you consider X alternative design" but planning down to the level of function signatures has usually turned out to be a waste of time.
We don't build our "bridges", our compilers/interpreters do.
That really depends on the type of code you are writting.
Writing code going into a space craft, or Nuclear Power Plant, or Encryption code that can be relied on by people to protect their actual life, or code going into a medical device or.... you get the picture
Yes if your writing code going into the next Pokemon time waste game sure you can be fast and lose, but to not presume all code is the same.
In this instance, code is going into devices that historically do not get updated properly, I think that warrants taking a more "bridge building" approach and less "Code is just a document" approach
The more important code is, the more I want to see it subjected to a realistic and comprehensive test suite, careful peer review, etc. Although you're right, I ultimately work on backend systems that can cause some downtime at worst, not industrial process control or crypto libraries. I also have the luxury of doing continuous delivery, incremental rollouts, feature flags, staging environments with shadow traffic, etc. so there are a lot of safeguards standing between a mistake and widespread impact.
Why on earth would you want bridge construction to be more like software engineering? Bridges work. We know how to build them bug free, every time. We don't know how to make working, bug-free software. There's even an old, not very funny joke about exactly this comparison. (Spoiler: it doesn't flatter the code monkeys.)
You might want to look up the Cynefin model[1]. Bridges are complicated, software is complex. This supports your bent towards experimentation, sort of; when solutions are unknown, that's required. But documentation and planning are part of what turns complex in to complicated, and that's a big part of the trick to successfully delivering big chunks of relatively bug-free code.
As will the need for planning beforehand.
Also, flowcharts are less readable than most programming languages in non-trivial cases. Graphical programming languages are mostly useful as DSLs. Text is unbeatable in the general case.
The developers insisted on all behaviour being specified and documented before they would start coding. Of course, a truly exacting specification is equivalent to code. So the users who had been tasked with describing the required functionality ended up inventing their own DSL and “coding” the entire system in Microsoft Word.
Needless to say, they were the only ones who understood the spec. IT cried foul. Business cried “this is what you asked for!”
Cue months of arguments over what constituted a proper spec, during which the users essentially taught themselves how to code. The software eventually ended up being written by transliterating the DSL into actual code.
It worked, but remains to this day an unmaintainable mess.
Congratulations!
You see that "X hours ago" to the right of the username? Yeah, click that...
But it's a good tip nonetheless. Once you click the "x minutes/hours/days ago" link, besides bookmarking the resulting URL in your browser or elsewhere, you also have a few more options that show up at the top of the comment page. One of them is to "favorite" the comment. You can also favorite a submission in a similar way.
Just be advised that your favorite submissions and comments lists are public.
I totally agree that this is an example of insane, hidden functionality. How could anyone know that "click timestamp" = "view details"? Makes no sense.
However, seemingly every site/app has adopted this, from Twitter to Facebook to several PM services.
Why not acknowledge that this is a problem and just add a little "Permalink" link, which some sites used to have? Or at least a permalink icon?
Surely the combined design talent of Google, Facebook, and Twitter can solve this problem better.
A hypertext system that doesn't treat links as slightly opaque, explaining them in detail wherever they appear, sounds unpleasant to me.
I guess you could probably modify most such systems to have a flashing popup on every link that said "There is more information available if you click on the text here!!!!".
The question is: is it a worse mess than if you'd have started without the spec? My intuition says "no", and the experience the users gained regarding formal thinking is a huge net benefit that will be an asset for years to come.
Essentially the same problem, just on a higher level of abstraction.
Oh, and failing to document DSLs is really a common mistake: No docs, no spec, no helpful error messages, and so on. Just like the very early parsers or compilers. But DSLs are really the most important thing to document, as these are so much harder to get into ... the "simpler" parts of the program are usually readable and understandable with less effort, even with pure code and no docs at all.
What's wrong with demanding to document a DSL?
That is, the DSL as a language is still much simpler (fewer data types, fewer elements, fewer rules, etc.) than the whole application, which is built using that DSL.
So I'd expect the DSL's documentation to be short and targeted at the people writing within that DSL.
If the DSL's documentation is more complicated than the original problem (spec), it failed at its purpose.
BTW, ultimately you have a chain of languages, such as:
Spec <- DSL <- Meta-DSL <- ... <- programing language
So, take this with a grain of salt.
I can't code without a diagram. I make a diagram and process the logic. I make lots of sub diagrams. I make notes and ask myself a lot of questions. I'll also ask other people, if I can.
I can't do it. I can't program 'on the fly.' My attempts have resulted in horrible results, not even qualified to be called results. If I don't process the logic, pretty much from start to finish, I can't do it. I use a notation system that isn't even a real programming language and leave lots of room to cram more stuff in and make corrections.
Most of this is past tense, I don't do much anymore. I'm retired and my efforts are just little automation tasks for my own needs.
Anyhow, I figured I'd offer another perspective/opinion. I envy you if you can do it off the cuff. I've tried, I can't.
I have coded on-the-fly and I have coded from diagram first approaches.
on-the-fly works for me when there is an obvious data structure to work to, otherwise it takes a lot longer than planning it out because of all the edge cases
So my tip here is if you want to learn how to do it on the fly you should start with small steps by reducing the amount of stuff you need to see in a paper before start coding. In the other hand it's perfectly normal and there is no problem in doing what you do.
In other words, how would you express in code: "state Z can only be entered through either state W or X, but not through state Y", or "state V must be followed by state W, but only after condition A"? Sure, you can write a switch statement. But half the rules of a state machine can only be implemented by omission (i.e. by not coding it, instead of hardcoding the requirements).
But then the changes start and now I either discard the diagrams or accept that I have two things to maintain. Generally I take the former path because divergence from the plan is almost inevitable on anything that's alive.
That must be the origin of all the useful but unofficial SVG ones I'd seen :)
Beurdouche et al., "A Messy State of the Union: Taming the Composite State Machines of TLS"
From the abstract: "mplementations of the Transport Layer Security (TLS) protocol must handle a variety of protocol versions and extensions, authentication modes and key exchange methods, where each combination may prescribe a different message sequence between the client and the server. We address the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes. We systematically test popular open-source TLS implementations for state machine bugs and discover several critical security vulnerabilities that have lain hidden in these libraries for years ..."
Based on this work you might say that there are formal state machines for TLS, but they aren't in the standard.
I shared the LTSA model with a few others at the time, but no-one else seemed very interested in doing anything with it.
https://www.doc.ic.ac.uk/ltsa/
https://tools.ietf.org/html/rfc4340
Edit: I dug through my old backups, and I think this is probably the model I used:
http://nrg.cs.ucl.ac.uk/mjh/dccp.lts
It's nothing fancy, but my point is that even simple modelling can spot errors that a whole standards group of smart people miss.
Don't agile approaches encourage this, focusing on features and things that can cleanly be assigned story points at the expense of a bigger picture, with velocity being the focus?
If the spec is not wrong, careful planning is probably better than high velocity iteration.
I think cryptography is a good example of this--would you develop a cryptographic API on which people's lives might depend iteratively through a release early and fail often method? I hope not.
In a lot of software development, especially large scale enterprise software (where you're trying to map a complex set of existing business practices and workflows into software) and embedded software (where you have to write something that provides fixed, well-understood functionality running on hardware with a months- or years-long iteration time) you do have a complete and correct spec (or at least the means to generate one). In these cases a less ad-hoc approach than Agile can be beneficial.
Let's reflect: iterative design is popular in software engineering because software usually suits it. Changes are easily iterable, you can often roll changes back, there's relatively low cost to cloning changes across millions of instances, code's design lifetime is relatively short, etc. In contrast, 'real world' engineering (civil, heavy mechanical) favours FEED because the cost of change rapidly and prohibitively rises with time, so nailing down the scope and structure early is critical, there's long procurement times for changes, the design lifetime of the finished product is measured in decades, etc.
The rub is that there's a small niche of software design, such as protocol design like this, or certain firmware scenarios, which far more closely resembles the latter even though it's usually done by a community used to and trained in the former. Although it's for different reasons, all the things that make FEED appropriate for 'real world' engineering also apply to these sorts of software tasks, but software engineering as a whole doesn't appear to[2] focus on teaching and supporting the necessary tools and techniques for performing that process well.
Flip that on its head, and it's why software companies quickly begin to run rings around companies traditionally focused on hardware once software starts to play a bigger part and the limitations stopping iterative design from working begin to disappear. Software engineering largely biases towards iteration (understandably) and when it works it allows for good advantages. But in embracing those advantages, software engineering as a discipline has begun to lose an understanding of FEED and the careful methodology it delivers.
[1]: https://en.wikipedia.org/wiki/Front-end_engineering & https://en.wikipedia.org/wiki/Front-end_loading
[2] I admit I've not done a CS/SE degree, but I've gone through a couple of subjects run online and I talk to friends who did do it and that's the feel I get. Besides, just look at HN's generally trending articles.
edit: With all I wrote, I don't mean to undermine the extremely good work that the devs designing these protocols, etc. almost always perform. It's far beyond my ability. I am speaking more in a general sense about how Soft. Eng. seems to have thrown out the baby with the bathwater in declaring agile philosophies as 'the best way'. My feel is that the pendulum seems to have swung too far past 'best' towards becoming 'only'.
Totally right.
Here is what the paper actually says:
The 802.11i amendment does not contain a formal state machine describing how the supplicant must implement the 4-way handshake. ... Fortunately, 802.11r ... does provide a detailed state machine of the supplicant.
The problem, as I understand it, was that when the protocol was formally verified, the properties checked were only the escape of the private key and identity related issues. The property of the nonce never being reset was simply not considered.
The missing piece, then, wasn't a precise description of how the system works, but rather a precise list of what it's supposed to guarantee. Without a clear and concise description of the requirements, it's hard to verify that the system satisfies them. Alternatively, it's possible that the list of guarantees was complete, in which case reviewers should have noticed that no nonce reset isn't one of them, yet it's required for the security of certain communication protocols used over the channel.
The first result for "802.11i" is the Wiki page for IEEE 802.11i-2004, which mentions that it's incorporated into 802.11-2007, and if you search for "802.11-2007", the first result at the top (after the amusing calculation that 802.11 - 2007 = -1 204.89) is the PDF of the full standard.
...and I'm not even a security researcher. But I agree with the rest of the criticism of the IEEE and the 802.11 standard in particular, once you've acquired it.
One of my pasttimes is seeking out and reading standards for protocols, file formats, and other things; and so I've seen quite a few. As an overall impression: IETF's are very readable, most of the ITU ones are pretty good if somewhat terse, ANSIs and IEEEs vary widely between "a little bit of effort" and "I feel like my brain is melting if I read more than a paragraph an hour", and 3GPPs along with BlueTooth are very much in the "take a 10 minute break to digest after every sentence or two" category. 802.11 is also like that. The acronym density in that document is one of the highest I've ever seen.
Maybe KRACK will at least make them consider editing their standards and formatting them to be somewhat less of a chore to understand; things like https://files.catbox.moe/xym9dq.PNG should really be put into tables.
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 other words, it's getting better, but vendors are burning silicon by the time researchers have the time to even crack open whitepapers -- too late.
What I was able to understand so far is that the use of a particular nonce is being forced on the client and given that invariant keystream one can decrypt known messages. I'm still fuzzy on how the attacker can force this step.
EDIT: Further question, isn't timestamp synchronization taken into account here when invalidating a nonce? What happens when I disconnect from wifi to a mobile network and back to the wifi?
The attacker couldn't just MitM the protocol on layer 3 as it cannot authenticate with the WiFi router. Of course, the attacker already could just pretend to be the wifi router and then forward and inspect all traffic to the internet. What is scary here is that it breaks into a Local network as opposed to the internet.
Suppose the real AP is on channel 1. The attacker is nearer the victim than the AP, and is on channel 6. The attacker repeats on channel 6 everything the AP sends on channel 1, and repeats on channel 1 everything the victim sends on channel 6. The victim sees the same AP on both channels, channel 1 and channel 6 (the attacker modifies the part of the AP beacon/responses which says "I'm on channel X"), which is a perfectly legitimate and normal thing, and chooses channel 6 because it has a stronger signal.
Since now the attacker is in the middle, it can modify anything. Change the AP beacon to say "I'm on channel 6", drop any packet it wants, duplicate any packet it wants, and so on.
> What happens when I disconnect from wifi to a mobile network and back to the wifi?
The wifi negotiation starts from scratch, with a new step 1.
So really this is blocking step #4 from occurring, pedantic perhaps, but it's sort of important.
2) In response to "How can someone block step #4?" Since we're discussing Wifi then signal jamming seems apt. From the actual paper discussing krack: "Inspired by this observation, an adversary could also selectively jam message 4 ..." There's much literature here (google). The reference the KRACK paper provides is: "Mathy Vanhoef and Frank Piessens. 2014. Advanced Wi-Fi attacks using commodity hardware. In ACSAC" link here: [https://people.cs.kuleuven.be/~mathy.vanhoef/papers/acsac201...]
"And separately, to answer a question: how did this attack slip through, despite the fact that the 802.11i handshake was formally proven secure?"
Implies that the formal verification failed.
Yet from the paper on the attack:
"Interestingly, our attacks do not violate the security properties proven in formal analysis of the 4-way and group key handshake."
This is a good thing! One of the hard things for software developers to do is separate the theorem (spec) from the proof (implementation). I can see how the article author would posit such a question.
The paper answers the question.
What do we do about it? More theorems, modelling, and proofs. Research on synthesizing the implementation from its specification. Treat events like this as we treat auto-collisions and correct the processes, tools, and technology that enable attacks like this to occur in our systems... at least that's my 0.02. :)
Bingo.
A pay-for-play standards development organization should charge to _participate_ in the standards-setting activity, and NOT charge the public for access to the standards.
The ITU-T seems to have learned this, at least as to some things (e.g., the ASN.1 family of standards, such as x.680 and x.690). The IEEE should do the same.
Better yet, they should look at the IETF model, which has been working for _decades_. In the IETF model there is no charge at all, except for attending physical meetings. Mailing list participation is free. RFC publication is free. The IETF is financed via meeting fees and donations. Vendors have an interest in the IETF staying afloat, so they see to it -- their interest is, of course, the IETF's overall low cost to them (by comparison to OASIS, IEEE, ANSI/ISO, or the ITU-T), and the amount of review their specifications get.
Maybe 802.x dev should move to the IETF lock stock and barrel, you might say, but there is a problem: the IETF doesn't have a lot of expertise with physical layer protocol specifications. _Most_ IETF participants are at layer 2 and up. Of course, this can be fixed by... just moving all the 802.x work (and the people working on it) to the IETF.
EDIT: Mind you, getting the work done at the IETF would not be a guarantee of no such bugs. It would address the procedural and public access problems TFA talks about. But that alone is a huge improvement over using the IEEE for highly consequential specifications that greatly affect the public.
Also, that program only allows access to the latest release of each standard. Which means that, when there's a new release of a standard, access to any version of it is closed for six months.
I think this will only work against android/linux clients, since in that case the attacker actually knows the key, and can perform a proper MITM.
In that video, because HSTS isn't used on match.com (unfortunate), the browser doesn't attempt to make an HTTPS connection at first. Obviously, if you have control of that TCP connection, you can do whatever you want. The browser is oblivious to HTTPS existing.
Also, be careful not to confuse the layers here. The encryption algorithms in WPA2 are completely unrelated to TLS/HTTPS. TLS is... somewhere in the OSI model, but it's well above WPA2/packet handling, and TLS can/does work with a compromised network.
(somebody let me know if I'm wrong in this)
So while there are VPNs with great security, you have to make sure your VPN is not vulnerable to common MITM attacks. So choose your VPN which has been well vetted. I'm a fan of OpenVPN due to it being able to pass as HTTPS traffic, but a popular recommendation is algo which is IKEv2 based IPSec VPN.
There is ongoing work to produce AEAD cipher modes that do not fall apart when {key, nonce} pairs are reused (for different message plaintexts, naturally).
Crypto is tricky...
It's easy enough to construct AEAD cipher modes by generic composition that don't have this problem. For example, the Kerberos enctypes don't.
The key is to construct AEAD cipher modes that are efficient (Kerberos' add a block's worth (16 bytes) of "confounder" to each message, bloating it, and also adds a block's worth of cipher operation, slowing it down) and don't require additional random numbers if at all possible (those confounders in Kerberos are random numbers prepended to the plaintext). Also, Kerberos' enctypes use HMAC for the integrity protection part, which is not a very fast MAC.
He is also able to modify this traffic and serve compromised pages.
The attacker needs to have a stronger signal than the legitimate access point. So he has to stand pretty close to the victim, physically.
In practice, as long as you only trust data received through TLS, you should be fine.
The only situation where trust in the router would be relevant to me is for communication within a local network, so I'm controlling every device involved. And there, this attack might actually be harmful, as far as I understand.
Which is the case for the vast majority of wifi users.
It is completely irrelevant how any of us here consider their access point. The problem is that the masses could be subject to these attacks and allows propagating malwares and botnets.
As the post says, they thought about the individual components, but failed (or maybe it is just too difficult) to define the security considering composability of schemes. This is a clear limitation of modern cryptography.
Great post!
https://www.theguardian.com/world/2013/sep/05/nsa-gchq-encry...
"$250m-a-year US program works covertly with tech companies to insert weaknesses into products"
"The documents show that the agency has already achieved another of the goals laid out in the budget request: to influence the international standards upon which encryption systems rely." [emphasis mine]
Now compare with the details from KRACK regarding Android and Linux:
https://www.krackattacks.com/#details-android
"Our attack is especially catastrophic against version 2.4 and above of wpa_supplicant, a Wi-Fi client commonly used on Linux. Here, the client will install an all-zero encryption key instead of reinstalling the real key. This vulnerability appears to be caused by a remark in the Wi-Fi standard that suggests to clear the encryption key from memory once it has been installed for the first time." [emphasis mine]
Sometimes adding an innocent-appearing remark, and later acting on it would be all that's needed for a rich and mighty adversary.
I don't claim it happened this time, but I worry when the possibility isn't being considered and properly investigated.
The attacker impersonates an existing AP and forces the client to reuse IVs / reset the encryption key to zero (in the case of wpa_supplicant), and is able to decrypt traffic that way.
From what I understand the credentials won't matter. Anyone else more knowledgeable please correct me if I'm wrong, but the attack goes something like this:
1. Capture trafic that includes the 4-way handshake
2. replay message #3 of the handshake
3. client's encryption key is set to zero (in the case of wpa_supplicant), and nonce/IV are reused going forward
4. you are now in control of the encryption key being used (again, only wpa_supplicant) so you can go ahead and MITM the victim's DNS queries, capture cookies, etc...
The Details section of the researcher's site explains it pretty well:
https://www.krackattacks.com/#details
Lastly, the most urgent task for mitigating this is to patch client devices as quickly as possible.
Android's fractured vendor-specific distributions and lack of long-term support for the low-mid level models is going to make this a difficult/impossible task...
Note that our attacks do not recover the password of the Wi-Fi network. They also do not recover (any parts of) the fresh encryption key that is negotiated during the 4-way handshake.
The initial authorization/pre-shared keys are used to negotiate and share session keys. It is the negotiation of these session keys that is attacked, leading to insecure session keys being used. The initial auth parts of the handshake are not being abused here, only steps 3/4 of the 4-way handshake.
So, even by impersonating an AP you don't get the user's password.
None of these work when taken in isolation and given to actual people to work with.
So, which way is it?
The layman answer that is formal verification should've been done on those systems after integration. I'm not sure how much that would've helped though, since the proofs for each of those was complex enough. And then actual code written tends to sway far away from what protocol implementers (also crypto folks) think it should look like.
So I'd say more formal verification, but also make it easier and accessible for normal developers without a Math PhD. And verification of actual code would be ideal.
Something I've come across recently is formal verification of cryptographic implementations not on paper (i.e. mathematically) but in plain C using tools and languages developed recently.
For example, a three part series on how SAW and Crytol were used to formally verify s2n (AWS's TLS lib):
https://galois.com/blog/2016/09/verifying-s2n-hmac-with-saw/
https://galois.com/blog/2016/09/specifying-hmac-in-cryptol/
https://galois.com/blog/2016/09/proving-program-equivalence-...
PS(A) for the adventurous: I've also come across a github repo that lists related stuff
Because you are awful at programming, and security, and these things will help you. Sure, they won't be enough, but to think they are anything other than minimum requirements for security is being incredibly arrogant and deluded.
As programmers we are always somewhere in the middle :)
Here's how the fourth last paragraph starts:
> The critical problem is that while people looked closely at the two components — handshake and encryption protocol — in isolation, apparently nobody looked closely at the two components as they were connected together.
And yet, there are still regular posts here about whether static type systems have any merit at all... never mind advanced things like linear/dependent types, theorem provers, TLA+, etc. Just use Go!
The article seems to imply there's nothing wrong with the proof or the statement of the properties to be proved, it's about integration with another component. But if "don't reuse nonces" is a standard security property to verify, then I would think that that is a hole in the verification.
Could someone shed more light on this?
> The 4-way handshake was mathematically proven as secure. How is your attack possible?
> The brief answer is that the formal proof does not assure a key is installed once. Instead, it only assures the negotiated key remains secret, and that handshake messages cannot be forged.
That is the reason why we have/had WEP, WPA, WPA2 to allow a local infrastructure to have the very same trust like physical cables.
it is true, as the responders point out, that some of the control protocols used in the internet blindly trust what they receive. fixing those protocols and ensuring reasonable end to end authentication is a much better use of time than fussing around about a single link level solution.
imagine being able to forget about half assed measures like policy based firewalls and stateful nat for security.
Worse: IoTs generally have no firmware/software update cycles, so vulnerabilities like this one are forever.
My plan is to build tiny one-device wifi/wired bridges for all my IoT devices that have wired ethernet. For the other IoT devices the plan is to update or replace them. What's yours?