[TLS] Re: Clarification on security considerations of RFC9261

[Muhammad Usama Sardar <[e-mail]>]

Hi UFMRG and CFRG,

I didn't get any answer/opinion at TLS WG. So I wanted to check if 
someone here has any answer/opinion.

Best regards,

-Usama


On 12.02.26 13:59, Muhammad Usama Sardar wrote:
>
> Just a reminder that it's /not/ necessary to answer /all/ the 
> questions :) Whatever answers/opinions anyone has are welcome.
>
> Given lack of clarity, we are basically making assumptions, which may 
> not match the intentions of the WG.
>
> Thanks.
>
> -Usama
>
>
> On 03.02.26 21:08, Muhammad Usama Sardar wrote:
>>
>> [ Sorry for the length ]
>>
>> Hi Nick, all,
>>
>> Thank you for the work on RFC9261. We found it a useful foundation 
>> for our work.
>>
>> # *Context*
>>
>> Four developers (Peg Jones from Flashbots, Markus Rudy from Edgeless 
>> Systems, Ayoub Benaissa from Zama, and Pavel Nikonorov from GA4GH and 
>> Elixir Europe) are developing implementations of RFC 9261. I am doing 
>> the formal analysis in ProVerif. We request the following clarifications.
>>
>> # *Scope*
>>
>> I basically care about TLS 1.3 only. While many things apply to DTLS 
>> 1.3 as well as TLS 1.2, the scope of my questions is only limited to 
>> TLS 1.3 /only/.
>>
>> Of the three options in Section 3, I care about Server 
>> Authentication. That is, Client Authentication and Spontaneous Server 
>> Authentication are out of scope of this email.
>>
>> While Authenticators can be conveyed "out of band" as mentioned in 
>> RFC (which I don't really see why), let's say I put it out of scope. 
>> When there is already an established connection, then I think it is 
>> preferable to use that. So let's say Authenticator Request and 
>> Authenticator are sent over the connection established by the 
>> handshake (and hence "out of band" being out of scope).
>>
>> For further simplicity, let's say Server does not send 
>> CertificateRequest during the handshake, so the client authentication 
>> is not done during the handshake.
>>
>> # *Known implementation*
>>
>> The only public implementation currently known to us is Cloudflare's 
>> opaque-ea [0], which as acknowledged [1] by Cloudflare, is a partial 
>> implementation of RFC9261. It implements TLS messages here [2] and is 
>> based on mint [3] - a minimal TLS 1.3 stack for learning purposes. Is 
>> there any other open-source implementation?
>>
>> For future, could we please reference the implementations within the 
>> RFCs (either in text or in "additional resources" in datatracker) to 
>> avoid the trouble to find it?
>>
>> The developers are ultimately aiming at code that they will use in 
>> production.
>>
>>
>> # *Security considerations*
>>
>> I agree with the last paragraph of security considerations, but 
>> couldn't parse the 2nd paragraph (see below).
>>
>> ## *Formal analysis in ProVerif*
>>
>> I am trying to understand the security considerations of RFC9261. It 
>> acknowledges Karthik for suggestions on security considerations. Does 
>> someone happen to recall whether he actually did some formal analysis 
>> in ProVerif or was it based on his intuition? If the former, could 
>> someone point me to the analysis? I did check reftls repo [4] which 
>> does not contain it. I also checked his personal repos [5] but could 
>> not find something relevant.
>>
>> I know some formal analysis was done in Tamarin but I would like to 
>> compare my ProVerif model with his model, if he had one.
>>
>> For future, could we please reference the formal analysis within the 
>> RFCs (either in text or in "additional resources" in datatracker) to 
>> avoid the trouble to find it?
>>
>> ## *2nd paragraph *
>>
>> A whole lot of my trouble is understanding what is being reasoned in 
>> this paragraph and how this is leading to the first bullet as a 
>> conclusion. Could someone explain? For example:
>>
>> > Authenticators are independent and unidirectional.
>>
>> "Independent" of what? Authenticator would use the 
>> /certificate_request_context/ from Authenticator Request, 
>> so Authenticator is not independent of Authenticator Request, right? 
>> If Authenticator is independent of Authenticator Request, then what 
>> prevents replay attacks? (Recall Spontaneous Server Authentication is 
>> out of scope of my email. One could argue that is still in scope for 
>> RFC but the quoted statement in RFC comes without qualifier and 
>> logically should apply to all cases.)
>>
>> "Unidirectional" in what sense? The whole idea of RFC9261 in my mind 
>> is to enable the server to send Authenticators too, since after the 
>> handshake, RFC8446bis allows only the Client to authenticate itself 
>> and not the Server [Sec. 4.2.6 and 4.6.2 of 8446bis]. To me, RFC9261 
>> is bidirectional, as both server and client can generate Authenticators.
>>
>> > This property makes it difficult to formally prove that a server is 
>> jointly authoritative over multiple identities, rather than 
>> individually authoritative over each.
>>
>> Which property? I couldn't parse it how it was derived from the 
>> statements above it.
>>
>> ## *State*
>>
>> RFC uses 3x"state" but never defines it. What exactly does it entail 
>> in this context? The most important for me is the one in security 
>> considerations.
>>
>> > The application in possession of a validated authenticator can rely 
>> on any semantics associated with data in the certificate_request_context.
>>
>> I couldn't parse above quoted statement. What does it mean? As per 
>> scope mentioned above, Client validates Authenticator.
>>
>> ## *TLS Layer*
>>
>> RFC uses TLS layer, and I don't find any definition of this in this 
>> document or in RFC8446bis. In particular, does it mean the end of 
>> handshake protocol? Or does it include the Authenticator Request and  
>> Authenticator too? I am a bit confused because Section 7 says the 
>> messages SHOULD be implemented inside the TLS library.
>>
>>
>> # *(Hopefully) some nits*
>>
>> ## *EA vs. "Exported Authenticator" vs. "Authenticator"*
>>
>> EA is used but never defined. Is it any different from "Exported 
>> Authenticator" used in the same sentence?
>>
>> How exactly are both of them different from "Authenticator" defined 
>> in Section 5?
>>
>> ## *Lower-case vs. Upper-case*
>>
>> In Section 3 (and in general), is there a subtle difference between 
>> "Authenticator" and "authenticator"? Similarly, "Authenticator 
>> Request" and "authenticator request".
>>
>> ## *"exporter value" vs. "exported value"*
>>
>> Is there a subtle difference between "exporter value" and "exported 
>> value"?
>>
>>
>> Thanks.
>>
>> -Usama
>>
>>
>> [0] https://github.com/cloudflare/opaque-ea
>>
>> [1] 
>> https://github.com/cloudflare/opaque-ea?tab=readme-ov-file#library-packages
>>
>> [2] 
>> https://github.com/cloudflare/opaque-ea/blob/master/src/expauth/tls_messages.go
>>
>> [3] https://github.com/tatianab/mint
>>
>> [4] https://github.com/Inria-Prosecco/reftls
>>
>> [5] https://github.com/karthikbhargavan
>>