[Cryptography] Security proofs prove non-failproof

[Jon Callas]

As a mathematical logician, I'm a huge fan of proofs, and yet sneer at a lot of security proofs.

We don't have formal definitions of what security even means. Our reasoning is based on concepts like "distinguishability" which are obviously flawed. Distinguishability is the same thing as saying, "Hey, we don't know if it's a duck but it quacks, has webbed feet, flies and swims." We also have a bunch of models like The Random Oracle Model, which is good as far as it goes, but sometimes it doesn't go as far as we'd like.

There are also a number of tacit assumptions that might be relevant in implementation. There is a marvelous proof of SSH, but Kenny Paterson and crew found a security break in it. The break came because of leaks from packet sizes, and the proof had an abstract definition of packets. Obviously, an implementation has to have the concept of a size and that's where the disconnect is.

As an analogy, assume an unpickable lock. But also assume that said lock is installed in a glass door, and by looking through the glass door and a reflection you can see information that lets you get the right key made. This isn't at all part of the model and likely the proof of security didn't have that in it. Their security model was different than the one where the lock was implemented.

(As a logician, what I would say is that the actual model is an elementary extension of the proof model that includes symbols in the formal language that lead to a contradiction in the extension that don't exist in the base model.)

In any event, this is the core of why proofs of security useful (hey, who doesn't want an unpick able lock?) and yet often don't matter in the real world (because it was installed in a glass door).

	Jon