inductive Term : Type

• atom : String → Term
• pair : Term → Term → Term
• op : String → Term → Term
• hash : Term → Term

def instDecidableEqTerm.decEq (x✝ x✝¹ : Term) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqTerm.decEq (Term.atom a) (Term.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqTerm.decEq (Term.atom a) (a_1.pair a_2) = isFalse ⋯
• instDecidableEqTerm.decEq (Term.atom a) (Term.op a_1 a_2) = isFalse ⋯
• instDecidableEqTerm.decEq (Term.atom a) a_1.hash = isFalse ⋯
• instDecidableEqTerm.decEq (a.pair a_1) (Term.atom a_2) = isFalse ⋯
• instDecidableEqTerm.decEq (a.pair a_1) (Term.op a_2 a_3) = isFalse ⋯
• instDecidableEqTerm.decEq (a.pair a_1) a_2.hash = isFalse ⋯
• instDecidableEqTerm.decEq (Term.op a a_1) (Term.atom a_2) = isFalse ⋯
• instDecidableEqTerm.decEq (Term.op a a_1) (a_2.pair a_3) = isFalse ⋯
• instDecidableEqTerm.decEq (Term.op a a_1) a_2.hash = isFalse ⋯
• instDecidableEqTerm.decEq a.hash (Term.atom a_1) = isFalse ⋯
• instDecidableEqTerm.decEq a.hash (a_1.pair a_2) = isFalse ⋯
• instDecidableEqTerm.decEq a.hash (Term.op a_1 a_2) = isFalse ⋯
• instDecidableEqTerm.decEq a.hash b.hash = if h : a = b then h ▸ have inst := instDecidableEqTerm.decEq a a; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instDecidableEqTerm : DecidableEq Term

Equations

• instDecidableEqTerm = instDecidableEqTerm.decEq

def instReprTerm.repr : Term → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprTerm.repr (Term.atom a) prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Term.atom" ++ Std.Format.line ++ reprArg a)).group prec✝

@[implicit_reducible]

instance instReprTerm : Repr Term

Equations

• instReprTerm = { reprPrec := instReprTerm.repr }

inductive ReducesStar (R : Term → Term → Prop) : Term → Term → Prop

• refl {R : Term → Term → Prop} (t : Term) : ReducesStar R t t
• trans {R : Term → Term → Prop} (t1 t2 t3 : Term) : R t1 t2 → ReducesStar R t2 t3 → ReducesStar R t1 t3

def IsNormalForm (R : Term → Term → Prop) (t : Term) : Prop

Equations

• IsNormalForm R t = ∀ (t' : Term), ¬R t t'

theorem normal_form_reduces_star_eq {R : Term → Term → Prop} {t t' : Term} (hnf : IsNormalForm R t) (hr : ReducesStar R t t') : t = t'

theorem uniqueness_of_normal_forms {R : Term → Term → Prop} (h_confl : ∀ {t t1 t2 : Term}, ReducesStar R t t1 → ReducesStar R t t2 → ∃ (t3 : Term), ReducesStar R t1 t3 ∧ ReducesStar R t2 t3) {t t1 t2 : Term} (h1 : ReducesStar R t t1) (h2 : ReducesStar R t t2) (hnf1 : IsNormalForm R t1) (hnf2 : IsNormalForm R t2) : t1 = t2

inductive Derivable (S : List Term) : Term → Prop

• member {S : List Term} (t : Term) (h : t ∈ S) : Derivable S t
• pair_intro {S : List Term} (t1 t2 : Term) (h1 : Derivable S t1) (h2 : Derivable S t2) : Derivable S (t1.pair t2)
• pair_elim_left {S : List Term} (t1 t2 : Term) (h : Derivable S (t1.pair t2)) : Derivable S t1
• pair_elim_right {S : List Term} (t1 t2 : Term) (h : Derivable S (t1.pair t2)) : Derivable S t2
• op_intro {S : List Term} (name : String) (t : Term) (h : Derivable S t) : Derivable S (Term.op name t)
• op_elim {S : List Term} (name : String) (t : Term) (h : Derivable S (Term.op name t)) : Derivable S t
• hash_intro {S : List Term} (t : Term) (h : Derivable S t) : Derivable S t.hash

def termSize : Term → Nat

Equations

• termSize (Term.atom a) = 1
• termSize (a.pair a_1) = termSize a + termSize a_1 + 1
• termSize (Term.op a a_1) = termSize a_1 + 1
• termSize a.hash = termSize a + 1

def NoHash (nf : Term) : Term → Prop

Equations

• NoHash nf (Term.atom a) = True
• NoHash nf (a.pair a_1) = (NoHash nf a ∧ NoHash nf a_1)
• NoHash nf (Term.op a a_1) = NoHash nf a_1
• NoHash nf a.hash = (a ≠ nf ∧ NoHash nf a)

theorem size_pos (t : Term) : termSize t > 0

theorem size_contains_hash {nf t : Term} (h : ¬NoHash nf t) : termSize t ≥ termSize nf.hash

theorem nohash_nf (nf : Term) : NoHash nf nf

def subst (nf d : Term) : Term → Term

Equations

• subst nf d (Term.atom a) = Term.atom a
• subst nf d (a.pair a_1) = (subst nf d a).pair (subst nf d a_1)
• subst nf d (Term.op a a_1) = Term.op a (subst nf d a_1)
• subst nf d a.hash = if a = nf then d else (subst nf d a).hash

theorem subst_noop {nf d t : Term} (h : NoHash nf t) : subst nf d t = t

theorem mem_map_of_mem {α β : Type} (f : α → β) {a : α} {l : List α} (h : a ∈ l) : f a ∈ List.map f l

theorem derivable_mono (S1 S2 : List Term) (h_sub : ∀ (x : Term), x ∈ S1 → x ∈ S2) {t : Term} (h : Derivable S1 t) : Derivable S2 t

theorem derivable_subst_map (S : List Term) (nf d : Term) (hd : Derivable (List.map (subst nf d) S) d) {t : Term} (h : Derivable S t) : Derivable (List.map (subst nf d) S) (subst nf d t)

theorem derivable_cut (S1 S2 : List Term) (h_sub : ∀ (x : Term), x ∈ S1 → Derivable S2 x) {t : Term} (h : Derivable S1 t) : Derivable S2 t

theorem map_subst_noop {nf d : Term} {l : List Term} (h : ∀ (x : Term), x ∈ l → NoHash nf x) : List.map (subst nf d) l = l

inductive BuiltFromHash (nf : Term) : Term → Prop

• base {nf : Term} : BuiltFromHash nf nf.hash
• pair_intro {nf t1 t2 : Term} (h1 : BuiltFromHash nf t1) (h2 : BuiltFromHash nf t2) : BuiltFromHash nf (t1.pair t2)
• op_intro {nf : Term} {o : String} {t : Term} (h : BuiltFromHash nf t) : BuiltFromHash nf (Term.op o t)
• hash_intro {nf t : Term} (h : BuiltFromHash nf t) : BuiltFromHash nf t.hash

theorem built_from_hash_size {nf t : Term} (h : BuiltFromHash nf t) : termSize t > termSize nf

theorem derivable_single_hash_imp {nf : Term} {S : List Term} {t : Term} (hS : S = [nf.hash]) (h : Derivable S t) : BuiltFromHash nf t

theorem derivable_single_hash_nf {nf : Term} (h : Derivable [nf.hash] nf) : False

theorem built_from_hash_not_nohash {nf t : Term} (h : BuiltFromHash nf t) : ¬NoHash nf t

theorem non_deducibility_of_preimages_symbolic (S : List Term) (nf : Term) (h_nohash : ∀ (x : Term), x ∈ S → NoHash nf x) : ¬Derivable S nf → ¬Derivable (nf.hash :: S) nf

theorem hash_noninterference_symbolic (S : List Term) (nf t' : Term) (_h_ne : nf ≠ t') (h_nohash_S : ∀ (x : Term), x ∈ S → NoHash nf x) (h_nohash_t' : NoHash nf t') : ¬Derivable S t' → ¬Derivable (nf.hash :: S) t'

theorem hash_preserves_non_derivability (S : List Term) (nf t' : Term) (h_nohash_S : ∀ (x : Term), x ∈ S → NoHash nf x) (h_nohash_t' : NoHash nf t') : ¬Derivable S t' → ¬Derivable (nf.hash :: S) t'

def SymbolicallySecret (S : List Term) (nf : Term) : Prop

Symbolic Secrecy: The normal form nf is not derivable from the adversary's view S.

Equations

• SymbolicallySecret S nf = ¬Derivable S nf

theorem forward_secrecy (S : List Term) (nf : Term) (h_nohash_S : ∀ (x : Term), x ∈ S → NoHash nf x) (h_not_derivable : ¬Derivable S nf) : ¬Derivable (nf.hash :: S) nf

structure AnchorChain : Type

Anchor chain state: an evolving context S and a list of normal forms nfs with their anchors.

• S : List Term
• nfs : List Term

def exposeAnchors (c : AnchorChain) : List Term

Expose all anchors for a chain by consing their hashes onto S.

Equations

• exposeAnchors c = List.map (fun (nf : Term) => nf.hash) c.nfs ++ c.S

def ChainIndependent (nfs S : List Term) : Prop

Equations

• ChainIndependent nfs S = (nfs.Nodup ∧ (∀ (x : Term), x ∈ nfs → ∀ (y : Term), y ∈ S → NoHash x y) ∧ ∀ (x : Term), x ∈ nfs → ∀ (y : Term), y ∈ nfs → x ≠ y → NoHash x y)

theorem derivable_under_hashes (S nfs : List Term) (t : Term) (h_not : ¬Derivable S t) (h_nohash : ∀ (x : Term), x ∈ nfs → NoHash x t) (h_nohash_S : ∀ (x : Term), x ∈ nfs → ∀ (y : Term), y ∈ S → NoHash x y) (h_nohash_self : ∀ (x : Term), x ∈ nfs → ∀ (y : Term), y ∈ nfs → x ≠ y → NoHash x y) (h_nodup : nfs.Nodup) : ¬Derivable (List.map (fun (nf : Term) => nf.hash) nfs ++ S) t

theorem chain_forward_secrecy (c : AnchorChain) (h_ind : ChainIndependent c.nfs c.S) (h_opaque : ∀ (nf : Term), nf ∈ c.nfs → SymbolicallySecret c.S nf) (nf : Term) : nf ∈ c.nfs → SymbolicallySecret (exposeAnchors c) nf

def mask : Term → Term

Equations

• mask (Term.atom a) = Term.atom "masked"
• mask (a.pair a_1) = (mask a).pair (mask a_1)
• mask (Term.op a a_1) = Term.op a (mask a_1)
• mask a.hash = (mask a).hash

def restore : Term → String → Term

Equations

• restore (Term.atom a) x✝ = Term.atom ("restored_with_".append x✝)
• restore (t1.pair t2) x✝ = (restore t1 x✝).pair (restore t2 x✝)
• restore (Term.op name t) x✝ = Term.op name (restore t x✝)
• restore t.hash x✝ = (restore t x✝).hash

def merge (t1 t2 : Term) : Term

Equations

• merge t1 t2 = t1.pair t2

theorem mask_distributes_over_merge (t1 t2 : Term) : mask (merge t1 t2) = merge (mask t1) (mask t2)

theorem homomorphic_merge (t1 t2 : Term) (a : String) : restore (merge (mask t1) (mask t2)) a = merge (restore (mask t1) a) (restore (mask t2) a)