Hash Definitions

Here we define what we explicitly define properties about hash funcitons.

Hash Operations as Classes

We say that elements in α can be hashed to ℍ through mhash.

class Hash (α ℍ : Type) : Type

• mhash : α → ℍ

Additionally, we define another function combining hashes comb

class HashMagma (ℍ : Type) : Type

• comb : ℍ → ℍ → ℍ

Usually, Hash and Hashmagma would go together.

Hash Properties

Hash function collision resistant and Injective

class CollResistant (α ℍ : Type) [op : Hash α ℍ] : Prop

• noCollisions (a b : α) : a ≠ b → op.mhash a ≠ op.mhash b

class InjectiveHash (α ℍ : Type) [h : Hash α ℍ] : Prop

• inject (a b : α) : h.mhash a = h.mhash b → a = b

Injective is stronger than Collision resistant

def injIsCollResis {α ℍ : Type} [m : Hash α ℍ] (inj : InjectiveHash α ℍ) : CollResistant α ℍ

Equations

• ⋯ = ⋯

Hash combination respects collision resistant (both arguments) and Injective.

class SLawFulHash (ℍ : Type) [m : HashMagma ℍ] : Prop

• neqLeft (a1 a2 b1 b2 : ℍ) : a1 ≠ a2 → m.comb a1 b1 ≠ m.comb a2 b2
• neqRight (a1 a2 b1 b2 : ℍ) : b1 ≠ b2 → m.comb a1 b1 ≠ m.comb a2 b2

class InjectiveMagma (ℍ : Type) [m : HashMagma ℍ] : Prop

• injectL (a1 a2 b1 b2 : ℍ) : m.comb a1 b1 = m.comb a2 b2 → a1 = a2
• injectR (a1 a2 b1 b2 : ℍ) : m.comb a1 b1 = m.comb a2 b2 → b1 = b2

Injective is stronger than Collision resistant

def injIsLawful {ℍ : Type} {m : HashMagma ℍ} (inj : InjectiveMagma ℍ) : SLawFulHash ℍ

Equations

• ⋯ = ⋯

class HomomorphicHash (α ℍ : Type) [h : Hash α ℍ] [m : HashMagma ℍ] : Prop

• homHash (a : α) (b c : ℍ) : h.mhash a ≠ m.comb b c

Decidability through α and CollResistant

This is kinda important, it actually hides when we are using CollResistant hashes

def eq_eqhash {α ℍ : Type} [eqa : DecidableEq α] [o : Hash α ℍ] [cfree : CollResistant α ℍ] (a b : α) : Decidable (o.mhash a = o.mhash b)

Equations

• eq_eqhash a b = match eqa a b with | isTrue e => isTrue ⋯ | isFalse e => isFalse ⋯