[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: IPsec near term work




Russ_Housley.McLean_CSD@xerox.com says:
> Perry:
> 
> You said:
> > I agree that formally characterizing the properties of the model is
> > hard. Of course, formally characterizing the failure modes of SMTP
> > email is also hard, and yet people manage to trust that SMTP will
> > deliver their mail most of the time just fine.
> 
> Authentication that can be trusted most of the time to be correct is not
> acceptable! I am not willing to call it authentication if I can trust it most
> of the time, but not always.

Anyone who can produce a proven correct *implementation* of any
security protocol that is longer than 1000 lines of code in length is
invited to reply.  Otherwise, the notion of proving a protocol correct
(when we can't even properly characterize all the threats) and then
using a non-provably correct implementation is inane.

I am also reminded of a project I worked at at Bellcore. We had a PhD
in math checking a protocol simulation, and he proved the program
correct. Unfortunately, both the proof and the program had a subtle
bug.

As for the authentication protocol, it doesn't have to be provably
correct.  The authentication protocol merely has to be correct.
Provably correct would be nice, but its unlikely to happen, and
systems like Kerberos have shown that good systems can be built
without formal proofs of correctness. As I've said, any such "proof"
is in any case rendered useless in the face of unprovable
implementations, unprovable compilers compiling the implemenations,
unprovable operating systems, unprovable hardware, etc.


Perry


References: