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