26
$\begingroup$

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?

$\endgroup$
4
  • 1
    $\begingroup$ You could also consider arxiv.org/abs/2012.03141 and mtpsym.github.io $\endgroup$ Feb 25 at 12:59
  • 2
    $\begingroup$ The 3shake attack on TLS is probably the highest profile protocol. $\endgroup$
    – Daniel S
    Feb 25 at 13:33
  • 4
    $\begingroup$ Much of modern cryptography has never been "proven secure" in any meaningful sense of the term. For example, to the best of my understanding, AES-256 is believed to be secure primarily because a lot of smart people have tried to break it over a long period of time, and made very little progress. The other issue is that practical, real-world attacks often focus on side-channels rather than direct attacks on cryptographic algorithms, because the former often provide much lower-hanging fruit in practice. $\endgroup$
    – Kevin
    Feb 26 at 1:13
  • $\begingroup$ @Ievgeni guess I made a mistake when typing security. Fixed! $\endgroup$ Apr 15 at 14:33

7 Answers 7

17
$\begingroup$

One example is OCB2;

However, Akiko Inoue and Kazuhiko Minematsu describe practical forgery attacks against OCB2 in 2018. From the abstract;

We present practical attacks against OCB2, an ISO-standard authenticated encryption (AE) scheme. OCB2 is a highly-efficient blockcipher mode of operation. It has been extensively studied and widely believed to be secure thanks to the provable security proofs. Our attacks allow the adversary to create forgeries with single encryption query of almost-known plaintext. This attack can be further extended to powerful almost-universal and universal forgeries using more queries. The source of our attacks is the way OCB2 implements AE using a tweakable blockcipher, called XEX∗ . We have verified our attacks using a reference code of OCB2. Our attacks do not break the privacy of OCB2, and are not applicable to the others, including OCB1 and OCB3.

And other works that improve the Inoue and Minematsu's work;


A half one;

$\endgroup$
3
  • $\begingroup$ Luckily it was not widely adopted. $\endgroup$
    – kelalaka
    Feb 25 at 10:27
  • $\begingroup$ Apparently that was partially because it was patented $\endgroup$
    – SWdV
    Feb 26 at 13:27
  • $\begingroup$ @SWdV I've not aware of a patent for OCB2 and OCB was free to use for free software... $\endgroup$
    – kelalaka
    Feb 26 at 13:35
10
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Oh, thanks a lot, I didn't know that SSH was subject to this kind of attacks. Here, I guess it's different from the OCB2 attack : the flow lies in the security model and not in a mistake in the proof. $\endgroup$ Feb 25 at 14:03
9
$\begingroup$

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:

$\endgroup$
4
  • $\begingroup$ Thanks a lot! Do you know if ISO/IEC 9796-2:1997 had some sort of security proof? $\endgroup$ Feb 25 at 17:31
  • $\begingroup$ @LéoColisson: the closest is what I state in the second sentence of the answer, with link. I don't regard it as a security proof in the modern sense. $\endgroup$
    – fgrieu
    Feb 25 at 18:05
  • $\begingroup$ I was referring to your second example (the one from 1997, not 1991), I couldn't see any reference to the proof in this one in the answer. In the ISO paper, I can just see "Schemes very similar to Digital signature scheme 3 have mathematical proofs of security (see [5]). However, these proof techniques do not apply to Digital signature scheme 1.", and in the paper crypto-uni.lu/jscoron/publications/iso97962joc.pdf I can see that the scheme is proven secure if k_h > 2/3 the size of the modulus, but it's not clear after a quick look if it is the setting in which the attack lies. $\endgroup$ Feb 25 at 21:39
  • 1
    $\begingroup$ @LéoColisson: sorry, had misread you. No, there never was (AFAIK) a claimed security proof for ISO/IEC 9796-2:1997, or even a detailed security argument AFAIK. Only the later schemes (2 and 3) have some security proof in a modern sense. I know only few applications that use the new schemes, none of which as an upgrade of the old one. $\endgroup$
    – fgrieu
    Feb 28 at 12:16
4
$\begingroup$

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

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).

$\endgroup$
1
  • $\begingroup$ As you can see, the proof is valid in their term. That is actually good work to prove full protocol. $\endgroup$
    – kelalaka
    Feb 26 at 13:11
2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.