Soft question: Examples where lack of mathematical rigour cause security breaches? 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 Bleichenbacher RSAES-PKCS1-v1_5 padding oracle attack, which breaks an RSA-based encryption scheme designed without formal analysis, broke SSLv3 with RSA key agreement in 1998, and then broke it again in 2014 with the POODLE attack because of security-destroying protocol compatibility fallbacks, and then broke it again in 2018 with the ROBOT attack.
The BEAST attack, which had been noted by Phil Rogaway in 2002 and documented in theory for SSL/TLS in 2004, exploited the failure of SSL/TLS to follow the security contract of CBC which requires the IV to be unpredictable in advance for each message—the protocol had deployed CBC without formal analysis of how the IV is chosen.
The Lucky 13 attack (web site) recovers plaintext by using timing of padding verification as a CBC padding oracle, which arose from a CBC padding mechanism designed without even a simple-minded formal analysis of its timing characteristics.
The TLS renegotiation attack exploited a complicated state machine in the TLS protocol involving key renegotiation and authentication, which was never formally analyzed for its security properties, to forge messages sent to a TLS peer without its notice.

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!