Demo
Everything else here is abstract, which is what makes the theorems apply to any
curve and also what makes nothing executable. This module fixes a tiny instance
-- the additive group of ZMod 23, where discrete logs are division -- so the
scheme and the attack can be RUN: exactly why the attack is executable here, and
why the instance offers no security. Each #eval is wrapped in #guard_msgs,
so the numbers in the docstrings are build-checked assertions.
See docs/dksap-asymmetry.md.
instFactPrime23
23 is prime, so ZMod 23 is a field.
instance instFactPrime23 : Fact (Nat.Prime 23) := ⟨by norm_num⟩F
abbrev F := ZMod 23gen
def gen : F := 5hash
def hash (x : F) : F := 7 * x + 3gen_injective
theorem gen_injective : Function.Injective (fun x : F => x • gen) := byproof
simpa only [smul_eq_mul] using mul_left_injective₀ (b := gen) (by decide)A tiny field and a generator
m
Recipient's spending secret.
def m : F := 9v
def v : F := 4r
def r : F := 3M
def M : F := m • genV
def V : F := v • genR
def R : F := r • genP
def P : F := M + (hash (r • V)) • genhonestKey
def honestKey : F := m + hash (v • R)One recipient, one payment
genInv
The generator's multiplicative inverse, 5 * 14 = 70 = 1 mod 23.
def genInv : F := 14genInv_spec
theorem genInv_spec : genInv * gen = 1 := by decidedlog
def dlog (x : F) : F := genInv * xrecovered
def recovered : F := recover hash (dlog M) (dlog V) RThe attack
Run it
scheme
DKSAP at the toy instance.
def scheme : StealthScheme (F × F) (F × F) (F × F) := dksap gen hashgen_bijective
theorem gen_bijective : Function.Bijective (fun x : F => x • gen) :=
Finite.injective_iff_bijective.mp gen_injective