RE: SOI QUESTIONS: 2.6 Formal proofs of security

[Ran Canetti <canetti@watson.ibm.com>]

Please excuse the length of this note.

I've been following this thread (the need for analysis) with great interest,
and would like to make some remarks from the point of of view of a person
who spent much of the past 13 years or so trying to analyze the security 
of protocols (and to understand what security means in the first place).

The bottom line is that "security analysis" is not a binary
do-it-and-be-done-with-it process. No single analysis of IKE/SOI is 
likely to ever be perfect or complete. Still, security analysis
is indispensible. (There are so many protocols that were designed by smart
and experienced people and were later found insecure via more careful 
analysis. STS is just one very relevant example.) It is thus crucial 
to obtain as many analyses of IKE as possbible, using as many tools 
as possible. And it is imperative to write the spec in a clear way that 
is conducive to analysis.

A couple of more specific points:

1. IETF RFCs only provide the essentials for interoperabiltiy, plus maybe some 
implementation tips. They do NOT give a complete specification of a protocol.
So even if a standard is "secure" in the sense that it is possible to
implement it in a perfectly secure way, it is still possible (and easy...) to
implement it in a fully compliant, yet grossly insecure way. 
This basic fact has two immediate consequences:
-Being compliant with a "secure" IETF standard does NOT guarantee security.
An implementation of the standard that wants to verify its security must
use its own shrink and undergo its own analysis.
-This of course does not mean that there is no point in analyzing the
security of IKE/SOI. (If the standard is insecure then implementations have no 
hope of being secure.) However, what it does mean is that in analyzing IKE/SOI
it is important to analyze the principles of the protocol design rather than
the implementation details. Such higher-level analysis will be easier to 
apply to complying implementations. 

2. There are numerous quite different approaches to analyzing security of
protocols, where each approach has its own strong and weak points. Here are
three main trends, going from the abstract to the concrete:

 * "Formal methods" style analysis.
 Here the protocol is first written in an abstract language where the 
 basic cryptographic primitives (such as signature, encryption, hashing) 
 are modeled as "ideal boxes". Next, this abstract protocol is run through an 
 automatic state-analyzer that makes sure that no attacker can reach a state 
 that was designated as udesired. The main strength of this approach is that 
 it allows for automated (or semi-automated) proofs, and is thus less 
 susceptible to human error. However, these methods provide only very partial 
 security guarantee. One main discrepancy with "real-life" protocols is that
 the abstractions of the cryptographic primitives are often overly strong,
 and assume properties that are not obtainable by actual algorithms (such 
 as RSA, DH, SHA1, etc). Thus, while this method is good in finding 
 flaws in the overall structure of the protocol, it cannot guarantee
 security. 
 
 * Cryptographic analysis.
 Here the protocol is represented in a much less abstract way, and the
 cryptographic primitives are represented in a way that is proven to be
 realizable via actual algorithms (under appropriate computational
 intractability assumptions). Consequently, here proofs of security are 
 coonsiderably more meaningful and apply more directly to the actual 
 "real-life" protocol. The down side of this analysis style is that it is
 inherently complex. Moreover to date we have no automation technology
 here, so proofs are hand-written and thus more susceptible to human errors.
 
 * Implementation analysis.
 Even the cryptographic approach typically makes numerous abstractions while 
 representing and analyzing protocols. Typical axamples include implementation
 issues such as interaction with the operating system and the protocol stack,
 various buffer overflows, memory backups and erasures, auditing, etc.
 Unfortunately, experience shows us that many security flaws result from
 such issues. Thus direct analysis of the implementation is essential. 
 Here, however, we have no complete analysis tools. Our only hope is to 
 keep finding and fixing those flaws, and hope to do it faster than the rate
 in which new flaws are found...

Clearly, IKE/SOI can benefit from analysis on all three levels described
above, and the more the better. This holds both to the standard itself and
to actual implementations of the standard. (And, even if it may seem that 
customers dont care about security analysis, I believe it is our duty  and
responsibility to seek it. Otherwise, lets just replace all crytographic
operations with empty procedures. This way we'll have a very efficient 
and highly interoperable standard... )

Ran



PS. The above note did not even touch the issue of what security properties 
should cryptographic (or formal-methods) analysis try to assert.
This is a whole other can of worms...