[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
RE: SOI QUESTIONS: 2.6 Formal proofs of security
Was the Needham-Schroeder flaw discovered by a formal proof? (I got the
impression it was discovered via machine simulation.) It would be nice if we
had some kind of magical Turing machine that would read in an RFC and tell
us if the protocol was secure, but in reality the formal methods are
imperfect because they rely on too much human input.
Yes, we should continue to analyze the protocol and improve the machine
analysis tools. However, the question Ted posed is what are we willing to
trade off in order to get a security proof. I don't think we need to dumb
down the protocol to cater to the limitations of formal analysis. I would
trust a logical analsis more than a formalized one at this point.
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 Paul Koning
> Sent: Friday, June 21, 2002 5:59 PM
> To: andrew.krywaniuk@alcatel.com
> Cc: grebus@fddimax.zk3.dec.com; ipsec@lists.tislabs.com
> Subject: RE: SOI QUESTIONS: 2.6 Formal proofs of security
>
>
> Excerpt of message (sent 21 June 2002) by Andrew Krywaniuk:
> > 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.
>
> That's true for some flawed protocols. Some were so flawed that it
> only took knowledge at the level of Crypto 101 to spot the holes.
>
> But what you say does not apply to all flawed protocols. There's the
> classic example of the initial Needham-Schroeder protocol, yet I don't
> think many people would want to describe those two authors as "not
> technically savvy".
>
> paul
>