[Cryptography] Security proofs prove non-failproof

[Benjamin Kreuter]

On Mon, 2017-02-20 at 11:59 -0500, Phillip Hallam-Baker wrote:
> 
> 1) Formal proofs of code correctness
> 
> 2) Formal proofs of algorithm or protocol security

> I remain skeptical on the second and suspect that the current state
> of the art is doing more harm than good.

What is the alternative?  For something like TLS, maybe we can avoid
formal methods, but what about protocols that solve more complex
problems?  Secure multiparty computation is seeing use in more and more
real-world settings, and I would be skeptical of any MPC protocol that
did not undergo at least some formal analysis.

Yes, it is sometimes the case that fragility or complexity is added to
a protocol just to make a proof work.  That needs to be weighed against
the benefit of catching subtle flaws early, before a system has been
deployed and before there can be any real damage.  Maybe the benefits
do not justify the costs for TLS, but there is not much doubt about the
value for cryptographic protocols in general.

-- Ben
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 847 bytes
Desc: This is a digitally signed message part
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170221/6d4f618d/attachment.sig>