--- a/src/HOL/Auth/NS_Shared.ML Tue Nov 18 15:30:50 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Tue Nov 18 16:36:33 1997 +0100
@@ -19,7 +19,7 @@
(*A "possibility property": there are traces that reach the end*)
goal thy
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
-\ ==> EX N K. EX evs: ns_shared. \
+\ ==> EX N K. EX evs: ns_shared. \
\ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
by (REPEAT (resolve_tac [exI,bexI] 1));
by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS
@@ -62,7 +62,7 @@
fun parts_induct_tac i =
etac ns_shared.induct i THEN
forward_tac [Oops_parts_spies] (i+7) THEN
- dtac NS3_msg_in_parts_spies (i+4) THEN
+ forward_tac [NS3_msg_in_parts_spies] (i+4) THEN
prove_simple_subgoals_tac i;
@@ -100,9 +100,9 @@
(*Fake*)
by (best_tac
(claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
- addIs [impOfSubs analz_subset_parts]
- addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
- addss (simpset())) 1);
+ addIs [impOfSubs analz_subset_parts]
+ addDs [impOfSubs (analz_subset_parts RS keysFor_mono)]
+ addss (simpset())) 1);
(*NS2, NS4, NS5*)
by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
qed_spec_mp "new_keys_not_used";
@@ -152,7 +152,7 @@
\ | X : analz (spies evs)";
by (case_tac "A : bad" 1);
by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
- addss (simpset())) 1);
+ addss (simpset())) 1);
by (forward_tac [Says_imp_spies RS parts.Inj] 1);
by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
qed "Says_S_message_form";
@@ -181,12 +181,12 @@
We require that agents should behave like this subsequently also.*)
goal thy
"!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \
-\ (Crypt KAB X) : parts (spies evs) & \
+\ (Crypt KAB X) : parts (spies evs) & \
\ Key K : parts {X} --> Key K : parts (spies evs)";
by (parts_induct_tac 1);
(*Deals with Faked messages*)
by (blast_tac (claset() addSEs partsEs
- addDs [impOfSubs parts_insert_subset_Un]) 1);
+ addDs [impOfSubs parts_insert_subset_Un]) 1);
(*Base, NS4 and NS5*)
by (Auto_tac());
result();
@@ -196,8 +196,8 @@
(*The equality makes the induction hypothesis easier to apply*)
goal thy
- "!!evs. evs : ns_shared ==> \
-\ ALL K KK. KK <= Compl (range shrK) --> \
+ "!!evs. evs : ns_shared ==> \
+\ ALL K KK. KK <= Compl (range shrK) --> \
\ (Key K : analz (Key``KK Un (spies evs))) = \
\ (K : KK | Key K : analz (spies evs))";
by (etac ns_shared.induct 1);
@@ -214,7 +214,7 @@
goal thy
- "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \
+ "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \
\ Key K : analz (insert (Key KAB) (spies evs)) = \
\ (K = KAB | Key K : analz (spies evs))";
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
@@ -225,7 +225,7 @@
goal thy
"!!evs. evs : ns_shared ==> \
-\ EX A' NA' B' X'. ALL A NA B X. \
+\ EX A' NA' B' X'. ALL A NA B X. \
\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
\ --> A=A' & NA=NA' & B=B' & X=X'";
by (etac ns_shared.induct 1);
@@ -237,15 +237,15 @@
(*NS2: it can't be a new key*)
by (expand_case_tac "K = ?y" 1);
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
-by (blast_tac (claset() delrules [conjI] (*prevent split-up into 4 subgoals*)
- addSEs spies_partsEs) 1);
+by (blast_tac (claset() delrules [conjI] (*prevent splitup into 4 subgoals*)
+ addSEs spies_partsEs) 1);
val lemma = result();
(*In messages of this form, the session key uniquely identifies the rest*)
goal thy
- "!!evs. [| Says Server A \
-\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
-\ Says Server A' \
+ "!!evs. [| Says Server A \
+\ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \
+\ Says Server A' \
\ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
\ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
by (prove_unique_tac lemma 1);
@@ -267,14 +267,15 @@
by (ALLGOALS
(asm_simp_tac
(simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @
- pushes @ expand_ifs))));
+ pushes @ expand_ifs))));
(*Oops*)
by (blast_tac (claset() addDs [unique_session_keys]) 5);
(*NS3, replay sub-case*)
by (Blast_tac 4);
(*NS2*)
by (blast_tac (claset() addSEs spies_partsEs
- addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
+ addIs [parts_insertI,
+ impOfSubs analz_subset_parts]) 2);
(*Fake*)
by (spy_analz_tac 1);
(*NS3, Server sub-case*) (**LEVEL 6 **)
@@ -289,9 +290,9 @@
(*Final version: Server's message in the most abstract form*)
goal thy
- "!!evs. [| Says Server A \
-\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
-\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
+ "!!evs. [| Says Server A \
+\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \
+\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \
\ A ~: bad; B ~: bad; evs : ns_shared \
\ |] ==> Key K ~: analz (spies evs)";
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
@@ -306,8 +307,8 @@
(*If the encrypted message appears then it originated with the Server*)
goal thy
- "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
-\ B ~: bad; evs : ns_shared |] \
+ "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
+\ B ~: bad; evs : ns_shared |] \
\ ==> EX NA. Says Server A \
\ (Crypt (shrK A) {|NA, Agent B, Key K, \
\ Crypt (shrK B) {|Key K, Agent A|}|}) \
@@ -337,7 +338,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
(**LEVEL 7**)
by (blast_tac (claset() addSDs [Crypt_Fake_parts_insert]
- addDs [impOfSubs analz_subset_parts]) 1);
+ addDs [impOfSubs analz_subset_parts]) 1);
by (Blast_tac 2);
by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
(*Subgoal 1: contradiction from the assumptions
@@ -349,9 +350,9 @@
by (thin_tac "?PP-->?QQ" 1);
by (case_tac "Ba : bad" 1);
by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3,
- unique_session_keys]) 2);
+ unique_session_keys]) 2);
by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
- Crypt_Spy_analz_bad]) 1);
+ Crypt_Spy_analz_bad]) 1);
val lemma = result();
goal thy
@@ -362,5 +363,5 @@
\ A ~: bad; B ~: bad; evs : ns_shared |] \
\ ==> Says B A (Crypt K (Nonce NB)) : set evs";
by (blast_tac (claset() addSIs [lemma RS mp RS mp RS mp]
- addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
+ addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
qed "A_trusts_NS4";