Minor corrections
authorpaulson
Mon Oct 28 15:59:39 1996 +0100 (1996-10-28)
changeset 213580477862ab33
parent 2134 04a71407089d
child 2136 217ae06dc291
Minor corrections
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees.thy
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Oct 28 15:36:18 1996 +0100
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Oct 28 15:59:39 1996 +0100
     1.3 @@ -16,6 +16,7 @@
     1.4  
     1.5  proof_timing:=true;
     1.6  HOL_quantifiers := false;
     1.7 +Pretty.setdepth 15;
     1.8  
     1.9  
    1.10  (*Weak liveness: there are traces that reach the end*)
    1.11 @@ -54,21 +55,21 @@
    1.12  
    1.13  (** For reasoning about the encrypted portion of messages **)
    1.14  
    1.15 -goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs ==> \
    1.16 -\                X : analz (sees lost Spy evs)";
    1.17 +goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set_of_list evs \
    1.18 +\                ==> X : analz (sees lost Spy evs)";
    1.19  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.20  qed "OR2_analz_sees_Spy";
    1.21  
    1.22 -goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs ==> \
    1.23 -\                X : analz (sees lost Spy evs)";
    1.24 +goal thy "!!evs. Says S B {|N, X, X'|} : set_of_list evs \
    1.25 +\                ==> X : analz (sees lost Spy evs)";
    1.26  by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
    1.27  qed "OR4_analz_sees_Spy";
    1.28  
    1.29 -goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \
    1.30 -\                K : parts (sees lost Spy evs)";
    1.31 +goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \
    1.32 +\                 ==> K : parts (sees lost Spy evs)";
    1.33  by (fast_tac (!claset addSEs partsEs
    1.34                        addSDs [Says_imp_sees_Spy RS parts.Inj]) 1);
    1.35 -qed "Reveal_parts_sees_Spy";
    1.36 +qed "Oops_parts_sees_Spy";
    1.37  
    1.38  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
    1.39    argument as for the Fake case.  This is possible for most, but not all,
    1.40 @@ -86,7 +87,7 @@
    1.41      let val tac = forw_inst_tac [("lost","lost")] 
    1.42      in  tac OR2_parts_sees_Spy 4 THEN 
    1.43          tac OR4_parts_sees_Spy 6 THEN
    1.44 -        tac Reveal_parts_sees_Spy 7
    1.45 +        tac Oops_parts_sees_Spy 7
    1.46      end;
    1.47  
    1.48  (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
    1.49 @@ -105,34 +106,27 @@
    1.50  
    1.51  (*Spy never sees another agent's shared key! (unless it's lost at start)*)
    1.52  goal thy 
    1.53 - "!!evs. [| evs : otway lost;  A ~: lost |]    \
    1.54 -\        ==> Key (shrK A) ~: parts (sees lost Spy evs)";
    1.55 + "!!evs. evs : otway lost \
    1.56 +\        ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
    1.57  by (parts_induct_tac 1);
    1.58  by (Auto_tac());
    1.59 -qed "Spy_not_see_shrK";
    1.60 -
    1.61 -bind_thm ("Spy_not_analz_shrK",
    1.62 -          [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD);
    1.63 -
    1.64 -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK];
    1.65 +qed "Spy_see_shrK";
    1.66 +Addsimps [Spy_see_shrK];
    1.67  
    1.68 -(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    1.69 -  As usual fast_tac cannot be used because it uses the equalities too soon*)
    1.70 -val major::prems = 
    1.71 -goal thy  "[| Key (shrK A) : parts (sees lost Spy evs);       \
    1.72 -\             evs : otway lost;                                 \
    1.73 -\             A:lost ==> R                                  \
    1.74 -\           |] ==> R";
    1.75 -by (rtac ccontr 1);
    1.76 -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1);
    1.77 -by (swap_res_tac prems 2);
    1.78 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    1.79 -qed "Spy_see_shrK_E";
    1.80 +goal thy 
    1.81 + "!!evs. evs : otway lost \
    1.82 +\        ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)";
    1.83 +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset));
    1.84 +qed "Spy_analz_shrK";
    1.85 +Addsimps [Spy_analz_shrK];
    1.86  
    1.87 -bind_thm ("Spy_analz_shrK_E", 
    1.88 -          analz_subset_parts RS subsetD RS Spy_see_shrK_E);
    1.89 +goal thy  "!!A. [| Key (shrK A) : parts (sees lost Spy evs);       \
    1.90 +\                  evs : otway lost |] ==> A:lost";
    1.91 +by (fast_tac (!claset addDs [Spy_see_shrK]) 1);
    1.92 +qed "Spy_see_shrK_D";
    1.93  
    1.94 -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E];
    1.95 +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D);
    1.96 +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
    1.97  
    1.98  
    1.99  (*** Future keys can't be seen or used! ***)
   1.100 @@ -246,40 +240,27 @@
   1.101  
   1.102  (*** Proofs involving analz ***)
   1.103  
   1.104 -(*Describes the form of Key K when the following message is sent.  The use of
   1.105 -  "parts" strengthens the induction hyp for proving the Fake case.  The
   1.106 -  assumption A ~: lost prevents its being a Faked message.  (Based
   1.107 -  on NS_Shared/Says_S_message_form) *)
   1.108 -goal thy
   1.109 - "!!evs. evs: otway lost ==>                                           \
   1.110 -\          Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) &   \
   1.111 -\          A ~: lost -->                                               \
   1.112 -\        (EX evt: otway lost. K = newK evt)";
   1.113 -by (parts_induct_tac 1);
   1.114 -by (Auto_tac());
   1.115 -qed_spec_mp "Reveal_message_lemma";
   1.116 -
   1.117 -(*EITHER describes the form of Key K when the following message is sent, 
   1.118 -  OR     reduces it to the Fake case.*)
   1.119 -
   1.120 +(*Describes the form of K and NA when the Server sends this message.  Also
   1.121 +  for Oops case.*)
   1.122  goal thy 
   1.123 - "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs;  \
   1.124 -\           evs : otway lost |]                      \
   1.125 -\        ==> (EX evt: otway lost. K = newK evt)          \
   1.126 -\          | Key K : analz (sees lost Spy evs)";
   1.127 -br (Reveal_message_lemma RS disjCI) 1;
   1.128 -ba 1;
   1.129 -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
   1.130 -                      addDs [impOfSubs analz_subset_parts]
   1.131 -                      addss (!simpset)) 1);
   1.132 -qed "Reveal_message_form";
   1.133 + "!!evs. [| Says Server B \
   1.134 +\            {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.135 +\           evs : otway lost |]                                   \
   1.136 +\        ==> (EX evt: otway lost. K = Key(newK evt)) &            \
   1.137 +\            (EX i. NA = Nonce i) & (EX j. NB = Nonce j)";
   1.138 +by (etac rev_mp 1);
   1.139 +by (etac otway.induct 1);
   1.140 +by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.141 +qed "Says_Server_message_form";
   1.142  
   1.143  
   1.144  (*For proofs involving analz.  We again instantiate the variable to "lost".*)
   1.145  val analz_Fake_tac = 
   1.146      dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN 
   1.147      dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN
   1.148 -    forw_inst_tac [("lost","lost")] Reveal_message_form 7;
   1.149 +    forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN
   1.150 +    assume_tac 7 THEN Full_simp_tac 7 THEN
   1.151 +    REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7);
   1.152  
   1.153  
   1.154  (****
   1.155 @@ -289,7 +270,6 @@
   1.156            Key K : analz (sees lost Spy evs)
   1.157  
   1.158   A more general formula must be proved inductively.
   1.159 -
   1.160  ****)
   1.161  
   1.162  
   1.163 @@ -303,16 +283,15 @@
   1.164  by (etac otway.induct 1);
   1.165  by analz_Fake_tac;
   1.166  by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
   1.167 -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7));
   1.168 -by (ALLGOALS (*Takes 28 secs*)
   1.169 +by (ALLGOALS (*Takes 22 secs*)
   1.170      (asm_simp_tac 
   1.171       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   1.172                           @ pushes)
   1.173                 setloop split_tac [expand_if])));
   1.174  (** LEVEL 5 **)
   1.175 -(*Reveal case 2, OR4, OR2, Fake*) 
   1.176 -by (EVERY (map spy_analz_tac [7,5,3,2]));
   1.177 -(*Reveal case 1, OR3, Base*)
   1.178 +(*OR4, OR2, Fake*) 
   1.179 +by (EVERY (map spy_analz_tac [5,3,2]));
   1.180 +(*Oops, OR3, Base*)
   1.181  by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1));
   1.182  qed_spec_mp "analz_image_newK";
   1.183  
   1.184 @@ -329,15 +308,11 @@
   1.185  
   1.186  (*** The Key K uniquely identifies the Server's  message. **)
   1.187  
   1.188 -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1);
   1.189 -
   1.190  goal thy 
   1.191 - "!!evs. evs : otway lost ==>                      \
   1.192 -\      EX A' B' NA' NB'. ALL A B NA NB.                    \
   1.193 -\       Says Server B \
   1.194 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.195 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   1.196 -\       A=A' & B=B' & NA=NA' & NB=NB'";
   1.197 + "!!evs. evs : otway lost ==>                                                 \
   1.198 +\   EX B' NA' NB' X'. ALL B NA NB X.                                          \
   1.199 +\     Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \
   1.200 +\     B=B' & NA=NA' & NB=NB' & X=X'";
   1.201  by (etac otway.induct 1);
   1.202  by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib])));
   1.203  by (Step_tac 1);
   1.204 @@ -353,16 +328,11 @@
   1.205  val lemma = result();
   1.206  
   1.207  goal thy 
   1.208 - "!!evs. [| Says Server B                                          \
   1.209 -\              {|NA, Crypt {|NA, K|} (shrK A),                     \
   1.210 -\                    Crypt {|NB, K|} (shrK B)|}                    \
   1.211 + "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|}      \
   1.212  \            : set_of_list evs;                                    \ 
   1.213 -\           Says Server B'                                         \
   1.214 -\              {|NA', Crypt {|NA', K|} (shrK A'),                  \
   1.215 -\                     Crypt {|NB', K|} (shrK B')|}                 \
   1.216 +\           Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|}    \
   1.217  \            : set_of_list evs;                                    \
   1.218 -\           evs : otway lost |]                                         \
   1.219 -\        ==> A=A' & B=B' & NA=NA' & NB=NB'";
   1.220 +\           evs : otway lost |] ==> X=X' & B=B' & NA=NA' & NB=NB'";
   1.221  by (dtac lemma 1);
   1.222  by (REPEAT (etac exE 1));
   1.223  (*Duplicate the assumption*)
   1.224 @@ -494,21 +464,6 @@
   1.225  qed "A_trust_OR4";
   1.226  
   1.227  
   1.228 -(*Describes the form of K and NA when the Server sends this message.*)
   1.229 -goal thy 
   1.230 - "!!evs. [| Says Server B \
   1.231 -\            {|NA, Crypt {|NA, K|} (shrK A),                      \
   1.232 -\                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;  \
   1.233 -\           evs : otway lost |]                                        \
   1.234 -\        ==> (EX evt: otway lost. K = Key(newK evt)) &                  \
   1.235 -\            (EX i. NA = Nonce i) &                  \
   1.236 -\            (EX j. NB = Nonce j)";
   1.237 -by (etac rev_mp 1);
   1.238 -by (etac otway.induct 1);
   1.239 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.240 -qed "Says_Server_message_form";
   1.241 -
   1.242 -
   1.243  (** Crucial secrecy property: Spy does not see the keys sent in msg OR3
   1.244      Does not in itself guarantee security: an attack could violate 
   1.245      the premises, e.g. by having A=Spy **)
   1.246 @@ -518,11 +473,10 @@
   1.247  \        ==> Says Server B                                                 \
   1.248  \              {|NA, Crypt {|NA, Key K|} (shrK A),                         \
   1.249  \                Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs -->      \
   1.250 -\            Says A Spy {|NA, Key K|} ~: set_of_list evs -->               \
   1.251 +\            Says B Spy {|NA, NB, Key K|} ~: set_of_list evs -->           \
   1.252  \            Key K ~: analz (sees lost Spy evs)";
   1.253  by (etac otway.induct 1);
   1.254  by analz_Fake_tac;
   1.255 -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac));
   1.256  by (ALLGOALS
   1.257      (asm_full_simp_tac 
   1.258       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   1.259 @@ -532,24 +486,18 @@
   1.260  by (fast_tac (!claset addSIs [parts_insertI]
   1.261                        addEs [Says_imp_old_keys RS less_irrefl]
   1.262                        addss (!simpset addsimps [parts_insert2])) 3);
   1.263 -(*Reveal case 2, OR4, OR2, Fake*) 
   1.264 +(*OR4, OR2, Fake*) 
   1.265  by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac));
   1.266 -(*Reveal case 1*) (** LEVEL 6 **)
   1.267 -by (case_tac "Aa : lost" 1);
   1.268 -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *)
   1.269 -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1);
   1.270 -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
   1.271 -(*So now we have  Aa ~: lost *)
   1.272 -by (dtac A_trust_OR4 1);
   1.273 -by (REPEAT (assume_tac 1));
   1.274 -by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1);
   1.275 +(*Oops*) (** LEVEL 5 **)
   1.276 +by (fast_tac (!claset delrules [disjE]
   1.277 +		      addDs [unique_session_keys] addss (!simpset)) 1);
   1.278  val lemma = result() RS mp RS mp RSN(2,rev_notE);
   1.279  
   1.280  goal thy 
   1.281   "!!evs. [| Says Server B \
   1.282  \            {|NA, Crypt {|NA, K|} (shrK A),                             \
   1.283  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   1.284 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.285 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   1.286  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.287  \        ==> K ~: analz (sees lost Spy evs)";
   1.288  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
   1.289 @@ -562,7 +510,7 @@
   1.290  \           Says Server B                                                \
   1.291  \            {|NA, Crypt {|NA, K|} (shrK A),                             \
   1.292  \                  Crypt {|NB, K|} (shrK B)|} : set_of_list evs;         \
   1.293 -\           Says A Spy {|NA, K|} ~: set_of_list evs;                     \
   1.294 +\           Says B Spy {|NA, NB, K|} ~: set_of_list evs;                 \
   1.295  \           A ~: lost;  B ~: lost;  evs : otway lost |]                  \
   1.296  \        ==> K ~: analz (sees lost C evs)";
   1.297  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
   1.298 @@ -684,9 +632,9 @@
   1.299      encrypted by a good agent C.  NEEDED?  INTERESTING?**)
   1.300  goal thy 
   1.301   "!!evs. evs : otway lost ==>                                           \
   1.302 -\      EX A B. ALL C N.                                            \
   1.303 -\         C ~: lost -->                                             \
   1.304 -\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) --> \
   1.305 +\      EX A B. ALL C N.                                                 \
   1.306 +\         C ~: lost -->                                                 \
   1.307 +\         Crypt {|N, Key K|} (shrK C) : parts (sees lost Spy evs) -->   \
   1.308  \         C=A | C=B";
   1.309  by (Simp_tac 1);        (*Miniscoping*)
   1.310  by (etac otway.induct 1);
   1.311 @@ -713,5 +661,3 @@
   1.312                                      delrules [disjCI, disjE]
   1.313                                      addss (!simpset))));
   1.314  qed "key_identifies_senders";
   1.315 -
   1.316 -
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Mon Oct 28 15:36:18 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Mon Oct 28 15:59:39 1996 +0100
     2.3 @@ -62,7 +62,7 @@
     2.4  
     2.5           (*Bob receives the Server's (?) message and compares the Nonces with
     2.6  	   those in the message he previously sent the Server.*)
     2.7 -    OR4  "[| evs: otway lost;  A ~= B;  B ~= Server;
     2.8 +    OR4  "[| evs: otway lost;  A ~= B;  
     2.9               Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.10                 : set_of_list evs;
    2.11               Says B Server {|Nonce NA, Agent A, Agent B, X', 
    2.12 @@ -71,14 +71,11 @@
    2.13                 : set_of_list evs |]
    2.14            ==> Says B A {|Nonce NA, X|} # evs : otway lost"
    2.15  
    2.16 -         (*This message models possible leaks of session keys.  Alice's Nonce
    2.17 -           identifies the protocol run.*)
    2.18 -    Revl "[| evs: otway lost;  A ~= Spy;
    2.19 -             Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|}
    2.20 -               : set_of_list evs;
    2.21 -             Says A  B {|Nonce NA, Agent A, Agent B, 
    2.22 -                         Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|}
    2.23 +         (*This message models possible leaks of session keys.  The nonces
    2.24 +           identify the protocol run.*)
    2.25 +    Oops "[| evs: otway lost;  B ~= Spy;
    2.26 +             Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|}
    2.27                 : set_of_list evs |]
    2.28 -          ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost"
    2.29 +          ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost"
    2.30  
    2.31  end