src/HOL/Auth/OtwayRees_AN.ML
changeset 2131 3106a99d30a5
parent 2106 1a52e2c5897e
child 2160 ad4382e546fc
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Sun Oct 27 13:47:02 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Oct 28 12:55:24 1996 +0100
     1.3 @@ -59,16 +59,15 @@
     1.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     1.5  qed "OR4_analz_sees_Spy";
     1.6  
     1.7 -goal thy "!!evs. Says B' A (Crypt {|N,Agent A,B,K|} K') : set_of_list evs ==> \
     1.8 -\                K : parts (sees lost Spy evs)";
     1.9 +goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
    1.10 +\                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    1.11  by (fast_tac (!claset addSEs partsEs
    1.12                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.13 -qed "Reveal_parts_sees_Spy";
    1.14 +qed "Oops_parts_sees_Spy";
    1.15  
    1.16 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.17 +(*OR4_analz_sees_Spy lets us treat those cases using the same 
    1.18    argument as for the Fake case.  This is possible for most, but not all,
    1.19 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.20 -  messages originate from the Spy. *)
    1.21 +  proofs, since Fake messages originate from the Spy. *)
    1.22  
    1.23  bind_thm ("OR4_parts_sees_Spy",
    1.24            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    1.25 @@ -77,7 +76,7 @@
    1.26    harder to complete, since simplification does less for us.*)
    1.27  val parts_Fake_tac = 
    1.28      forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    1.29 -    forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 7;
    1.30 +    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
    1.31  
    1.32  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.33  fun parts_induct_tac i = SELECT_GOAL
    1.34 @@ -95,34 +94,27 @@
    1.35  
    1.36  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.37  goal thy 
    1.38 - "!!evs. [| evs : otway lost;  A ~: lost |]    \
    1.39 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.40 + "!!evs. evs : otway lost \
    1.41 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.42  by (parts_induct_tac 1);
    1.43  by (Auto_tac());
    1.44 -qed "Spy_not_see_shrK";
    1.45 -
    1.46 -bind_thm ("Spy_not_analz_shrK",
    1.47 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    1.48 -
    1.49 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    1.50 +qed "Spy_see_shrK";
    1.51 +Addsimps [Spy_see_shrK];
    1.52  
    1.53 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.54 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.55 -val major::prems = 
    1.56 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    1.57 -\             evs : otway lost;                                 \
    1.58 -\             A:lost ==> R                                  \
    1.59 -\           |] ==> R";
    1.60 -by (rtac ccontr 1);
    1.61 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    1.62 -by (swap_res_tac prems 2);
    1.63 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.64 -qed "Spy_see_shrK_E";
    1.65 +goal thy 
    1.66 + "!!evs. evs : otway lost \
    1.67 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.68 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.69 +qed "Spy_analz_shrK";
    1.70 +Addsimps [Spy_analz_shrK];
    1.71  
    1.72 -bind_thm ("Spy_analz_shrK_E", 
    1.73 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    1.74 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.75 +\                  evs : otway lost |] ==> A:lost";
    1.76 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.77 +qed "Spy_see_shrK_D";
    1.78  
    1.79 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    1.80 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.81 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.82  
    1.83  
    1.84  (*** Future keys can't be seen or used! ***)
    1.85 @@ -134,7 +126,7 @@
    1.86        The Union over C is essential for the induction! *)
    1.87  goal thy "!!evs. evs : otway lost ==> \
    1.88  \                length evs <= length evs' --> \
    1.89 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.90 +\                Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    1.91  by (parts_induct_tac 1);
    1.92  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    1.93                                             impOfSubs parts_insert_subset_Un,
    1.94 @@ -224,39 +216,27 @@
    1.95  
    1.96  (*** Proofs involving analz ***)
    1.97  
    1.98 -(*Describes the form of Key K when the following message is sent.  The use of
    1.99 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.100 -  assumption A ~: lost prevents its being a Faked message.  (Based
   1.101 -  on NS_Shared/Says_S_message_form) *)
   1.102 -goal thy
   1.103 - "!!evs. evs: otway lost ==>                                           \
   1.104 -\        Crypt {|N, Agent A, B, Key K|} (shrK A) : parts (sees lost Spy evs)  \
   1.105 -\        --> A ~: lost --> (EX evt: otway lost. K = newK evt)";
   1.106 -by (parts_induct_tac 1);
   1.107 -by (Auto_tac());
   1.108 -qed_spec_mp "Reveal_message_lemma";
   1.109 -
   1.110 -(*EITHER describes the form of Key K when the following message is sent, 
   1.111 -  OR     reduces it to the Fake case.*)
   1.112 -
   1.113 +(*Describes the form of K and NA when the Server sends this message.*)
   1.114  goal thy 
   1.115 - "!!evs. [| Says B' A (Crypt {|N, Agent A, B, Key K|} (shrK A)) \
   1.116 -\            : set_of_list evs;                                 \
   1.117 -\           evs : otway lost |]                                 \
   1.118 -\        ==> (EX evt: otway lost. K = newK evt)                 \
   1.119 -\          | Key K : analz (sees lost Spy evs)";
   1.120 -br (Reveal_message_lemma RS disjCI) 1;
   1.121 -ba 1;
   1.122 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.123 -                      addDs [impOfSubs analz_subset_parts]) 1);
   1.124 -by (fast_tac (!claset addSDs [Says_Crypt_lost]) 1);
   1.125 -qed "Reveal_message_form";
   1.126 + "!!evs. [| Says Server B \
   1.127 +\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.128 +\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.129 +\           evs : otway lost |]                                        \
   1.130 +\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   1.131 +\            (EX i. NA = Nonce i) &                  \
   1.132 +\            (EX j. NB = Nonce j)";
   1.133 +by (etac rev_mp 1);
   1.134 +by (etac otway.induct 1);
   1.135 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.136 +qed "Says_Server_message_form";
   1.137  
   1.138  
   1.139  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.140  val analz_Fake_tac = 
   1.141      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.142 -    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   1.143 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.144 +    assume_tac 7 THEN Full_simp_tac 7 THEN
   1.145 +    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.146  
   1.147  
   1.148  (****
   1.149 @@ -280,16 +260,15 @@
   1.150  by (etac otway.induct 1);
   1.151  by analz_Fake_tac;
   1.152  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.153 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.154  by (ALLGOALS (*Takes 28 secs*)
   1.155      (asm_simp_tac 
   1.156       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.157                           @ pushes)
   1.158                 setloop split_tac [expand_if])));
   1.159  (** LEVEL 5 **)
   1.160 -(*Reveal case 2, OR4, Fake*) 
   1.161 -by (EVERY (map spy_analz_tac [6, 4, 2]));
   1.162 -(*Reveal case 1, OR3, Base*)
   1.163 +(*OR4, Fake*) 
   1.164 +by (EVERY (map spy_analz_tac [4,2]));
   1.165 +(*Oops, OR3, Base*)
   1.166  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.167  qed_spec_mp "analz_image_newK";
   1.168  
   1.169 @@ -306,8 +285,6 @@
   1.170  
   1.171  (*** The Key K uniquely identifies the Server's  message. **)
   1.172  
   1.173 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.174 -
   1.175  goal thy 
   1.176   "!!evs. evs : otway lost ==>                      \
   1.177  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.178 @@ -387,21 +364,6 @@
   1.179  qed "A_trust_OR4";
   1.180  
   1.181  
   1.182 -(*Describes the form of K and NA when the Server sends this message.*)
   1.183 -goal thy 
   1.184 - "!!evs. [| Says Server B \
   1.185 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.186 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.187 -\           evs : otway lost |]                                        \
   1.188 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   1.189 -\            (EX i. NA = Nonce i) &                  \
   1.190 -\            (EX j. NB = Nonce j)";
   1.191 -by (etac rev_mp 1);
   1.192 -by (etac otway.induct 1);
   1.193 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.194 -qed "Says_Server_message_form";
   1.195 -
   1.196 -
   1.197  (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.198      Does not in itself guarantee security: an attack could violate 
   1.199      the premises, e.g. by having A=Spy **)
   1.200 @@ -412,40 +374,31 @@
   1.201  \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
   1.202  \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
   1.203  \            : set_of_list evs -->                                         \
   1.204 -\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   1.205 +\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   1.206  \            Key K ~: analz (sees lost Spy evs)";
   1.207  by (etac otway.induct 1);
   1.208  by analz_Fake_tac;
   1.209 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.210  by (ALLGOALS
   1.211      (asm_full_simp_tac 
   1.212       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.213                            analz_insert_Key_newK] @ pushes)
   1.214                 setloop split_tac [expand_if])));
   1.215 -(** LEVEL 4 **)
   1.216  (*OR3*)
   1.217  by (fast_tac (!claset addSIs [parts_insertI]
   1.218                        addEs [Says_imp_old_keys RS less_irrefl]
   1.219                        addss (!simpset addsimps [parts_insert2])) 2);
   1.220 -(*Reveal case 2, OR4, Fake*) 
   1.221 +(*OR4, Fake*) 
   1.222  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.223 -(*Reveal case 1*) (** LEVEL 6 **)
   1.224 -by (case_tac "Aa : lost" 1);
   1.225 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.226 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.227 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.228 -(*So now we have  Aa ~: lost *)
   1.229 -by (dtac A_trust_OR4 1);
   1.230 -by (REPEAT (assume_tac 1));
   1.231 +(*Oops*) 
   1.232  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.233  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.234  
   1.235  goal thy 
   1.236   "!!evs. [| Says Server B                                                     \
   1.237 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   1.238 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.239 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.240 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.241 +\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.242 +\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   1.243 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   1.244 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   1.245  \        ==> K ~: analz (sees lost Spy evs)";
   1.246  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.247  by (fast_tac (!claset addSEs [lemma]) 1);
   1.248 @@ -455,9 +408,9 @@
   1.249  goal thy 
   1.250   "!!evs. [| C ~: {A,B,Server};                                                \
   1.251  \           Says Server B                                                     \
   1.252 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   1.253 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   1.254 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.255 +\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   1.256 +\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   1.257 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   1.258  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.259  \        ==> K ~: analz (sees lost C evs)";
   1.260  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);