X25519 as a group operation

Scalar multiplication on Curve25519, using Mathlib's WeierstrassCurve.Affine.Point for the group law (y² = x³ + 486662x² + x is already in Weierstrass form). Public keys and shared secrets are 32-byte RFC 7748 u-coordinates; liftX recovers a point from a u-coordinate.

Axioms: p_prime and liftX_isSome_of_exists.

The base field

axiom Cryptlib.Primitives.NIKE.X25519.p_prime : Nat.Prime X25519Common.p

2^255 - 19 is prime. Taken as an axiom.

instance Cryptlib.Primitives.NIKE.X25519.instFactPrimeP : Fact (Nat.Prime X25519Common.p)

theorem Cryptlib.Primitives.NIKE.X25519.p_lt_pow : X25519Common.p < 256 ^ 32

The group

def Cryptlib.Primitives.NIKE.X25519.curve : WeierstrassCurve.Affine (ZMod X25519Common.p)

Curve25519 y² = x³ + 486662x² + x as a Weierstrass curve in affine coordinates.

Equations

• Cryptlib.Primitives.NIKE.X25519.curve = { a₁ := 0, a₂ := 486662, a₃ := 0, a₄ := 1, a₆ := 0 }

@[reducible, inline]

abbrev Cryptlib.Primitives.NIKE.X25519.Point : Type

The points of Curve25519, including the point at infinity.

Equations

• Cryptlib.Primitives.NIKE.X25519.Point = Cryptlib.Primitives.NIKE.X25519.curve.Point

def Cryptlib.Primitives.NIKE.X25519.onCurve (x y : ZMod X25519Common.p) : Prop

Equations

• Cryptlib.Primitives.NIKE.X25519.onCurve x y = (y ^ 2 = x ^ 3 + 486662 * x ^ 2 + x)

@[instance_reducible]

instance Cryptlib.Primitives.NIKE.X25519.decidableOnCurve (x y : ZMod X25519Common.p) : Decidable (onCurve x y)

Equations

• Cryptlib.Primitives.NIKE.X25519.decidableOnCurve x y = Cryptlib.Primitives.NIKE.X25519.decidableOnCurve._aux_1 x y

theorem Cryptlib.Primitives.NIKE.X25519.equation_iff {x y : ZMod X25519Common.p} : curve.Equation x y ↔ onCurve x y

theorem Cryptlib.Primitives.NIKE.X25519.curve_Δ_ne_zero : WeierstrassCurve.Δ curve ≠ 0

theorem Cryptlib.Primitives.NIKE.X25519.nonsingular_iff_onCurve {x y : ZMod X25519Common.p} : curve.Nonsingular x y ↔ onCurve x y

Curve25519 is nonsingular, so the curve equation is the only condition for a point.

def Cryptlib.Primitives.NIKE.X25519.mkPoint {x y : ZMod X25519Common.p} (h : onCurve x y) : Point

Build a point from coordinates that pass the curve check.

Equations

• Cryptlib.Primitives.NIKE.X25519.mkPoint h = WeierstrassCurve.Affine.Point.some x y ⋯

def Cryptlib.Primitives.NIKE.X25519.xCoord : Point → ZMod X25519Common.p

The x-coordinate, 0 at infinity.

Equations

• Cryptlib.Primitives.NIKE.X25519.xCoord WeierstrassCurve.Affine.Point.zero = 0
• Cryptlib.Primitives.NIKE.X25519.xCoord (WeierstrassCurve.Affine.Point.some x_1 y h) = x_1

The basepoint

def Cryptlib.Primitives.NIKE.X25519.basepointYNat : ℕ

The y-coordinate of the standard basepoint x = 9, as a natural number.

Equations

• Cryptlib.Primitives.NIKE.X25519.basepointYNat = 14781619447589544791020593568409986887264606134616475288964881837755586237401

def Cryptlib.Primitives.NIKE.X25519.basepointY : ZMod X25519Common.p

The y-coordinate of the standard basepoint x = 9.

Equations

• Cryptlib.Primitives.NIKE.X25519.basepointY = ↑Cryptlib.Primitives.NIKE.X25519.basepointYNat

theorem Cryptlib.Primitives.NIKE.X25519.basepoint_onCurve : onCurve X25519Common.basepoint basepointY

def Cryptlib.Primitives.NIKE.X25519.G : Point

The standard basepoint of X25519, as a group element.

Equations

• Cryptlib.Primitives.NIKE.X25519.G = Cryptlib.Primitives.NIKE.X25519.mkPoint Cryptlib.Primitives.NIKE.X25519.basepoint_onCurve

Commutativity

theorem Cryptlib.Primitives.NIKE.X25519.dh_commutes (a b : ℕ) (P : Point) : a • b • P = b • a • P

The Diffie-Hellman identity.

Encoding field elements

32 bytes, little-endian.

def Cryptlib.Primitives.NIKE.X25519.encodeField (z : ZMod X25519Common.p) : List UInt8

A field element as 32 little-endian bytes.

Equations

• Cryptlib.Primitives.NIKE.X25519.encodeField z = List.map UInt8.ofNat (Nat.digits 256 z.val ++ List.replicate (32 - (Nat.digits 256 z.val).length) 0)

def Cryptlib.Primitives.NIKE.X25519.decodeField (bs : List UInt8) : ZMod X25519Common.p

Little-endian bytes back to a field element.

Equations

• Cryptlib.Primitives.NIKE.X25519.decodeField bs = ↑(Nat.ofDigits 256 (List.map UInt8.toNat bs))

theorem Cryptlib.Primitives.NIKE.X25519.digits_length_le (z : ZMod X25519Common.p) : (Nat.digits 256 z.val).length ≤ 32

@[simp]

theorem Cryptlib.Primitives.NIKE.X25519.encodeField_length (z : ZMod X25519Common.p) : (encodeField z).length = 32

@[simp]

theorem Cryptlib.Primitives.NIKE.X25519.decodeField_encodeField (z : ZMod X25519Common.p) : decodeField (encodeField z) = z

Encoding points

0x04 ‖ x ‖ y, or 65 zero bytes for the point at infinity.

def Cryptlib.Primitives.NIKE.X25519.encodePoint : Point → List UInt8

Equations

• Cryptlib.Primitives.NIKE.X25519.encodePoint WeierstrassCurve.Affine.Point.zero = 0 :: List.replicate 64 0
• Cryptlib.Primitives.NIKE.X25519.encodePoint (WeierstrassCurve.Affine.Point.some x_1 y h) = 4 :: (Cryptlib.Primitives.NIKE.X25519.encodeField x_1 ++ Cryptlib.Primitives.NIKE.X25519.encodeField y)

@[simp]

theorem Cryptlib.Primitives.NIKE.X25519.encodePoint_length (P : Point) : (encodePoint P).length = 65

def Cryptlib.Primitives.NIKE.X25519.decodePointRaw : List UInt8 → Option Point

Parse without checking that the encoding is canonical.

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.NIKE.X25519.decodePointRaw [] = none

@[simp]

theorem Cryptlib.Primitives.NIKE.X25519.decodePointRaw_encodePoint (P : Point) : decodePointRaw (encodePoint P) = some P

def Cryptlib.Primitives.NIKE.X25519.decodePoint (bs : List UInt8) : Option Point

Parse and reject non-canonical encodings (coordinates ≥ p).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Cryptlib.Primitives.NIKE.X25519.decodePoint_encodePoint (P : Point) : decodePoint (encodePoint P) = some P

theorem Cryptlib.Primitives.NIKE.X25519.encodePoint_of_decodePoint {bs : List UInt8} {P : Point} (h : decodePoint bs = some P) : encodePoint P = bs

RFC 7748 interface

A u-coordinate is lifted to a point by square root: p ≡ 5 mod 8, so a root of a is a^((p+3)/8), possibly times √-1. The candidate is checked against the curve equation.

def Cryptlib.Primitives.NIKE.X25519.sqrtMinusOne : ZMod X25519Common.p

√-1 in ZMod p, i.e. 2^((p-1)/4).

Equations

• Cryptlib.Primitives.NIKE.X25519.sqrtMinusOne = ↑19681161376707505956807079304988542015446066515923890162744021073123829784752

def Cryptlib.Primitives.NIKE.X25519.liftX (x : ZMod X25519Common.p) : Option Point

Recover a point from its u-coordinate, or none if u is on the quadratic twist.

Equations

• One or more equations did not get rendered due to their size.

axiom Cryptlib.Primitives.NIKE.X25519.liftX_isSome_of_exists {x : ZMod X25519Common.p} : (∃ (y : ZMod X25519Common.p), onCurve x y) → (liftX x).isSome = true

liftX succeeds on every x-coordinate of a curve point. Taken as an axiom.

theorem Cryptlib.Primitives.NIKE.X25519.xCoord_of_liftX_eq_some {x : ZMod X25519Common.p} {Q : Point} (hQ : liftX x = some Q) : xCoord Q = x

liftX preserves the x-coordinate.

The NIKE scheme

Public keys and shared secrets are both x-coordinates in ZMod p.

def Cryptlib.Primitives.NIKE.X25519.scalarOf (sk : X25519Common.PrivateKey) : ℕ

The clamped scalar of a private key, as a natural number. Not reduced modulo p: clamped scalars can exceed p.

Equations

• Cryptlib.Primitives.NIKE.X25519.scalarOf sk = Nat.ofDigits 256 (List.map UInt8.toNat (Cryptlib.Primitives.NIKE.X25519Common.clampScalar sk.data).toList)

def Cryptlib.Primitives.NIKE.X25519.SafeX (x : ZMod X25519Common.p) : Prop

An x-coordinate is safe when it lifts to a curve point.

Equations

• Cryptlib.Primitives.NIKE.X25519.SafeX x = ((Cryptlib.Primitives.NIKE.X25519.liftX x).isSome = true)

@[instance_reducible]

instance Cryptlib.Primitives.NIKE.X25519.instDecidablePredZModPSafeX : DecidablePred SafeX

Equations

• Cryptlib.Primitives.NIKE.X25519.instDecidablePredZModPSafeX _x = Cryptlib.Primitives.NIKE.X25519.instDecidablePredZModPSafeX._aux_1 _x

def Cryptlib.Primitives.NIKE.X25519.toPoint (x : ZMod X25519Common.p) (h : SafeX x) : Point

Recover the point a safe x-coordinate represents.

Equations

• Cryptlib.Primitives.NIKE.X25519.toPoint x h = (Cryptlib.Primitives.NIKE.X25519.liftX x).get h

theorem Cryptlib.Primitives.NIKE.X25519.xCoord_toPoint (x : ZMod X25519Common.p) (h : SafeX x) : xCoord (toPoint x h) = x

toPoint returns a point with the given x-coordinate.

def Cryptlib.Primitives.NIKE.X25519.groupActionX (sk : X25519Common.PrivateKey) (x : ZMod X25519Common.p) (h : SafeX x) : ZMod X25519Common.p

Equations

• Cryptlib.Primitives.NIKE.X25519.groupActionX sk x h = Cryptlib.Primitives.NIKE.X25519.xCoord (Cryptlib.Primitives.NIKE.X25519.scalarOf sk • Cryptlib.Primitives.NIKE.X25519.toPoint x h)

def Cryptlib.Primitives.NIKE.X25519.derivePublicKeyX (sk : X25519Common.PrivateKey) : ZMod X25519Common.p

Equations

• Cryptlib.Primitives.NIKE.X25519.derivePublicKeyX sk = Cryptlib.Primitives.NIKE.X25519.xCoord (Cryptlib.Primitives.NIKE.X25519.scalarOf sk • Cryptlib.Primitives.NIKE.X25519.G)

theorem Cryptlib.Primitives.NIKE.X25519.exists_onCurve_xCoord (P : Point) : ∃ (y : ZMod X25519Common.p), onCurve (xCoord P) y

Every curve point's x-coordinate is safe.

def Cryptlib.Primitives.NIKE.X25519.decodeFieldChecked (v : Vector UInt8 32) : Option (ZMod X25519Common.p)

32-byte little-endian decoding, rejecting values ≥ p.

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.X25519.encodeFieldChecked (z : ZMod X25519Common.p) : Vector UInt8 32

Equations

• Cryptlib.Primitives.NIKE.X25519.encodeFieldChecked z = Vector.mk (Cryptlib.Primitives.NIKE.X25519.encodeField z).toArray ⋯

Commutativity of groupActionX

toPoint picks one of the points sharing an x-coordinate. The x-coordinate of a scalar multiple does not depend on which: the other point is the negation, or for x = 0 a point of order 2.

theorem Cryptlib.Primitives.NIKE.X25519.xCoord_neg (P : Point) : xCoord (-P) = xCoord P

theorem Cryptlib.Primitives.NIKE.X25519.nsmul_neg (P : Point) (n : ℕ) : n • -P = -(n • P)

Natural-number scalar multiplication commutes with negation.

theorem Cryptlib.Primitives.NIKE.X25519.nsmul_zero_point (n : ℕ) : n • 0 = 0

Scalar multiples of the identity are the identity.

def Cryptlib.Primitives.NIKE.X25519.zeroZeroPoint (h : curve.Nonsingular 0 0) : Point

The finite point (0, 0), given it's on the curve.

Equations

• Cryptlib.Primitives.NIKE.X25519.zeroZeroPoint h = WeierstrassCurve.Affine.Point.some 0 0 h

theorem Cryptlib.Primitives.NIKE.X25519.zeroZeroPoint_add_self (h : curve.Nonsingular 0 0) : zeroZeroPoint h + zeroZeroPoint h = 0

The point (0, 0) is its own negative.

theorem Cryptlib.Primitives.NIKE.X25519.nsmul_eq_zero_or_self {R : Point} (hRR : R + R = 0) (n : ℕ) : n • R = 0 ∨ n • R = R

Every scalar multiple of a point R with R + R = 0 is 0 or R.

theorem Cryptlib.Primitives.NIKE.X25519.xCoord_smul_zero {y : ZMod X25519Common.p} (h : curve.Nonsingular 0 y) (n : ℕ) : xCoord (n • WeierstrassCurve.Affine.Point.some 0 y h) = 0

Scalar multiples of a point with x-coordinate 0 have x-coordinate 0.

theorem Cryptlib.Primitives.NIKE.X25519.xCoord_smul_congr (n : ℕ) {P Q : Point} (hPQ : xCoord P = xCoord Q) : xCoord (n • P) = xCoord (n • Q)

Points with equal x-coordinates have scalar multiples with equal x-coordinates.

theorem Cryptlib.Primitives.NIKE.X25519.groupActionX_commutes (sk₁ sk₂ : X25519Common.PrivateKey) (h₁ : SafeX (derivePublicKeyX sk₁)) (h₂ : SafeX (derivePublicKeyX sk₂)) : groupActionX sk₁ (derivePublicKeyX sk₂) h₂ = groupActionX sk₂ (derivePublicKeyX sk₁) h₁

The Diffie-Hellman identity for groupActionX.

theorem Cryptlib.Primitives.NIKE.X25519.groupActionX_safe (sk : X25519Common.PrivateKey) (x : ZMod X25519Common.p) (h : SafeX x) : SafeX (groupActionX sk x h)

groupActionX always returns a safe x-coordinate.

theorem Cryptlib.Primitives.NIKE.X25519.groupActionX_comm (sk₁ sk₂ : X25519Common.PrivateKey) (x : ZMod X25519Common.p) (h : SafeX x) : groupActionX sk₁ (groupActionX sk₂ x h) ⋯ = groupActionX sk₂ (groupActionX sk₁ x h) ⋯

Group actions by two private keys commute on any safe x-coordinate.

def Cryptlib.Primitives.NIKE.X25519.Scheme : NIKE.NIKE

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.NIKE.X25519.uBytes (P : Point) : Vector UInt8 32

A u-coordinate as 32 little-endian bytes.

Equations

• Cryptlib.Primitives.NIKE.X25519.uBytes P = Cryptlib.Primitives.NIKE.X25519.encodeFieldChecked (Cryptlib.Primitives.NIKE.X25519.xCoord P)

def Cryptlib.Primitives.NIKE.X25519.x25519 (scalarBytes uCoordBytes : Vector UInt8 32) : Option (Vector UInt8 32)

RFC 7748 X25519, computed by scalar multiplication in the group. none when the input u-coordinate is not on the curve.

Equations

• One or more equations did not get rendered due to their size.