[Cryptography] Security proofs prove non-failproof

Bill Frantz frantz at pwpconsult.com
Mon Feb 20 18:29:34 EST 2017


On 2/20/17 at 12:51 PM, perry at piermont.com (Perry E. Metzger) wrote:

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

The TLS working group has held up publication of TLS 1.3 so 
people can do formal analysis and feed back into the standard. 
That work has turned up some issues.


On 2/20/17 at 5:28 AM, perry at piermont.com (Perry E. Metzger) wrote:

>The cliff is there because the UI sucks, the documentation is
>mediocre, and you need to understand a bunch of type theory and formal
>logic in order to make progress. Patience. Things will get better.

The critical mass is probably when someone reports that they 
saved real money using formal methods to achieve a level of 
software reliability. Some things that will help:

   Make the UI better than teco/CMS EDIT.

   Teach formal methods in computer science courses.

My knowledge is limited. I've been exposed to some of the type 
theory at the Friday morning FRIAM meeting, and someday I may be 
able to explain what a monad is.

Cheers - Bill

-----------------------------------------------------------------------
Bill Frantz        |Security, like correctness, is| Periwinkle
(408)356-8506      |not an add-on feature. - Attr-| 16345 
Englewood Ave
www.pwpconsult.com |ibuted to Andrew Tanenbaum    | Los Gatos, 
CA 95032



More information about the cryptography mailing list