Montgomery Ladder Algebraic Correctness

Proves that the Montgomery double-and-add ladder, viewed as an iterated group operation on an abstract abelian group G, computes n · P for a scalar n processed bit-by-bit from MSB to LSB.

Scope

This is the algebraic correctness of the ladder. It does not depend on:

• Any specific field (would specialise to 𝔽_{2²⁵⁵-19} for Curve25519).
• Any specific curve (would specialise to Curve25519's Montgomery form).
• The x-only formulas (dadd, xdbl) — at this level we use the full group operation. The x-only ladder uses the same invariant; showing that the x-only formulas agree with the full group's x-coordinate is a separate algebraic lemma (a well-known 2-page argument, deferred).

What is proved

For any abelian group G, any element P : G, and any natural number n with n.size bits, starting from the state (0 · P, 1 · P) and iterating the ladder step over the bits of n from MSB to LSB, the final state (R₀, R₁) satisfies R₀ = n · P and R₁ = (n + 1) · P.

This is the invariant-based correctness argument: standard folklore dating to Montgomery's 1987 paper, formalised here as a pure induction on bit length.

What is NOT proved

• Field-op correctness. The x-only differential-addition formula dadd(x₀, x₁, x_P) = x(R₀ + R₁) when x_P = x(R₁ - R₀): this is the algebraic identity that makes the x-only ladder work. Proving it requires the full Montgomery-form group law (a case analysis and polynomial identity over the base field). Fiat-crypto proves it in Rocq.

References

• Montgomery, "Speeding the Pollard and Elliptic Curve Methods of Factorization", Math. Comp. 1987.
• Bernstein, "Curve25519: new Diffie-Hellman speed records", PKC 2006.
• Costello & Smith, "Montgomery curves and the Montgomery ladder", IACR eprint 2017/212, §4.

Ladder step

def CatCrypt.Crypto.ECC.ladderStep {G : Type u_1} [AddCommGroup G] (acc : G × G) (b : Bool) : G × G

One step of the Montgomery ladder, operating on a pair of group elements. The state (R₀, R₁) is intended to maintain the invariant R₀ = a · P, R₁ = (a + 1) · P for some running a; a single step with bit b updates a to 2 a + (if b then 1 else 0).

Equations

• CatCrypt.Crypto.ECC.ladderStep (R₀, R₁) b = if b = true then (R₀ + R₁, R₁ + R₁) else (R₀ + R₀, R₀ + R₁)

def CatCrypt.Crypto.ECC.ladderFold {G : Type u_1} [AddCommGroup G] (P : G) : List Bool → G × G

Running the ladder on a list of bits (head = MSB processed first).

Equations

• CatCrypt.Crypto.ECC.ladderFold P [] = (0, P)
• CatCrypt.Crypto.ECC.ladderFold P (b :: bs) = CatCrypt.Crypto.ECC.ladderStep (CatCrypt.Crypto.ECC.ladderFold P bs) b

Key invariant

def CatCrypt.Crypto.ECC.LadderInv {G : Type u_1} [AddCommGroup G] (P : G) (a : ℕ) (st : G × G) : Prop

The invariant predicate: (R₀, R₁) = (a · P, (a + 1) · P).

Equations

• CatCrypt.Crypto.ECC.LadderInv P a st = (st.fst = a • P ∧ st.snd = (a + 1) • P)

theorem CatCrypt.Crypto.ECC.ladderInv_init {G : Type u_1} [AddCommGroup G] (P : G) : LadderInv P 0 (0, P)

Initial state (0, P) satisfies the invariant with a = 0.

theorem CatCrypt.Crypto.ECC.ladderStep_inv {G : Type u_1} [AddCommGroup G] (P : G) (a : ℕ) (st : G × G) (b : Bool) (h : LadderInv P a st) : LadderInv P (2 * a + if b = true then 1 else 0) (ladderStep st b)

Core step lemma: if (R₀, R₁) satisfies the invariant at scalar a, then ladderStep (R₀, R₁) b satisfies the invariant at scalar 2 a + (if b then 1 else 0).

Scalar reconstruction from bits

def CatCrypt.Crypto.ECC.bitsToNat : List Bool → ℕ

Compute the natural number represented by a list of bits, MSB first. bitsToNat [b₂, b₁, b₀] = 4 b₂ + 2 b₁ + b₀ etc.

Equations

• CatCrypt.Crypto.ECC.bitsToNat [] = 0
• CatCrypt.Crypto.ECC.bitsToNat (b :: bs) = 2 * CatCrypt.Crypto.ECC.bitsToNat bs + if b = true then 1 else 0

Main correctness theorem

theorem CatCrypt.Crypto.ECC.ladderFold_correct {G : Type u_1} [AddCommGroup G] (P : G) (bits : List Bool) : LadderInv P (bitsToNat bits) (ladderFold P bits)

Montgomery ladder correctness (algebraic). Running ladderFold P on a list of bits (MSB first) produces a state (n · P, (n + 1) · P) where n = bitsToNat bits.

theorem CatCrypt.Crypto.ECC.ladderFold_fst_eq_nsmul {G : Type u_1} [AddCommGroup G] (P : G) (bits : List Bool) : (ladderFold P bits).fst = bitsToNat bits • P

Corollary — scalar multiplication via ladder. The first component of ladderFold P bits equals (bitsToNat bits) • P. This is what the Montgomery ladder is supposed to compute.