RE: SOI QUESTIONS: 2.6 Formal proofs of security

["Andrew Krywaniuk" <andrew.krywaniuk@alcatel.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").


> 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:

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.

Then add some lessons we have learned from experience:

5. Hash all payloads, not just some payloads so that new, optional payloads
will automatically be included.
6. Use stateless cookies.
7. Build dead peer detection into the protocol.
8. Clearly state the security properties of the protocol so the reader
doesn't get any false impressions.

I have a high degree of confidence that what we produce will be secure.


> True, but they can still tell us things we didn't previously know.
> The DEC report I just mentioned describes its analysis of the Yahalom
> protocol, and the fact that this analysis discovered some non-obvious
> properties that came as a surprise both to the analysts and to the
> inventor of the protocol.  (In this case, they were not flaws, but
> they were still properties that were important to be aware of.)

In other words, they weren't design constraints. This just re-enforces my
earlier point that the problem with formal analysis is that you won't find a
problem unless you are specifically looking for it.


> As for "dumbing down" the protocol to accommodate formal analysis, is
> that speculation at this point or do we have concrete examples where
> this applies?  If the latter, what are they?  As I said earlier, I
> would tend to start out suspicious of features so complex that they
> aren't amenable to formal analysis.

In the not too distant past, "X is too complicated" was the catch-all
technique that list members had for criticizing any idea they didn't like.
This led to various amusing threads, such as the infamous "Puh-leeze".
Anyway, some people claim that a 2-phase protocol is by nature too complex;
others say that a 9 message protocol is too complex; still others state that
IKE is really 12 protocols and that is too complex.

I find some of these arguments lacking. For one thing, I have noticed that
longer protocols are generally easier to analyze than shorter ones [that
accomplish the same thing], and I can give you plenty of examples within IKE
(I've posted them to this list before, so I won't do it again unless you're
particularly interested).

Also, if you have a protocol with 4 Boolean options then a formal analysis
has to handle 16 different permutations, but a human may be able to
determine that none of the options actually interact with each other so the
analysis isn't actually that complicated.

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.

Andrew
-------------------------------------------
There are no rules, only regulations. Luckily,
history has shown that with time, hard work,
and lots of love, anyone can be a technocrat.