--- a/src/HOL/Auth/KerberosIV.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/KerberosIV.thy Sat Aug 17 14:55:08 2002 +0200
@@ -44,7 +44,7 @@
(* A is the true creator of X if she has sent X and X never appeared on
the trace before this event. Recall that traces grow from head. *)
- Issues :: [agent , agent, msg, event list] => bool ("_ Issues _ with _ on _")
+ Issues :: [agent, agent, msg, event list] => bool ("_ Issues _ with _ on _")
"A Issues B with X on evs ==
\\<exists>Y. Says A B Y \\<in> set evs & X \\<in> parts {Y} &
X \\<notin> parts (spies (takeWhile (% z. z \\<noteq> Says A B Y) (rev evs)))"
--- a/src/HOL/Auth/Kerberos_BAN.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Kerberos_BAN.thy Sat Aug 17 14:55:08 2002 +0200
@@ -89,5 +89,4 @@
Expired Ts evso |]
==> Notes Spy {|Number Ts, Key K|} # evso \\<in> kerberos_ban"
-
end
--- a/src/HOL/Auth/NS_Public.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Public.thy Sat Aug 17 14:55:08 2002 +0200
@@ -103,8 +103,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
done
@@ -166,8 +165,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast intro: no_nonce_NS1_NS2)+
done
--- a/src/HOL/Auth/NS_Public_Bad.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Public_Bad.thy Sat Aug 17 14:55:08 2002 +0200
@@ -106,8 +106,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NA \<notin> analz (spies evs)"
apply (erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+
done
@@ -167,8 +166,7 @@
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)"
apply (erule rev_mp, erule rev_mp)
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
apply (simp_all add: all_conj_distrib) (*speeds up the next step*)
apply (blast intro: no_nonce_NS1_NS2)+
done
@@ -197,17 +195,15 @@
lemma "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk>
\<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs
\<longrightarrow> Nonce NB \<notin> analz (spies evs)"
-apply (erule ns_public.induct, simp_all)
-apply spy_analz
+apply (erule ns_public.induct, simp_all, spy_analz)
(*NS1: by freshness*)
apply blast
(*NS2: by freshness and unicity of NB*)
apply (blast intro: no_nonce_NS1_NS2)
(*NS3: unicity of NB identifies A and NA, but not B*)
apply clarify
-apply (frule_tac A' = "A" in
- Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB])
-apply auto
+apply (frule_tac A' = A in
+ Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto)
apply (rename_tac C B' evs3)
oops
--- a/src/HOL/Auth/NS_Shared.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Sat Aug 17 14:55:08 2002 +0200
@@ -85,8 +85,7 @@
apply (intro exI bexI)
apply (rule_tac [2] ns_shared.Nil
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
- THEN ns_shared.NS4, THEN ns_shared.NS5])
-apply possibility
+ THEN ns_shared.NS4, THEN ns_shared.NS5], possibility)
done
(*This version is similar, while instantiating ?K and ?N to epsilon-terms
@@ -116,9 +115,7 @@
(*Spy never sees another agent's shared key! (unless it's bad at start)*)
lemma Spy_see_shrK [simp]:
"evs \\<in> ns_shared \\<Longrightarrow> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
-apply blast+;
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -129,8 +126,7 @@
(*Nobody can have used non-existent keys!*)
lemma new_keys_not_used [rule_format, simp]:
"evs \\<in> ns_shared \\<Longrightarrow> Key K \\<notin> used evs \\<longrightarrow> K \\<notin> keysFor (parts (spies evs))"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
(*Fake, NS2, NS4, NS5*)
apply (blast dest!: keysFor_parts_insert)+
done
@@ -154,8 +150,7 @@
A \\<notin> bad; evs \\<in> ns_shared\\<rbrakk>
\\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs"
apply (erule rev_mp)
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply auto
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done
lemma cert_A_form:
@@ -182,7 +177,7 @@
\\<Longrightarrow> Says Server A (Crypt (shrK A) \\<lbrace>Nonce NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs
\\<or> X \\<in> analz (spies evs)"
apply (case_tac "A \\<in> bad")
-apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
+apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj])
by (blast dest!: A_trusts_NS2 Says_Server_message_form)
*)
@@ -202,8 +197,7 @@
lemma "\\<lbrakk>evs \\<in> ns_shared; Kab \\<notin> range shrK\\<rbrakk> \\<Longrightarrow>
(Crypt KAB X) \\<in> parts (spies evs) \\<and>
Key K \\<in> parts {X} \\<longrightarrow> Key K \\<in> parts (spies evs)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply simp_all
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
(*Fake*)
apply (blast dest: parts_insert_subset_Un)
(*Base, NS4 and NS5*)
@@ -222,9 +216,7 @@
(K \\<in> KK \\<or> Key K \\<in> analz (spies evs))"
apply (erule ns_shared.induct, force)
apply (drule_tac [7] Says_Server_message_form)
-apply (erule_tac [4] Says_S_message_form [THEN disjE])
-apply analz_freshK
-apply spy_analz
+apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
done
@@ -242,9 +234,7 @@
"\\<lbrakk>Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs;
Says Server A' (Crypt (shrK A') \\<lbrace>NA', Agent B', Key K, X'\\<rbrace>) \\<in> set evs;
evs \\<in> ns_shared\\<rbrakk> \\<Longrightarrow> A=A' \\<and> NA=NA' \\<and> B=B' \\<and> X = X'"
-apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
-apply simp_all
-apply blast+
+apply (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+)
done
@@ -263,8 +253,7 @@
apply (frule_tac [7] Says_Server_message_form)
apply (frule_tac [4] Says_S_message_form)
apply (erule_tac [5] disjE)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
-apply spy_analz (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) (*Fake*)
apply blast (*NS2*)
(*NS3, Server sub-case*) (**LEVEL 8 **)
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
@@ -295,8 +284,7 @@
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>)
\\<in> set evs"
apply (erule rev_mp)
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply auto
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto)
done
@@ -307,12 +295,10 @@
Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
Says B A (Crypt K (Nonce NB)) \\<in> set evs"
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply (analz_mono_contra, simp_all)
-apply blast (*Fake*)
+apply (analz_mono_contra, simp_all, blast) (*Fake*)
(*NS2: contradiction from the assumptions
Key K \\<notin> used evs2 and Crypt K (Nonce NB) \\<in> parts (spies evs2) *)
-apply (force dest!: Crypt_imp_keysFor)
-apply blast (*NS3*)
+apply (force dest!: Crypt_imp_keysFor, blast) (*NS3*)
(*NS4*)
apply (blast dest!: B_trusts_NS3
dest: Says_imp_knows_Spy [THEN analz.Inj]
@@ -338,10 +324,8 @@
Says Server A (Crypt (shrK A) \\<lbrace>NA, Agent B, Key K, X\\<rbrace>) \\<in> set evs \\<longrightarrow>
Crypt K (Nonce NB) \\<in> parts (spies evs) \\<longrightarrow>
(\\<exists>A'. Says A' B X \\<in> set evs)"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply analz_mono_contra
-apply (simp_all add: ex_disj_distrib)
-apply blast (*Fake*)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
+apply (simp_all add: ex_disj_distrib, blast) (*Fake*)
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
apply blast (*NS3*)
(*NS4*)
@@ -359,10 +343,7 @@
Crypt (shrK B) \\<lbrace>Key K, Agent A\\<rbrace>\\<rbrace>) \\<in> set evs \\<longrightarrow>
Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace> \\<in> parts (spies evs) \\<longrightarrow>
Says A B (Crypt K \\<lbrace>Nonce NB, Nonce NB\\<rbrace>) \\<in> set evs"
-apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
-apply analz_mono_contra
-apply simp_all
-apply blast (*Fake*)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast) (*Fake*)
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) (*NS2*)
apply (blast dest!: cert_A_form) (*NS3*)
(*NS5*)
--- a/src/HOL/Auth/OtwayRees.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees.thy Sat Aug 17 14:55:08 2002 +0200
@@ -98,15 +98,13 @@
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
done
lemma Gets_imp_Says [dest!]:
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
done
@@ -141,8 +139,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -162,8 +159,7 @@
"[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs;
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
-apply (erule rev_mp, erule otway.induct, simp_all)
-apply blast
+apply (erule rev_mp, erule otway.induct, simp_all, blast)
done
@@ -188,9 +184,7 @@
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
done
@@ -225,8 +219,7 @@
Crypt (shrK A) {|NA, Agent A, Agent B|}|}
\<in> set evs"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
lemma Crypt_imp_OR1_Gets:
@@ -248,8 +241,7 @@
==> B = C"
apply (erule rev_mp, erule rev_mp)
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
@@ -262,8 +254,7 @@
==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)"
apply (erule rev_mp)
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
(*Crucial property: If the encrypted message appears, and A has used NA
@@ -278,8 +269,7 @@
Crypt (shrK A) {|NA, Key K|},
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
(*OR1: it cannot be a new Nonce, contradiction.*)
apply blast
(*OR3*)
@@ -321,8 +311,7 @@
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*)
(*OR3, OR4, Oops*)
apply (blast dest: unique_session_keys)+
done
@@ -363,8 +352,7 @@
\<in> set evs"
apply (erule rev_mp)
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
@@ -397,8 +385,7 @@
\<in> set evs)"
apply simp
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast)
(*OR1: it cannot be a new Nonce, contradiction.*)
(*OR2*)
apply blast
--- a/src/HOL/Auth/OtwayRees_AN.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees_AN.thy Sat Aug 17 14:55:08 2002 +0200
@@ -90,8 +90,7 @@
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
done
lemma Gets_imp_Says [dest!]:
@@ -115,8 +114,7 @@
(*Spy never sees a good agent's shared key!*)
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
-apply (erule otway.induct, simp_all)
-apply blast+
+apply (erule otway.induct, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -139,9 +137,7 @@
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
apply (erule rev_mp)
-apply (erule otway.induct)
-apply simp_all
-apply blast
+apply (erule otway.induct, simp_all, blast)
done
@@ -166,9 +162,7 @@
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
-apply (drule_tac [6] OR4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [6] OR4_analz_knows_Spy, analz_freshK, spy_analz)
done
lemma analz_insert_freshK:
@@ -191,8 +185,7 @@
\<in> set evs;
evs \<in> otway |]
==> A=A' & B=B' & NA=NA' & NB=NB'"
-apply (erule rev_mp, erule rev_mp, erule otway.induct)
-apply simp_all
+apply (erule rev_mp, erule rev_mp, erule otway.induct, simp_all)
(*Remaining cases: OR3 and OR4*)
apply blast+
done
@@ -211,7 +204,7 @@
apply (erule otway.induct, force)
apply (simp_all add: ex_disj_distrib)
(*Fake, OR3*)
-apply blast+;
+apply blast+
done
@@ -242,8 +235,7 @@
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*)
(*OR3, OR4, Oops*)
apply (blast dest: unique_session_keys)+
done
@@ -284,7 +276,7 @@
\<in> set evs)"
apply (erule otway.induct, force, simp_all add: ex_disj_distrib)
(*Fake, OR3*)
-apply blast+;
+apply blast+
done
--- a/src/HOL/Auth/OtwayRees_Bad.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Sat Aug 17 14:55:08 2002 +0200
@@ -98,15 +98,13 @@
apply (rule_tac [2] otway.Nil
[THEN otway.OR1, THEN otway.Reception,
THEN otway.OR2, THEN otway.Reception,
- THEN otway.OR3, THEN otway.Reception, THEN otway.OR4])
-apply possibility
+ THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility)
done
lemma Gets_imp_Says [dest!]:
"[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs"
apply (erule rev_mp)
-apply (erule otway.induct)
-apply auto
+apply (erule otway.induct, auto)
done
@@ -142,8 +140,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -164,8 +161,7 @@
evs \<in> otway |]
==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)"
apply (erule rev_mp)
-apply (erule otway.induct, simp_all)
-apply blast
+apply (erule otway.induct, simp_all, blast)
done
@@ -190,9 +186,7 @@
apply (erule otway.induct, force)
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
-apply (drule_tac [4] OR2_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz)
done
lemma analz_insert_freshK:
@@ -231,8 +225,7 @@
apply (frule_tac [7] Says_Server_message_form)
apply (drule_tac [6] OR4_analz_knows_Spy)
apply (drule_tac [4] OR2_analz_knows_Spy)
-apply (simp_all add: analz_insert_eq analz_insert_freshK pushes)
-apply spy_analz (*Fake*)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*)
(*OR3, OR4, Oops*)
apply (blast dest: unique_session_keys)+
done
@@ -259,8 +252,7 @@
Says A B {|NA, Agent A, Agent B,
Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+)
done
@@ -279,8 +271,7 @@
Crypt (shrK A) {|NA, Key K|},
Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)"
apply (erule otway.induct, force,
- drule_tac [4] OR2_parts_knows_Spy)
-apply simp_all
+ drule_tac [4] OR2_parts_knows_Spy, simp_all)
(*Fake*)
apply blast
(*OR1: it cannot be a new Nonce, contradiction.*)
--- a/src/HOL/Auth/Recur.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Recur.thy Sat Aug 17 14:55:08 2002 +0200
@@ -122,8 +122,7 @@
END|} \<in> set evs"
apply (intro exI bexI)
apply (rule_tac [2] recur.Nil [THEN recur.RA1,
- THEN recur.RA3 [OF _ _ respond.One]])
-apply possibility
+ THEN recur.RA3 [OF _ _ respond.One]], possibility)
done
@@ -131,8 +130,7 @@
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (cut_tac Nonce_supply2 Key_supply2)
-apply clarify
+apply (cut_tac Nonce_supply2 Key_supply2, clarify)
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
@@ -149,8 +147,7 @@
lemma "\<exists>K. \<exists>NA. \<exists>evs \<in> recur.
Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},
END|} \<in> set evs"
-apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1")
-apply clarify
+apply (tactic "cut_facts_tac [Nonce_supply3, Key_supply3] 1", clarify)
apply (intro exI bexI)
apply (rule_tac [2]
recur.Nil [THEN recur.RA1,
@@ -210,8 +207,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> recur ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule recur.induct)
-apply auto
+apply (erule recur.induct, auto)
(*RA3. It's ugly to call auto twice, but it seems necessary.*)
apply (auto dest: Key_in_parts_respond simp add: parts_insert_spies)
done
@@ -254,9 +250,7 @@
apply (erule recur.induct)
apply (drule_tac [4] RA2_analz_spies,
drule_tac [5] respond_imp_responses,
- drule_tac [6] RA4_analz_spies)
-apply analz_freshK
-apply spy_analz
+ drule_tac [6] RA4_analz_spies, analz_freshK, spy_analz)
(*RA3*)
apply (simp_all add: resp_analz_image_freshK_lemma)
done
@@ -289,8 +283,7 @@
drule_tac [5] respond_imp_responses,
drule_tac [4] RA2_parts_spies)
(*RA3 requires a further induction*)
-apply (erule_tac [5] responses.induct)
-apply simp_all
+apply (erule_tac [5] responses.induct, simp_all)
(*Nil*)
apply force
(*Fake*)
@@ -345,8 +338,7 @@
apply (simp_all del: image_insert
add: analz_image_freshK_simps resp_analz_image_freshK_lemma)
(*Simplification using two distinct treatments of "image"*)
-apply (simp add: parts_insert2)
-apply blast
+apply (simp add: parts_insert2, blast)
done
lemmas resp_analz_insert =
@@ -403,8 +395,7 @@
(*Base case of respond*)
apply blast
(*Inductive step of respond*)
-apply (intro allI conjI impI)
-apply simp_all
+apply (intro allI conjI impI, simp_all)
(*by unicity, either B=Aa or B=A', a contradiction if B \<in> bad*)
apply (blast dest: unique_session_keys [OF _ respond_certificate])
apply (blast dest!: respond_certificate)
@@ -449,8 +440,7 @@
(PB,RB,K) \<in> respond evs |]
==> Hash {|Key (shrK B), M|} \<in> parts H"
apply (erule rev_mp)
-apply (erule respond_imp_responses [THEN responses.induct])
-apply auto
+apply (erule respond_imp_responses [THEN responses.induct], auto)
done
(*Only RA1 or RA2 can have caused such a part of a message to appear.
--- a/src/HOL/Auth/Shared.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Shared.thy Sat Aug 17 14:55:08 2002 +0200
@@ -39,7 +39,7 @@
(*Lets blast_tac perform this step without needing the simplifier*)
lemma invKey_shrK_iff [iff]:
"(Key (invKey K) \<in> X) = (Key K \<in> X)"
-by auto;
+by auto
(*Specialized methods*)
--- a/src/HOL/Auth/TLS.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/TLS.thy Sat Aug 17 14:55:08 2002 +0200
@@ -318,9 +318,7 @@
[THEN tls.ClientHello, THEN tls.ServerHello,
THEN tls.Certificate, THEN tls.ClientKeyExch,
THEN tls.ClientFinished, THEN tls.ServerFinished,
- THEN tls.ClientAccepts])
-apply possibility
-apply blast+
+ THEN tls.ClientAccepts], possibility, blast+)
done
@@ -333,9 +331,7 @@
[THEN tls.ClientHello, THEN tls.ServerHello,
THEN tls.Certificate, THEN tls.ClientKeyExch,
THEN tls.ServerFinished, THEN tls.ClientFinished,
- THEN tls.ServerAccepts])
-apply possibility
-apply blast+
+ THEN tls.ServerAccepts], possibility, blast+)
done
@@ -348,9 +344,7 @@
apply (rule_tac [2] tls.Nil
[THEN tls.ClientHello, THEN tls.ServerHello,
THEN tls.Certificate, THEN tls.ClientKeyExch,
- THEN tls.CertVerify])
-apply possibility
-apply blast+
+ THEN tls.CertVerify], possibility, blast+)
done
@@ -370,9 +364,7 @@
apply (intro exI bexI)
apply (rule_tac [2] tls.ClientHello
[THEN tls.ServerHello,
- THEN tls.ServerResume, THEN tls.ClientResume])
-apply possibility
-apply blast+
+ THEN tls.ServerResume, THEN tls.ClientResume], possibility, blast+)
done
@@ -395,8 +387,7 @@
(*Spy never sees a good agent's private key!*)
lemma Spy_see_priK [simp]:
"evs \<in> tls ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
done
lemma Spy_analz_priK [simp]:
@@ -415,8 +406,7 @@
lemma certificate_valid:
"[| certificate B KB \<in> parts (spies evs); evs \<in> tls |] ==> KB = pubK B"
apply (erule rev_mp)
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
done
lemmas CX_KB_is_pubKB = Says_imp_spies [THEN parts.Inj, THEN certificate_valid]
@@ -467,8 +457,7 @@
evs \<in> tls; A \<notin> bad |]
==> Says A B X \<in> set evs"
apply (erule rev_mp, erule ssubst)
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
done
(*Final version: B checks X using the distributed KA instead of priK A*)
@@ -487,8 +476,7 @@
evs \<in> tls; A \<notin> bad |]
==> Notes A {|Agent B, Nonce PMS|} \<in> set evs"
apply (erule rev_mp)
-apply (erule tls.induct, force, simp_all)
-apply blast
+apply (erule tls.induct, force, simp_all, blast)
done
(*Final version using the distributed KA instead of priK A*)
--- a/src/HOL/Auth/WooLam.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/WooLam.thy Sat Aug 17 14:55:08 2002 +0200
@@ -74,8 +74,7 @@
apply (intro exI bexI)
apply (rule_tac [2] woolam.Nil
[THEN woolam.WL1, THEN woolam.WL2, THEN woolam.WL3,
- THEN woolam.WL4, THEN woolam.WL5])
-apply possibility
+ THEN woolam.WL4, THEN woolam.WL5], possibility)
done
(*Could prove forwarding lemmas for WL4, but we do not need them!*)
@@ -88,8 +87,7 @@
(*Spy never sees a good agent's shared key!*)
lemma Spy_see_shrK [simp]:
"evs \<in> woolam ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
-apply (erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule woolam.induct, force, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -110,8 +108,7 @@
"[| Crypt (shrK A) (Nonce NB) \<in> parts (spies evs);
A \<notin> bad; evs \<in> woolam |]
==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
done
(*Guarantee for Server: if it gets a message containing a certificate from
@@ -133,8 +130,7 @@
evs \<in> woolam |]
==> \<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|}
\<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
done
(*If the encrypted message appears then it originated with the Server!*)
@@ -142,8 +138,7 @@
"[| Crypt (shrK B) {|Agent A, NB|} \<in> parts (spies evs);
B \<notin> bad; evs \<in> woolam |]
==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
done
(*Guarantee for B. If B gets the Server's certificate then A has encrypted
@@ -161,8 +156,7 @@
lemma B_said_WL2:
"[| Says B A (Nonce NB) \<in> set evs; B \<noteq> Spy; evs \<in> woolam |]
==> \<exists>A'. Says A' B (Agent A) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast+
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast+)
done
@@ -171,9 +165,7 @@
==> Crypt (shrK A) (Nonce NB) \<in> parts (spies evs) &
Says B A (Nonce NB) \<in> set evs
--> Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
-apply (erule rev_mp, erule woolam.induct, force, simp_all)
-apply blast
-apply auto
+apply (erule rev_mp, erule woolam.induct, force, simp_all, blast, auto)
oops
end
--- a/src/HOL/Auth/Yahalom.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom.thy Sat Aug 17 14:55:08 2002 +0200
@@ -94,8 +94,7 @@
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4])
-apply possibility
+ THEN yahalom.YM4], possibility)
done
lemma Gets_imp_Says:
@@ -135,8 +134,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule yahalom.induct, force,
- drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -170,8 +168,7 @@
"[| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|}
\<in> set evs; evs \<in> yahalom |]
==> K \<notin> range shrK"
-apply (erule rev_mp, erule yahalom.induct, simp_all)
-apply blast
+apply (erule rev_mp, erule yahalom.induct, simp_all, blast)
done
@@ -197,9 +194,7 @@
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
apply (erule yahalom.induct, force,
- drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+ drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
apply (simp only: Says_Server_not_range analz_image_freshK_simps)
done
@@ -238,8 +233,7 @@
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force,
drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*)
apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
done
@@ -401,8 +395,7 @@
(*Fake*)
apply spy_analz
(*YM4*) (** LEVEL 6 **)
-apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl)
-apply clarify
+apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify)
(*If A \<in> bad then NBa is known, therefore NBa \<noteq> NB. Previous two steps make
the next step faster.*)
apply (blast dest!: Gets_imp_Says Says_imp_spies Crypt_Spy_analz_bad
@@ -423,7 +416,7 @@
(Nonce NB \<in> analz (knows Spy evs))"
by (simp_all del: image_insert image_Un imp_disjL
add: analz_image_freshK_simps split_ifs
- Nonce_secrecy Says_Server_KeyWithNonce);
+ Nonce_secrecy Says_Server_KeyWithNonce)
(*** The Nonce NB uniquely identifies B's message. ***)
@@ -474,8 +467,7 @@
evs \<in> yahalom |]
==> Gets Server {| Agent B, Crypt (shrK B) {|Agent A, na, nb|} |}
\<in> set evs"
-apply (erule rev_mp, erule yahalom.induct)
-apply auto
+apply (erule rev_mp, erule yahalom.induct, auto)
done
--- a/src/HOL/Auth/Yahalom2.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom2.thy Sat Aug 17 14:55:08 2002 +0200
@@ -87,8 +87,7 @@
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4])
-apply possibility
+ THEN yahalom.YM4], possibility)
done
lemma Gets_imp_Says:
@@ -124,8 +123,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule yahalom.induct, force,
- drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -172,9 +170,7 @@
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
- drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+ drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
done
lemma analz_insert_freshK:
@@ -212,8 +208,7 @@
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form,
drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*)
apply (blast dest: unique_session_keys)+ (*YM3, Oops*)
done
--- a/src/HOL/Auth/Yahalom_Bad.thy Fri Aug 16 17:19:43 2002 +0200
+++ b/src/HOL/Auth/Yahalom_Bad.thy Sat Aug 17 14:55:08 2002 +0200
@@ -76,8 +76,7 @@
[THEN yahalom.YM1, THEN yahalom.Reception,
THEN yahalom.YM2, THEN yahalom.Reception,
THEN yahalom.YM3, THEN yahalom.Reception,
- THEN yahalom.YM4])
-apply possibility
+ THEN yahalom.YM4], possibility)
done
lemma Gets_imp_Says:
@@ -113,8 +112,7 @@
lemma Spy_see_shrK [simp]:
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)"
apply (erule yahalom.induct, force,
- drule_tac [6] YM4_parts_knows_Spy, simp_all)
-apply blast+
+ drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+)
done
lemma Spy_analz_shrK [simp]:
@@ -152,9 +150,7 @@
(Key K \<in> analz (Key`KK Un (knows Spy evs))) =
(K \<in> KK | Key K \<in> analz (knows Spy evs))"
apply (erule yahalom.induct, force,
- drule_tac [6] YM4_analz_knows_Spy)
-apply analz_freshK
-apply spy_analz
+ drule_tac [6] YM4_analz_knows_Spy, analz_freshK, spy_analz)
done
lemma analz_insert_freshK: "[| evs \<in> yahalom; KAB \<notin> range shrK |] ==>
@@ -189,8 +185,7 @@
\<in> set evs -->
Key K \<notin> analz (knows Spy evs)"
apply (erule yahalom.induct, force, drule_tac [6] YM4_analz_knows_Spy)
-apply (simp_all add: pushes analz_insert_eq analz_insert_freshK)
-apply spy_analz (*Fake*)
+apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) (*Fake*)
apply (blast dest: unique_session_keys) (*YM3*)
done