From 7367681bc64c68ed9152d8c4308d8eab212e43a0 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 4 Mar 2026 00:56:37 +0100 Subject: [PATCH] Simplified proofs in NS_Public --- InductiveVerification/Event.lean | 15 + InductiveVerification/Message.lean | 96 +++-- InductiveVerification/NS_Public.lean | 581 ++++++++++----------------- InductiveVerification/Public.lean | 12 + 4 files changed, 313 insertions(+), 391 deletions(-) diff --git a/InductiveVerification/Event.lean b/InductiveVerification/Event.lean index 10b29ca..a9b1408 100644 --- a/InductiveVerification/Event.lean +++ b/InductiveVerification/Event.lean @@ -375,6 +375,21 @@ lemma parts_knows_Spy_subset_used [Bad] : · simp[used, knows]; split_ifs with ABad · simp; apply subset_trans; apply ih; simp · apply subset_trans; apply ih; simp + +lemma parts_knows_Spy_subset_used_neg [Bad] : + M ∉ used evs → M ∉ parts (knows Agent.Spy evs) := by + intro h₁ h₂; apply h₁; aapply parts_knows_Spy_subset_used + +lemma analz_knows_Spy_subset_used [Bad] [InvKey] : + analz (knows Agent.Spy evs) ⊆ used evs +:= by + apply subset_trans ( b := parts (knows Agent.Spy evs) ) + · exact analz_subset_parts + · exact parts_knows_Spy_subset_used + +lemma analz_knows_Spy_subset_used_neg [Bad] [InvKey] : + M ∉ used evs → M ∉ analz (knows Agent.Spy evs) := by + intro h₁ h₂; apply h₁; aapply analz_knows_Spy_subset_used -- Parts of what the Spy knows are a subset of what is used lemma usedI [Bad] : diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index f1bb933..4a429b2 100644 --- a/InductiveVerification/Message.lean +++ b/InductiveVerification/Message.lean @@ -220,7 +220,7 @@ by | 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 := @@ -323,7 +323,6 @@ abbrev partsClosureOperator : ClosureOperator (Set Msg) := 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 @@ -338,12 +337,20 @@ by intro a b; rw[parts_union]; rw[parts_insert] at a; cases a <;> grind[parts_trans] @[simp] -lemma parts_cut_eq : - X ∈ parts H → (parts (insert X H) = parts H) := +lemma parts_cut_eq {h : X ∈ parts H}: + parts (insert X H) = parts H := by - intro h; simp[parts_insert]; rw[parts_idem] + simp[parts_insert]; apply_rules [parts_subset_iff.mp, Set.singleton_subset_iff.mpr] +-- parts_element lemma +lemma parts_element: + X ∈ parts H ↔ parts {X} ⊆ parts H +:= by + constructor + · intro h; apply_rules [ parts_subset_iff.mp, Set.singleton_subset_iff.mpr ] + · intro h; aapply parts_subset_iff.mpr; simp + @[simp] lemma parts_insert_Agent {H : Set Msg} {agt : Agent} : parts (insert (Agent agt) H) = insert (Agent agt) (parts H) := @@ -383,7 +390,7 @@ by lemma parts_singleton_Nonce : parts {Nonce N} = {Nonce N} := by rw[Set.singleton_def, parts_insert_Nonce, parts_empty] - + @[simp] lemma parts_insert_Number {H : Set Msg} {N : Nat} : parts (insert (Number N) H) = insert (Number N) (parts H) := @@ -805,11 +812,11 @@ lemma analz_insert_MPair {H : Set Msg} {X Y : Msg} [InvKey] : | snd => aapply analz.snd | decrypt => aapply analz.decrypt -lemma analz_insert_Decrypt {H : Set Msg} {K : Key} {X : Msg} [InvKey] : - Key (invKey K) ∈ analz H → +@[simp] +lemma analz_insert_Decrypt [InvKey] + { h : 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 @@ -835,11 +842,10 @@ by | decrypt => aapply analz.decrypt @[simp] -lemma analz_Crypt {H : Set Msg} {K : Key} {X : Msg} [InvKey] : - (Key (invKey K) ∉ analz H) → +lemma analz_Crypt [InvKey] + { h : (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 @@ -870,6 +876,19 @@ by cases ih₁ with | inl => simp_all; apply analz.inj; left; trivial | inr => aapply analz.decrypt + +lemma analz_insert_Crypt_element [InvKey] : + M ∈ analz (insert (Crypt K X) H) ↔ + ((Key (invKey K) ∈ analz H ∧ M ∈ insert (Crypt K X) (analz (insert X H))) ∨ + (Key (invKey K) ∉ analz H ∧ M ∈ insert (Crypt K X) (analz H))) +:= by + constructor + · intro h; by_cases invK_in_H : Msg.Key (invKey K) ∈ analz H + · left; rw[←analz_insert_Decrypt]; aapply And.intro; assumption + · right; rw[←analz_Crypt]; aapply And.intro; assumption + · intro h; rcases h with (⟨_, _⟩ | ⟨_, _⟩) + · rw[analz_insert_Decrypt]; assumption; assumption + · rw[analz_Crypt]; assumption; assumption @[simp] lemma analz_image_Key {N : Set Key} [InvKey] : analz (Key '' N) = Key '' N := @@ -1066,17 +1085,25 @@ by intro hY hX; apply synth_trans; apply hY intro a h; cases h; simp_all; aapply synth.inj -@[simp] -lemma Crypt_synth_eq [InvKey] {H : Set Msg} {K : Key} {X : Msg} : - Key K ∉ H → (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) := -by - intro hK +lemma Crypt_synth_EK [InvKey] : + (Crypt K X ∈ synth H) ↔ + (Crypt K X ∈ H ∨ ( Key K ∈ H ∧ X ∈ synth H)) := + by constructor - · intro h - cases h; assumption; contradiction - · intro h - exact synth.inj h + · intro h; cases h <;> tauto + · intro h; cases h + · aapply synth.inj + · apply synth.crypt <;> tauto +@[simp] +lemma Crypt_synth_eq [InvKey] + { hK : Key K ∉ H } : + (Crypt K X ∈ synth H ↔ Crypt K X ∈ H) := +by + constructor + · intro h; simp[Crypt_synth_EK] at h; tauto + · intro h; exact synth.inj h + @[simp] lemma keysFor_synth [InvKey] {H : Set Msg} : keysFor (synth H) = keysFor H ∪ invKey '' {K | Key K ∈ H} := @@ -1102,7 +1129,22 @@ by · exists Number 0; aapply synth.crypt; apply synth.number · assumption - +@[simp] +lemma Nonce_synth [InvKey] : + Nonce NA ∈ synth H ↔ Nonce NA ∈ H +:= by + constructor + · intro h; cases h; assumption + · aapply synth.inj + +@[simp] +lemma Key_synth [InvKey] : + Key K ∈ synth H ↔ Key K ∈ H +:= by + constructor + · intro h; cases h; assumption + · aapply synth.inj + -- Combinations of parts, analz, and synth @[simp] @@ -1246,7 +1288,7 @@ lemma analz_disj_parts [InvKey] {H : Set Msg} {X : Msg} : exact Or.inr h @[simp] -lemma MPair_synth_analz [InvKey] {H : Set Msg} {X Y : Msg} : +lemma MPair_synth_analz [InvKey] : ⦃X, Y⦄ ∈ synth (analz H) ↔ X ∈ synth (analz H) ∧ Y ∈ synth (analz H) := by constructor @@ -1257,10 +1299,12 @@ lemma MPair_synth_analz [InvKey] {H : Set Msg} {X Y : Msg} : · apply And.intro <;> assumption · intro h; exact synth.mpair h.1 h.2 -lemma Crypt_synth_analz [InvKey] {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)) := +@[simp] +lemma Crypt_synth_analz [InvKey] + { h₁ : Key K ∈ analz H } + { 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 diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index 67fb5ae..232ee06 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -1,5 +1,4 @@ import InductiveVerification.Public -set_option diagnostics true -- The Needham-Schroeder Public-Key Protocol namespace NS_Public @@ -47,32 +46,33 @@ theorem possibility_property : all_goals tauto · simp +-- Lemmata for some very specific recurring cases in the following proof +omit [InvKey] [Bad] in +lemma Fake_parts_sing_helper {A B : Set Msg} +{ h : A ⊆ B } : +X ∈ A ∨ h₁ → X ∈ B ∨ h₁ +:= by + intro h; cases h <;> try simp_all + left; aapply h + -- Spy never sees another agent's private key unless it's bad at the start -set_option trace.aesop true @[simp] theorem Spy_see_priEK {h : ns_public evs} : (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by constructor - -- · induction h <;> aesop (add norm spies, norm knows, norm initState, norm pubEK, norm priEK, norm pubSK, norm priSK, norm injective_publicKey) · induction h with - | Nil => simp[spies, knows, initState]; intro h; cases h with - | inl h => cases h with - | inl => aesop (add norm pubEK, norm pubSK, safe forward injective_publicKey) - | inr h => simp[pubEK, priEK] at h; cases h with - | intro _ h => apply publicKey_neq_privateKey at h; contradiction - | inr h => simp[pubSK, priEK] at h; cases h with - | intro _ h => apply publicKey_neq_privateKey at h; contradiction - | Fake _ h ih => apply Fake_parts_sing at h - simp[spies, knows] - intro h₁; apply ih; - cases h₁ with - | inl h₁ => apply h at h₁; cases h₁ with - | inl h₁ => cases h₁; aapply analz_subset_parts - | inr => assumption - | inr => assumption - | NS1 _ _ ih => aesop (add norm spies, norm knows) - | NS2 _ _ _ ih => aesop (add norm spies, norm knows) - | NS3 _ _ _ ih => rw[spies, knows]; simp; intro _; apply ih; grind + | Nil => + simp[spies, knows, initState, pubEK, priEK, pubSK]; intro h + rcases h with (((⟨B, bad, h⟩ | ⟨B, bad, h⟩) | ⟨B, h⟩) | ⟨B, h⟩) <;> + try (apply injective_publicKey at h; simp_all) + all_goals (apply publicKey_neq_privateKey at h; contradiction) + | Fake _ h ih => + apply Fake_parts_sing at h + intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁ + simp at h₁; aapply ih; + | NS1 _ _ ih => simp; assumption + | NS2 _ _ _ ih => simp; assumption + | NS3 _ _ _ ih => simp; assumption · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey @[simp] @@ -82,33 +82,8 @@ theorem Spy_analz_priEK {h : ns_public evs} : · intro h₁; apply analz_subset_parts at h₁; aapply Spy_see_priEK.mp · intro h₁; apply analz_increasing; aapply Spy_spies_bad_privateKey --- Lammata for some very specific recurring cases in the following proof -lemma no_nonce_NS1_NS2_helper1 -{h : synth (analz (spies evsf)) ⦃Nonce NA, Msg.Agent A⦄} -: Nonce NA ∈ analz (knows Agent.Spy evsf) := by - cases h with - | inj => aapply analz.fst - | mpair n => cases n; assumption - -lemma no_nonce_NS1_NS2_helper2 -{ih : Crypt (pubEK C) ⦃NA', ⦃Nonce NA, Msg.Agent D⦄⦄ ∈ parts (spies evsf) - → Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf) - → Nonce NA ∈ analz (spies evsf)} -{h : parts {X} ⊆ synth (analz (spies evsf)) ∪ parts (spies evsf)} -{h₁ : Crypt (pubEK C) ⦃NA', ⦃Nonce NA, Msg.Agent D⦄⦄ ∈ parts (knows Agent.Spy evsf)} -{h₂ : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts {X} ∨ - Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (knows Agent.Spy evsf)} -: Nonce NA ∈ analz (knows Agent.Spy evsf) := by - apply ih at h₁; cases h₂ with - | inl h₂ => apply h at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj => apply h₁; aapply analz_subset_parts - | crypt h₂ => aapply no_nonce_NS1_NS2_helper1 - | inr => aapply h₁ - | inr => aapply h₁ - -- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret -theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } {A B C D : Agent} : +theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : (Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs) → (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → Nonce NA ∈ analz (spies evs))) := by @@ -116,65 +91,40 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } {A B C D : Ag induction h with | Nil => rw[spies, knows] at h₂; simp[initState] at h₂ | Fake _ h ih => + simp; apply analz_insert; right apply Fake_parts_sing at h - simp[spies, knows] at h₁ - apply analz_insert; right; - cases h₁ with - | inl h₁ => simp_all; apply h at h₁; cases h₁ with - | inl h₁ => cases h₁ with - | inj h₁ => apply analz_subset_parts at h₁ - aapply no_nonce_NS1_NS2_helper2 - | crypt h₁ => cases h₁ with - | inj => apply analz.fst; aapply analz.snd - | mpair _ h₁ => aapply no_nonce_NS1_NS2_helper1 - | inr h₁ => aapply no_nonce_NS1_NS2_helper2 - | inr h₁ => simp[spies, knows] at h₂; aapply no_nonce_NS1_NS2_helper2 - | NS1 => - simp[spies] at h₁; simp[spies] at h₂; cases h₂ with - | inl h => rcases h with ⟨_ , ⟨n , _⟩⟩; - apply parts.body at h₁; apply parts.snd at h₁; apply parts.fst at h₁ - apply parts_knows_Spy_subset_used at h₁; rw[n] at h₁; contradiction - | inr => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all - | NS2 => - simp[spies] at h₁; simp[spies] at h₂; cases h₁ with - | inl h => rcases h with ⟨_, ⟨_, ⟨n, _⟩⟩⟩ - apply parts.body at h₂; apply parts.fst at h₂ - apply parts_knows_Spy_subset_used at h₂; rw[n] at h₂; contradiction - | inr => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all - | NS3 => rw[spies, knows]; apply analz_mono; apply Set.subset_insert; simp_all - -lemma unique_Nonce_apply_ih {P : Prop} -{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy C X :: evsf))} -{h₁ : M₁ ∈ parts (spies evsf)} -{h₂ : M₂ ∈ parts (spies evsf)} -{a_ih : M₁ ∈ parts (spies evsf) - → M₂ ∈ parts (spies evsf) - → Nonce NA ∉ analz (spies evsf) → P} -: P := by - simp[spies, knows] at h₃; apply Set.notMem_subset at h₃ - · aapply a_ih; - · apply analz_mono; apply Set.subset_insert - -lemma unique_NA_apply_ih {P : Prop} -{a_ih : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf) - → Crypt (pubEK B') ⦃Nonce NA, Msg.Agent A'⦄ ∈ parts (spies evsf) - → Nonce NA ∉ analz (spies evsf) → P} -{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy C X :: evsf))} -{h₁ : Crypt (pubEK B) ⦃Nonce NA, Msg.Agent A⦄ ∈ parts (spies evsf)} -{h₂ : Crypt (pubEK B') ⦃Nonce NA, Msg.Agent A'⦄ ∈ parts (spies evsf)} -: P := by - aapply unique_Nonce_apply_ih (h₁ := h₁) (h₂ := h₂) - -lemma unique_NA_contradict -{h₃ : Nonce NA ∉ analz (spies (Says Agent.Spy B X :: evsf))} -{h₂ : synth (analz (spies evsf)) ⦃Nonce NA, Msg.Agent A'⦄} -{P : Prop} -: P := by - apply MPair_synth_analz.mp at h₂; rcases h₂ with ⟨⟨n⟩, m⟩; - simp[spies, knows] at h₃; apply Set.notMem_subset at h₃ - · contradiction; - · apply analz_mono; apply Set.subset_insert + simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁; simp at h₁ + simp at h₂; apply Fake_parts_sing_helper (h := h) at h₂; simp at h₂ + rcases h₁ with ((_ | _) | _) <;> + rcases h₂ with ((_ | _) | _) <;> + try simp_all + all_goals (aapply ih <;> aapply analz_subset_parts) + | NS1 _ nonce_not_used => + apply parts_knows_Spy_subset_used_neg at nonce_not_used; + simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁; + simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂; + apply analz_mono; apply Set.subset_insert + cases h₂ <;> simp_all + | NS2 _ nonce_not_used => + apply parts_knows_Spy_subset_used_neg at nonce_not_used; + simp[spies] at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁; + simp[spies] at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂; + apply analz_mono; apply Set.subset_insert + cases h₁ <;> simp_all + | NS3 _ _ _ a_ih => simp at h₁; simp at h₂; apply analz_mono + apply Set.subset_insert; aapply a_ih +@[simp] +lemma injective_pubEK_helper: + ( pubEK A = pubEK B ∧ h) ↔ ( A = B ∧ h ) +:= by + constructor + · intro h₁ + rcases h₁ with ⟨e, _⟩ + apply injective_publicKey at e + aapply And.intro; simp_all + · intro h₁; simp_all + -- Unicity for NS1: nonce NA identifies agents A and B theorem unique_NA { h : ns_public evs } : (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → @@ -185,57 +135,33 @@ theorem unique_NA { h : ns_public evs } : | Nil => aesop (add norm spies, norm knows, safe analz_insertI) | Fake _ a a_ih => apply Fake_parts_sing at a; intro h₁ h₂ h₃; - simp[spies, knows] at h₁; cases h₁ with - | inl h₁ => apply a at h₁; cases h₁ with - | inl h₁ => cases h₁ with - | inj h₁ => simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₁ - apply analz_subset_parts at h₂ - aapply unique_NA_apply_ih - | crypt h₂ => aapply unique_NA_contradict - | inr h₂ => apply analz_subset_parts at h₁ - aapply unique_NA_apply_ih - | inr h₂ => apply analz_subset_parts at h₁ - aapply unique_NA_apply_ih - | crypt h₁ => aapply unique_NA_contradict - | inr h₁ => simp[spies] at h₁; simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₂ - aapply unique_NA_apply_ih - | crypt => aapply unique_NA_contradict - | inr => aapply unique_NA_apply_ih - | inr => aapply unique_NA_apply_ih - | inr => simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₂ - aapply unique_NA_apply_ih - | crypt => aapply unique_NA_contradict - | inr => aapply unique_NA_apply_ih - | inr => aapply unique_NA_apply_ih - | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; cases h₁ with - | inl h₁ => simp at h₂; cases h₂ with - | inl h₂ => rcases h₁ with ⟨h₁, _⟩; rcases h₂ with ⟨h₂, _⟩; - apply injective_publicKey at h₁; - apply injective_publicKey at h₂; - simp_all; - | inr h₂ => apply parts.body at h₂; apply parts.fst at h₂; - apply parts_knows_Spy_subset_used at h₂; simp_all; - | inr h₁ => simp at h₂; cases h₂ with - | inl h₂ => apply parts.body at h₁; apply parts.fst at h₁; - apply parts_knows_Spy_subset_used at h₁; simp_all; - | inr => aapply unique_NA_apply_ih; - | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih - apply Set.notMem_subset at h₃ - · apply h₃; - · apply_rules [analz_mono, Set.subset_insert] - | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; - apply Set.notMem_subset at h₃ - · apply h₃; - · apply_rules [analz_mono, Set.subset_insert] + simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁ + simp at h₁ + simp[spies, knows] at h₂; apply Fake_parts_sing_helper (h := a) at h₂ + simp at h₂ + simp[spies, knows] at h₃; + rcases h₁ with ((_ | _) | _) <;> + rcases h₂ with ((_ | _) | _) <;> + try ( + apply False.elim; apply h₃; apply analz_mono; aapply Set.subset_insert + tauto + ) + all_goals (aapply a_ih <;> try aapply analz_subset_parts + all_goals ( + intro _; apply h₃; aapply analz_mono; aapply Set.subset_insert + )) + | NS1 _ nonce_not_used a_ih => + intro h₁ h₂ h₃ + simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁ + simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂ + apply parts_knows_Spy_subset_used_neg at nonce_not_used + cases h₁ <;> cases h₂ <;> simp_all + aapply a_ih; intro h; apply h₃; apply_rules[analz_mono, Set.subset_insert] + | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; intro h; apply h₃ + apply_rules [analz_mono, Set.subset_insert] + | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih + intro h; apply h₃ + apply_rules [analz_mono, Set.subset_insert] -- Spy does not see the nonce sent in NS1 if A and B are secure theorem Spy_not_see_NA { h : ns_public evs } @@ -247,27 +173,18 @@ theorem Spy_not_see_NA { h : ns_public evs } induction h with | Nil => simp_all | Fake _ a a_ih => - apply Fake_analz_insert at a; apply a at h₄; simp_all; cases h₁ with - | inl h => rcases h with ⟨l, _⟩; simp_all [Spy_in_bad]; - | inr h => cases h₄ with - | inl h₄ => cases h₄; apply a_ih at h; contradiction; - | inr => apply a_ih at h; contradiction; + have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all | NS1 _ a a_ih => simp_all; cases h₁ with - | inl h => rcases h with ⟨_, ⟨_, ⟨_, ⟨h, _⟩⟩⟩⟩; simp_all; apply a - apply parts_knows_Spy_subset_used - aapply analz_subset_parts - | inr h => apply analz_insert_Crypt_subset at h₄; cases h₄ with - | inl h₄ => contradiction; - | inr h₄ => simp at h₄; cases h₄ - · simp_all; apply a; apply Says_imp_used at h; - apply used_parts_subset_parts at h; simp at h; apply h; - tauto; - · simp_all; - | NS2 _ not_used_NB a a_ih => + | inl => simp_all; apply a; aapply analz_knows_Spy_subset_used + | inr h => apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄ + · simp_all; apply Says_imp_used at h + apply used_parts_subset_parts at h; apply a; apply h; simp + · aapply a_ih + | NS2 _ not_used_NB a a_ih => cases h₁ with | tail _ b => have _ := h₄ simp at h₄; apply analz_insert_Crypt_subset at h₄ - simp at h₄; rcases h₄ with ( h | ( h | h )) + simp at h₄; rcases h₄ with ( h | h | h) · simp at a_ih; have c := b; apply a_ih at c; rw[h] at b; have _ := c; rw[h] at c; apply Says_imp_parts_knows_Spy at b @@ -282,8 +199,8 @@ theorem Spy_not_see_NA { h : ns_public evs } cases h₁ with | tail _ b => have _ := h₄ simp at h₄; apply analz_insert_Crypt_subset at h₄ - simp at h₄; rcases h₄ with ( h | ( h | h )) - · have c := b; have d := a₁; have e := a₂ + simp at h₄; rcases h₄ with ( h | h | h) + · have _ := b; have _ := a₁; have _ := a₂ rw[h] at b; apply Says_imp_parts_knows_Spy at b apply Says_imp_parts_knows_Spy at a₂ aapply a_ih; apply no_nonce_NS1_NS2 @@ -304,42 +221,38 @@ theorem A_trusts_NS2 {h : ns_public evs } Says B A (Crypt (pubEK B) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs := by intro h₁ h₂; - -- have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption apply Says_imp_parts_knows_Spy at h₂ -- use unique_NA to show that B' = B induction h with | Nil => simp_all | Fake _ a a_ih => have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption + simp at h₁; simp at h₂; cases h₁ - · have _ := Spy_in_bad; contradiction - · right; simp at h₂; cases h₂ with - | inl h₂ => apply Fake_parts_sing at a; apply a at h₂; cases h₂ with - | inl h₂ => aapply a_ih; cases h₂ with - | inj => aapply analz_subset_parts - | crypt h => apply False.elim; apply snsNA - apply MPair_synth_analz.mp at h; rcases h with ⟨⟨l⟩ , _⟩; - aapply analz_spies_mono - | inr h₂ => aapply a_ih; - | inr => aapply a_ih; + · have _ := Spy_in_bad; simp_all + · right; apply Fake_parts_sing at a; + apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ + rcases h₂ with ((_ | _) | _) <;> aapply a_ih + · aapply analz_subset_parts + · apply False.elim; apply snsNA; apply analz_spies_mono; tauto; · aapply ns_public.Fake | NS1 _ a a_ih => right; simp at h₂; cases h₁ · apply False.elim; apply a apply parts_knows_Spy_subset_used; apply parts.fst aapply parts.body · aapply a_ih; - | NS2 _ _ a a_ih => simp at h₁; have b := h₁; have snsNA := h₁ - apply Spy_not_see_NA at snsNA <;> try assumption - simp at h₂; cases h₂ with - | inl h => apply Says_imp_parts_knows_Spy at a - apply Says_imp_parts_knows_Spy at b - rcases h with ⟨e₁ , ⟨e₂ , ⟨e₃, e₄⟩⟩⟩ - apply unique_NA at a - rw[e₂] at b; rw[e₂] at snsNA - apply a at b - apply b at snsNA - simp_all[-e₄]; assumption - | inr => right; aapply a_ih + | NS2 _ _ a a_ih => + simp at h₁; have b := h₁; have snsNA := h₁ + apply Spy_not_see_NA at snsNA <;> try assumption + simp at h₂; rcases h₂ with (⟨_ , e₂ , _, e₄⟩ | _) + · apply Says_imp_parts_knows_Spy at a + apply Says_imp_parts_knows_Spy at b + apply unique_NA at a + rw[e₂] at b; rw[e₂] at snsNA + apply a at b + apply b at snsNA + simp_all[-e₄]; assumption + · right; aapply a_ih | NS3 _ _ a a_ih => simp at h₁; simp at h₂; right; aapply a_ih -- If the encrypted message appears then it originated with Alice in `NS1` @@ -351,47 +264,21 @@ lemma B_trusts_NS1 { h : ns_public evs} : intro h₁ h₂ induction h with | Nil => simp[spies] at h₁; rw[knows] at h₁; simp[initState] at h₁ - | Fake _ a a_ih => simp at h₁; cases h₁ with - | inl h₁ => apply Fake_parts_sing at a; apply a at h₁; cases h₁ with - | inl h₁ => cases h₁ with - | inj h₁ => right; apply analz_subset_parts at h₁; aapply a_ih - aapply analz_spies_mono_neg - | crypt h₁ => apply False.elim; - apply MPair_synth_analz.mp at h₁ - rcases h₁ with ⟨⟨h₁⟩, _⟩; aapply analz_spies_mono_neg - | inr => right; aapply a_ih; aapply analz_spies_mono_neg - | inr h₁ => right; aapply a_ih; aapply analz_spies_mono_neg - | NS1 _ _ a_ih => simp at h₁; cases h₁ with - | inl h₁ => rcases h₁ with ⟨e₁, ⟨e₂, e₃⟩⟩; apply injective_publicKey at e₁ - simp_all - | inr => right; aapply a_ih; aapply analz_spies_mono_neg + | Fake _ a a_ih => + simp at h₁; apply Fake_parts_sing at a; + apply Fake_parts_sing_helper (h := a) at h₁; simp at h₁ + rcases h₁ with ((h₁ | h₁ )| h₁); + · right; aapply a_ih; aapply analz_subset_parts; aapply analz_spies_mono_neg + · apply False.elim; apply h₂; apply analz_spies_mono; simp_all + · right; aapply a_ih; aapply analz_spies_mono_neg + | NS1 _ _ a_ih => simp at h₁; cases h₁ + · simp_all + · right; aapply a_ih; aapply analz_spies_mono_neg | NS2 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg | NS3 _ _ _ a_ih => simp at h₁; right; aapply a_ih; aapply analz_spies_mono_neg -- Authenticity Properties obtained from `NS2` --- Helper lemmas for unique_NB -lemma unique_NB_apply_ih {P : Prop} -{ a_ih : - Crypt (pubEK A) ⦃Nonce NA, ⦃Nonce NB, Msg.Agent B⦄⦄ ∈ parts (spies evsf) → - Crypt (pubEK A') ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ ∈ parts (spies evsf) → - Nonce NB ∉ analz (spies evsf) → P } -{ h₁ : Crypt (pubEK A) ⦃Nonce NA, ⦃Nonce NB, Msg.Agent B⦄⦄ ∈ parts (spies evsf) } -{ h₂ : Crypt (pubEK A') ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ ∈ parts (spies evsf) } -{ h₃ : Nonce NB ∉ analz (spies (Says Agent.Spy B X :: evsf)) } -: P := by - aapply unique_Nonce_apply_ih (h₁ := h₁) (h₂ := h₂) (h₃ := h₃) - -lemma unique_NB_contradict -{ h₃ : Nonce NB ∉ analz (spies (Says Agent.Spy B X :: evsf)) } -{ h₂ : synth (analz (spies evsf)) ⦃Nonce NA', ⦃Nonce NB, Msg.Agent B'⦄⦄ } -{P : Prop} -: P := by - apply MPair_synth_analz.mp at h₂; apply False.elim - rcases h₂ with ⟨_, r⟩; cases r with - | inj r => aapply analz_spies_mono_neg; aapply analz.fst - | mpair r₁ _ => cases r₁; aapply analz_spies_mono_neg - -- Unicity for `NS2`: nonce `NB` identifies nonce `NA` and agent `A` theorem unique_NB { h : ns_public evs } : (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄ ∈ parts (spies evs) → @@ -402,57 +289,31 @@ theorem unique_NB { h : ns_public evs } : induction h with | Nil => aesop (add norm spies, norm knows, safe analz_insertI) | Fake _ a a_ih => - apply Fake_parts_sing at a; intro h₁ h₂ h₃; - simp[spies, knows] at h₁; cases h₁ with - | inl h₁ => apply a at h₁; cases h₁ with - | inl h₁ => cases h₁ with - | inj h₁ => simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₁ - apply analz_subset_parts at h₂ - aapply unique_NB_apply_ih - | crypt h₂ => aapply unique_NB_contradict - | inr h₂ => apply analz_subset_parts at h₁ - aapply unique_NB_apply_ih - | inr h₂ => apply analz_subset_parts at h₁ - aapply unique_NB_apply_ih - | crypt h₁ => aapply unique_NB_contradict - | inr h₁ => simp[spies] at h₁; simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₂ - aapply unique_NB_apply_ih - | crypt => aapply unique_NB_contradict - | inr => aapply unique_NB_apply_ih - | inr => aapply unique_NB_apply_ih - | inr => simp[spies, knows] at h₂; cases h₂ with - | inl h₂ => apply a at h₂; cases h₂ with - | inl h₂ => cases h₂ with - | inj h₂ => apply analz_subset_parts at h₂ - aapply unique_NB_apply_ih - | crypt => aapply unique_NB_contradict - | inr => aapply unique_NB_apply_ih - | inr => aapply unique_NB_apply_ih + intro h₁ h₂ h₃; + apply Fake_parts_sing at a + simp[spies, knows] at h₁; apply Fake_parts_sing_helper (h := a) at h₁ + simp at h₁; + simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂; + apply analz_spies_mono_neg at h₃ + rcases h₁ with ((h₁ | h₁) | h₁) <;> + rcases h₂ with ((h₂ | h₂) | h₂) <;> + simp_all + all_goals (aapply a_ih; repeat aapply analz_subset_parts) | NS1 _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; aapply a_ih aapply analz_spies_mono_neg - | NS2 _ _ _ a_ih => intro h₁ h₂ h₃; simp at h₁; simp at h₂; cases h₁ with - | inl h₁ => rcases h₁ with ⟨e₁, _⟩; apply injective_publicKey at e₁ - cases h₂ with - | inl h₂ => rcases h₂ with ⟨e₂, _⟩; apply injective_publicKey at e₂ - simp_all - | inr h₂ => apply parts.body at h₂; apply parts.snd at h₂ - apply parts.fst at h₂; apply parts_knows_Spy_subset_used at h₂; - simp_all; - | inr h₁ => cases h₂ with - | inl h₂ => apply parts.body at h₁; apply parts.snd at h₁ - apply parts.fst at h₁; apply parts_knows_Spy_subset_used at h₁; - simp_all - | inr => aapply a_ih; aapply analz_spies_mono_neg - | NS3 _ _ _ a_ih => intro h₁ h₂ h₃; simp_all; apply a_ih; - apply Set.notMem_subset at h₃ - · apply h₃; - · apply_rules [analz_mono, Set.subset_insert] + | NS2 _ nonce_not_used _ a_ih => + intro h₁ h₂ h₃; + -- This is how to rewrite `M ∈ parts` terms into something useful + -- TODO create a macro for this + -- TODO this should work with analz as well + simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁ + simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂ + apply analz_spies_mono_neg at h₃; + apply parts_knows_Spy_subset_used_neg at nonce_not_used + rcases h₁ with (_ | h₁) <;> + rcases h₂ with (_ | h₂) <;> simp_all + | NS3 _ _ _ a_ih => + intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all; -- `NB` remains secret theorem Spy_not_see_NB { h : ns_public evs } @@ -464,46 +325,34 @@ theorem Spy_not_see_NB { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | Fake _ a a_ih => - apply Fake_analz_insert at a; apply a at h₄; simp_all; cases h₁ with - | inl h => rcases h with ⟨l, _⟩; simp_all [Spy_in_bad]; - | inr h => cases h₄ with - | inl h₄ => cases h₄; apply a_ih at h; contradiction; - | inr => apply a_ih at h; contradiction; - | NS1 _ a a_ih => simp at h₁; simp[spies, knows] at h₄ - apply analz_insert_Crypt_subset at h₄; simp at h₄ - cases h₄ with - | inl e => rw[e] at h₁; apply a; apply parts_knows_Spy_subset_used - apply parts.fst; apply parts.snd; apply parts.body - aapply Says_imp_parts_knows_Spy + | Fake _ a a_ih => + have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all; + | NS1 _ nonce_not_used a_ih => + simp at h₁ + simp[spies, knows] at h₄; apply analz_insert_Crypt_subset at h₄; simp at h₄ + apply parts_knows_Spy_subset_used_neg at nonce_not_used + cases h₄ with + | inl e => apply Says_imp_parts_knows_Spy at h₁; + rw[parts_element, Set.subset_def] at h₁; simp_all | inr => aapply a_ih - | NS2 _ not_used_NB a a_ih => simp at h₁; simp[spies, knows] at h₄; - cases h₁ with - | inl h => rcases h with ⟨_, ⟨_, ⟨e₃, _⟩⟩⟩; apply injective_publicKey at e₃; - simp_all; apply not_used_NB; apply parts_knows_Spy_subset_used; - aapply analz_subset_parts - | inr h => apply analz_insert_Crypt_subset at h₄; simp at h₄; cases h₄ with - | inl e => aapply a_ih; rw[e]; apply Says_imp_parts_knows_Spy at a - apply Says_imp_parts_knows_Spy at h; rw[e] at h - aapply no_nonce_NS1_NS2 - | inr h => cases h - · simp_all; apply not_used_NB; apply parts_knows_Spy_subset_used - apply parts.fst; apply parts.snd; apply parts.body - aapply Says_imp_parts_knows_Spy - · aapply a_ih - | @NS3 evs3 _ B' _ _ _ _ a₁ a₂ a_ih => - cases h₁ with | tail _ b => - simp at h₄; by_cases bad_B' : Key (invKey (pubEK B')) ∈ analz (spies evs3) - · have aC := bad_B'; apply analz_subset_parts at bad_B' - apply Spy_see_priEK.mp at bad_B'; have c := b; apply a_ih at c; - apply analz_insert_Decrypt at aC; rw[aC] at h₄; simp at h₄; cases h₄ with - | inl h₄ => - apply Says_imp_parts_knows_Spy at a₂ - apply Says_imp_parts_knows_Spy at b; rw[h₄] at b - apply unique_NB at a₂; apply a₂ at b; - rw[h₄] at c; simp_all; assumption - | inr h₄ => aapply a_ih - · apply analz_Crypt at aC; rw[aC] at h₄; simp at h₄; aapply a_ih; + | NS2 _ not_used_NB a a_ih => + simp at h₁; + simp[spies, knows] at h₄; + apply parts_knows_Spy_subset_used_neg at not_used_NB + rcases h₁ with (_ | h₁) + · simp_all; apply not_used_NB; aapply analz_subset_parts + · apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (_ |_ |_ ) + · aapply a_ih; apply Says_imp_parts_knows_Spy at a; + apply Says_imp_parts_knows_Spy at h₁; simp_all; aapply no_nonce_NS1_NS2 + · apply Says_imp_parts_knows_Spy at h₁; + rw[parts_element, Set.subset_def] at h₁; simp_all + · aapply a_ih + | NS3 _ _ a a_ih => + simp at h₁; simp[analz_insert_Crypt_element] at h₄; + rcases h₄ with (⟨_, _⟩ | ⟨_, _⟩) <;> simp_all + apply Says_imp_parts_knows_Spy at a + apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at a + apply a at h₁; apply h₁ at a_ih; simp_all; assumption -- Authentication for `B`: if he receives message 3 and has used `NB` in message 2, then `A` has sent message 3. theorem B_trusts_NS3 { h : ns_public evs } @@ -517,31 +366,32 @@ theorem B_trusts_NS3 { h : ns_public evs } apply Says_imp_parts_knows_Spy at h₂ induction h with | Nil => simp_all - | Fake _ a a_ih => right; simp at h₁; simp at h₂; cases h₁ with - | inl => simp_all[Spy_in_bad] - | inr h₁ => cases h₂ with - | inl h₂ => apply Fake_parts_sing at a; apply a at h₂; cases h₂ with - | inl h₂ => simp at h₂; cases h₂ with - | inj => aapply a_ih; aapply analz_subset_parts; - | crypt h₂ => cases h₂; apply Spy_not_see_NB at h₁ <;> simp_all - | inr => aapply a_ih - | inr => aapply a_ih + | Fake _ a a_ih => + right; simp at h₁ + apply Fake_parts_sing at a + simp at h₂; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ + rw[parts_element, Set.subset_def] at h₂; simp at h₂ + have _ := Spy_in_bad + rcases h₁ with (h₁ | h₁) <;> rcases h₂ with ((h₂ | h₂) | h₂) <;> simp_all + · aapply a_ih; aapply analz_subset_parts + · apply Spy_not_see_NB at h₁ <;> simp_all + · aapply a_ih | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih; - | NS2 _ _ a a_ih => right; simp at h₁; simp at h₂; cases h₁ with - | inl => apply parts.body at h₂; apply parts_knows_Spy_subset_used at h₂ - simp_all - | inr => aapply a_ih - | NS3 _ a₁ a₂ a_ih => simp at h₁; simp at h₂; cases h₂ with - | inl h₂ => simp_all; left; rcases h₂ with ⟨e₁, _⟩ - apply injective_publicKey at e₁; simp_all - have h₁c := h₁ - apply Says_imp_parts_knows_Spy at h₁ - apply Says_imp_parts_knows_Spy at a₂ - apply unique_NB at h₁; apply h₁ at a₂ - apply Spy_not_see_NB at h₁c - apply a₂ at h₁c - all_goals simp_all - | inr => right; aapply a_ih + | NS2 _ nonce_not_used a a_ih => + right + apply parts_knows_Spy_subset_used_neg at nonce_not_used; + simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂ + simp at h₁; cases h₁ <;> simp_all; aapply a_ih + | NS3 _ _ a₂ a_ih => + simp at h₁ + simp at h₂; rw[parts_element, Set.subset_def] at h₂; simp at h₂ + cases h₂ <;> simp_all + have h₁c := h₁ + apply Spy_not_see_NB at h₁c + apply Says_imp_parts_knows_Spy at h₁ + apply Says_imp_parts_knows_Spy at a₂ + apply unique_NB at h₁; apply h₁ at a₂ + apply a₂ at h₁c; all_goals simp_all -- Overall guarantee for `B` @@ -555,30 +405,31 @@ theorem B_trusts_protocol { h : ns_public evs } intro h₁ h₂ induction h with | Nil => simp_all - | Fake _ a a_ih => right; simp at h₁; simp at h₂; cases h₂ with - | inl => simp_all[Spy_in_bad] - | inr h₂ => cases h₁ with - | inl h₁ => apply Fake_parts_sing at a; apply a at h₁; cases h₁ with - | inl h₁ => simp at h₁; cases h₁ with - | inj => aapply a_ih; aapply analz_subset_parts - | crypt h₁ => cases h₁; apply Spy_not_see_NB at h₂ <;> simp_all - | inr => aapply a_ih - | inr => aapply a_ih + | Fake _ a a_ih => + right + apply Fake_parts_sing at a + simp at h₁; apply Fake_parts_sing_helper (h := a) at h₁; + rw[parts_element, Set.subset_def] at h₁; simp at h₁ + have _ := Spy_in_bad + simp at h₂; rcases h₂ with (_ | h₂) <;> simp_all + rcases h₁ with (((_ |_ ) | _) | _) <;> try (aapply a_ih) + · aapply analz_subset_parts + · apply Spy_not_see_NB at h₂ <;> simp_all + · simp_all | NS1 _ a a_ih => right; simp at h₂; simp at h₁; aapply a_ih; | NS2 _ _ a a_ih => right; simp at h₁; simp at h₂; cases h₂ with | inl => apply parts.body at h₁; apply parts_knows_Spy_subset_used at h₁ simp_all | inr => aapply a_ih - | NS3 _ a₁ a₂ a_ih => simp at h₁; simp at h₂; cases h₁ with - | inl h₁ => simp_all; rcases h₁ with ⟨e₁, _⟩ - apply injective_publicKey at e₁; simp_all - have h₂c := h₂ - apply Says_imp_parts_knows_Spy at h₂ - apply Says_imp_parts_knows_Spy at a₂ - apply unique_NB at h₂; apply h₂ at a₂ - apply Spy_not_see_NB at h₂c - apply a₂ at h₂c - all_goals simp_all - | inr => right; aapply a_ih + | NS3 _ _ a₂ a_ih => + simp at h₂ + simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁ + cases h₁ <;> simp_all + have h₂c := h₂ + apply Spy_not_see_NB at h₂c + apply Says_imp_parts_knows_Spy at h₂ + apply Says_imp_parts_knows_Spy at a₂ + apply unique_NB at h₂; apply h₂ at a₂ + apply a₂ at h₂c; all_goals simp_all end NS_Public diff --git a/InductiveVerification/Public.lean b/InductiveVerification/Public.lean index e0c3443..347ad3d 100644 --- a/InductiveVerification/Public.lean +++ b/InductiveVerification/Public.lean @@ -390,6 +390,18 @@ lemma Crypt_Spy_analz_bad : simp[invKey_shrK] aapply Spy_spies_bad_shrK +@[simp] +lemma Crypt_synth_pubK : + (Msg.Crypt (pubEK A) X ∈ synth (spies evs)) ↔ + (Msg.Crypt (pubEK A) X ∈ (spies evs) ∨ ( X ∈ synth (spies evs))) := +by simp[Crypt_synth_EK]; + +@[simp] +lemma Crypt_synth_analz_pubK : + (Msg.Crypt (pubEK A) X ∈ synth (analz (spies evs))) ↔ + (Msg.Crypt (pubEK A) X ∈ (analz (spies evs)) ∨ ( X ∈ synth (analz (spies evs)))) := +by simp[Crypt_synth_EK]; + @[simp] lemma Nonce_notin_initState {B : Agent} : Msg.Nonce N ∉ parts (initState B) := by cases B <;>