Hi Dave,

On Tue, 9 Nov 2021 at 16:13, Dave Cridland <[email protected]> wrote:

> On Tue, 9 Nov 2021 at 16:01, Jonathan Hoyland
> <[email protected]> wrote:
> >
> > Hi All,
> >
> > My specific solution is to simply include a different fixed string for
> each variant of SCRAM and GSS-API, and ideally a nonce.
>
> I think you may mean SASL and GSS-API, but more probably I think you
> need to decide what it is you mean.
>
>
I meant what I wrote.

SCRAM *already* includes a nonce in its hash calculations. Your
> proposal is to include another, to avoid an unspecified attack.
>
>
Firstly, the proposal under question is *NOT* just for SCRAM, it is for an
arbitrary number of unspecified protocols. And the nonce is to prevent
messages being moved between runs of an upper level protocol over a single
TLS channel.


> > Given that applications will have to update their stacks anyway to
> accommodate the new fixed string in the current proposal I don't see that
> as a hugely difficult proposition.
> >
> > The goal of labels in material that is used to derive keys (yes,
> material that is used to derive keys is necessarily secret, yes material
> derived from keys is not necessarily secret), is to exclude classes of
> attack.
> > It is good protocol design.
> >
> > One of the things use of a TLS channel binding gives you is protection
> for the upper level protocol against TLS being MITMed.
> > Using a fixed string for multiple protocols probably gives you that
> protection (assuming the channel binding is correctly agreed by both sides).
> >
> > Using a distinct channel binding, even if the upper level protocol is
> not secure, means that if both sides agree on the channel binding they
> agree on the intent of the upper layer protocol, i.e. it gives you some
> level assurance that the client and server agree on what was intended.
> > This eliminates classes of attack such as message confusion.
> > Adding this protection costs virtually nothing, given that you are
> _already_ commiting to updating this section of code (no code currently
> makes this specific call to the TLS-Exporter interface).
> > Leaving it out means that people like me who do formal analysis can't
> reasonably analyse these designs.
> > I build models of protocols and prove they meet certain properties.
> > The only way to keep that analysis viable (we're already talking
> hundreds of hours of work) is to eliminate classes of attack wholesale.
> > Yes, you can add unique and clever protections into every sub-protocol,
> but it makes formally proving anything about the security exponentially
> harder (and yes, I mean that in the literal / mathematical sense).
>
> SASL (and GSS-API) are pluggable authentication systems which means
> that if you want a formal proof (or even just a finger-in-the-air
> back-of-the-envelope one) you have to do it against a specific SASL
> (or GSS-API) mechanism.
>

That's correct. If you want to do a proof you have to do it against a
specific mechanism.
The problem is that the analysis has to include all sources of protocol
messages from the same key space (yes, again. I know that channel bindings
are not keys. Yes I know that channel bindings are not required to be
secret.)
With the draft as proposed that is an arbitrary number of protocols,
including any that may be written in future.
Even if you managed to do some huge analysis of anything that falls into
this space, it would immediately be invalidated the moment any new version
or design came along.


> Without knowing the mechanism, it's impossible to perform a formal
> proof, because you don't know how the channel binding is exchanged and
> proven, and so you would be missing an absolutely crucial part of your
> model.
>
>
Firstly, even without knowing the mechanism there are lots of things we can
prove or that we assume.
For example, I assume that an attacker cannot decrypt messages for which it
does not have the key.
Most formal analysis is based on a fairly small set of assumptions and
standard proofs.
One key assumption is that different protocols use unrelated keys. (Yes,
again. I know that channel bindings are not keys. Yes I know that channel
bindings are not required to be secret.)
If you include channel bindings in your key derivation then you cannot
assume that the keys are unrelated.

Now it's totally possible to prove your protocol is universally composable
irrespective of channel bindings, but if you're proving that you might as
well just drop the TLS layer.

Second: The issue isn't about picking a specific mechanism, the issue is
that I can't ignore other mechanisms.

Regards,

Jonathan



> Dave.
>
_______________________________________________
TLS mailing list
[email protected]
https://www.ietf.org/mailman/listinfo/tls
              • ... Simo Sorce
              • ... Jonathan Hoyland
              • ... Ruslan N. Marchenko
              • ... Alexey Melnikov
              • ... Simon Josefsson
              • ... Sam Whited
              • ... Jonathan Hoyland
              • ... Dave Cridland
              • ... Jonathan Hoyland
              • ... Dave Cridland
              • ... Jonathan Hoyland
              • ... Sam Whited
              • ... Ruslan N. Marchenko
              • ... Sean Turner
              • ... Salz, Rich
              • ... Sam Whited
      • Re: [TLS] ... Eric Rescorla
  • Re: [TLS] Fwd: Last... Ross, Michael D (54510) CIV USN NIWC ATLANTIC SC (USA)

Reply via email to