Symbolic/Specifications/Model/EquationalTheory/X25519.lean

@[expose] public def p25519 : Nat := 2 ^ 255 - 19

Little-endian Nat value of a byte list.

@[expose] public def leValue : List Nat → Nat
  | [] => 0
  | x :: xs => x + 256 * leValue xs

def uCoordL34–35 ↗#

RFC 7748 decodeUCoordinate: clear bit 255 and reduce modulo p25519.

@[expose] public def uCoord (bytes : List Nat) : Nat := leValue bytes % 2 ^ 255 % p25519

def lowOrderUsL37–42 ↗#

Curve25519 and twist u-coordinates in [0, p25519) on which clamped X25519 scalar multiplication outputs all zeros.

@[expose] public def lowOrderUs : List Nat :=
  [0, 1, 325606250916557431795983626356110631294008115727848805560023387167927233504,
    39382357235489614581723060781553021112529911719440698176882885853963445705823,
    p25519 - 1]

def isLowOrderKeyL44–46 ↗#

Whether bytes is a 32-byte key whose uCoord lies in lowOrderUs.

@[expose] public def isLowOrderKey (bytes : List Nat) : Bool :=
  bytes.length == 32 && lowOrderUs.contains (uCoord bytes)

structure SubFL50–56 ↗#

Public key paired with a non-canonical encoding selector variation and 8-torsion shift torsion.

public
structure SubF (Bytes: Type) where
  key: Bytes
  variation: Fin 4
  torsion: Fin 8 := 0

instanceL58 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .unary SubF.key

instanceL59–65 ↗#

public instance: SubBytesFunctor SubF :=
  .unaryData (Fin 32)
    (fun {variation, torsion, ..} => ⟨variation.val + 4 * torsion.val, bya✝:Typex✝:SubF a✝key✝:a✝variation:Fin 4torsion:Fin 8⊢ ↑variation + 4 * ↑torsion < 32 omegaAll goals completed! 🐙⟩)
    SubF.key
    (fun d key => { key, variation := ⟨d.val % 4, bya✝:Typed:Fin 32key:a✝⊢ ↑d % 4 < 4 omegaAll goals completed! 🐙⟩, torsion := ⟨d.val / 4, bya✝:Typed:Fin 32key:a✝⊢ ↑d / 4 < 8 omegaAll goals completed! 🐙⟩ })
    (fun {key, variation, torsion} => bya✝:Typex✝:SubF a✝key:a✝variation:Fin 4torsion:Fin 8⊢ { key := { key := key, variation := variation, torsion := torsion }.key,
    variation :=
      ⟨↑(match { key := key, variation := variation, torsion := torsion } with
            | { key := key, variation := variation, torsion := torsion } => ⟨↑variation + 4 * ↑torsion, ⋯⟩) %
          4,
        ⋯⟩,
    torsion :=
      ⟨↑(match { key := key, variation := variation, torsion := torsion } with
            | { key := key, variation := variation, torsion := torsion } => ⟨↑variation + 4 * ↑torsion, ⋯⟩) /
          4,
        ⋯⟩ } =
  { key := key, variation := variation, torsion := torsion } simp [Fin.ext_iff]a✝:Typex✝:SubF a✝key:a✝variation:Fin 4torsion:Fin 8⊢ (↑variation + 4 * ↑torsion) / 4 = ↑torsion <;>a✝:Typex✝:SubF a✝key:a✝variation:Fin 4torsion:Fin 8⊢ (↑variation + 4 * ↑torsion) / 4 = ↑torsion omegaAll goals completed! 🐙)
    (fun d _ => bya✝:Typed:Fin 32x✝:a✝⊢ (match { key := x✝, variation := ⟨↑d % 4, ⋯⟩, torsion := ⟨↑d / 4, ⋯⟩ } with
  | { key := key, variation := variation, torsion := torsion } => ⟨↑variation + 4 * ↑torsion, ⋯⟩) =
  d simp [Fin.ext_iff]a✝:Typed:Fin 32x✝:a✝⊢ ↑d % 4 + 4 * (↑d / 4) = ↑d; omegaAll goals completed! 🐙)

def SubF.lengthL67–69 ↗#

public
def SubF.length [BytesFunctor]: Bytes.PartialLength SubF :=
  fun _ _ => 32

#combineL73–74 ↗#

#combine into BytesFunctor, BytesLength from
  Variant,

abbrev Variant.SubF.packL78–79 ↗#

public
abbrev Variant.SubF.pack (x: Variant.SubF Bytes) := BytesView.pack x

def normalizeX25519KeyL81–86 ↗#

Strip an outer Variant.SubF wrapper if present.

@[expose] public
def normalizeX25519Key (pk: Bytes): Bytes :=
  match pk.view? Variant.SubF with
  | some x => x.key
  | none => pk

def x25519TorsionVariantL88–93 ↗#

Apply encoding selector v and 8-torsion shift t to normalizeX25519Key key, returning the normalized key unchanged when v = 0 ∧ t = 0.

@[expose] public
def x25519TorsionVariant (key: Bytes) (v: Fin 4) (t: Fin 8): Bytes :=
  if v = 0 ∧ t = 0 then normalizeX25519Key key
  else ({key := normalizeX25519Key key, variation := v, torsion := t}: Variant.SubF Bytes).pack

def x25519Variant.attackerKnowledgeL95–97 ↗#

@[expose] public
def x25519Variant.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ key v t, out = x25519TorsionVariant key v t ∧ p key

def normalizeX25519Key.attackerKnowledgeL99–101 ↗#

@[expose] public
def normalizeX25519Key.attackerKnowledge: SubAttackerKnowledge SubF where
  pred p out := ∃ x: Variant.SubF Bytes, p x.pack ∧ out = x.key

#combineL103–105 ↗#

#combine [BytesFunctor.Has SubF] into attackerKnowledge' from
  x25519Variant,
  normalizeX25519Key,

def x25519LowOrderL107–112 ↗#

Whether normalizeX25519Key pk is a literal 32-byte low-order key.

@[expose] public
def x25519LowOrder [BytesFunctor.Has Literal.SubF] (pk: Bytes): Bool :=
  match Literal.bytesToLiteral (normalizeX25519Key pk) with
  | some b => isLowOrderKey (b.data.toList.map (·.toNat))
  | none => false

def isCanonicalKeyL114–118 ↗#

Symbolic PublicKey::is_canonical check: rejects Variant.SubF wrappers and literal low-order keys.

@[expose] public
def isCanonicalKey [BytesFunctor.Has Literal.SubF] (pk: Bytes): Bool :=
  (pk.view? Variant.SubF).isNone && !x25519LowOrder pk

def agreeL120–126 ↗#

Symbolic X25519 Diffie-Hellman agreement on normalizeX25519Key pk and secret key sk.

@[expose] public
def agree [BytesFunctor.Has DiffieHellman.SubF] (pk sk: Bytes): Bytes :=
  DiffieHellman.dh (normalizeX25519Key pk) sk

AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

X25519.lean🔗