From 943525dfb55a2923102688b58d368d2ade3c6b75 Mon Sep 17 00:00:00 2001 From: Your Name Date: Thu, 5 Mar 2026 10:02:06 +0100 Subject: [PATCH] Replaced some cases instances with grind --- InductiveVerification/NS_Public.lean | 208 +++++++++++---------------- 1 file changed, 80 insertions(+), 128 deletions(-) diff --git a/InductiveVerification/NS_Public.lean b/InductiveVerification/NS_Public.lean index eb3e230..69751d2 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -11,6 +11,8 @@ open Bad open HasInitState open InvKey +attribute [-simp] Key.injEq + -- Define the inductive set `ns_public` inductive ns_public : List Event → Prop | Nil : ns_public [] @@ -40,7 +42,7 @@ theorem possibility_property : constructor · apply ns_public.NS3 · apply ns_public.NS2 - · apply_rules [ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty] + · apply_rules[ns_public.NS1, ns_public.Nil, Nonce_notin_used_empty] · simp · tauto all_goals tauto @@ -52,16 +54,15 @@ theorem Spy_see_priEK {h : ns_public evs} : (Key (priEK A) ∈ parts (spies evs)) ↔ A ∈ bad := by constructor · induction h with - | Nil => - simp[spies, knows, initState, pubEK, priEK, pubSK] - | Fake _ h ih => + | Nil => simp[spies, knows, initState, pubEK, priEK, pubSK, Key.injEq] + | Fake _ h => apply Fake_parts_sing at h intro h₁; simp at h₁; apply Fake_parts_sing_helper (h := h) at h₁ simp_all | NS1 => simp_all | NS2 => simp_all | NS3 => simp_all - · intro h₁; apply parts_increasing; aapply Spy_spies_bad_privateKey + · intro _; apply_rules [ parts_increasing, Spy_spies_bad_privateKey ] @[simp] theorem Spy_analz_priEK {h : ns_public evs} : @@ -79,26 +80,22 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : induction h with | 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 ((_ | _) | _) <;> - simp_all - all_goals (right; aapply ih <;> aapply analz_subset_parts) + apply analz_spies_mono + simp [*] at * + apply Fake_parts_sing at h + apply Fake_parts_sing_helper (h := h) at h₁ + apply Fake_parts_sing_helper (h := h) at h₂ + simp [*] at *; grind[analz_subset_parts] | NS1 _ nonce_not_used => apply analz_spies_mono simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; expand_parts_element at h₁; expand_parts_element at h₂; - cases h₂ <;> simp_all + grind [ parts_knows_Spy_subset_used ] | NS2 _ nonce_not_used => apply analz_spies_mono simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; expand_parts_element at h₂; - cases h₁ <;> simp_all[-Key.injEq] + grind [ parts_knows_Spy_subset_used ] | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all -- Unicity for NS1: nonce NA identifies agents A and B @@ -116,14 +113,10 @@ theorem unique_NA { h : ns_public evs } : 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₃ - 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 + | NS1 => + intro h₁ h₂ _; simp [*] at * + expand_parts_element at h₁; expand_parts_element at h₂ + grind [ analz_insert_mono_neg, parts_knows_Spy_subset_used_neg ] | NS2 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all | NS3 => intro _ _ h₃; apply analz_insert_mono_neg at h₃; simp_all; @@ -144,29 +137,22 @@ theorem Spy_not_see_NA { h : ns_public evs } · 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 + | NS2 _ _ a a_ih => + simp [*] at *; have _ := h₄; have c := h₁ + apply Says_imp_parts_knows_Spy at h₁ + have d := h₁ + expand_parts_element at d + apply analz_insert_Crypt_subset at h₄; simp at h₄; rcases h₄ with (h |h |h) + <;> simp [*] at *; + · apply a_ih at c; have _ := c; 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₄ + · grind[parts_knows_Spy_subset_used] + | NS3 => 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 + grind [Says_imp_parts_knows_Spy, no_nonce_NS1_NS2] --- Authentication for `A`: if she receives message 2 and has used `NA` to start a run, then `B` has sent message 2. +-- 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 } { not_bad_B : B ∉ bad } : @@ -179,28 +165,23 @@ 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 => have snsNA := h₁; apply Spy_not_see_NA at snsNA <;> try assumption apply analz_spies_mono_neg at snsNA simp [*] at * cases h₁ - · have _ := Spy_in_bad; simp_all + · simp_all[Spy_in_bad] · apply Fake_parts_sing at a; apply Fake_parts_sing_helper (h := a) at h₂; simp at h₂ - rcases h₂ with ((_ | _) | _) <;> (right; aapply a_ih) - · aapply analz_subset_parts - · tauto + grind [analz_subset_parts] · aapply ns_public.Fake - | 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 => + | NS1 => + simp [*] at *; expand_parts_element at h₂ + grind[parts_knows_Spy_subset_used_neg] + | NS2 => 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; + grind [ Spy_not_see_NA, Says_imp_parts_knows_Spy, unique_NA ] + | NS3 => simp_all; -- If the encrypted message appears then it originated with Alice in `NS1` lemma B_trusts_NS1 { h : ns_public evs} : @@ -215,10 +196,9 @@ lemma B_trusts_NS1 { h : ns_public evs} : 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_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; + | NS1 => apply analz_spies_mono_neg at h₂; simp_all; cases h₁ <;> simp_all + | NS2 => apply analz_spies_mono_neg at h₂; simp_all; + | NS3 => apply analz_spies_mono_neg at h₂; simp_all; -- Authenticity Properties obtained from `NS2` @@ -236,22 +216,14 @@ theorem unique_NB { h : ns_public evs } : 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₃; simp [*] at * + grind[analz_subset_parts] + | NS1 => intro _ _ h₃; apply analz_spies_mono_neg at h₃; simp_all + | NS2 => + intro 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[-Key.injEq] + grind[analz_insert_mono_neg, parts_knows_Spy_subset_used] + | NS3 => intro _ _ _; simp_all; grind[analz_insert_mono_neg] -- `NB` remains secret theorem Spy_not_see_NB { h : ns_public evs } @@ -263,33 +235,34 @@ theorem Spy_not_see_NB { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | 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 => + | Fake _ a => + apply Fake_analz_insert at a; apply a at h₄; simp_all[Spy_in_bad]; + | NS1 => simp [*] at * apply analz_insert_Crypt_subset at h₄; simp at h₄ - apply parts_knows_Spy_subset_used_neg at nonce_not_used 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 => + expand_parts_element at h₂ + grind[parts_knows_Spy_subset_used] + | NS2 => simp [*] at * - apply parts_knows_Spy_subset_used_neg at not_used_NB + have _ := h₄ + apply analz_insert_Crypt_subset at h₄; simp at h₄ 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₁; - expand_parts_element at h₁; simp_all - · aapply a_ih - | NS3 _ _ a a_ih => + · simp_all; grind[parts_knows_Spy_subset_used, analz_subset_parts] + · have _ := h₁; apply Says_imp_parts_knows_Spy at h₁ + expand_parts_element at h₁ + grind[ + parts_knows_Spy_subset_used, + Says_imp_parts_knows_Spy, + no_nonce_NS1_NS2 + ]; + | NS3 => 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 + grind[Says_imp_parts_knows_Spy, unique_NB] --- Authentication for `B`: if he receives message 3 and has used `NB` in message 2, then `A` has sent message 3. +-- 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 } { not_bad_A : A ∉ bad } { not_bad_B : B ∉ bad } : @@ -305,24 +278,14 @@ theorem B_trusts_NS3 { h : ns_public evs } simp [*] at * apply Fake_parts_sing at a 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 + grind [ Spy_in_bad, analz_subset_parts, Spy_not_see_NB ] | NS1 => simp_all - | NS2 _ nonce_not_used => - simp [*] at * - apply parts_knows_Spy_subset_used_neg at nonce_not_used; - expand_parts_element at h₂; cases h₁ <;> simp_all - | NS3 _ _ a₂ => + | NS2 => + simp [*] at *; expand_parts_element at h₂ + grind[ parts_knows_Spy_subset_used ]; + | NS3 => 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 unique_NB at h₁; - apply Says_imp_parts_knows_Spy at a₂; apply h₁ at a₂ - all_goals simp_all + grind [Spy_not_see_NB, Says_imp_parts_knows_Spy, unique_NB] -- Overall guarantee for `B` @@ -342,24 +305,13 @@ theorem B_trusts_protocol { h : ns_public evs } apply Fake_parts_sing at a 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 + grind[Spy_in_bad, analz_subset_parts, Spy_not_see_NB] | NS1 => simp_all | NS2 _ nonce_not_used a a_ih => + simp [*] at *; expand_parts_element at h₁ + grind[parts_knows_Spy_subset_used]; + | NS3 => 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 * - 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 + grind[Spy_not_see_NB, Says_imp_parts_knows_Spy, unique_NB ] end NS_Public