Cryptographic hash functions

Security properties are computational and cannot be fields. The laws relate the one-shot and incremental interfaces: hash_spec (one call agrees with a fresh state) and update_append (two chunks agree with their concatenation).

structure Cryptlib.Primitives.Hash.Hash.Hash : Type 1

• State : Type

  The running state of an incremental hash.

• name : String
• digestSize : Nat
• blockSize : Nat

  The compression function's input width in bytes, used by HMAC for key padding.

• init : self.State
• update : self.State → ByteArray → self.State
• finalize : self.State → Vector UInt8 self.digestSize
• hash : ByteArray → Vector UInt8 self.digestSize
• hash_spec (m : ByteArray) : self.hash m = self.finalize (self.update self.init m)
• update_append (s : self.State) (a b : ByteArray) : self.update (self.update s a) b = self.update s (a ++ b)

@[instance_reducible]

instance Cryptlib.Primitives.Hash.Hash.instInhabitedHash : Inhabited Hash

The empty hash, to show Hash is inhabited. Not a hash.

Equations

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