[Cryptography] Security proofs prove non-failproof

Perry E. Metzger perry at piermont.com
Tue Feb 21 14:05:53 EST 2017


On Tue, 21 Feb 2017 13:52:32 -0500
Phillip Hallam-Baker <phill at hallambaker.com> wrote:
> 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.

I'm not familiar with the details of that situation (my schedule
hasn't permitted me to watch TLS for the last few years in much
depth). I would certainly hope that in the medium term, especially if
a lot of experience is gained, it should be possible to dramatically
increase the complexity of the protocols and code that can be subject
to formal methods. That sould help with the problem of people wanting
to shoehorn protocols into designs they can verify. (That said, it
will always be easier to verify cleaner, simpler designs, but I don't
see that as a flaw.)

Proof engineering is in its infancy right now. Given more experience,
it should be possible to do better, but there's only one way to get the
experience, which is for people to dive in and work hard on the problem.

I'll also note that if the software and protocol engineers leave it up
to other people to do the verification work, there won't be nearly as
much progress as there might be if the engineers learn a lot about how
to do this stuff themselves. This is one of the reasons I keep
encouraging people on the engineering side of the fence to learn about
these tools and gain practical experience with them.

Perry


More information about the cryptography mailing list