Hi everyone, I am interested in collaborating on new ProVerif models that explore PQ crypto as well.
Earlier this year, I forked Sardar et al.'s open-source ProVerif models — released alongside the Identity Crisis academic paper — to model the flaws identified by CVE-2026-33697 [0], a vulnerability reported for an intra-handshake attestation implementation of TLS + RA, along with a proposed mitigation [1]. While that model is focused on a real-world deployment, both of my repository clones that Usama identified in the Editor's Copy are subject to the same modeling artifacts [2], [3]. This includes the Cocos AI model itself, which inherits the same DH commutativity limitations Usama has identified [4]. > We welcome feedback from the community on how to fix the ProVerif proofs preserving the cryptographic soundness [5]. To help facilitate this, I worked to replace the idealized DH key exchange with an idealized KEM abstraction reflecting the current work in draft-ietf-tls-mlkem-07. The goal was to confirm that the naive attestation binder at the root of CVE-2026-33697 fails in the same way under ML-KEM as it does under classical DHKE — and to verify that no new attack surface opens in the transition. Helpful insights from Nadim [6] and Yaakov [7] in the thread informed this work along the way. Based on the results, I believe the basic groundwork is now in place for a symbolic representation of standalone ML-KEM in TLS 1.3 [8]. These results build directly on the iterative work that Bhargavan et al. and Sardar et al. have made available to the public — thank you! It is worth noting that my forks include queries designed to evaluate the security properties of TLS + RA in combination, with fixes based on personal I-Ds submitted to the SEAT WG. As such, if there is any sustained interest beyond the SEAT WG, I would be happy to build from an alternative version of my recent revisions that evaluates standalone ML-KEM in TLS 1.3 without RA integration. As per the TLSWG chairs' request [10], any detailed back-and-forth on the models themselves should have the TLSWG removed moving forward; I have copied the UFMRG in case there is any interest there (hence the heavy citations). Other than that, I can report that the ML-KEM variant appears to behave as I expected, which is an open invite for additional scrutiny by any interested experts :). Cheers, Nathanael p.s. Regarding copyright attribution — Usama has indicated that he and co-authors may have a number of models currently under peer review or not yet publicly available that are related to the same kind of research [9]. To prevent any kind of ambiguity, I have used the Apache 2.0 copyright notice to clearly delineate my independent contributions from those of Sardar et al. If there is any interest from the TLSWG, SEAT, or UFMRG (copied, hence the heavy citations) for open collaboration based on the models I have linked, I am quite happy to update how attribution is referenced of course. [0] https://github.com/ultravioletrs/cocos/security/advisories/GHSA-vfgg-mvxx-mgg7 [1] https://github.com/nathanaelritz/formal-spec-id-crisis/tree/main/cocosai/ [2] https://github.com/muhammad-usama-sardar/risks-of-mlkem/blob/f8de07565c7bf812de2294445abfd46fd6f3f09c/draft-usama-tls-risks-of-mlkem.md?plain=1#L209 [3] https://github.com/muhammad-usama-sardar/risks-of-mlkem/blob/f8de07565c7bf812de2294445abfd46fd6f3f09c/draft-usama-tls-risks-of-mlkem.md?plain=1#L210 [4] https://github.com/nathanaelritz/formal-spec-id-crisis/blob/main/cocosai/dhe/cve/tls-lib-simple.pvl#L66 [5] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#section-3-6 [6] https://mailarchive.ietf.org/arch/msg/tls/hmZH_Rkibo55nS62hQeo3Lx-TqQ/ [7] https://mailarchive.ietf.org/arch/msg/tls/CxQw8uLohg6lhPpyn8INlLw1TLQ/ [8] https://github.com/nathanaelritz/formal-spec-id-crisis/tree/main/cocosai/mlkem/ [9] https://muhammad-usama-sardar.github.io/risks-of-mlkem/draft-usama-tls-risks-of-mlkem.html#section-4-6.3.1 [10] https://mailarchive.ietf.org/arch/msg/tls/SG10yIg7zjl5dJP06p6LlK-slQ0/ On Thu, 28 May 2026 at 14:25, Nadim Kobeissi <[email protected]> wrote: > You know what? I did my PhD work mostly in ProVerif. I’ll just go and > write some new models myself. I’ll keep you all posted, if that’s how > you’re going to be. > > Nadim Kobeissi > Symbolic Software • https://symbolic.software > > On 28 May 2026, at 10:20 PM, Nadim Kobeissi <[email protected]> > wrote: > > Hi Eric, > > I think this would be reasonable if the discussion had veered off to, say, > some kind of high-level ProVerif tutorial, or worse, some eggheaded > discussion on esoteric properties of Horn clauses as they apply to > ProVerif. But neither of these are true; the discussion was still very much > grounded in how to best apply ProVerif to TLS 1.3, and came after I had > done hours of work today trying to explain the impact of the three papers > you cited on the discussion. > > In that light, the chairs’ decision feels quite stifling. > > Nadim Kobeissi > Symbolic Software • https://symbolic.software > > On 28 May 2026, at 10:17 PM, Eric Rescorla <[email protected]> wrote: > > I agree with Sean. This is not the right place to debug/refine the formal > models. It would be the right place to report on the results of the > modelling work/ > > -Ekr > > > On Thu, May 28, 2026 at 12:59 PM Nadim Kobeissi <[email protected]> > wrote: > >> I did an actual real-life double-take reading this. Discussions formal >> models of TLS are off-topic for this list? >> >> Is this a joke? >> >> Also, it’s ProVerif, Sean, not “pro-verify”. >> >> Nadim Kobeissi >> Symbolic Software • https://symbolic.software >> >> On 28 May 2026, at 9:26 PM, Sean Turner <[email protected]> wrote: >> >> Please take the detailed discussion about the pro-verify model off list. >> >> Discussions about the specifics of any formal analysis model are off >> topic for this mailing list as well as in-person/virtual TLS WG meetings. >> >> Please note that what is in scope WRT formal analysis is the draft, the >> claims, and the results of the formal analysis. The specific details about >> how the formal analysis is arrived at is not on topic. >> >> Thanks, >> Joe and Sean >> >> On May 28, 2026, at 12:05, Muhammad Usama Sardar < >> [email protected]> wrote: >> >> Hi Yaakov, >> >> Thanks for your valuable input. That's indeed very useful. Some quick >> thoughts inline, since you requested. I will report back more details after >> carefully and thoroughly double-checking everything. >> >> Whenever you have time, I will appreciate a couple of clarifying >> questions inline. In case it helps, [0] has full details of my ProVerif >> modeling and its semantics. >> >> Kindly let me know if I misunderstood some of your comments: >> On 28.05.26 16:06, Yaakov Stein wrote: >> >> The fact that commutativity is blocking your formal correctness proof >> must be an artifact. >> There are many commutative schemes that are not safe (how about adding >> two partial keys?), >> and many non-commutative ones that are (as most informally believe for >> KEMs). >> >> Sure, there are several cryptographic proofs for DHKE which are the basis >> for this property. I will add those references to be clear. >> >> I am not a ProVerif expert, but I waded through your code, >> and think I understand where the issue appears and what to do about it. >> >> Thanks a lot. Really appreciate your time. >> >> As I believe you said (but couldn’t find the email), the commutativity of >> DH is posited here >> (and mentioning “commutativity” or “symmetry” in a comment would make it >> easier to find): >> >> Sure, I'll add comments for easier search. Thanks for your valuable >> feedback. If some areas of code were hard to understand or need more >> comments, I'll love to hear that to make it more readable for other authors >> so that they can extend the models in future. >> >> fun dh_ideal(element,bitstring):element. >> equation forall x:bitstring, y:bitstring; >> dh_ideal(dh_ideal(G,x),y) = >> dh_ideal(dh_ideal(G,y),x). >> >> Now, in >> fun dh_exp(group,element,bitstring):element >> reduc forall g:group, e:element, x:bitstring; >> dh_exp(WeakDH,e,x) = BadElement >> otherwise forall g:group, e:element, x:bitstring; >> dh_exp(StrongDH,BadElement,x) = BadElement >> otherwise forall g:group, e:element, x:bitstring; >> dh_exp(StrongDH,e,x) = dh_ideal(e,x). >> >> when one side computes: >> let gxy = e2b(dh_exp(g,gy,x)) >> while the other side does: >> let gxy = e2b(dh_exp(g,gx,y)) >> they are provably equal. >> >> Please note that gxy,g,x,y etc. are all local variables of Client and >> Server processes. For simplicity, ignoring transformation 'e2b' and >> assuming StrongHash and there is no BadElement, Client process will have: >> >> gxy = gy^x >> >> and Server process will have: >> >> gxy = gx^y >> >> These are two separate 'terms' in ProVerif. ProVerif is unable to >> distinguish between the two. Could you please clarify how without the >> "equation" they can both be equal? >> >> To be clear: is your understanding that even if I remove the 'equation,' >> the proof should still work as-is? I think it is an essential ingredient in >> the proof. >> >> So, you are not really using the fact that either side could have >> initiated the TLS >> and we would get the same shared secret (which is not what happens in >> client-server usage anyway) >> >> To clarify, my understanding is that the client is by definition the >> endpoint which initiates the connection, consistent with RFC8446bis, Sec. >> 1.1 [1]. >> >> I know that some papers in literature have taken the position that you >> are mentioning. I do not object to that, but to the best of my knowledge, >> they haven't found any *real* additional attacks. >> >> you are just relying on it to prove that the two sides end up with the >> SAME shared secret >> in a single TLS session. >> >> Could you please explain this point? I think this is the main point of >> confusion. See my clarification of the two 'gxy' above. >> >> >> >> Now, KEMs do not build a shared secret from symmetric participation of >> two sides, >> but they still end up with the two sides arriving at the same shared >> secret. >> This arises from one side generating the secret (and thus knowing it) >> and the other side decrypting a public key encrypted version (and thus >> also learning it). >> >> So, you need to model *decap(sk,ct) produces the same shared secret ss* >> and drop this in, instead of agreement from commutativity. >> >> It didn't work for me. I think at the very least something to replace >> commutativity is required. >> >> Something like (forgive my not being an expert in ProVerify syntax) >> >> no worries at all. This is still very useful. I think we are largely in >> sync. Syntax is no problem. Please don't worry about that. >> >> fun pk(kem_sk): kem_pk. >> >> fun encap_ct(kem_pk, bitstring): kem_ct. >> fun encap_ss(kem_pk, bitstring): kem_ss. >> >> fun decap(kem_sk, kem_ct): kem_ss. >> >> Mind clarifying what do you have 'bitstring' for? That's the only >> difference I have (using your symbols): >> >> fun encap_ct(kem_pk): kem_ct. >> >> fun encap_ss(kem_pk): kem_ss. >> >> I have followed the NIST FIPS 203: Algorithm 20, p. 37 [2]. It seems that >> the algorithm takes as input only variable (ek in [2]). Please correct me >> if I am misunderstanding something or missing something in the FIPS 203 >> spec. >> >> Now, the last thing I want is for this to produce the result that pure >> MLKEM is sufficient now. >> The real missing element in your code is not the removing of the >> commutativity artifact, >> but rather modeling different failure modes: >> >> Sure, the purpose of both Karthik et al.'s work as well as mine was to >> study security under non-PQ threat model. I started updating it for the >> simplest scenario (mode 1 in your proposal). Once the simplest PQ case >> works out, I will add the four scenarios as per your guidance. >> >> >> 1. There is no CRQC, and neither ECC nor MLKEM are broken (hybrid and >> pure are proven safe) >> 2. There is no CRQC, but someone finds a classical break for MLKEM >> (in which case hybrids are OK but pure MLKEM is not) >> 3. There is a CRQC and thus ECC is broken, but MLKEM withstands all >> classical and quantum attacks (and pure MLKEM is proven correct), >> 4. There is a CRQC and thus ECC is broken, and someone finds a >> classical or quantum break for MLKEM (in which case we expect nothing to >> be >> safe) >> >> (I left out some less likely cases such as ECC breaking classically and >> MLKEM not.) >> >> I would appreciate hearing from you what you think about both points. >> >> Please feel free to share if more explanation on any of points will be >> helpful. Would be happy to explain anything unclear. >> >> Kind regards, >> >> -Usama >> >> >> [0] >> https://www.researchgate.net/publication/396593308_Perspicuity_of_Attestation_Mechanisms_in_Confidential_Computing_General_Approach >> >> [1] >> https://www.ietf.org/archive/id/draft-ietf-tls-rfc8446bis-14.html#section-1.1 >> >> [2] https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.203.pdf >> _______________________________________________ >> 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] >> >> >> _______________________________________________ >> 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] >
_______________________________________________ TLS mailing list -- [email protected] To unsubscribe send an email to [email protected]
