[Cryptography] Security proofs prove non-failproof

[Phillip Hallam-Baker]

On Sat, Feb 18, 2017 at 12:49 PM, Jon Callas <jon at callas.org> wrote:

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

​I note that a lot of folk in the crypto world did Formal Methods at
university and don't seem to be all that keen on formal security proofs,
myself included.

One problem is the difficulty of defining what security is, another is that
the proofs of security we have are based on a set of security assumptions
that are themselves not provable. Which is problematic to say the least.

Formal verification of code such as a compiler or a kernel like Perry
suggests is a very good thing. We can define the problem and the security
properties (no buffer overrun, etc.). Security properties of crypto
protocols on the other hand hit the problem that what we can prove to be
secure often requires us to make simplifications that make the protocol
less robust and thus less secure in practice.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170218/dcad999c/attachment.html>