Helpers shared by NIKE-Sphinx and KEM-Sphinx #

theorem Cryptlib.Protocols.Sphinx.Common.cascading_xor_step (ks riFragment Rk1 prevPad : ByteArray) (ksLen perHop : ℕ) (hks : ks.size = ksLen + prevPad.size + perHop) (hRk1 : riFragment.size + Rk1.size = ksLen) :

(xorBytes (xorBytes (riFragment ++ Rk1) (ks.extract 0 ksLen) ++ prevPad ++ { data := Array.replicate perHop 0 }) ks).extract 0 ksLen = riFragment ++ Rk1 ∧ (xorBytes (xorBytes (riFragment ++ Rk1) (ks.extract 0 ksLen) ++ prevPad ++ { data := Array.replicate perHop 0 }) ks).extract ksLen (ksLen + prevPad.size + perHop) = xorBytes ((ks.extract ksLen ks.size).extract 0 prevPad.size) prevPad ++ (ks.extract ksLen ks.size).extract prevPad.size (ks.extract ksLen ks.size).size

Cascading padding (§3.2), at the byte level: XOR-ing the sender's Rk := xorBytes (riFragment ++ Rk1) riKeyStream against the full keystream ks recovers riFragment ++ Rk1 in its first ksLen bytes and the next padding in its trailing bytes.

source

theorem Cryptlib.Protocols.Sphinx.Common.Except.eq_ok_of_map_eq_ok {ε α β : Type} {f : α → β} {e : Except ε α} {b : β} (h : f <$> e = Except.ok b) :

∃ (a : α), e = Except.ok a ∧ f a = b

source

theorem Cryptlib.Protocols.Sphinx.Common.Except.eq_ok_of_bind_eq_ok {ε α β : Type} {e : Except ε α} {f : α → Except ε β} {b : β} (h : e >>= f = Except.ok b) :

∃ (a : α), e = Except.ok a ∧ f a = Except.ok b

source

theorem Cryptlib.Protocols.Sphinx.Common.List.forIn_congr_of_forall_mem {α β ε γ : Type} (l : List β) (f : β → α → Except ε (ForInStep α)) (φ : α → γ) (hyield : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.yield a') → φ a' = φ a) (hdone : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.done a') → φ a' = φ a) (init final : α) :

forIn l init f = Except.ok final → φ final = φ init

A forIn whose every step leaves φ unchanged leaves it unchanged overall.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.forIn_add_of_forall_mem {α β ε : Type} (l : List β) (f : β → α → Except ε (ForInStep α)) (φ : α → ℕ) (k : ℕ) (hyield : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.yield a') → φ a' = φ a + k) (hdone : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.done a') → False) (init final : α) :

forIn l init f = Except.ok final → φ final = φ init + l.length * k

A forIn that never exits early and grows φ by k per step grows it by l.length * k.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.forIn_const_of_forall_mem {α β ε γ : Type} (l : List β) (hl : l ≠ []) (f : β → α → Except ε (ForInStep α)) (ψ : α → γ) (v : γ) (hyield : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.yield a') → ψ a' = v) (hdone : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.done a') → False) (init final : α) :

forIn l init f = Except.ok final → ψ final = v

A forIn over a nonempty list that never exits early and sets ψ to v at every step ends with ψ = v.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.forIn_exists_trace {α β ε : Type} (l : List β) (f : β → α → Except ε (ForInStep α)) (hnd : ∀ (b : β) (a a' : α), b ∈ l → f b a ≠ Except.ok (ForInStep.done a')) (init final : α) :

forIn l init f = Except.ok final → ∃ (s : ℕ → α), s 0 = init ∧ s l.length = final ∧ ∀ (j : ℕ) (hj : j < l.length), f l[j] (s j) = Except.ok (ForInStep.yield (s (j + 1)))

A forIn that never exits early has a trace of intermediate accumulator values.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.foldl_exists_trace {α β : Type} (l : List β) (g : α → β → α) (init : α) :

∃ (s : ℕ → α), s 0 = init ∧ s l.length = List.foldl g init l ∧ ∀ (j : ℕ) (hj : j < l.length), s (j + 1) = g (s j) l[j]

l.foldl g init has a trace of intermediate accumulator values.

source

theorem Cryptlib.Protocols.Sphinx.Common.Array.getElem!_push_stable {α : Type} [Inhabited α] (a : Array α) (x : α) (i : ℕ) (h : i < a.size) :

(a.push x)[i]! = a[i]!

Pushing onto an array never disturbs an existing index.

source

theorem Cryptlib.Protocols.Sphinx.Common.Array.getElem!_stable_of_pushes {α : Type} [Inhabited α] (t : ℕ → Array α) (n : ℕ) (hpush : ∀ j < n, ∃ (x : α), t (j + 1) = (t j).push x) (hsize : ∀ j ≤ n, (t j).size = j) (i m : ℕ) :

i < m → m ≤ n → (t m)[i]! = (t (i + 1))[i]!

In a sequence of arrays each obtained from the last by one push, index i never changes after it is written.

source

def Cryptlib.Protocols.Sphinx.Common.mac (key : Vector UInt8 32) (msg : ByteArray) :

Vector UInt8 32

Equations

Cryptlib.Protocols.Sphinx.Common.mac key msg = Cryptlib.Primitives.MAC.HMAC.hmacSha256 (Cryptlib.Util.Bytes.ofVector key) msg

Instances For

source

def Cryptlib.Protocols.Sphinx.Common.zeroPadTo (n : ℕ) (b : ByteArray) :

ByteArray

Equations

Cryptlib.Protocols.Sphinx.Common.zeroPadTo n b = if b.size ≥ n then b else b ++ { data := Array.replicate (n - b.size) 0 }

Instances For

source

theorem Cryptlib.Protocols.Sphinx.Common.zeroPadTo_size {n : ℕ} {b : ByteArray} (h : b.size ≤ n) :

(zeroPadTo n b).size = n

zeroPadTo n b has size n when b.size ≤ n.

source

theorem Cryptlib.Protocols.Sphinx.Common.zeroPadTo_eq_append (b : ByteArray) (n : ℕ) (h : b.size ≤ n) :

zeroPadTo n b = b ++ { data := Array.replicate (n - b.size) 0 }

zeroPadTo, as an explicit append.

source

theorem Cryptlib.Protocols.Sphinx.Common.replicate_extract (k lo hi : ℕ) (h : hi ≤ k) :

{ data := Array.replicate k 0 }.extract lo hi = { data := Array.replicate (hi - lo) 0 }

source

def Cryptlib.Protocols.Sphinx.Common.commandsToBytes (budget : ℕ) (cmds : List Commands.RoutingCommand) :

Except String ByteArray

Serialize cmds, failing if the result exceeds budget bytes.

Equations

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

Instances For

source

theorem Cryptlib.Protocols.Sphinx.Common.commandsToBytes_size_le {budget : ℕ} {cmds : List Commands.RoutingCommand} {b : ByteArray} (h : commandsToBytes budget cmds = Except.ok b) :

b.size ≤ budget

A successful commandsToBytes fits within budget.

source

theorem Cryptlib.Protocols.Sphinx.Common.commandsToBytes_append_singleton {budget budget' : ℕ} {cmds : List Commands.RoutingCommand} {b : ByteArray} (hcb : commandsToBytes budget' cmds = Except.ok b) (c : Commands.RoutingCommand) (hbudget : b.size + c.toBytes.size ≤ budget) :

commandsToBytes budget (cmds ++ [c]) = Except.ok (b ++ c.toBytes)

Appending one command to a successful commandsToBytes call still succeeds, under a large enough budget.

source

theorem Cryptlib.Protocols.Sphinx.Common.parseAll_commandsToBytes (n budget : ℕ) (cmds : List Commands.RoutingCommand) (hn : ∀ c ∈ cmds, c ≠ Commands.RoutingCommand.null) (b : ByteArray) (hcb : commandsToBytes budget cmds = Except.ok b) (_hble : b.size ≤ n) :

Commands.parseAll (zeroPadTo n b) = Except.ok cmds

parseAll undoes commandsToBytes followed by zeroPadTo, given no .null commands.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.foldl_size_preserving {α : Type} (l : List α) (step : ByteArray → α → ByteArray) (hstep : ∀ (b : ByteArray) (a : α), (step b a).size = b.size) (init : ByteArray) :

(List.foldl step init l).size = init.size

A fold whose step preserves ByteArray size preserves it overall.

source

theorem Cryptlib.Protocols.Sphinx.Common.List.forIn_push_size_of_forall_mem {α β ε : Type} (l : List β) (n : ℕ) (π : α → Array ByteArray) (f : β → α → Except ε (ForInStep α)) (hyield : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.yield a') → ∃ (x : ByteArray), x.size = n ∧ π a' = (π a).push x) (hdone : ∀ (a a' : α), ∀ b ∈ l, f b a = Except.ok (ForInStep.done a') → False) (init final : α) :

(∀ (j : ℕ) (hj : j < (π init).size), (π init)[j].size = n) → forIn l init f = Except.ok final → ∀ (j : ℕ) (hj : j < (π final).size), (π final)[j].size = n

If every step of a forIn only pushes a ByteArray of size n, and the initial array's entries all have size n, so do the final array's.

Documentation

Cryptlib.Protocols.Sphinx.common

Helpers shared by NIKE-Sphinx and KEM-Sphinx #