Re: SOI QUESTIONS: 2.6 Formal proofs of security

[Paul Koning <pkoning@equallogic.com>]

>>>>> "VPNC" == VPNC  <Paul> writes:

 VPNC> At 1:04 PM -0400 6/20/02, Theodore Ts'o wrote:
 >> 2.6.)  Does SOI need to provide a formal proof of security?  (Is
 >> this a "must have" or a "nice to have"?  What are we willing to
 >> trade-off for having a formal proof of security?)

 VPNC> In the typical VPN scenario (either gateway-to-gateway or
 VPNC> remote-access WAN), this is not important. It is nice to have,
 VPNC> of course, but only to keep ourselves happy.

I disagree.

The scenarios are irrelevant to this question.

The point is: what level of assurance do we want that there aren't
design errors in the protocol?  Some people build "security" protocols
that don't provide security.  Some of the errors made are obvious to
casual observers; some are not.  It would be good for IPsec/IKE to be
secure in reality.  Formal analysis is part of the QA that helps
confirm this property.  Without it, you may still be secure, and you
may have caught most bugs by informal analysis, but the level of
assurance is less.

So I would rate it as "very desirable".

   paul