Re: [IPsec] Charter review

["Dan Harkins" <[e-mail]>]

On Fri, November 7, 2014 12:03 am, Yaron Sheffer wrote:
> <hats off>
>
> Regarding formal security proofs, I strongly disagree.
>
> The current wording is extremely mild. It does not require an actual
> security proof (which would not be realistic), but says "The solution
> should be in line with current best practices, including ... possible
> formal protocol security proofs."
>
> This to me means that people have looked at the modified protocol and
> can say that the new stuff does not inhibit such a security proof in the
> future, and that we formally understand the security properties that are
> supposed to be provided by the protocol.
>
> We are making a major change to IKE, and as much as I care about its
> goals, we should try to do it right. Relying on "the security afforded
> by DH" is not easy when in the real world, both peers might be reusing
> exponents and/or using too short DH groups.

  This "major change" is to remove authentication. Peers reusing
exponents is already entirely permissible in IKE. Authenticating a
reused exponent does not change the problem caused by reusing
an exponent. I don't even know what "too short DH groups" are but
if you can do it in IKE with authentication then what's the issue that
is introduced when you take away authentication?

  I welcome the new interest in formal security proofs in the IETF but
I don't think this particular charter change compels one.

  regards,

  Dan.