GHASH, the GCM authenticator (NIST SP 800-38D §6.4)

Blocks are read as big-endian 128-bit integers. GCM numbers bits from the most significant end, so the coefficient of x⁰ is the integer's top bit and multiplying by x is a right shift, reduced by R = 0xE1 ‖ 0¹²⁰.

def Cryptlib.Primitives.Cipher.GHash.R : Nat

Equations

• Cryptlib.Primitives.Cipher.GHash.R = 225 <<< 120

def Cryptlib.Primitives.Cipher.GHash.ofBytes (b : Array UInt8) : Nat

Equations

• Cryptlib.Primitives.Cipher.GHash.ofBytes b = Array.foldl (fun (acc : Nat) (x : UInt8) => acc <<< 8 ||| x.toNat) 0 b

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

Equations

• Cryptlib.Primitives.Cipher.GHash.toBytes n = Vector.ofFn fun (i : Fin 16) => UInt8.ofNat (n >>> (8 * (15 - ↑i)))

def Cryptlib.Primitives.Cipher.GHash.mul (x y : Nat) : Nat

SP 800-38D Algorithm 1, X • Y in GF(2¹²⁸).

Equations

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

def Cryptlib.Primitives.Cipher.GHash.ghash (h : Vector UInt8 16) (blocks : ByteArray) : Vector UInt8 16

GHASH_H over a byte string, a short final block read as zero-padded.

Equations

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