RE: SOI QUESTIONS: 2.6 Formal proofs of security

[Paul Koning <pkoning@equallogic.com>]

>>>>> "Phill" == Hallam-Baker, Phillip <pbaker@verisign.com> writes:

 >> > I have yet to see a really convincing Formal Method for >
 >> proving a protocol is secure. I very much doubt that such > a
 >> calculus could exist.
 >> 
 >> I don't doubt that it could exist, but I am certain that we don't
 >> have it (at least not for any comprehensive definition of
 >> "secure").

 Phill> The lack of a comprehensive definition of secure is the
 Phill> problem.

 Phill> Sure we can develop a calculus that can be used to prove that
 Phill> code is free of buffer overrun bugs, but that is not the only
 Phill> type of bug. At the specification level things get much harder
 Phill> and the approach is still 'prove that the spec has every
 Phill> security property in the set X', but no way to know that the
 Phill> set X is complete.

True.

Correctness proofs in general are a tough thing to attempt.  In my
view, the value isn't necessarily in a complete proof of security, but
rather in the fact that a formal analysis will turn up bugs that had
not been found by other methods.

	paul