src/HOL/Auth/Public.ML
author paulson
Tue Nov 11 11:16:18 1997 +0100 (1997-11-11)
changeset 4198 c63639beeff1
parent 4091 771b1f6422a8
child 4422 21238c9d363e
permissions -rw-r--r--
Fixed spelling error
     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 (** Rewrites should not refer to  initState(Friend i) 
    38     -- not in normal form! **)
    39 
    40 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    41 by (induct_tac "C" 1);
    42 by (auto_tac (claset() addIs [range_eqI], simpset()));
    43 qed "keysFor_parts_initState";
    44 Addsimps [keysFor_parts_initState];
    45 
    46 
    47 (*** Function "spies" ***)
    48 
    49 (*Agents see their own private keys!*)
    50 goal thy "Key (priK A) : initState A";
    51 by (induct_tac "A" 1);
    52 by (Auto_tac());
    53 qed "priK_in_initState";
    54 AddIffs [priK_in_initState];
    55 
    56 (*All public keys are visible*)
    57 goal thy "Key (pubK A) : spies evs";
    58 by (induct_tac "evs" 1);
    59 by (ALLGOALS (asm_simp_tac
    60 	      (simpset() addsimps [imageI, spies_Cons]
    61 	                addsplits [expand_event_case, expand_if])));
    62 qed_spec_mp "spies_pubK";
    63 
    64 (*Spy sees private keys of bad agents!*)
    65 goal thy "!!A. A: bad ==> Key (priK A) : spies evs";
    66 by (induct_tac "evs" 1);
    67 by (ALLGOALS (asm_simp_tac
    68 	      (simpset() addsimps [imageI, spies_Cons]
    69 	                addsplits [expand_event_case, expand_if])));
    70 qed "Spy_spies_bad";
    71 
    72 AddIffs [spies_pubK, spies_pubK RS analz.Inj];
    73 AddSIs  [Spy_spies_bad];
    74 
    75 
    76 (*For not_bad_tac*)
    77 goal thy "!!A. [| Crypt (pubK A) X : analz (spies evs);  A: bad |] \
    78 \              ==> X : analz (spies evs)";
    79 by (blast_tac (claset() addSDs [analz.Decrypt]) 1);
    80 qed "Crypt_Spy_analz_bad";
    81 
    82 (*Prove that the agent is uncompromised by the confidentiality of 
    83   a component of a message she's said.*)
    84 fun not_bad_tac s =
    85     case_tac ("(" ^ s ^ ") : bad") THEN'
    86     SELECT_GOAL 
    87       (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
    88        REPEAT_DETERM (etac MPair_analz 1) THEN
    89        THEN_BEST_FIRST 
    90          (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
    91          (has_fewer_prems 1, size_of_thm)
    92          Safe_tac);
    93 
    94 
    95 (*** Fresh nonces ***)
    96 
    97 goal thy "Nonce N ~: parts (initState B)";
    98 by (induct_tac "B" 1);
    99 by (Auto_tac ());
   100 qed "Nonce_notin_initState";
   101 AddIffs [Nonce_notin_initState];
   102 
   103 goal thy "Nonce N ~: used []";
   104 by (simp_tac (simpset() addsimps [used_Nil]) 1);
   105 qed "Nonce_notin_used_empty";
   106 Addsimps [Nonce_notin_used_empty];
   107 
   108 
   109 (*** Supply fresh nonces for possibility theorems. ***)
   110 
   111 (*In any trace, there is an upper bound N on the greatest nonce in use.*)
   112 goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
   113 by (induct_tac "evs" 1);
   114 by (res_inst_tac [("x","0")] exI 1);
   115 by (ALLGOALS (asm_simp_tac
   116 	      (simpset() addsimps [used_Cons]
   117 			addsplits [expand_event_case, expand_if])));
   118 by Safe_tac;
   119 by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
   120 by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
   121 val lemma = result();
   122 
   123 goal thy "EX N. Nonce N ~: used evs";
   124 by (rtac (lemma RS exE) 1);
   125 by (Blast_tac 1);
   126 qed "Nonce_supply1";
   127 
   128 goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
   129 by (rtac (lemma RS exE) 1);
   130 by (rtac selectI 1);
   131 by (Fast_tac 1);
   132 qed "Nonce_supply";
   133 
   134 (*Tactic for possibility theorems*)
   135 fun possibility_tac st = st |>
   136     REPEAT (*omit used_Says so that Nonces start from different traces!*)
   137     (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
   138      THEN
   139      REPEAT_FIRST (eq_assume_tac ORELSE' 
   140                    resolve_tac [refl, conjI, Nonce_supply]));
   141 
   142 
   143 (*** Specialized rewriting for the analz_image_... theorems ***)
   144 
   145 goal thy "insert (Key K) H = Key `` {K} Un H";
   146 by (Blast_tac 1);
   147 qed "insert_Key_singleton";
   148 
   149 goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   150 by (Blast_tac 1);
   151 qed "insert_Key_image";
   152 
   153 (*Reverse the normal simplification of "image" to build up (not break down)
   154   the set of keys.  Based on analz_image_freshK_ss, but simpler.*)
   155 val analz_image_keys_ss = 
   156      simpset() addcongs [if_weak_cong]
   157 	      delsimps [image_insert, image_Un]
   158               delsimps [imp_disjL]    (*reduces blow-up*)
   159               addsimps [image_insert RS sym, image_Un RS sym,
   160 			rangeI, 
   161 			insert_Key_singleton, 
   162 			insert_Key_image, Un_assoc RS sym]
   163               addsplits [expand_if];
   164