[Cryptography] Security proofs prove non-failproof

[Phillip Hallam-Baker]

On Mon, Feb 20, 2017 at 3:51 PM, Perry E. Metzger <perry at piermont.com>
wrote:

> On Mon, 20 Feb 2017 11:59:11 -0500
> Phillip Hallam-Baker <phill at hallambaker.com> wrote:
> > You are conflating two things
> >
> > 1) Formal proofs of code correctness
> >
> > 2) Formal proofs of algorithm or protocol security
> >
> > I very strongly believe the first is possible. My doctoral thesis is
> > on a formal proof of correctness for a significantly large system.
> >
> > I remain skeptical on the second and suspect that the current state
> > of the art is doing more harm than good.
>
> There exist a number of formal proofs of security for protocols. My
> understanding is that several such attempts have found significant
> flaws in both proposed and deployed protocols.
>
> (On a related note: In an earlier message, Peter expressed skepticism of
> the usefulness of formal verification of protocol implementations
> because, for example, a TLS implementation verification ran into a
> question of an edge case that none of the "normal" implementations had
> cared to even implement. I see such discoveries of holes in a
> specification as enlightening rather than useless, as, historically,
> protocol security flaws have often appeared in edge conditions that
> "normal" implementers have ignored or not thought much about. Formal
> specifications of protocols tend to smoke out such things. One of
> course needs a formal specification of a protocol in order to determine
> if a given implementation complies with the formal specification.)
>

​I certainly agree that formal analysis can reveal certain types of flaw.

My skepticism comes from seeing how restricting designs to what can be
analyzed with formal methods has led to fragile protocols.

To give an example. TLS ephemeral key agreement is botched. The results
from the master key agreement are not fed into the ephemeral. So if the
ephemeral is weak, the key agreement is weak even if the master agreement
was strong. One of the reasons given for not chaining the master key
agreement into the ephemeral was concern for preserving some sort of half
baked model.​
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.metzdowd.com/pipermail/cryptography/attachments/20170221/9cfa9999/attachment.html>