From 0f017b08b570903e208b2b1c36feb090de64f348 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 | 11 ++++ InductiveVerification/NS_Public.lean | 83 +++++++++++----------------- 2 files changed, 44 insertions(+), 50 deletions(-) diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index 4a429b2..2adc922 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) := diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index 232ee06..144a98a 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -89,7 +89,7 @@ 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₂ + | Nil => simp[spies, knows] at h₂ | Fake _ h ih => simp; apply analz_insert; right apply Fake_parts_sing at h @@ -101,14 +101,14 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : 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₂; + simp[spies] at h₁; expand_parts_element at h₁; + simp[spies] at h₂; expand_parts_element 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₂; + simp[spies] at h₁; expand_parts_element at h₁; + simp[spies] at h₂; expand_parts_element 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 @@ -135,11 +135,9 @@ 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₁; 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₃; + simp 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₂ + simp at h₃; rcases h₁ with ((_ | _) | _) <;> rcases h₂ with ((_ | _) | _) <;> try ( @@ -152,8 +150,8 @@ theorem unique_NA { h : ns_public evs } : )) | 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₂ + simp at h₁; expand_parts_element at h₁ + simp 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] @@ -199,7 +197,7 @@ 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) + simp at h₄; rcases h₄ with ( 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₂ @@ -207,10 +205,7 @@ theorem Spy_not_see_NA { h : ns_public evs } · 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 + · aapply a_ih -- 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 } @@ -236,23 +231,16 @@ theorem A_trusts_NS2 {h : ns_public evs } · 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; + | NS1 _ a a_ih => + simp at h₂; expand_parts_element at h₂ + apply parts_knows_Spy_subset_used_neg at a; cases h₁ <;> simp_all + 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 + simp at h₂; 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 at h₁; simp at h₂; right; aapply a_ih -- If the encrypted message appears then it originated with Alice in `NS1` @@ -263,7 +251,7 @@ 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 => simp at h₁; apply Fake_parts_sing at a; apply Fake_parts_sing_helper (h := a) at h₁; simp at h₁ @@ -289,25 +277,20 @@ 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₁; + apply Fake_parts_sing at a; intro h₁ h₂ h₃; + simp 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₂) <;> + 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₂ + simp at h₁; expand_parts_element at h₁ + simp at h₂; expand_parts_element at h₂ apply analz_spies_mono_neg at h₃; apply parts_knows_Spy_subset_used_neg at nonce_not_used rcases h₁ with (_ | h₁) <;> @@ -333,7 +316,7 @@ theorem Spy_not_see_NB { h : ns_public evs } 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 + expand_parts_element at h₁; simp_all | inr => aapply a_ih | NS2 _ not_used_NB a a_ih => simp at h₁; @@ -345,7 +328,7 @@ theorem Spy_not_see_NB { h : ns_public evs } · 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₄; @@ -370,7 +353,7 @@ theorem B_trusts_NS3 { h : ns_public evs } 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₂ + expand_parts_element 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 @@ -380,11 +363,11 @@ theorem B_trusts_NS3 { h : ns_public evs } | 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₂; expand_parts_element 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₂ + simp at h₂; expand_parts_element at h₂; cases h₂ <;> simp_all have h₁c := h₁ apply Spy_not_see_NB at h₁c @@ -409,7 +392,7 @@ theorem B_trusts_protocol { h : ns_public evs } 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₁ + expand_parts_element at h₁ have _ := Spy_in_bad simp at h₂; rcases h₂ with (_ | h₂) <;> simp_all rcases h₁ with (((_ |_ ) | _) | _) <;> try (aapply a_ih) @@ -423,7 +406,7 @@ theorem B_trusts_protocol { h : ns_public evs } | inr => aapply a_ih | NS3 _ _ a₂ a_ih => simp at h₂ - simp at h₁; rw[parts_element, Set.subset_def] at h₁; simp at h₁ + simp at h₁; expand_parts_element at h₁ cases h₁ <;> simp_all have h₂c := h₂ apply Spy_not_see_NB at h₂c