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