From 7324a942d9f646a7bf305e828d40cf6b45bcabb5 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/Message.lean | 2 - InductiveVerification/NS_Public.lean | 234 +++++++++++---------------- Main.lean | 2 +- 3 files changed, 93 insertions(+), 145 deletions(-) diff --git a/InductiveVerification/Message.lean b/InductiveVerification/Message.lean index 04ce031..c307656 100644 --- a/InductiveVerification/Message.lean +++ b/InductiveVerification/Message.lean @@ -1628,5 +1628,3 @@ X ∈ A ∨ h₁ → X ∈ B ∨ h₁ 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 eb3e230..7ca9a8d 100644 --- a/InductiveVerification/NS_Public.lean +++ b/InductiveVerification/NS_Public.lean @@ -40,7 +40,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 +52,16 @@ 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 => + -- TODO add these attributes to simp, also check what can be added to grind + | Nil => simp[spies, knows, initState, pubEK, priEK, pubSK] + | 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} : @@ -70,7 +70,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 --- It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce is secret +-- 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 } : (Crypt (pubEK C) ⦃NA', Nonce NA, Agent D⦄ ∈ parts (spies evs) → (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄ ∈ parts (spies evs) → @@ -78,28 +79,24 @@ theorem no_nonce_NS1_NS2 { evs: List Event} { h : ns_public evs } : intro h₁ h₂ 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) - | NS1 _ nonce_not_used => + | Fake _ h => + 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 => 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 - | NS2 _ nonce_not_used => + grind [ parts_knows_Spy_subset_used ] + | NS2 => 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] - | NS3 _ _ _ a_ih => apply analz_spies_mono; simp_all + grind [ parts_knows_Spy_subset_used ] + | NS3 => apply analz_spies_mono; simp_all -- Unicity for NS1: nonce NA identifies agents A and B theorem unique_NA { h : ns_public evs } : @@ -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; @@ -136,37 +129,29 @@ theorem Spy_not_see_NA { h : ns_public evs } intro h₁ h₄ induction h with | Nil => simp_all - | Fake _ a => - have _ := Spy_in_bad; apply Fake_analz_insert at a; apply a at h₄; simp_all - | NS1 _ a a_ih => + | Fake _ a => apply Fake_analz_insert at a; apply a at h₄; simp_all[Spy_in_bad] + | NS1 _ a => 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 + | 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 +164,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} : @@ -211,14 +191,13 @@ lemma B_trusts_NS1 { h : ns_public evs} : intro h₁ h₂ induction h with | Nil => simp[spies, knows] at h₁ - | Fake _ a a_ih => + | Fake _ a => 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` @@ -231,27 +210,19 @@ theorem unique_NB { h : ns_public evs } : -- Proof closely follows that of unique_NA induction h with | Nil => aesop (add norm spies, norm knows, safe analz_insertI) - | Fake _ a a_ih => + | Fake _ a => 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₃; 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 +234,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 } : @@ -301,28 +273,17 @@ 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 => + | Fake _ a => 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₂ => - 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 + | NS2 => + simp [*] at *; expand_parts_element at h₂; + grind[ parts_knows_Spy_subset_used ]; + | NS3 => + simp [*] at *; grind [ Spy_not_see_NB, Says_imp_parts_knows_Spy, unique_NB ] -- Overall guarantee for `B` @@ -337,29 +298,18 @@ theorem B_trusts_protocol { h : ns_public evs } intro h₁ h₂ induction h with | Nil => simp_all - | Fake _ a a_ih => + | Fake _ a => simp [*] at * 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 => + | NS2 => + 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 diff --git a/Main.lean b/Main.lean index bfa0201..b647d88 100644 --- a/Main.lean +++ b/Main.lean @@ -1,5 +1,5 @@ -- import InductiveVerification -import InductiveVerification.Public +import InductiveVerification.NS_Public def main : IO Unit := IO.println "Hello, world!"