Are there moderns (post World War II) and famous protocols that were proven secure (in any model: game-based, UC...) but whose proof was wrong and could have led to real-world attacks?

Note that:

• I'm not really concerned about attacks on the mathematical assumptions themself (which seem to be the focus of this thread, and can't be considered as mistakes in the proof: they are "just" unfortunate assumptions). But of course, I'd love to hear about protocols that claimed to be secure as soon as assumption X was true, while in fact they are broken despite the fact that X is not broken.
• By "real world attack", I would prefer attacks that broke protocols used in practice by non-specialist end-users, but I'm also fine with well known protocols that are mostly known and used in the academic world.

Ideally, I'd love to learn if the "mistake" in the proof was really a mistake or is likely to be created on purpose (NSA backdoor...).

EDIT

Could you also be precise, whenever possible, if the attack is due to a mistake in the proof itself, or if the model of security is not appropriately chosen?

Perhaps "Plaintext Recovery Attacks against SSH" qualifies?

Some readers might wonder at this point how we would be able to attack a variant of SSH that was already proven secure in [1]. The basic reason is that, while the authors of [1] recognise that the decryption operation in SSH is not “atomic” and might fail in various ways, their security model does not distinguish between the various modes of failure when reporting errors to the adversary. Moreover, their model does not explicitly take into account the fact that the amount of data needed to complete the decryption operation is itself determined by data that has to be decrypted (the length field). Unfortunately, it seems that real-world cryptographic implementations are more complex than the current security models for SSH handle.

Then see "A Surfeit of SSH Cipher Suites" for a follow up.

Perhaps we can count the first international standard on digital signature, ISO/IEC 9796:1991, which specified RSA and Rabin signature using a redundant padding of the message to sign. Security was justified by a then state-the-art rationale, published in proceedings of Eurocrypt 1990. That states properties of the standard's signature padding necessary for security despite the multiplicative property of the raw RSA function $x\mapsto x^d\bmod n$, like:

• Shifting or complementing representative elements does not result into other ones.
• The natural product of any representative element by any constant other than 1 is not a representative element.

These properties are true. But they do not form a security proof in the modern sense of that. They only prove the impossibility of some attacks, rather than of any attack.

And it was found¹ in 1999 a computationally inexpensive method exhibiting large classes of messages such that the signature of one is found by submitting another (sometime three at first) for RSA signature; or the private key is found (a total break) by submitting two messages for Rabin signature. The standard was withdrawn a year later.

Despite that standard being used in practice, the attack never degenerated to exploitation as far as I know, because applications do not allow obtaining the signature of even a few messages meeting precise constraints.

A similar example is ISO/IEC 9796-2:1997 signature (but it came with even less security claims). It's broken by an attack: Jean-Sébastien Coron, David Naccache, Mehdi Tibouchi, Ralf-Philipp Weinmann's Practical Cryptanalysis of ISO 9796-2 and EMV Signatures, in Journal of Cryptology (2015), and before in proceedings of Crypto 2009. The scheme is widely used in bank Smart Cards, with parameters allowing a feasible computation of a few hundred thousand messages such that, should an adversary manage to obtain the signatures of all except one, that allows finding the signature of the last message. But it can't degenerate to practical exploitation.

¹ The reference paper on the attacks is Don Coppersmith, Jean-Sébastien Coron, François Grieu, Shai Halevi, Charanjit Jutla, David Naccache, Julien P. Stern: Cryptanalysis of ISO/IEC 9796-1, in Journal of Cryptology (2007). It regroups earlier attacks:

• A new signature forgery strategy applicable to ISO 9796–1/2, ECASH™, PKCS#1 V2.0, ANSI X9.31, SSL-3.02, expert contribution ISO/IEC JTC1/SC27 (1999) which showed an attack path, that turned out not directly applicable to the standard due to a one-bit detail.
• ISO 9796-1 and the new forgery strategy (working draft) improves on that strategy to tackle the full standard, but requires many chosen messages.
• A Chosen Messages Attack on the ISO/IEC 9796-1 Signature Scheme (slides) uses another strategy, which works with few messages, and makes finding them inexpensive.

Recently, WPA2 was found vulnerable to Key Reinstallation attacks, despite the WPA2 4-way handshake having been proven secure.

• Key Reinstallation Attacks: Forcing Nonce Reuse in WPA by Mathy Vanhoef and Frank Piessens

From their website

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 only once. Instead, it merely assures the negotiated key remains secret, and that handshake messages cannot be forged.

The longer answer is mentioned in the introduction of our research paper: our attacks do not violate the security properties proven in formal analysis of the 4-way handshake. In particular, these proofs state that the negotiated encryption key remains private, and that the identity of both the client and Access Point (AP) is confirmed. Our attacks do not leak the encryption key. Additionally, although normal data frames can be forged if TKIP or GCMP is used, an attacker cannot forge handshake messages and hence cannot impersonate the client or AP during handshakes. Therefore, the properties that were proven in formal analysis of the 4-way handshake remain true. However, the problem is that the proofs do not model key installation. Put differently, the formal models did not define when a negotiated key should be installed. In practice, this means the same key can be installed multiple times, thereby resetting nonces and replay counters used by the encryption protocol (e.g. by WPA-TKIP or AES-CCMP).

The Clipper Chip with the Skipjack Cipher

This might be lower hanging fruit than you intended, as the "Real world attack vector" may not be very useful to attack with, as only the AT&T TSD-3600-E was the device to have been known to have implemented this for this, and most other devices appeared to have only be bought by the United States Department of Justice. This said, it might help elaborate on @Kevin's comment on how side-channels are more common to be attack vectors for said algorithms, given the most well known reason it's no longer in use.

The Clipper Chip, and the Law Enforcement Access Field (LEAF)

The LEAF was intended as a way to allow the government to read information necessary to be able to determine the encryption key, and be able to decrypt the message when they had a warrant to do so.

This had 2 major problems later discovered:

1.) Matt Blaze, in 1994, discovered that it was possible to use the fact that the LEAF system requires a 16-bit hash for an encryption key to verify that it was a valid message to encrypt (Such that it could be decrypted), it was possible to brute force for ~30-50 minutes a new 16-bit checksum for a different encryption key than the one used to encrypt the message, effectively bypassing the "Decryptable if necessary" step.

2.) Yair Frankel and Moti Yung in 1995 discovered that it was possible to use one LEAF capable device to generate validation attached for messages encrypted on another device, thus bypassing the "Decryptable if necessary" step in real time.

Ultimately, these issues are what most likely lead to the disuse of this method, with the U.S. government being the most notable largest customer of the AT&T TSD-3600-E. I'm unaware of how many of these were actually used as a result, since reportedly most of the boxes were left unopened. Which leaves us with concerning the actual Skipjack cipher.

Skipjack

This was the encryption that, as I understand, was used by the Clipper Chip such that, without that valid LEAF from the hashes above, would be secured against someone decrypting what was in the message.

This is harder to proof that it was proven secure, given that originally, it was classified, but...Academic researchers were brought in to evaluate Skipjack, and found that "Thus, there is no significant risk that SKIPJACK will be broken by exhaustive search in the next 30-40 years."

June 25, 1998, when Skipjack was declassified, Eli Biham and Adi Shamir had discovered that when Skipjack is reduced to 16 instead of 32 rounds, it was breakable with an attack vector discovered at that time. Later in 1999, with Alex Biryukov, they were able to extend it to 31 of 32 rounds.

Apparently, as of 2009, a full breakthrough of all 32 rounds had not been fully broken, but these appear to indicate that the original proof may have been wrong, given that it appears that the first 31 rounds of 32-round Skipjack relied primarily on the classification of the algorithm at the time.

As @Kevin said in his comment to the question above, primarily side-channels would be the way to break it - and in this case, the Clipper Chip and its LEAF protocol itself proved to be the weaker link - breaking the protocol that would have been used to decrypt the underlying encrypted messages when warranted.

In 2019 a counterfeiting vulnerability was discovered in Zcash [see here].

Prior to its remediation, an attacker could have created fake Zcash without being detected!

With a current market capitalisation of $1.7B, it seems Zcash is, at least today, enjoying widespread adoption beyond a few specialist users. The vulnerability stems from a subtle cryptographic flaw in the [BCTV14] paper that describes the zk-SNARK construction used in the original launch of Zcash. The vulnerability is so subtle, that it evaded years of analysis by cryptographic experts. Furthermore, some subsequent works by renowned researchers also inherited the same flaw.

Importantly, the [BCTV14] construction did not have a dedicated security proof, as noted in [Parno15], and relied mainly on the [PGHR13] security proof and the similarity between the two schemes. The Zcash Company team did attempt to write a security proof in [BGG17], but it did not uncover this vulnerability. Zcash has since upgraded to a new proving system [Groth16] which has multiple independent proofs and significantly better analysis.

For the wast majority of modern cryptographic algorithms there is no strict mathematical proof that they are secure. Most often when such a proof is published or discussed, it is based on assumptions which are merely believed to be true. If these assumptions don't hold, the proof falls apart even if there are no mistakes in it. For example, the security of triple-DES was based on the assumption that the regular DES is secure (albeit with a key size insufficient to prevent brute-force attacks). If a serious flaw would have been discovered in DES, it would likely compromise 3DES security as well.

The second kind of assumptions in security proofs comes from the fact that they are trying to prove a negative. So, instead of proving that an algorithm cannot be broken, researches evaluate its security w.r.t. known attacks. If an algorithm has been widely known for several decades, it is believed to be "proven in practice", which is in fact an assumption that no new attacks can be designed against it.

The above two points come in addition to banal mistakes in a proof's logic.

So, depending on the level of proof you consider adequate, you can either say that none of the famous real-world protocols have ever been proven secure, or that those protocols which were later cracked were "proven" secure at some point (else they wouldn't have been used), but the proof didn't hold.