def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.fromField (x : ZMod X25519Common.p) : Vector UInt8 X25519Common.keySize

Little-endian byte encoding, exactly 32 bytes.

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.fromField x = Vector.ofFn fun (i : Fin Cryptlib.Primitives.NIKE.X25519Common.keySize) => (x.val >>> (8 * ↑i)).toUInt8

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.basepointBytes : Vector UInt8 X25519Common.keySize

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.basepointBytes = Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.fromField Cryptlib.Primitives.NIKE.X25519Common.basepoint

structure Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.LadderState : Type

• x1 : ZMod X25519Common.p
• x2 : ZMod X25519Common.p
• z2 : ZMod X25519Common.p
• x3 : ZMod X25519Common.p
• z3 : ZMod X25519Common.p

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.montgomery_step (s : LadderState) : LadderState

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.cswap (swap : Bool) (x y : ZMod X25519Common.p) : ZMod X25519Common.p × ZMod X25519Common.p

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.cswap swap x y = if swap = true then (y, x) else (x, y)

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.montgomery_ladder (e : Vector UInt8 X25519Common.keySize) (point : ZMod X25519Common.p) : Id LadderState

The ladder takes the scalar as bytes: a clamped scalar can exceed p, so it must not be reduced modulo p.

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.scalarmult (scalarBytes : Vector UInt8 X25519Common.keySize) (point : ZMod X25519Common.p) : ZMod X25519Common.p

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519 (scalar point : Vector UInt8 X25519Common.keySize) : Vector UInt8 X25519Common.keySize

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.x25519 (scalarBytes uCoordBytes : Vector UInt8 X25519Common.keySize) : Vector UInt8 X25519Common.keySize

RFC 7748 X25519. Total: the ladder is defined on every u-coordinate, including twist points.

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.x25519 scalarBytes uCoordBytes = Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519 scalarBytes uCoordBytes

The same ladder on Field25519.Fe

The ladder on fixed-width limbs, with masked swaps so it does not branch on scalar bits. Tested against the ZMod ladder and RFC 7748 vectors, not yet proved equal to it.

structure Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.LadderStateFe : Type

• x1 : Field25519.Fe
• x2 : Field25519.Fe
• z2 : Field25519.Fe
• x3 : Field25519.Fe
• z3 : Field25519.Fe

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.montgomery_step_fe (s : LadderStateFe) : LadderStateFe

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.montgomery_ladder_fe (e : Vector UInt8 X25519Common.keySize) (point : Field25519.Fe) : LadderStateFe

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.scalarmult_fe (scalarBytes : Vector UInt8 X25519Common.keySize) (point : Field25519.Fe) : Field25519.Fe

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_fe (scalar point : Vector UInt8 X25519Common.keySize) : Vector UInt8 X25519Common.keySize

Equations

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

structure Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.PublicKey : Type

• data : Vector UInt8 X25519Common.keySize

structure Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.SharedSecret : Type

• data : Vector UInt8 X25519Common.keySize

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.derivePub (sk : X25519Common.PrivateKey) : PublicKey

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.smallOrderPoints : List (Vector UInt8 X25519Common.keySize)

Curve25519 small-order points, little-endian. Compared after masking the high bit of byte 31, so each also covers its +2^255 variant. See eprint.iacr.org/2017/806.

Equations

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

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.maskHighBit (v : Vector UInt8 X25519Common.keySize) : Vector UInt8 X25519Common.keySize

Clear the high bit of byte 31.

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.maskHighBit v = v.set 31 (v[31] &&& 127) Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.maskHighBit._proof_1

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.SafePub (pk : PublicKey) : Prop

Equations

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

@[instance_reducible]

instance Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.instDecidablePredPublicKeySafePub : DecidablePred SafePub

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.instDecidablePredPublicKeySafePub pk = id inferInstance

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.derivePub_safe (sk : X25519Common.PrivateKey) : SafePub (derivePub sk)

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_commutes (sk₁ sk₂ : X25519Common.PrivateKey) : curve25519 sk₁.data (derivePub sk₂).data = curve25519 sk₂.data (derivePub sk₁).data

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_safe (sk : X25519Common.PrivateKey) (pk : PublicKey) : SafePub { data := curve25519 sk.data pk.data }

The ladder's output is never a small-order point: clamping makes every scalar a multiple of the cofactor 8.

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_comm_gen (sk₁ sk₂ : X25519Common.PrivateKey) (pk : Vector UInt8 X25519Common.keySize) : curve25519 sk₁.data (curve25519 sk₂.data pk) = curve25519 sk₂.data (curve25519 sk₁.data pk)

Group actions by two private keys commute on any public key, not only on derived ones as in curve25519_commutes.

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.SchemeName : String

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.SchemeName = "X25519-ladder"

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.LadderScheme : NIKE.NIKE

Equations

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

The ladder on Field25519 limbs, as a NIKE

LadderScheme with curve25519_fe in place of curve25519. Its axioms restate the ladder's for curve25519_fe; proving curve25519_fe = curve25519 would remove them.

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.derivePubFe (sk : X25519Common.PrivateKey) : PublicKey

Equations

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

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.derivePubFe_safe (sk : X25519Common.PrivateKey) : SafePub (derivePubFe sk)

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_fe_commutes (sk₁ sk₂ : X25519Common.PrivateKey) : curve25519_fe sk₁.data (derivePubFe sk₂).data = curve25519_fe sk₂.data (derivePubFe sk₁).data

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_fe_safe (sk : X25519Common.PrivateKey) (pk : PublicKey) : SafePub { data := curve25519_fe sk.data pk.data }

axiom Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.curve25519_fe_comm_gen (sk₁ sk₂ : X25519Common.PrivateKey) (pk : Vector UInt8 X25519Common.keySize) : curve25519_fe sk₁.data (curve25519_fe sk₂.data pk) = curve25519_fe sk₂.data (curve25519_fe sk₁.data pk)

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.FeSchemeName : String

Equations

• Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.FeSchemeName = "X25519"

def Cryptlib.Primitives.NIKE.X25519_montgomery_ladder.FeScheme : NIKE.NIKE

Equations

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