Signature verification is correct

A signature R ‖ s with R = r·B, A = a·B, and s ≡ r + k·a (mod ℓ) satisfies the cofactored check 8s·B = 8R + 8k·A.

def Cryptlib.Primitives.Sign.Ed25519Verify.sBytes (s : ℕ) : Vector UInt8 32

The 32 little-endian bytes of s.

Equations

• Cryptlib.Primitives.Sign.Ed25519Verify.sBytes s = Vector.ofFn fun (i : Fin 32) => (s >>> (8 * ↑i)).toUInt8

theorem Cryptlib.Primitives.Sign.Ed25519Verify.bytesToNat_sBytes (s : ℕ) (h : s < 256 ^ 32) : Ed25519Math.bytesToNat (sBytes s).toList = s

theorem Cryptlib.Primitives.Sign.Ed25519Verify.extract_eq (rBytes sb : Vector UInt8 32) : (rBytes ++ sb).toArray.extract 0 32 = rBytes.toArray

theorem Cryptlib.Primitives.Sign.Ed25519Verify.verify_of_parts (pk rBytes : Vector UInt8 32) (m : ByteArray) (a r k s : ℕ) (hpk : pk = Ed25519Math.encodePoint (Ed25519Math.scalarMul a Ed25519Math.basepoint)) (hR : rBytes = Ed25519Math.encodePoint (Ed25519Math.scalarMul r Ed25519Math.basepoint)) (hk : Ed25519Math.hashNat [{ data := rBytes.toArray }, Ed25519Math.vectorToByteArray pk, m] % Ed25519Math.ell = k) (hs : s < Ed25519Math.ell) (hsk : s % Ed25519Math.ell = (r + k * a) % Ed25519Math.ell) : Ed25519Math.verifyNative pk m (rBytes ++ sBytes s) = true

theorem Cryptlib.Primitives.Sign.Ed25519Verify.sig_eq (rBytes : Vector UInt8 32) (s : ℕ) : (Vector.ofFn fun (i : Fin 64) => if ↑i < 32 then rBytes[↑i]! else (s >>> (8 * (↑i - 32))).toUInt8) = rBytes ++ sBytes s

A signature laid out as R ‖ s.

theorem Cryptlib.Primitives.Sign.Ed25519Verify.verify_signNative (sk : Vector UInt8 32) (m : ByteArray) : Ed25519Math.verifyNative (Ed25519Math.publicKey sk) m (Ed25519Math.signNative sk m) = true

RFC 8032 correctness of the native signer.

def Cryptlib.Primitives.Sign.Ed25519Verify.nativeSignature : Sign.Signature

Ed25519 as a plain signature scheme, over the native arithmetic.

Equations

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