Thanks David for sharing the insights. I naturally support interpretation of what is actually sent/received by the endpoints. Changing it is an unnecessary and additional proof work to maintain my existing formal proofs. A particular challenge seems to be to ensure the thing sent/received vs. the one used links properly to avoid introducing new attack vectors. My intuition is that it may even be hard to ensure completely at /symbolic/ analysis tools, like ProVerif, and may warrant additional /computational/ (cryptographic) proofs, like CryptoVerif.

As you mention, changing it seems to be significant effort for implementations too.

On 11.02.26 16:01, David Benjamin wrote:
On Wed, Feb 11, 2026, 09:15 Muhammad Usama Sardar <[email protected]> wrote:

    In formal model, I always take what is actually sent/received by
    the endpoints. I suspect additional lemmas will be required for
    the proofs if it is not the case.

I think everyone takes this interpretation. Let's not change it.
I can't say for everyone. But I, for sure, would like it not to be changed.

    I like to think of those as addition of new message. In this case,
    RFC 6066 is for TLS 1.2. I don't directly see how this is
    necessarily relevant for RFC8446bis. Is there any RFC where a new
    message was added to TLS 1.3 handshake?


The one we are talking about right now does this? It replaces a message with a different one.
From a formal analysis perspective, it seems to fall in /modification/ of existing messages category since it /replaces/ an existing message, rather than adding a completely new message in addition to the existing ones. Anyway, that doesn't matter much, since your next answer covers all the three cases.

    When that happens, such changes are reflected in the handshake
    transcript.
    Could you clarify what exactly "that" refers to: the last one (new
    message) or all three above?


All of the above.
Thanks for the clarification.

    Indeed some handle the transcript automatically under the
    handshake layer and would /only/ be able to implement this version.
    I don't quite get that "/only/". Whatever layer it is implemented,
    it is still software which -- in principle -- can be changed
    (hardware can be changed, too but a bit more costly). This may
    need some work to re-architecture (just like you were able to) but
    I don't think the reasoning is that they are /not able/ to
    implement the other version.


Yes, I mean that it would be a significant amount of effort and break some core assumptions to implement the other version. It sounds like your formal models are the same.
Yes, as summarized at the beginning of this email, I would expect so.

But it does not sound like anyone wants the other version, so this is all fine.

    If you "take literally", I couldn't follow how you came to
    conclusion "unless it says otherwise", specially given that the
    quoted text says "*always*", independent of whatever the
    extensions define.


It is always the case that updating documents are allowed to override text in the base document.
Sure, but RFC8879 does not seem to update RFC8846. I still don't see how you derive this based on the statement you quoted. Perhaps you meant "unless it says otherwise and updates RFC8446(bis)".

    That's not what we want, both by how real implementations
    work, or by the security goals of the transcript.
    I can't say anything for real implementations but agree for
    security goals from a formal analysis perspective.
    But in TLS we're sloppy enough about messages with and without
    the header that it's worth being explicit.

    Do the headers contain any security-relevant information? If not,
    isn't it intentionally just left over as an implementation choice,
    rather than being sloppy?


I think you misunderstand the comment. It is very, very much not implementation choice whether the decompressed message should contain or not contain the header. You cannot interop if you don't agree here.

Sorry if I misunderstood. It's always unclear to me what exactly "TLS" entails. I interpreted "TLS" in your quoted message to mean "RFC8446(bis)". So, I was saying that from RFC8446bis (and not RFC 8879) perspective.

-Usama


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
TLS mailing list -- [email protected]
To unsubscribe send an email to [email protected]

Reply via email to