src/HOL/Auth/Shared.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6915 4ab8e31a8421
child 9970 dfe4747c8318
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/Shared
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of Shared Keys (common to all symmetric-key protocols)
     7 
     8 Shared, long-term keys; initial states of agents
     9 *)
    10 
    11 (*** Basic properties of shrK ***)
    12 
    13 (*Injectiveness: Agents' long-term keys are distinct.*)
    14 AddIffs [inj_shrK RS inj_eq];
    15 
    16 (* invKey(shrK A) = shrK A *)
    17 Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
    18 
    19 (** Rewrites should not refer to  initState(Friend i) 
    20     -- not in normal form! **)
    21 
    22 Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
    23 by (induct_tac "C" 1);
    24 by Auto_tac;
    25 qed "keysFor_parts_initState";
    26 Addsimps [keysFor_parts_initState];
    27 
    28 (*Specialized to shared-key model: no need for addss in protocol proofs*)
    29 Goal "[| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
    30 \              ==> K : keysFor (parts H) | Key K : parts H";
    31 by (force_tac
    32       (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
    33 			impOfSubs (analz_subset_parts RS keysFor_mono)]
    34 		addIs  [impOfSubs analz_subset_parts],
    35        simpset()) 1);
    36 qed "keysFor_parts_insert";
    37 
    38 Goal "Crypt K X : H ==> K : keysFor H";
    39 by (dtac Crypt_imp_invKey_keysFor 1);
    40 by (Asm_full_simp_tac 1);
    41 qed "Crypt_imp_keysFor";
    42 
    43 
    44 (*** Function "knows" ***)
    45 
    46 (*Spy sees shared keys of agents!*)
    47 Goal "A: bad ==> Key (shrK A) : knows Spy evs";
    48 by (induct_tac "evs" 1);
    49 by (ALLGOALS (asm_simp_tac
    50 	      (simpset() addsimps [imageI, knows_Cons]
    51 	                addsplits [expand_event_case])));
    52 qed "Spy_knows_Spy_bad";
    53 AddSIs [Spy_knows_Spy_bad];
    54 
    55 (*For not_bad_tac*)
    56 Goal "[| Crypt (shrK A) X : analz (knows Spy evs);  A: bad |] \
    57 \              ==> X : analz (knows Spy evs)";
    58 by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1);
    59 qed "Crypt_Spy_analz_bad";
    60 
    61 (*Prove that the agent is uncompromised by the confidentiality of 
    62   a component of a message she's said.*)
    63 fun not_bad_tac s =
    64     case_tac ("(" ^ s ^ ") : bad") THEN'
    65     SELECT_GOAL 
    66       (REPEAT_DETERM (etac exE 1) THEN
    67        REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    68        REPEAT_DETERM (etac MPair_analz 1) THEN
    69        THEN_BEST_FIRST 
    70          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    71          (has_fewer_prems 1, size_of_thm)
    72          (Step_tac 1));
    73 
    74 
    75 (** Fresh keys never clash with long-term shared keys **)
    76 
    77 (*Agents see their own shared keys!*)
    78 Goal "Key (shrK A) : initState A";
    79 by (induct_tac "A" 1);
    80 by Auto_tac;
    81 qed "shrK_in_initState";
    82 AddIffs [shrK_in_initState];
    83 
    84 Goal "Key (shrK A) : used evs";
    85 by (rtac initState_into_used 1);
    86 by (Blast_tac 1);
    87 qed "shrK_in_used";
    88 AddIffs [shrK_in_used];
    89 
    90 (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
    91   from long-term shared keys*)
    92 Goal "Key K ~: used evs ==> K ~: range shrK";
    93 by (Blast_tac 1);
    94 qed "Key_not_used";
    95 
    96 Goal "Key K ~: used evs ==> shrK B ~= K";
    97 by (Blast_tac 1);
    98 qed "shrK_neq";
    99 
   100 Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
   101 
   102 
   103 (*** Fresh nonces ***)
   104 
   105 Goal "Nonce N ~: parts (initState B)";
   106 by (induct_tac "B" 1);
   107 by Auto_tac;
   108 qed "Nonce_notin_initState";
   109 AddIffs [Nonce_notin_initState];
   110 
   111 Goal "Nonce N ~: used []";
   112 by (simp_tac (simpset() addsimps [used_Nil]) 1);
   113 qed "Nonce_notin_used_empty";
   114 Addsimps [Nonce_notin_used_empty];
   115 
   116 
   117 (*** Supply fresh nonces for possibility theorems. ***)
   118 
   119 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   120 Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   121 by (induct_tac "evs" 1);
   122 by (res_inst_tac [("x","0")] exI 1);
   123 by (ALLGOALS (asm_simp_tac
   124 	      (simpset() addsimps [used_Cons]
   125 			addsplits [expand_event_case])));
   126 by Safe_tac;
   127 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   128 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
   129 val lemma = result();
   130 
   131 Goal "EX N. Nonce N ~: used evs";
   132 by (rtac (lemma RS exE) 1);
   133 by (Blast_tac 1);
   134 qed "Nonce_supply1";
   135 
   136 Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
   137 by (cut_inst_tac [("evs","evs")] lemma 1);
   138 by (cut_inst_tac [("evs","evs'")] lemma 1);
   139 by (Clarify_tac 1);
   140 by (res_inst_tac [("x","N")] exI 1);
   141 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
   142 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
   143 				      less_Suc_eq_le]) 1);
   144 qed "Nonce_supply2";
   145 
   146 Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
   147 \                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
   148 by (cut_inst_tac [("evs","evs")] lemma 1);
   149 by (cut_inst_tac [("evs","evs'")] lemma 1);
   150 by (cut_inst_tac [("evs","evs''")] lemma 1);
   151 by (Clarify_tac 1);
   152 by (res_inst_tac [("x","N")] exI 1);
   153 by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
   154 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
   155 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2,
   156 				      less_Suc_eq_le]) 1);
   157 qed "Nonce_supply3";
   158 
   159 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
   160 by (rtac (lemma RS exE) 1);
   161 by (rtac selectI 1);
   162 by (Blast_tac 1);
   163 qed "Nonce_supply";
   164 
   165 (*** Supply fresh keys for possibility theorems. ***)
   166 
   167 Goal "EX K. Key K ~: used evs";
   168 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
   169 by (Blast_tac 1);
   170 qed "Key_supply1";
   171 
   172 Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
   173 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
   174 by (etac exE 1);
   175 by (cut_inst_tac [("evs","evs'")] 
   176     (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
   177 by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
   178 qed "Key_supply2";
   179 
   180 Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
   181 \                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
   182 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
   183 by (etac exE 1);
   184 (*Blast_tac requires instantiation of the keys for some reason*)
   185 by (cut_inst_tac [("evs","evs'"), ("a1","K")] 
   186     (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
   187 by (etac exE 1);
   188 by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
   189     (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
   190 by (Blast_tac 1);
   191 qed "Key_supply3";
   192 
   193 Goal "Key (@ K. Key K ~: used evs) ~: used evs";
   194 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
   195 by (rtac selectI 1);
   196 by (Blast_tac 1);
   197 qed "Key_supply";
   198 
   199 (*** Tactics for possibility theorems ***)
   200 
   201 (*Omitting used_Says makes the tactic much faster: it leaves expressions
   202     such as  Nonce ?N ~: used evs that match Nonce_supply*)
   203 fun possibility_tac st = st |>
   204    (REPEAT 
   205     (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] 
   206                          setSolver safe_solver))
   207      THEN
   208      REPEAT_FIRST (eq_assume_tac ORELSE' 
   209                    resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
   210 
   211 (*For harder protocols (such as Recur) where we have to set up some
   212   nonces and keys initially*)
   213 fun basic_possibility_tac st = st |>
   214     REPEAT 
   215     (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
   216      THEN
   217      REPEAT_FIRST (resolve_tac [refl, conjI]));
   218 
   219 
   220 (*** Specialized rewriting for analz_insert_freshK ***)
   221 
   222 Goal "A <= - (range shrK) ==> shrK x ~: A";
   223 by (Blast_tac 1);
   224 qed "subset_Compl_range";
   225 
   226 Goal "insert (Key K) H = Key `` {K} Un H";
   227 by (Blast_tac 1);
   228 qed "insert_Key_singleton";
   229 
   230 Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   231 by (Blast_tac 1);
   232 qed "insert_Key_image";
   233 
   234 (*Reverse the normal simplification of "image" to build up (not break down)
   235   the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
   236   erase occurrences of forwarded message components (X).*)
   237 val analz_image_freshK_ss = 
   238      simpset() delsimps [image_insert, image_Un]
   239 	       delsimps [imp_disjL]    (*reduces blow-up*)
   240 	       addsimps [image_insert RS sym, image_Un RS sym,
   241 			 analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
   242 			 insert_Key_singleton, subset_Compl_range,
   243 			 Key_not_used, insert_Key_image, Un_assoc RS sym]
   244 			@disj_comms;
   245 
   246 (*Lemma for the trivial direction of the if-and-only-if*)
   247 Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
   248 \        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
   249 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   250 qed "analz_image_freshK_lemma";