# HG changeset patch # User paulson # Date 1051612609 -7200 # Node ID 4822d9597d1e4a5d40eb7f49fa7428480c83de5b # Parent 8c23dea4648e5a5b021fcc62761879e55e5d3610 tweaks diff -r 8c23dea4648e -r 4822d9597d1e src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Tue Apr 29 12:36:40 2003 +0200 +++ b/src/HOL/Auth/Event.thy Tue Apr 29 12:36:49 2003 +0200 @@ -73,10 +73,12 @@ used_Nil: "used [] = (UN B. parts (initState B))" used_Cons: "used (ev # evs) = (case ev of - Says A B X => parts {X} \ (used evs) + Says A B X => parts {X} \ used evs | Gets A X => used evs - | Notes A X => parts {X} \ (used evs))" - + | Notes A X => parts {X} \ used evs)" + --{*The case for @{term Gets} seems anomalous, but @{term Gets} always + follows @{term Says} in real protocols. Seems difficult to change. + See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}. *} lemma Notes_imp_used [rule_format]: "Notes A X \ set evs --> X \ used evs" apply (induct_tac evs) @@ -101,7 +103,7 @@ = parts {X} \ parts (knows Spy evs)"}. The general case loops.*) text{*This version won't loop with the simplifier.*} -lemmas parts_insert_knows_Spy = parts_insert [of _ "knows Spy evs", standard] +lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard] lemma knows_Spy_Says [simp]: "knows Spy (Says A B X # evs) = insert X (knows Spy evs)" @@ -118,15 +120,15 @@ by simp lemma knows_Spy_subset_knows_Spy_Says: - "knows Spy evs <= knows Spy (Says A B X # evs)" + "knows Spy evs \ knows Spy (Says A B X # evs)" by (simp add: subset_insertI) lemma knows_Spy_subset_knows_Spy_Notes: - "knows Spy evs <= knows Spy (Notes A X # evs)" + "knows Spy evs \ knows Spy (Notes A X # evs)" by force lemma knows_Spy_subset_knows_Spy_Gets: - "knows Spy evs <= knows Spy (Gets A X # evs)" + "knows Spy evs \ knows Spy (Gets A X # evs)" by (simp add: subset_insertI) text{*Spy sees what is sent on the traffic*} @@ -152,7 +154,7 @@ text{*Compatibility for the old "spies" function*} lemmas spies_partsEs = knows_Spy_partsEs lemmas Says_imp_spies = Says_imp_knows_Spy -lemmas parts_insert_spies = parts_insert_knows_Spy +lemmas parts_insert_spies = parts_insert_knows_A [of _ Spy] subsection{*Knowledge of Agents*} @@ -168,17 +170,14 @@ by simp -lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A' B X # evs)" -apply (simp add: subset_insertI) -done +lemma knows_subset_knows_Says: "knows A evs \ knows A (Says A' B X # evs)" +by (simp add: subset_insertI) -lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A' X # evs)" -apply (simp add: subset_insertI) -done +lemma knows_subset_knows_Notes: "knows A evs \ knows A (Notes A' X # evs)" +by (simp add: subset_insertI) -lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A' X # evs)" -apply (simp add: subset_insertI) -done +lemma knows_subset_knows_Gets: "knows A evs \ knows A (Gets A' X # evs)" +by (simp add: subset_insertI) text{*Agents know what they say*} lemma Says_imp_knows [rule_format]: "Says A B X \ set evs --> X \ knows A evs" @@ -224,27 +223,16 @@ apply blast done - - - -text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} -declare knows_Cons [simp del] - - -subsection{*Fresh Nonces*} - -lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs" -apply (induct_tac "evs") -apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split) -apply blast+ +lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) \ used evs" +apply (induct_tac "evs", force) +apply (simp add: parts_insert_knows_A knows_Cons add: event.split, blast) done lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] lemma initState_into_used: "X \ parts (initState B) ==> X \ used evs" apply (induct_tac "evs") -apply (simp_all (no_asm_simp) add: parts_insert_knows_Spy split add: event.split) -apply blast +apply (simp_all add: parts_insert_knows_A split add: event.split, blast) done lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} \ used evs" @@ -256,13 +244,14 @@ lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" by simp -lemma used_nil_subset: "used [] <= used evs" -apply (simp) +lemma used_nil_subset: "used [] \ used evs" +apply simp apply (blast intro: initState_into_used) done text{*NOTE REMOVAL--laws above are cleaner, as they don't involve "case"*} -declare used_Nil [simp del] used_Cons [simp del] +declare knows_Cons [simp del] + used_Nil [simp del] used_Cons [simp del] text{*For proving theorems of the form @{term "X \ analz (knows Spy evs) --> P"} @@ -291,7 +280,7 @@ lemma knows_subset_knows_Cons: "knows A evs \ knows A (e # evs)" by (induct e, auto simp: knows_Cons) -lemma initState_subset_knows: "initState A <= knows A evs" +lemma initState_subset_knows: "initState A \ knows A evs" apply (induct_tac evs, simp) apply (blast intro: knows_subset_knows_Cons [THEN subsetD]) done @@ -322,31 +311,17 @@ val Notes_imp_used = thm "Notes_imp_used"; val Says_imp_used = thm "Says_imp_used"; val MPair_used = thm "MPair_used"; -val parts_insert_knows_Spy = thm "parts_insert_knows_Spy"; -val knows_Spy_Says = thm "knows_Spy_Says"; -val knows_Spy_Notes = thm "knows_Spy_Notes"; -val knows_Spy_Gets = thm "knows_Spy_Gets"; -val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; -val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; -val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; val Says_imp_knows_Spy = thm "Says_imp_knows_Spy"; val Notes_imp_knows_Spy = thm "Notes_imp_knows_Spy"; val knows_Spy_partsEs = thms "knows_Spy_partsEs"; val spies_partsEs = thms "spies_partsEs"; val Says_imp_spies = thm "Says_imp_spies"; val parts_insert_spies = thm "parts_insert_spies"; -val knows_Says = thm "knows_Says"; -val knows_Notes = thm "knows_Notes"; -val knows_Gets = thm "knows_Gets"; -val knows_subset_knows_Says = thm "knows_subset_knows_Says"; -val knows_subset_knows_Notes = thm "knows_subset_knows_Notes"; -val knows_subset_knows_Gets = thm "knows_subset_knows_Gets"; val Says_imp_knows = thm "Says_imp_knows"; val Notes_imp_knows = thm "Notes_imp_knows"; val Gets_imp_knows_agents = thm "Gets_imp_knows_agents"; val knows_imp_Says_Gets_Notes_initState = thm "knows_imp_Says_Gets_Notes_initState"; val knows_Spy_imp_Says_Notes_initState = thm "knows_Spy_imp_Says_Notes_initState"; -val parts_knows_Spy_subset_used = thm "parts_knows_Spy_subset_used"; val usedI = thm "usedI"; val initState_into_used = thm "initState_into_used"; val used_Says = thm "used_Says"; @@ -361,6 +336,11 @@ val synth_analz_mono = thm "synth_analz_mono"; +val knows_Spy_subset_knows_Spy_Says = thm "knows_Spy_subset_knows_Spy_Says"; +val knows_Spy_subset_knows_Spy_Notes = thm "knows_Spy_subset_knows_Spy_Notes"; +val knows_Spy_subset_knows_Spy_Gets = thm "knows_Spy_subset_knows_Spy_Gets"; + + val synth_analz_mono_contra_tac = let val syan_impI = inst "P" "?Y \ synth (analz (knows Spy ?evs))" impI in diff -r 8c23dea4648e -r 4822d9597d1e src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Tue Apr 29 12:36:40 2003 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Tue Apr 29 12:36:49 2003 +0200 @@ -302,9 +302,9 @@ apply (force dest!: Crypt_imp_keysFor) txt{*NS3*} apply blast -txt{*NS4*} -apply (blast dest!: B_trusts_NS3 - dest: Says_imp_knows_Spy [THEN analz.Inj] +txt{*NS4*} +apply (blast dest: B_trusts_NS3 + Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad unique_session_keys) done @@ -334,7 +334,7 @@ txt{*NS3*} apply blast txt{*NS4*} -apply (blast dest!: B_trusts_NS3 +apply (blast dest: B_trusts_NS3 dest: Says_imp_knows_Spy [THEN analz.Inj] unique_session_keys Crypt_Spy_analz_bad) done diff -r 8c23dea4648e -r 4822d9597d1e src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Tue Apr 29 12:36:40 2003 +0200 +++ b/src/HOL/Auth/Public.thy Tue Apr 29 12:36:49 2003 +0200 @@ -176,9 +176,10 @@ (Key ` range pubEK) \ (Key ` range pubSK)" - text{*These lemmas allow reasoning about @{term "used evs"} rather than - @{term "knows Spy evs"}, which is useful when there are private Notes. *} + @{term "knows Spy evs"}, which is useful when there are private Notes. + Because they depend upon the definition of @{term initState}, they cannot + be moved up.*} lemma used_parts_subset_parts [rule_format]: "\X \ used evs. parts {X} \ used evs" @@ -186,14 +187,10 @@ prefer 2 apply (simp add: used_Cons) apply (rule ballI) - apply (case_tac a, auto) - apply (drule parts_cut, assumption, simp) - apply (drule parts_cut, assumption, simp) + apply (case_tac a, auto) +apply (auto dest!: parts_cut) txt{*Base case*} -apply (simp add: used_Nil, clarify) -apply (rename_tac B) -apply (rule_tac x=B in exI) -apply (case_tac B, auto) +apply (simp add: used_Nil) done lemma MPair_used_D: "{|X,Y|} \ used H ==> X \ used H & Y \ used H" @@ -218,6 +215,9 @@ lemma Crypt_notin_initState: "Crypt K X \ parts (initState B)" by (induct B, auto) +lemma Crypt_notin_used_empty [simp]: "Crypt K X \ used []" +by (simp add: Crypt_notin_initState used_Nil) + (*** Basic properties of shrK ***) diff -r 8c23dea4648e -r 4822d9597d1e src/HOL/Auth/Recur.thy --- a/src/HOL/Auth/Recur.thy Tue Apr 29 12:36:40 2003 +0200 +++ b/src/HOL/Auth/Recur.thy Tue Apr 29 12:36:49 2003 +0200 @@ -392,8 +392,8 @@ apply blast txt{*Inductive step of respond*} apply (intro allI conjI impI, simp_all) -txt{*by unicity, either B=Aa or B=A', a contradiction if B \ bad*} -apply (blast dest: unique_session_keys [OF _ respond_certificate]) +txt{*by unicity, either B=Aa or B=A', a contradiction if B \ bad*} +apply (blast dest: unique_session_keys respond_certificate) apply (blast dest!: respond_certificate) apply (blast dest!: resp_analz_insert) done