Re: [TLS] [kitten] Fwd: Last Call: <draft-ietf-kitten-tls-channel-bindings-for-tls13-09.txt> (Channel Bindings for TLS 1.3) to Proposed Standard

[Dave Cridland <[e-mail]>]

On Tue, 9 Nov 2021 at 16:01, Jonathan Hoyland
<[e-mail]> 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.

SCRAM *already* includes a nonce in its hash calculations. Your
proposal is to include another, to avoid an unspecified attack.

> 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.

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.

Dave.