How to prove the security of block ciphers

Question

I see very often proofs of security for asymmetric crypto algorithms, for instance, using reductions to known hard problems, or game based proofs...

In the field of protocols (like authentication) it happens too, for instance proofs using formal models...

But what about the symmetric crypto? More specifically, the blockciphers?

For example, this paper (presenting the Piccolo blockcipher) has a section named Security Analysis on which the authors just argue why they think Piccolo is secure against some knowns attacks. This is actually the opposite of the "philosophy" of the provable secure crypto, that tries to analyse the security of a primitive without exhaustively trying the known attacks, because it may exist some attack that is not know by the academic community.

Thus,

1. Are the blockciphers usually proved to be secure?
2. If yes, how is it done? If not, how the security is measured?
3. Is the approach of security analysis used in the paper above common on blockciphers papers?
4. And since the answer to the first question seems to be no, is there any blockcipher whose security analysis was done following a "provable secure like" approach?

Answer 1

There is actually a field of study regarding provably secure block ciphers. The seminal paper was "How to construct pseudorandom permutations from pseudorandom functions" (1988) by Luby and Rackoff. Their paper used pseudorandom round functions in a Feistel construction, and proved that 4 rounds were sufficient to make the resulting block cipher a pseudorandom permutation against chosen plaintext and ciphertext attacks. That paper spawned a cottage industry of similar papers based around the Feistel construction, or generalizations thereof. In addition to academic papers and theoretical cipher constructions, this also inspired a few actual concrete block ciphers, such as the BEAR and LION ciphers by Anderson and Biham that Marcellus mentioned, and the Turtle block cipher, by Matt Blaze, for which the author claims that "recovery of its internal state given its inputs and outputs in NP-complete."

More recently, a similar wave of papers have developed regarding provably secure "key alternating" block ciphers, which are like AES in that the round function consists of the entire state being xored with a key, followed by an unkeyed permutation. The seminal paper for this wave was "A Construction of a Cipher From a Single Pseudorandom Permutation" (1991) by Even and Mansour, which focused on the security of a key alternating block cipher with a single round. This was then expanded to iterated constructions with multiple rounds in "Tight Security Bounds for Key-Alternating Ciphers" (2013) by Chen and Steinberger, inspiring a similar cottage industry of related papers in recent years.

But the overwhelming majority of actual, concrete block ciphers are not provably secure in the sense of the above literature. Instead, they accumulate confidence over time insofar as they continually resist cryptanalytical efforts. As Biv described, they may also attempt to prove immunity to certain specific kinds of known attack; whereas the academic papers above purport to prove security against all attacks, known and unknown.

Answer 2

In symmetric cryptography it is hard to prove security properties on algorithm. Most of block ciphers relies on showing resistances to the current attacks (cf the paper you linked or any paper that introduce a new block cipher). As nobody can know what will be the next attack vector, it is not possible to be prepared against it.

From The design of Rijndael (p 72-73):

5.5.2 Unknown Attacks Versus Known Attacks

‘Prediction is very difficult, especially about the future.’ (Niels Bohr)

Sometimes in cipher design, so-called resistance against future, as yet unknown, types of cryptanalysis is used as a rationale to introduce complexity. We prefer to base our ciphers on well-understood components that interact in well-understood ways allowing us to provide bounds that give evidence that the cipher is secure with respect to all known attacks. For ciphers making use of many different operations that interact in hard-to-analyse ways, it is much harder to provide such bounds.

5.5.3 Provable Security Versus Provable Bounds

Often claims are made that a cipher would be provably secure. Designing a block cipher that is provably secure in an absolute sense seems for now an unattainable goal. Reasonings that have been presented as proofs of security have been shown to be based on (often implicit) assumptions that make these ‘proofs of security’ irrelevant in the real world. Still, we consider having provable bounds for the workload of known types of cryptanalysis for a block cipher an important feature of the design.

Some examples of approaches used:

In Rijndael (quite similar to Piccolo but far more developed in their book).

They showed that no differential on the S-box has a probability over $4/256$. Using the Walsh-Hadamard Transform, they also provided a bound on the security against Linear cryptanalysis.

In Keccak

To prove the security of Keccak, the designers followed the bound approach. It is impossible to build a the list of possible differential on the state of Keccak ($2^{1600}$ difference possible). Therefore it is more interesting to provide some bounds on the difficulty to find a collision.

(Simplified version)

1. They calculated the Differential Probability on differences with low Hamming weight on a small number of rounds
2. They showed that the Differential Probability decreases when the Hamming weight increases
3. They deduced and provided an approximation of the maximum probability on the full round function : $DP \ge \frac{1}{2^{296}}$

   For the 24 rounds of Keccak-f[1600], a differential trail has at least a weight 296.

from Differential propagation analysis of Keccak.

Answer 3

I remember that BEAR and LION are two block ciphers are provably secure under the assumption that the primitives used (hash and stream cipher) are secure.

This is the most "provable secure like" approach I can remember.

A part of that, I think the securite of block ciphers are anaylized as the paper you have cited do. Checking the security against the known attacks.

This question is a few old but may be usefull. As people aswered there is no known reduction for AES and I think it holds for almost all the block ciphers.