[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: SOI QUESTIONS: 2.6 Formal proofs of security
For some flawed security protocols, the problem was that the authors didn't
have any technically savvy people review them. A security proof might give
you some confidence in those protocols by virtue of the fact that they had
to hire/enlist an expert to write the security proof.
For IKEv1, there are lots of minor flaws that people knew about for a long
time. These are not issues that slipped through the cracks because we didn't
have a formal analysis. They are design tradeoffs that, in hindsight, were
probably ill-advised.
Some examples:
1. Problem: Some payloads are not included in the phase 1 authentication
hash.
Cause: Hash was constructed in such a way as to have (subjectively) better
repudiation properties.
2. Problem: IKE is vulnerable to time & state DoS in aggressive mode and
state DoS in main mode, even though 3 antecedent documents (Photuris,
Oakley, and Isakmp) discuss the problem.
Cause: An optimization. Some list members wanted to reduce round trips, even
at the expense of DoS prevention.
These are problems by design. A formal analysis doesn't help. In problem 1,
the protocol was designed by cryptographers, and I doubt that most people
understood at the time that this was the tradeoff (a statement of design
rationale might have helped). In problem 2, the tradeoff was a conscious
choice by list members.
But what about non-obvious problems that may lay dormant for years? Here are
the two newest security flaws that were discussed on this list:
3. Problem: IKE key stretching truncates the entropy of the DH shared
secret.
I'm speculating here, but this is the kind of thing that a formal analysis
might find. However when it was posted, a large number of list members
(including some advocates of formal analysis) said that it was not really a
flaw at all, since it is not practical to exploit it.
4. Problem: Non-random IVs allow an active attack against IPsec traffic.
Would a formal analysis have discovered this problem? I highly doubt it. The
scenario in which this attack is feasible was discussed on the list several
times last year and no one ever noticed the attack until recently. In order
to discover the attack by formal analysis, you first have to postulate the
existance of the attack and add it to your list of axioms.
An explanation of design rationale is a good thing if it prevents us from
making flawed design tradeoffs. A formal analysis using predicate logic
and/or state machines can't hurt, but it may give us a false sense of
security.
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.
> -----Original Message-----
> From: owner-ipsec@lists.tislabs.com
> [mailto:owner-ipsec@lists.tislabs.com]On Behalf Of Gary Grebus USG
> Sent: Thursday, June 20, 2002 6:43 PM
> To: ipsec@lists.tislabs.com
> Subject: Re: SOI QUESTIONS: 2.6 Formal proofs of security
>
>
> >
> > 2.6 Formal proofs of security
> >
>
> I haven't seen any specific claim that something would have
> to be traded off to get a
> formal proof of security of at least the core cryptographic
> protocol. It
> would seem prudent to use whatever formal methods are
> available to check for
> protocol errors. Especially in light of past "security
> protocols" that were
> shown to be insecure.
>
> --
> Gary Grebus
> Hewlett-Packard Company
> Tru64 UNIX Base OS Networking
> Gary.Grebus@hp.com
>