So like, you could imagine yourself looking at the SSL 3.0 "Finished" message and the SSH "Exchange Hash" and asking yourself, why do the complicated thing? The SSH thing seems to work!
And: if you asked yourself that, like, in 2013, you could go on believing for ten years that everything was fine, and SSH just found a clever way to do handshake integrity less cumbersomely than SSL 3.0.
There's like an obvious lesson here about PGP and the MDC, right?
Not sure that all the readers will already know about our constant quibbling about the security of the MDC. I have in the past suggested that the fact that the MDC has remained unbroken for 20+ years is evidence that it is secure.
Interestingly enough, I have recently stumbled across a paper[1] that shows that preventing an attacker from computing the hash is important for insuring the security of hash than encrypt schemes like the MDC. OpenPGP does that by preseeding the hash with a random, encrypted value.
So does that mean that the MDC is secure? Unfortunately, when you come up with a set of requirements for security, you have to use your knowledge of existing attacks. You don't get to know about about future attacks. So the fact that a particular construct has never been broken over a long time is in a sense the only objective evidence available.
OpenPGP gets a fair amount of academic scrutiny. What is going to change that would allow someone to find a weakness in OCFB-MDC at this late date?
Also, why do you care so much that you bring it up out of nowhere in unrelated contexts?
I don't understand your second question.
This seems like... not a great stance to take on post about a vulnerability that existed for 20+ years.
I don't understand the defensiveness.
This seems unsurprising for me. Formal verification advocates believe it will prevent all issues, but it seemed obvious to me that the verification is still vulnerable to human fallibility in deciding _what_ to verify.
https://ntrs.nasa.gov/api/citations/20000055731/downloads/20...
Uh, if it was that easy. I recently(!) audited a brand new system for deployment in what most nations consider critical infrastructure. They had just updated to the newest firmware supplied by a well-known and established manufacturer in that industry (not some garbage by a small company). That ran a dropbear ssh server version from 2016 with multiple CVEs, including an unauthenticated RCE. So essentially it's a root shell for anyone that can talk IP to that device.
I predict I will start seeing this terrapin in my Nessus reports soon, and stop seeing it when I enter pension.
Strictly speaking audit is the wrong word for what I did (I'm not a certified auditor). I don't want to say too much in case I break some confidentiality agreement. Though I'm curious how that will be argued away, or if they get the manufacturer to get their shit together and build a new firmware...
Two things stand out to me;
1. That the SSH protocol lacked a robust transcript hash all along, this seems like a staggering decision, and even though I'd read the RFCs, I'd never put this together. Turns out it's to allow for injection of messages designed to defeat traffic analysis? Not the right way to do it.
2. The SSH handshake had been formally verified ... and the proofs are still "true". But the researchers found non-obvious gaps between the environmental assumptions for the proofs and what is actually true in the real world. Formal verification is still the most comprehensive and exhaustive form of testing that we have, but gaps can really bite you. It is like relying Pythagoras' theorem for a triangle, but then it turns out that your triangles are on the surface of a sphere, which isn't a plane. The math itself is right, but the environment was different all along.