Hi Usama, Thanks for the detailed questions, and apologies for the slow response. Thank you as well to Jack for reading the draft and providing correct answers to many of the questions posed. I'm a bit surprised Jonathan hasn't chimed in yet, given his deep involvement in the analysis and longstanding interest in this area. In any case, let me try to answer as many questions as I can.
There really was formal analysis behind this work, but the public trail is a bit scattered. The best public references I can point you to are RFC 9261 (https://www.rfc-editor.org/rfc/rfc9261), the shepherd write-up (https://datatracker.ietf.org/doc/draft-ietf-tls-exported-authenticator/shepherdwriteup/), the IETF 101 security-analysis slides by Cas Cremers and Jonathan Hoyland (https://www.ietf.org/proceedings/101/slides/slides-101-tls-sessa-exported-authenticators-security-analysis-00.pdf ), Jonathan's retrospective (https://blog.cloudflare.com/exported-authenticators-the-long-road-to-rfc/), Jonathan's thesis abstract (https://pure.royalholloway.ac.uk/en/publications/an-analysis-of-tls-13-and-its-use-in-composite-protocols/), and the follow-on Layered Exported Authenticators draft (draft-hoyland-tls-layered-exported-authenticator-00). On the formal-model question: Section 9 points to SIGMAC and RFC 8446 Appendix E.1.6 as the relevant analysis framing. The shepherd write-up says the draft received formal security review from Cas and Jonathan. The RFC itself only says that Karthikeyan provided suggestions for Section 9. I do not know of a public Karthik-authored ProVerif model for EAs that I can point you to. The most visible public trail I know of is Jonathan's, and that work is Tamarin-oriented rather than ProVerif-oriented. On implementations: the shepherd write-up says there were at least two implementations by independent parties at the time, but Sean said that he could not recover their names from the archive. I do not have a better public implementation list to point you to today. The original motivating use case for this draft was HTTP Secondary Certificates (https://datatracker.ietf.org/doc/draft-ietf-httpbis-secondary-server-certs/), which is currently inactive. This draft was also cited in a previous attempt to port modern PAKEs to TLS, which was implemented at Cloudflare but never widely deployed (https://github.com/cloudflare/opaque-ea). On the Section 9 paragraph, the intended reading is roughly this: First, "independent" is not meant to mean "independent of the Authenticator Request." In the request/response case, the authenticator is clearly bound to the request: certificate_request_context is echoed into the Certificate, the authenticator transcript includes the request when present, and the context value must be unique within a connection. So the request and context are definitely part of what is being bound. What "independent" is trying to get at is that separate authenticators are not recursively chained to each other by the base RFC. Second, "unidirectional" is best read as a property of each individual authenticator, not as a statement that the protocol only works in one direction overall. RFC 9261 supports both client-generated and server-generated authenticators, but each authenticator is created by one side and verified by the other. The exporter labels differ depending on whether the sender is the client or the server. Third, "this property" in the first bullet is mainly referring to that independence across authenticators. A server can prove authority over identity A and authority over identity B on the same TLS connection, but the base RFC does not make EA(B) a proof layered on top of EA(A). That is exactly the kind of gap Jonathan's later Layered EAs work was trying to address. So base EAs are bound to the TLS connection and to the specific request/context that produced them, but they are not automatically chained together into a single compound proof over a set of multiple identities. That is also why I think Jack's explanation in the thread gets at the intended meaning pretty well. On "state" and "TLS layer": I did not mean that there is literally no state anywhere. There is obviously implementation and application state around uniqueness of certificate_request_context, validation, and whether an application chooses to act on a validated authenticator. What I meant is that EAs do not introduce a new TLS state-machine transition analogous to renegotiation or TLS 1.3 post-handshake authentication. They reuse TLS handshake message syntax and are often best implemented inside the TLS library, but they are carried at the application layer and their semantics live above the TLS state machine. That is also why the RFC introduction frames EAs as a building block for application protocols rather than a TLS-native authentication transition: unlike renegotiation, they do not require changes at the TLS layer; unlike TLS 1.3 post-handshake authentication, they do not add state to the TLS state machine; and support negotiation and authentication-error handling are left to the application protocol. Relatedly, the sentence about an application relying on semantics associated with certificate_request_context is intended pretty literally. The context is opaque to TLS, must be unique within a connection, and should generally be unpredictable, but the application is free to choose a value that also corresponds to some existing application data structure or higher-layer meaning. During IESG review, I argued against standardizing an API that would only generate a random value, precisely because an application may want to use that field for its own semantics (https://mailarchive.ietf.org/arch/msg/tls/mzCBPeijLeGV27FGO10v1yWt_bc/). On your ProVerif modeling move: adding an explicit application-level check that ties certificate_request_context to additional data seems like a reasonable way to model stronger application semantics, but I would view that as an application-level strengthening on top of RFC 9261 rather than something required by the base RFC. The base RFC requires that the context be echoed and bound into the authenticator transcript; anything stronger than that comes from the higher-layer protocol using EAs. On the terminology nits ("EA" vs "Exported Authenticator" vs "Authenticator" capitalization differences, or "exporter value" vs "exported value"): those are editorial inconsistencies and an oversight on my part as author, not an attempt to distinguish different protocol objects. I hope this helps. I agree the public trail is harder to reconstruct than it should be. Best, Nick On Wed, Feb 4, 2026 at 4:08 AM Muhammad Usama Sardar <[email protected]> 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 > > _______________________________________________ > TLS mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
