Stronger proofs; work for Otway-Rees
authorpaulson
Mon Sep 09 17:34:24 1996 +0200 (1996-09-09)
changeset 1964d551e68b7a36
parent 1963 a4abf41134e2
child 1965 789c12ea0b30
Stronger proofs; work for Otway-Rees
src/HOL/Auth/Message.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/Shared.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Mon Sep 09 17:33:23 1996 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Mon Sep 09 17:34:24 1996 +0200
     1.3 @@ -60,6 +60,7 @@
     1.4  goalw thy [keysFor_def]
     1.5      "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)";
     1.6  by (Auto_tac());
     1.7 +by (Fast_tac 1);
     1.8  qed "keysFor_insert_Crypt";
     1.9  
    1.10  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
     2.1 --- a/src/HOL/Auth/OtwayRees.ML	Mon Sep 09 17:33:23 1996 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees.ML	Mon Sep 09 17:34:24 1996 +0200
     2.3 @@ -62,7 +62,10 @@
     2.4  qed "OR5_parts_sees_Enemy";
     2.5  
     2.6  (*OR2_analz... and OR4_analz... let us treat those cases using the same 
     2.7 -  argument as for the Fake case.*)
     2.8 +  argument as for the Fake case.  This is possible for most, but not all,
     2.9 +  proofs: Fake does not invent new nonces (as in OR2), and of course Fake
    2.10 +  messages originate from the Enemy. *)
    2.11 +
    2.12  val OR2_OR4_tac = 
    2.13      dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN
    2.14      dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6;
    2.15 @@ -70,9 +73,9 @@
    2.16  
    2.17  (*** Shared keys are not betrayed ***)
    2.18  
    2.19 -(*Enemy never sees another agent's shared key!*)
    2.20 +(*Enemy never sees another agent's shared key! (unless it is leaked at start)*)
    2.21  goal thy 
    2.22 - "!!evs. [| evs : otway; A ~= Enemy |] ==> \
    2.23 + "!!evs. [| evs : otway; A ~= Enemy; A ~: Friend``leaked |] ==> \
    2.24  \        Key (shrK A) ~: parts (sees Enemy evs)";
    2.25  be otway.induct 1;
    2.26  by OR2_OR4_tac;
    2.27 @@ -90,16 +93,20 @@
    2.28  	  Enemy_not_analz_shrK, 
    2.29  	  not_sym RSN (2, Enemy_not_analz_shrK)];
    2.30  
    2.31 -(*We go to some trouble to preserve R in the 3rd subgoal*)
    2.32 +(*We go to some trouble to preserve R in the 3rd and 4th subgoals
    2.33 +  As usual fast_tac cannot be used because it uses the equalities too soon*)
    2.34  val major::prems = 
    2.35 -goal thy  "[| Key (shrK A) : parts (sees Enemy evs);    \
    2.36 -\             evs : otway;                                  \
    2.37 -\             A=Enemy ==> R                                  \
    2.38 +goal thy  "[| Key (shrK A) : parts (sees Enemy evs);       \
    2.39 +\             evs : otway;                                 \
    2.40 +\             A=Enemy ==> R;                               \
    2.41 +\             !!i. [| A = Friend i; i: leaked |] ==> R     \
    2.42  \           |] ==> R";
    2.43  br ccontr 1;
    2.44  br ([major, Enemy_not_see_shrK] MRS rev_notE) 1;
    2.45 +br notI 3;
    2.46 +be imageE 3;
    2.47  by (swap_res_tac prems 2);
    2.48 -by (ALLGOALS (fast_tac (!claset addIs prems)));
    2.49 +by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems)));
    2.50  qed "Enemy_see_shrK_E";
    2.51  
    2.52  bind_thm ("Enemy_analz_shrK_E", 
    2.53 @@ -109,28 +116,6 @@
    2.54  AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E];
    2.55  
    2.56  
    2.57 -(*No Friend will ever see another agent's shared key 
    2.58 -  (excluding the Enemy, who might transmit his).
    2.59 -  The Server, of course, knows all shared keys.*)
    2.60 -goal thy 
    2.61 - "!!evs. [| evs : otway; A ~= Enemy;  A ~= Friend j |] ==> \
    2.62 -\        Key (shrK A) ~: parts (sees (Friend j) evs)";
    2.63 -br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1;
    2.64 -by (ALLGOALS Asm_simp_tac);
    2.65 -qed "Friend_not_see_shrK";
    2.66 -
    2.67 -
    2.68 -(*Not for Addsimps -- it can cause goals to blow up!*)
    2.69 -goal thy  
    2.70 - "!!evs. evs : otway ==>                                  \
    2.71 -\        (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) =  \
    2.72 -\        (A=B | A=Enemy)";
    2.73 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts]
    2.74 -		      addIs [impOfSubs (subset_insertI RS analz_mono)]
    2.75 -	              addss (!simpset)) 1);
    2.76 -qed "shrK_mem_analz";
    2.77 -
    2.78 -
    2.79  (*** Future keys can't be seen or used! ***)
    2.80  
    2.81  (*Nobody can have SEEN keys that will be generated in the future.
    2.82 @@ -220,9 +205,8 @@
    2.83  (****
    2.84   The following is to prove theorems of the form
    2.85  
    2.86 -          Key K : analz (insert (Key (newK evt)) 
    2.87 -	                   (insert (Key (shrK C)) (sees Enemy evs))) ==>
    2.88 -          Key K : analz (insert (Key (shrK C)) (sees Enemy evs))
    2.89 +          Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==>
    2.90 +          Key K : analz (sees Enemy evs)
    2.91  
    2.92   A more general formula must be proved inductively.
    2.93  
    2.94 @@ -243,9 +227,9 @@
    2.95  by (best_tac (!claset addSEs partsEs
    2.96  		      addDs [impOfSubs analz_subset_parts,
    2.97                               impOfSubs parts_insert_subset_Un]
    2.98 -                      addss (!simpset)) 1);
    2.99 -(*OR5*)
   2.100 -by (fast_tac (!claset addss (!simpset)) 1);
   2.101 +                      addss (!simpset)) 2);
   2.102 +(*Base case and OR5*)
   2.103 +by (Auto_tac());
   2.104  result();
   2.105  
   2.106  
   2.107 @@ -254,6 +238,9 @@
   2.108  Delsimps [image_insert];
   2.109  Addsimps [image_insert RS sym];
   2.110  
   2.111 +Delsimps [image_Un];
   2.112 +Addsimps [image_Un RS sym];
   2.113 +
   2.114  goal thy "insert (Key (newK x)) (sees A evs) = \
   2.115  \         Key `` (newK``{x}) Un (sees A evs)";
   2.116  by (Fast_tac 1);
   2.117 @@ -294,25 +281,22 @@
   2.118  
   2.119  (*Lemma for the trivial direction of the if-and-only-if*)
   2.120  goal thy  
   2.121 - "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \
   2.122 -\          (K : nE | Key K : analz (insert KsC sEe))  ==>     \
   2.123 -\        (Key K : analz (insert KsC (Key``nE Un sEe))) = \
   2.124 -\          (K : nE | Key K : analz (insert KsC sEe))";
   2.125 + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \
   2.126 +\         (K : nE | Key K : analz sEe)  ==>     \
   2.127 +\        (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)";
   2.128  by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1);
   2.129  val lemma = result();
   2.130  
   2.131 +
   2.132  goal thy  
   2.133   "!!evs. evs : otway ==> \
   2.134 -\  ALL K E. (Key K : analz (insert (Key (shrK C)) \
   2.135 -\                             (Key``(newK``E) Un (sees Enemy evs)))) = \
   2.136 -\           (K : newK``E |  \
   2.137 -\            Key K : analz (insert (Key (shrK C)) \
   2.138 -\                             (sees Enemy evs)))";
   2.139 +\  ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \
   2.140 +\           (K : newK``E | Key K : analz (sees Enemy evs))";
   2.141  be otway.induct 1;
   2.142  bd OR2_analz_sees_Enemy 4;
   2.143  bd OR4_analz_sees_Enemy 6;
   2.144  by (REPEAT_FIRST (resolve_tac [allI, lemma]));
   2.145 -by (ALLGOALS (*Takes 40 secs*)
   2.146 +by (ALLGOALS (*Takes 35 secs*)
   2.147      (asm_simp_tac 
   2.148       (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK]
   2.149  			 @ pushes)
   2.150 @@ -321,14 +305,14 @@
   2.151  by (enemy_analz_tac 5);
   2.152  (*OR3*)
   2.153  by (Fast_tac 4);
   2.154 -(*OR2*) (** LEVEL 11 **)
   2.155 +(*OR2*) (** LEVEL 7 **)
   2.156  by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] 
   2.157      (insert_commute RS ssubst) 3);
   2.158  by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")]
   2.159      (insert_commute RS ssubst) 3);
   2.160  by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3);
   2.161  by (enemy_analz_tac 3);
   2.162 -(*Fake case*) (** LEVEL 6 **)
   2.163 +(*Fake case*) (** LEVEL 11 **)
   2.164  by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] 
   2.165      (insert_commute RS ssubst) 2);
   2.166  by (enemy_analz_tac 2);
   2.167 @@ -339,12 +323,8 @@
   2.168  
   2.169  goal thy
   2.170   "!!evs. evs : otway ==>                               \
   2.171 -\        Key K : analz (insert (Key (newK evt))            \
   2.172 -\                         (insert (Key (shrK C))      \
   2.173 -\                          (sees Enemy evs))) =            \
   2.174 -\             (K = newK evt |                              \
   2.175 -\              Key K : analz (insert (Key (shrK C))   \
   2.176 -\                               (sees Enemy evs)))";
   2.177 +\        Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \
   2.178 +\        (K = newK evt | Key K : analz (sees Enemy evs))";
   2.179  by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, 
   2.180  				   insert_Key_singleton]) 1);
   2.181  by (Fast_tac 1);
   2.182 @@ -371,9 +351,8 @@
   2.183   "!!evs. [| Says Server (Friend j) \
   2.184  \            {|Ni, Crypt {|Ni, K|} (shrK (Friend i)),                      \
   2.185  \                  Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs;  \
   2.186 -\           evs : otway;  Friend i ~= C;  Friend j ~= C              \
   2.187 -\        |] ==>                                                       \
   2.188 -\     K ~: analz (insert (Key (shrK C)) (sees Enemy evs))";
   2.189 +\           i ~: leaked;  j ~: leaked;  evs : otway |] ==>                 \
   2.190 +\     K ~: analz (sees Enemy evs)";
   2.191  be rev_mp 1;
   2.192  be otway.induct 1;
   2.193  bd OR2_analz_sees_Enemy 4;
   2.194 @@ -383,14 +362,14 @@
   2.195  by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   2.196  by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac));
   2.197  by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac));
   2.198 -by (ALLGOALS 
   2.199 +by (ALLGOALS
   2.200      (asm_full_simp_tac 
   2.201       (!simpset addsimps ([analz_subset_parts RS contra_subsetD,
   2.202  			  analz_insert_Key_newK] @ pushes)
   2.203                 setloop split_tac [expand_if])));
   2.204  (*OR3*)
   2.205  by (fast_tac (!claset addSEs [less_irrefl]) 3);
   2.206 -(*Fake*) (** LEVEL 8 **)
   2.207 +(*Fake*) (** LEVEL 10 **)
   2.208  by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1);
   2.209  by (enemy_analz_tac 1);
   2.210  (*OR4*)
   2.211 @@ -411,9 +390,9 @@
   2.212  (** First, two lemmas for the Fake, OR2 and OR4 cases **)
   2.213  
   2.214  goal thy 
   2.215 - "!!evs. [| X : synth (analz (sees Enemy evs));       \
   2.216 -\           Crypt X' (shrK C) : parts{X};             \
   2.217 -\           C ~= Enemy;   evs : otway |]              \
   2.218 + "!!evs. [| X : synth (analz (sees Enemy evs));                \
   2.219 +\           Crypt X' (shrK C) : parts{X};                      \
   2.220 +\           C ~= Enemy;  C ~: Friend``leaked;  evs : otway |]  \
   2.221  \        ==> Crypt X' (shrK C) : parts (sees Enemy evs)";
   2.222  by (best_tac (!claset addSEs [impOfSubs analz_subset_parts]
   2.223  	              addDs [impOfSubs parts_insert_subset_Un]
   2.224 @@ -433,9 +412,9 @@
   2.225  (*The Key K uniquely identifies a pair of senders in the message encrypted by
   2.226    C, but if C=Enemy then he could send all sorts of nonsense.*)
   2.227  goal thy 
   2.228 - "!!evs. evs : otway ==>                        \
   2.229 -\      EX A B. ALL C.                    \
   2.230 -\         C ~= Enemy -->                        \
   2.231 + "!!evs. evs : otway ==>                                     \
   2.232 +\      EX A B. ALL C.                                        \
   2.233 +\         C ~= Enemy & C ~: Friend``leaked -->               \
   2.234  \         (ALL S S' X. Says S S' X : set_of_list evs -->     \
   2.235  \           (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)";
   2.236  by (Simp_tac 1);
     3.1 --- a/src/HOL/Auth/Shared.ML	Mon Sep 09 17:33:23 1996 +0200
     3.2 +++ b/src/HOL/Auth/Shared.ML	Mon Sep 09 17:34:24 1996 +0200
     3.3 @@ -20,6 +20,12 @@
     3.4  
     3.5  open Shared;
     3.6  
     3.7 +(*Holds because Friend is injective: thus cannot prove for all f*)
     3.8 +goal thy "(Friend x : Friend``A) = (x:A)";
     3.9 +by (Auto_tac());
    3.10 +qed "Friend_image_eq";
    3.11 +Addsimps [Friend_image_eq];
    3.12 +
    3.13  Addsimps [Un_insert_left, Un_insert_right];
    3.14  
    3.15  (*By default only o_apply is built-in.  But in the presence of eta-expansion
    3.16 @@ -96,19 +102,20 @@
    3.17  Addsimps [shrK_notin_image_newK];
    3.18  
    3.19  
    3.20 -(*Agents see their own shrKs!*)
    3.21 -goal thy "Key (shrK A) : analz (sees A evs)";
    3.22 +(*Agents see their own shared keys!*)
    3.23 +goal thy "Key (shrK A) : sees A evs";
    3.24  by (list.induct_tac "evs" 1);
    3.25 -by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
    3.26  by (agent.induct_tac "A" 1);
    3.27 -by (auto_tac (!claset addIs [range_eqI], !simpset));
    3.28 -qed "analz_own_shrK";
    3.29 +by (Auto_tac ());
    3.30 +qed "sees_own_shrK";
    3.31  
    3.32 -bind_thm ("parts_own_shrK",
    3.33 -	  [analz_subset_parts, analz_own_shrK] MRS subsetD);
    3.34 +(*Enemy sees leaked shrKs!*)
    3.35 +goal thy "!!i. i: leaked ==> Key (shrK (Friend i)) : sees Enemy evs";
    3.36 +by (list.induct_tac "evs" 1);
    3.37 +by (Auto_tac ());
    3.38 +qed "Enemy_sees_leaked";
    3.39  
    3.40 -Addsimps [analz_own_shrK, parts_own_shrK];
    3.41 -
    3.42 +AddSIs [sees_own_shrK, Enemy_sees_leaked];
    3.43  
    3.44  
    3.45  (** Specialized rewrite rules for (sees A (Says...#evs)) **)