curve!: use constant-time compressed Ristretto equality testing#669
Conversation
|
Note that dalek-cryptography/subtle#131 would also supply a marker trait that could be useful here to signal this "all equality is constant time" behavior. |
| /// The Ristretto encoding is canonical, so two points are equal if and | ||
| /// only if their encodings are equal. | ||
| #[derive(Copy, Clone, Eq, PartialEq, Hash)] | ||
| #[derive(Copy, Clone, Hash)] |
There was a problem hiding this comment.
While it's unlikely to cause real-world breakages, I believe this is technically a breaking change.
Here's an example of what is possible with a derived PartialEq which won't be possible with this change: https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=33e85cff0772c968767a0417a8a7a541
There was a problem hiding this comment.
Interesting! I was not aware of this behavior. Thoughts on the tradeoff between the functionality and the implications of the breaking change?
There was a problem hiding this comment.
I would strongly agree with making this change if it weren't for the potential breakages
There was a problem hiding this comment.
Ought this PR stay open until the next breaking release? I remain of the opinion that the benefit (consistency with safety goals) outweighs the cost.
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
2 times, most recently
from
e03cc24 to
326eeda
Compare
|
Yeah that's unfortunate. I really doubt anyone has ever used a |
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
from
326eeda to
f36fd77
Compare
|
Given that this seems to be a desired change, I'll keep it open for the next breaking release. Feel free to close if this isn't the case! |
AaronFeickert
changed the title
AaronFeickert
changed the title
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
from
f36fd77 to
235a59d
Compare
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
2 times, most recently
from
304104b to
07c098f
Compare
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
from
07c098f to
fb15923
Compare
AaronFeickert
force-pushed
the
compressed-eq-is-ct
branch
from
fb15923 to
4c3fd82
Compare
* Verify mul_bits_be Montgomery ladder and ProjectivePoint::identity Prove correctness of MontgomeryPoint::mul_bits_be (Algorithm 8 from Costello-Smith 2017) for computing [n]P on the Montgomery curve. - Enhanced differential_add_and_double spec with: - Limb bounds preconditions/postconditions (fe51_limbs_bounded at 54/51) - Ladder-step postconditions expressing [k]P, [k+1]P → [2k]P, [2k+1]P * Verify ProjectivePoint::identity(): * Prove bounds for differential_add_and_double field operations * Strengthened ProjectivePoint::identity spec with 51-bounded postconditions * Clean up mul_bits_be proof and tighten bounds assertions * Complete differential_add_and_double and mul_bits_be verification * Structure Montgomery ladder verification using axiom-based approach: ## Architecture (Costello-Smith 2017) 1. **Algebraic Specs** (montgomery_specs.rs) — Algorithms 1 & 2: - `spec_xdbl_projective`: U' = (U+W)²·(U−W)², W' = [(U+W)²−(U−W)²]·[...] - `spec_xadd_projective`: U' = [...+...]², W' = u_diff·[...−...]² 2. **Axioms** (montgomery_curve_lemmas.rs) — Equations 9 & 10: - `axiom_xdbl_projective_correct`: xDBL computes [2]P - `axiom_xadd_projective_correct`: xADD computes P+Q 3. **Implementation Proof** (montgomery.rs): - differential_add_and_double outputs match spec functions - Axioms applied to get scalar multiplication correctness - mul_bits_be loop invariant updated with projective representation * Fix Montgomery ladder infinity representation Tighten the projective (U:W) representation predicate for infinity to exclude the degenerate (0:0) case (require U!=0 when W==0). This avoids unsound uses of x-only formulas (xADD/xDBL) and lets the Montgomery ladder proof apply xADD/xDBL axioms without introducing new assume()s in differential_add_and_double. * Improve Montgomery curve comments and cleanup unused lemmas * Remove unused trivial lemmas, add rlimit notes * Refactor differential_add_and_double proofs to assert...by style * Add ladder_invariant spec fn to simplify mul_bits_be proof * Address PR review comments Co-authored-by: Cursor <cursoragent@cursor.com>
3 participants
In line with the safety goals, this PR ensures that
CompressedRistrettoequality testing is always done in constant time.Previous work in #229 implemented
ConstantTimeEqforCompressedRistretto, but this is not used forEqequality testing. It's already the case thatRistrettoPointandScalarperform all equality testing in constant time; this PR unifies this behavior for compressed points as well.BREAKING CHANGE: As noted by @tarcieri, this can break certain uses of
match.