Cryptographic tools can often become adopted even when their security proofs lack mathematical rigour - or altogether missing.
Are there famous cases of security breaches in the industry, where the underlying cryptography was (up until then) considered secure?
The SSH protocol has a complicated record format with an encrypted message length, variable padding, encrypt-and-MAC, etc. This complicated system, which was designed without any formal analysis relating the security of the system to the security of the building blocks, turned out to be vulnerable to an attack (paywall-free) exploiting the MAC verification as an oracle for information about the plaintext, leading to plaintext recovery attacks on SSH in popular implementations like OpenSSH.
The SSL/TLS protocols have a long and sordid history of informal design, leading to a multitude of attacks:
The OpenPGP protocol was designed by the ad hoc '90s-style composition of generic and poorly-understood public-key encryption and signature building blocks with no formal treatment for how they fit together.
The original promise of ‘Pretty Good Privacy’ was to keep email private. But the method for combining fancy math primitives like RSA and standard symmetric cryptography like AES to encrypt long messages in OpenPGP was designed without formal analysis relating them to the security of the building blocks.
And it turned out this method was exploitable in practice in real email clients in an attack dubbed EFAIL that can leak message content (my answer on it). It took a decade and a half after the problem was first reported in theory in 2002 for the OpenPGP world to catch up when an attack was published in practice in 2018.
A secondary promise of PGP was to prevent forgery in private email. But there is no formal concept of a message from Alice to Bob—only of an encrypted message to Bob, and a signed message from Alice, nested however you please*…and usually nested in a way that Charlie can take a message Alice sent to him and make it look to Bob like Alice had sent it to Bob instead. Alice can, of course, take the extra step to name the recipient in the message, and Bob can take the extra step to check for his name. The software could also do this. The OpenPGP designers could have tried to formalize the human-relevant interactions and analyzed their security properties—and could have designed the cryptography to support human use.
But, when confronted with the problem, instead the OpenPGP designers abdicated that responsibility by asserting that cryptography cannot solve the problem of appropriate use of technology. To this day the OpenPGP protocol doesn't have a formal concept of a message from Alice to Bob—which could be implemented by standard well-understood public-key authenticated encryption—even though it is nominally intended for private email.
The public-key encryption and signature schemes chosen in OpenPGP were themselves designed without any formal analysis relating them to well-studied hard problems like the RSA problem or the discrete log problem, and it turned out that both the particular Elgamal signature scheme and RSA encryption scheme used by OpenPGP were problematic.
It is unclear to me whether these led to practical exploits on OpenPGP—except perhaps for the implementation error in GnuPG of using the same per-message secret for Elgamal signature and encryption, which illustrates the danger of proving a protocol secure without proving the code implements the protocol correctly.
These attacks are all on protocols that were designed by ad hoc engineering without formal analysis guaranteeing the security of the protocol relative to the security of its building blocks. But the primitive building blocks—like $x^3 \bmod{pq}$, cubing modulo a product of secret primes; like $g^x \bmod p$, exponentiation of a standard base modulo a safe prime; like the AES-256 permutation family; like the Keccak permutation—don't have formal analysis guaranteeing their security relative to anything. What gives?
The formal analysis or provable security for protocols, which consists of theorems relating security of a protocol to security of its building blocks, is only one part of a global sociological system for getting confidence in security of cryptography:
The reason we suspect the RSA problem is hard is that some of the smartest cryptanalysts on the planet have had strong motivation to study it for decades, and they have left a track record of decades of failure to find any way to break (say) RSA-2048 at cost less than $2^{100}$ per key. The same goes for discrete logs in certain groups, for AES-256, etc.
The formal analysis of a protocol using RSA and AES enables the cryptanalysts to focus their effort so they don't have to waste time studying SSH, studying OpenPGP, studying SSLv3, studying TLS, studying WPA, etc., to find whether there's some way to break those protocols. If the formal analysis is done well enough, the cryptanalysts can spend their effort on a small number of primitives, and the more effort they spend failing to break those primitives, the more confidence we have in the primitives and everything built on them.
Protocols like SSH, OpenPGP, SSL/TLS, etc., without formal analysis, are a colossal waste by society of the world's supply of cryptanalysts. Formal analysis enables much more efficient use of the world's resources—and it would have paid off, because nearly all of the above attacks could have been caught just by studying the security properties of the protocols involved and the security contracts of the building blocks: CBC in TLS with predictable IVs, public-key encryption in PGP failing the IND-CCA standard, RSA-based encryption schemes in PGP and TLS without a reduction to RSA security, representing one's error responses in SSH and TLS as oracles for a chosen-ciphertext adversary.
Not all protocols are easy to formally analyze once designed—like the trainwreck that was TLS renegotiation—but protocols can be designed out of well-understood composable parts with clear security contracts to facilitate formal analysis, instead of ad hoc agglomerations of crypto gadgets like the '90s, and today there are tools like the Noise protocol framework with the Noise explorer to compose protocols with built-in formal analysis.
* Sometimes infinitely nested!
When choosing curves for use in elliptic curve cryptography, some have suggested using various classes of curves which avoid certain "bad" properties which would make the system vulnerable to attack.
The MOV attack breaks the ECDSA on a class called supersingular curves. To avoid this, some suggested using curves from another class called anomalous curves, which are guaranteed to not be supersingular.
However it was then found that these curves suffer from an arguably worse flaw exploited by Smart's attack, which also breaks the ECDSA.
I don't know if anyone acted on the suggestion to use these in the meantime, but it demonstrates that very subtle mathematical properties of elliptic curves can have a massive impact on the system as a whole, and that not understanding these properties sufficiently well can have serious consequences.
I'm surprised that nobody has mentioned the Dual EC DRBG backdoor.
In short, there was an issue with a specific random number generator, because it was shown that by chosing specific initial parameters the possibility of a backdoor existed.
As a key part of a campaign to embed encryption software that it could crack into widely used computer products, the U.S. National Security Agency arranged a secret $10 million contract with RSA, one of the most influential firms in the computer security industry… RSA’s contract made Dual Elliptic Curve the default option for producing random numbers in the RSA toolkit.
After the Snowden leaks it's now presumed to be true that the NSA indeed had a backdoor implemented and thus could break the security.
Important: The possibility of a backdoor was published before the Snowden leaks.
I think this was in hindsight certainly foolish of people to assume that it was still a secure algorithm even after showing mathematically that a backdoor could theoretically exist.
For more informations:
Note that even where an algorithm is proven "correct" (that is to say, where the algorithm is proven to have certain well-defined properties), there may still be flaws in the implementation: the implementation is likely to rely on underlying hardware and software that almost certainly has not been subject to the same level of mathematical scrutiny. So you get flaws such as Meltdown and Sceptre, whereby execution of an algorithm leaves discoverable traces of its internal variables. Any mathematical proof of a security algorithm is almost certainly going to rely on assumptions that the implementation at that level is flawless.
Early WiFI protocols (WEP) had too far small of an IV. Plugging in known data rates, and analyzing the protocol would have told them this.
The MIFARE Classic is a type of contactless smart card used for many applications such as transit fare collection, tolling, loyalty cards, and more.
NXP, the creator of these cards, used a proprietary security protocol Crypto-1 to secure them.
Wikipedia quotes that "the security of this cipher is ... close to zero".
These cards in the field today are known to be easily crackable with the right equipment and very insecure.
Although this is a dramatic example, Crypto-1 was probably never widely considered secure, as it was a proprietary, closed source cipher. Despite that, these card had very wide circulation and are still in the field today.
