src/HOL/Auth/Public.ML
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 6915 4ab8e31a8421
child 8054 2ce57ef2a4aa
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     1 (*  Title:      HOL/Auth/Public
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Theory of Public Keys (common to all symmetric-key protocols)
     7 
     8 Server keys; initial states of agents; new nonces and keys; function "sees" 
     9 *)
    10 
    11 (*** Basic properties of pubK & priK ***)
    12 
    13 AddIffs [inj_pubK RS inj_eq];
    14 
    15 Goal "(priK A = priK B) = (A=B)";
    16 by Safe_tac;
    17 by (dres_inst_tac [("f","invKey")] arg_cong 1);
    18 by (Full_simp_tac 1);
    19 qed "priK_inj_eq";
    20 
    21 AddIffs [priK_inj_eq];
    22 AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym];
    23 
    24 Goalw [isSymKey_def] "~ isSymKey (pubK A)";
    25 by (Simp_tac 1);
    26 qed "not_isSymKey_pubK";
    27 
    28 Goalw [isSymKey_def] "~ isSymKey (priK A)";
    29 by (Simp_tac 1);
    30 qed "not_isSymKey_priK";
    31 
    32 AddIffs [not_isSymKey_pubK, not_isSymKey_priK];
    33 
    34 
    35 (** "Image" equations that hold for injective functions **)
    36 
    37 Goal "(invKey x : invKey``A) = (x:A)";
    38 by Auto_tac;
    39 qed "invKey_image_eq";
    40 
    41 (*holds because invKey is injective*)
    42 Goal "(pubK x : pubK``A) = (x:A)";
    43 by Auto_tac;
    44 qed "pubK_image_eq";
    45 
    46 Goal "(priK x ~: pubK``A)";
    47 by Auto_tac;
    48 qed "priK_pubK_image_eq";
    49 Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
    50 
    51 
    52 (** Rewrites should not refer to  initState(Friend i) 
    53     -- not in normal form! **)
    54 
    55 Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
    56 by (induct_tac "C" 1);
    57 by (auto_tac (claset() addIs [range_eqI], simpset()));
    58 qed "keysFor_parts_initState";
    59 Addsimps [keysFor_parts_initState];
    60 
    61 
    62 (*** Function "spies" ***)
    63 
    64 (*Agents see their own private keys!*)
    65 Goal "Key (priK A) : initState A";
    66 by (induct_tac "A" 1);
    67 by Auto_tac;
    68 qed "priK_in_initState";
    69 AddIffs [priK_in_initState];
    70 
    71 (*All public keys are visible*)
    72 Goal "Key (pubK A) : spies evs";
    73 by (induct_tac "evs" 1);
    74 by (ALLGOALS (asm_simp_tac
    75 	      (simpset() addsimps [imageI, knows_Cons]
    76 	                addsplits [expand_event_case])));
    77 qed_spec_mp "spies_pubK";
    78 
    79 (*Spy sees private keys of bad agents!*)
    80 Goal "A: bad ==> Key (priK A) : spies evs";
    81 by (induct_tac "evs" 1);
    82 by (ALLGOALS (asm_simp_tac
    83 	      (simpset() addsimps [imageI, knows_Cons]
    84 	                addsplits [expand_event_case])));
    85 qed "Spy_spies_bad";
    86 
    87 AddIffs [spies_pubK, spies_pubK RS analz.Inj];
    88 AddSIs  [Spy_spies_bad];
    89 
    90 
    91 (*For not_bad_tac*)
    92 Goal "[| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
    93 \           ==> X : analz (spies evs)";
    94 by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
    95 qed "Crypt_Spy_analz_bad";
    96 
    97 (*Prove that the agent is uncompromised by the confidentiality of 
    98   a component of a message she's said.*)
    99 fun not_bad_tac s =
   100     case_tac ("(" ^ s ^ ") : bad") THEN'
   101     SELECT_GOAL 
   102       (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
   103        REPEAT_DETERM (etac MPair_analz 1) THEN
   104        THEN_BEST_FIRST 
   105          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
   106          (has_fewer_prems 1, size_of_thm)
   107          Safe_tac);
   108 
   109 
   110 (*** Fresh nonces ***)
   111 
   112 Goal "Nonce N ~: parts (initState B)";
   113 by (induct_tac "B" 1);
   114 by Auto_tac;
   115 qed "Nonce_notin_initState";
   116 AddIffs [Nonce_notin_initState];
   117 
   118 Goal "Nonce N ~: used []";
   119 by (simp_tac (simpset() addsimps [used_Nil]) 1);
   120 qed "Nonce_notin_used_empty";
   121 Addsimps [Nonce_notin_used_empty];
   122 
   123 
   124 (*** Supply fresh nonces for possibility theorems. ***)
   125 
   126 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   127 Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   128 by (induct_tac "evs" 1);
   129 by (res_inst_tac [("x","0")] exI 1);
   130 by (ALLGOALS (asm_simp_tac
   131 	      (simpset() addsimps [used_Cons]
   132 			addsplits [expand_event_case])));
   133 by Safe_tac;
   134 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   135 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
   136 val lemma = result();
   137 
   138 Goal "EX N. Nonce N ~: used evs";
   139 by (rtac (lemma RS exE) 1);
   140 by (Blast_tac 1);
   141 qed "Nonce_supply1";
   142 
   143 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
   144 by (rtac (lemma RS exE) 1);
   145 by (rtac selectI 1);
   146 by (Fast_tac 1);
   147 qed "Nonce_supply";
   148 
   149 (*Tactic for possibility theorems*)
   150 fun possibility_tac st = st |>
   151     REPEAT (*omit used_Says so that Nonces start from different traces!*)
   152     (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
   153      THEN
   154      REPEAT_FIRST (eq_assume_tac ORELSE' 
   155                    resolve_tac [refl, conjI, Nonce_supply]));
   156 
   157 
   158 (*** Specialized rewriting for the analz_image_... theorems ***)
   159 
   160 Goal "insert (Key K) H = Key `` {K} Un H";
   161 by (Blast_tac 1);
   162 qed "insert_Key_singleton";
   163 
   164 Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   165 by (Blast_tac 1);
   166 qed "insert_Key_image";
   167 
   168 (*Reverse the normal simplification of "image" to build up (not break down)
   169   the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
   170 val analz_image_keys_ss = 
   171      simpset() delsimps [image_insert, image_Un]
   172 	       delsimps [imp_disjL]    (*reduces blow-up*)
   173 	       addsimps [image_insert RS sym, image_Un RS sym,
   174 			 rangeI, 
   175 			 insert_Key_singleton, 
   176 			 insert_Key_image, Un_assoc RS sym];
   177