[ 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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
