Changing from the Reveal to the Oops rule
authorpaulson
Mon Oct 28 12:55:24 1996 +0100 (1996-10-28)
changeset 21313106a99d30a5
parent 2130 53b6e0bc8ccf
child 2132 aeba09ebd8bc
Changing from the Reveal to the Oops rule
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/OtwayRees_Bad.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.ML	Sun Oct 27 13:47:02 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.ML	Mon Oct 28 12:55:24 1996 +0100
     1.3 @@ -50,22 +50,22 @@
     1.4  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
     1.5  
     1.6  (*For reasoning about the encrypted portion of message NS3*)
     1.7 -goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \
     1.8 -\                X : parts (sees lost Spy evs)";
     1.9 +goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \
    1.10 +\                ==> X : 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 "NS3_msg_in_parts_sees_Spy";
    1.14                                
    1.15  goal thy
    1.16 -    "!!evs. Says S A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs ==> \
    1.17 -\                K : parts (sees lost Spy evs)";
    1.18 +    "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs \
    1.19 +\           ==> K : parts (sees lost Spy evs)";
    1.20  by (fast_tac (!claset addSEs partsEs
    1.21                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.22 -qed "Reveal_parts_sees_Spy";
    1.23 +qed "Oops_parts_sees_Spy";
    1.24  
    1.25  val parts_Fake_tac = 
    1.26      dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN
    1.27 -    forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 8;
    1.28 +    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8;
    1.29  
    1.30  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.31  fun parts_induct_tac i = SELECT_GOAL
    1.32 @@ -82,47 +82,29 @@
    1.33  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    1.34      sends messages containing X! **)
    1.35  
    1.36 -(*Spy never sees another agent's shared key!*)
    1.37 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.38  goal thy 
    1.39 - "!!evs. [| evs : ns_shared lost; A ~: lost |]    \
    1.40 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.41 + "!!evs. evs : ns_shared lost \
    1.42 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.43  by (parts_induct_tac 1);
    1.44  by (Auto_tac());
    1.45 -qed "Spy_not_see_shrK";
    1.46 -
    1.47 -bind_thm ("Spy_not_analz_shrK",
    1.48 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    1.49 -
    1.50 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    1.51 +qed "Spy_see_shrK";
    1.52 +Addsimps [Spy_see_shrK];
    1.53  
    1.54 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.55 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.56 -val major::prems = 
    1.57 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    1.58 -\             evs : ns_shared lost;                             \
    1.59 -\             A:lost ==> R                                  \
    1.60 -\           |] ==> R";
    1.61 -by (rtac ccontr 1);
    1.62 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    1.63 -by (swap_res_tac prems 2);
    1.64 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.65 -qed "Spy_see_shrK_E";
    1.66 +goal thy 
    1.67 + "!!evs. evs : ns_shared lost \
    1.68 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.69 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.70 +qed "Spy_analz_shrK";
    1.71 +Addsimps [Spy_analz_shrK];
    1.72  
    1.73 -bind_thm ("Spy_analz_shrK_E", 
    1.74 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    1.75 -
    1.76 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    1.77 -
    1.78 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.79 +\                  evs : ns_shared lost |] ==> A:lost";
    1.80 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.81 +qed "Spy_see_shrK_D";
    1.82  
    1.83 -goal thy  
    1.84 - "!!evs. evs : ns_shared lost ==>                              \
    1.85 -\        (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.86 -by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)]
    1.87 -                      addss (!simpset)) 1);
    1.88 -qed "shrK_mem_analz";
    1.89 -
    1.90 -Addsimps [shrK_mem_analz];
    1.91 -
    1.92 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.93 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.94  
    1.95  
    1.96  (*** Future keys can't be seen or used! ***)
    1.97 @@ -256,12 +238,7 @@
    1.98  \                       Crypt {|Key K, Agent A|} (shrK B)|} (shrK A))  \
    1.99  \             : set_of_list evs";
   1.100  by (etac rev_mp 1);
   1.101 -by (etac ns_shared.induct 1);
   1.102 -by parts_Fake_tac;
   1.103 -(*Fake case*)
   1.104 -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert]
   1.105 -                      addDs  [impOfSubs analz_subset_parts]
   1.106 -                      addss  (!simpset)) 2);
   1.107 +by (parts_induct_tac 1);
   1.108  by (Auto_tac());
   1.109  qed "A_trust_NS2";
   1.110  
   1.111 @@ -287,6 +264,13 @@
   1.112  qed "Says_S_message_form";
   1.113  
   1.114  
   1.115 +(*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.116 +val analz_Fake_tac = 
   1.117 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN
   1.118 +    forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN 
   1.119 +    Full_simp_tac 7 THEN
   1.120 +    REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac);
   1.121 +
   1.122  
   1.123  (****
   1.124   The following is to prove theorems of the form
   1.125 @@ -320,45 +304,13 @@
   1.126  
   1.127  (** Session keys are not used to encrypt other session keys **)
   1.128  
   1.129 -(*Describes the form of Key K when the following message is sent.  The use of
   1.130 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.131 -  assumption A ~: lost prevents its being a Faked message. *)
   1.132 -goal thy
   1.133 - "!!evs. evs: ns_shared lost ==>                                           \
   1.134 -\        Crypt {|NA, Agent B, Key K, X|} (shrK A)          \
   1.135 -\          : parts (sees lost Spy evs)   &   A ~: lost              \
   1.136 -\        --> (EX evt: ns_shared lost. K = newK evt)";
   1.137 -by (parts_induct_tac 1);
   1.138 -by (Auto_tac());
   1.139 -val lemma = result() RS mp;
   1.140 -
   1.141 -
   1.142 -(*EITHER describes the form of Key K when the following message is sent, 
   1.143 -  OR     reduces it to the Fake case.*)
   1.144 -goal thy 
   1.145 - "!!evs. [| Says S A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   1.146 -\           : set_of_list evs;  \
   1.147 -\           evs : ns_shared lost |]                      \
   1.148 -\        ==> (EX evt: ns_shared lost. K = newK evt)          \
   1.149 -\          | Key K : analz (sees lost Spy evs)";
   1.150 -by (case_tac "A : lost" 1);
   1.151 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.152 -                      addss (!simpset)) 1);
   1.153 -by (forward_tac [lemma] 1);
   1.154 -by (fast_tac (!claset addEs  partsEs
   1.155 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   1.156 -by (Fast_tac 1);
   1.157 -qed "Reveal_message_form";
   1.158 -
   1.159  (*The equality makes the induction hypothesis easier to apply*)
   1.160  goal thy  
   1.161   "!!evs. evs : ns_shared lost ==> \
   1.162  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   1.163  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   1.164  by (etac ns_shared.induct 1);
   1.165 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.166 -by (dtac Reveal_message_form 8);
   1.167 -by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac));
   1.168 +by analz_Fake_tac;
   1.169  by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma]));
   1.170  by (ALLGOALS 
   1.171      (asm_simp_tac 
   1.172 @@ -366,8 +318,8 @@
   1.173                           @ pushes)
   1.174                 setloop split_tac [expand_if])));
   1.175  (** LEVEL 6 **)
   1.176 -(*Reveal case 2, NS3, Fake*) 
   1.177 -by (EVERY (map spy_analz_tac [7,5,2]));
   1.178 +(*NS3, Fake*) 
   1.179 +by (EVERY (map spy_analz_tac [5,2]));
   1.180  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.181  (*NS3, NS2, Base*)
   1.182  by (REPEAT (Fast_tac 3));
   1.183 @@ -393,10 +345,8 @@
   1.184  \       Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))         \
   1.185  \       : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'";
   1.186  by (etac ns_shared.induct 1);
   1.187 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.188 -by (REPEAT_FIRST (eresolve_tac [conjE, bexE, disjE] ORELSE' hyp_subst_tac));
   1.189  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.190 -by (step_tac (!claset delrules [conjI]) 1);
   1.191 +by (Step_tac 1);
   1.192  (*NS3*)
   1.193  by (ex_strip_tac 2);
   1.194  by (Fast_tac 2);
   1.195 @@ -438,9 +388,7 @@
   1.196  \        (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \
   1.197  \        Key K ~: analz (sees lost Spy evs)";
   1.198  by (etac ns_shared.induct 1);
   1.199 -by (forward_tac [Reveal_message_form] 8);
   1.200 -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5);     
   1.201 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.202 +by analz_Fake_tac;
   1.203  by (ALLGOALS 
   1.204      (asm_simp_tac 
   1.205       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.206 @@ -450,9 +398,9 @@
   1.207  by (fast_tac (!claset addIs [parts_insertI]
   1.208                        addEs [Says_imp_old_keys RS less_irrefl]
   1.209                        addss (!simpset)) 2);
   1.210 -(*Revl case 2, OR4, OR2, Fake*) 
   1.211 +(*OR4, OR2, Fake*) 
   1.212  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.213 -(*NS3 and Revl subcases*) (**LEVEL 7 **)
   1.214 +(*NS3 and Oops subcases*) (**LEVEL 7 **)
   1.215  by (step_tac (!claset delrules [impCE]) 1);
   1.216  by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2);
   1.217  be conjE 2;
   1.218 @@ -555,11 +503,11 @@
   1.219  val lemma = result();
   1.220  
   1.221  goal thy
   1.222 - "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs);            \
   1.223 + "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs);           \
   1.224  \           Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A))  \
   1.225 -\           : set_of_list evs;            \
   1.226 +\           : set_of_list evs;                                        \
   1.227  \           ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs;  \
   1.228 -\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]            \
   1.229 +\           A ~: lost;  B ~: lost;  evs : ns_shared lost |]           \
   1.230  \        ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs";
   1.231  by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp]
   1.232  		      addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1);
     2.1 --- a/src/HOL/Auth/NS_Shared.thy	Sun Oct 27 13:47:02 1996 +0100
     2.2 +++ b/src/HOL/Auth/NS_Shared.thy	Mon Oct 28 12:55:24 1996 +0100
     2.3 @@ -67,10 +67,11 @@
     2.4            ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost"
     2.5    
     2.6           (*This message models possible leaks of session keys.
     2.7 -           The two Nonces identify the protocol run.*)
     2.8 -    Revl "[| evs: ns_shared lost;  A ~= Spy;
     2.9 -             Says B' A (Crypt (Nonce NB) K) : set_of_list evs;
    2.10 -             Says S  A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    2.11 +           The two Nonces identify the protocol run: the rule insists upon
    2.12 +           the true senders in order to make them accurate.*)
    2.13 +    Oops "[| evs: ns_shared lost;  A ~= Spy;
    2.14 +             Says B A (Crypt (Nonce NB) K) : set_of_list evs;
    2.15 +             Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A))
    2.16                 : set_of_list evs |]
    2.17            ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost"
    2.18  
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Sun Oct 27 13:47:02 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Mon Oct 28 12:55:24 1996 +0100
     3.3 @@ -59,16 +59,15 @@
     3.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     3.5  qed "OR4_analz_sees_Spy";
     3.6  
     3.7 -goal thy "!!evs. Says B' A (Crypt {|N,Agent A,B,K|} K') : set_of_list evs ==> \
     3.8 -\                K : parts (sees lost Spy evs)";
     3.9 +goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \
    3.10 +\                  : set_of_list evs ==> K : parts (sees lost Spy evs)";
    3.11  by (fast_tac (!claset addSEs partsEs
    3.12                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    3.13 -qed "Reveal_parts_sees_Spy";
    3.14 +qed "Oops_parts_sees_Spy";
    3.15  
    3.16 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    3.17 +(*OR4_analz_sees_Spy lets us treat those cases using the same 
    3.18    argument as for the Fake case.  This is possible for most, but not all,
    3.19 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    3.20 -  messages originate from the Spy. *)
    3.21 +  proofs, since Fake messages originate from the Spy. *)
    3.22  
    3.23  bind_thm ("OR4_parts_sees_Spy",
    3.24            OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts));
    3.25 @@ -77,7 +76,7 @@
    3.26    harder to complete, since simplification does less for us.*)
    3.27  val parts_Fake_tac = 
    3.28      forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN
    3.29 -    forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 7;
    3.30 +    forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7;
    3.31  
    3.32  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    3.33  fun parts_induct_tac i = SELECT_GOAL
    3.34 @@ -95,34 +94,27 @@
    3.35  
    3.36  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    3.37  goal thy 
    3.38 - "!!evs. [| evs : otway lost;  A ~: lost |]    \
    3.39 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    3.40 + "!!evs. evs : otway lost \
    3.41 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    3.42  by (parts_induct_tac 1);
    3.43  by (Auto_tac());
    3.44 -qed "Spy_not_see_shrK";
    3.45 -
    3.46 -bind_thm ("Spy_not_analz_shrK",
    3.47 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    3.48 -
    3.49 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    3.50 +qed "Spy_see_shrK";
    3.51 +Addsimps [Spy_see_shrK];
    3.52  
    3.53 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    3.54 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    3.55 -val major::prems = 
    3.56 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    3.57 -\             evs : otway lost;                                 \
    3.58 -\             A:lost ==> R                                  \
    3.59 -\           |] ==> R";
    3.60 -by (rtac ccontr 1);
    3.61 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    3.62 -by (swap_res_tac prems 2);
    3.63 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    3.64 -qed "Spy_see_shrK_E";
    3.65 +goal thy 
    3.66 + "!!evs. evs : otway lost \
    3.67 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    3.68 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    3.69 +qed "Spy_analz_shrK";
    3.70 +Addsimps [Spy_analz_shrK];
    3.71  
    3.72 -bind_thm ("Spy_analz_shrK_E", 
    3.73 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    3.74 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    3.75 +\                  evs : otway lost |] ==> A:lost";
    3.76 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    3.77 +qed "Spy_see_shrK_D";
    3.78  
    3.79 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    3.80 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    3.81 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    3.82  
    3.83  
    3.84  (*** Future keys can't be seen or used! ***)
    3.85 @@ -134,7 +126,7 @@
    3.86        The Union over C is essential for the induction! *)
    3.87  goal thy "!!evs. evs : otway lost ==> \
    3.88  \                length evs <= length evs' --> \
    3.89 -\                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    3.90 +\                Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    3.91  by (parts_induct_tac 1);
    3.92  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    3.93                                             impOfSubs parts_insert_subset_Un,
    3.94 @@ -224,39 +216,27 @@
    3.95  
    3.96  (*** Proofs involving analz ***)
    3.97  
    3.98 -(*Describes the form of Key K when the following message is sent.  The use of
    3.99 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   3.100 -  assumption A ~: lost prevents its being a Faked message.  (Based
   3.101 -  on NS_Shared/Says_S_message_form) *)
   3.102 -goal thy
   3.103 - "!!evs. evs: otway lost ==>                                           \
   3.104 -\        Crypt {|N, Agent A, B, Key K|} (shrK A) : parts (sees lost Spy evs)  \
   3.105 -\        --> A ~: lost --> (EX evt: otway lost. K = newK evt)";
   3.106 -by (parts_induct_tac 1);
   3.107 -by (Auto_tac());
   3.108 -qed_spec_mp "Reveal_message_lemma";
   3.109 -
   3.110 -(*EITHER describes the form of Key K when the following message is sent, 
   3.111 -  OR     reduces it to the Fake case.*)
   3.112 -
   3.113 +(*Describes the form of K and NA when the Server sends this message.*)
   3.114  goal thy 
   3.115 - "!!evs. [| Says B' A (Crypt {|N, Agent A, B, Key K|} (shrK A)) \
   3.116 -\            : set_of_list evs;                                 \
   3.117 -\           evs : otway lost |]                                 \
   3.118 -\        ==> (EX evt: otway lost. K = newK evt)                 \
   3.119 -\          | Key K : analz (sees lost Spy evs)";
   3.120 -br (Reveal_message_lemma RS disjCI) 1;
   3.121 -ba 1;
   3.122 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   3.123 -                      addDs [impOfSubs analz_subset_parts]) 1);
   3.124 -by (fast_tac (!claset addSDs [Says_Crypt_lost]) 1);
   3.125 -qed "Reveal_message_form";
   3.126 + "!!evs. [| Says Server B \
   3.127 +\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   3.128 +\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   3.129 +\           evs : otway lost |]                                        \
   3.130 +\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   3.131 +\            (EX i. NA = Nonce i) &                  \
   3.132 +\            (EX j. NB = Nonce j)";
   3.133 +by (etac rev_mp 1);
   3.134 +by (etac otway.induct 1);
   3.135 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.136 +qed "Says_Server_message_form";
   3.137  
   3.138  
   3.139  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   3.140  val analz_Fake_tac = 
   3.141      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   3.142 -    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   3.143 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   3.144 +    assume_tac 7 THEN Full_simp_tac 7 THEN
   3.145 +    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   3.146  
   3.147  
   3.148  (****
   3.149 @@ -280,16 +260,15 @@
   3.150  by (etac otway.induct 1);
   3.151  by analz_Fake_tac;
   3.152  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   3.153 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   3.154  by (ALLGOALS (*Takes 28 secs*)
   3.155      (asm_simp_tac 
   3.156       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   3.157                           @ pushes)
   3.158                 setloop split_tac [expand_if])));
   3.159  (** LEVEL 5 **)
   3.160 -(*Reveal case 2, OR4, Fake*) 
   3.161 -by (EVERY (map spy_analz_tac [6, 4, 2]));
   3.162 -(*Reveal case 1, OR3, Base*)
   3.163 +(*OR4, Fake*) 
   3.164 +by (EVERY (map spy_analz_tac [4,2]));
   3.165 +(*Oops, OR3, Base*)
   3.166  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   3.167  qed_spec_mp "analz_image_newK";
   3.168  
   3.169 @@ -306,8 +285,6 @@
   3.170  
   3.171  (*** The Key K uniquely identifies the Server's  message. **)
   3.172  
   3.173 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   3.174 -
   3.175  goal thy 
   3.176   "!!evs. evs : otway lost ==>                      \
   3.177  \      EX A' B' NA' NB'. ALL A B NA NB.                    \
   3.178 @@ -387,21 +364,6 @@
   3.179  qed "A_trust_OR4";
   3.180  
   3.181  
   3.182 -(*Describes the form of K and NA when the Server sends this message.*)
   3.183 -goal thy 
   3.184 - "!!evs. [| Says Server B \
   3.185 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   3.186 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   3.187 -\           evs : otway lost |]                                        \
   3.188 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   3.189 -\            (EX i. NA = Nonce i) &                  \
   3.190 -\            (EX j. NB = Nonce j)";
   3.191 -by (etac rev_mp 1);
   3.192 -by (etac otway.induct 1);
   3.193 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   3.194 -qed "Says_Server_message_form";
   3.195 -
   3.196 -
   3.197  (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   3.198      Does not in itself guarantee security: an attack could violate 
   3.199      the premises, e.g. by having A=Spy **)
   3.200 @@ -412,40 +374,31 @@
   3.201  \             {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A),            \
   3.202  \               Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|}           \
   3.203  \            : set_of_list evs -->                                         \
   3.204 -\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   3.205 +\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   3.206  \            Key K ~: analz (sees lost Spy evs)";
   3.207  by (etac otway.induct 1);
   3.208  by analz_Fake_tac;
   3.209 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   3.210  by (ALLGOALS
   3.211      (asm_full_simp_tac 
   3.212       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   3.213                            analz_insert_Key_newK] @ pushes)
   3.214                 setloop split_tac [expand_if])));
   3.215 -(** LEVEL 4 **)
   3.216  (*OR3*)
   3.217  by (fast_tac (!claset addSIs [parts_insertI]
   3.218                        addEs [Says_imp_old_keys RS less_irrefl]
   3.219                        addss (!simpset addsimps [parts_insert2])) 2);
   3.220 -(*Reveal case 2, OR4, Fake*) 
   3.221 +(*OR4, Fake*) 
   3.222  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   3.223 -(*Reveal case 1*) (** LEVEL 6 **)
   3.224 -by (case_tac "Aa : lost" 1);
   3.225 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   3.226 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   3.227 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   3.228 -(*So now we have  Aa ~: lost *)
   3.229 -by (dtac A_trust_OR4 1);
   3.230 -by (REPEAT (assume_tac 1));
   3.231 +(*Oops*) 
   3.232  by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   3.233  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   3.234  
   3.235  goal thy 
   3.236   "!!evs. [| Says Server B                                                     \
   3.237 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   3.238 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   3.239 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   3.240 -\           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   3.241 +\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   3.242 +\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   3.243 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                      \
   3.244 +\           A ~: lost;  B ~: lost;  evs : otway lost |]                       \
   3.245  \        ==> K ~: analz (sees lost Spy evs)";
   3.246  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   3.247  by (fast_tac (!claset addSEs [lemma]) 1);
   3.248 @@ -455,9 +408,9 @@
   3.249  goal thy 
   3.250   "!!evs. [| C ~: {A,B,Server};                                                \
   3.251  \           Says Server B                                                     \
   3.252 -\           {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                     \
   3.253 -\             Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \
   3.254 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   3.255 +\            {|Crypt {|NA, Agent A, Agent B, K|} (shrK A),                    \
   3.256 +\              Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\
   3.257 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   3.258  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   3.259  \        ==> K ~: analz (sees lost C evs)";
   3.260  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
     4.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Sun Oct 27 13:47:02 1996 +0100
     4.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Mon Oct 28 12:55:24 1996 +0100
     4.3 @@ -51,7 +51,7 @@
     4.4  
     4.5           (*Bob receives the Server's (?) message and compares the Nonces with
     4.6  	   those in the message he previously sent the Server.*)
     4.7 -    OR4  "[| evs: otway lost;  A ~= B;  B ~= Server;
     4.8 +    OR4  "[| evs: otway lost;  A ~= B;
     4.9               Says S B {|X, 
    4.10                          Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    4.11                 : set_of_list evs;
    4.12 @@ -59,12 +59,13 @@
    4.13                 : set_of_list evs |]
    4.14            ==> Says B A X # evs : otway lost"
    4.15  
    4.16 -         (*This message models possible leaks of session keys.  Alice's Nonce
    4.17 -           identifies the protocol run.*)
    4.18 -    Revl "[| evs: otway lost;  A ~= Spy;
    4.19 -             Says B' A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A))
    4.20 -               : set_of_list evs;
    4.21 -             Says A  B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |]
    4.22 -          ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
    4.23 +         (*This message models possible leaks of session keys.  The nonces
    4.24 +           identify the protocol run.  B is not assumed to know shrK A.*)
    4.25 +    Oops "[| evs: otway lost;  B ~= Spy;
    4.26 +             Says Server B 
    4.27 +                      {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), 
    4.28 +                        Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|}
    4.29 +               : set_of_list evs |]
    4.30 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    4.31  
    4.32  end
     5.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Sun Oct 27 13:47:02 1996 +0100
     5.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Mon Oct 28 12:55:24 1996 +0100
     5.3 @@ -68,11 +68,11 @@
     5.4  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
     5.5  qed "OR4_analz_sees_Spy";
     5.6  
     5.7 -goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
     5.8 -\                K : parts (sees lost Spy evs)";
     5.9 +goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
    5.10 +\                 ==> K : parts (sees lost Spy evs)";
    5.11  by (fast_tac (!claset addSEs partsEs
    5.12                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    5.13 -qed "Reveal_parts_sees_Spy";
    5.14 +qed "Oops_parts_sees_Spy";
    5.15  
    5.16  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    5.17    argument as for the Fake case.  This is possible for most, but not all,
    5.18 @@ -87,46 +87,46 @@
    5.19  val parts_Fake_tac = 
    5.20      forward_tac [OR2_parts_sees_Spy] 4 THEN 
    5.21      forward_tac [OR4_parts_sees_Spy] 6 THEN
    5.22 -    forward_tac [Reveal_parts_sees_Spy] 7;
    5.23 +    forward_tac [Oops_parts_sees_Spy] 7;
    5.24 +
    5.25 +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    5.26 +fun parts_induct_tac i = SELECT_GOAL
    5.27 +    (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN
    5.28 +	     (*Fake message*)
    5.29 +	     TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    5.30 +					   impOfSubs Fake_parts_insert]
    5.31 +                                    addss (!simpset)) 2)) THEN
    5.32 +     (*Base case*)
    5.33 +     fast_tac (!claset addss (!simpset)) 1 THEN
    5.34 +     ALLGOALS Asm_simp_tac) i;
    5.35  
    5.36  
    5.37  (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY
    5.38      sends messages containing X! **)
    5.39  
    5.40 -(*Spy never sees another agent's shared key! (unless it is leaked at start)*)
    5.41 +(*Spy never sees another agent's shared key! (unless it's lost at start)*)
    5.42  goal thy 
    5.43 - "!!evs. [| evs : otway;  A ~: lost |]    \
    5.44 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    5.45 -by (etac otway.induct 1);
    5.46 -by parts_Fake_tac;
    5.47 + "!!evs. evs : otway \
    5.48 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    5.49 +by (parts_induct_tac 1);
    5.50  by (Auto_tac());
    5.51 -(*Deals with Fake message*)
    5.52 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
    5.53 -                             impOfSubs Fake_parts_insert]) 1);
    5.54 -qed "Spy_not_see_shrK";
    5.55 -
    5.56 -bind_thm ("Spy_not_analz_shrK",
    5.57 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    5.58 -
    5.59 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    5.60 +qed "Spy_see_shrK";
    5.61 +Addsimps [Spy_see_shrK];
    5.62  
    5.63 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    5.64 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    5.65 -val major::prems = 
    5.66 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    5.67 -\             evs : otway;                                 \
    5.68 -\             A:lost ==> R                                  \
    5.69 -\           |] ==> R";
    5.70 -by (rtac ccontr 1);
    5.71 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    5.72 -by (swap_res_tac prems 2);
    5.73 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    5.74 -qed "Spy_see_shrK_E";
    5.75 +goal thy 
    5.76 + "!!evs. evs : otway \
    5.77 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    5.78 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    5.79 +qed "Spy_analz_shrK";
    5.80 +Addsimps [Spy_analz_shrK];
    5.81  
    5.82 -bind_thm ("Spy_analz_shrK_E", 
    5.83 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    5.84 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    5.85 +\                  evs : otway |] ==> A:lost";
    5.86 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    5.87 +qed "Spy_see_shrK_D";
    5.88  
    5.89 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    5.90 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    5.91 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    5.92  
    5.93  
    5.94  (*** Future keys can't be seen or used! ***)
    5.95 @@ -139,10 +139,7 @@
    5.96  goal thy "!!evs. evs : otway ==> \
    5.97  \                length evs <= length evs' --> \
    5.98  \                          Key (newK evs') ~: (UN C. parts (sees lost C evs))";
    5.99 -by (etac otway.induct 1);
   5.100 -by parts_Fake_tac;
   5.101 -(*auto_tac does not work here, as it performs safe_tac first*)
   5.102 -by (ALLGOALS Asm_simp_tac);
   5.103 +by (parts_induct_tac 1);
   5.104  by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   5.105                                         impOfSubs parts_insert_subset_Un,
   5.106                                         Suc_leD]
   5.107 @@ -214,9 +211,7 @@
   5.108  goal thy "!!evs. evs : otway ==> \
   5.109  \                length evs <= length evs' --> \
   5.110  \                newK evs' ~: keysFor (UN C. parts (sees lost C evs))";
   5.111 -by (etac otway.induct 1);
   5.112 -by parts_Fake_tac;
   5.113 -by (ALLGOALS Asm_simp_tac);
   5.114 +by (parts_induct_tac 1);
   5.115  (*OR1 and OR3*)
   5.116  by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2]));
   5.117  (*Fake, OR2, OR4: these messages send unknown (X) components*)
   5.118 @@ -242,7 +237,30 @@
   5.119  Addsimps [new_keys_not_used, new_keys_not_analzd];
   5.120  
   5.121  
   5.122 -(** Lemmas concerning the form of items passed in messages **)
   5.123 +
   5.124 +(*** Proofs involving analz ***)
   5.125 +
   5.126 +(*Describes the form of K and NA when the Server sends this message.  Also
   5.127 +  for Oops case.*)
   5.128 +goal thy 
   5.129 + "!!evs. [| Says Server B \
   5.130 +\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   5.131 +\           evs : otway |]                                   \
   5.132 +\        ==> (EX evt: otway. K = Key(newK evt)) &            \
   5.133 +\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   5.134 +by (etac rev_mp 1);
   5.135 +by (etac otway.induct 1);
   5.136 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   5.137 +qed "Says_Server_message_form";
   5.138 +
   5.139 +
   5.140 +(*For proofs involving analz.*)
   5.141 +val analz_Fake_tac = 
   5.142 +    dtac OR2_analz_sees_Spy 4 THEN 
   5.143 +    dtac OR4_analz_sees_Spy 6 THEN
   5.144 +    forward_tac [Says_Server_message_form] 7 THEN
   5.145 +    assume_tac 7 THEN Full_simp_tac 7 THEN
   5.146 +    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   5.147  
   5.148  
   5.149  (****
   5.150 @@ -258,40 +276,6 @@
   5.151  
   5.152  (** Session keys are not used to encrypt other session keys **)
   5.153  
   5.154 -(*Describes the form of Key K when the following message is sent.  The use of
   5.155 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   5.156 -  assumptions on A are needed to prevent its being a Faked message.  (Based
   5.157 -  on NS_Shared/Says_S_message_form) *)
   5.158 -goal thy
   5.159 - "!!evs. evs: otway ==>  \
   5.160 -\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \
   5.161 -\          A ~: lost --> \
   5.162 -\        (EX evt:otway. K = newK evt)";
   5.163 -by (etac otway.induct 1);
   5.164 -by parts_Fake_tac;
   5.165 -by (Auto_tac());
   5.166 -(*Deals with Fake message*)
   5.167 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
   5.168 -                             impOfSubs Fake_parts_insert]) 1);
   5.169 -val lemma = result() RS mp;
   5.170 -
   5.171 -
   5.172 -(*EITHER describes the form of Key K when the following message is sent, 
   5.173 -  OR     reduces it to the Fake case.*)
   5.174 -goal thy 
   5.175 - "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   5.176 -\           evs : otway |]                      \
   5.177 -\        ==> (EX evt:otway. K = newK evt) | Key K : analz (sees lost Spy evs)";
   5.178 -by (case_tac "A : lost" 1);
   5.179 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   5.180 -                      addss (!simpset)) 1);
   5.181 -by (forward_tac [lemma] 1);
   5.182 -by (fast_tac (!claset addEs  partsEs
   5.183 -                      addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
   5.184 -by (Fast_tac 1);
   5.185 -qed "Reveal_message_form";
   5.186 -
   5.187 -
   5.188  (*Lemma for the trivial direction of the if-and-only-if*)
   5.189  goal thy  
   5.190   "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   5.191 @@ -307,21 +291,18 @@
   5.192  \  ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \
   5.193  \           (K : newK``E | Key K : analz (sees lost Spy evs))";
   5.194  by (etac otway.induct 1);
   5.195 -by (dtac OR2_analz_sees_Spy 4);
   5.196 -by (dtac OR4_analz_sees_Spy 6);
   5.197 -by (dtac Reveal_message_form 7);
   5.198 +by analz_Fake_tac;
   5.199  by (REPEAT_FIRST (ares_tac [allI, lemma]));
   5.200 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   5.201 -by (ALLGOALS (*Takes 28 secs*)
   5.202 +by (ALLGOALS
   5.203      (asm_simp_tac 
   5.204       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   5.205                           @ pushes)
   5.206                 setloop split_tac [expand_if])));
   5.207  (** LEVEL 7 **)
   5.208 -(*Reveal case 2, OR4, OR2, Fake*) 
   5.209 -by (EVERY (map spy_analz_tac [7,5,3,2]));
   5.210 -(*Reveal case 1, OR3, Base*)
   5.211 -by (Auto_tac());
   5.212 +(*OR4, OR2, Fake*) 
   5.213 +by (EVERY (map spy_analz_tac [5,3,2]));
   5.214 +(*Oops, OR3, Base*)
   5.215 +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   5.216  qed_spec_mp "analz_image_newK";
   5.217  
   5.218  
   5.219 @@ -335,82 +316,13 @@
   5.220  qed "analz_insert_Key_newK";
   5.221  
   5.222  
   5.223 -(*Describes the form of K and NA when the Server sends this message.*)
   5.224 -goal thy 
   5.225 - "!!evs. [| Says Server B \
   5.226 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   5.227 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   5.228 -\           evs : otway |]                                        \
   5.229 -\        ==> (EX evt:otway. K = Key(newK evt)) &            \
   5.230 -\            (EX i. NA = Nonce i) &                  \
   5.231 -\            (EX j. NB = Nonce j)";
   5.232 -by (etac rev_mp 1);
   5.233 -by (etac otway.induct 1);
   5.234 -by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset))));
   5.235 -qed "Says_Server_message_form";
   5.236 -
   5.237 -
   5.238 -(*Crucial security property, but not itself enough to guarantee correctness!
   5.239 -  The need for quantification over N, C seems to indicate the problem.
   5.240 -  Omitting the Reveal message from the description deprives us of even 
   5.241 -        this clue. *)
   5.242 -goal thy 
   5.243 - "!!evs. [| A ~: lost;  B ~: lost;  evs : otway;  evt : otway |]        \
   5.244 -\    ==> Says Server B \
   5.245 -\          {|NA, Crypt {|NA, Key K|} (shrK A), \
   5.246 -\            Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
   5.247 -\        (ALL N C. Says C Spy {|N, Key K|} ~: set_of_list evs) --> \
   5.248 -\        Key K ~: analz (sees lost Spy evs)";
   5.249 -by (etac otway.induct 1);
   5.250 -by (dtac OR2_analz_sees_Spy 4);
   5.251 -by (dtac OR4_analz_sees_Spy 6);
   5.252 -by (dtac Reveal_message_form 7);
   5.253 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   5.254 -by (ALLGOALS
   5.255 -    (asm_full_simp_tac 
   5.256 -     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   5.257 -                          analz_insert_Key_newK] @ pushes)
   5.258 -               setloop split_tac [expand_if])));
   5.259 -(** LEVEL 6 **)
   5.260 -(*Reveal case 1*)
   5.261 -by (Fast_tac 5);
   5.262 -(*OR3*)
   5.263 -by (fast_tac (!claset addSIs [parts_insertI]
   5.264 -                      addEs [Says_imp_old_keys RS less_irrefl]
   5.265 -                      addss (!simpset addsimps [parts_insert2])) 3);
   5.266 -(*Reveal case 2, OR4, OR2, Fake*) 
   5.267 -by (rtac conjI 3);
   5.268 -by (REPEAT (spy_analz_tac 1));
   5.269 -val lemma = result() RS mp RS mp RSN(2,rev_notE);
   5.270 -
   5.271 -
   5.272 -
   5.273 -(*WEAK VERSION: NEED TO ELIMINATE QUANTIFICATION OVER N, C!!*)
   5.274 -goal thy 
   5.275 - "!!evs. [| Says Server B \
   5.276 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   5.277 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   5.278 -\           (ALL N C. Says C Spy {|N, K|} ~: set_of_list evs);  \
   5.279 -\           A ~: lost;  B ~: lost;  evs : otway |]                  \
   5.280 -\        ==> K ~: analz (sees lost Spy evs)";
   5.281 -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.282 -by (fast_tac (!claset addSEs [lemma]) 1);
   5.283 -qed "Spy_not_see_encrypted_key";
   5.284 -
   5.285 -
   5.286 -(*** Attempting to prove stronger properties ***)
   5.287 -
   5.288 -(** The Key K uniquely identifies the Server's  message. **)
   5.289 -
   5.290 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   5.291 +(*** The Key K uniquely identifies the Server's  message. **)
   5.292  
   5.293  goal thy 
   5.294 - "!!evs. evs : otway ==>                      \
   5.295 -\      EX A' B' NA' NB'. ALL A B NA NB.                    \
   5.296 -\       Says Server B \
   5.297 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   5.298 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   5.299 -\       A=A' & B=B' & NA=NA' & NB=NB'";
   5.300 + "!!evs. evs : otway ==>                                                 \
   5.301 +\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
   5.302 +\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   5.303 +\     B=B' & NA=NA' & NB=NB' & X=X'";
   5.304  by (etac otway.induct 1);
   5.305  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   5.306  by (Step_tac 1);
   5.307 @@ -426,16 +338,11 @@
   5.308  val lemma = result();
   5.309  
   5.310  goal thy 
   5.311 - "!!evs. [| Says Server B                                          \
   5.312 -\              {|NA, Crypt {|NA, K|} (shrK A),                     \
   5.313 -\                    Crypt {|NB, K|} (shrK B)|}                    \
   5.314 + "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
   5.315  \            : set_of_list evs;                                    \ 
   5.316 -\           Says Server B'                                         \
   5.317 -\              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   5.318 -\                     Crypt {|NB', K|} (shrK B')|}                 \
   5.319 +\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
   5.320  \            : set_of_list evs;                                    \
   5.321 -\           evs : otway |]                                         \
   5.322 -\        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   5.323 +\           evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   5.324  by (dtac lemma 1);
   5.325  by (REPEAT (etac exE 1));
   5.326  (*Duplicate the assumption*)
   5.327 @@ -444,59 +351,91 @@
   5.328  qed "unique_session_keys";
   5.329  
   5.330  
   5.331 +(*Crucial security property, but not itself enough to guarantee correctness!*)
   5.332 +goal thy 
   5.333 + "!!evs. [| A ~: lost;  B ~: lost;  evs : otway;  evt : otway |]        \
   5.334 +\    ==> Says Server B \
   5.335 +\          {|NA, Crypt {|NA, Key K|} (shrK A), \
   5.336 +\            Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \
   5.337 +\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   5.338 +\        Key K ~: analz (sees lost Spy evs)";
   5.339 +by (etac otway.induct 1);
   5.340 +by analz_Fake_tac;
   5.341 +by (ALLGOALS
   5.342 +    (asm_full_simp_tac 
   5.343 +     (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   5.344 +                          analz_insert_Key_newK] @ pushes)
   5.345 +               setloop split_tac [expand_if])));
   5.346 +(*OR3*)
   5.347 +by (fast_tac (!claset addSIs [parts_insertI]
   5.348 +                      addEs [Says_imp_old_keys RS less_irrefl]
   5.349 +                      addss (!simpset addsimps [parts_insert2])) 3);
   5.350 +(*OR4, OR2, Fake*) 
   5.351 +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   5.352 +(*Oops*) (** LEVEL 5 **)
   5.353 +by (fast_tac (!claset delrules [disjE]
   5.354 +		      addDs [unique_session_keys] addss (!simpset)) 1);
   5.355 +val lemma = result() RS mp RS mp RSN(2,rev_notE);
   5.356 +
   5.357 +
   5.358 +goal thy 
   5.359 + "!!evs. [| Says Server B                                         \
   5.360 +\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   5.361 +\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   5.362 +\            Says B Spy {|NA, NB, K|} ~: set_of_list evs;         \
   5.363 +\           A ~: lost;  B ~: lost;  evs : otway |]                \
   5.364 +\        ==> K ~: analz (sees lost Spy evs)";
   5.365 +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   5.366 +by (fast_tac (!claset addSEs [lemma]) 1);
   5.367 +qed "Spy_not_see_encrypted_key";
   5.368 +
   5.369 +
   5.370 +(*** Attempting to prove stronger properties ***)
   5.371 +
   5.372  (*Only OR1 can have caused such a part of a message to appear.
   5.373    I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it.
   5.374    Perhaps it's because OR2 has two similar-looking encrypted messages in
   5.375  	this version.*)
   5.376  goal thy 
   5.377 - "!!evs. [| A ~: lost;  A ~= B; evs : otway |]               \
   5.378 -\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)        \
   5.379 + "!!evs. [| A ~: lost;  A ~= B; evs : otway |]                 \
   5.380 +\        ==> Crypt {|NA, Agent A, Agent B|} (shrK A)           \
   5.381  \             : parts (sees lost Spy evs) -->                  \
   5.382 -\            Says A B {|NA, Agent A, Agent B,               \
   5.383 +\            Says A B {|NA, Agent A, Agent B,                  \
   5.384  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   5.385  \             : set_of_list evs";
   5.386 -by (etac otway.induct 1);
   5.387 -by parts_Fake_tac;
   5.388 -by (ALLGOALS Asm_simp_tac);
   5.389 -(*Fake*)
   5.390 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   5.391 -                              impOfSubs Fake_parts_insert]) 2);
   5.392 -by (Auto_tac());
   5.393 +by (parts_induct_tac 1);
   5.394 +by (Fast_tac 1);
   5.395  qed_spec_mp "Crypt_imp_OR1";
   5.396  
   5.397  
   5.398 -(*This key property is FALSE.  Somebody could make a fake message to Server
   5.399 +(*Crucial property: If the encrypted message appears, and A has used NA
   5.400 +  to start a run, then it originated with the Server!*)
   5.401 +(*Only it is FALSE.  Somebody could make a fake message to Server
   5.402            substituting some other nonce NA' for NB.*)
   5.403  goal thy 
   5.404   "!!evs. [| A ~: lost;  A ~= Spy;  evs : otway |]                        \
   5.405  \        ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \
   5.406 -\            Says A B {|NA, Agent A, Agent B,  \
   5.407 +\            Says A B {|NA, Agent A, Agent B,                  \
   5.408  \                       Crypt {|NA, Agent A, Agent B|} (shrK A)|}  \
   5.409 -\             : set_of_list evs --> \
   5.410 -\            (EX B NB. Says Server B               \
   5.411 -\                 {|NA,               \
   5.412 +\             : set_of_list evs -->                            \
   5.413 +\            (EX B NB. Says Server B                           \
   5.414 +\                 {|NA,                                        \
   5.415  \                   Crypt {|NA, Key K|} (shrK A),              \
   5.416  \                   Crypt {|NB, Key K|} (shrK B)|}             \
   5.417  \                   : set_of_list evs)";
   5.418 -by (etac otway.induct 1);
   5.419 -by parts_Fake_tac;
   5.420 -by (ALLGOALS Asm_simp_tac);
   5.421 -(*Fake*)
   5.422 -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts,
   5.423 -                              impOfSubs Fake_parts_insert]) 1);
   5.424 +by (parts_induct_tac 1);
   5.425  (*OR1: it cannot be a new Nonce, contradiction.*)
   5.426  by (fast_tac (!claset addSIs [parts_insertI]
   5.427                        addSEs partsEs
   5.428                        addEs [Says_imp_old_nonces RS less_irrefl]
   5.429                        addss (!simpset)) 1);
   5.430 -(*OR3 and OR4*)  (** LEVEL 5 **)
   5.431  (*OR4*)
   5.432  by (REPEAT (Safe_step_tac 2));
   5.433  by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3));
   5.434  by (fast_tac (!claset addSIs [Crypt_imp_OR1]
   5.435                        addEs  partsEs
   5.436                        addDs [Says_imp_sees_Spy RS parts.Inj]) 2);
   5.437 -(*OR3*)  (** LEVEL 8 **)
   5.438 +(*OR3*)  (** LEVEL 5 **)
   5.439  by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib])));
   5.440  by (step_tac (!claset delrules [disjCI, impCE]) 1);
   5.441  (*The hypotheses at this point suggest an attack in which nonce NA is used
   5.442 @@ -511,7 +450,7 @@
   5.443               Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
   5.444            : set_of_list evsa 
   5.445  *)
   5.446 -writeln "GIVE UP!";
   5.447 +writeln "GIVE UP! on NA_Crypt_imp_Server_msg";
   5.448  
   5.449  
   5.450  (*Thus the key property A_can_trust probably fails too.*)
     6.1 --- a/src/HOL/Auth/OtwayRees_Bad.thy	Sun Oct 27 13:47:02 1996 +0100
     6.2 +++ b/src/HOL/Auth/OtwayRees_Bad.thy	Mon Oct 28 12:55:24 1996 +0100
     6.3 @@ -61,21 +61,18 @@
     6.4  
     6.5           (*Bob receives the Server's (?) message and compares the Nonces with
     6.6  	   those in the message he previously sent the Server.*)
     6.7 -    OR4  "[| evs: otway;  A ~= B;  B ~= Server;
     6.8 +    OR4  "[| evs: otway;  A ~= B;
     6.9               Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    6.10                 : set_of_list evs;
    6.11               Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|}
    6.12                 : set_of_list evs |]
    6.13            ==> Says B A {|Nonce NA, X|} # evs : otway"
    6.14  
    6.15 -         (*This message models possible leaks of session keys.  Alice's Nonce
    6.16 -           identifies the protocol run.*)
    6.17 -    Revl "[| evs: otway;  A ~= Spy;
    6.18 -             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    6.19 -               : set_of_list evs;
    6.20 -             Says A  B {|Nonce NA, Agent A, Agent B, 
    6.21 -                         Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    6.22 +         (*This message models possible leaks of session keys.  The nonces
    6.23 +           identify the protocol run.*)
    6.24 +    Oops "[| evs: otway;  B ~= Spy;
    6.25 +             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    6.26                 : set_of_list evs |]
    6.27 -          ==> Says A Spy {|Nonce NA, Key K|} # evs : otway"
    6.28 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway"
    6.29  
    6.30  end