diff --git a/.gitignore b/.gitignore
index bfb30ec..ad22248 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /.lake
+.aider*
diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean
new file mode 100644
index 0000000..d6e1d9d
--- /dev/null
+++ b/InductiveVerification/Message.lean
@@ -0,0 +1,1496 @@
+import Mathlib
+
+-- Keys are integers
+abbrev Key := Nat
+
+-- Define constants
+def all_symmetric : Bool := true -- true if all keys are symmetric
+
+-- Define the inverse of a symmetric key
+def invKey : Key → Key := fun k => k -- Placeholder definition
+
+-- Specification for invKey
+axiom invKey_spec : ∀ K : Key, invKey (invKey K) = K
+axiom invKey_symmetric : all_symmetric → invKey = id
+
+-- Define the set of symmetric keys
+@[grind]
+def symKeys : Set Key := { K | invKey K = K }
+
+-- Define the datatype for agents
+@[grind]
+inductive Agent
+  | Server : Agent
+  | Friend : Nat → Agent
+  | Spy : Agent
+
+@[grind]
+inductive Msg
+  | Agent : Agent → Msg -- Agent names
+  | Number : Nat → Msg -- Ordinary integers, timestamps, ...
+  | Nonce : Nat → Msg -- Unguessable nonces
+  | Key : Key → Msg -- Crypto keys
+  | Hash : Msg → Msg -- Hashing
+  | MPair : Msg → Msg → Msg -- Compound messages
+  | Crypt : Key → Msg → Msg -- Encryption, public- or shared-key
+
+namespace Msg
+-- Define concrete syntax for message tuples
+notation "⦃" x ", " y "⦄" => MPair x y
+notation "⦃" x ", " y ", " z "⦄" => MPair x (MPair y z)
+end Msg
+
+open Msg
+open Agent
+-- Define HPair
+def HPair (X Y : Msg) : Msg :=
+  ⦃Hash ⦃X, Y⦄, Y⦄
+
+notation "⦃" x ", " y "⦄ₕ" => HPair x y
+
+-- Define keysFor
+@[simp]
+def keysFor (H : Set Msg) : Set Key :=
+  invKey '' { K | ∃ X, Crypt K X ∈ H }
+
+-- Define the inductive set `parts`
+@[grind]
+inductive parts (H : Set Msg) : Set Msg
+  | inj {X : Msg} : X ∈ H → parts H X
+  | fst {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H X
+  | snd {X Y : Msg} : ⦃X, Y⦄ ∈ parts H → parts H Y
+  | body {K : Key} {X : Msg} : Crypt K X ∈ parts H → parts H X
+
+-- Monotonicity lemmas
+
+/--
+An `apply` tactic that also calls the assumptions
+-/
+syntax "aapply" term  : tactic
+macro_rules
+  |`(tactic| aapply $l:term) => `(tactic| apply $l <;> try assumption)
+
+@[simp]
+lemma parts_mono: Monotone parts := by
+  intro _ _ h _ a
+  induction a
+  · apply parts.inj; aapply h
+  · aapply parts.fst
+  · aapply parts.snd
+  · aapply parts.body
+
+-- Equations for injective constructors
+@[simp]
+lemma Friend_image_eq {A : Set Nat} {x : Nat} :
+  ((Friend x) ∈ Friend '' A) = (x ∈ A) := by
+  simp
+
+@[simp]
+lemma Key_image_eq {A : Set Key} {x : Key} :
+  (Key x ∈ Key '' A) = (x ∈ A) := by
+  simp
+
+@[simp]
+lemma Nonce_Key_image_eq {A : Set Key} {x : Nat} :
+  (Nonce x ∉ Key '' A) := by
+  simp
+
+-- Lemma: Inverse of keys
+@[simp]
+lemma invKey_eq (K K' : Key) : (invKey K = invKey K') ↔ (K = K') := by
+  apply Iff.intro
+  case mp =>
+    intro h
+    rw [←invKey_spec K, ←invKey_spec K', h]
+  case mpr =>
+    intro h
+    rw [h]
+
+-- Lemmas for the `keysFor` operator
+@[simp]
+lemma keysFor_empty : keysFor ∅ = ∅ := by
+  simp
+
+@[simp]
+lemma keysFor_union (H H' : Set Msg) : keysFor (H ∪ H') = keysFor H ∪ keysFor H' := by
+  simp
+  ext
+  constructor
+  · intro h; simp_all; grind
+  · intro h; simp_all; grind
+
+-- Monotonicity
+@[simp]
+lemma keysFor_mono {G H : Set Msg} (h : G ⊆ H) : keysFor G ⊆ keysFor H := by
+  simp
+  grind
+
+-- Lemmas for `keysFor` with specific message types
+@[simp]
+lemma keysFor_insert_Agent (A : Agent) (H : Set Msg) :
+    keysFor (insert (Agent A) H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_Nonce (N : Nat) (H : Set Msg) :
+    keysFor (insert (Nonce N) H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_Number (N : Nat) (H : Set Msg) :
+    keysFor (insert (Msg.Hash (Nonce N)) H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_Key (K : Key) (H : Set Msg) :
+    keysFor (insert (Key K) H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_Hash (X : Msg) (H : Set Msg) :
+    keysFor (insert (Hash X) H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_MPair (X Y : Msg) (H : Set Msg) :
+    keysFor (insert ⦃X, Y⦄ H) = keysFor H := by
+  simp
+
+@[simp]
+lemma keysFor_insert_Crypt (K : Key) (X : Msg) (H : Set Msg) :
+    keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H) := by
+  simp[insert,Set.insert,invKey]
+  ext
+  grind
+
+@[simp]
+lemma keysFor_image_Key (E : Set Key) : keysFor (Key '' E) = ∅ := by
+  simp
+
+@[simp]
+lemma Crypt_imp_invKey_keysFor (K : Key) (X : Msg) (H : Set Msg) :
+    Crypt K X ∈ H → invKey K ∈ keysFor H := by
+  intro h
+  simp
+  exact ⟨_, h⟩
+
+-- MPair_parts lemma
+@[simp]
+lemma MPair_parts {H : Set Msg} {X Y : Msg} { P : Prop} :
+  ⦃X, Y⦄ ∈ parts H → (parts H X  → parts H Y → P) → P :=
+by
+  grind
+
+-- parts_increasing lemma
+@[simp]
+lemma parts_increasing {H : Set Msg} : H ⊆ parts H :=
+  λ _ hx => parts.inj hx
+
+-- parts_empty_aux lemma
+@[simp]
+lemma parts_empty_aux {X : Msg} : parts ∅ X → False :=
+by
+  intro h
+  induction h <;> assumption
+
+-- parts_empty lemma
+@[simp]
+lemma parts_empty : parts ∅ = ∅ :=
+  Set.eq_empty_of_forall_notMem @parts_empty_aux
+
+-- parts_emptyE lemma
+lemma parts_emptyE {X : Msg} {P: Prop} : X ∈ parts ∅ → P :=
+  λ h => False.elim (parts_empty_aux h)
+
+-- parts_singleton lemma
+lemma parts_singleton {H : Set Msg} {X : Msg} :
+  X ∈ parts H → ∃ Y ∈ H, X ∈ parts {Y} :=
+by
+  intro h
+  induction h with
+  | inj h => exact ⟨_, h, parts.inj (Set.mem_singleton _)⟩
+  | fst _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.fst; exact r
+  | snd _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.snd; exact r
+  | body _ ih => rcases ih with ⟨Z, ⟨l, r⟩⟩; exists Z; and_intros; apply l; apply parts.body; exact r
+
+-- parts_union lemma
+@[simp]
+lemma parts_union {G H : Set Msg} : parts (G ∪ H) = parts G ∪ parts H :=
+by
+  apply Set.ext
+  intro X
+  constructor
+  · intro h
+    induction h with
+    | inj h => cases h with
+      | inl hG => exact Or.inl (parts.inj hG)
+      | inr hH => exact Or.inr (parts.inj hH)
+    | fst h ih => cases ih with
+      | inl hG => exact Or.inl (parts.fst hG)
+      | inr hH => exact Or.inr (parts.fst hH)
+    | snd h ih => cases ih with
+      | inl hG => exact Or.inl (parts.snd hG)
+      | inr hH => exact Or.inr (parts.snd hH)
+    | body h ih => cases ih with
+      | inl hG => exact Or.inl (parts.body hG)
+      | inr hH => exact Or.inr (parts.body hH)
+  · intro h
+    cases h with
+    | inl hG => induction hG with
+      | inj hG => exact parts.inj (Or.inl hG)
+      | fst h ih => exact parts.fst ih
+      | snd h ih => exact parts.snd ih
+      | body h ih => exact parts.body ih
+    | inr hH => induction hH with
+      | inj hH => exact parts.inj (Or.inr hH)
+      | fst h ih => exact parts.fst ih
+      | snd h ih => exact parts.snd ih
+      | body h ih => exact parts.body ih
+
+-- parts_insert lemma
+@[simp]
+lemma parts_insert {X : Msg} {H : Set Msg} :
+  parts (insert X H) = parts {X} ∪ parts H :=
+by
+  rw [Set.insert_eq, parts_union]
+
+-- parts_insert2 lemma
+@[simp]
+lemma parts_insert2 {X Y : Msg} {H : Set Msg} :
+  parts (insert X (insert Y H)) = parts {X} ∪ parts {Y} ∪ parts H :=
+by
+rw [Set.insert_eq, Set.insert_eq, parts_union, parts_union]
+grind
+
+-- parts_image lemma
+@[simp]
+lemma parts_image {f : Msg → Msg} {A : Set Msg} :
+  parts (f '' A) = ⋃ x ∈ A, parts {f x} :=
+by
+  apply Set.ext
+  intro X
+  constructor
+  · intro h
+    induction h with
+    | inj h => rcases h with ⟨a, ha, rfl⟩; exact Set.mem_biUnion ha (parts.inj (Set.mem_singleton _))
+    | fst _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.fst at r; exists W;
+    | snd _ ih => simp_all; rcases ih with ⟨W, ⟨_, r⟩⟩; apply parts.snd at r; exists W;
+    | body _ ih => simp_all; rcases ih with ⟨K, ⟨_, r⟩⟩; apply parts.body at r; exists K;
+  · intro h
+    simp_all
+    rcases h with ⟨W, ⟨_, r⟩⟩; induction r with
+      | inj a => simp_all; apply parts.inj; exists W;
+      | fst _ ih => exact parts.fst ih
+      | snd _ ih => exact parts.snd ih
+      | body _ ih => exact parts.body ih
+
+-- parts_insert_subset lemma
+@[simp]
+lemma parts_insert_subset {X : Msg} {H : Set Msg} :
+  insert X (parts H) ⊆ parts (insert X H) :=
+by
+  intro x hx
+  cases hx with
+  | inl h => simp_all; left; apply parts.inj; simp;
+  | inr h => induction h with
+    | inj h => exact parts.inj (Set.mem_insert_of_mem _ h)
+    | fst h ih => exact parts.fst ih
+    | snd h ih => exact parts.snd ih
+    | body h ih => exact parts.body ih
+
+
+-- Idempotence and transitivity lemmas for `parts`
+@[simp]
+lemma parts_partsD {H : Set Msg} : parts (parts H) ⊆ parts H :=
+by
+  intro x h
+  induction h
+  · assumption
+  · aapply parts.fst
+  · aapply parts.snd
+  · aapply parts.body
+
+abbrev partsClosureOperator : ClosureOperator (Set Msg) :=
+  ClosureOperator.mk' parts parts_mono @parts_increasing @parts_partsD
+
+@[simp]
+lemma parts_idem {H : Set Msg} : parts (parts H) = parts H :=
+  by apply partsClosureOperator.idempotent
+
+@[simp]
+lemma parts_subset_iff {G H : Set Msg} : (G ⊆ parts H) ↔ (parts G ⊆ parts H) :=
+by apply partsClosureOperator.le_closure_iff
+
+@[simp, grind]
+lemma parts_trans {G H : Set Msg} {X : Msg} :
+  X ∈ parts G → G ⊆ parts H → X ∈ parts H :=
+by intro a b; apply parts_mono at b; rw[parts_idem] at b; apply b; apply a;
+
+-- Cut lemma
+@[simp]
+lemma parts_cut {G H : Set Msg} {X Y : Msg} :
+  Y ∈ parts (insert X G) → X ∈ parts H → Y ∈ parts (G ∪ H) :=
+by
+  intro a b; rw[parts_union]; rw[parts_insert] at a; cases a <;> grind
+
+-- Rewrite rules for pulling out atomic messages
+
+@[simp]
+lemma parts_insert_Agent {H : Set Msg} {agt : Agent} :
+  parts (insert (Agent agt) H) = insert (Agent agt) (parts H) :=
+by
+  ext
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => right; assumption
+  · apply parts_insert_subset
+
+@[simp]
+lemma parts_insert_Nonce {H : Set Msg} {N : Nat} :
+  parts (insert (Nonce N) H) = insert (Nonce N) (parts H) :=
+by
+  ext
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => right; assumption
+  · apply parts_insert_subset
+
+@[simp]
+lemma parts_insert_Number {H : Set Msg} {N : Nat} :
+  parts (insert (Number N) H) = insert (Number N) (parts H) :=
+by
+  ext
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => right; assumption
+  · apply parts_insert_subset
+
+@[simp]
+lemma parts_insert_Key {H : Set Msg} {K : Key} :
+  parts (insert (Key K) H) = insert (Key K) (parts H) :=
+by
+  ext
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => right; assumption
+  · apply parts_insert_subset
+
+@[simp]
+lemma parts_insert_Hash {H : Set Msg} {X : Msg} :
+  parts (insert (Hash X) H) = insert (Hash X) (parts H) :=
+by
+  ext
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => right; assumption
+  · apply parts_insert_subset
+
+@[simp]
+lemma parts_insert_Crypt {H : Set Msg} {K : Key} {X : Msg} :
+  parts (insert (Crypt K X) H) = insert (Crypt K X) (parts (insert X H)) :=
+by
+  ext x
+  constructor
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => left; assumption;
+      | fst _ a_ih => cases a_ih; contradiction; right; aapply parts.fst
+      | snd _ a_ih => cases a_ih; contradiction; right; aapply parts.snd
+      | body _ a_ih => cases a_ih with
+        | inl => simp_all; right; left; apply parts_increasing; trivial;
+        | inr h => apply parts.body at h; right; exact h;
+    | inr => right; simp; right; assumption;
+  · intro h; cases h with
+    | inl => apply parts.inj; left; assumption
+    | inr h => 
+      apply (parts_cut (G := H) (H := {Crypt K X}) (X := X) (Y := x)) at h 
+      rw[←Set.singleton_union, Set.union_comm]
+      apply h
+      apply parts.body (K := K) (X := X)
+      apply parts.inj
+      trivial
+      
+@[simp]
+lemma parts_insert_MPair {H: Set Msg} {X Y : Msg} :
+  parts (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (parts (insert X (insert Y H))) :=
+by 
+  ext x
+  constructor;
+  · intro h; rw[parts_insert] at h; cases h with
+    | inl h => induction h with
+      | inj => simp_all;
+      | @fst A B _ a_ih => cases a_ih with
+        | inl h => cases h; right; apply parts.inj; left; trivial
+        | inr h => right; aapply parts.fst;
+      | @snd A B _ a_ih => cases a_ih with
+        | inl h => cases h; right; apply parts.inj; right; left; trivial;
+        | inr h => right; aapply parts.snd;
+      | body _ a_ih => cases a_ih; contradiction; right; aapply parts.body
+    | inr h => simp; right; right; right; assumption;
+  · intro h; cases h with
+    | inl => rw[parts_insert]; left; apply parts.inj; assumption;
+    | inr h => simp_all; cases h with
+      | inl h => 
+        left;
+        apply parts_trans ( H := {⦃X, Y⦄}) at h;
+        simp at h;
+        apply h;
+        apply parts.fst;
+        apply parts.inj;
+        trivial;
+      | inr h => cases h with
+        | inl h => 
+            left;
+            apply parts_trans ( H := {⦃X, Y⦄}) at h;
+            simp at h;
+            apply h;
+            apply parts.snd;
+            apply parts.inj;
+            trivial;
+        | inr => right; assumption;
+
+@[simp]
+lemma parts_image_Key {N : Set Key} : parts (Key '' N) = Key '' N :=
+by 
+  ext
+  constructor
+  · intro a; simp; induction a <;> simp_all;
+  · simp; intro y _ _; apply parts.inj; simp; exists y;
+
+-- In any message, there is an upper bound N on its greatest nonce.
+lemma msg_Nonce_supply {msg : Msg} : ∃ N, ∀ n, N ≤ n → Nonce n ∉ parts {msg} :=
+by
+  induction msg with
+  | Agent a => exists 0;
+               have ins_agt := parts_insert_Agent (H := {}) (agt := a);
+               simp_all
+  | Number a => exists 0;
+                have ins_number := parts_insert_Number (H := {}) (N := a);
+                simp_all;
+  | Nonce n => exists n.succ;
+               intro _ _ _;
+               have ins_nonce := parts_insert_Nonce (H := {}) (N := n);
+               simp_all;
+  | Key k => exists 0;
+             have ins_key := parts_insert_Key (H := {}) (K := k);
+             simp_all;
+  | Hash X ih => exists 0;
+                 have ins_hash := parts_insert_Hash (H := {}) (X := X);
+                 simp_all;
+  | MPair X Y ihX ihY =>
+    rcases ihX with ⟨wX, hH⟩;
+    cases ihY with
+    | intro wY hY => exists Nat.max wX wY; intro n h₁ h₂;
+                     have ins_mpair := parts_insert_MPair (H := {}) (X := X) (Y := Y);
+                     simp_all;
+  | Crypt K X ih => rcases ih with ⟨N, h⟩; exists N;
+                    have ins_crypt := parts_insert_Crypt (H := {}) (K := K) (X := X);
+                    simp_all;
+
+-- Inductive relation "analz"
+inductive analz (H : Set Msg) : Set Msg
+  | inj {X : Msg} : X ∈ H → analz H X
+  | fst {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H X
+  | snd {X Y : Msg} : ⦃X, Y⦄ ∈ analz H → analz H Y
+  | decrypt {K : Key} {X : Msg} :
+      Crypt K X ∈ analz H → Key (invKey K) ∈ analz H → analz H X
+
+-- Monotonicity
+lemma analz_mono : Monotone analz :=
+by 
+  intro A B h₁ X h₂
+  induction h₂ with
+  | inj h => exact analz.inj (h₁ h)
+  | fst h ih => exact analz.fst ih
+  | snd h ih => exact analz.snd ih
+  | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
+
+-- Making it safe speeds up proofs
+@[simp]
+lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} :
+  ⦃X, Y⦄ ∈ analz H → (analz H X → analz H Y → P) → P :=
+by
+  intro h ih
+  apply ih
+  · apply analz.fst h
+  · apply analz.snd h
+
+@[simp]
+lemma analz_increasing {H : Set Msg} : H ⊆ analz H :=
+  λ _ hx => analz.inj hx
+
+lemma analz_into_parts {H : Set Msg} {X : Msg} : X ∈ analz H → X ∈ parts H :=
+by
+  intro h
+  induction h with
+  | inj h => aapply parts.inj
+  | fst _ ih => aapply parts.fst
+  | snd _ ih => aapply parts.snd
+  | decrypt _ _ ih₁ => aapply parts.body
+
+lemma analz_subset_parts {H : Set Msg} : analz H ⊆ parts H :=
+  λ _ hx => analz_into_parts hx
+
+@[simp]
+lemma analz_parts {H : Set Msg} : analz (parts H) = parts H :=
+by
+  ext X; constructor
+  · intro h; induction h with
+    | inj => assumption;
+    | fst => aapply parts.fst;
+    | snd => aapply parts.snd;
+    | decrypt => aapply parts.body;
+  · apply analz_increasing;
+
+lemma not_parts_not_analz {H : Set Msg} {X : Msg} :
+  X ∉ parts H → X ∉ analz H :=
+  λ h₁ h₂ => h₁ (analz_into_parts h₂)
+
+@[simp]
+lemma parts_analz {H : Set Msg} : parts (analz H) = parts H :=
+  by 
+    ext; constructor;
+    · intro h; induction h with
+      | inj => aapply analz_subset_parts
+      | fst => aapply parts.fst
+      | snd => aapply parts.snd
+      | body => aapply parts.body
+    · apply parts_mono; apply analz_increasing;
+
+@[simp]
+lemma analz_insertI {X : Msg} {H : Set Msg} :
+  insert X (analz H) ⊆ analz (insert X H) :=
+by
+  intro x hx
+  cases hx with
+  | inl h => apply analz.inj; left; assumption;
+  | inr h => exact analz_mono (Set.subset_insert _ _) h
+
+-- General equational properties
+
+@[simp]
+lemma analz_empty : analz ∅ = ∅ :=
+by 
+  ext; constructor;
+  · intro h; induction h <;> contradiction;
+  · apply analz_increasing
+
+
+@[simp]
+lemma analz_union {G H : Set Msg} : analz G ∪ analz H ⊆ analz (G ∪ H) :=
+  by
+    intro x hx
+    cases hx with
+    | inl hG => exact analz_mono (Set.subset_union_left) hG; 
+    | inr hH => exact analz_mono (Set.subset_union_right) hH
+
+lemma analz_insert {X : Msg} {H : Set Msg} :
+  insert X (analz H) ⊆ analz (insert X H) :=
+  by
+    intro x hx
+    cases hx with
+    | inl h => apply analz.inj; left; assumption
+    | inr h => exact analz_mono (Set.subset_insert _ _) h
+
+-- Rewrite rules for pulling out atomic messages
+
+@[simp]
+lemma analz_insert_Agent {H : Set Msg} {agt : Agent} :
+  analz (insert (Agent agt) H) = insert (Agent agt) (analz H) :=
+  by
+    ext
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr h => exact Or.inr (analz.inj h)
+      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
+      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
+      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
+                               cases ih₂; contradiction;
+                               aapply analz.decrypt;
+    · apply analz_insert
+
+@[simp]
+lemma analz_insert_Nonce {H : Set Msg} {N : Nat} :
+  analz (insert (Nonce N) H) = insert (Nonce N) (analz H) :=
+  by
+    ext
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr h => exact Or.inr (analz.inj h)
+      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
+      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
+      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
+                               cases ih₂; contradiction;
+                               aapply analz.decrypt;
+    · apply analz_insert
+
+@[simp]
+lemma analz_insert_Number {H : Set Msg} {N : Nat} :
+  analz (insert (Number N) H) = insert (Number N) (analz H) :=
+  by
+    ext
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr h => exact Or.inr (analz.inj h)
+      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
+      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
+      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
+                               cases ih₂; contradiction;
+                               aapply analz.decrypt;
+    · apply analz_insert
+
+@[simp]
+lemma analz_insert_Hash {H : Set Msg} {X : Msg} :
+  analz (insert (Hash X) H) = insert (Hash X) (analz H) :=
+  by
+    ext
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr h => exact Or.inr (analz.inj h)
+      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
+      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
+      | decrypt _ _ ih₁ ih₂ => right; cases ih₁; contradiction;
+                               cases ih₂; contradiction;
+                               aapply analz.decrypt;
+    · apply analz_insert
+
+@[simp]
+lemma analz_insert_Key {H : Set Msg} {K : Key} :
+  K ∉ keysFor (analz H) →
+  analz (insert (Key K) H) = insert (Key K) (analz H) :=
+  by
+    intro hK
+    ext x
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr h => exact Or.inr (analz.inj h)
+      | fst _ ih => right; cases ih; contradiction; aapply analz.fst;
+      | snd _ ih => right; cases ih; contradiction; aapply analz.snd;
+      | @decrypt _ _ _ _ ih₁ ih₂ =>
+      right
+      cases ih₂ with
+      | inl h => simp at h; simp at ih₁; apply Crypt_imp_invKey_keysFor at ih₁
+                 rw[h] at ih₁; contradiction;
+      | inr => cases ih₁; simp_all; aapply analz.decrypt
+    · apply analz_insert
+
+@[simp]
+lemma analz_insert_MPair {H : Set Msg} {X Y : Msg} :
+  analz (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (analz (insert X (insert Y H))) :=
+  by
+    ext
+    constructor
+    · intro h
+      induction h with
+      | inj h => cases h with
+        | inl h => exact Or.inl h
+        | inr => right; apply analz.inj; right; right; assumption
+      | fst _ ih => right; cases ih
+                    · simp_all; apply analz.inj; left; trivial
+                    · aapply analz.fst
+      | snd _ ih => right; cases ih
+                    · simp_all; apply analz.inj; right; left; trivial
+                    · aapply analz.snd
+      | decrypt h₁ h₂ ih₁ ih₂ =>
+      right
+      cases ih₂; contradiction
+      cases ih₁; contradiction
+      aapply analz.decrypt
+    · intro h
+      cases h with
+      | inl => apply analz.inj; left; trivial
+      | inr h => induction h with
+        | inj a => cases a with
+          | inl h => apply analz.fst; apply analz.inj; left; rw[h]
+          | inr h => cases h with
+            | inl h => apply analz.snd; apply analz.inj; left; rw[h]
+            | inr => apply analz.inj; right; assumption
+        | fst => aapply analz.fst
+        | snd => aapply analz.snd
+        | decrypt => aapply analz.decrypt
+
+lemma analz_insert_Decrypt {H : Set Msg} {K : Key} {X : Msg} :
+  Key (invKey K) ∈ analz H →
+  analz (insert (Crypt K X) H) = insert (Crypt K X) (analz (insert X H)) :=
+by
+  intro
+  ext
+  constructor
+  · intro h
+    induction h with
+    | inj h => cases h with
+      | inl => left; assumption;
+      | inr => right; apply analz.inj; right; assumption
+    | fst _ ih => right; cases ih; contradiction; aapply analz.fst
+    | snd _ ih => right; cases ih; contradiction; aapply analz.snd
+    | decrypt _ _ ih₁ ih₂ => cases ih₁ with
+      | inl h => right; apply analz.inj; left; simp_all
+      | inr => right; cases ih₂; contradiction; aapply analz.decrypt
+  · intro h
+    cases h with
+    | inl h => apply analz.inj; left; assumption
+    | inr h => induction h with
+      | inj a => cases a with
+        | inl h => apply analz.decrypt; apply analz.inj; left; rw[h]
+                   apply analz_mono; apply Set.subset_insert; assumption
+        | inr => apply analz.inj; right; assumption
+      | fst => aapply analz.fst
+      | snd => aapply analz.snd
+      | decrypt => aapply analz.decrypt
+
+-- TODO split into two lemmata
+@[simp]
+lemma analz_Crypt {H : Set Msg} {K : Key} {X : Msg} :
+  (Key (invKey K) ∉ analz H) →
+  (analz (insert (Crypt K X) H) = insert (Crypt K X) (analz H)) :=
+by
+  intro h
+  ext
+  constructor
+  · intro a; induction a with
+    | inj a => cases a; left; assumption; right; aapply analz.inj
+    | fst _ a_ih => cases a_ih; contradiction; right; aapply analz.fst
+    | snd _ a_ih => cases a_ih; contradiction; right; aapply analz.snd
+    | decrypt h₁ h₂ ih₁ ih₂ =>
+    cases ih₂; contradiction 
+    cases ih₁; simp_all; right; aapply analz.decrypt
+  · intro a; cases a with
+    | inl => apply analz.inj; left; assumption
+    | inr => apply analz_mono; apply Set.subset_insert; assumption
+          
+-- This rule supposes "for the sake of argument" that we have the key.
+lemma analz_insert_Crypt_subset {H : Set Msg} {K : Key} {X : Msg} :
+  analz (insert (Crypt K X) H) ⊆ insert (Crypt K X) (analz (insert X H)) :=
+by
+  intro Y h
+  induction h with
+  | inj h => cases h with
+    | inl => left; assumption
+    | inr => right; apply analz.inj; right; assumption
+  | fst _ ih => right; cases ih; contradiction; aapply analz.fst
+  | snd _ ih => right; cases ih; contradiction; aapply analz.snd
+  | decrypt _ _ ih₁ ih₂ =>
+  right
+  cases ih₂; contradiction
+  cases ih₁ with
+  | inl => simp_all; apply analz.inj; left; trivial
+  | inr => aapply analz.decrypt
+
+@[simp]
+lemma analz_image_Key {N : Set Key} : analz (Key '' N) = Key '' N :=
+by
+  apply Set.ext
+  intro X
+  constructor
+  · intro h
+    induction h <;> simp_all
+  · intro h
+    rcases h with ⟨k, hk, rfl⟩
+    exact analz.inj ⟨k, hk, rfl⟩
+
+-- Idempotence and transitivity
+
+@[simp]
+lemma analz_analzD {H : Set Msg} {X : Msg} : X ∈ analz (analz H) → X ∈ analz H :=
+by
+  intro h
+  induction h with
+  | inj h => exact h
+  | fst h ih => exact analz.fst ih
+  | snd h ih => exact analz.snd ih
+  | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
+ 
+abbrev analzClosureOperator : ClosureOperator (Set Msg) :=
+  ClosureOperator.mk' analz analz_mono @analz_increasing @analz_analzD
+
+@[simp]
+lemma analz_idem {H : Set Msg} : analz (analz H) = analz H :=
+  by apply analzClosureOperator.idempotent
+
+@[simp]
+lemma analz_subset_iff {G H : Set Msg} : (G ⊆ analz H) ↔ (analz G ⊆ analz H) :=
+  by apply analzClosureOperator.le_closure_iff
+
+@[simp]
+lemma analz_trans {G H : Set Msg} {X : Msg} :
+  X ∈ analz G → G ⊆ analz H → X ∈ analz H :=
+by
+  intro hG hGH
+  apply analz_mono at hGH; rw [ analz_idem ] at hGH; apply hGH; assumption;
+
+-- Cut; Lemma 2 of Lowe
+@[simp]
+lemma analz_cut {H : Set Msg} {X Y : Msg} :
+  Y ∈ analz (insert X H) → X ∈ analz H → Y ∈ analz H :=
+by
+  intro hY _
+  apply analz_trans; apply hY
+  intro a h; cases h; simp_all; aapply analz.inj
+
+-- Simplification of messages involving forwarding of unknown components
+@[simp]
+lemma analz_insert_eq {H : Set Msg} {X : Msg} :
+  X ∈ analz H → analz (insert X H) = analz H :=
+by
+  intro
+  ext
+  constructor
+  · intro; aapply analz_cut
+  · apply analz_mono; apply Set.subset_insert
+
+-- A congruence rule for "analz"
+@[simp]
+lemma analz_subset_cong {G G' H H' : Set Msg} :
+  analz G ⊆ analz G' → analz H ⊆ analz H' → analz (G ∪ H) ⊆ analz (G' ∪ H') :=
+by
+  intro hG hH
+  have a_sub := analz_subset_iff (G := G ∪ H) (H := G' ∪ H')
+  apply a_sub.mp
+  apply subset_trans (b := analz G ∪ analz H)
+  apply Set.union_subset_union (h₁ := @analz_increasing (H := G)) (h₂ := @analz_increasing (H := H))
+  apply subset_trans (b := analz G' ∪ analz H')
+  apply Set.union_subset_union (h₁ := hG) (h₂ := hH)
+  apply analz_union
+
+lemma analz_cong {G G' H H' : Set Msg} :
+  analz G = analz G' → analz H = analz H' → analz (G ∪ H) = analz (G' ∪ H') :=
+by
+  intro hG hH
+  ext
+  constructor
+  · apply analz_subset_cong; aapply Eq.subset; aapply Eq.subset
+  · apply analz_subset_cong; rw[Eq.comm] at hG; aapply Eq.subset; rw[Eq.comm] at hH; aapply Eq.subset
+
+
+lemma analz_insert_cong {H H' : Set Msg} {X : Msg} :
+  analz H = analz H' → analz (insert X H) = analz (insert X H') :=
+by
+  intro hH
+  rw [Set.insert_eq, Set.insert_eq]
+  exact analz_cong rfl hH
+
+-- If there are no pairs or encryptions, then analz does nothing
+lemma analz_trivial {H : Set Msg} :
+  (∀ X Y, ⦃X, Y⦄ ∉ H) → (∀ X K, Crypt K X ∉ H) → analz H = H :=
+by
+  intro hPairs hCrypts
+  apply Set.ext
+  intro X
+  constructor
+  · intro h
+    induction h with
+    | inj h => exact h
+    | fst => simp_all
+    | snd => simp_all
+    | decrypt h₁ _ _ => simp_all
+  · exact analz.inj
+
+-- Inductive relation "synth"
+
+inductive synth (H : Set Msg) : Set Msg
+  | inj {X : Msg} : X ∈ H → synth H X
+  | agent {agt : Agent} : synth H (Agent agt)
+  | number {n : Nat} : synth H (Number n)
+  | hash {X : Msg} : synth H X → synth H (Hash X)
+  | mpair {X Y : Msg} : synth H X → synth H Y → synth H ⦃X, Y⦄
+  | crypt {K : Key} {X : Msg} : synth H X → Key K ∈ H → synth H (Crypt K X)
+
+-- Monotonicity
+lemma synth_mono : Monotone synth := by
+  intro _ _ h _ hx
+  induction hx with
+  | inj hG => exact synth.inj (h hG)
+  | agent => exact synth.agent
+  | number => exact synth.number
+  | hash _ ih => exact synth.hash ih
+  | mpair _ _ ihX ihY => exact synth.mpair ihX ihY
+  | crypt => aapply synth.crypt; aapply h 
+
+-- Simplification rules for `synth`
+@[simp]
+lemma synth_increasing {H : Set Msg} : H ⊆ synth H :=
+  λ _ hx => synth.inj hx
+
+-- Unions
+lemma synth_union {G H : Set Msg} : synth G ∪ synth H ⊆ synth (G ∪ H) :=
+by
+  intro x hx
+  cases hx with
+  | inl hG => exact synth_mono (Set.subset_union_left) hG
+  | inr hH => exact synth_mono (Set.subset_union_right) hH
+
+lemma synth_insert {X : Msg} {H : Set Msg} :
+  insert X (synth H) ⊆ synth (insert X H) :=
+by
+  intro x hx
+  cases hx with
+  | inl h => apply synth.inj; left; assumption
+  | inr h => exact synth_mono (Set.subset_insert _ _) h
+
+-- Idempotence and transitivity
+@[simp]
+lemma synth_synthD {H : Set Msg} {X : Msg} : X ∈ synth (synth H) → X ∈ synth H :=
+by
+  intro h
+  induction h with
+  | inj h => exact h
+  | agent => exact synth.agent
+  | number => exact synth.number
+  | hash _ ih => exact synth.hash ih
+  | mpair _ _ ihX ihY => exact synth.mpair ihX ihY
+  | crypt _ a => cases a; aapply synth.crypt;
+  
+abbrev synthClosureOperator : ClosureOperator (Set Msg) :=
+  ClosureOperator.mk' synth synth_mono @synth_increasing @synth_synthD
+
+@[simp]
+lemma synth_idem {H : Set Msg} : synth (synth H) = synth H :=
+  by apply synthClosureOperator.idempotent
+
+@[simp]
+lemma synth_subset_iff {G H : Set Msg} : (G ⊆ synth H) ↔ (synth G ⊆ synth H) :=
+by apply synthClosureOperator.le_closure_iff
+
+@[simp, grind]
+lemma synth_trans {G H : Set Msg} {X : Msg} :
+  X ∈ synth G → G ⊆ synth H → X ∈ synth H :=
+by
+  intro hG hGH; apply synth_mono at hGH; rw[synth_idem] at hGH; apply hGH; apply hG
+
+-- Cut; Lemma 2 of Lowe
+@[simp]
+lemma synth_cut {H : Set Msg} {X Y : Msg} :
+  Y ∈ synth (insert X H) → X ∈ synth H → Y ∈ synth H :=
+by
+  intro hY hX; apply synth_trans; apply hY
+  intro a h; cases h; simp_all; aapply synth.inj
+
+@[simp]
+lemma Crypt_synth_eq {H : Set Msg} {K : Key} {X : Msg} :
+  Key K ∉ H → (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) :=
+by
+  intro hK
+  constructor
+  · intro h
+    cases h; assumption; contradiction
+  · intro h
+    exact synth.inj h
+
+@[simp]
+lemma keysFor_synth {H : Set Msg} :
+  keysFor (synth H) = keysFor H ∪ invKey '' {K | Key K ∈ H} :=
+by
+  ext K
+  simp
+  constructor
+  · intro h
+    rcases h with ⟨Y, ⟨⟨X, h⟩, _⟩⟩;
+    cases h with
+    | inj h => left; exists Y; apply And.intro; exists X; assumption
+    | crypt _ _ => right; exists Y
+  · intro h; cases h with
+  | inl h =>  cases h with
+    | intro Y h =>
+    exists Y; rcases h with ⟨⟨X, _⟩, _⟩;
+    apply And.intro
+    · exists X; aapply synth.inj
+    · assumption
+  | inr h =>
+    rcases h with ⟨Y, ⟨_, _⟩⟩;
+    exists Y; apply And.intro
+    · exists Number 0; aapply synth.crypt; apply synth.number
+    · assumption
+
+
+-- Combinations of parts, analz, and synth
+
+@[simp]
+lemma parts_synth {H : Set Msg} : parts (synth H) = parts H ∪ synth H :=
+by
+  apply Set.ext
+  intro X
+  constructor
+  · intro h
+    induction h with
+    | inj => right; assumption
+    | fst _ ih => cases ih with
+      | inl => left; aapply parts.fst
+      | inr h => cases h
+                 · left; apply parts.fst; aapply parts.inj; 
+                 · right; assumption
+    | snd _ ih => cases ih with
+      | inl => left; aapply parts.snd
+      | inr h => cases h
+                 · left; apply parts.snd; aapply parts.inj; 
+                 · right; assumption
+    | body h ih => cases ih with
+      | inl h => left; aapply parts.body
+      | inr h => cases h
+                 · left; aapply parts.body; aapply parts.inj
+                 · right; assumption
+  · intro h
+    cases h with
+    | inl h =>
+    apply parts_mono
+    · apply synth_increasing
+    · assumption
+    | inr h => exact parts.inj h
+
+@[simp]
+lemma analz_analz_Un {G H : Set Msg} : analz (analz G ∪ H) = analz (G ∪ H) :=
+by
+  apply analz_cong
+  · exact analz_idem
+  · trivial
+
+@[simp]
+lemma analz_synth_Un {G H : Set Msg} : analz (synth G ∪ H) = analz (G ∪ H) ∪ synth G :=
+by
+  ext
+  constructor
+  · intro h; induction h with
+    | inj a => cases a
+               · right; assumption
+               · left; apply analz.inj; right; assumption
+    | fst _ ih =>
+    cases ih with
+        | inl => left; aapply analz.fst
+        | inr h => 
+        cases h
+        · left; apply analz.fst; apply analz.inj; left; assumption
+        · right; assumption
+    | snd _ ih => 
+    cases ih with
+        | inl => left; aapply analz.snd
+        | inr h => 
+        cases h
+        · left; apply analz.snd; apply analz.inj; left; assumption
+        · right; assumption
+    | decrypt _ _ ih₁ ih₂ =>
+    cases ih₂ with
+    | inl => cases ih₁ with
+      | inl => left; aapply analz.decrypt
+      | inr h => cases h
+                 · left; aapply analz.decrypt; apply analz.inj; left; assumption
+                 · right; assumption
+    | inr h => cases h; cases ih₁ with
+      | inl => left; aapply analz.decrypt; apply analz.inj; left; assumption
+      | inr h => cases h
+                 · left; aapply analz.decrypt <;> (apply analz.inj; left; assumption)
+                 · right; assumption
+  · apply sup_le (a := analz (G ∪ H)) (b := synth G) (c := analz ( synth G ∪ H ))
+    · apply analz_mono; apply Set.union_subset_union; apply synth_increasing; trivial
+    · apply analz_subset_iff.mpr; apply analz_mono; exact le_sup_left
+
+@[simp]
+lemma analz_synth {H : Set Msg} : analz (synth H) = analz H ∪ synth H :=
+  by have asu := analz_synth_Un (G := H) (H := ∅); simp_all
+
+-- For reasoning about the Fake rule in traces
+
+lemma parts_insert_subset_Un {G H : Set Msg} {X : Msg} :
+  X ∈ G → parts (insert X H) ⊆ parts G ∪ parts H :=
+by
+  intro hX
+  rw [Set.insert_eq, parts_union]
+  apply Set.union_subset_union
+  · apply parts_mono; simp_all
+  · trivial
+
+lemma Fake_parts_insert {H : Set Msg} {X : Msg} :
+  X ∈ synth (analz H) → parts (insert X H) ⊆ synth (analz H) ∪ parts H :=
+by
+  intro hX
+  rw [parts_insert]
+  apply sup_le
+  · apply subset_trans (b := synth (analz H) ∪ parts (analz H))
+    · rw [Set.union_comm, ←parts_synth]; apply parts_mono; simp; assumption
+    · rw [parts_analz]
+  · apply le_sup_of_le_right; trivial
+
+lemma Fake_parts_insert_in_Un {H : Set Msg} {X Z : Msg} :
+  Z ∈ parts (insert X H) → X ∈ synth (analz H) → Z ∈ synth (analz H) ∪ parts H :=
+by
+  intro hZ hX
+  exact Set.mem_of_subset_of_mem (Fake_parts_insert hX) hZ
+
+lemma Fake_analz_insert {G H : Set Msg} {X : Msg} :
+  X ∈ synth (analz G) → analz (insert X H) ⊆ synth (analz G) ∪ analz (G ∪ H) :=
+by
+  intro
+  apply subset_trans (b := analz (synth (analz G) ∪ H))
+  · apply analz_mono; rw[Set.insert_eq]; apply Set.union_subset_union; simp_all; trivial;
+  · rw[analz_synth_Un, Set.union_comm, analz_analz_Un]
+
+@[simp]
+lemma analz_conj_parts {H : Set Msg} {X : Msg} :
+  (X ∈ analz H ∧ X ∈ parts H) ↔ X ∈ analz H :=
+  by
+    constructor
+    · intro h
+      exact h.1
+    · intro h
+      exact ⟨h, analz_subset_parts h⟩
+
+@[simp]
+lemma analz_disj_parts {H : Set Msg} {X : Msg} :
+  (X ∈ analz H ∨ X ∈ parts H) ↔ X ∈ parts H :=
+  by
+    constructor
+    · intro h
+      cases h with
+      | inl h => apply analz_conj_parts.mpr at h; cases h; assumption
+      | inr h => assumption
+    · intro h
+      exact Or.inr h
+
+@[simp]
+lemma MPair_synth_analz {H : Set Msg} {X Y : Msg} :
+  ⦃X, Y⦄ ∈ synth (analz H) ↔ X ∈ synth (analz H) ∧ Y ∈ synth (analz H) :=
+  by
+    constructor
+    · intro h; cases h
+      · apply And.intro
+        · apply synth.inj; aapply analz.fst
+        · apply synth.inj; aapply analz.snd
+      · apply And.intro <;> assumption
+    · intro h; exact synth.mpair h.1 h.2
+
+lemma Crypt_synth_analz {H : Set Msg} {K : Key} {X : Msg} :
+  Key K ∈ analz H → Key (invKey K) ∈ analz H → ((Crypt K X ∈ synth (analz H)) ↔ X ∈ synth (analz H)) :=
+  by
+  intro _ _
+  constructor
+  · intro h; cases h
+    · apply synth.inj; aapply analz.decrypt
+    · assumption
+  · intro _; aapply synth.crypt
+
+@[simp]
+lemma Hash_synth_analz {H : Set Msg} {X Y : Msg} :
+  X ∉ synth (analz H) → ((Hash ⦃X, Y⦄ ∈ synth (analz H)) ↔ Hash ⦃X, Y⦄ ∈ analz H) :=
+  by
+  intro _
+  constructor
+  · intro h; cases h with
+    | inj => assumption
+    | hash h => cases h with
+      | inj a => apply analz.fst at a; apply synth.inj at a; contradiction
+      | mpair => contradiction
+  · intro h; aapply synth.inj
+
+-- HPair: a combination of Hash and MPair
+
+-- Freeness
+
+@[simp]
+lemma Agent_neq_HPair {A : Agent} {X Y : Msg} : Agent A ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma Nonce_neq_HPair {N : Nat} {X Y : Msg} : Nonce N ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma Number_neq_HPair {N : Nat} {X Y : Msg} : Number N ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma Key_neq_HPair {K : Key} {X Y : Msg} : Key K ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma Hash_neq_HPair {Z X Y : Msg} : Hash Z ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma Crypt_neq_HPair {K : Key} {X' X Y : Msg} : Crypt K X' ≠ ⦃X, Y⦄ₕ :=
+  by simp [HPair]
+
+@[simp]
+lemma HPair_eq {X' Y' X Y : Msg} : (⦃X', Y'⦄ₕ = ⦃X, Y⦄ₕ) ↔ (X' = X ∧ Y' = Y) :=
+  by simp [HPair]
+
+@[simp]
+lemma MPair_eq_HPair {X' Y' X Y : Msg} : (⦃X', Y'⦄ = ⦃X, Y⦄ₕ) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
+  by simp [HPair]
+
+@[simp]
+lemma HPair_eq_MPair {X' Y' X Y : Msg} : (⦃X, Y⦄ₕ = ⦃X', Y'⦄) ↔ (X' = Hash ⦃X, Y⦄ ∧ Y' = Y) :=
+  by simp [HPair]; nth_rw 1 [Eq.comm]; nth_rw 2 [Eq.comm]
+
+-- Specialized laws, proved in terms of those for Hash and MPair
+
+@[simp]
+lemma keysFor_insert_HPair {H : Set Msg} {X Y : Msg} :
+  keysFor (insert (⦃X, Y⦄ₕ) H) = keysFor H :=
+  by simp [HPair]
+
+@[simp]
+lemma parts_insert_HPair {H : Set Msg} {X Y : Msg} :
+  parts (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (parts (insert Y H))) :=
+by
+  simp [HPair]; rw[←Set.union_empty (a:= {⦃Hash ⦃X, Y⦄, Y⦄}), ←Set.insert_eq, parts_insert_MPair, parts_insert_Hash]
+  rw[Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq, Set.insert_eq]
+  rw[Set.union_empty]; simp only [Set.union_assoc]
+
+@[simp]
+lemma analz_insert_HPair {H : Set Msg} {X Y : Msg} :
+  analz (insert (⦃X, Y⦄ₕ) H) = insert (⦃X, Y⦄ₕ) (insert (Hash ⦃X, Y⦄) (analz (insert Y H))) :=
+  by simp [HPair]
+
+@[simp]
+lemma HPair_synth_analz {H : Set Msg} {X Y : Msg} :
+  X ∉ synth (analz H) →
+  ((⦃X, Y⦄ₕ ∈ synth (analz H)) ↔ (Hash ⦃X, Y⦄ ∈ analz H ∧ Y ∈ synth (analz H))) :=
+by
+  intro _; simp [HPair]; intro _; constructor
+  · intro h; cases h with
+    | inj => assumption
+    | hash a => cases a with
+      | inj a => apply analz.fst at a; apply synth.inj at a; contradiction
+      | mpair => contradiction
+  · intro _; aapply synth.inj
+
+-- We do NOT want Crypt... messages broken up in protocols!!
+-- TODO rewrite this
+attribute [-simp] parts.body
+
+-- Rewrites to push in Key and Crypt messages, so that other messages can
+-- be pulled out using the `analz_insert` rules
+
+lemma pushKeysAgent {K : Key} {C : Agent} {H : Set Msg}:
+  insert (Key K) (insert (Agent C) H) = insert (Agent C) (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushKeysNumber {K : Key} {N : Nat} {H : Set Msg}:
+  insert (Key K) (insert (Number N) H) = insert (Number N) (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushKeysNonce {K : Key} {N : Nat} {H : Set Msg}:
+  insert (Key K) (insert (Nonce N) H) = insert (Nonce N) (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushKeysHash {K : Key} {X : Msg} {H : Set Msg}:
+  insert (Key K) (insert (Hash X) H) = insert (Hash X) (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushKeysMPair {K : Key} {X Y : Msg} {H : Set Msg}:
+  insert (Key K) (insert ⦃X, Y⦄ H) = insert ⦃X, Y⦄ (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushKeysCrypt {K K' : Key} {X : Msg} {H : Set Msg}:
+  insert (Key K) (insert (Crypt K' N) H) = insert (Crypt K' N) (insert (Key K) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushCryptsAgent {X : Msg} {K : Key} {C : Agent} {H : Set Msg} :
+  insert (Crypt K X) (insert (Agent C) H) = insert (Agent C) (insert (Crypt K X) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushCryptsNonce {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
+  insert (Crypt K X) (insert (Nonce N) H) = insert (Nonce N) (insert (Crypt K X) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushCryptsNumber {X : Msg} {K : Key} {N : Nat} {H : Set Msg} :
+  insert (Crypt K X) (insert (Number N) H) = insert (Number N) (insert (Crypt K X) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushCryptsHash {X X' : Msg} {K : Key} {H : Set Msg} :
+  insert (Crypt K X) (insert (Hash X') H) = insert (Hash X') (insert (Crypt K X) H) :=
+  by simp [Set.insert_comm]
+
+lemma pushCryptsMPair {X X' Y : Msg} {K : Key} {H : Set Msg} :
+  insert (Crypt K X) (insert ⦃X', Y⦄ H) = insert ⦃X', Y⦄ (insert (Crypt K X) H) :=
+  by simp [Set.insert_comm]
+
+-- The set of key-free messages
+
+inductive keyfree : Set Msg
+  | agent {A : Agent} : keyfree (Agent A)
+  | number {N : Nat} : keyfree (Number N)
+  | nonce {N : Nat} : keyfree (Nonce N)
+  | hash {X : Msg} : keyfree (Hash X)
+  | mpair {X Y : Msg} : keyfree X → keyfree Y → keyfree ⦃X, Y⦄
+  | crypt {K : Key} {X : Msg} : keyfree X → keyfree (Crypt K X)
+
+-- Inductive cases
+lemma keyfree_KeyE {K : Key} : ¬keyfree (Key K) :=
+  by intro h; cases h
+
+lemma keyfree_MPairEL {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree X :=
+  by intro h; cases h; assumption
+
+lemma keyfree_MPairER {X Y : Msg} : keyfree ⦃X, Y⦄ → keyfree Y :=
+  by intro h; cases h; assumption
+
+lemma keyfree_CryptE {K : Key} {X : Msg} : keyfree (Crypt K X) → keyfree X :=
+  by intro h; cases h; assumption
+
+-- Parts of key-free messages remain key-free
+lemma parts_keyfree : parts keyfree ⊆ keyfree :=
+by
+  intro X h
+  induction h with
+  | inj => assumption
+  | fst => aapply keyfree_MPairEL
+  | snd => aapply keyfree_MPairER
+  | body => aapply keyfree_CryptE
+
+-- The key-free part of a set of messages can be removed from the scope of the `analz` operator
+lemma analz_keyfree_into_Un {G H : Set Msg} {X : Msg} :
+  X ∈ analz (G ∪ H) → G ⊆ keyfree → X ∈ parts G ∪ analz H :=
+by
+  intro hG hKeyFree
+  induction hG with
+  | inj h => cases h with
+    | inl hG => exact Or.inl (parts.inj hG)
+    | inr hH => exact Or.inr (analz.inj hH)
+  | fst _ ih =>
+  cases ih
+  · left; aapply parts.fst
+  · right; aapply analz.fst
+  | snd _ ih => 
+  cases ih
+  · left; aapply parts.snd
+  · right; aapply analz.snd
+  | @decrypt K _ h₁ h₂ ih₁ ih₂ => cases ih₂ with
+    | inl h => apply parts_mono at hKeyFree
+               apply subset_trans (c := keyfree) at hKeyFree
+               have pkf := parts_keyfree
+               apply hKeyFree at pkf
+               apply pkf at h
+               have kf_k := keyfree_KeyE (K := invKey K)
+               contradiction
+    | inr =>
+    cases ih₁
+    · left; aapply parts.body
+    · right; aapply analz.decrypt
+
+-- Crypt and Hash are not in the image of Key
+@[simp]
+lemma Crypt_notin_image_Key {K : Key} {X : Msg} {A : Set Key} : Crypt K X ∉ Key '' A :=
+  by simp
+
+@[simp]
+lemma Hash_notin_image_Key {X : Msg} {A : Set Key} : Hash X ∉ Key '' A :=
+  by simp
+
+-- Monotonicity of `synth` over `analz`
+lemma synth_analz_mono {G H : Set Msg} : G ⊆ H → synth (analz G) ⊆ synth (analz H) :=
+  λ h => synth_mono (analz_mono h)
+
+-- Simplification for Fake cases
+@[simp]
+lemma Fake_analz_eq {H : Set Msg} {X : Msg} :
+  X ∈ synth (analz H) → synth (analz (insert X H)) = synth (analz H) :=
+by
+  intro hX
+  ext
+  constructor
+  · apply synth_subset_iff.mp
+    apply subset_trans (b := synth (analz H) ∪ analz H)
+    · apply Fake_analz_insert (G := H) (H := H) (X := X) at hX
+      rw[Set.union_self] at hX
+      assumption
+    · apply sup_le_iff.mpr; apply And.intro
+      · trivial
+      · exact synth_increasing
+  · apply synth_analz_mono; simp
+
+-- Generalizations of `analz_insert_eq`
+lemma gen_analz_insert_eq {H G : Set Msg} {X : Msg} :
+  X ∈ analz H → H ⊆ G → analz (insert X G) = analz G :=
+by
+  intro hX hSubset
+  apply Set.ext
+  intro Y
+  constructor
+  · intro h
+    induction h with
+    | inj h => cases h with
+      | inl hX' => apply analz_mono at hSubset; apply hSubset at hX; rw[hX']; assumption
+      | inr hG => aapply analz.inj
+    | fst h ih => exact analz.fst ih
+    | snd h ih => exact analz.snd ih
+    | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂
+  · intro h
+    exact analz_mono (Set.subset_insert _ _) h
+
+lemma synth_analz_insert_eq {H G : Set Msg} {X : Msg} {K : Key} :
+  X ∈ synth (analz H) → H ⊆ G → ((Key K ∈ analz (insert X G)) ↔ (Key K ∈ analz G)) :=
+by
+  intro h₁ h₂
+  constructor
+  · induction h₁ with
+    | inj a => apply gen_analz_insert_eq (G := G) at a; apply a at h₂; simp[h₂]
+    | agent => rw [analz_insert_Agent]; intro h; cases h; contradiction; assumption
+    | number => rw [analz_insert_Number]; intro h; cases h; contradiction; assumption
+    | hash => rw [analz_insert_Hash]; intro h; cases h; contradiction; assumption
+    | @mpair _ Y h₁ _ _ ih₂ => rw [analz_insert_MPair]; intro h; cases h with
+      | inl => contradiction 
+      | inr h => apply Fake_analz_insert (H := insert Y G) at h₁; apply h₁ at h;
+                 cases h with
+        | inl h => cases h; aapply analz_mono
+        | inr h => apply ih₂; have b := h₂; apply subset_trans (c := insert Y G) at b
+                   have c := Set.subset_insert (x := Y) (s := G)
+                   apply b at c
+                   apply sup_le (a := H) (b := insert Y G) (c := insert Y G) at c
+                   have e := le_refl (a := insert Y G)
+                   apply c at e
+                   apply analz_mono at e
+                   aapply e
+    | crypt b a a_ih => intro h; apply a_ih; apply analz_insert_Crypt_subset at h
+                        cases h; contradiction; assumption
+  · apply analz_mono; apply Set.subset_insert
+
+  
+
+-- Fake parts for single messages
+lemma Fake_parts_sing {H : Set Msg} {X : Msg} :
+  X ∈ synth (analz H) → parts {X} ⊆ synth (analz H) ∪ parts H :=
+by
+  intro h
+  rw[Set.singleton_def]
+  apply subset_trans (b := parts (insert X H))
+  · apply parts_mono; simp
+  · aapply Fake_parts_insert