RE: SOI QUESTIONS: 2.6 Formal proofs of security

["Hallam-Baker, Phillip" <pbaker@verisign.com>]

In response to Ran's note I suspect that all the people in the thread
actually have a mutually compatible view of what formal methods can do and
what should be required.

Some of the negativity in my posts probably comes from the fact that having
seen Formal methods massively oversold I think it is important to set
expectations.

Clearly formal methods can add significant value. However what people have
been cautioning against is setting the bar to SOI to be a formal 'proof of
security' ignoring the fact that what consitutes a proof of security is
highly debatable (even in forums other than IETF mailing lists where
anything is highly debatable), and the fact that we did not put IKE through
that analysis.

I think it would be quite reasonable to state specific empirical tests that
a SOI protocol should pass, provided that the analysis methods involved do
not introduce arbitrary constraints into the solution space whose only
purpose is to allow the analysis.

		Phill