From 80db88efbef67a9a476d74b99119ac5964a94472 Mon Sep 17 00:00:00 2001 From: Your Name Date: Wed, 4 Mar 2026 18:44:21 +0100 Subject: [PATCH] Added expand_parts_element macro Further simplified proofs in NS_public --- InductiveVerification/Message.lean | 33 +++ InductiveVerification/NS_Public.lean | 348 +++++++++++---------------- InductiveVerification/Public.lean | 41 +--- 3 files changed, 185 insertions(+), 237 deletions(-) diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index 4a429b2..04ce031 100644 --- a/InductiveVerification/Message.lean +++ b/InductiveVerification/Message.lean @@ -1,5 +1,6 @@ import Init.Data.Nat.Lemmas import Init.Prelude +import Lean import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Dist import Mathlib.Data.Set.Basic @@ -12,6 +13,8 @@ import Mathlib.Order.Lattice import Mathlib.Tactic.ApplyAt import Mathlib.Tactic.SimpIntro import Mathlib.Tactic.NthRewrite +open Lean Elab Command Term Meta +open Parser.Tactic -- Keys are integers abbrev Key := Nat @@ -351,6 +354,14 @@ lemma parts_element: · intro h; apply_rules [ parts_subset_iff.mp, Set.singleton_subset_iff.mpr ] · intro h; aapply parts_subset_iff.mpr; simp +/-- +A tactic that expands terms like `X ∈ parts H` +-/ +syntax (name := expandPartsElement) "expand_parts_element" (ppSpace location) : tactic +macro_rules + | `(tactic| expand_parts_element at $loc) => + `(tactic| rw[parts_element, Set.subset_def] at $loc; simp at $loc) + @[simp] lemma parts_insert_Agent {H : Set Msg} {agt : Agent} : parts (insert (Agent agt) H) = insert (Agent agt) (parts H) := @@ -593,6 +604,16 @@ by | snd h ih => exact analz.snd ih | decrypt h₁ h₂ ih₁ ih₂ => exact analz.decrypt ih₁ ih₂ +lemma analz_mono_neg [InvKey] { h : A ⊆ B } : + X ∉ analz B → X ∉ analz A +:= by + intro h₁ h₂; apply h₁; aapply analz_mono; + +lemma analz_insert_mono_neg [InvKey] : + X ∉ analz (insert Y H) → X ∉ analz H +:= by + apply_rules [ analz_mono_neg, Set.subset_insert ] + -- Making it safe speeds up proofs -- @[simp] lemma MPair_analz {H : Set Msg} {X Y : Msg} {P : Prop} [InvKey] : @@ -1597,3 +1618,15 @@ by apply subset_trans (b := parts (insert X H)) · apply parts_mono; simp · aapply Fake_parts_insert + +-- Often the result of Fake_parts_sing needs to be applied to a term in a +-- disjunction +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 + +attribute [-simp] Key.injEq + diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index 232ee06..eb3e230 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -42,19 +42,10 @@ theorem possibility_property : · apply ns_public.NS2 · apply_rules [ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty] · simp - · left + · tauto 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 @[simp] theorem Spy_see_priEK {h : ns_public evs} : @@ -62,17 +53,14 @@ theorem Spy_see_priEK {h : ns_public evs} : constructor · induction h with | 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) + simp[spies, knows, initState, pubEK, priEK, pubSK] | 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 + simp_all + | NS1 => simp_all + | NS2 => simp_all + | NS3 => simp_all · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey @[simp] @@ -89,42 +77,30 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : Nonce NA ∈ analz (spies evs))) := by intro h₁ h₂ induction h with - | Nil => rw[spies, knows] at h₂; simp[initState] at h₂ - | Fake _ h ih => - simp; apply analz_insert; right + | Nil => simp[spies, knows] at h₂ + | Fake _ h ih => + simp; apply analz_insert; apply Fake_parts_sing at h 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 ((_ | _) | _) <;> rcases h₂ with ((_ | _) | _) <;> - try simp_all - all_goals (aapply ih <;> aapply analz_subset_parts) + simp_all + all_goals (right; aapply ih <;> aapply analz_subset_parts) | NS1 _ nonce_not_used => + apply analz_spies_mono + simp [*] at * 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 + expand_parts_element at h₁; expand_parts_element at h₂; cases h₂ <;> simp_all | NS2 _ nonce_not_used => + apply analz_spies_mono + simp [*] at * 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 + expand_parts_element at h₂; + cases h₁ <;> simp_all[-Key.injEq] + | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all -@[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) → @@ -132,36 +108,24 @@ theorem unique_NA { h : ns_public evs } : (Nonce NA ∉ analz (spies evs) → A = A' ∧ B = B'))) := by induction h with - | Nil => aesop (add norm spies, norm knows, safe analz_insertI) + | Nil => simp[spies, knows] | Fake _ a a_ih => apply Fake_parts_sing at a; intro h₁ h₂ h₃; - 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 - )) + apply analz_spies_mono_neg at h₃; + simp [*] at * + apply Fake_parts_sing_helper (h := a) at h₁ + apply Fake_parts_sing_helper (h := a) at h₂ + simp_all | 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 analz_insert_mono_neg at h₃ + simp [*] at * + expand_parts_element at h₁ + expand_parts_element 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] + | NS2 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all + | NS3 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all; -- Spy does not see the nonce sent in NS1 if A and B are secure theorem Spy_not_see_NA { h : ns_public evs } @@ -172,46 +136,36 @@ theorem Spy_not_see_NA { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a => 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 => 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 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 - apply Says_imp_parts_knows_Spy at a - apply unique_NA at b; apply b at a; apply a at c; simp_all - assumption - · rw [h] at b - apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst; - apply parts.body; apply Says_imp_parts_knows_Spy; assumption - · aapply a_ih - | NS3 _ a₁ 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) - · 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 - · assumption - · rw[h]; exact a₂ - · rw[h]; exact b - · aapply a_ih; aapply analz.inj - · aapply a_ih; aapply analz.fst - · aapply a_ih; aapply analz.snd - · aapply a_ih; aapply analz.decrypt - + | NS1 _ a a_ih => + simp_all; rcases h₁ with (_ | h) + · simp_all; apply a; aapply analz_knows_Spy_subset_used + · 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 + simp_all[Set.subset_def] + | NS2 _ not_used_NB a a_ih => + simp at h₁ + have _ := h₄ + simp at h₄; apply analz_insert_Crypt_subset at h₄ + simp at h₄; rcases h₄ with ( h | h | h) + · simp [*] at *; have c := h₁; apply a_ih at c; + have _ := c; + apply Says_imp_parts_knows_Spy at h₁ + apply Says_imp_parts_knows_Spy at a + apply unique_NA at h₁; apply h₁ at a; apply a at c; all_goals simp_all + · simp_all + apply not_used_NB; apply parts_knows_Spy_subset_used; apply parts.fst; + apply parts.body; apply Says_imp_parts_knows_Spy; assumption + · aapply a_ih + | NS3 _ _ a₂ a_ih => + simp [*] at * + have _ := h₄ + apply analz_insert_Crypt_subset at h₄; simp[*] at h₄; + have _ := h₁; simp[*] at h₁; apply Says_imp_parts_knows_Spy at h₁ + apply Says_imp_parts_knows_Spy at a₂ + aapply a_ih; apply no_nonce_NS1_NS2 <;> try simp [*] <;> assumption + -- Authentication for `A`: if she receives message 2 and has used `NA` to start a run, then `B` has sent message 2. theorem A_trusts_NS2 {h : ns_public evs } { not_bad_A : A ∉ bad } @@ -225,36 +179,29 @@ theorem A_trusts_NS2 {h : ns_public evs } -- use unique_NA to show that B' = B induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a a_ih => have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption - simp at h₁; simp at h₂; + apply analz_spies_mono_neg at snsNA + simp [*] at * cases h₁ · have _ := Spy_in_bad; simp_all - · right; apply Fake_parts_sing at a; + · apply Fake_parts_sing at a; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ - rcases h₂ with ((_ | _) | _) <;> aapply a_ih + rcases h₂ with ((_ | _) | _) <;> (right; aapply a_ih) · aapply analz_subset_parts - · apply False.elim; apply snsNA; apply analz_spies_mono; tauto; + · 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; + | NS1 _ a a_ih => + apply parts_knows_Spy_subset_used_neg at a; + simp [*] at *; expand_parts_element at h₂; cases h₁ <;> simp_all | 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 - + simp [*] at * + have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption + cases h₂ <;> simp_all + apply Says_imp_parts_knows_Spy at a; apply unique_NA at a; + apply Says_imp_parts_knows_Spy at h₁; apply a at h₁; all_goals simp_all + | NS3 _ _ a a_ih => simp_all; + -- If the encrypted message appears then it originated with Alice in `NS1` lemma B_trusts_NS1 { h : ns_public evs} : Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → @@ -263,20 +210,16 @@ lemma B_trusts_NS1 { h : ns_public evs} : := by intro h₁ h₂ induction h with - | Nil => simp[spies] at h₁; rw[knows] at h₁; simp[initState] at h₁ + | Nil => simp[spies, knows] at h₁ | Fake _ a a_ih => + apply analz_spies_mono_neg at h₂ 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 - + apply Fake_parts_sing_helper (h := a) at h₁; simp_all + | NS1 _ _ a_ih => + apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all + | NS2 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all; + | NS3 _ _ _ a_ih => apply analz_spies_mono_neg at h₂; simp_all; + -- Authenticity Properties obtained from `NS2` -- Unicity for `NS2`: nonce `NB` identifies nonce `NA` and agent `A` @@ -289,33 +232,28 @@ theorem unique_NB { h : ns_public evs } : induction h with | Nil => aesop (add norm spies, norm knows, safe analz_insertI) | Fake _ a a_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₂) <;> + apply Fake_parts_sing at a; intro h₁ h₂ h₃; simp [*] at * + apply Fake_parts_sing_helper (h := a) at h₁; + apply Fake_parts_sing_helper (h := a) at h₂; simp [*] at * + apply analz_insert_mono_neg at h₃ + rcases h₁ with ((_ | _) | _) <;> + rcases h₂ with ((_ | _) | _) <;> 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 _ 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₃; + intro h₁ h₂ h₃; simp [*] at * + expand_parts_element at h₁ + expand_parts_element at h₂ + apply analz_insert_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; + intro h₁ h₂ h₃; apply analz_spies_mono_neg at h₃; simp_all[-Key.injEq] --- `NB` remains secret +-- `NB` remains secret theorem Spy_not_see_NB { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -328,74 +266,68 @@ theorem Spy_not_see_NB { h : ns_public evs } | 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₄ + simp [*] at * + 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 + have h₂ := h₁; apply Says_imp_parts_knows_Spy at h₂ + expand_parts_element at h₂; simp_all | NS2 _ not_used_NB a a_ih => - simp at h₁; - simp[spies, knows] at h₄; + simp [*] at * 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; + · 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 + expand_parts_element at h₁; simp_all · aapply a_ih | NS3 _ _ a a_ih => - simp at h₁; simp[analz_insert_Crypt_element] at h₄; + 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 } +theorem B_trusts_NS3 { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB, Agent B⦄) ∈ evs → Says A' B (Crypt (pubEK B) (Nonce NB)) ∈ evs → Says A B (Crypt (pubEK B) (Nonce NB)) ∈ evs -:= by +:= by intro h₁ h₂ apply Says_imp_parts_knows_Spy at h₂ induction h with | Nil => simp_all | Fake _ a a_ih => - right; simp at h₁ + simp [*] at * 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 Fake_parts_sing_helper (h := a) at h₂; simp at h₂ + expand_parts_element at h₂; + rcases h₁ with (_ | h₁) <;> + rcases h₂ with ((h₂ | _) | _) <;> simp_all[Spy_in_bad] + · apply analz_subset_parts at h₂; simp_all · 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 _ nonce_not_used a a_ih => - right + | NS1 => simp_all + | NS2 _ nonce_not_used => + simp [*] at * 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 + expand_parts_element at h₂; cases h₁ <;> simp_all + | NS3 _ _ a₂ => + simp [*] at *; + expand_parts_element 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 + apply Says_imp_parts_knows_Spy at h₁; apply unique_NB at h₁; + apply Says_imp_parts_knows_Spy at a₂; apply h₁ at a₂ + all_goals simp_all -- Overall guarantee for `B` - --- If NS3 has been sent and the nonce NB agrees with the nonce B joined with NA, then A initiated the run using NA + +-- If NS3 has been sent and the nonce NB agrees with the nonce B joined with NA, +-- then A initiated the run using NA theorem B_trusts_protocol { h : ns_public evs } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -406,24 +338,22 @@ theorem B_trusts_protocol { h : ns_public evs } induction h with | Nil => simp_all | Fake _ a a_ih => - right + simp [*] at * 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 Fake_parts_sing_helper (h := a) at h₁; + expand_parts_element at h₁ + rcases h₂ with (_ | h₂) <;> simp_all[Spy_in_bad] + rcases h₁ with (((_ |_ ) | _) | _) <;> try simp_all + · right; 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 + | NS1 => simp_all + | NS2 _ nonce_not_used a a_ih => + simp [*] at * + apply parts_knows_Spy_subset_used_neg at nonce_not_used; + expand_parts_element at h₁; cases h₂ <;> simp_all | NS3 _ _ a₂ a_ih => - simp at h₂ - simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁ + simp [*] at * + expand_parts_element at h₁ cases h₁ <;> simp_all have h₂c := h₂ apply Spy_not_see_NB at h₂c diff --git a/InductiveVerification/Public.lean b/InductiveVerification/Public.lean index 347ad3d..5e2f4a0 100644 --- a/InductiveVerification/Public.lean +++ b/InductiveVerification/Public.lean @@ -3,7 +3,6 @@ import Init.Data.Nat.Lemmas import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.Dist import Mathlib.Order.Defs.PartialOrder -set_option diagnostics true -- Theory of Public Keys (common to all public-key protocols) @@ -35,15 +34,18 @@ noncomputable abbrev pubK (A : Agent) : Key := pubEK A noncomputable abbrev priK (A : Agent) : Key := invKey (pubEK A) -- Axioms for private and public keys +@[simp] axiom privateKey_neq_publicKey {b c : KeyMode} {A A' : Agent} : privateKey b A ≠ publicKey c A' +@[simp] lemma publicKey_neq_privateKey {b c : KeyMode} {A A' : Agent} : publicKey b A ≠ privateKey c A' := by exact privateKey_neq_publicKey.symm -- Basic properties of pubK and priK omit [InvKey] in +@[simp] lemma publicKey_inject {b c : KeyMode} {A A' : Agent} : (publicKey b A = publicKey c A') ↔ (b = c ∧ A = A') := by grind[injective_publicKey] @@ -59,7 +61,7 @@ by lemma not_symKeys_priK {b : KeyMode} {A : Agent} : privateKey b A ∉ symKeys := by - simp [symKeys, privateKey, invKey_eq]; grind[privateKey_neq_publicKey]; + simp [symKeys, privateKey, invKey_eq, privateKey_neq_publicKey] lemma syKey_neq_priEK : K ∈ symKeys → K ≠ priEK A := by @@ -93,7 +95,7 @@ omit [InvKey] in @[simp] lemma publicKey_image_eq : (publicKey b x ∈ publicKey c '' AA) ↔ (b = c ∧ x ∈ AA) := by - simp [Set.mem_image, publicKey_inject, And.comm, Eq.comm] + simp [Set.mem_image, And.comm, Eq.comm] @[simp] lemma privateKey_notin_image_publicKey : @@ -252,22 +254,16 @@ lemma MPair_used {P : Prop} : lemma keysFor_parts_initState {C : Agent} : keysFor (parts (initState C)) = ∅ := by cases C <;> - simp[initState, keysFor] <;> - repeat rw[Set.singleton_def, parts_insert_Key, parts_empty] <;> - simp + simp[initState, keysFor] lemma Crypt_notin_initState {B : Agent} : Msg.Crypt K X ∉ parts ( initState B ) := by - cases B <;> simp[initState, priEK, priSK, shrK] <;> - apply And.intro <;> try apply And.intro - all_goals repeat rw[Set.singleton_def, parts_insert_Key, parts_empty] <;> - simp + cases B <;> simp[initState, priEK, priSK] @[simp] lemma Crypt_notin_used_empty : Msg.Crypt K X ∉ used [] := by - simp[used]; intro A; cases A <;> simp <;> apply And.intro <;> try apply And.intro - all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty] ; simp) + simp[used]; intro A; cases A <;> simp -- Basic properties of shrK @@ -324,10 +320,7 @@ lemma priK_in_initState {b : KeyMode} {A : Agent} : Msg.Key (privateKey b A) ∈ initState A := by induction A <;> simp [HasInitState.initState, initState, privateKey, pubEK, pubSK] <;> - cases b <;> - try simp - · left; left; right; exists Agent.Spy; apply And.intro; exact Spy_in_bad; rfl - · left; left; left; exists Agent.Spy; apply And.intro; exact Spy_in_bad; rfl + cases b <;> simp[Spy_in_bad] @[simp] lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} : @@ -342,9 +335,7 @@ lemma publicKey_in_initState {b : KeyMode} {A : Agent} {B : Agent} : lemma spies_pubK : Msg.Key (publicKey b A) ∈ spies evs := by induction evs with | nil => simp [spies, knows] - cases b - · right; exists A - · left; right; exists A + cases b <;> tauto | cons e evs ih => cases e <;> rw [spies] <;> apply knows_subset_knows_Cons <;> assumption @@ -355,10 +346,7 @@ lemma analz_spies_pubK : Msg.Key (publicKey b A) ∈ analz (spies evs) := by -- Spy sees private keys of bad agents lemma Spy_spies_bad_privateKey { h : A ∈ bad } : Msg.Key (privateKey b A) ∈ spies evs := by induction evs with - | nil => simp [spies, knows, pubSK, pubEK]; left; left - cases b - · right; exists A - · left; exists A + | nil => simp_all [spies, knows, pubSK, pubEK]; cases b <;> tauto | cons e evs ih => cases e <;> rw[spies] <;> aapply knows_subset_knows_Cons @@ -405,14 +393,11 @@ by simp[Crypt_synth_EK]; @[simp] lemma Nonce_notin_initState {B : Agent} : Msg.Nonce N ∉ parts (initState B) := by cases B <;> - simp [initState] <;> apply And.intro <;> try (apply And.intro) - all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty]; simp) + simp [initState] @[simp] lemma Nonce_notin_used_empty : Msg.Nonce N ∉ used [] := by - simp [used]; intro A; cases A <;> simp <;> - apply And.intro <;> try (apply And.intro) - all_goals (rw[Set.singleton_def, parts_insert_Key, parts_empty]; simp) + simp [used]; intro A; cases A <;> simp -- Supply fresh nonces for possibility theorems lemma Nonce_supply_lemma : ∃ N, ∀ n, N ≤ n → Msg.Nonce n ∉ used evs := by