RE: SOI QUESTIONS: 2.6 Formal proofs of security

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

> > 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").

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

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

> > I believe that the value from formal methods comes from
> > addressing a problem in an appropriate formalism so that the
> > human brain needs to do less work to interpolate the gap
> > from requirements to specification.
> 
> I think we shouldn't understate the fact that we are building 
> a new protocol
> out of building blocks of existing protocols. The fact that 
> we aren't doing
> anything revolutionary is more comfort to me than a formal 
> proof. You start
> by just following sound cryptographic principles:

I don't find re-use of existing blocks all that comforting.
Many security problems come from applying a security control
out of the domain in which it has been demonstrated effective.
Consider the arguments used to justify use of four digit pins
on the Internet by analogy to ATM machines.

> 1. Start with a fully vetted cryptographic core.
> 2. Ensure that all inputs to the MAC are encoded in an 
> unambiguous form.
> 3. Add entropy explicitly through a nonce, rather than 
> assuming that some
> parameters are pseudo-random.
> 4. Don't use the same key for multiple things.

I agree that we probably know how to build a key agreement
protocol. Certainly I think we know enough at this point
to be able to develop new key agreements that are no more
likely to fail than existing ones.

> You can't test every permutation, but if your implementation 
> is modular
> enough then you can test enough to get full coverage. I once 
> knew a guy who
> wanted to verify the correctness of his 3DES implementation 
> by testing every
> possible key. That still makes me laugh.

Why? The approach works just fine for DES...

	Phill