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