<div dir="ltr"><div class="gmail_default" style="font-size:small">On Sat, Feb 18, 2017 at 12:49 PM, Jon Callas <span dir="ltr"><<a href="mailto:jon@callas.org" target="_blank">jon@callas.org</a>></span> wrote:<br></div><div class="gmail_extra"><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">As a mathematical logician, I'm a huge fan of proofs, and yet sneer at a lot of security proofs.<div class="gmail_default" style="font-size:small;display:inline">​</div></blockquote><div><br></div><div class="gmail_default" style="font-size:small">​I note that a lot of folk in the crypto world did Formal Methods at university and don't seem to be all that keen on formal security proofs, myself included.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">One problem is the difficulty of defining what security is, another is that the proofs of security we have are based on a set of security assumptions that are themselves not provable. Which is problematic to say the least.</div><div class="gmail_default" style="font-size:small"><br></div><div class="gmail_default" style="font-size:small">Formal verification of code such as a compiler or a kernel like Perry suggests is a very good thing. We can define the problem and the security properties (no buffer overrun, etc.). Security properties of crypto protocols on the other hand hit the problem that what we can prove to be secure often requires us to make simplifications that make the protocol less robust and thus less secure in practice.</div></div></div></div>