src/HOL/Auth/NS_Shared.ML
changeset 4237 fb01353e363b
parent 4091 771b1f6422a8
child 4267 cdc193e38925
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Nov 18 15:30:50 1997 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Tue Nov 18 16:36:33 1997 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  (*A "possibility property": there are traces that reach the end*)
     1.5  goal thy 
     1.6   "!!A B. [| A ~= B; A ~= Server; B ~= Server |]       \
     1.7 -\        ==> EX N K. EX evs: ns_shared.          \
     1.8 +\        ==> EX N K. EX evs: ns_shared.               \
     1.9  \               Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs";
    1.10  by (REPEAT (resolve_tac [exI,bexI] 1));
    1.11  by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS 
    1.12 @@ -62,7 +62,7 @@
    1.13  fun parts_induct_tac i = 
    1.14      etac ns_shared.induct i  THEN 
    1.15      forward_tac [Oops_parts_spies] (i+7)  THEN
    1.16 -    dtac NS3_msg_in_parts_spies (i+4)     THEN
    1.17 +    forward_tac [NS3_msg_in_parts_spies] (i+4)     THEN
    1.18      prove_simple_subgoals_tac i;
    1.19  
    1.20  
    1.21 @@ -100,9 +100,9 @@
    1.22  (*Fake*)
    1.23  by (best_tac
    1.24        (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
    1.25 -               addIs  [impOfSubs analz_subset_parts]
    1.26 -               addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.27 -               addss  (simpset())) 1);
    1.28 +                addIs  [impOfSubs analz_subset_parts]
    1.29 +                addDs  [impOfSubs (analz_subset_parts RS keysFor_mono)]
    1.30 +                addss  (simpset())) 1);
    1.31  (*NS2, NS4, NS5*)
    1.32  by (ALLGOALS (blast_tac (claset() addSEs spies_partsEs)));
    1.33  qed_spec_mp "new_keys_not_used";
    1.34 @@ -152,7 +152,7 @@
    1.35  \            | X : analz (spies evs)";
    1.36  by (case_tac "A : bad" 1);
    1.37  by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]
    1.38 -                      addss (simpset())) 1);
    1.39 +                       addss (simpset())) 1);
    1.40  by (forward_tac [Says_imp_spies RS parts.Inj] 1);
    1.41  by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1);
    1.42  qed "Says_S_message_form";
    1.43 @@ -181,12 +181,12 @@
    1.44    We require that agents should behave like this subsequently also.*)
    1.45  goal thy 
    1.46   "!!evs. [| evs : ns_shared;  Kab ~: range shrK |] ==>  \
    1.47 -\           (Crypt KAB X) : parts (spies evs) &      \
    1.48 +\           (Crypt KAB X) : parts (spies evs) &         \
    1.49  \           Key K : parts {X} --> Key K : parts (spies evs)";
    1.50  by (parts_induct_tac 1);
    1.51  (*Deals with Faked messages*)
    1.52  by (blast_tac (claset() addSEs partsEs
    1.53 -                       addDs [impOfSubs parts_insert_subset_Un]) 1);
    1.54 +                        addDs [impOfSubs parts_insert_subset_Un]) 1);
    1.55  (*Base, NS4 and NS5*)
    1.56  by (Auto_tac());
    1.57  result();
    1.58 @@ -196,8 +196,8 @@
    1.59  
    1.60  (*The equality makes the induction hypothesis easier to apply*)
    1.61  goal thy  
    1.62 - "!!evs. evs : ns_shared ==>                                \
    1.63 -\  ALL K KK. KK <= Compl (range shrK) -->                        \
    1.64 + "!!evs. evs : ns_shared ==>                             \
    1.65 +\  ALL K KK. KK <= Compl (range shrK) -->                \
    1.66  \            (Key K : analz (Key``KK Un (spies evs))) =  \
    1.67  \            (K : KK | Key K : analz (spies evs))";
    1.68  by (etac ns_shared.induct 1);
    1.69 @@ -214,7 +214,7 @@
    1.70  
    1.71  
    1.72  goal thy
    1.73 - "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>     \
    1.74 + "!!evs. [| evs : ns_shared;  KAB ~: range shrK |] ==>  \
    1.75  \        Key K : analz (insert (Key KAB) (spies evs)) = \
    1.76  \        (K = KAB | Key K : analz (spies evs))";
    1.77  by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
    1.78 @@ -225,7 +225,7 @@
    1.79  
    1.80  goal thy 
    1.81   "!!evs. evs : ns_shared ==>                                        \
    1.82 -\      EX A' NA' B' X'. ALL A NA B X.                                    \
    1.83 +\      EX A' NA' B' X'. ALL A NA B X.                                      \
    1.84  \       Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \
    1.85  \       -->         A=A' & NA=NA' & B=B' & X=X'";
    1.86  by (etac ns_shared.induct 1);
    1.87 @@ -237,15 +237,15 @@
    1.88  (*NS2: it can't be a new key*)
    1.89  by (expand_case_tac "K = ?y" 1);
    1.90  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
    1.91 -by (blast_tac (claset() delrules [conjI]    (*prevent split-up into 4 subgoals*)
    1.92 -                      addSEs spies_partsEs) 1);
    1.93 +by (blast_tac (claset() delrules [conjI]   (*prevent splitup into 4 subgoals*)
    1.94 +                        addSEs spies_partsEs) 1);
    1.95  val lemma = result();
    1.96  
    1.97  (*In messages of this form, the session key uniquely identifies the rest*)
    1.98  goal thy 
    1.99 - "!!evs. [| Says Server A                                    \
   1.100 -\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ 
   1.101 -\           Says Server A'                                   \
   1.102 + "!!evs. [| Says Server A                                               \
   1.103 +\             (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs;     \ 
   1.104 +\           Says Server A'                                              \
   1.105  \             (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \
   1.106  \           evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'";
   1.107  by (prove_unique_tac lemma 1);
   1.108 @@ -267,14 +267,15 @@
   1.109  by (ALLGOALS 
   1.110      (asm_simp_tac 
   1.111       (simpset() addsimps ([analz_insert_eq, analz_insert_freshK] @ 
   1.112 -			 pushes @ expand_ifs))));
   1.113 +			  pushes @ expand_ifs))));
   1.114  (*Oops*)
   1.115  by (blast_tac (claset() addDs [unique_session_keys]) 5);
   1.116  (*NS3, replay sub-case*) 
   1.117  by (Blast_tac 4);
   1.118  (*NS2*)
   1.119  by (blast_tac (claset() addSEs spies_partsEs
   1.120 -                       addIs [parts_insertI, impOfSubs analz_subset_parts]) 2);
   1.121 +                        addIs  [parts_insertI, 
   1.122 +			        impOfSubs analz_subset_parts]) 2);
   1.123  (*Fake*) 
   1.124  by (spy_analz_tac 1);
   1.125  (*NS3, Server sub-case*) (**LEVEL 6 **)
   1.126 @@ -289,9 +290,9 @@
   1.127  
   1.128  (*Final version: Server's message in the most abstract form*)
   1.129  goal thy 
   1.130 - "!!evs. [| Says Server A                                               \
   1.131 -\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;            \
   1.132 -\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);          \
   1.133 + "!!evs. [| Says Server A                                        \
   1.134 +\            (Crypt K' {|NA, Agent B, Key K, X|}) : set evs;     \
   1.135 +\           (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs);   \
   1.136  \           A ~: bad;  B ~: bad;  evs : ns_shared                \
   1.137  \        |] ==> Key K ~: analz (spies evs)";
   1.138  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.139 @@ -306,8 +307,8 @@
   1.140  
   1.141  (*If the encrypted message appears then it originated with the Server*)
   1.142  goal thy
   1.143 - "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \
   1.144 -\           B ~: bad;  evs : ns_shared |]                        \
   1.145 + "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs);     \
   1.146 +\           B ~: bad;  evs : ns_shared |]                              \
   1.147  \         ==> EX NA. Says Server A                                     \
   1.148  \              (Crypt (shrK A) {|NA, Agent B, Key K,                   \
   1.149  \                                Crypt (shrK B) {|Key K, Agent A|}|})  \
   1.150 @@ -337,7 +338,7 @@
   1.151  by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib])));
   1.152  (**LEVEL 7**)
   1.153  by (blast_tac (claset() addSDs [Crypt_Fake_parts_insert]
   1.154 -                       addDs [impOfSubs analz_subset_parts]) 1);
   1.155 +                        addDs [impOfSubs analz_subset_parts]) 1);
   1.156  by (Blast_tac 2);
   1.157  by (REPEAT_FIRST (rtac impI ORELSE' etac conjE ORELSE' hyp_subst_tac));
   1.158  (*Subgoal 1: contradiction from the assumptions  
   1.159 @@ -349,9 +350,9 @@
   1.160  by (thin_tac "?PP-->?QQ" 1);
   1.161  by (case_tac "Ba : bad" 1);
   1.162  by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, 
   1.163 -			      unique_session_keys]) 2);
   1.164 +			       unique_session_keys]) 2);
   1.165  by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS
   1.166 -			      Crypt_Spy_analz_bad]) 1);
   1.167 +			       Crypt_Spy_analz_bad]) 1);
   1.168  val lemma = result();
   1.169  
   1.170  goal thy
   1.171 @@ -362,5 +363,5 @@
   1.172  \           A ~: bad;  B ~: bad;  evs : ns_shared |]           \
   1.173  \        ==> Says B A (Crypt K (Nonce NB)) : set evs";
   1.174  by (blast_tac (claset() addSIs [lemma RS mp RS mp RS mp]
   1.175 -                       addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   1.176 +                        addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1);
   1.177  qed "A_trusts_NS4";