Mfcttrf

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 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 public-key encryption and signature schemes chosen in OpenPGP were 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.

    
    
  
  

  • The mechanism for combining fancy math primitives like RSA and standard symmetric cryptography to encrypt long messages in OpenPGP was designed without formal analysis relating them to the security of the building blocks, and it turned out they were exploitable in practice in real email clients in an attack dubbed EFAIL (my answer on it).

  
  


• 
  

  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.
  
  

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 bmodpq$, 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 all of the above attacks could have been caught by studying the formal security properties of all the protocols involved, and in most cases the analysis is not actually that hard.

Two well known candidates are md5 and DES.

In general, I think if there is no security proof, we should for all intents and purposes, consider it insecure and not roll it out.

Edit: Squeemish made a good point in that RSA/AES/Keccak do not have security proofs. With this, I have taken a softer stance in that we should avoid rolling out implementations which have not been proven secure.

By rolling out, I am referring to initially rolling out. If it’s already in the wild at this moment, then it is too late.