Ran isatool fixgoal
authorpaulson
Wed Jun 24 11:24:52 1998 +0200 (1998-06-24)
changeset 5076fbc9d95b62ba
parent 5075 9a3d48fa28ca
child 5077 71043526295f
Ran isatool fixgoal
src/HOL/Auth/Event.ML
src/HOL/Auth/Kerberos_BAN.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
     1.1 --- a/src/HOL/Auth/Event.ML	Wed Jun 24 10:33:42 1998 +0200
     1.2 +++ b/src/HOL/Auth/Event.ML	Wed Jun 24 11:24:52 1998 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4  	  read_instantiate_sg (sign_of thy) [("H", "spies evs")]);
     1.5  
     1.6  
     1.7 -goal thy
     1.8 +Goal
     1.9      "P(event_case sf nf ev) = \
    1.10  \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
    1.11  \       (ALL A X. ev = Notes A X --> P(nf A X)))";
    1.12 @@ -30,34 +30,34 @@
    1.13  by Auto_tac;
    1.14  qed "expand_event_case";
    1.15  
    1.16 -goal thy "spies (Says A B X # evs) = insert X (spies evs)";
    1.17 +Goal "spies (Says A B X # evs) = insert X (spies evs)";
    1.18  by (Simp_tac 1);
    1.19  qed "spies_Says";
    1.20  
    1.21  (*The point of letting the Spy see "bad" agents' notes is to prevent
    1.22    redundant case-splits on whether A=Spy and whether A:bad*)
    1.23 -goal thy "spies (Notes A X # evs) = \
    1.24 +Goal "spies (Notes A X # evs) = \
    1.25  \         (if A:bad then insert X (spies evs) else spies evs)";
    1.26  by (Simp_tac 1);
    1.27  qed "spies_Notes";
    1.28  
    1.29 -goal thy "spies evs <= spies (Says A B X # evs)";
    1.30 +Goal "spies evs <= spies (Says A B X # evs)";
    1.31  by (simp_tac (simpset() addsimps [subset_insertI]) 1);
    1.32  qed "spies_subset_spies_Says";
    1.33  
    1.34 -goal thy "spies evs <= spies (Notes A X # evs)";
    1.35 +Goal "spies evs <= spies (Notes A X # evs)";
    1.36  by (Simp_tac 1);
    1.37  by (Fast_tac 1);
    1.38  qed "spies_subset_spies_Notes";
    1.39  
    1.40  (*Spy sees all traffic*)
    1.41 -goal thy "Says A B X : set evs --> X : spies evs";
    1.42 +Goal "Says A B X : set evs --> X : spies evs";
    1.43  by (induct_tac "evs" 1);
    1.44  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    1.45  qed_spec_mp "Says_imp_spies";
    1.46  
    1.47  (*Spy sees Notes of bad agents*)
    1.48 -goal thy "Notes A X : set evs --> A: bad --> X : spies evs";
    1.49 +Goal "Notes A X : set evs --> A: bad --> X : spies evs";
    1.50  by (induct_tac "evs" 1);
    1.51  by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_event_case])));
    1.52  qed_spec_mp "Notes_imp_spies";
    1.53 @@ -74,7 +74,7 @@
    1.54  
    1.55  (*** Fresh nonces ***)
    1.56  
    1.57 -goal thy "parts (spies evs) <= used evs";
    1.58 +Goal "parts (spies evs) <= used evs";
    1.59  by (induct_tac "evs" 1);
    1.60  by (ALLGOALS (asm_simp_tac
    1.61  	      (simpset() addsimps [parts_insert_spies]
    1.62 @@ -85,7 +85,7 @@
    1.63  bind_thm ("usedI", impOfSubs parts_spies_subset_used);
    1.64  AddIs [usedI];
    1.65  
    1.66 -goal thy "parts (initState B) <= used evs";
    1.67 +Goal "parts (initState B) <= used evs";
    1.68  by (induct_tac "evs" 1);
    1.69  by (ALLGOALS (asm_simp_tac
    1.70  	      (simpset() addsimps [parts_insert_spies]
    1.71 @@ -93,17 +93,17 @@
    1.72  by (ALLGOALS Blast_tac);
    1.73  bind_thm ("initState_into_used", impOfSubs (result()));
    1.74  
    1.75 -goal thy "used (Says A B X # evs) = parts{X} Un used evs";
    1.76 +Goal "used (Says A B X # evs) = parts{X} Un used evs";
    1.77  by (Simp_tac 1);
    1.78  qed "used_Says";
    1.79  Addsimps [used_Says];
    1.80  
    1.81 -goal thy "used (Notes A X # evs) = parts{X} Un used evs";
    1.82 +Goal "used (Notes A X # evs) = parts{X} Un used evs";
    1.83  by (Simp_tac 1);
    1.84  qed "used_Notes";
    1.85  Addsimps [used_Notes];
    1.86  
    1.87 -goal thy "used [] <= used evs";
    1.88 +Goal "used [] <= used evs";
    1.89  by (Simp_tac 1);
    1.90  by (blast_tac (claset() addIs [initState_into_used]) 1);
    1.91  qed "used_nil_subset";
    1.92 @@ -113,7 +113,7 @@
    1.93  
    1.94  
    1.95  (*currently unused*)
    1.96 -goal thy "used evs <= used (evs@evs')";
    1.97 +Goal "used evs <= used (evs@evs')";
    1.98  by (induct_tac "evs" 1);
    1.99  by (simp_tac (simpset() addsimps [used_nil_subset]) 1);
   1.100  by (induct_tac "a" 1);
     2.1 --- a/src/HOL/Auth/Kerberos_BAN.ML	Wed Jun 24 10:33:42 1998 +0200
     2.2 +++ b/src/HOL/Auth/Kerberos_BAN.ML	Wed Jun 24 11:24:52 1998 +0200
     2.3 @@ -33,7 +33,7 @@
     2.4  
     2.5  
     2.6  (*A "possibility property": there are traces that reach the end.*)
     2.7 -goal thy 
     2.8 +Goal 
     2.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
    2.10  \        ==> EX Timestamp K. EX evs: kerberos_ban.    \
    2.11  \               Says B A (Crypt K (Number Timestamp)) \
    2.12 @@ -52,7 +52,7 @@
    2.13  (**** Inductive proofs about kerberos_ban ****)
    2.14  
    2.15  (*Nobody sends themselves messages*)
    2.16 -goal thy "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
    2.17 +Goal "!!evs. evs : kerberos_ban ==> ALL A X. Says A A X ~: set evs";
    2.18  by (etac kerberos_ban.induct 1);
    2.19  by Auto_tac;
    2.20  qed_spec_mp "not_Says_to_self";
    2.21 @@ -61,12 +61,12 @@
    2.22  
    2.23  
    2.24  (*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*)
    2.25 -goal thy "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
    2.26 +Goal "!!evs. Says S A (Crypt KA {|Timestamp, B, K, X|}) : set evs \
    2.27  \                ==> X : parts (spies evs)";
    2.28  by (Blast_tac 1);
    2.29  qed "Kb3_msg_in_parts_spies";
    2.30                                
    2.31 -goal thy
    2.32 +Goal
    2.33      "!!evs. Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) : set evs \
    2.34  \           ==> K : parts (spies evs)";
    2.35  by (Blast_tac 1);
    2.36 @@ -81,7 +81,7 @@
    2.37  
    2.38  
    2.39  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    2.40 -goal thy 
    2.41 +Goal 
    2.42  "!!evs. evs : kerberos_ban ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    2.43  by (parts_induct_tac 1);
    2.44  by (ALLGOALS Blast_tac);
    2.45 @@ -89,13 +89,13 @@
    2.46  Addsimps [Spy_see_shrK];
    2.47  
    2.48  
    2.49 -goal thy 
    2.50 +Goal 
    2.51  "!!evs. evs : kerberos_ban ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    2.52  by Auto_tac;
    2.53  qed "Spy_analz_shrK";
    2.54  Addsimps [Spy_analz_shrK];
    2.55  
    2.56 -goal thy  "!!A. [| Key (shrK A) : parts (spies evs);       \
    2.57 +Goal  "!!A. [| Key (shrK A) : parts (spies evs);       \
    2.58  \                  evs : kerberos_ban |] ==> A:bad";
    2.59  by (blast_tac (claset() addDs [Spy_see_shrK]) 1);
    2.60  qed "Spy_see_shrK_D";
    2.61 @@ -105,7 +105,7 @@
    2.62  
    2.63  
    2.64  (*Nobody can have used non-existent keys!*)
    2.65 -goal thy "!!evs. evs : kerberos_ban ==>      \
    2.66 +Goal "!!evs. evs : kerberos_ban ==>      \
    2.67  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    2.68  by (parts_induct_tac 1);
    2.69  (*Fake*)
    2.70 @@ -124,7 +124,7 @@
    2.71  (** Lemmas concerning the form of items passed in messages **)
    2.72  
    2.73  (*Describes the form of K, X and K' when the Server sends this message.*)
    2.74 -goal thy 
    2.75 +Goal 
    2.76   "!!evs. [| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|})  \
    2.77  \           : set evs; evs : kerberos_ban |]                           \
    2.78  \        ==> K ~: range shrK &                                         \
    2.79 @@ -141,7 +141,7 @@
    2.80  
    2.81    This shows implicitly the FRESHNESS OF THE SESSION KEY to A
    2.82  *)
    2.83 -goal thy
    2.84 +Goal
    2.85   "!!evs. [| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} \
    2.86  \             : parts (spies evs);                          \
    2.87  \           A ~: bad;  evs : kerberos_ban |]                \
    2.88 @@ -155,7 +155,7 @@
    2.89  
    2.90  (*If the TICKET appears then it originated with the Server*)
    2.91  (*FRESHNESS OF THE SESSION KEY to B*)
    2.92 -goal thy
    2.93 +Goal
    2.94   "!!evs. [| Crypt (shrK B) {|Number Ts, Agent A, Key K|} : parts (spies evs); \
    2.95  \           B ~: bad;  evs : kerberos_ban |]                        \
    2.96  \         ==> Says Server A                                         \
    2.97 @@ -171,7 +171,7 @@
    2.98  (*EITHER describes the form of X when the following message is sent, 
    2.99    OR     reduces it to the Fake case.
   2.100    Use Says_Server_message_form if applicable.*)
   2.101 -goal thy 
   2.102 +Goal 
   2.103   "!!evs. [| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})     \
   2.104  \              : set evs;                                                  \
   2.105  \           evs : kerberos_ban |]                                          \
   2.106 @@ -206,7 +206,7 @@
   2.107  
   2.108  (** Session keys are not used to encrypt other session keys **)
   2.109  
   2.110 -goal thy  
   2.111 +Goal  
   2.112   "!!evs. evs : kerberos_ban ==>                          \
   2.113  \  ALL K KK. KK <= Compl (range shrK) -->                \
   2.114  \            (Key K : analz (Key``KK Un (spies evs))) =  \
   2.115 @@ -222,7 +222,7 @@
   2.116  qed_spec_mp "analz_image_freshK";
   2.117  
   2.118  
   2.119 -goal thy
   2.120 +Goal
   2.121   "!!evs. [| evs : kerberos_ban;  KAB ~: range shrK |] ==>     \
   2.122  \        Key K : analz (insert (Key KAB) (spies evs)) =       \
   2.123  \        (K = KAB | Key K : analz (spies evs))";
   2.124 @@ -232,7 +232,7 @@
   2.125  
   2.126  (** The session key K uniquely identifies the message **)
   2.127  
   2.128 -goal thy 
   2.129 +Goal 
   2.130   "!!evs. evs : kerberos_ban ==>                                         \
   2.131  \      EX A' Ts' B' X'. ALL A Ts B X.                                   \
   2.132  \       Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   2.133 @@ -248,7 +248,7 @@
   2.134  val lemma = result();
   2.135  
   2.136  (*In messages of this form, the session key uniquely identifies the rest*)
   2.137 -goal thy 
   2.138 +Goal 
   2.139   "!!evs. [| Says Server A                                    \
   2.140  \             (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) : set evs; \ 
   2.141  \           Says Server A'                                   \
   2.142 @@ -262,7 +262,7 @@
   2.143      if the spy could see it!
   2.144  **)
   2.145  
   2.146 -goal thy 
   2.147 +Goal 
   2.148   "!!evs. [| A ~: bad;  B ~: bad;  evs : kerberos_ban |]           \
   2.149  \    ==> Says Server A                                            \
   2.150  \            (Crypt (shrK A) {|Number Ts, Agent B, Key K,         \
   2.151 @@ -294,7 +294,7 @@
   2.152                       Spy does not see the keys sent in msg Kb2 
   2.153                       as long as they have NOT EXPIRED
   2.154  **)
   2.155 -goal thy 
   2.156 +Goal 
   2.157   "!!evs. [| Says Server A                                           \
   2.158  \            (Crypt K' {|Number T, Agent B, Key K, X|}) : set evs;  \
   2.159  \           ~ Expired T evs;                                        \
   2.160 @@ -312,7 +312,7 @@
   2.161  
   2.162  (** CONFIDENTIALITY for ALICE: **)
   2.163  (** Also A_trusts_K_by_Kb2 RS Confidentiality_S **)
   2.164 -goal thy 
   2.165 +Goal 
   2.166  "!!evs. [| Crypt (shrK A) {|Number T, Agent B, Key K, X|} : parts (spies evs);\
   2.167  \           ~ Expired T evs;          \
   2.168  \           A ~: bad;  B ~: bad;  evs : kerberos_ban                \
   2.169 @@ -323,7 +323,7 @@
   2.170  
   2.171  (** CONFIDENTIALITY for BOB: **)
   2.172  (** Also B_trusts_K_by_Kb3 RS Confidentiality_S **)
   2.173 -goal thy
   2.174 +Goal
   2.175  "!!evs. [| Crypt (shrK B) {|Number Tk, Agent A, Key K|} \
   2.176  \            : parts (spies evs);              \
   2.177  \          ~ Expired Tk evs;          \
   2.178 @@ -334,7 +334,7 @@
   2.179  qed "Confidentiality_B";
   2.180  
   2.181  
   2.182 -goal thy
   2.183 +Goal
   2.184   "!!evs. [| B ~: bad;  evs : kerberos_ban |]                        \
   2.185  \        ==> Key K ~: analz (spies evs) -->                    \
   2.186  \            Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \
   2.187 @@ -367,7 +367,7 @@
   2.188  
   2.189  
   2.190  (*AUTHENTICATION OF B TO A*)
   2.191 -goal thy
   2.192 +Goal
   2.193   "!!evs. [| Crypt K (Number Ta) : parts (spies evs);           \
   2.194  \           Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}    \
   2.195  \           : parts (spies evs);                               \
   2.196 @@ -380,7 +380,7 @@
   2.197  qed "Authentication_B";
   2.198  
   2.199  
   2.200 -goal thy
   2.201 +Goal
   2.202   "!!evs. [| A ~: bad; B ~: bad; evs : kerberos_ban |]      ==>         \ 
   2.203  \           Key K ~: analz (spies evs) -->         \
   2.204  \           Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|})  \
   2.205 @@ -404,7 +404,7 @@
   2.206  
   2.207  
   2.208  (*AUTHENTICATION OF A TO B*)
   2.209 -goal thy
   2.210 +Goal
   2.211   "!!evs. [| Crypt K {|Agent A, Number Ta|} : parts (spies evs);  \
   2.212  \           Crypt (shrK B) {|Number Ts, Agent A, Key K|}         \
   2.213  \           : parts (spies evs);                                 \
     3.1 --- a/src/HOL/Auth/Message.ML	Wed Jun 24 10:33:42 1998 +0200
     3.2 +++ b/src/HOL/Auth/Message.ML	Wed Jun 24 11:24:52 1998 +0200
     3.3 @@ -19,15 +19,15 @@
     3.4  AddIffs msg.inject;
     3.5  
     3.6  (*Equations hold because constructors are injective; cannot prove for all f*)
     3.7 -goal thy "(Friend x : Friend``A) = (x:A)";
     3.8 +Goal "(Friend x : Friend``A) = (x:A)";
     3.9  by Auto_tac;
    3.10  qed "Friend_image_eq";
    3.11  
    3.12 -goal thy "(Key x : Key``A) = (x:A)";
    3.13 +Goal "(Key x : Key``A) = (x:A)";
    3.14  by Auto_tac;
    3.15  qed "Key_image_eq";
    3.16  
    3.17 -goal thy "(Nonce x ~: Key``A)";
    3.18 +Goal "(Nonce x ~: Key``A)";
    3.19  by Auto_tac;
    3.20  qed "Nonce_Key_image_eq";
    3.21  Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    3.22 @@ -35,7 +35,7 @@
    3.23  
    3.24  (** Inverse of keys **)
    3.25  
    3.26 -goal thy "!!K K'. (invKey K = invKey K') = (K=K')";
    3.27 +Goal "!!K K'. (invKey K = invKey K') = (K=K')";
    3.28  by Safe_tac;
    3.29  by (rtac box_equals 1);
    3.30  by (REPEAT (rtac invKey 2));
    3.31 @@ -47,48 +47,48 @@
    3.32  
    3.33  (**** keysFor operator ****)
    3.34  
    3.35 -goalw thy [keysFor_def] "keysFor {} = {}";
    3.36 +Goalw [keysFor_def] "keysFor {} = {}";
    3.37  by (Blast_tac 1);
    3.38  qed "keysFor_empty";
    3.39  
    3.40 -goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    3.41 +Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    3.42  by (Blast_tac 1);
    3.43  qed "keysFor_Un";
    3.44  
    3.45 -goalw thy [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
    3.46 +Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))";
    3.47  by (Blast_tac 1);
    3.48  qed "keysFor_UN";
    3.49  
    3.50  (*Monotonicity*)
    3.51 -goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    3.52 +Goalw [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    3.53  by (Blast_tac 1);
    3.54  qed "keysFor_mono";
    3.55  
    3.56 -goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    3.57 +Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    3.58  by (Blast_tac 1);
    3.59  qed "keysFor_insert_Agent";
    3.60  
    3.61 -goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    3.62 +Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
    3.63  by (Blast_tac 1);
    3.64  qed "keysFor_insert_Nonce";
    3.65  
    3.66 -goalw thy [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    3.67 +Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    3.68  by (Blast_tac 1);
    3.69  qed "keysFor_insert_Number";
    3.70  
    3.71 -goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    3.72 +Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    3.73  by (Blast_tac 1);
    3.74  qed "keysFor_insert_Key";
    3.75  
    3.76 -goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    3.77 +Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    3.78  by (Blast_tac 1);
    3.79  qed "keysFor_insert_Hash";
    3.80  
    3.81 -goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    3.82 +Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    3.83  by (Blast_tac 1);
    3.84  qed "keysFor_insert_MPair";
    3.85  
    3.86 -goalw thy [keysFor_def]
    3.87 +Goalw [keysFor_def]
    3.88      "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    3.89  by Auto_tac;
    3.90  qed "keysFor_insert_Crypt";
    3.91 @@ -100,12 +100,12 @@
    3.92  AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
    3.93  	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
    3.94  
    3.95 -goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    3.96 +Goalw [keysFor_def] "keysFor (Key``E) = {}";
    3.97  by Auto_tac;
    3.98  qed "keysFor_image_Key";
    3.99  Addsimps [keysFor_image_Key];
   3.100  
   3.101 -goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
   3.102 +Goalw [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
   3.103  by (Blast_tac 1);
   3.104  qed "Crypt_imp_invKey_keysFor";
   3.105  
   3.106 @@ -113,7 +113,7 @@
   3.107  (**** Inductive relation "parts" ****)
   3.108  
   3.109  val major::prems = 
   3.110 -goal thy "[| {|X,Y|} : parts H;       \
   3.111 +Goal "[| {|X,Y|} : parts H;       \
   3.112  \            [| X : parts H; Y : parts H |] ==> P  \
   3.113  \         |] ==> P";
   3.114  by (cut_facts_tac [major] 1);
   3.115 @@ -130,32 +130,32 @@
   3.116       compound message.  They work well on THIS FILE, perhaps because its
   3.117       proofs concern only atomic messages.*)
   3.118  
   3.119 -goal thy "H <= parts(H)";
   3.120 +Goal "H <= parts(H)";
   3.121  by (Blast_tac 1);
   3.122  qed "parts_increasing";
   3.123  
   3.124  (*Monotonicity*)
   3.125 -goalw thy parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
   3.126 +Goalw parts.defs "!!G H. G<=H ==> parts(G) <= parts(H)";
   3.127  by (rtac lfp_mono 1);
   3.128  by (REPEAT (ares_tac basic_monos 1));
   3.129  qed "parts_mono";
   3.130  
   3.131  val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
   3.132  
   3.133 -goal thy "parts{} = {}";
   3.134 +Goal "parts{} = {}";
   3.135  by Safe_tac;
   3.136  by (etac parts.induct 1);
   3.137  by (ALLGOALS Blast_tac);
   3.138  qed "parts_empty";
   3.139  Addsimps [parts_empty];
   3.140  
   3.141 -goal thy "!!X. X: parts{} ==> P";
   3.142 +Goal "!!X. X: parts{} ==> P";
   3.143  by (Asm_full_simp_tac 1);
   3.144  qed "parts_emptyE";
   3.145  AddSEs [parts_emptyE];
   3.146  
   3.147  (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
   3.148 -goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
   3.149 +Goal "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
   3.150  by (etac parts.induct 1);
   3.151  by (ALLGOALS Blast_tac);
   3.152  qed "parts_singleton";
   3.153 @@ -163,43 +163,43 @@
   3.154  
   3.155  (** Unions **)
   3.156  
   3.157 -goal thy "parts(G) Un parts(H) <= parts(G Un H)";
   3.158 +Goal "parts(G) Un parts(H) <= parts(G Un H)";
   3.159  by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1));
   3.160  val parts_Un_subset1 = result();
   3.161  
   3.162 -goal thy "parts(G Un H) <= parts(G) Un parts(H)";
   3.163 +Goal "parts(G Un H) <= parts(G) Un parts(H)";
   3.164  by (rtac subsetI 1);
   3.165  by (etac parts.induct 1);
   3.166  by (ALLGOALS Blast_tac);
   3.167  val parts_Un_subset2 = result();
   3.168  
   3.169 -goal thy "parts(G Un H) = parts(G) Un parts(H)";
   3.170 +Goal "parts(G Un H) = parts(G) Un parts(H)";
   3.171  by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1));
   3.172  qed "parts_Un";
   3.173  
   3.174 -goal thy "parts (insert X H) = parts {X} Un parts H";
   3.175 +Goal "parts (insert X H) = parts {X} Un parts H";
   3.176  by (stac (read_instantiate [("A","H")] insert_is_Un) 1);
   3.177  by (simp_tac (HOL_ss addsimps [parts_Un]) 1);
   3.178  qed "parts_insert";
   3.179  
   3.180  (*TWO inserts to avoid looping.  This rewrite is better than nothing.
   3.181    Not suitable for Addsimps: its behaviour can be strange.*)
   3.182 -goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
   3.183 +Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H";
   3.184  by (simp_tac (simpset() addsimps [Un_assoc]) 1);
   3.185  by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1);
   3.186  qed "parts_insert2";
   3.187  
   3.188 -goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
   3.189 +Goal "(UN x:A. parts(H x)) <= parts(UN x:A. H x)";
   3.190  by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1));
   3.191  val parts_UN_subset1 = result();
   3.192  
   3.193 -goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
   3.194 +Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
   3.195  by (rtac subsetI 1);
   3.196  by (etac parts.induct 1);
   3.197  by (ALLGOALS Blast_tac);
   3.198  val parts_UN_subset2 = result();
   3.199  
   3.200 -goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
   3.201 +Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))";
   3.202  by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1));
   3.203  qed "parts_UN";
   3.204  
   3.205 @@ -209,36 +209,36 @@
   3.206  AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE,
   3.207  	parts_UN RS equalityD1 RS subsetD RS UN_E];
   3.208  
   3.209 -goal thy "insert X (parts H) <= parts(insert X H)";
   3.210 +Goal "insert X (parts H) <= parts(insert X H)";
   3.211  by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1);
   3.212  qed "parts_insert_subset";
   3.213  
   3.214  (** Idempotence and transitivity **)
   3.215  
   3.216 -goal thy "!!H. X: parts (parts H) ==> X: parts H";
   3.217 +Goal "!!H. X: parts (parts H) ==> X: parts H";
   3.218  by (etac parts.induct 1);
   3.219  by (ALLGOALS Blast_tac);
   3.220  qed "parts_partsD";
   3.221  AddSDs [parts_partsD];
   3.222  
   3.223 -goal thy "parts (parts H) = parts H";
   3.224 +Goal "parts (parts H) = parts H";
   3.225  by (Blast_tac 1);
   3.226  qed "parts_idem";
   3.227  Addsimps [parts_idem];
   3.228  
   3.229 -goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
   3.230 +Goal "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
   3.231  by (dtac parts_mono 1);
   3.232  by (Blast_tac 1);
   3.233  qed "parts_trans";
   3.234  
   3.235  (*Cut*)
   3.236 -goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
   3.237 +Goal "!!H. [| Y: parts (insert X G);  X: parts H |] \
   3.238  \              ==> Y: parts (G Un H)";
   3.239  by (etac parts_trans 1);
   3.240  by Auto_tac;
   3.241  qed "parts_cut";
   3.242  
   3.243 -goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
   3.244 +Goal "!!H. X: parts H ==> parts (insert X H) = parts H";
   3.245  by (fast_tac (claset() addSDs [parts_cut]
   3.246                         addIs  [parts_insertI] 
   3.247                         addss (simpset())) 1);
   3.248 @@ -254,27 +254,27 @@
   3.249           etac parts.induct i,
   3.250           REPEAT (Blast_tac i)];
   3.251  
   3.252 -goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   3.253 +Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
   3.254  by (parts_tac 1);
   3.255  qed "parts_insert_Agent";
   3.256  
   3.257 -goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   3.258 +Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
   3.259  by (parts_tac 1);
   3.260  qed "parts_insert_Nonce";
   3.261  
   3.262 -goal thy "parts (insert (Number N) H) = insert (Number N) (parts H)";
   3.263 +Goal "parts (insert (Number N) H) = insert (Number N) (parts H)";
   3.264  by (parts_tac 1);
   3.265  qed "parts_insert_Number";
   3.266  
   3.267 -goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
   3.268 +Goal "parts (insert (Key K) H) = insert (Key K) (parts H)";
   3.269  by (parts_tac 1);
   3.270  qed "parts_insert_Key";
   3.271  
   3.272 -goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
   3.273 +Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
   3.274  by (parts_tac 1);
   3.275  qed "parts_insert_Hash";
   3.276  
   3.277 -goal thy "parts (insert (Crypt K X) H) = \
   3.278 +Goal "parts (insert (Crypt K X) H) = \
   3.279  \         insert (Crypt K X) (parts (insert X H))";
   3.280  by (rtac equalityI 1);
   3.281  by (rtac subsetI 1);
   3.282 @@ -284,7 +284,7 @@
   3.283  by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
   3.284  qed "parts_insert_Crypt";
   3.285  
   3.286 -goal thy "parts (insert {|X,Y|} H) = \
   3.287 +Goal "parts (insert {|X,Y|} H) = \
   3.288  \         insert {|X,Y|} (parts (insert X (insert Y H)))";
   3.289  by (rtac equalityI 1);
   3.290  by (rtac subsetI 1);
   3.291 @@ -299,7 +299,7 @@
   3.292            parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
   3.293  
   3.294  
   3.295 -goal thy "parts (Key``N) = Key``N";
   3.296 +Goal "parts (Key``N) = Key``N";
   3.297  by Auto_tac;
   3.298  by (etac parts.induct 1);
   3.299  by Auto_tac;
   3.300 @@ -308,7 +308,7 @@
   3.301  
   3.302  
   3.303  (*In any message, there is an upper bound N on its greatest nonce.*)
   3.304 -goal thy "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
   3.305 +Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
   3.306  by (induct_tac "msg" 1);
   3.307  by (induct_tac "atomic" 1);
   3.308  by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2])));
   3.309 @@ -323,7 +323,7 @@
   3.310  (**** Inductive relation "analz" ****)
   3.311  
   3.312  val major::prems = 
   3.313 -goal thy "[| {|X,Y|} : analz H;       \
   3.314 +Goal "[| {|X,Y|} : analz H;       \
   3.315  \            [| X : analz H; Y : analz H |] ==> P  \
   3.316  \         |] ==> P";
   3.317  by (cut_facts_tac [major] 1);
   3.318 @@ -337,11 +337,11 @@
   3.319  
   3.320  Addsimps [analz.Inj];
   3.321  
   3.322 -goal thy "H <= analz(H)";
   3.323 +Goal "H <= analz(H)";
   3.324  by (Blast_tac 1);
   3.325  qed "analz_increasing";
   3.326  
   3.327 -goal thy "analz H <= parts H";
   3.328 +Goal "analz H <= parts H";
   3.329  by (rtac subsetI 1);
   3.330  by (etac analz.induct 1);
   3.331  by (ALLGOALS Blast_tac);
   3.332 @@ -350,7 +350,7 @@
   3.333  bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
   3.334  
   3.335  
   3.336 -goal thy "parts (analz H) = parts H";
   3.337 +Goal "parts (analz H) = parts H";
   3.338  by (rtac equalityI 1);
   3.339  by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
   3.340  by (Simp_tac 1);
   3.341 @@ -358,7 +358,7 @@
   3.342  qed "parts_analz";
   3.343  Addsimps [parts_analz];
   3.344  
   3.345 -goal thy "analz (parts H) = parts H";
   3.346 +Goal "analz (parts H) = parts H";
   3.347  by Auto_tac;
   3.348  by (etac analz.induct 1);
   3.349  by Auto_tac;
   3.350 @@ -366,7 +366,7 @@
   3.351  Addsimps [analz_parts];
   3.352  
   3.353  (*Monotonicity; Lemma 1 of Lowe*)
   3.354 -goalw thy analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
   3.355 +Goalw analz.defs "!!G H. G<=H ==> analz(G) <= analz(H)";
   3.356  by (rtac lfp_mono 1);
   3.357  by (REPEAT (ares_tac basic_monos 1));
   3.358  qed "analz_mono";
   3.359 @@ -375,7 +375,7 @@
   3.360  
   3.361  (** General equational properties **)
   3.362  
   3.363 -goal thy "analz{} = {}";
   3.364 +Goal "analz{} = {}";
   3.365  by Safe_tac;
   3.366  by (etac analz.induct 1);
   3.367  by (ALLGOALS Blast_tac);
   3.368 @@ -384,11 +384,11 @@
   3.369  
   3.370  (*Converse fails: we can analz more from the union than from the 
   3.371    separate parts, as a key in one might decrypt a message in the other*)
   3.372 -goal thy "analz(G) Un analz(H) <= analz(G Un H)";
   3.373 +Goal "analz(G) Un analz(H) <= analz(G Un H)";
   3.374  by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1));
   3.375  qed "analz_Un";
   3.376  
   3.377 -goal thy "insert X (analz H) <= analz(insert X H)";
   3.378 +Goal "insert X (analz H) <= analz(insert X H)";
   3.379  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   3.380  qed "analz_insert";
   3.381  
   3.382 @@ -399,30 +399,30 @@
   3.383           etac analz.induct i,
   3.384           REPEAT (Blast_tac i)];
   3.385  
   3.386 -goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   3.387 +Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   3.388  by (analz_tac 1);
   3.389  qed "analz_insert_Agent";
   3.390  
   3.391 -goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   3.392 +Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   3.393  by (analz_tac 1);
   3.394  qed "analz_insert_Nonce";
   3.395  
   3.396 -goal thy "analz (insert (Number N) H) = insert (Number N) (analz H)";
   3.397 +Goal "analz (insert (Number N) H) = insert (Number N) (analz H)";
   3.398  by (analz_tac 1);
   3.399  qed "analz_insert_Number";
   3.400  
   3.401 -goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
   3.402 +Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
   3.403  by (analz_tac 1);
   3.404  qed "analz_insert_Hash";
   3.405  
   3.406  (*Can only pull out Keys if they are not needed to decrypt the rest*)
   3.407 -goalw thy [keysFor_def]
   3.408 +Goalw [keysFor_def]
   3.409      "!!K. K ~: keysFor (analz H) ==>  \
   3.410  \         analz (insert (Key K) H) = insert (Key K) (analz H)";
   3.411  by (analz_tac 1);
   3.412  qed "analz_insert_Key";
   3.413  
   3.414 -goal thy "analz (insert {|X,Y|} H) = \
   3.415 +Goal "analz (insert {|X,Y|} H) = \
   3.416  \         insert {|X,Y|} (analz (insert X (insert Y H)))";
   3.417  by (rtac equalityI 1);
   3.418  by (rtac subsetI 1);
   3.419 @@ -433,13 +433,13 @@
   3.420  qed "analz_insert_MPair";
   3.421  
   3.422  (*Can pull out enCrypted message if the Key is not known*)
   3.423 -goal thy "!!H. Key (invKey K) ~: analz H ==>  \
   3.424 +Goal "!!H. Key (invKey K) ~: analz H ==>  \
   3.425  \              analz (insert (Crypt K X) H) = \
   3.426  \              insert (Crypt K X) (analz H)";
   3.427  by (analz_tac 1);
   3.428  qed "analz_insert_Crypt";
   3.429  
   3.430 -goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.431 +Goal "!!H. Key (invKey K) : analz H ==>  \
   3.432  \              analz (insert (Crypt K X) H) <= \
   3.433  \              insert (Crypt K X) (analz (insert X H))";
   3.434  by (rtac subsetI 1);
   3.435 @@ -447,7 +447,7 @@
   3.436  by (ALLGOALS (Blast_tac));
   3.437  val lemma1 = result();
   3.438  
   3.439 -goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.440 +Goal "!!H. Key (invKey K) : analz H ==>  \
   3.441  \              insert (Crypt K X) (analz (insert X H)) <= \
   3.442  \              analz (insert (Crypt K X) H)";
   3.443  by Auto_tac;
   3.444 @@ -456,7 +456,7 @@
   3.445  by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
   3.446  val lemma2 = result();
   3.447  
   3.448 -goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.449 +Goal "!!H. Key (invKey K) : analz H ==>  \
   3.450  \              analz (insert (Crypt K X) H) = \
   3.451  \              insert (Crypt K X) (analz (insert X H))";
   3.452  by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1));
   3.453 @@ -466,7 +466,7 @@
   3.454    Effective, but can cause subgoals to blow up!
   3.455    Use with split_if;  apparently split_tac does not cope with patterns
   3.456    such as "analz (insert (Crypt K X) H)" *)
   3.457 -goal thy "analz (insert (Crypt K X) H) =                \
   3.458 +Goal "analz (insert (Crypt K X) H) =                \
   3.459  \         (if (Key (invKey K) : analz H)                \
   3.460  \          then insert (Crypt K X) (analz (insert X H)) \
   3.461  \          else insert (Crypt K X) (analz H))";
   3.462 @@ -480,7 +480,7 @@
   3.463            analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   3.464  
   3.465  (*This rule supposes "for the sake of argument" that we have the key.*)
   3.466 -goal thy  "analz (insert (Crypt K X) H) <=  \
   3.467 +Goal  "analz (insert (Crypt K X) H) <=  \
   3.468  \          insert (Crypt K X) (analz (insert X H))";
   3.469  by (rtac subsetI 1);
   3.470  by (etac analz.induct 1);
   3.471 @@ -488,7 +488,7 @@
   3.472  qed "analz_insert_Crypt_subset";
   3.473  
   3.474  
   3.475 -goal thy "analz (Key``N) = Key``N";
   3.476 +Goal "analz (Key``N) = Key``N";
   3.477  by Auto_tac;
   3.478  by (etac analz.induct 1);
   3.479  by Auto_tac;
   3.480 @@ -499,24 +499,24 @@
   3.481  
   3.482  (** Idempotence and transitivity **)
   3.483  
   3.484 -goal thy "!!H. X: analz (analz H) ==> X: analz H";
   3.485 +Goal "!!H. X: analz (analz H) ==> X: analz H";
   3.486  by (etac analz.induct 1);
   3.487  by (ALLGOALS Blast_tac);
   3.488  qed "analz_analzD";
   3.489  AddSDs [analz_analzD];
   3.490  
   3.491 -goal thy "analz (analz H) = analz H";
   3.492 +Goal "analz (analz H) = analz H";
   3.493  by (Blast_tac 1);
   3.494  qed "analz_idem";
   3.495  Addsimps [analz_idem];
   3.496  
   3.497 -goal thy "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
   3.498 +Goal "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
   3.499  by (dtac analz_mono 1);
   3.500  by (Blast_tac 1);
   3.501  qed "analz_trans";
   3.502  
   3.503  (*Cut; Lemma 2 of Lowe*)
   3.504 -goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
   3.505 +Goal "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
   3.506  by (etac analz_trans 1);
   3.507  by (Blast_tac 1);
   3.508  qed "analz_cut";
   3.509 @@ -528,34 +528,34 @@
   3.510  (*This rewrite rule helps in the simplification of messages that involve
   3.511    the forwarding of unknown components (X).  Without it, removing occurrences
   3.512    of X can be very complicated. *)
   3.513 -goal thy "!!H. X: analz H ==> analz (insert X H) = analz H";
   3.514 +Goal "!!H. X: analz H ==> analz (insert X H) = analz H";
   3.515  by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1);
   3.516  qed "analz_insert_eq";
   3.517  
   3.518  
   3.519  (** A congruence rule for "analz" **)
   3.520  
   3.521 -goal thy "!!H. [| analz G <= analz G'; analz H <= analz H' \
   3.522 +Goal "!!H. [| analz G <= analz G'; analz H <= analz H' \
   3.523  \              |] ==> analz (G Un H) <= analz (G' Un H')";
   3.524  by (Clarify_tac 1);
   3.525  by (etac analz.induct 1);
   3.526  by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD])));
   3.527  qed "analz_subset_cong";
   3.528  
   3.529 -goal thy "!!H. [| analz G = analz G'; analz H = analz H' \
   3.530 +Goal "!!H. [| analz G = analz G'; analz H = analz H' \
   3.531  \              |] ==> analz (G Un H) = analz (G' Un H')";
   3.532  by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong]
   3.533            ORELSE' etac equalityE));
   3.534  qed "analz_cong";
   3.535  
   3.536  
   3.537 -goal thy "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   3.538 +Goal "!!H. analz H = analz H' ==> analz(insert X H) = analz(insert X H')";
   3.539  by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv]
   3.540                              setloop (rtac analz_cong)) 1);
   3.541  qed "analz_insert_cong";
   3.542  
   3.543  (*If there are no pairs or encryptions then analz does nothing*)
   3.544 -goal thy "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
   3.545 +Goal "!!H. [| ALL X Y. {|X,Y|} ~: H;  ALL X K. Crypt K X ~: H |] ==> \
   3.546  \         analz H = H";
   3.547  by Safe_tac;
   3.548  by (etac analz.induct 1);
   3.549 @@ -563,12 +563,12 @@
   3.550  qed "analz_trivial";
   3.551  
   3.552  (*These two are obsolete (with a single Spy) but cost little to prove...*)
   3.553 -goal thy "!!X. X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
   3.554 +Goal "!!X. X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)";
   3.555  by (etac analz.induct 1);
   3.556  by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono])));
   3.557  val lemma = result();
   3.558  
   3.559 -goal thy "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
   3.560 +Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)";
   3.561  by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1);
   3.562  qed "analz_UN_analz";
   3.563  Addsimps [analz_UN_analz];
   3.564 @@ -591,12 +591,12 @@
   3.565  
   3.566  AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
   3.567  
   3.568 -goal thy "H <= synth(H)";
   3.569 +Goal "H <= synth(H)";
   3.570  by (Blast_tac 1);
   3.571  qed "synth_increasing";
   3.572  
   3.573  (*Monotonicity*)
   3.574 -goalw thy synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
   3.575 +Goalw synth.defs "!!G H. G<=H ==> synth(G) <= synth(H)";
   3.576  by (rtac lfp_mono 1);
   3.577  by (REPEAT (ares_tac basic_monos 1));
   3.578  qed "synth_mono";
   3.579 @@ -605,54 +605,54 @@
   3.580  
   3.581  (*Converse fails: we can synth more from the union than from the 
   3.582    separate parts, building a compound message using elements of each.*)
   3.583 -goal thy "synth(G) Un synth(H) <= synth(G Un H)";
   3.584 +Goal "synth(G) Un synth(H) <= synth(G Un H)";
   3.585  by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1));
   3.586  qed "synth_Un";
   3.587  
   3.588 -goal thy "insert X (synth H) <= synth(insert X H)";
   3.589 +Goal "insert X (synth H) <= synth(insert X H)";
   3.590  by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1);
   3.591  qed "synth_insert";
   3.592  
   3.593  (** Idempotence and transitivity **)
   3.594  
   3.595 -goal thy "!!H. X: synth (synth H) ==> X: synth H";
   3.596 +Goal "!!H. X: synth (synth H) ==> X: synth H";
   3.597  by (etac synth.induct 1);
   3.598  by (ALLGOALS Blast_tac);
   3.599  qed "synth_synthD";
   3.600  AddSDs [synth_synthD];
   3.601  
   3.602 -goal thy "synth (synth H) = synth H";
   3.603 +Goal "synth (synth H) = synth H";
   3.604  by (Blast_tac 1);
   3.605  qed "synth_idem";
   3.606  
   3.607 -goal thy "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
   3.608 +Goal "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
   3.609  by (dtac synth_mono 1);
   3.610  by (Blast_tac 1);
   3.611  qed "synth_trans";
   3.612  
   3.613  (*Cut; Lemma 2 of Lowe*)
   3.614 -goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
   3.615 +Goal "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
   3.616  by (etac synth_trans 1);
   3.617  by (Blast_tac 1);
   3.618  qed "synth_cut";
   3.619  
   3.620 -goal thy "Agent A : synth H";
   3.621 +Goal "Agent A : synth H";
   3.622  by (Blast_tac 1);
   3.623  qed "Agent_synth";
   3.624  
   3.625 -goal thy "Number n : synth H";
   3.626 +Goal "Number n : synth H";
   3.627  by (Blast_tac 1);
   3.628  qed "Number_synth";
   3.629  
   3.630 -goal thy "(Nonce N : synth H) = (Nonce N : H)";
   3.631 +Goal "(Nonce N : synth H) = (Nonce N : H)";
   3.632  by (Blast_tac 1);
   3.633  qed "Nonce_synth_eq";
   3.634  
   3.635 -goal thy "(Key K : synth H) = (Key K : H)";
   3.636 +Goal "(Key K : synth H) = (Key K : H)";
   3.637  by (Blast_tac 1);
   3.638  qed "Key_synth_eq";
   3.639  
   3.640 -goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
   3.641 +Goal "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
   3.642  by (Blast_tac 1);
   3.643  qed "Crypt_synth_eq";
   3.644  
   3.645 @@ -660,7 +660,7 @@
   3.646  	  Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   3.647  
   3.648  
   3.649 -goalw thy [keysFor_def]
   3.650 +Goalw [keysFor_def]
   3.651      "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
   3.652  by (Blast_tac 1);
   3.653  qed "keysFor_synth";
   3.654 @@ -669,7 +669,7 @@
   3.655  
   3.656  (*** Combinations of parts, analz and synth ***)
   3.657  
   3.658 -goal thy "parts (synth H) = parts H Un synth H";
   3.659 +Goal "parts (synth H) = parts H Un synth H";
   3.660  by (rtac equalityI 1);
   3.661  by (rtac subsetI 1);
   3.662  by (etac parts.induct 1);
   3.663 @@ -679,12 +679,12 @@
   3.664  qed "parts_synth";
   3.665  Addsimps [parts_synth];
   3.666  
   3.667 -goal thy "analz (analz G Un H) = analz (G Un H)";
   3.668 +Goal "analz (analz G Un H) = analz (G Un H)";
   3.669  by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
   3.670  by (ALLGOALS Simp_tac);
   3.671  qed "analz_analz_Un";
   3.672  
   3.673 -goal thy "analz (synth G Un H) = analz (G Un H) Un synth G";
   3.674 +Goal "analz (synth G Un H) = analz (G Un H) Un synth G";
   3.675  by (rtac equalityI 1);
   3.676  by (rtac subsetI 1);
   3.677  by (etac analz.induct 1);
   3.678 @@ -692,7 +692,7 @@
   3.679  by (ALLGOALS (blast_tac (claset() addIs analz.intrs)));
   3.680  qed "analz_synth_Un";
   3.681  
   3.682 -goal thy "analz (synth H) = analz H Un synth H";
   3.683 +Goal "analz (synth H) = analz H Un synth H";
   3.684  by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
   3.685  by (Full_simp_tac 1);
   3.686  qed "analz_synth";
   3.687 @@ -701,14 +701,14 @@
   3.688  
   3.689  (** For reasoning about the Fake rule in traces **)
   3.690  
   3.691 -goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   3.692 +Goal "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   3.693  by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
   3.694  by (Blast_tac 1);
   3.695  qed "parts_insert_subset_Un";
   3.696  
   3.697  (*More specifically for Fake.  Very occasionally we could do with a version
   3.698    of the form  parts{X} <= synth (analz H) Un parts H *)
   3.699 -goal thy "!!H. X: synth (analz H) ==> \
   3.700 +Goal "!!H. X: synth (analz H) ==> \
   3.701  \              parts (insert X H) <= synth (analz H) Un parts H";
   3.702  by (dtac parts_insert_subset_Un 1);
   3.703  by (Full_simp_tac 1);
   3.704 @@ -716,7 +716,7 @@
   3.705  qed "Fake_parts_insert";
   3.706  
   3.707  (*H is sometimes (Key `` KK Un spies evs), so can't put G=H*)
   3.708 -goal thy "!!H. X: synth (analz G) ==> \
   3.709 +Goal "!!H. X: synth (analz G) ==> \
   3.710  \              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
   3.711  by (rtac subsetI 1);
   3.712  by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
   3.713 @@ -726,11 +726,11 @@
   3.714  by (Blast_tac 1);
   3.715  qed "Fake_analz_insert";
   3.716  
   3.717 -goal thy "(X: analz H & X: parts H) = (X: analz H)";
   3.718 +Goal "(X: analz H & X: parts H) = (X: analz H)";
   3.719  by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
   3.720  val analz_conj_parts = result();
   3.721  
   3.722 -goal thy "(X: analz H | X: parts H) = (X: parts H)";
   3.723 +Goal "(X: analz H | X: parts H) = (X: parts H)";
   3.724  by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1);
   3.725  val analz_disj_parts = result();
   3.726  
   3.727 @@ -738,20 +738,20 @@
   3.728  
   3.729  (*Without this equation, other rules for synth and analz would yield
   3.730    redundant cases*)
   3.731 -goal thy "({|X,Y|} : synth (analz H)) = \
   3.732 +Goal "({|X,Y|} : synth (analz H)) = \
   3.733  \         (X : synth (analz H) & Y : synth (analz H))";
   3.734  by (Blast_tac 1);
   3.735  qed "MPair_synth_analz";
   3.736  
   3.737  AddIffs [MPair_synth_analz];
   3.738  
   3.739 -goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
   3.740 +Goal "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
   3.741  \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   3.742  by (Blast_tac 1);
   3.743  qed "Crypt_synth_analz";
   3.744  
   3.745  
   3.746 -goal thy "!!K. X ~: synth (analz H) \
   3.747 +Goal "!!K. X ~: synth (analz H) \
   3.748  \   ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
   3.749  by (Blast_tac 1);
   3.750  qed "Hash_synth_analz";
   3.751 @@ -762,27 +762,27 @@
   3.752  
   3.753  (*** Freeness ***)
   3.754  
   3.755 -goalw thy [HPair_def] "Agent A ~= Hash[X] Y";
   3.756 +Goalw [HPair_def] "Agent A ~= Hash[X] Y";
   3.757  by (Simp_tac 1);
   3.758  qed "Agent_neq_HPair";
   3.759  
   3.760 -goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
   3.761 +Goalw [HPair_def] "Nonce N ~= Hash[X] Y";
   3.762  by (Simp_tac 1);
   3.763  qed "Nonce_neq_HPair";
   3.764  
   3.765 -goalw thy [HPair_def] "Number N ~= Hash[X] Y";
   3.766 +Goalw [HPair_def] "Number N ~= Hash[X] Y";
   3.767  by (Simp_tac 1);
   3.768  qed "Number_neq_HPair";
   3.769  
   3.770 -goalw thy [HPair_def] "Key K ~= Hash[X] Y";
   3.771 +Goalw [HPair_def] "Key K ~= Hash[X] Y";
   3.772  by (Simp_tac 1);
   3.773  qed "Key_neq_HPair";
   3.774  
   3.775 -goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";
   3.776 +Goalw [HPair_def] "Hash Z ~= Hash[X] Y";
   3.777  by (Simp_tac 1);
   3.778  qed "Hash_neq_HPair";
   3.779  
   3.780 -goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
   3.781 +Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y";
   3.782  by (Simp_tac 1);
   3.783  qed "Crypt_neq_HPair";
   3.784  
   3.785 @@ -792,15 +792,15 @@
   3.786  AddIffs HPair_neqs;
   3.787  AddIffs (HPair_neqs RL [not_sym]);
   3.788  
   3.789 -goalw thy [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
   3.790 +Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)";
   3.791  by (Simp_tac 1);
   3.792  qed "HPair_eq";
   3.793  
   3.794 -goalw thy [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   3.795 +Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)";
   3.796  by (Simp_tac 1);
   3.797  qed "MPair_eq_HPair";
   3.798  
   3.799 -goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   3.800 +Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   3.801  by Auto_tac;
   3.802  qed "HPair_eq_MPair";
   3.803  
   3.804 @@ -809,23 +809,23 @@
   3.805  
   3.806  (*** Specialized laws, proved in terms of those for Hash and MPair ***)
   3.807  
   3.808 -goalw thy [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
   3.809 +Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H";
   3.810  by (Simp_tac 1);
   3.811  qed "keysFor_insert_HPair";
   3.812  
   3.813 -goalw thy [HPair_def]
   3.814 +Goalw [HPair_def]
   3.815      "parts (insert (Hash[X] Y) H) = \
   3.816  \    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))";
   3.817  by (Simp_tac 1);
   3.818  qed "parts_insert_HPair";
   3.819  
   3.820 -goalw thy [HPair_def]
   3.821 +Goalw [HPair_def]
   3.822      "analz (insert (Hash[X] Y) H) = \
   3.823  \    insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))";
   3.824  by (Simp_tac 1);
   3.825  qed "analz_insert_HPair";
   3.826  
   3.827 -goalw thy [HPair_def] "!!H. X ~: synth (analz H) \
   3.828 +Goalw [HPair_def] "!!H. X ~: synth (analz H) \
   3.829  \   ==> (Hash[X] Y : synth (analz H)) = \
   3.830  \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   3.831  by (Simp_tac 1);
     4.1 --- a/src/HOL/Auth/NS_Public.ML	Wed Jun 24 10:33:42 1998 +0200
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Wed Jun 24 11:24:52 1998 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4  AddIffs [Spy_in_bad];
     4.5  
     4.6  (*A "possibility property": there are traces that reach the end*)
     4.7 -goal thy 
     4.8 +Goal 
     4.9   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    4.10  \                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    4.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    4.12 @@ -31,7 +31,7 @@
    4.13  (**** Inductive proofs about ns_public ****)
    4.14  
    4.15  (*Nobody sends themselves messages*)
    4.16 -goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    4.17 +Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    4.18  by (etac ns_public.induct 1);
    4.19  by Auto_tac;
    4.20  qed_spec_mp "not_Says_to_self";
    4.21 @@ -54,14 +54,14 @@
    4.22      sends messages containing X! **)
    4.23  
    4.24  (*Spy never sees another agent's private key! (unless it's bad at start)*)
    4.25 -goal thy 
    4.26 +Goal 
    4.27   "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
    4.28  by (parts_induct_tac 1);
    4.29  by (Blast_tac 1);
    4.30  qed "Spy_see_priK";
    4.31  Addsimps [Spy_see_priK];
    4.32  
    4.33 -goal thy 
    4.34 +Goal 
    4.35   "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    4.36  by Auto_tac;
    4.37  qed "Spy_analz_priK";
    4.38 @@ -75,7 +75,7 @@
    4.39  
    4.40  (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    4.41    is secret.  (Honest users generate fresh nonces.)*)
    4.42 -goal thy 
    4.43 +Goal 
    4.44   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    4.45  \           Nonce NA ~: analz (spies evs);   evs : ns_public |]       \
    4.46  \ ==> Crypt (pubK C) {|NA', Nonce NA, Agent D|} ~: parts (spies evs)";
    4.47 @@ -90,7 +90,7 @@
    4.48  
    4.49  
    4.50  (*Unicity for NS1: nonce NA identifies agents A and B*)
    4.51 -goal thy 
    4.52 +Goal 
    4.53   "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
    4.54  \ ==> EX A' B'. ALL A B.                                            \
    4.55  \      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
    4.56 @@ -105,7 +105,7 @@
    4.57  by (Blast_tac 1);
    4.58  val lemma = result();
    4.59  
    4.60 -goal thy 
    4.61 +Goal 
    4.62   "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
    4.63  \           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
    4.64  \           Nonce NA ~: analz (spies evs);                            \
    4.65 @@ -122,7 +122,7 @@
    4.66  
    4.67  
    4.68  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
    4.69 -goal thy 
    4.70 +Goal 
    4.71   "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;   \
    4.72  \           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
    4.73  \        ==>  Nonce NA ~: analz (spies evs)";
    4.74 @@ -141,7 +141,7 @@
    4.75  
    4.76  (*Authentication for A: if she receives message 2 and has used NA
    4.77    to start a run, then B has sent message 2.*)
    4.78 -goal thy 
    4.79 +Goal 
    4.80   "!!evs. [| Says A  B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;  \
    4.81  \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|})   \
    4.82  \             : set evs;                                                \
    4.83 @@ -161,7 +161,7 @@
    4.84  
    4.85  
    4.86  (*If the encrypted message appears then it originated with Alice in NS1*)
    4.87 -goal thy 
    4.88 +Goal 
    4.89   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    4.90  \           Nonce NA ~: analz (spies evs);                            \
    4.91  \           evs : ns_public |]                                        \
    4.92 @@ -179,7 +179,7 @@
    4.93  (*Unicity for NS2: nonce NB identifies nonce NA and agents A, B 
    4.94    [unicity of B makes Lowe's fix work]
    4.95    [proof closely follows that for unique_NA] *)
    4.96 -goal thy 
    4.97 +Goal 
    4.98   "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]            \
    4.99  \ ==> EX A' NA' B'. ALL A NA B.                                           \
   4.100  \      Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} : parts (spies evs) \
   4.101 @@ -194,7 +194,7 @@
   4.102  by (Blast_tac 1);
   4.103  val lemma = result();
   4.104  
   4.105 -goal thy 
   4.106 +Goal 
   4.107   "!!evs. [| Crypt(pubK A)  {|Nonce NA, Nonce NB, Agent B|}   \
   4.108  \             : parts(spies evs);                            \
   4.109  \           Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \
   4.110 @@ -209,7 +209,7 @@
   4.111  
   4.112  
   4.113  (*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*)
   4.114 -goal thy 
   4.115 +Goal 
   4.116   "!!evs. [| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.117  \             : set evs;                                              \
   4.118  \           A ~: bad;  B ~: bad;  evs : ns_public |]                \
   4.119 @@ -231,7 +231,7 @@
   4.120  
   4.121  (*Authentication for B: if he receives message 3 and has used NB
   4.122    in message 2, then A has sent message 3.*)
   4.123 -goal thy 
   4.124 +Goal 
   4.125   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.126  \             : set evs;                                               \
   4.127  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
   4.128 @@ -255,7 +255,7 @@
   4.129  
   4.130  (*If B receives NS3 and the nonce NB agrees with the nonce he joined with
   4.131    NA, then A initiated the run using NA.  SAME proof as B_trusts_NS3!*)
   4.132 -goal thy 
   4.133 +Goal 
   4.134   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \
   4.135  \             : set evs;                                               \
   4.136  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;            \
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Wed Jun 24 10:33:42 1998 +0200
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Jun 24 11:24:52 1998 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4  AddIffs [Spy_in_bad];
     5.5  
     5.6  (*A "possibility property": there are traces that reach the end*)
     5.7 -goal thy 
     5.8 +Goal 
     5.9   "!!A B. A ~= B ==> EX NB. EX evs: ns_public.               \
    5.10  \                     Says A B (Crypt (pubK B) (Nonce NB)) : set evs";
    5.11  by (REPEAT (resolve_tac [exI,bexI] 1));
    5.12 @@ -35,7 +35,7 @@
    5.13  (**** Inductive proofs about ns_public ****)
    5.14  
    5.15  (*Nobody sends themselves messages*)
    5.16 -goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    5.17 +Goal "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
    5.18  by (etac ns_public.induct 1);
    5.19  by Auto_tac;
    5.20  qed_spec_mp "not_Says_to_self";
    5.21 @@ -58,14 +58,14 @@
    5.22      sends messages containing X! **)
    5.23  
    5.24  (*Spy never sees another agent's private key! (unless it's bad at start)*)
    5.25 -goal thy 
    5.26 +Goal 
    5.27   "!!A. evs: ns_public ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
    5.28  by (parts_induct_tac 1);
    5.29  by (Blast_tac 1);
    5.30  qed "Spy_see_priK";
    5.31  Addsimps [Spy_see_priK];
    5.32  
    5.33 -goal thy 
    5.34 +Goal 
    5.35   "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    5.36  by Auto_tac;
    5.37  qed "Spy_analz_priK";
    5.38 @@ -79,7 +79,7 @@
    5.39  
    5.40  (*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce
    5.41    is secret.  (Honest users generate fresh nonces.)*)
    5.42 -goal thy 
    5.43 +Goal 
    5.44   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    5.45  \           Nonce NA ~: analz (spies evs);   evs : ns_public |]       \
    5.46  \ ==> Crypt (pubK C) {|NA', Nonce NA|} ~: parts (spies evs)";
    5.47 @@ -94,7 +94,7 @@
    5.48  
    5.49  
    5.50  (*Unicity for NS1: nonce NA identifies agents A and B*)
    5.51 -goal thy 
    5.52 +Goal 
    5.53   "!!evs. [| Nonce NA ~: analz (spies evs);  evs : ns_public |]      \
    5.54  \ ==> EX A' B'. ALL A B.                                            \
    5.55  \      Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs) --> \
    5.56 @@ -109,7 +109,7 @@
    5.57  by (Blast_tac 1);
    5.58  val lemma = result();
    5.59  
    5.60 -goal thy 
    5.61 +Goal 
    5.62   "!!evs. [| Crypt(pubK B)  {|Nonce NA, Agent A|}  : parts(spies evs); \
    5.63  \           Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(spies evs); \
    5.64  \           Nonce NA ~: analz (spies evs);                            \
    5.65 @@ -126,7 +126,7 @@
    5.66  
    5.67  
    5.68  (*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*)
    5.69 -goal thy 
    5.70 +Goal 
    5.71   "!!evs. [| Says A B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;   \
    5.72  \           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
    5.73  \        ==>  Nonce NA ~: analz (spies evs)";
    5.74 @@ -145,7 +145,7 @@
    5.75  
    5.76  (*Authentication for A: if she receives message 2 and has used NA
    5.77    to start a run, then B has sent message 2.*)
    5.78 -goal thy 
    5.79 +Goal 
    5.80   "!!evs. [| Says A  B (Crypt(pubK B) {|Nonce NA, Agent A|}) : set evs;  \
    5.81  \           Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set evs;  \
    5.82  \           A ~: bad;  B ~: bad;  evs : ns_public |]                    \
    5.83 @@ -166,7 +166,7 @@
    5.84  
    5.85  
    5.86  (*If the encrypted message appears then it originated with Alice in NS1*)
    5.87 -goal thy 
    5.88 +Goal 
    5.89   "!!evs. [| Crypt (pubK B) {|Nonce NA, Agent A|} : parts (spies evs); \
    5.90  \           Nonce NA ~: analz (spies evs);                            \
    5.91  \           evs : ns_public |]                                        \
    5.92 @@ -183,7 +183,7 @@
    5.93  
    5.94  (*Unicity for NS2: nonce NB identifies nonce NA and agent A
    5.95    [proof closely follows that for unique_NA] *)
    5.96 -goal thy 
    5.97 +Goal 
    5.98   "!!evs. [| Nonce NB ~: analz (spies evs);  evs : ns_public |]            \
    5.99  \ ==> EX A' NA'. ALL A NA.                                                \
   5.100  \      Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (spies evs)          \
   5.101 @@ -197,7 +197,7 @@
   5.102  by (Blast_tac 1);
   5.103  val lemma = result();
   5.104  
   5.105 -goal thy 
   5.106 +Goal 
   5.107   "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|}  : parts(spies evs); \
   5.108  \           Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(spies evs); \
   5.109  \           Nonce NB ~: analz (spies evs);                            \
   5.110 @@ -208,7 +208,7 @@
   5.111  
   5.112  
   5.113  (*NB remains secret PROVIDED Alice never responds with round 3*)
   5.114 -goal thy 
   5.115 +Goal 
   5.116   "!!evs.[| Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs;  \
   5.117  \          ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set evs;      \
   5.118  \          A ~: bad;  B ~: bad;  evs : ns_public |]                     \
   5.119 @@ -232,7 +232,7 @@
   5.120  
   5.121  (*Authentication for B: if he receives message 3 and has used NB
   5.122    in message 2, then A has sent message 3--to somebody....*)
   5.123 -goal thy 
   5.124 +Goal 
   5.125   "!!evs. [| Says B A  (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs; \
   5.126  \           Says A' B (Crypt (pubK B) (Nonce NB)): set evs;              \
   5.127  \           A ~: bad;  B ~: bad;  evs : ns_public |]                   \
   5.128 @@ -254,7 +254,7 @@
   5.129  
   5.130  
   5.131  (*Can we strengthen the secrecy theorem?  NO*)
   5.132 -goal thy 
   5.133 +Goal 
   5.134   "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_public |]           \
   5.135  \ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set evs \
   5.136  \     --> Nonce NB ~: analz (spies evs)";
     6.1 --- a/src/HOL/Auth/NS_Shared.ML	Wed Jun 24 10:33:42 1998 +0200
     6.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Jun 24 11:24:52 1998 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4  
     6.5  
     6.6  (*A "possibility property": there are traces that reach the end*)
     6.7 -goal thy 
     6.8 +Goal 
     6.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
    6.10  \        ==> EX N K. EX evs: ns_shared.               \
    6.11  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    6.12 @@ -31,7 +31,7 @@
    6.13  by possibility_tac;
    6.14  result();
    6.15  
    6.16 -goal thy 
    6.17 +Goal 
    6.18   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
    6.19  \        ==> EX evs: ns_shared.          \
    6.20  \               Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs";
    6.21 @@ -43,7 +43,7 @@
    6.22  (**** Inductive proofs about ns_shared ****)
    6.23  
    6.24  (*Nobody sends themselves messages*)
    6.25 -goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
    6.26 +Goal "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
    6.27  by (etac ns_shared.induct 1);
    6.28  by Auto_tac;
    6.29  qed_spec_mp "not_Says_to_self";
    6.30 @@ -51,12 +51,12 @@
    6.31  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    6.32  
    6.33  (*For reasoning about the encrypted portion of message NS3*)
    6.34 -goal thy "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    6.35 +Goal "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \
    6.36  \                ==> X : parts (spies evs)";
    6.37  by (Blast_tac 1);
    6.38  qed "NS3_msg_in_parts_spies";
    6.39                                
    6.40 -goal thy
    6.41 +Goal
    6.42      "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \
    6.43  \           ==> K : parts (spies evs)";
    6.44  by (Blast_tac 1);
    6.45 @@ -75,14 +75,14 @@
    6.46      sends messages containing X! **)
    6.47  
    6.48  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    6.49 -goal thy 
    6.50 +Goal 
    6.51   "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    6.52  by (parts_induct_tac 1);
    6.53  by (ALLGOALS Blast_tac);
    6.54  qed "Spy_see_shrK";
    6.55  Addsimps [Spy_see_shrK];
    6.56  
    6.57 -goal thy 
    6.58 +Goal 
    6.59   "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    6.60  by Auto_tac;
    6.61  qed "Spy_analz_shrK";
    6.62 @@ -93,7 +93,7 @@
    6.63  
    6.64  
    6.65  (*Nobody can have used non-existent keys!*)
    6.66 -goal thy "!!evs. evs : ns_shared ==>      \
    6.67 +Goal "!!evs. evs : ns_shared ==>      \
    6.68  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    6.69  by (parts_induct_tac 1);
    6.70  (*Fake*)
    6.71 @@ -112,7 +112,7 @@
    6.72  (** Lemmas concerning the form of items passed in messages **)
    6.73  
    6.74  (*Describes the form of K, X and K' when the Server sends this message.*)
    6.75 -goal thy 
    6.76 +Goal 
    6.77   "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \
    6.78  \           evs : ns_shared |]                           \
    6.79  \        ==> K ~: range shrK &                           \
    6.80 @@ -125,7 +125,7 @@
    6.81  
    6.82  
    6.83  (*If the encrypted message appears then it originated with the Server*)
    6.84 -goal thy
    6.85 +Goal
    6.86   "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    6.87  \           A ~: bad;  evs : ns_shared |]                                 \
    6.88  \         ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})    \
    6.89 @@ -136,7 +136,7 @@
    6.90  qed "A_trusts_NS2";
    6.91  
    6.92  
    6.93 -goal thy
    6.94 +Goal
    6.95   "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
    6.96  \           A ~: bad;  evs : ns_shared |]                                 \
    6.97  \         ==> K ~: range shrK &  X = (Crypt (shrK B) {|Key K, Agent A|})";
    6.98 @@ -147,7 +147,7 @@
    6.99  (*EITHER describes the form of X when the following message is sent, 
   6.100    OR     reduces it to the Fake case.
   6.101    Use Says_Server_message_form if applicable.*)
   6.102 -goal thy 
   6.103 +Goal 
   6.104   "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})      \
   6.105  \              : set evs;                                                  \
   6.106  \           evs : ns_shared |]                                             \
   6.107 @@ -180,7 +180,7 @@
   6.108  (*NOT useful in this form, but it says that session keys are not used
   6.109    to encrypt messages containing other keys, in the actual protocol.
   6.110    We require that agents should behave like this subsequently also.*)
   6.111 -goal thy 
   6.112 +Goal 
   6.113   "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
   6.114  \           (Crypt KAB X) : parts (spies evs) &         \
   6.115  \           Key K : parts {X} --> Key K : parts (spies evs)";
   6.116 @@ -196,7 +196,7 @@
   6.117  (** Session keys are not used to encrypt other session keys **)
   6.118  
   6.119  (*The equality makes the induction hypothesis easier to apply*)
   6.120 -goal thy  
   6.121 +Goal  
   6.122   "!!evs. evs : ns_shared ==>                             \
   6.123  \  ALL K KK. KK <= Compl (range shrK) -->                \
   6.124  \            (Key K : analz (Key``KK Un (spies evs))) =  \
   6.125 @@ -212,7 +212,7 @@
   6.126  qed_spec_mp "analz_image_freshK";
   6.127  
   6.128  
   6.129 -goal thy
   6.130 +Goal
   6.131   "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
   6.132  \        Key K : analz (insert (Key KAB) (spies evs)) = \
   6.133  \        (K = KAB | Key K : analz (spies evs))";
   6.134 @@ -222,7 +222,7 @@
   6.135  
   6.136  (** The session key K uniquely identifies the message **)
   6.137  
   6.138 -goal thy 
   6.139 +Goal 
   6.140   "!!evs. evs : ns_shared ==>                                               \
   6.141  \      EX A' NA' B' X'. ALL A NA B X.                                      \
   6.142  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
   6.143 @@ -240,7 +240,7 @@
   6.144  val lemma = result();
   6.145  
   6.146  (*In messages of this form, the session key uniquely identifies the rest*)
   6.147 -goal thy 
   6.148 +Goal 
   6.149   "!!evs. [| Says Server A                                               \
   6.150  \             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
   6.151  \           Says Server A'                                              \
   6.152 @@ -252,7 +252,7 @@
   6.153  
   6.154  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   6.155  
   6.156 -goal thy 
   6.157 +Goal 
   6.158   "!!evs. [| A ~: bad;  B ~: bad;  evs : ns_shared |]                   \
   6.159  \        ==> Says Server A                                             \
   6.160  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   6.161 @@ -285,7 +285,7 @@
   6.162  
   6.163  
   6.164  (*Final version: Server's message in the most abstract form*)
   6.165 -goal thy 
   6.166 +Goal 
   6.167   "!!evs. [| Says Server A                                        \
   6.168  \              (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;   \
   6.169  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;      \
   6.170 @@ -302,7 +302,7 @@
   6.171  
   6.172  
   6.173  (*If the encrypted message appears then it originated with the Server*)
   6.174 -goal thy
   6.175 +Goal
   6.176   "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
   6.177  \           B ~: bad;  evs : ns_shared |]                              \
   6.178  \         ==> EX NA. Says Server A                                     \
   6.179 @@ -315,7 +315,7 @@
   6.180  qed "B_trusts_NS3";
   6.181  
   6.182  
   6.183 -goal thy
   6.184 +Goal
   6.185   "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
   6.186  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   6.187  \              : set evs;                                             \
   6.188 @@ -342,7 +342,7 @@
   6.189  
   6.190  
   6.191  (*This version no longer assumes that K is secure*)
   6.192 -goal thy
   6.193 +Goal
   6.194   "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);                   \
   6.195  \           Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \
   6.196  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;           \
   6.197 @@ -356,7 +356,7 @@
   6.198  (*If the session key has been used in NS4 then somebody has forwarded
   6.199    component X in some instance of NS4.  Perhaps an interesting property, 
   6.200    but not needed (after all) for the proofs below.*)
   6.201 -goal thy
   6.202 +Goal
   6.203   "!!evs. [| Crypt K (Nonce NB) : parts (spies evs);     \
   6.204  \           Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|})  \
   6.205  \             : set evs;                                              \
   6.206 @@ -383,7 +383,7 @@
   6.207  qed "NS4_implies_NS3";
   6.208  
   6.209  
   6.210 -goal thy
   6.211 +Goal
   6.212   "!!evs. [| B ~: bad;  evs : ns_shared |]                              \
   6.213  \        ==> Key K ~: analz (spies evs) -->                            \
   6.214  \            Says Server A                                             \
   6.215 @@ -411,7 +411,7 @@
   6.216  
   6.217  
   6.218  (*Very strong Oops condition reveals protocol's weakness*)
   6.219 -goal thy
   6.220 +Goal
   6.221   "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs);      \
   6.222  \           Says B A (Crypt K (Nonce NB))  : set evs;                \
   6.223  \           Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);   \
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Wed Jun 24 10:33:42 1998 +0200
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Jun 24 11:24:52 1998 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4  
     7.5  
     7.6  (*A "possibility property": there are traces that reach the end*)
     7.7 -goal thy 
     7.8 +Goal 
     7.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    7.10  \        ==> EX K. EX NA. EX evs: otway.          \
    7.11  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    7.12 @@ -37,7 +37,7 @@
    7.13  (**** Inductive proofs about otway ****)
    7.14  
    7.15  (*Nobody sends themselves messages*)
    7.16 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    7.17 +Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    7.18  by (etac otway.induct 1);
    7.19  by Auto_tac;
    7.20  qed_spec_mp "not_Says_to_self";
    7.21 @@ -47,19 +47,19 @@
    7.22  
    7.23  (** For reasoning about the encrypted portion of messages **)
    7.24  
    7.25 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.26 +Goal "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.27  \                ==> X : analz (spies evs)";
    7.28  by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.29  by (Blast_tac 1);
    7.30  qed "OR2_analz_spies";
    7.31  
    7.32 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.33 +Goal "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.34  \                ==> X : analz (spies evs)";
    7.35  by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.36  by (Blast_tac 1);
    7.37  qed "OR4_analz_spies";
    7.38  
    7.39 -goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    7.40 +Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    7.41  \                ==> K : parts (spies evs)";
    7.42  by (Blast_tac 1);
    7.43  qed "Oops_parts_spies";
    7.44 @@ -82,14 +82,14 @@
    7.45      sends messages containing X! **)
    7.46  
    7.47  (*Spy never sees a good agent's shared key!*)
    7.48 -goal thy 
    7.49 +Goal 
    7.50   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    7.51  by (parts_induct_tac 1);
    7.52  by (ALLGOALS Blast_tac);
    7.53  qed "Spy_see_shrK";
    7.54  Addsimps [Spy_see_shrK];
    7.55  
    7.56 -goal thy 
    7.57 +Goal 
    7.58   "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    7.59  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    7.60  qed "Spy_analz_shrK";
    7.61 @@ -100,7 +100,7 @@
    7.62  
    7.63  
    7.64  (*Nobody can have used non-existent keys!*)
    7.65 -goal thy "!!evs. evs : otway ==>          \
    7.66 +Goal "!!evs. evs : otway ==>          \
    7.67  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    7.68  by (parts_induct_tac 1);
    7.69  (*Fake*)
    7.70 @@ -121,7 +121,7 @@
    7.71  
    7.72  (*Describes the form of K and NA when the Server sends this message.  Also
    7.73    for Oops case.*)
    7.74 -goal thy 
    7.75 +Goal 
    7.76   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    7.77  \           evs : otway |]                                           \
    7.78  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    7.79 @@ -153,7 +153,7 @@
    7.80  (** Session keys are not used to encrypt other session keys **)
    7.81  
    7.82  (*The equality makes the induction hypothesis easier to apply*)
    7.83 -goal thy  
    7.84 +Goal  
    7.85   "!!evs. evs : otway ==>                                    \
    7.86  \  ALL K KK. KK <= Compl (range shrK) -->                   \
    7.87  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    7.88 @@ -168,7 +168,7 @@
    7.89  qed_spec_mp "analz_image_freshK";
    7.90  
    7.91  
    7.92 -goal thy
    7.93 +Goal
    7.94   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
    7.95  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
    7.96  \        (K = KAB | Key K : analz (spies evs))";
    7.97 @@ -178,7 +178,7 @@
    7.98  
    7.99  (*** The Key K uniquely identifies the Server's  message. **)
   7.100  
   7.101 -goal thy 
   7.102 +Goal 
   7.103   "!!evs. evs : otway ==>                                                  \
   7.104  \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
   7.105  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
   7.106 @@ -195,7 +195,7 @@
   7.107  by (blast_tac (claset() addSEs spies_partsEs) 1);
   7.108  val lemma = result();
   7.109  
   7.110 -goal thy 
   7.111 +Goal 
   7.112   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   7.113  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
   7.114  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   7.115 @@ -207,7 +207,7 @@
   7.116  (**** Authenticity properties relating to NA ****)
   7.117  
   7.118  (*Only OR1 can have caused such a part of a message to appear.*)
   7.119 -goal thy 
   7.120 +Goal 
   7.121   "!!evs. [| A ~: bad;  evs : otway |]                             \
   7.122  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   7.123  \            Says A B {|NA, Agent A, Agent B,                      \
   7.124 @@ -220,7 +220,7 @@
   7.125  
   7.126  (** The Nonce NA uniquely identifies A's message. **)
   7.127  
   7.128 -goal thy 
   7.129 +Goal 
   7.130   "!!evs. [| evs : otway; A ~: bad |]               \
   7.131  \ ==> EX B'. ALL B.                                 \
   7.132  \        Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) \
   7.133 @@ -233,7 +233,7 @@
   7.134  by (Blast_tac 1);
   7.135  val lemma = result();
   7.136  
   7.137 -goal thy 
   7.138 +Goal 
   7.139   "!!evs.[| Crypt (shrK A) {|NA, Agent A, Agent B|}: parts (spies evs); \
   7.140  \          Crypt (shrK A) {|NA, Agent A, Agent C|}: parts (spies evs); \
   7.141  \          evs : otway;  A ~: bad |]                                   \
   7.142 @@ -245,7 +245,7 @@
   7.143  (*It is impossible to re-use a nonce in both OR1 and OR2.  This holds because
   7.144    OR2 encrypts Nonce NB.  It prevents the attack that can occur in the
   7.145    over-simplified version of this protocol: see OtwayRees_Bad.*)
   7.146 -goal thy 
   7.147 +Goal 
   7.148   "!!evs. [| A ~: bad;  evs : otway |]                      \
   7.149  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   7.150  \            Crypt (shrK A) {|NA', NA, Agent A', Agent A|}  \
   7.151 @@ -258,7 +258,7 @@
   7.152  
   7.153  (*Crucial property: If the encrypted message appears, and A has used NA
   7.154    to start a run, then it originated with the Server!*)
   7.155 -goal thy 
   7.156 +Goal 
   7.157   "!!evs. [| A ~: bad;  evs : otway |]                                  \
   7.158  \    ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs)              \
   7.159  \        --> Says A B {|NA, Agent A, Agent B,                          \
   7.160 @@ -290,7 +290,7 @@
   7.161    then the key really did come from the Server!  CANNOT prove this of the
   7.162    bad form of this protocol, even though we can prove
   7.163    Spy_not_see_encrypted_key*)
   7.164 -goal thy 
   7.165 +Goal 
   7.166   "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
   7.167  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   7.168  \           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   7.169 @@ -308,7 +308,7 @@
   7.170      Does not in itself guarantee security: an attack could violate 
   7.171      the premises, e.g. by having A=Spy **)
   7.172  
   7.173 -goal thy 
   7.174 +Goal 
   7.175   "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
   7.176  \        ==> Says Server B                                            \
   7.177  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.178 @@ -331,7 +331,7 @@
   7.179  by (spy_analz_tac 1);
   7.180  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   7.181  
   7.182 -goal thy 
   7.183 +Goal 
   7.184   "!!evs. [| Says Server B                                           \
   7.185  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   7.186  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   7.187 @@ -345,7 +345,7 @@
   7.188  
   7.189  (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   7.190    what it is.*)
   7.191 -goal thy 
   7.192 +Goal 
   7.193   "!!evs. [| Says A  B {|NA, Agent A, Agent B,                       \
   7.194  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
   7.195  \           Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \
   7.196 @@ -360,7 +360,7 @@
   7.197  
   7.198  (*Only OR2 can have caused such a part of a message to appear.  We do not
   7.199    know anything about X: it does NOT have to have the right form.*)
   7.200 -goal thy 
   7.201 +Goal 
   7.202   "!!evs. [| B ~: bad;  evs : otway |]                         \
   7.203  \        ==> Crypt (shrK B) {|NA, NB, Agent A, Agent B|}       \
   7.204  \             : parts (spies evs) -->                       \
   7.205 @@ -375,7 +375,7 @@
   7.206  
   7.207  (** The Nonce NB uniquely identifies B's  message. **)
   7.208  
   7.209 -goal thy 
   7.210 +Goal 
   7.211   "!!evs. [| evs : otway; B ~: bad |]  \
   7.212  \ ==> EX NA' A'. ALL NA A.            \
   7.213  \      Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs) \
   7.214 @@ -388,7 +388,7 @@
   7.215  by (Blast_tac 1);
   7.216  val lemma = result();
   7.217  
   7.218 -goal thy 
   7.219 +Goal 
   7.220   "!!evs.[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(spies evs); \
   7.221  \          Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(spies evs); \
   7.222  \          evs : otway;  B ~: bad |]             \
   7.223 @@ -399,7 +399,7 @@
   7.224  
   7.225  (*If the encrypted message appears, and B has used Nonce NB,
   7.226    then it originated with the Server!*)
   7.227 -goal thy 
   7.228 +Goal 
   7.229   "!!evs. [| B ~: bad;  evs : otway |]                                    \
   7.230  \    ==> Crypt (shrK B) {|NB, Key K|} : parts (spies evs)                \
   7.231  \        --> (ALL X'. Says B Server                                      \
   7.232 @@ -430,7 +430,7 @@
   7.233  
   7.234  (*Guarantee for B: if it gets a message with matching NB then the Server
   7.235    has sent the correct message.*)
   7.236 -goal thy 
   7.237 +Goal 
   7.238   "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
   7.239  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   7.240  \            : set evs;                                            \
   7.241 @@ -446,7 +446,7 @@
   7.242  
   7.243  
   7.244  (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   7.245 -goal thy 
   7.246 +Goal 
   7.247   "!!evs. [| Says B Server {|NA, Agent A, Agent B, X',              \
   7.248  \                           Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \
   7.249  \             : set evs;                                           \
   7.250 @@ -458,7 +458,7 @@
   7.251  qed "B_gets_good_key";
   7.252  
   7.253  
   7.254 -goal thy 
   7.255 +Goal 
   7.256   "!!evs. [| B ~: bad;  evs : otway |]                            \
   7.257  \        ==> Says Server B                                       \
   7.258  \              {|NA, Crypt (shrK A) {|NA, Key K|},               \
   7.259 @@ -476,7 +476,7 @@
   7.260  (*After getting and checking OR4, agent A can trust that B has been active.
   7.261    We could probably prove that X has the expected form, but that is not
   7.262    strictly necessary for authentication.*)
   7.263 -goal thy 
   7.264 +Goal 
   7.265   "!!evs. [| Says B' A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs;        \
   7.266  \           Says A  B {|NA, Agent A, Agent B,                                \
   7.267  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Wed Jun 24 10:33:42 1998 +0200
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Jun 24 11:24:52 1998 +0200
     8.3 @@ -23,7 +23,7 @@
     8.4  
     8.5  
     8.6  (*A "possibility property": there are traces that reach the end*)
     8.7 -goal thy 
     8.8 +Goal 
     8.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                               \
    8.10  \        ==> EX K. EX NA. EX evs: otway.                                      \
    8.11  \             Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \
    8.12 @@ -37,7 +37,7 @@
    8.13  (**** Inductive proofs about otway ****)
    8.14  
    8.15  (*Nobody sends themselves messages*)
    8.16 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    8.17 +Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    8.18  by (etac otway.induct 1);
    8.19  by Auto_tac;
    8.20  qed_spec_mp "not_Says_to_self";
    8.21 @@ -47,13 +47,13 @@
    8.22  
    8.23  (** For reasoning about the encrypted portion of messages **)
    8.24  
    8.25 -goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    8.26 +Goal "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    8.27  \                X : analz (spies evs)";
    8.28  by (dtac (Says_imp_spies RS analz.Inj) 1);
    8.29  by (Blast_tac 1);
    8.30  qed "OR4_analz_spies";
    8.31  
    8.32 -goal thy "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    8.33 +Goal "!!evs. Says Server B {|X, Crypt K' {|NB, a, Agent B, K|}|} \
    8.34  \                  : set evs ==> K : parts (spies evs)";
    8.35  by (Blast_tac 1);
    8.36  qed "Oops_parts_spies";
    8.37 @@ -73,14 +73,14 @@
    8.38      sends messages containing X! **)
    8.39  
    8.40  (*Spy never sees a good agent's shared key!*)
    8.41 -goal thy 
    8.42 +Goal 
    8.43   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    8.44  by (parts_induct_tac 1);
    8.45  by (ALLGOALS Blast_tac);
    8.46  qed "Spy_see_shrK";
    8.47  Addsimps [Spy_see_shrK];
    8.48  
    8.49 -goal thy 
    8.50 +Goal 
    8.51   "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    8.52  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    8.53  qed "Spy_analz_shrK";
    8.54 @@ -91,7 +91,7 @@
    8.55  
    8.56  
    8.57  (*Nobody can have used non-existent keys!*)
    8.58 -goal thy "!!evs. evs : otway ==>          \
    8.59 +Goal "!!evs. evs : otway ==>          \
    8.60  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    8.61  by (parts_induct_tac 1);
    8.62  (*Fake*)
    8.63 @@ -111,7 +111,7 @@
    8.64  (*** Proofs involving analz ***)
    8.65  
    8.66  (*Describes the form of K and NA when the Server sends this message.*)
    8.67 -goal thy 
    8.68 +Goal 
    8.69   "!!evs. [| Says Server B                                           \
    8.70  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
    8.71  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
    8.72 @@ -146,7 +146,7 @@
    8.73  (** Session keys are not used to encrypt other session keys **)
    8.74  
    8.75  (*The equality makes the induction hypothesis easier to apply*)
    8.76 -goal thy  
    8.77 +Goal  
    8.78   "!!evs. evs : otway ==>                                 \
    8.79  \  ALL K KK. KK <= Compl (range shrK) -->                \
    8.80  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    8.81 @@ -161,7 +161,7 @@
    8.82  qed_spec_mp "analz_image_freshK";
    8.83  
    8.84  
    8.85 -goal thy
    8.86 +Goal
    8.87   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>       \
    8.88  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
    8.89  \        (K = KAB | Key K : analz (spies evs))";
    8.90 @@ -171,7 +171,7 @@
    8.91  
    8.92  (*** The Key K uniquely identifies the Server's message. **)
    8.93  
    8.94 -goal thy 
    8.95 +Goal 
    8.96   "!!evs. evs : otway ==>                                            \
    8.97  \      EX A' B' NA' NB'. ALL A B NA NB.                             \
    8.98  \       Says Server B                                               \
    8.99 @@ -191,7 +191,7 @@
   8.100  val lemma = result();
   8.101  
   8.102  
   8.103 -goal thy 
   8.104 +Goal 
   8.105  "!!evs. [| Says Server B                                           \
   8.106  \            {|Crypt (shrK A) {|NA, Agent A, Agent B, K|},         \
   8.107  \              Crypt (shrK B) {|NB, Agent A, Agent B, K|}|}        \
   8.108 @@ -210,7 +210,7 @@
   8.109  (**** Authenticity properties relating to NA ****)
   8.110  
   8.111  (*If the encrypted message appears then it originated with the Server!*)
   8.112 -goal thy 
   8.113 +Goal 
   8.114   "!!evs. [| A ~: bad;  evs : otway |]                 \
   8.115  \ ==> Crypt (shrK A) {|NA, Agent A, Agent B, Key K|} : parts (spies evs) \
   8.116  \     --> (EX NB. Says Server B                                          \
   8.117 @@ -227,7 +227,7 @@
   8.118  
   8.119  (*Corollary: if A receives B's OR4 message then it originated with the Server.
   8.120    Freshness may be inferred from nonce NA.*)
   8.121 -goal thy 
   8.122 +Goal 
   8.123   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   8.124  \            : set evs;                                                 \
   8.125  \           A ~: bad;  evs : otway |]                                  \
   8.126 @@ -243,7 +243,7 @@
   8.127      Does not in itself guarantee security: an attack could violate 
   8.128      the premises, e.g. by having A=Spy **)
   8.129  
   8.130 -goal thy 
   8.131 +Goal 
   8.132   "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                   \
   8.133  \        ==> Says Server B                                         \
   8.134  \             {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   8.135 @@ -267,7 +267,7 @@
   8.136  by (spy_analz_tac 1);
   8.137  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   8.138  
   8.139 -goal thy 
   8.140 +Goal 
   8.141   "!!evs. [| Says Server B                                           \
   8.142  \              {|Crypt (shrK A) {|NA, Agent A, Agent B, Key K|},    \
   8.143  \                Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|}   \
   8.144 @@ -282,7 +282,7 @@
   8.145  
   8.146  (*A's guarantee.  The Oops premise quantifies over NB because A cannot know
   8.147    what it is.*)
   8.148 -goal thy 
   8.149 +Goal 
   8.150   "!!evs. [| Says B' A (Crypt (shrK A) {|NA, Agent A, Agent B, Key K|})  \
   8.151  \            : set evs;                                                 \
   8.152  \           ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs;         \
   8.153 @@ -295,7 +295,7 @@
   8.154  (**** Authenticity properties relating to NB ****)
   8.155  
   8.156  (*If the encrypted message appears then it originated with the Server!*)
   8.157 -goal thy 
   8.158 +Goal 
   8.159   "!!evs. [| B ~: bad;  evs : otway |]                                 \
   8.160  \    ==> Crypt (shrK B) {|NB, Agent A, Agent B, Key K|} : parts (spies evs) \
   8.161  \        --> (EX NA. Says Server B                                          \
   8.162 @@ -312,7 +312,7 @@
   8.163  
   8.164  (*Guarantee for B: if it gets a well-formed certificate then the Server
   8.165    has sent the correct message in round 3.*)
   8.166 -goal thy 
   8.167 +Goal 
   8.168   "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   8.169  \             : set evs;                                                    \
   8.170  \           B ~: bad;  evs : otway |]                                       \
   8.171 @@ -325,7 +325,7 @@
   8.172  
   8.173  
   8.174  (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*)
   8.175 -goal thy 
   8.176 +Goal 
   8.177   "!!evs. [| Says S' B {|X, Crypt (shrK B) {|NB, Agent A, Agent B, Key K|}|} \
   8.178  \            : set evs;                                            \
   8.179  \           ALL NA. Notes Spy {|NA, NB, Key K|} ~: set evs;                \
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Wed Jun 24 10:33:42 1998 +0200
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Jun 24 11:24:52 1998 +0200
     9.3 @@ -26,7 +26,7 @@
     9.4  
     9.5  
     9.6  (*A "possibility property": there are traces that reach the end*)
     9.7 -goal thy 
     9.8 +Goal 
     9.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
    9.10  \        ==> EX K. EX NA. EX evs: otway.          \
    9.11  \               Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \
    9.12 @@ -40,7 +40,7 @@
    9.13  (**** Inductive proofs about otway ****)
    9.14  
    9.15  (*Nobody sends themselves messages*)
    9.16 -goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    9.17 +Goal "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
    9.18  by (etac otway.induct 1);
    9.19  by Auto_tac;
    9.20  qed_spec_mp "not_Says_to_self";
    9.21 @@ -50,19 +50,19 @@
    9.22  
    9.23  (** For reasoning about the encrypted portion of messages **)
    9.24  
    9.25 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    9.26 +Goal "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    9.27  \                ==> X : analz (spies evs)";
    9.28  by (dtac (Says_imp_spies RS analz.Inj) 1);
    9.29  by (Blast_tac 1);
    9.30  qed "OR2_analz_spies";
    9.31  
    9.32 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    9.33 +Goal "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    9.34  \                ==> X : analz (spies evs)";
    9.35  by (dtac (Says_imp_spies RS analz.Inj) 1);
    9.36  by (Blast_tac 1);
    9.37  qed "OR4_analz_spies";
    9.38  
    9.39 -goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    9.40 +Goal "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    9.41  \                ==> K : parts (spies evs)";
    9.42  by (Blast_tac 1);
    9.43  qed "Oops_parts_spies";
    9.44 @@ -85,14 +85,14 @@
    9.45      sends messages containing X! **)
    9.46  
    9.47  (*Spy never sees a good agent's shared key!*)
    9.48 -goal thy 
    9.49 +Goal 
    9.50   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    9.51  by (parts_induct_tac 1);
    9.52  by (ALLGOALS Blast_tac);
    9.53  qed "Spy_see_shrK";
    9.54  Addsimps [Spy_see_shrK];
    9.55  
    9.56 -goal thy 
    9.57 +Goal 
    9.58   "!!evs. evs : otway ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    9.59  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
    9.60  qed "Spy_analz_shrK";
    9.61 @@ -103,7 +103,7 @@
    9.62  
    9.63  
    9.64  (*Nobody can have used non-existent keys!*)
    9.65 -goal thy "!!evs. evs : otway ==>          \
    9.66 +Goal "!!evs. evs : otway ==>          \
    9.67  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
    9.68  by (parts_induct_tac 1);
    9.69  (*Fake*)
    9.70 @@ -124,7 +124,7 @@
    9.71  
    9.72  (*Describes the form of K and NA when the Server sends this message.  Also
    9.73    for Oops case.*)
    9.74 -goal thy 
    9.75 +Goal 
    9.76   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    9.77  \           evs : otway |]                                           \
    9.78  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    9.79 @@ -156,7 +156,7 @@
    9.80  (** Session keys are not used to encrypt other session keys **)
    9.81  
    9.82  (*The equality makes the induction hypothesis easier to apply*)
    9.83 -goal thy  
    9.84 +Goal  
    9.85   "!!evs. evs : otway ==>                                    \
    9.86  \  ALL K KK. KK <= Compl (range shrK) -->                   \
    9.87  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    9.88 @@ -171,7 +171,7 @@
    9.89  qed_spec_mp "analz_image_freshK";
    9.90  
    9.91  
    9.92 -goal thy
    9.93 +Goal
    9.94   "!!evs. [| evs : otway;  KAB ~: range shrK |] ==>          \
    9.95  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
    9.96  \        (K = KAB | Key K : analz (spies evs))";
    9.97 @@ -181,7 +181,7 @@
    9.98  
    9.99  (*** The Key K uniquely identifies the Server's  message. **)
   9.100  
   9.101 -goal thy 
   9.102 +Goal 
   9.103   "!!evs. evs : otway ==>                                                  \
   9.104  \   EX B' NA' NB' X'. ALL B NA NB X.                                      \
   9.105  \     Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|} : set evs -->     \
   9.106 @@ -198,7 +198,7 @@
   9.107  by (blast_tac (claset() addSEs spies_partsEs) 1);
   9.108  val lemma = result();
   9.109  
   9.110 -goal thy 
   9.111 +Goal 
   9.112   "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, K|}|}   : set evs; \ 
   9.113  \           Says Server B' {|NA',X',Crypt (shrK B') {|NB',K|}|} : set evs; \
   9.114  \           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   9.115 @@ -210,7 +210,7 @@
   9.116      Does not in itself guarantee security: an attack could violate 
   9.117      the premises, e.g. by having A=Spy **)
   9.118  
   9.119 -goal thy 
   9.120 +Goal 
   9.121   "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
   9.122  \        ==> Says Server B                                            \
   9.123  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   9.124 @@ -233,7 +233,7 @@
   9.125  by (spy_analz_tac 1);
   9.126  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   9.127  
   9.128 -goal thy 
   9.129 +Goal 
   9.130   "!!evs. [| Says Server B                                           \
   9.131  \            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   9.132  \                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   9.133 @@ -251,7 +251,7 @@
   9.134    I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
   9.135    Perhaps it's because OR2 has two similar-looking encrypted messages in
   9.136          this version.*)
   9.137 -goal thy 
   9.138 +Goal 
   9.139   "!!evs. [| A ~: bad;  A ~= B;  evs : otway |]                \
   9.140  \        ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (spies evs) --> \
   9.141  \            Says A B {|NA, Agent A, Agent B,                  \
   9.142 @@ -265,7 +265,7 @@
   9.143    to start a run, then it originated with the Server!*)
   9.144  (*Only it is FALSE.  Somebody could make a fake message to Server
   9.145            substituting some other nonce NA' for NB.*)
   9.146 -goal thy 
   9.147 +Goal 
   9.148   "!!evs. [| A ~: bad;  evs : otway |]                                \
   9.149  \        ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) -->    \
   9.150  \            Says A B {|NA, Agent A, Agent B,                        \
    10.1 --- a/src/HOL/Auth/Public.ML	Wed Jun 24 10:33:42 1998 +0200
    10.2 +++ b/src/HOL/Auth/Public.ML	Wed Jun 24 11:24:52 1998 +0200
    10.3 @@ -15,7 +15,7 @@
    10.4  
    10.5  AddIffs [inj_pubK RS inj_eq];
    10.6  
    10.7 -goal thy "!!A B. (priK A = priK B) = (A=B)";
    10.8 +Goal "!!A B. (priK A = priK B) = (A=B)";
    10.9  by Safe_tac;
   10.10  by (dres_inst_tac [("f","invKey")] arg_cong 1);
   10.11  by (Full_simp_tac 1);
   10.12 @@ -24,11 +24,11 @@
   10.13  AddIffs [priK_inj_eq];
   10.14  AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
   10.15  
   10.16 -goalw thy [isSymKey_def] "~ isSymKey (pubK A)";
   10.17 +Goalw [isSymKey_def] "~ isSymKey (pubK A)";
   10.18  by (Simp_tac 1);
   10.19  qed "not_isSymKey_pubK";
   10.20  
   10.21 -goalw thy [isSymKey_def] "~ isSymKey (priK A)";
   10.22 +Goalw [isSymKey_def] "~ isSymKey (priK A)";
   10.23  by (Simp_tac 1);
   10.24  qed "not_isSymKey_priK";
   10.25  
   10.26 @@ -37,16 +37,16 @@
   10.27  
   10.28  (** "Image" equations that hold for injective functions **)
   10.29  
   10.30 -goal thy "(invKey x : invKey``A) = (x:A)";
   10.31 +Goal "(invKey x : invKey``A) = (x:A)";
   10.32  by Auto_tac;
   10.33  qed "invKey_image_eq";
   10.34  
   10.35  (*holds because invKey is injective*)
   10.36 -goal thy "(pubK x : pubK``A) = (x:A)";
   10.37 +Goal "(pubK x : pubK``A) = (x:A)";
   10.38  by Auto_tac;
   10.39  qed "pubK_image_eq";
   10.40  
   10.41 -goal thy "(priK x ~: pubK``A)";
   10.42 +Goal "(priK x ~: pubK``A)";
   10.43  by Auto_tac;
   10.44  qed "priK_pubK_image_eq";
   10.45  Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
   10.46 @@ -55,7 +55,7 @@
   10.47  (** Rewrites should not refer to  initState(Friend i) 
   10.48      -- not in normal form! **)
   10.49  
   10.50 -goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
   10.51 +Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
   10.52  by (induct_tac "C" 1);
   10.53  by (auto_tac (claset() addIs [range_eqI], simpset()));
   10.54  qed "keysFor_parts_initState";
   10.55 @@ -65,14 +65,14 @@
   10.56  (*** Function "spies" ***)
   10.57  
   10.58  (*Agents see their own private keys!*)
   10.59 -goal thy "Key (priK A) : initState A";
   10.60 +Goal "Key (priK A) : initState A";
   10.61  by (induct_tac "A" 1);
   10.62  by Auto_tac;
   10.63  qed "priK_in_initState";
   10.64  AddIffs [priK_in_initState];
   10.65  
   10.66  (*All public keys are visible*)
   10.67 -goal thy "Key (pubK A) : spies evs";
   10.68 +Goal "Key (pubK A) : spies evs";
   10.69  by (induct_tac "evs" 1);
   10.70  by (ALLGOALS (asm_simp_tac
   10.71  	      (simpset() addsimps [imageI, spies_Cons]
   10.72 @@ -80,7 +80,7 @@
   10.73  qed_spec_mp "spies_pubK";
   10.74  
   10.75  (*Spy sees private keys of bad agents!*)
   10.76 -goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
   10.77 +Goal "!!A. A: bad ==> Key (priK A) : spies evs";
   10.78  by (induct_tac "evs" 1);
   10.79  by (ALLGOALS (asm_simp_tac
   10.80  	      (simpset() addsimps [imageI, spies_Cons]
   10.81 @@ -92,7 +92,7 @@
   10.82  
   10.83  
   10.84  (*For not_bad_tac*)
   10.85 -goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
   10.86 +Goal "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
   10.87  \              ==> X : analz (spies evs)";
   10.88  by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
   10.89  qed "Crypt_Spy_analz_bad";
   10.90 @@ -112,13 +112,13 @@
   10.91  
   10.92  (*** Fresh nonces ***)
   10.93  
   10.94 -goal thy "Nonce N ~: parts (initState B)";
   10.95 +Goal "Nonce N ~: parts (initState B)";
   10.96  by (induct_tac "B" 1);
   10.97  by Auto_tac;
   10.98  qed "Nonce_notin_initState";
   10.99  AddIffs [Nonce_notin_initState];
  10.100  
  10.101 -goal thy "Nonce N ~: used []";
  10.102 +Goal "Nonce N ~: used []";
  10.103  by (simp_tac (simpset() addsimps [used_Nil]) 1);
  10.104  qed "Nonce_notin_used_empty";
  10.105  Addsimps [Nonce_notin_used_empty];
  10.106 @@ -127,7 +127,7 @@
  10.107  (*** Supply fresh nonces for possibility theorems. ***)
  10.108  
  10.109  (*In any trace, there is an upper bound N on the greatest nonce in use.*)
  10.110 -goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
  10.111 +Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
  10.112  by (induct_tac "evs" 1);
  10.113  by (res_inst_tac [("x","0")] exI 1);
  10.114  by (ALLGOALS (asm_simp_tac
  10.115 @@ -138,12 +138,12 @@
  10.116  by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
  10.117  val lemma = result();
  10.118  
  10.119 -goal thy "EX N. Nonce N ~: used evs";
  10.120 +Goal "EX N. Nonce N ~: used evs";
  10.121  by (rtac (lemma RS exE) 1);
  10.122  by (Blast_tac 1);
  10.123  qed "Nonce_supply1";
  10.124  
  10.125 -goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  10.126 +Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  10.127  by (rtac (lemma RS exE) 1);
  10.128  by (rtac selectI 1);
  10.129  by (Fast_tac 1);
  10.130 @@ -160,11 +160,11 @@
  10.131  
  10.132  (*** Specialized rewriting for the analz_image_... theorems ***)
  10.133  
  10.134 -goal thy "insert (Key K) H = Key `` {K} Un H";
  10.135 +Goal "insert (Key K) H = Key `` {K} Un H";
  10.136  by (Blast_tac 1);
  10.137  qed "insert_Key_singleton";
  10.138  
  10.139 -goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
  10.140 +Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
  10.141  by (Blast_tac 1);
  10.142  qed "insert_Key_image";
  10.143  
    11.1 --- a/src/HOL/Auth/Recur.ML	Wed Jun 24 10:33:42 1998 +0200
    11.2 +++ b/src/HOL/Auth/Recur.ML	Wed Jun 24 11:24:52 1998 +0200
    11.3 @@ -20,7 +20,7 @@
    11.4  
    11.5  
    11.6  (*Simplest case: Alice goes directly to the server*)
    11.7 -goal thy
    11.8 +Goal
    11.9   "!!A. A ~= Server                                                      \
   11.10  \ ==> EX K NA. EX evs: recur.                                           \
   11.11  \     Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
   11.12 @@ -33,7 +33,7 @@
   11.13  
   11.14  
   11.15  (*Case two: Alice, Bob and the server*)
   11.16 -goal thy
   11.17 +Goal
   11.18   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]                 \
   11.19  \ ==> EX K. EX NA. EX evs: recur.                               \
   11.20  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
   11.21 @@ -52,7 +52,7 @@
   11.22  
   11.23  (*Case three: Alice, Bob, Charlie and the server
   11.24    TOO SLOW to run every time!
   11.25 -goal thy
   11.26 +Goal
   11.27   "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |]   \
   11.28  \ ==> EX K. EX NA. EX evs: recur.                                      \
   11.29  \       Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|},        \
   11.30 @@ -75,7 +75,7 @@
   11.31  (**** Inductive proofs about recur ****)
   11.32  
   11.33  (*Nobody sends themselves messages*)
   11.34 -goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
   11.35 +Goal "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
   11.36  by (etac recur.induct 1);
   11.37  by Auto_tac;
   11.38  qed_spec_mp "not_Says_to_self";
   11.39 @@ -84,17 +84,17 @@
   11.40  
   11.41  
   11.42  
   11.43 -goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
   11.44 +Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
   11.45  by (etac respond.induct 1);
   11.46  by (ALLGOALS Simp_tac);
   11.47  qed "respond_Key_in_parts";
   11.48  
   11.49 -goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
   11.50 +Goal "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
   11.51  by (etac respond.induct 1);
   11.52  by (REPEAT (assume_tac 1));
   11.53  qed "respond_imp_not_used";
   11.54  
   11.55 -goal thy
   11.56 +Goal
   11.57   "!!evs. [| Key K : parts {RB};  (PB,RB,K') : respond evs |] \
   11.58  \        ==> Key K ~: used evs";
   11.59  by (etac rev_mp 1);
   11.60 @@ -104,7 +104,7 @@
   11.61  qed_spec_mp "Key_in_parts_respond";
   11.62  
   11.63  (*Simple inductive reasoning about responses*)
   11.64 -goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
   11.65 +Goal "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
   11.66  by (etac respond.induct 1);
   11.67  by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
   11.68  qed "respond_imp_responses";
   11.69 @@ -114,7 +114,7 @@
   11.70  
   11.71  val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard;
   11.72  
   11.73 -goal thy "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
   11.74 +Goal "!!evs. Says C' B {|Crypt K X, X', RA|} : set evs \
   11.75  \                ==> RA : analz (spies evs)";
   11.76  by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
   11.77  qed "RA4_analz_spies";
   11.78 @@ -144,7 +144,7 @@
   11.79  
   11.80  (** Spy never sees another agent's shared key! (unless it's bad at start) **)
   11.81  
   11.82 -goal thy 
   11.83 +Goal 
   11.84   "!!evs. evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   11.85  by (parts_induct_tac 1);
   11.86  by (Fake_parts_insert_tac 1);
   11.87 @@ -155,7 +155,7 @@
   11.88  qed "Spy_see_shrK";
   11.89  Addsimps [Spy_see_shrK];
   11.90  
   11.91 -goal thy 
   11.92 +Goal 
   11.93   "!!evs. evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   11.94  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   11.95  qed "Spy_analz_shrK";
   11.96 @@ -168,7 +168,7 @@
   11.97  (** Nobody can have used non-existent keys! **)
   11.98  
   11.99  (*The special case of H={} has the same proof*)
  11.100 -goal thy
  11.101 +Goal
  11.102   "!!evs. [| K : keysFor (parts (insert RB H));  (PB,RB,K') : respond evs |] \
  11.103  \        ==> K : range shrK | K : keysFor (parts H)";
  11.104  by (etac rev_mp 1);
  11.105 @@ -177,7 +177,7 @@
  11.106  qed_spec_mp "Key_in_keysFor_parts";
  11.107  
  11.108  
  11.109 -goal thy "!!evs. evs : recur ==>          \
  11.110 +Goal "!!evs. evs : recur ==>          \
  11.111  \                Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
  11.112  by (parts_induct_tac 1);
  11.113  (*RA3*)
  11.114 @@ -209,7 +209,7 @@
  11.115  (*Version for "responses" relation.  Handles case RA3 in the theorem below.  
  11.116    Note that it holds for *any* set H (not just "spies evs")
  11.117    satisfying the inductive hypothesis.*)
  11.118 -goal thy  
  11.119 +Goal  
  11.120   "!!evs. [| RB : responses evs;                             \
  11.121  \           ALL K KK. KK <= Compl (range shrK) -->          \
  11.122  \                     (Key K : analz (Key``KK Un H)) =      \
  11.123 @@ -222,7 +222,7 @@
  11.124  qed "resp_analz_image_freshK_lemma";
  11.125  
  11.126  (*Version for the protocol.  Proof is almost trivial, thanks to the lemma.*)
  11.127 -goal thy  
  11.128 +Goal  
  11.129   "!!evs. evs : recur ==>                                 \
  11.130  \  ALL K KK. KK <= Compl (range shrK) -->                \
  11.131  \            (Key K : analz (Key``KK Un (spies evs))) =  \
  11.132 @@ -250,7 +250,7 @@
  11.133            raw_analz_image_freshK RSN
  11.134              (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp);
  11.135  
  11.136 -goal thy
  11.137 +Goal
  11.138   "!!evs. [| evs : recur;  KAB ~: range shrK |] ==>           \
  11.139  \        Key K : analz (insert (Key KAB) (spies evs)) =      \
  11.140  \        (K = KAB | Key K : analz (spies evs))";
  11.141 @@ -259,7 +259,7 @@
  11.142  
  11.143  
  11.144  (*Everything that's hashed is already in past traffic. *)
  11.145 -goal thy "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
  11.146 +Goal "!!evs. [| Hash {|Key(shrK A), X|} : parts (spies evs);  \
  11.147  \                   evs : recur;  A ~: bad |]                     \
  11.148  \                ==> X : parts (spies evs)";
  11.149  by (etac rev_mp 1);
  11.150 @@ -278,7 +278,7 @@
  11.151    Unicity is not used in other proofs but is desirable in its own right.
  11.152  **)
  11.153  
  11.154 -goal thy 
  11.155 +Goal 
  11.156   "!!evs. [| evs : recur; A ~: bad |]                   \
  11.157  \ ==> EX B' P'. ALL B P.                                     \
  11.158  \        Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \
  11.159 @@ -295,7 +295,7 @@
  11.160                                 addSEs spies_partsEs) 1));
  11.161  val lemma = result();
  11.162  
  11.163 -goalw thy [HPair_def]
  11.164 +Goalw [HPair_def]
  11.165   "!!A.[| Hash[Key(shrK A)] {|Agent A, B,NA,P|}   : parts (spies evs); \
  11.166  \        Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \
  11.167  \        evs : recur;  A ~: bad |]                                    \
  11.168 @@ -309,7 +309,7 @@
  11.169        (relations "respond" and "responses") 
  11.170  ***)
  11.171  
  11.172 -goal thy
  11.173 +Goal
  11.174   "!!evs. [| RB : responses evs;  evs : recur |] \
  11.175  \ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)";
  11.176  by (etac responses.induct 1);
  11.177 @@ -321,7 +321,7 @@
  11.178  Addsimps [shrK_in_analz_respond];
  11.179  
  11.180  
  11.181 -goal thy  
  11.182 +Goal  
  11.183   "!!evs. [| RB : responses evs;                             \
  11.184  \           ALL K KK. KK <= Compl (range shrK) -->          \
  11.185  \                     (Key K : analz (Key``KK Un H)) =      \
  11.186 @@ -344,7 +344,7 @@
  11.187  
  11.188  (*The Server does not send such messages.  This theorem lets us avoid
  11.189    assuming B~=Server in RA4.*)
  11.190 -goal thy 
  11.191 +Goal 
  11.192   "!!evs. evs : recur \
  11.193  \        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
  11.194  by (etac recur.induct 1);
  11.195 @@ -355,7 +355,7 @@
  11.196  
  11.197  
  11.198  (*The last key returned by respond indeed appears in a certificate*)
  11.199 -goal thy 
  11.200 +Goal 
  11.201   "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
  11.202  \      ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
  11.203  by (etac respond.elim 1);
  11.204 @@ -363,7 +363,7 @@
  11.205  qed "respond_certificate";
  11.206  
  11.207  
  11.208 -goal thy 
  11.209 +Goal 
  11.210   "!!K'. (PB,RB,KXY) : respond evs                          \
  11.211  \  ==> EX A' B'. ALL A B N.                                \
  11.212  \        Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
  11.213 @@ -385,7 +385,7 @@
  11.214  by (Fast_tac 1);
  11.215  val lemma = result();
  11.216  
  11.217 -goal thy 
  11.218 +Goal 
  11.219   "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB};      \
  11.220  \          Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB};   \
  11.221  \          (PB,RB,KXY) : respond evs |]                            \
  11.222 @@ -398,7 +398,7 @@
  11.223      Does not in itself guarantee security: an attack could violate 
  11.224      the premises, e.g. by having A=Spy **)
  11.225  
  11.226 -goal thy 
  11.227 +Goal 
  11.228   "!!evs. [| (PB,RB,KAB) : respond evs;  evs : recur |]              \
  11.229  \        ==> ALL A A' N. A ~: bad & A' ~: bad -->                   \
  11.230  \            Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} -->  \
  11.231 @@ -429,7 +429,7 @@
  11.232  qed_spec_mp "respond_Spy_not_see_session_key";
  11.233  
  11.234  
  11.235 -goal thy
  11.236 +Goal
  11.237   "!!evs. [| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \
  11.238  \           A ~: bad;  A' ~: bad;  evs : recur |]                      \
  11.239  \        ==> Key K ~: analz (spies evs)";
  11.240 @@ -463,7 +463,7 @@
  11.241  (**** Authenticity properties for Agents ****)
  11.242  
  11.243  (*The response never contains Hashes*)
  11.244 -goal thy
  11.245 +Goal
  11.246   "!!evs. [| Hash {|Key (shrK B), M|} : parts (insert RB H); \
  11.247  \           (PB,RB,K) : respond evs |]                      \
  11.248  \        ==> Hash {|Key (shrK B), M|} : parts H";
  11.249 @@ -476,7 +476,7 @@
  11.250    This result is of no use to B, who cannot verify the Hash.  Moreover,
  11.251    it can say nothing about how recent A's message is.  It might later be
  11.252    used to prove B's presence to A at the run's conclusion.*)
  11.253 -goalw thy [HPair_def]
  11.254 +Goalw [HPair_def]
  11.255   "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \
  11.256  \           A ~: bad;  evs : recur |]                      \
  11.257  \     ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs";
  11.258 @@ -493,7 +493,7 @@
  11.259  
  11.260  
  11.261  (*Certificates can only originate with the Server.*)
  11.262 -goal thy 
  11.263 +Goal 
  11.264   "!!evs. [| Crypt (shrK A) Y : parts (spies evs);    \
  11.265  \           A ~: bad;  evs : recur |]                \
  11.266  \        ==> EX C RC. Says Server C RC : set evs  &  \
    12.1 --- a/src/HOL/Auth/Shared.ML	Wed Jun 24 10:33:42 1998 +0200
    12.2 +++ b/src/HOL/Auth/Shared.ML	Wed Jun 24 11:24:52 1998 +0200
    12.3 @@ -22,14 +22,14 @@
    12.4  (** Rewrites should not refer to  initState(Friend i) 
    12.5      -- not in normal form! **)
    12.6  
    12.7 -goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    12.8 +Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
    12.9  by (induct_tac "C" 1);
   12.10  by Auto_tac;
   12.11  qed "keysFor_parts_initState";
   12.12  Addsimps [keysFor_parts_initState];
   12.13  
   12.14  (*Specialized to shared-key model: no need for addss in protocol proofs*)
   12.15 -goal thy "!!X. [| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
   12.16 +Goal "!!X. [| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
   12.17  \              ==> K : keysFor (parts H) | Key K : parts H";
   12.18  by (fast_tac
   12.19        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
   12.20 @@ -38,7 +38,7 @@
   12.21                  addss  (simpset())) 1);
   12.22  qed "keysFor_parts_insert";
   12.23  
   12.24 -goal thy "!!H. Crypt K X : H ==> K : keysFor H";
   12.25 +Goal "!!H. Crypt K X : H ==> K : keysFor H";
   12.26  by (dtac Crypt_imp_invKey_keysFor 1);
   12.27  by (Asm_full_simp_tac 1);
   12.28  qed "Crypt_imp_keysFor";
   12.29 @@ -47,7 +47,7 @@
   12.30  (*** Function "spies" ***)
   12.31  
   12.32  (*Spy sees shared keys of agents!*)
   12.33 -goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
   12.34 +Goal "!!A. A: bad ==> Key (shrK A) : spies evs";
   12.35  by (induct_tac "evs" 1);
   12.36  by (ALLGOALS (asm_simp_tac
   12.37  	      (simpset() addsimps [imageI, spies_Cons]
   12.38 @@ -57,7 +57,7 @@
   12.39  AddSIs [Spy_spies_bad];
   12.40  
   12.41  (*For not_bad_tac*)
   12.42 -goal thy "!!A. [| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
   12.43 +Goal "!!A. [| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
   12.44  \              ==> X : analz (spies evs)";
   12.45  by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1);
   12.46  qed "Crypt_Spy_analz_bad";
   12.47 @@ -78,13 +78,13 @@
   12.48  (** Fresh keys never clash with long-term shared keys **)
   12.49  
   12.50  (*Agents see their own shared keys!*)
   12.51 -goal thy "Key (shrK A) : initState A";
   12.52 +Goal "Key (shrK A) : initState A";
   12.53  by (induct_tac "A" 1);
   12.54  by Auto_tac;
   12.55  qed "shrK_in_initState";
   12.56  AddIffs [shrK_in_initState];
   12.57  
   12.58 -goal thy "Key (shrK A) : used evs";
   12.59 +Goal "Key (shrK A) : used evs";
   12.60  by (rtac initState_into_used 1);
   12.61  by (Blast_tac 1);
   12.62  qed "shrK_in_used";
   12.63 @@ -92,11 +92,11 @@
   12.64  
   12.65  (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
   12.66    from long-term shared keys*)
   12.67 -goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
   12.68 +Goal "!!K. Key K ~: used evs ==> K ~: range shrK";
   12.69  by (Blast_tac 1);
   12.70  qed "Key_not_used";
   12.71  
   12.72 -goal thy "!!K. Key K ~: used evs ==> shrK B ~= K";
   12.73 +Goal "!!K. Key K ~: used evs ==> shrK B ~= K";
   12.74  by (Blast_tac 1);
   12.75  qed "shrK_neq";
   12.76  
   12.77 @@ -105,13 +105,13 @@
   12.78  
   12.79  (*** Fresh nonces ***)
   12.80  
   12.81 -goal thy "Nonce N ~: parts (initState B)";
   12.82 +Goal "Nonce N ~: parts (initState B)";
   12.83  by (induct_tac "B" 1);
   12.84  by Auto_tac;
   12.85  qed "Nonce_notin_initState";
   12.86  AddIffs [Nonce_notin_initState];
   12.87  
   12.88 -goal thy "Nonce N ~: used []";
   12.89 +Goal "Nonce N ~: used []";
   12.90  by (simp_tac (simpset() addsimps [used_Nil]) 1);
   12.91  qed "Nonce_notin_used_empty";
   12.92  Addsimps [Nonce_notin_used_empty];
   12.93 @@ -120,7 +120,7 @@
   12.94  (*** Supply fresh nonces for possibility theorems. ***)
   12.95  
   12.96  (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   12.97 -goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   12.98 +Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   12.99  by (induct_tac "evs" 1);
  12.100  by (res_inst_tac [("x","0")] exI 1);
  12.101  by (ALLGOALS (asm_simp_tac
  12.102 @@ -131,12 +131,12 @@
  12.103  by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
  12.104  val lemma = result();
  12.105  
  12.106 -goal thy "EX N. Nonce N ~: used evs";
  12.107 +Goal "EX N. Nonce N ~: used evs";
  12.108  by (rtac (lemma RS exE) 1);
  12.109  by (Blast_tac 1);
  12.110  qed "Nonce_supply1";
  12.111  
  12.112 -goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
  12.113 +Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
  12.114  by (cut_inst_tac [("evs","evs")] lemma 1);
  12.115  by (cut_inst_tac [("evs","evs'")] lemma 1);
  12.116  by (Clarify_tac 1);
  12.117 @@ -147,7 +147,7 @@
  12.118  				     le_eq_less_Suc RS sym]) 1);
  12.119  qed "Nonce_supply2";
  12.120  
  12.121 -goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
  12.122 +Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
  12.123  \                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
  12.124  by (cut_inst_tac [("evs","evs")] lemma 1);
  12.125  by (cut_inst_tac [("evs","evs'")] lemma 1);
  12.126 @@ -161,7 +161,7 @@
  12.127  				     le_eq_less_Suc RS sym]) 1);
  12.128  qed "Nonce_supply3";
  12.129  
  12.130 -goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  12.131 +Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
  12.132  by (rtac (lemma RS exE) 1);
  12.133  by (rtac selectI 1);
  12.134  by (Blast_tac 1);
  12.135 @@ -169,12 +169,12 @@
  12.136  
  12.137  (*** Supply fresh keys for possibility theorems. ***)
  12.138  
  12.139 -goal thy "EX K. Key K ~: used evs";
  12.140 +Goal "EX K. Key K ~: used evs";
  12.141  by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
  12.142  by (Blast_tac 1);
  12.143  qed "Key_supply1";
  12.144  
  12.145 -goal thy "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
  12.146 +Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
  12.147  by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
  12.148  by (etac exE 1);
  12.149  by (cut_inst_tac [("evs","evs'")] 
  12.150 @@ -182,7 +182,7 @@
  12.151  by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
  12.152  qed "Key_supply2";
  12.153  
  12.154 -goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
  12.155 +Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
  12.156  \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
  12.157  by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
  12.158  by (etac exE 1);
  12.159 @@ -195,7 +195,7 @@
  12.160  by (Blast_tac 1);
  12.161  qed "Key_supply3";
  12.162  
  12.163 -goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
  12.164 +Goal "Key (@ K. Key K ~: used evs) ~: used evs";
  12.165  by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
  12.166  by (rtac selectI 1);
  12.167  by (Blast_tac 1);
  12.168 @@ -223,15 +223,15 @@
  12.169  
  12.170  (*** Specialized rewriting for analz_insert_freshK ***)
  12.171  
  12.172 -goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
  12.173 +Goal "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
  12.174  by (Blast_tac 1);
  12.175  qed "subset_Compl_range";
  12.176  
  12.177 -goal thy "insert (Key K) H = Key `` {K} Un H";
  12.178 +Goal "insert (Key K) H = Key `` {K} Un H";
  12.179  by (Blast_tac 1);
  12.180  qed "insert_Key_singleton";
  12.181  
  12.182 -goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
  12.183 +Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
  12.184  by (Blast_tac 1);
  12.185  qed "insert_Key_image";
  12.186  
  12.187 @@ -249,7 +249,7 @@
  12.188                          @disj_comms);
  12.189  
  12.190  (*Lemma for the trivial direction of the if-and-only-if*)
  12.191 -goal thy  
  12.192 +Goal  
  12.193   "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
  12.194  \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
  12.195  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
    13.1 --- a/src/HOL/Auth/TLS.ML	Wed Jun 24 10:33:42 1998 +0200
    13.2 +++ b/src/HOL/Auth/TLS.ML	Wed Jun 24 11:24:52 1998 +0200
    13.3 @@ -34,13 +34,13 @@
    13.4  
    13.5  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
    13.6  
    13.7 -goal thy "pubK A ~= sessionK arg";
    13.8 +Goal "pubK A ~= sessionK arg";
    13.9  by (rtac notI 1);
   13.10  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
   13.11  by (Full_simp_tac 1);
   13.12  qed "pubK_neq_sessionK";
   13.13  
   13.14 -goal thy "priK A ~= sessionK arg";
   13.15 +Goal "priK A ~= sessionK arg";
   13.16  by (rtac notI 1);
   13.17  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
   13.18  by (Full_simp_tac 1);
   13.19 @@ -64,7 +64,7 @@
   13.20  
   13.21  
   13.22  (*Possibility property ending with ClientAccepts.*)
   13.23 -goal thy 
   13.24 +Goal 
   13.25   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   13.26  \           A ~= B |]            \
   13.27  \  ==> EX SID M. EX evs: tls.    \
   13.28 @@ -78,7 +78,7 @@
   13.29  result();
   13.30  
   13.31  (*And one for ServerAccepts.  Either FINISHED message may come first.*)
   13.32 -goal thy 
   13.33 +Goal 
   13.34   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   13.35  \           A ~= B |]                        \
   13.36  \  ==> EX SID NA PA NB PB M. EX evs: tls.    \
   13.37 @@ -92,7 +92,7 @@
   13.38  result();
   13.39  
   13.40  (*Another one, for CertVerify (which is optional)*)
   13.41 -goal thy 
   13.42 +Goal 
   13.43   "!!A B. [| ALL evs. (@ N. Nonce N ~: used evs) ~: range PRF;  \
   13.44  \           A ~= B |]                       \
   13.45  \  ==> EX NB PMS. EX evs: tls.   \
   13.46 @@ -105,7 +105,7 @@
   13.47  result();
   13.48  
   13.49  (*Another one, for session resumption (both ServerResume and ClientResume) *)
   13.50 -goal thy 
   13.51 +Goal 
   13.52   "!!A B. [| evs0 : tls;     \
   13.53  \           Notes A {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   13.54  \           Notes B {|Number SID, Agent A, Agent B, Nonce M|} : set evs0; \
   13.55 @@ -128,7 +128,7 @@
   13.56  (**** Inductive proofs about tls ****)
   13.57  
   13.58  (*Nobody sends themselves messages*)
   13.59 -goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   13.60 +Goal "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
   13.61  by (etac tls.induct 1);
   13.62  by Auto_tac;
   13.63  qed_spec_mp "not_Says_to_self";
   13.64 @@ -152,14 +152,14 @@
   13.65      sends messages containing X! **)
   13.66  
   13.67  (*Spy never sees another agent's private key! (unless it's bad at start)*)
   13.68 -goal thy 
   13.69 +Goal 
   13.70   "!!evs. evs : tls ==> (Key (priK A) : parts (spies evs)) = (A : bad)";
   13.71  by (parts_induct_tac 1);
   13.72  by (Fake_parts_insert_tac 1);
   13.73  qed "Spy_see_priK";
   13.74  Addsimps [Spy_see_priK];
   13.75  
   13.76 -goal thy 
   13.77 +Goal 
   13.78   "!!evs. evs : tls ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
   13.79  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   13.80  qed "Spy_analz_priK";
   13.81 @@ -173,7 +173,7 @@
   13.82    model to include bogus certificates for the agents, but there seems
   13.83    little point in doing so: the loss of their private keys is a worse
   13.84    breach of security.*)
   13.85 -goalw thy [certificate_def]
   13.86 +Goalw [certificate_def]
   13.87   "!!evs. [| certificate B KB : parts (spies evs);  evs : tls |]  \
   13.88  \        ==> pubK B = KB";
   13.89  by (etac rev_mp 1);
   13.90 @@ -203,7 +203,7 @@
   13.91  
   13.92  (*** Properties of items found in Notes ***)
   13.93  
   13.94 -goal thy "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   13.95 +Goal "!!evs. [| Notes A {|Agent B, X|} : set evs;  evs : tls |]  \
   13.96  \                ==> Crypt (pubK B) X : parts (spies evs)";
   13.97  by (etac rev_mp 1);
   13.98  by (analz_induct_tac 1);
   13.99 @@ -211,7 +211,7 @@
  13.100  qed "Notes_Crypt_parts_spies";
  13.101  
  13.102  (*C may be either A or B*)
  13.103 -goal thy
  13.104 +Goal
  13.105   "!!evs. [| Notes C {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs; \
  13.106  \           evs : tls     \
  13.107  \        |] ==> Crypt (pubK B) (Nonce PMS) : parts (spies evs)";
  13.108 @@ -226,7 +226,7 @@
  13.109  qed "Notes_master_imp_Crypt_PMS";
  13.110  
  13.111  (*Compared with the theorem above, both premise and conclusion are stronger*)
  13.112 -goal thy
  13.113 +Goal
  13.114   "!!evs. [| Notes A {|s, Agent A, Agent B, Nonce(PRF(PMS,NA,NB))|} : set evs;\
  13.115  \           evs : tls     \
  13.116  \        |] ==> Notes A {|Agent B, Nonce PMS|} : set evs";
  13.117 @@ -240,7 +240,7 @@
  13.118  (*** Protocol goal: if B receives CertVerify, then A sent it ***)
  13.119  
  13.120  (*B can check A's signature if he has received A's certificate.*)
  13.121 -goal thy
  13.122 +Goal
  13.123   "!!evs. [| X : parts (spies evs);                          \
  13.124  \           X = Crypt (priK A) (Hash{|nb, Agent B, pms|});  \
  13.125  \           evs : tls;  A ~: bad |]                         \
  13.126 @@ -252,7 +252,7 @@
  13.127  val lemma = result();
  13.128  
  13.129  (*Final version: B checks X using the distributed KA instead of priK A*)
  13.130 -goal thy
  13.131 +Goal
  13.132   "!!evs. [| X : parts (spies evs);                            \
  13.133  \           X = Crypt (invKey KA) (Hash{|nb, Agent B, pms|}); \
  13.134  \           certificate A KA : parts (spies evs);             \
  13.135 @@ -263,7 +263,7 @@
  13.136  
  13.137  
  13.138  (*If CertVerify is present then A has chosen PMS.*)
  13.139 -goal thy
  13.140 +Goal
  13.141   "!!evs. [| Crypt (priK A) (Hash{|nb, Agent B, Nonce PMS|}) \
  13.142  \             : parts (spies evs);                          \
  13.143  \           evs : tls;  A ~: bad |]                         \
  13.144 @@ -274,7 +274,7 @@
  13.145  val lemma = result();
  13.146  
  13.147  (*Final version using the distributed KA instead of priK A*)
  13.148 -goal thy
  13.149 +Goal
  13.150   "!!evs. [| Crypt (invKey KA) (Hash{|nb, Agent B, Nonce PMS|}) \
  13.151  \             : parts (spies evs);                             \
  13.152  \           certificate A KA : parts (spies evs);              \
  13.153 @@ -284,7 +284,7 @@
  13.154  qed "UseCertVerify";
  13.155  
  13.156  
  13.157 -goal thy "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
  13.158 +Goal "!!evs. evs : tls ==> Notes A {|Agent B, Nonce (PRF x)|} ~: set evs";
  13.159  by (parts_induct_tac 1);
  13.160  (*ClientKeyExch: PMS is assumed to differ from any PRF.*)
  13.161  by (Blast_tac 1);
  13.162 @@ -292,7 +292,7 @@
  13.163  Addsimps [no_Notes_A_PRF];
  13.164  
  13.165  
  13.166 -goal thy "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
  13.167 +Goal "!!evs. [| Nonce (PRF (PMS,NA,NB)) : parts (spies evs);  \
  13.168  \                   evs : tls |]  \
  13.169  \                ==> Nonce PMS : parts (spies evs)";
  13.170  by (etac rev_mp 1);
  13.171 @@ -309,7 +309,7 @@
  13.172  (*** Unicity results for PMS, the pre-master-secret ***)
  13.173  
  13.174  (*PMS determines B.  Proof borrowed from NS_Public/unique_NA and from Yahalom*)
  13.175 -goal thy 
  13.176 +Goal 
  13.177   "!!evs. [| Nonce PMS ~: analz (spies evs);  evs : tls |]   \
  13.178  \        ==> EX B'. ALL B.   \
  13.179  \              Crypt (pubK B) (Nonce PMS) : parts (spies evs) --> B=B'";
  13.180 @@ -323,7 +323,7 @@
  13.181      blast_tac (claset() addSEs partsEs) 1);
  13.182  val lemma = result();
  13.183  
  13.184 -goal thy 
  13.185 +Goal 
  13.186   "!!evs. [| Crypt(pubK B)  (Nonce PMS) : parts (spies evs); \
  13.187  \           Crypt(pubK B') (Nonce PMS) : parts (spies evs); \
  13.188  \           Nonce PMS ~: analz (spies evs);                 \
  13.189 @@ -340,7 +340,7 @@
  13.190  **)
  13.191  
  13.192  (*In A's internal Note, PMS determines A and B.*)
  13.193 -goal thy "!!evs. evs : tls               \
  13.194 +Goal "!!evs. evs : tls               \
  13.195  \                ==> EX A' B'. ALL A B.  \
  13.196  \                    Notes A {|Agent B, Nonce PMS|} : set evs --> A=A' & B=B'";
  13.197  by (parts_induct_tac 1);
  13.198 @@ -350,7 +350,7 @@
  13.199      blast_tac (claset() addSDs [Notes_Crypt_parts_spies] addSEs partsEs) 1);
  13.200  val lemma = result();
  13.201  
  13.202 -goal thy 
  13.203 +Goal 
  13.204   "!!evs. [| Notes A  {|Agent B,  Nonce PMS|} : set evs;  \
  13.205  \           Notes A' {|Agent B', Nonce PMS|} : set evs;  \
  13.206  \           evs : tls |]                               \
  13.207 @@ -364,7 +364,7 @@
  13.208  
  13.209  (*Key compromise lemma needed to prove analz_image_keys.
  13.210    No collection of keys can help the spy get new private keys.*)
  13.211 -goal thy  
  13.212 +Goal  
  13.213   "!!evs. evs : tls ==>                                      \
  13.214  \  ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \
  13.215  \          (priK B : KK | B : bad)";
  13.216 @@ -378,12 +378,12 @@
  13.217  
  13.218  
  13.219  (*slightly speeds up the big simplification below*)
  13.220 -goal thy "!!evs. KK <= range sessionK ==> priK B ~: KK";
  13.221 +Goal "!!evs. KK <= range sessionK ==> priK B ~: KK";
  13.222  by (Blast_tac 1);
  13.223  val range_sessionkeys_not_priK = result();
  13.224  
  13.225  (*Lemma for the trivial direction of the if-and-only-if*)
  13.226 -goal thy  
  13.227 +Goal  
  13.228   "!!evs. (X : analz (G Un H)) --> (X : analz H)  ==> \
  13.229  \        (X : analz (G Un H))  =  (X : analz H)";
  13.230  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
  13.231 @@ -394,7 +394,7 @@
  13.232  \           (Nonce N : analz (spies evs))";
  13.233  **)
  13.234  
  13.235 -goal thy  
  13.236 +Goal  
  13.237   "!!evs. evs : tls ==>                                    \
  13.238  \    ALL KK. KK <= range sessionK -->                     \
  13.239  \            (Nonce N : analz (Key``KK Un (spies evs))) = \
  13.240 @@ -403,7 +403,7 @@
  13.241  by (ClientKeyExch_tac 7);
  13.242  by (REPEAT_FIRST (resolve_tac [allI, impI]));
  13.243  by (REPEAT_FIRST (rtac analz_image_keys_lemma));
  13.244 -by (ALLGOALS    (*18 seconds*)
  13.245 +by (ALLGOALS    (*4.5 seconds*)
  13.246      (asm_simp_tac (analz_image_keys_ss 
  13.247  		   addsimps (split_ifs@pushes)
  13.248  		   addsimps [range_sessionkeys_not_priK, 
  13.249 @@ -414,7 +414,7 @@
  13.250  qed_spec_mp "analz_image_keys";
  13.251  
  13.252  (*Knowing some session keys is no help in getting new nonces*)
  13.253 -goal thy
  13.254 +Goal
  13.255   "!!evs. evs : tls ==>          \
  13.256  \        Nonce N : analz (insert (Key (sessionK z)) (spies evs)) =  \
  13.257  \        (Nonce N : analz (spies evs))";
  13.258 @@ -432,7 +432,7 @@
  13.259    Nonces don't have to agree, allowing session resumption.
  13.260    Converse doesn't hold; revealing PMS doesn't force the keys to be sent.
  13.261    THEY ARE NOT SUITABLE AS SAFE ELIM RULES.*)
  13.262 -goal thy 
  13.263 +Goal 
  13.264   "!!evs. [| Nonce PMS ~: parts (spies evs);  \
  13.265  \           K = sessionK((Na, Nb, PRF(PMS,NA,NB)), b);  \
  13.266  \           evs : tls |]             \
  13.267 @@ -455,14 +455,14 @@
  13.268                           addSEs spies_partsEs) 1));
  13.269  val lemma = result();
  13.270  
  13.271 -goal thy 
  13.272 +Goal 
  13.273   "!!evs. [| Key (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) : parts (spies evs); \
  13.274  \           evs : tls |]             \
  13.275  \        ==> Nonce PMS : parts (spies evs)";
  13.276  by (blast_tac (claset() addDs [lemma]) 1);
  13.277  qed "PMS_sessionK_not_spied";
  13.278  
  13.279 -goal thy 
  13.280 +Goal 
  13.281   "!!evs. [| Crypt (sessionK((Na, Nb, PRF(PMS,NA,NB)), b)) Y  \
  13.282  \             : parts (spies evs);  evs : tls |]             \
  13.283  \        ==> Nonce PMS : parts (spies evs)";
  13.284 @@ -473,7 +473,7 @@
  13.285    Converse doesn't hold; betraying M doesn't force the keys to be sent!
  13.286    The strong Oops condition can be weakened later by unicity reasoning, 
  13.287  	with some effort.*)
  13.288 -goal thy 
  13.289 +Goal 
  13.290   "!!evs. [| ALL A. Says A Spy (Key (sessionK((NA,NB,M),b))) ~: set evs; \
  13.291  \           Nonce M ~: analz (spies evs);  evs : tls |]   \
  13.292  \        ==> Key (sessionK((NA,NB,M),b)) ~: parts (spies evs)";
  13.293 @@ -491,7 +491,7 @@
  13.294  
  13.295  
  13.296  (*If A sends ClientKeyExch to an honest B, then the PMS will stay secret.*)
  13.297 -goal thy
  13.298 +Goal
  13.299   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
  13.300  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
  13.301  \            Nonce PMS ~: analz (spies evs)";
  13.302 @@ -513,7 +513,7 @@
  13.303  
  13.304  (*If A sends ClientKeyExch to an honest B, then the MASTER SECRET
  13.305    will stay secret.*)
  13.306 -goal thy
  13.307 +Goal
  13.308   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]           \
  13.309  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs  -->   \
  13.310  \            Nonce (PRF(PMS,NA,NB)) ~: analz (spies evs)";
  13.311 @@ -541,7 +541,7 @@
  13.312  
  13.313  (*If A created PMS then nobody other than the Spy would send a message
  13.314    using a clientK generated from that PMS.*)
  13.315 -goal thy
  13.316 +Goal
  13.317   "!!evs. [| evs : tls;  A' ~= Spy |]                \
  13.318  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
  13.319  \      Says A' B' (Crypt (clientK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
  13.320 @@ -561,7 +561,7 @@
  13.321  
  13.322  (*If A created PMS and has not leaked her clientK to the Spy, 
  13.323    then nobody has.*)
  13.324 -goal thy
  13.325 +Goal
  13.326   "!!evs. evs : tls                         \
  13.327  \  ==> Says A Spy (Key(clientK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
  13.328  \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
  13.329 @@ -585,7 +585,7 @@
  13.330  
  13.331  (*If A created PMS for B, then nobody other than B or the Spy would
  13.332    send a message using a serverK generated from that PMS.*)
  13.333 -goal thy
  13.334 +Goal
  13.335   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad;  B' ~= Spy |]                \
  13.336  \  ==> Notes A {|Agent B, Nonce PMS|} : set evs -->                  \
  13.337  \      Says B' A' (Crypt (serverK(Na,Nb,PRF(PMS,NA,NB))) Y) : set evs -->  \
  13.338 @@ -608,7 +608,7 @@
  13.339  
  13.340  (*If A created PMS for B, and B has not leaked his serverK to the Spy, 
  13.341    then nobody has.*)
  13.342 -goal thy
  13.343 +Goal
  13.344   "!!evs. [| evs : tls;  A ~: bad;  B ~: bad |]                        \
  13.345  \  ==> Says B Spy (Key(serverK(Na,Nb,PRF(PMS,NA,NB)))) ~: set evs --> \
  13.346  \      Notes A {|Agent B, Nonce PMS|} : set evs -->                   \
  13.347 @@ -634,7 +634,7 @@
  13.348  ***)
  13.349  
  13.350  (*The mention of her name (A) in X assures A that B knows who she is.*)
  13.351 -goal thy
  13.352 +Goal
  13.353   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
  13.354  \                 (Hash{|Number SID, Nonce M,             \
  13.355  \                        Nonce Na, Number PA, Agent A,    \
  13.356 @@ -659,7 +659,7 @@
  13.357  val lemma = normalize_thm [RSmp] (result());
  13.358  
  13.359  (*Final version*)
  13.360 -goal thy
  13.361 +Goal
  13.362   "!!evs. [| X = Crypt (serverK(Na,Nb,M))                  \
  13.363  \                 (Hash{|Number SID, Nonce M,             \
  13.364  \                        Nonce Na, Number PA, Agent A,    \
  13.365 @@ -681,7 +681,7 @@
  13.366    have changed A's identity in all other messages, so we can't be sure
  13.367    that B sends his message to A.  If CLIENT KEY EXCHANGE were augmented
  13.368    to bind A's identity with PMS, then we could replace A' by A below.*)
  13.369 -goal thy
  13.370 +Goal
  13.371   "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |]     \
  13.372  \        ==> (ALL A. Says A Spy (Key(serverK(Na,Nb,M))) ~: set evs) --> \
  13.373  \            Notes A {|Agent B, Nonce PMS|} : set evs -->              \
  13.374 @@ -709,7 +709,7 @@
  13.375  val lemma = normalize_thm [RSmp] (result());
  13.376  
  13.377  (*Final version*)
  13.378 -goal thy
  13.379 +Goal
  13.380   "!!evs. [| M = PRF(PMS,NA,NB);                           \
  13.381  \           Crypt (serverK(Na,Nb,M)) Y : parts (spies evs); \
  13.382  \           Notes A {|Agent B, Nonce PMS|} : set evs;     \
  13.383 @@ -728,7 +728,7 @@
  13.384       ClientFinished, then B can then check the quoted values PA, PB, etc.
  13.385  ***)
  13.386  
  13.387 -goal thy
  13.388 +Goal
  13.389   "!!evs. [| M = PRF(PMS,NA,NB);  evs : tls;  A ~: bad;  B ~: bad |] \
  13.390  \    ==> (ALL A. Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs) --> \
  13.391  \        Notes A {|Agent B, Nonce PMS|} : set evs -->               \
  13.392 @@ -751,7 +751,7 @@
  13.393  val lemma = normalize_thm [RSmp] (result());
  13.394  
  13.395  (*Final version*)
  13.396 -goal thy
  13.397 +Goal
  13.398   "!!evs. [| M = PRF(PMS,NA,NB);                           \
  13.399  \           Crypt (clientK(Na,Nb,M)) Y : parts (spies evs);  \
  13.400  \           Notes A {|Agent B, Nonce PMS|} : set evs;        \
  13.401 @@ -768,7 +768,7 @@
  13.402       check a CertVerify from A, then A has used the quoted
  13.403       values PA, PB, etc.  Even this one requires A to be uncompromised.
  13.404   ***)
  13.405 -goal thy
  13.406 +Goal
  13.407   "!!evs. [| M = PRF(PMS,NA,NB);                           \
  13.408  \           Says A Spy (Key(clientK(Na,Nb,M))) ~: set evs;\
  13.409  \           Says A' B (Crypt (clientK(Na,Nb,M)) Y) : set evs; \
    14.1 --- a/src/HOL/Auth/WooLam.ML	Wed Jun 24 10:33:42 1998 +0200
    14.2 +++ b/src/HOL/Auth/WooLam.ML	Wed Jun 24 11:24:52 1998 +0200
    14.3 @@ -21,7 +21,7 @@
    14.4  
    14.5  
    14.6  (*A "possibility property": there are traces that reach the end*)
    14.7 -goal thy 
    14.8 +Goal 
    14.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   14.10  \        ==> EX NB. EX evs: woolam.               \
   14.11  \              Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs";
   14.12 @@ -35,7 +35,7 @@
   14.13  (**** Inductive proofs about woolam ****)
   14.14  
   14.15  (*Nobody sends themselves messages*)
   14.16 -goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
   14.17 +Goal "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
   14.18  by (etac woolam.induct 1);
   14.19  by Auto_tac;
   14.20  qed_spec_mp "not_Says_to_self";
   14.21 @@ -45,7 +45,7 @@
   14.22  
   14.23  (** For reasoning about the encrypted portion of messages **)
   14.24  
   14.25 -goal thy "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
   14.26 +Goal "!!evs. Says A' B X : set evs ==> X : analz (spies evs)";
   14.27  by (etac (Says_imp_spies RS analz.Inj) 1);
   14.28  qed "WL4_analz_spies";
   14.29  
   14.30 @@ -63,14 +63,14 @@
   14.31      sends messages containing X! **)
   14.32  
   14.33  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
   14.34 -goal thy 
   14.35 +Goal 
   14.36   "!!evs. evs : woolam ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   14.37  by (parts_induct_tac 1);
   14.38  by (Blast_tac 1);
   14.39  qed "Spy_see_shrK";
   14.40  Addsimps [Spy_see_shrK];
   14.41  
   14.42 -goal thy 
   14.43 +Goal 
   14.44   "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   14.45  by Auto_tac;
   14.46  qed "Spy_analz_shrK";
   14.47 @@ -86,7 +86,7 @@
   14.48  (*** WL4 ***)
   14.49  
   14.50  (*If the encrypted message appears then it originated with Alice*)
   14.51 -goal thy 
   14.52 +Goal 
   14.53   "!!evs. [| Crypt (shrK A) (Nonce NB) : parts (spies evs);  \
   14.54  \           A ~: bad;  evs : woolam |]                      \
   14.55  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   14.56 @@ -98,7 +98,7 @@
   14.57  (*Guarantee for Server: if it gets a message containing a certificate from 
   14.58    Alice, then she originated that certificate.  But we DO NOT know that B
   14.59    ever saw it: the Spy may have rerouted the message to the Server.*)
   14.60 -goal thy 
   14.61 +Goal 
   14.62   "!!evs. [| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \
   14.63  \             : set evs;                                                   \
   14.64  \           A ~: bad;  evs : woolam |]                                     \
   14.65 @@ -112,7 +112,7 @@
   14.66  (*** WL5 ***)
   14.67  
   14.68  (*Server sent WL5 only if it received the right sort of message*)
   14.69 -goal thy 
   14.70 +Goal 
   14.71   "!!evs. [| Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs;      \
   14.72  \           evs : woolam |]                                                \
   14.73  \        ==> EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \
   14.74 @@ -125,7 +125,7 @@
   14.75  AddDs [Server_sent_WL5];
   14.76  
   14.77  (*If the encrypted message appears then it originated with the Server!*)
   14.78 -goal thy 
   14.79 +Goal 
   14.80   "!!evs. [| Crypt (shrK B) {|Agent A, NB|} : parts (spies evs);  \
   14.81  \           B ~: bad;  evs : woolam |]                           \
   14.82  \        ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set evs";
   14.83 @@ -138,7 +138,7 @@
   14.84    the nonce using her key.  This event can be no older than the nonce itself.
   14.85    But A may have sent the nonce to some other agent and it could have reached
   14.86    the Server via the Spy.*)
   14.87 -goal thy 
   14.88 +Goal 
   14.89   "!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \
   14.90  \           A ~: bad;  B ~: bad;  evs : woolam  |]                  \
   14.91  \        ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs";
   14.92 @@ -147,7 +147,7 @@
   14.93  
   14.94  
   14.95  (*B only issues challenges in response to WL1.  Not used.*)
   14.96 -goal thy 
   14.97 +Goal 
   14.98   "!!evs. [| Says B A (Nonce NB) : set evs;  B ~= Spy;  evs : woolam |]  \
   14.99  \        ==> EX A'. Says A' B (Agent A) : set evs";
  14.100  by (etac rev_mp 1);
  14.101 @@ -157,7 +157,7 @@
  14.102  
  14.103  
  14.104  (**CANNOT be proved because A doesn't know where challenges come from...
  14.105 -goal thy 
  14.106 +Goal 
  14.107   "!!evs. [| A ~: bad;  B ~= Spy;  evs : woolam |]           \
  14.108  \    ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) &  \
  14.109  \        Says B A (Nonce NB) : set evs                       \
    15.1 --- a/src/HOL/Auth/Yahalom.ML	Wed Jun 24 10:33:42 1998 +0200
    15.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Jun 24 11:24:52 1998 +0200
    15.3 @@ -18,7 +18,7 @@
    15.4  
    15.5  
    15.6  (*A "possibility property": there are traces that reach the end*)
    15.7 -goal thy 
    15.8 +Goal 
    15.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   15.10  \        ==> EX X NB K. EX evs: yahalom.          \
   15.11  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   15.12 @@ -32,7 +32,7 @@
   15.13  (**** Inductive proofs about yahalom ****)
   15.14  
   15.15  (*Nobody sends themselves messages*)
   15.16 -goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
   15.17 +Goal "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
   15.18  by (etac yahalom.induct 1);
   15.19  by Auto_tac;
   15.20  qed_spec_mp "not_Says_to_self";
   15.21 @@ -43,7 +43,7 @@
   15.22  (** For reasoning about the encrypted portion of messages **)
   15.23  
   15.24  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   15.25 -goal thy "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
   15.26 +Goal "!!evs. Says S A {|Crypt (shrK A) Y, X|} : set evs ==> \
   15.27  \                X : analz (spies evs)";
   15.28  by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
   15.29  qed "YM4_analz_spies";
   15.30 @@ -52,7 +52,7 @@
   15.31            YM4_analz_spies RS (impOfSubs analz_subset_parts));
   15.32  
   15.33  (*Relates to both YM4 and Oops*)
   15.34 -goal thy "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
   15.35 +Goal "!!evs. Says S A {|Crypt (shrK A) {|B,K,NA,NB|}, X|} : set evs ==> \
   15.36  \                K : parts (spies evs)";
   15.37  by (blast_tac (claset() addSEs partsEs
   15.38                          addSDs [Says_imp_spies RS parts.Inj]) 1);
   15.39 @@ -78,7 +78,7 @@
   15.40      sends messages containing X! **)
   15.41  
   15.42  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
   15.43 -goal thy 
   15.44 +Goal 
   15.45   "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   15.46  by (parts_induct_tac 1);
   15.47  by (Fake_parts_insert_tac 1);
   15.48 @@ -86,7 +86,7 @@
   15.49  qed "Spy_see_shrK";
   15.50  Addsimps [Spy_see_shrK];
   15.51  
   15.52 -goal thy 
   15.53 +Goal 
   15.54   "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   15.55  by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset()));
   15.56  qed "Spy_analz_shrK";
   15.57 @@ -97,7 +97,7 @@
   15.58  
   15.59  
   15.60  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   15.61 -goal thy "!!evs. evs : yahalom ==>          \
   15.62 +Goal "!!evs. evs : yahalom ==>          \
   15.63  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   15.64  by (parts_induct_tac 1);
   15.65  (*Fake*)
   15.66 @@ -115,7 +115,7 @@
   15.67  
   15.68  (*Describes the form of K when the Server sends this message.  Useful for
   15.69    Oops as well as main secrecy property.*)
   15.70 -goal thy 
   15.71 +Goal 
   15.72   "!!evs. [| Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} \
   15.73  \             : set evs;                                                   \
   15.74  \           evs : yahalom |]                                          \
   15.75 @@ -143,7 +143,7 @@
   15.76  
   15.77  (** Session keys are not used to encrypt other session keys **)
   15.78  
   15.79 -goal thy  
   15.80 +Goal  
   15.81   "!!evs. evs : yahalom ==>                              \
   15.82  \  ALL K KK. KK <= Compl (range shrK) -->               \
   15.83  \            (Key K : analz (Key``KK Un (spies evs))) = \
   15.84 @@ -158,7 +158,7 @@
   15.85  by (spy_analz_tac 1);
   15.86  qed_spec_mp "analz_image_freshK";
   15.87  
   15.88 -goal thy
   15.89 +Goal
   15.90   "!!evs. [| evs : yahalom;  KAB ~: range shrK |]              \
   15.91  \         ==> Key K : analz (insert (Key KAB) (spies evs)) =  \
   15.92  \             (K = KAB | Key K : analz (spies evs))";
   15.93 @@ -168,7 +168,7 @@
   15.94  
   15.95  (*** The Key K uniquely identifies the Server's  message. **)
   15.96  
   15.97 -goal thy 
   15.98 +Goal 
   15.99   "!!evs. evs : yahalom ==>                                     \
  15.100  \      EX A' B' na' nb' X'. ALL A B na nb X.                   \
  15.101  \          Says Server A                                       \
  15.102 @@ -187,7 +187,7 @@
  15.103                          delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
  15.104  val lemma = result();
  15.105  
  15.106 -goal thy 
  15.107 +Goal 
  15.108  "!!evs. [| Says Server A                                                 \
  15.109  \            {|Crypt (shrK A) {|Agent B, Key K, na, nb|}, X|} : set evs; \
  15.110  \          Says Server A'                                                \
  15.111 @@ -200,7 +200,7 @@
  15.112  
  15.113  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
  15.114  
  15.115 -goal thy 
  15.116 +Goal 
  15.117   "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]                \
  15.118  \        ==> Says Server A                                        \
  15.119  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
  15.120 @@ -226,7 +226,7 @@
  15.121  
  15.122  
  15.123  (*Final version*)
  15.124 -goal thy 
  15.125 +Goal 
  15.126   "!!evs. [| Says Server A                                         \
  15.127  \              {|Crypt (shrK A) {|Agent B, Key K, na, nb|},       \
  15.128  \                Crypt (shrK B) {|Agent A, Key K|}|}              \
  15.129 @@ -241,7 +241,7 @@
  15.130  (** Security Guarantee for A upon receiving YM3 **)
  15.131  
  15.132  (*If the encrypted message appears then it originated with the Server*)
  15.133 -goal thy
  15.134 +Goal
  15.135   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
  15.136  \           A ~: bad;  evs : yahalom |]                          \
  15.137  \         ==> Says Server A                                            \
  15.138 @@ -254,7 +254,7 @@
  15.139  qed "A_trusts_YM3";
  15.140  
  15.141  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
  15.142 -goal thy
  15.143 +Goal
  15.144   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na, nb|} : parts (spies evs); \
  15.145  \           Notes Spy {|na, nb, Key K|} ~: set evs;               \
  15.146  \           A ~: bad;  B ~: bad;  evs : yahalom |]                \
  15.147 @@ -266,7 +266,7 @@
  15.148  
  15.149  (*B knows, by the first part of A's message, that the Server distributed 
  15.150    the key for A and B.  But this part says nothing about nonces.*)
  15.151 -goal thy 
  15.152 +Goal 
  15.153   "!!evs. [| Crypt (shrK B) {|Agent A, Key K|} : parts (spies evs);      \
  15.154  \           B ~: bad;  evs : yahalom |]                                 \
  15.155  \        ==> EX NA NB. Says Server A                                    \
  15.156 @@ -285,7 +285,7 @@
  15.157    the key quoting nonce NB.  This part says nothing about agent names. 
  15.158    Secrecy of NB is crucial.  Note that  Nonce NB  ~: analz (spies evs)  must
  15.159    be the FIRST antecedent of the induction formula.*)
  15.160 -goal thy 
  15.161 +Goal 
  15.162   "!!evs. evs : yahalom                                          \
  15.163  \        ==> Nonce NB ~: analz (spies evs) -->                  \
  15.164  \            Crypt K (Nonce NB) : parts (spies evs) -->         \
  15.165 @@ -312,14 +312,14 @@
  15.166  
  15.167  (** Lemmas about the predicate KeyWithNonce **)
  15.168  
  15.169 -goalw thy [KeyWithNonce_def]
  15.170 +Goalw [KeyWithNonce_def]
  15.171   "!!evs. Says Server A                                              \
  15.172  \            {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|} \
  15.173  \          : set evs ==> KeyWithNonce K NB evs";
  15.174  by (Blast_tac 1);
  15.175  qed "KeyWithNonceI";
  15.176  
  15.177 -goalw thy [KeyWithNonce_def]
  15.178 +Goalw [KeyWithNonce_def]
  15.179     "KeyWithNonce K NB (Says S A X # evs) =                                    \
  15.180  \    (Server = S &                                                            \
  15.181  \     (EX B n X'. X = {|Crypt (shrK A) {|Agent B, Key K, n, Nonce NB|}, X'|}) \
  15.182 @@ -329,7 +329,7 @@
  15.183  qed "KeyWithNonce_Says";
  15.184  Addsimps [KeyWithNonce_Says];
  15.185  
  15.186 -goalw thy [KeyWithNonce_def]
  15.187 +Goalw [KeyWithNonce_def]
  15.188     "KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs";
  15.189  by (Simp_tac 1);
  15.190  qed "KeyWithNonce_Notes";
  15.191 @@ -337,14 +337,14 @@
  15.192  
  15.193  (*A fresh key cannot be associated with any nonce 
  15.194    (with respect to a given trace). *)
  15.195 -goalw thy [KeyWithNonce_def]
  15.196 +Goalw [KeyWithNonce_def]
  15.197   "!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs";
  15.198  by (blast_tac (claset() addSEs spies_partsEs) 1);
  15.199  qed "fresh_not_KeyWithNonce";
  15.200  
  15.201  (*The Server message associates K with NB' and therefore not with any 
  15.202    other nonce NB.*)
  15.203 -goalw thy [KeyWithNonce_def]
  15.204 +Goalw [KeyWithNonce_def]
  15.205   "!!evs. [| Says Server A                                                \
  15.206  \                {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB'|}, X|} \
  15.207  \             : set evs;                                                 \
  15.208 @@ -361,13 +361,13 @@
  15.209  
  15.210  (*As with analz_image_freshK, we take some pains to express the property
  15.211    as a logical equivalence so that the simplifier can apply it.*)
  15.212 -goal thy  
  15.213 +Goal  
  15.214   "!!evs. P --> (X : analz (G Un H)) --> (X : analz H)  ==> \
  15.215  \        P --> (X : analz (G Un H)) = (X : analz H)";
  15.216  by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
  15.217  val Nonce_secrecy_lemma = result();
  15.218  
  15.219 -goal thy 
  15.220 +Goal 
  15.221   "!!evs. evs : yahalom ==>                                      \
  15.222  \        (ALL KK. KK <= Compl (range shrK) -->                  \
  15.223  \             (ALL K: KK. ~ KeyWithNonce K NB evs)   -->        \
  15.224 @@ -402,7 +402,7 @@
  15.225  (*Version required below: if NB can be decrypted using a session key then it
  15.226    was distributed with that key.  The more general form above is required
  15.227    for the induction to carry through.*)
  15.228 -goal thy 
  15.229 +Goal 
  15.230   "!!evs. [| Says Server A                                               \
  15.231  \            {|Crypt (shrK A) {|Agent B, Key KAB, na, Nonce NB'|}, X|}  \
  15.232  \           : set evs;                                                  \
  15.233 @@ -416,7 +416,7 @@
  15.234  
  15.235  (*** The Nonce NB uniquely identifies B's message. ***)
  15.236  
  15.237 -goal thy 
  15.238 +Goal 
  15.239   "!!evs. evs : yahalom ==>                                         \
  15.240  \   EX NA' A' B'. ALL NA A B.                                      \
  15.241  \      Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts(spies evs) \
  15.242 @@ -432,7 +432,7 @@
  15.243  by (blast_tac (claset() addSEs spies_partsEs) 1);
  15.244  val lemma = result();
  15.245  
  15.246 -goal thy 
  15.247 +Goal 
  15.248   "!!evs.[| Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs);    \
  15.249  \          Crypt (shrK B') {|Agent A', Nonce NA', nb|} : parts (spies evs); \
  15.250  \          evs : yahalom;  B ~: bad;  B' ~: bad |]  \
  15.251 @@ -443,7 +443,7 @@
  15.252  
  15.253  (*Variant useful for proving secrecy of NB: the Says... form allows 
  15.254    not_bad_tac to remove the assumption B' ~: bad.*)
  15.255 -goal thy 
  15.256 +Goal 
  15.257   "!!evs.[| Says C D   {|X,  Crypt (shrK B) {|Agent A, Nonce NA, nb|}|}    \
  15.258  \            : set evs;          B ~: bad;                                \
  15.259  \          Says C' D' {|X', Crypt (shrK B') {|Agent A', Nonce NA', nb|}|} \
  15.260 @@ -459,7 +459,7 @@
  15.261  
  15.262  (** A nonce value is never used both as NA and as NB **)
  15.263  
  15.264 -goal thy 
  15.265 +Goal 
  15.266   "!!evs. evs : yahalom                     \
  15.267  \ ==> Nonce NB ~: analz (spies evs) -->    \
  15.268  \     Crypt (shrK B') {|Agent A', Nonce NB, nb'|} : parts(spies evs) --> \
  15.269 @@ -475,7 +475,7 @@
  15.270  standard (result() RS mp RSN (2,rev_mp));
  15.271  
  15.272  (*The Server sends YM3 only in response to YM2.*)
  15.273 -goal thy 
  15.274 +Goal 
  15.275   "!!evs. [| Says Server A                                                \
  15.276  \            {|Crypt (shrK A) {|Agent B, k, na, nb|}, X|} : set evs;     \
  15.277  \           evs : yahalom |]                                             \
  15.278 @@ -490,7 +490,7 @@
  15.279  
  15.280  
  15.281  (*A vital theorem for B, that nonce NB remains secure from the Spy.*)
  15.282 -goal thy 
  15.283 +Goal 
  15.284   "!!evs. [| A ~: bad;  B ~: bad;  evs : yahalom |]  \
  15.285  \ ==> Says B Server                                                    \
  15.286  \          {|Agent B, Crypt (shrK B) {|Agent A, Nonce NA, Nonce NB|}|} \
  15.287 @@ -549,7 +549,7 @@
  15.288    assumption must quantify over ALL POSSIBLE keys instead of our particular K.
  15.289    If this run is broken and the spy substitutes a certificate containing an
  15.290    old key, B has no means of telling.*)
  15.291 -goal thy 
  15.292 +Goal 
  15.293   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  15.294  \                       Crypt K (Nonce NB)|} : set evs;                     \
  15.295  \           Says B Server                                                   \
  15.296 @@ -574,7 +574,7 @@
  15.297  
  15.298  
  15.299  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
  15.300 -goal thy 
  15.301 +Goal 
  15.302   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  15.303  \                       Crypt K (Nonce NB)|} : set evs;                     \
  15.304  \           Says B Server                                                   \
  15.305 @@ -590,7 +590,7 @@
  15.306  (*** Authenticating B to A ***)
  15.307  
  15.308  (*The encryption in message YM2 tells us it cannot be faked.*)
  15.309 -goal thy 
  15.310 +Goal 
  15.311   "!!evs. evs : yahalom                                            \
  15.312  \  ==> Crypt (shrK B) {|Agent A, Nonce NA, nb|} : parts (spies evs) --> \
  15.313  \      B ~: bad -->                                              \
  15.314 @@ -601,7 +601,7 @@
  15.315  bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp);
  15.316  
  15.317  (*If the server sends YM3 then B sent YM2*)
  15.318 -goal thy 
  15.319 +Goal 
  15.320   "!!evs. evs : yahalom                                                      \
  15.321  \  ==> Says Server A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  15.322  \         : set evs -->                                                     \
  15.323 @@ -618,7 +618,7 @@
  15.324  val lemma = result() RSN (2, rev_mp) RS mp |> standard;
  15.325  
  15.326  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  15.327 -goal thy
  15.328 +Goal
  15.329   "!!evs. [| Says S A {|Crypt (shrK A) {|Agent B, Key K, Nonce NA, nb|}, X|} \
  15.330  \             : set evs;                                                    \
  15.331  \           A ~: bad;  B ~: bad;  evs : yahalom |]                        \
  15.332 @@ -634,7 +634,7 @@
  15.333  (*Assuming the session key is secure, if both certificates are present then
  15.334    A has said NB.  We can't be sure about the rest of A's message, but only
  15.335    NB matters for freshness.*)  
  15.336 -goal thy 
  15.337 +Goal 
  15.338   "!!evs. evs : yahalom                                             \
  15.339  \        ==> Key K ~: analz (spies evs) -->                     \
  15.340  \            Crypt K (Nonce NB) : parts (spies evs) -->         \
  15.341 @@ -659,7 +659,7 @@
  15.342  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
  15.343    Moreover, A associates K with NB (thus is talking about the same run).
  15.344    Other premises guarantee secrecy of K.*)
  15.345 -goal thy 
  15.346 +Goal 
  15.347   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Key K|},                  \
  15.348  \                       Crypt K (Nonce NB)|} : set evs;                     \
  15.349  \           Says B Server                                                   \
    16.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Jun 24 10:33:42 1998 +0200
    16.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Jun 24 11:24:52 1998 +0200
    16.3 @@ -23,7 +23,7 @@
    16.4  
    16.5  
    16.6  (*A "possibility property": there are traces that reach the end*)
    16.7 -goal thy 
    16.8 +Goal 
    16.9   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]   \
   16.10  \        ==> EX X NB K. EX evs: yahalom.          \
   16.11  \               Says A B {|X, Crypt K (Nonce NB)|} : set evs";
   16.12 @@ -37,7 +37,7 @@
   16.13  (**** Inductive proofs about yahalom ****)
   16.14  
   16.15  (*Nobody sends themselves messages*)
   16.16 -goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
   16.17 +Goal "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
   16.18  by (etac yahalom.induct 1);
   16.19  by Auto_tac;
   16.20  qed_spec_mp "not_Says_to_self";
   16.21 @@ -48,7 +48,7 @@
   16.22  (** For reasoning about the encrypted portion of messages **)
   16.23  
   16.24  (*Lets us treat YM4 using a similar argument as for the Fake case.*)
   16.25 -goal thy "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
   16.26 +Goal "!!evs. Says S A {|NB, Crypt (shrK A) Y, X|} : set evs ==> \
   16.27  \                X : analz (spies evs)";
   16.28  by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
   16.29  qed "YM4_analz_spies";
   16.30 @@ -57,7 +57,7 @@
   16.31            YM4_analz_spies RS (impOfSubs analz_subset_parts));
   16.32  
   16.33  (*Relates to both YM4 and Oops*)
   16.34 -goal thy "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
   16.35 +Goal "!!evs. Says S A {|NB, Crypt (shrK A) {|B,K,NA|}, X|} : set evs ==> \
   16.36  \                K : parts (spies evs)";
   16.37  by (Blast_tac 1);
   16.38  qed "YM4_Key_parts_spies";
   16.39 @@ -82,14 +82,14 @@
   16.40      sends messages containing X! **)
   16.41  
   16.42  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
   16.43 -goal thy 
   16.44 +Goal 
   16.45   "!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
   16.46  by (parts_induct_tac 1);
   16.47  by (ALLGOALS Blast_tac);
   16.48  qed "Spy_see_shrK";
   16.49  Addsimps [Spy_see_shrK];
   16.50  
   16.51 -goal thy 
   16.52 +Goal 
   16.53   "!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   16.54  by Auto_tac;
   16.55  qed "Spy_analz_shrK";
   16.56 @@ -100,7 +100,7 @@
   16.57  
   16.58  
   16.59  (*Nobody can have used non-existent keys!  Needed to apply analz_insert_Key*)
   16.60 -goal thy "!!evs. evs : yahalom ==>          \
   16.61 +Goal "!!evs. evs : yahalom ==>          \
   16.62  \         Key K ~: used evs --> K ~: keysFor (parts (spies evs))";
   16.63  by (parts_induct_tac 1);
   16.64  (*YM4: Key K is not fresh!*)
   16.65 @@ -119,7 +119,7 @@
   16.66  
   16.67  (*Describes the form of K when the Server sends this message.  Useful for
   16.68    Oops as well as main secrecy property.*)
   16.69 -goal thy 
   16.70 +Goal 
   16.71   "!!evs. [| Says Server A {|nb', Crypt (shrK A) {|Agent B, Key K, na|}, X|} \
   16.72  \            : set evs;                                            \
   16.73  \           evs : yahalom |]                                       \
   16.74 @@ -150,7 +150,7 @@
   16.75  
   16.76  (** Session keys are not used to encrypt other session keys **)
   16.77  
   16.78 -goal thy  
   16.79 +Goal  
   16.80   "!!evs. evs : yahalom ==>                               \
   16.81  \  ALL K KK. KK <= Compl (range shrK) -->                \
   16.82  \            (Key K : analz (Key``KK Un (spies evs))) =  \
   16.83 @@ -164,7 +164,7 @@
   16.84  by (spy_analz_tac 1);
   16.85  qed_spec_mp "analz_image_freshK";
   16.86  
   16.87 -goal thy
   16.88 +Goal
   16.89   "!!evs. [| evs : yahalom;  KAB ~: range shrK |] ==>     \
   16.90  \        Key K : analz (insert (Key KAB) (spies evs)) =  \
   16.91  \        (K = KAB | Key K : analz (spies evs))";
   16.92 @@ -174,7 +174,7 @@
   16.93  
   16.94  (*** The Key K uniquely identifies the Server's  message. **)
   16.95  
   16.96 -goal thy 
   16.97 +Goal 
   16.98   "!!evs. evs : yahalom ==>                                     \
   16.99  \      EX A' B' na' nb' X'. ALL A B na nb X.                   \
  16.100  \          Says Server A                                       \
  16.101 @@ -191,7 +191,7 @@
  16.102                          addss (simpset() addsimps [parts_insertI])) 1);
  16.103  val lemma = result();
  16.104  
  16.105 -goal thy 
  16.106 +Goal 
  16.107  "!!evs. [| Says Server A                                            \
  16.108  \            {|nb, Crypt (shrK A) {|Agent B, Key K, na|}, X|} : set evs; \
  16.109  \          Says Server A'                                           \
  16.110 @@ -204,7 +204,7 @@
  16.111  
  16.112  (** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **)
  16.113  
  16.114 -goal thy 
  16.115 +Goal 
  16.116   "!!evs. [| A ~: bad;  B ~: bad;  A ~= B;                       \
  16.117  \           evs : yahalom |]                                    \
  16.118  \        ==> Says Server A                                      \
  16.119 @@ -229,7 +229,7 @@
  16.120  
  16.121  
  16.122  (*Final version*)
  16.123 -goal thy 
  16.124 +Goal 
  16.125   "!!evs. [| Says Server A                                    \
  16.126  \              {|nb, Crypt (shrK A) {|Agent B, Key K, na|},  \
  16.127  \                    Crypt (shrK B) {|Agent A, Agent B, Key K, nb|}|}    \
  16.128 @@ -246,7 +246,7 @@
  16.129  
  16.130  (*If the encrypted message appears then it originated with the Server.
  16.131    May now apply Spy_not_see_encrypted_key, subject to its conditions.*)
  16.132 -goal thy
  16.133 +Goal
  16.134   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|}                      \
  16.135  \            : parts (spies evs);                                      \
  16.136  \           A ~: bad;  evs : yahalom |]                                \
  16.137 @@ -260,7 +260,7 @@
  16.138  qed "A_trusts_YM3";
  16.139  
  16.140  (*The obvious combination of A_trusts_YM3 with Spy_not_see_encrypted_key*)
  16.141 -goal thy
  16.142 +Goal
  16.143   "!!evs. [| Crypt (shrK A) {|Agent B, Key K, na|} : parts (spies evs); \
  16.144  \           ALL nb. Notes Spy {|na, nb, Key K|} ~: set evs;            \
  16.145  \           A ~: bad;  B ~: bad;  evs : yahalom |]                     \
  16.146 @@ -273,7 +273,7 @@
  16.147  
  16.148  (*B knows, by the first part of A's message, that the Server distributed 
  16.149    the key for A and B, and has associated it with NB.*)
  16.150 -goal thy 
  16.151 +Goal 
  16.152   "!!evs. [| Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|} \
  16.153  \             : parts (spies evs);                               \
  16.154  \           B ~: bad;  evs : yahalom |]                          \
  16.155 @@ -293,7 +293,7 @@
  16.156  
  16.157  (*What can B deduce from receipt of YM4?  Stronger and simpler than Yahalom
  16.158    because we do not have to show that NB is secret. *)
  16.159 -goal thy 
  16.160 +Goal 
  16.161   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
  16.162  \                       X|}                                         \
  16.163  \             : set evs;                                            \
  16.164 @@ -308,7 +308,7 @@
  16.165  
  16.166  
  16.167  (*The obvious combination of B_trusts_YM4 with Spy_not_see_encrypted_key*)
  16.168 -goal thy 
  16.169 +Goal 
  16.170   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
  16.171  \                       X|}                                         \
  16.172  \             : set evs;                                            \
  16.173 @@ -323,7 +323,7 @@
  16.174  (*** Authenticating B to A ***)
  16.175  
  16.176  (*The encryption in message YM2 tells us it cannot be faked.*)
  16.177 -goal thy 
  16.178 +Goal 
  16.179   "!!evs. [| Crypt (shrK B) {|Agent A, Nonce NA|} : parts (spies evs);  \
  16.180  \           B ~: bad;  evs : yahalom                                   \
  16.181  \        |] ==> EX NB. Says B Server {|Agent B, Nonce NB,              \
  16.182 @@ -337,7 +337,7 @@
  16.183  
  16.184  
  16.185  (*If the server sends YM3 then B sent YM2, perhaps with a different NB*)
  16.186 -goal thy 
  16.187 +Goal 
  16.188   "!!evs. [| Says Server A                                              \
  16.189  \               {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  16.190  \             : set evs;                                               \
  16.191 @@ -356,7 +356,7 @@
  16.192  val lemma = result();
  16.193  
  16.194  (*If A receives YM3 then B has used nonce NA (and therefore is alive)*)
  16.195 -goal thy
  16.196 +Goal
  16.197   "!!evs. [| Says S A {|nb, Crypt (shrK A) {|Agent B, Key K, Nonce NA|}, X|} \
  16.198  \             : set evs;                                                    \
  16.199  \           A ~: bad;  B ~: bad;  evs : yahalom |]                   \
  16.200 @@ -373,7 +373,7 @@
  16.201    A has said NB.  We can't be sure about the rest of A's message, but only
  16.202    NB matters for freshness.  Note that  Key K ~: analz (spies evs)  must be
  16.203    the FIRST antecedent of the induction formula.*)  
  16.204 -goal thy 
  16.205 +Goal 
  16.206   "!!evs. evs : yahalom                                     \
  16.207  \        ==> Key K ~: analz (spies evs) -->                \
  16.208  \            Crypt K (Nonce NB) : parts (spies evs) -->    \
  16.209 @@ -398,7 +398,7 @@
  16.210  (*If B receives YM4 then A has used nonce NB (and therefore is alive).
  16.211    Moreover, A associates K with NB (thus is talking about the same run).
  16.212    Other premises guarantee secrecy of K.*)
  16.213 -goal thy 
  16.214 +Goal 
  16.215   "!!evs. [| Says A' B {|Crypt (shrK B) {|Agent A, Agent B, Key K, Nonce NB|}, \
  16.216  \                       Crypt K (Nonce NB)|} : set evs;                 \
  16.217  \           (ALL NA. Notes Spy {|Nonce NA, Nonce NB, Key K|} ~: set evs); \