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