<div dir="ltr"><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Feb 20, 2017 at 3:51 PM, Perry E. Metzger <span dir="ltr"><<a href="mailto:perry@piermont.com" target="_blank">perry@piermont.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Mon, 20 Feb 2017 11:59:11 -0500<br>
Phillip Hallam-Baker <<a href="mailto:phill@hallambaker.com">phill@hallambaker.com</a>> wrote:<br>
> You are conflating two things<br>
><br>
> 1) Formal proofs of code correctness<br>
><br>
> 2) Formal proofs of algorithm or protocol security<br>
><br>
> I very strongly believe the first is possible. My doctoral thesis is<br>
> on a formal proof of correctness for a significantly large system.<br>
><br>
> I remain skeptical on the second and suspect that the current state<br>
> of the art is doing more harm than good.<br>
<br>
</span>There exist a number of formal proofs of security for protocols. My<br>
understanding is that several such attempts have found significant<br>
flaws in both proposed and deployed protocols.<br>
<br>
(On a related note: In an earlier message, Peter expressed skepticism of<br>
the usefulness of formal verification of protocol implementations<br>
because, for example, a TLS implementation verification ran into a<br>
question of an edge case that none of the "normal" implementations had<br>
cared to even implement. I see such discoveries of holes in a<br>
specification as enlightening rather than useless, as, historically,<br>
protocol security flaws have often appeared in edge conditions that<br>
"normal" implementers have ignored or not thought much about. Formal<br>
specifications of protocols tend to smoke out such things. One of<br>
course needs a formal specification of a protocol in order to determine<br>
if a given implementation complies with the formal specification.)<br></blockquote><div><br></div><div><div class="gmail_default" style="font-size:small">​I certainly agree that formal analysis can reveal certain types of flaw.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">My skepticism comes from seeing how restricting designs to what can be analyzed with formal methods has led to fragile protocols.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">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.​</div><br></div><div> </div></div></div></div>