POLYVAL, the GCM-SIV authenticator

RFC 8452 §3: POLYVAL(H, X₁, …, Xₛ) = Σᵢ Xᵢ • H^(s-i+1) where a • b = a·b·x⁻¹²⁸, over GF(2)[x] / (x¹²⁸ + x¹²⁷ + x¹²⁶ + x¹²¹ + 1). Field elements are little-endian Nats: byte j, bit i is the coefficient of x^(8j+i).

def Cryptlib.Primitives.Cipher.Polyval.modulus : Nat

x¹²⁸ + x¹²⁷ + x¹²⁶ + x¹²¹ + 1, as bits of a Nat.

Equations

• Cryptlib.Primitives.Cipher.Polyval.modulus = 1 ||| 1 <<< 121 ||| 1 <<< 126 ||| 1 <<< 127 ||| 1 <<< 128

def Cryptlib.Primitives.Cipher.Polyval.ofBytes (v : Vector UInt8 16) : Nat

A 16-byte string as a field element, little-endian per RFC 8452 §3.

Equations

• Cryptlib.Primitives.Cipher.Polyval.ofBytes v = Array.foldr (fun (b : UInt8) (acc : Nat) => acc <<< 8 ||| b.toNat) 0 v.toArray

def Cryptlib.Primitives.Cipher.Polyval.toBytes (n : Nat) : Vector UInt8 16

A field element as 16 little-endian bytes. Bits at or above x¹²⁸ are dropped.

Equations

• Cryptlib.Primitives.Cipher.Polyval.toBytes n = Vector.ofFn fun (i : Fin 16) => UInt8.ofNat (n >>> (8 * ↑i) % 256)

def Cryptlib.Primitives.Cipher.Polyval.clmul (a b : Nat) : Nat

Carry-less multiplication over GF(2), without reduction.

Equations

• Cryptlib.Primitives.Cipher.Polyval.clmul a b = List.foldl (fun (acc i : Nat) => if a.testBit i = true then acc ^^^ b <<< i else acc) 0 (List.range 128)

def Cryptlib.Primitives.Cipher.Polyval.divX128 (c : Nat) : Nat

Multiplication by x⁻¹²⁸, one division by x at a time; also reduces the input below x¹²⁸.

Equations

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

def Cryptlib.Primitives.Cipher.Polyval.dot (a b : Nat) : Nat

RFC 8452's dot: a • b = a·b·x⁻¹²⁸.

Equations

• Cryptlib.Primitives.Cipher.Polyval.dot a b = Cryptlib.Primitives.Cipher.Polyval.divX128 (Cryptlib.Primitives.Cipher.Polyval.clmul a b)

def Cryptlib.Primitives.Cipher.Polyval.polyval (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16

POLYVAL(H, X₁ ‖ … ‖ Xₛ), in Horner form: Sⱼ = (Sⱼ₋₁ + Xⱼ) • H.

Equations

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