[Cryptography] Security proofs prove non-failproof

[Perry E. Metzger]

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.)

Perry