RE: SOI QUESTIONS: 2.6 Formal proofs of security

[Paul Koning <pkoning@equallogic.com>]

>>>>> "Andrew" == Andrew Krywaniuk <andrew.krywaniuk@alcatel.com> writes:

 Andrew> Was the Needham-Schroeder flaw discovered by a formal proof?

I don't know.  My reference to it was prompted by reading about it in
DEC SRC report 39, "A logic of authentication" (Burrows, Abadi,
Needham). 

 Andrew> (I got the impression it was discovered via machine
 Andrew> simulation.) It would be nice if we had some kind of magical
 Andrew> Turing machine that would read in an RFC and tell us if the
 Andrew> protocol was secure, but in reality the formal methods are
 Andrew> imperfect because they rely on too much human input.

True, but they can still tell us things we didn't previously know.
The DEC report I just mentioned describes its analysis of the Yahalom
protocol, and the fact that this analysis discovered some non-obvious
properties that came as a surprise both to the analysts and to the
inventor of the protocol.  (In this case, they were not flaws, but
they were still properties that were important to be aware of.)

 Andrew> Yes, we should continue to analyze the protocol and improve
 Andrew> the machine analysis tools. However, the question Ted posed
 Andrew> is what are we willing to trade off in order to get a
 Andrew> security proof. I don't think we need to dumb down the
 Andrew> protocol to cater to the limitations of formal analysis. I
 Andrew> would trust a logical analsis more than a formalized one at
 Andrew> this point.

I wouldn't want to push one at the exclusion of the other.

As for "dumbing down" the protocol to accommodate formal analysis, is
that speculation at this point or do we have concrete examples where
this applies?  If the latter, what are they?  As I said earlier, I
would tend to start out suspicious of features so complex that they
aren't amenable to formal analysis.

       paul