src/HOL/Auth/OtwayRees_Bad.ML
changeset 4537 4e835bd9fada
parent 4509 828148415197
child 4598 649bf14debe7
     1.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:09:47 1998 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Thu Jan 08 18:10:34 1998 +0100
     1.3 @@ -20,6 +20,10 @@
     1.4  set proof_timing;
     1.5  HOL_quantifiers := false;
     1.6  
     1.7 +AddEs spies_partsEs;
     1.8 +AddDs [impOfSubs analz_subset_parts];
     1.9 +AddDs [impOfSubs Fake_parts_insert];
    1.10 +
    1.11  
    1.12  (*A "possibility property": there are traces that reach the end*)
    1.13  goal thy 
    1.14 @@ -46,26 +50,23 @@
    1.15  
    1.16  (** For reasoning about the encrypted portion of messages **)
    1.17  
    1.18 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs ==> \
    1.19 -\                X : analz (spies evs)";
    1.20 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.21 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    1.22 +\                ==> X : analz (spies evs)";
    1.23 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    1.24 +by (Blast_tac 1);
    1.25  qed "OR2_analz_spies";
    1.26  
    1.27 -goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs ==> \
    1.28 -\                X : analz (spies evs)";
    1.29 -by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1);
    1.30 +goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    1.31 +\                ==> X : analz (spies evs)";
    1.32 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    1.33 +by (Blast_tac 1);
    1.34  qed "OR4_analz_spies";
    1.35  
    1.36  goal thy "!!evs. Says Server B {|NA, X, Crypt K' {|NB,K|}|} : set evs \
    1.37 -\                 ==> K : parts (spies evs)";
    1.38 -by (blast_tac (claset() addSEs spies_partsEs) 1);
    1.39 +\                ==> K : parts (spies evs)";
    1.40 +by (Blast_tac 1);
    1.41  qed "Oops_parts_spies";
    1.42  
    1.43 -(*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.44 -  argument as for the Fake case.  This is possible for most, but not all,
    1.45 -  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    1.46 -  messages originate from the Spy. *)
    1.47 -
    1.48  bind_thm ("OR2_parts_spies",
    1.49            OR2_analz_spies RS (impOfSubs analz_subset_parts));
    1.50  bind_thm ("OR4_parts_spies",
    1.51 @@ -83,11 +84,10 @@
    1.52  (** Theorems of the form X ~: parts (spies evs) imply that NOBODY
    1.53      sends messages containing X! **)
    1.54  
    1.55 -(*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.56 +(*Spy never sees a good agent's shared key!*)
    1.57  goal thy 
    1.58   "!!evs. evs : otway ==> (Key (shrK A) : parts (spies evs)) = (A : bad)";
    1.59  by (parts_induct_tac 1);
    1.60 -by (Fake_parts_insert_tac 1);
    1.61  by (ALLGOALS Blast_tac);
    1.62  qed "Spy_see_shrK";
    1.63  Addsimps [Spy_see_shrK];
    1.64 @@ -108,7 +108,7 @@
    1.65  by (parts_induct_tac 1);
    1.66  (*Fake*)
    1.67  by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1);
    1.68 -(*OR1-3*)
    1.69 +(*OR2, OR3*)
    1.70  by (ALLGOALS Blast_tac);
    1.71  qed_spec_mp "new_keys_not_used";
    1.72  
    1.73 @@ -125,14 +125,13 @@
    1.74  (*Describes the form of K and NA when the Server sends this message.  Also
    1.75    for Oops case.*)
    1.76  goal thy 
    1.77 - "!!evs. [| Says Server B                                                 \
    1.78 -\            {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs;           \
    1.79 -\           evs : otway |]                                                \
    1.80 + "!!evs. [| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \
    1.81 +\           evs : otway |]                                           \
    1.82  \     ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
    1.83  by (etac rev_mp 1);
    1.84  by (etac otway.induct 1);
    1.85 -by (prove_simple_subgoals_tac 1);
    1.86 -by (Blast_tac 1); 
    1.87 +by (ALLGOALS Simp_tac);
    1.88 +by (ALLGOALS Blast_tac);
    1.89  qed "Says_Server_message_form";
    1.90  
    1.91  
    1.92 @@ -140,7 +139,7 @@
    1.93  val analz_spies_tac = 
    1.94      dtac OR2_analz_spies 4 THEN 
    1.95      dtac OR4_analz_spies 6 THEN
    1.96 -    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN 
    1.97 +    forward_tac [Says_Server_message_form] 7 THEN assume_tac 7 THEN
    1.98      REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 7);
    1.99  
   1.100  
   1.101 @@ -192,12 +191,11 @@
   1.102  by (ALLGOALS Clarify_tac);
   1.103  (*Remaining cases: OR3 and OR4*)
   1.104  by (ex_strip_tac 2);
   1.105 -by (Blast_tac 2);
   1.106 +by (Best_tac 2);	(*Blast_tac's too slow (in reconstruction)*)
   1.107  by (expand_case_tac "K = ?y" 1);
   1.108  by (REPEAT (ares_tac [refl,exI,impI,conjI] 2));
   1.109  (*...we assume X is a recent message, and handle this case by contradiction*)
   1.110 -by (blast_tac (claset() addSEs spies_partsEs
   1.111 -                      delrules [conjI]    (*no split-up to 4 subgoals*)) 1);
   1.112 +by (blast_tac (claset() addSEs spies_partsEs) 1);
   1.113  val lemma = result();
   1.114  
   1.115  goal thy 
   1.116 @@ -208,37 +206,39 @@
   1.117  qed "unique_session_keys";
   1.118  
   1.119  
   1.120 -(*Crucial security property, but not itself enough to guarantee correctness!*)
   1.121 +(** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.122 +    Does not in itself guarantee security: an attack could violate 
   1.123 +    the premises, e.g. by having A=Spy **)
   1.124 +
   1.125  goal thy 
   1.126 - "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                    \
   1.127 + "!!evs. [| A ~: bad;  B ~: bad;  evs : otway |]                      \
   1.128  \        ==> Says Server B                                            \
   1.129  \              {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.130  \                Crypt (shrK B) {|NB, Key K|}|} : set evs -->         \
   1.131 -\            Says B Spy {|NA, NB, Key K|} ~: set evs -->              \
   1.132 +\            Notes Spy {|NA, NB, Key K|} ~: set evs -->               \
   1.133  \            Key K ~: analz (spies evs)";
   1.134  by (etac otway.induct 1);
   1.135  by analz_spies_tac;
   1.136  by (ALLGOALS
   1.137      (asm_simp_tac (simpset() addcongs [conj_cong] 
   1.138 -                            addsimps [analz_insert_eq, analz_insert_freshK]
   1.139 -                            addsimps (pushes@expand_ifs))));
   1.140 +                             addsimps [analz_insert_eq, analz_insert_freshK]
   1.141 +                             addsimps (pushes@expand_ifs))));
   1.142  (*Oops*)
   1.143  by (blast_tac (claset() addSDs [unique_session_keys]) 4);
   1.144  (*OR4*) 
   1.145  by (Blast_tac 3);
   1.146  (*OR3*)
   1.147 -by (blast_tac (claset() addSEs spies_partsEs
   1.148 -                       addIs [impOfSubs analz_subset_parts]) 2);
   1.149 +by (Blast_tac 2);
   1.150  (*Fake*) 
   1.151  by (spy_analz_tac 1);
   1.152  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.153  
   1.154  goal thy 
   1.155 - "!!evs. [| Says Server B                                         \
   1.156 -\            {|NA, Crypt (shrK A) {|NA, Key K|},                  \
   1.157 -\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;      \
   1.158 -\           Says B Spy {|NA, NB, Key K|} ~: set evs;              \
   1.159 -\           A ~: bad;  B ~: bad;  evs : otway |]                \
   1.160 + "!!evs. [| Says Server B                                           \
   1.161 +\            {|NA, Crypt (shrK A) {|NA, Key K|},                    \
   1.162 +\                  Crypt (shrK B) {|NB, Key K|}|} : set evs;        \
   1.163 +\           Notes Spy {|NA, NB, Key K|} ~: set evs;                 \
   1.164 +\           A ~: bad;  B ~: bad;  evs : otway |]                    \
   1.165  \        ==> Key K ~: analz (spies evs)";
   1.166  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.167  by (blast_tac (claset() addSEs [lemma]) 1);
   1.168 @@ -257,8 +257,7 @@
   1.169  \            Says A B {|NA, Agent A, Agent B,                  \
   1.170  \                       Crypt (shrK A) {|NA, Agent A, Agent B|}|}  : set evs";
   1.171  by (parts_induct_tac 1);
   1.172 -by (Fake_parts_insert_tac 1);
   1.173 -by (Blast_tac 1);
   1.174 +by (ALLGOALS Blast_tac);
   1.175  qed_spec_mp "Crypt_imp_OR1";
   1.176  
   1.177  
   1.178 @@ -277,16 +276,15 @@
   1.179  \                   Crypt (shrK A) {|NA, Key K|},                    \
   1.180  \                   Crypt (shrK B) {|NB, Key K|}|}  : set evs)";
   1.181  by (parts_induct_tac 1);
   1.182 -by (Fake_parts_insert_tac 1);
   1.183 +(*Fake*)
   1.184 +by (Blast_tac 1);
   1.185  (*OR1: it cannot be a new Nonce, contradiction.*)
   1.186 -by (blast_tac (claset() addSIs [parts_insertI]
   1.187 -                       addSEs spies_partsEs) 1);
   1.188 +by (Blast_tac 1);
   1.189  (*OR3 and OR4*)
   1.190  by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib])));
   1.191  by (ALLGOALS Clarify_tac);
   1.192  (*OR4*)
   1.193 -by (blast_tac (claset() addSIs [Crypt_imp_OR1]
   1.194 -                       addEs  spies_partsEs) 2);
   1.195 +by (blast_tac (claset() addSIs [Crypt_imp_OR1]) 2);
   1.196  (*OR3*)  (** LEVEL 5 **)
   1.197  (*The hypotheses at this point suggest an attack in which nonce NB is used
   1.198    in two different roles: