[alex]

From the rustls provider analysis in #991: loading a server key with PrivateKey::from_crt runs at 0.10–0.20 of aws-lc-rs's speed, because from_crt checks the key with a whole constant-time private-key operation on 0. This PR is the spec half of replacing that with a cheap, proven check; the implementation follows in a separate PR, per "One kind of change per PR".

Trust change (Spec/)

This is a spec change. It adds no ISA semantics and does not touch TCB/.

• Spec/Rsa.lean: crtKeyValid and checkCrtKey. These are keyValid/checkKey (BoringSSL's RSA_check_key) with the checks of d dropped, because the private-key operations never use d:

  • modulusValid n k and exponentValid e
  • p q = n
  • dP < p - 1 and e dP ≡ 1 (mod p - 1)
  • dQ < q - 1 and e dQ ≡ 1 (mod q - 1)
  • qInv < p and q qInv ≡ 1 (mod p)

  keyValid's p < n and q < n are left out. They follow from p q = n once neither factor is 1, and the congruences modulo p - 1 and q - 1 already rule that out, because e ≥ 3.

• Spec/Rsa/Contract.lean: checkCrtKeySig, checkCrtKeyContract and checkCrtKeyApi for vg_rsa_check_crt_key. They mirror vg_rsa_check_key's signature, preconditions, leak and docs without d:

  • it returns 1 if checkCrtKey holds and 0 otherwise
  • it writes nothing but scratch
  • it is constant time except for n and e

• VerifiedGarbageTest/Rsa.lean: checkCrtKey on the CAVP-derived keys that checkKey is already tested on:

  • it accepts each key, with p and q either way round and with leading zeros
  • it rejects each condition failing on its own, including p = 1
  • for a key it accepts, privateChecked gives 0 for 0

What from_crt will guarantee

Today from_crt accepts a key exactly when privateChecked(n, e, 0, p, q, dP, dQ, qInv) is ok. That holds when n and e are valid, p q = n, qInv < p, and the CRT result m for 0 passes m^e ≡ 0 (mod n). The last condition only fails in degenerate cases such as dP = 0.

After the implementation PR, from_crt will accept exactly the keys checkCrtKey accepts. That guarantee is stronger in both directions:

• It still implies everything private_op relies on: modulus valid, p q = n and qInv < p. So a refusal from vg_rsa_private_checked still means the input is out of range.
• It implies dP, dQ ≥ 1, so 0's result is 0 and passes the old check. Every key the new check accepts, the old one accepted too.
• It also rejects keys whose CRT values are inconsistent with e at load time, with InvalidPrivateKey. Today those load and then fail every operation with Fault.

private_op's fault check stays as it is.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PqW9NMssoiBx9i4PpksckL

---

Generated by Claude Code