Message authentication codes

keySize is informational; mac accepts any key length. Unforgeability is computational, so there are no law fields.

structure Cryptlib.Primitives.MAC.MAC : Type

• keySize : Nat
• tagSize : Nat
• mac : ByteArray → ByteArray → Vector UInt8 self.tagSize

@[instance_reducible]

instance Cryptlib.Primitives.MAC.instInhabitedMAC : Inhabited MAC

The empty MAC, to show MAC is inhabited. Not a MAC.

Equations

• Cryptlib.Primitives.MAC.instInhabitedMAC = { default := { keySize := 0, tagSize := 0, mac := fun (x x_1 : ByteArray) => #v[] } }