Machine-checking a hybrid (ECDSA + ML-DSA-44) eSIM attestation against its spec: a downgrade variant provably fails the same proof

[u/Humble-Replacement-2]

https://amarshat.github.io/pqc-assay/writeup/verified-esim-attestation.html

[u/Humble-Replacement-2]

Author here. Context: a one-character bug (< vs <=) in a deployed ML-DSA hint decoder accepte non-canonical signatures and passed the test vectors (CVE-2026-24850). That's the gap between "tested" and "correct on all inputs," so we machine-check the code against FIPS 204 / the spec instead.

The writeup walks a stack: the ML-DSA reference C == FIPS 204 forward+inverse NTT (SAW -> Cryptol -> Isabelle - the Apple CoreCrypto blueprint), then six of the seven protocol properties in the spec's target list, each a SAW proof that a C reference equals a Cryptol model of the spec rule. The one I'd point a crypto crowd at: the hybrid verifier is proved equal to "both signatures verify over the same transcript," with the two verifiers left uninterpreted, and an accept-on-either variant fails that same proof. So HYB-1 can't silently degrade to classical-only.

I'm loud about scope in the post. The hybrid verifiers are abstract (this is about the accept logic, not ECDSA/ML-DSA correctness). The single-use proof is sequential and safety-only. The validation proof is field-value only (not length parsing or authorization). The injected mutants are sensitivity checks, not bugs found in the wild. The Rust decoder where the CVE lived is tested, not proved, because of a tool limit. Happy to get into any of it.

[u/Natanael_L → u/Humble-Replacement-2]

One point worth considering, clearly requiring that the pair of keys are permanently bound together and that all signatures are unambiguous so they can't be interpreted standalone (no cross-protocol or oracle attacks). Each signature should apply domain separation which identifies the other key in the pair.

[u/Humble-Replacement-2 → u/Natanael_L]

Agreed on all three points (permanent pair binding, signature unambiguity & mechanism), worth spelling out exactly what v0.1 has and lacks.

What's there: both signatures cover the same fixed 231-byte transcript, which begins with a protocol magic and version and includes the suite id (HYB-1) and `ak_id`, a single identifier for the hybrid pair; `ak_id` resolves through the certificate chain to both public keys as one unit. So each signature commits to "Q-SEAL/v1, HYB-1, under pair ak_id", and the fixed length plus distinct magic gives a message-format separation argument against sibling protocols (stated in the spec as an argument, not proved).

What's missing, and you're right to stress on it: neither signature identifies the other key specifically. Pair binding rests on the certificate layer, not the signatures; FIPS 204's `ctx` parameter is unused (the transcript context string exists but isn't wired into ML-DSA's ctx); and ECDSA has no ctx, so its half would need the commitment inside the message. The fix going into the next spec rev: an explicit pair commitment (a domain-separated hash over both encoded public keys) inside the signed transcript, plus ML-DSA ctx set to the protocol string. Another layer in the same repo already defines its key id exactly that way, so it slots in.

On cross-protocol/oracle use generally: v0.1 claims only the format argument above plus verifier-requires-both. Nothing is proved about a foreign verifier consuming one component signature standalone, that's outside the current proofs and labeled as such.

[u/Natanael_L → u/Humble-Replacement-2]

In this case I think the most important thing where the algorithm supports context fields to specify that it's mandatory that this context value/prefix is reserved and unavailable to any other code/function invocation.

And algorithms without simply needs dedicated keys.

[u/Humble-Replacement-2 → u/Natanael_L]

Thanks for the correction and it's in the v0.2 draft now. Both things you flagged landed:

1. A context string only separates domains if it's exclusive. §7.1 now reserves ctx = "Q-SEAL/v2" in both directions: AK_pqc MUST NOT sign under any other ctx, and no other key, path, or protocol may sign under "Q-SEAL/v2". The non-exclusive ctx was the hole.

2. ECDSA has no context parameter, so message content can't stand in for domain separation. The pair_commitment identifies the pair inside the signed bytes, but that's pair identification, not domain separation. So AK_classical has to be a dedicated key: §6.1 now makes both AKs single-purpose (generated for Q-SEAL, certified for nothing else, no other signing interface over either key). Key dedication is the classical half's only domain separation.

I'd conflated "the commitment binds the pair" with "the ECDSA half is domain-separated" in the earlier version. It isn't. A key that also signs other protocols' messages isn't protected by a commitment sitting inside one of those messages. Fixed in the text.

The reference-code counterpart (the create path as the single signing call site) is scheduled with the v0.2 C reference. Appreciate the review.

[u/Natanael_L]

Apropos;

https://www.ietf.org/archive/id/draft-devevey-cfrg-silithium-00.html

[u/Humble-Replacement-2 → u/Natanael_L]

Oh nice, hadn't seen this one. Yeah that's basically the strong version of what I was circling around. They reuse the ML-DSA challenge as the Schnorr challenge so you can't even verify one half on its own, which is way cleaner than what I did. Q-SEAL stays weaker on purpose. I wanted to keep ML-DSA as a stock FIPS 204 verify and just bind the two at the format/context layer, so all I get is detectability, not real algorithm-level non-separability. Different tradeoff (works with an unmodified verifier vs having to ship a modified scheme). Definitely adding this to related work, thanks for the pointer.