src/HOL/Auth/Shared.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5351 6d6467c2b8b9
permissions -rw-r--r--
even more tidying of Goal commands
paulson@2320
     1
(*  Title:      HOL/Auth/Shared
paulson@1934
     2
    ID:         $Id$
paulson@1934
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@1934
     4
    Copyright   1996  University of Cambridge
paulson@1934
     5
paulson@1934
     6
Theory of Shared Keys (common to all symmetric-key protocols)
paulson@1934
     7
paulson@3512
     8
Shared, long-term keys; initial states of agents
paulson@2032
     9
*)
paulson@2032
    10
paulson@3472
    11
(*** Basic properties of shrK ***)
paulson@1934
    12
paulson@3472
    13
(*Injectiveness: Agents' long-term keys are distinct.*)
paulson@3472
    14
AddIffs [inj_shrK RS inj_eq];
paulson@2376
    15
paulson@3472
    16
(* invKey(shrK A) = shrK A *)
paulson@3472
    17
Addsimps [rewrite_rule [isSymKey_def] isSym_keys];
paulson@2320
    18
paulson@1934
    19
(** Rewrites should not refer to  initState(Friend i) 
paulson@1934
    20
    -- not in normal form! **)
paulson@1934
    21
paulson@5076
    22
Goalw [keysFor_def] "keysFor (parts (initState C)) = {}";
paulson@3667
    23
by (induct_tac "C" 1);
paulson@4477
    24
by Auto_tac;
paulson@1934
    25
qed "keysFor_parts_initState";
paulson@1934
    26
Addsimps [keysFor_parts_initState];
paulson@1934
    27
paulson@4509
    28
(*Specialized to shared-key model: no need for addss in protocol proofs*)
paulson@5114
    29
Goal "[| K: keysFor (parts (insert X H));  X : synth (analz H) |] \
paulson@4509
    30
\              ==> K : keysFor (parts H) | Key K : parts H";
paulson@4509
    31
by (fast_tac
paulson@4509
    32
      (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono),
paulson@4509
    33
			impOfSubs (analz_subset_parts RS keysFor_mono)]
paulson@4509
    34
		addIs  [impOfSubs analz_subset_parts]
paulson@4509
    35
                addss  (simpset())) 1);
paulson@4509
    36
qed "keysFor_parts_insert";
paulson@4509
    37
paulson@5114
    38
Goal "Crypt K X : H ==> K : keysFor H";
paulson@4238
    39
by (dtac Crypt_imp_invKey_keysFor 1);
paulson@4238
    40
by (Asm_full_simp_tac 1);
paulson@4238
    41
qed "Crypt_imp_keysFor";
paulson@4238
    42
paulson@2032
    43
paulson@3683
    44
(*** Function "spies" ***)
paulson@1934
    45
paulson@3519
    46
(*Spy sees shared keys of agents!*)
paulson@5114
    47
Goal "A: bad ==> Key (shrK A) : spies evs";
paulson@3667
    48
by (induct_tac "evs" 1);
paulson@3683
    49
by (ALLGOALS (asm_simp_tac
wenzelm@4091
    50
	      (simpset() addsimps [imageI, spies_Cons]
nipkow@4686
    51
	                addsplits [expand_event_case])));
paulson@3683
    52
qed "Spy_spies_bad";
paulson@1934
    53
paulson@3683
    54
AddSIs [Spy_spies_bad];
paulson@2032
    55
paulson@3683
    56
(*For not_bad_tac*)
paulson@5114
    57
Goal "[| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
paulson@3683
    58
\              ==> X : analz (spies evs)";
wenzelm@4091
    59
by (fast_tac (claset() addSDs [analz.Decrypt] addss (simpset())) 1);
paulson@3683
    60
qed "Crypt_Spy_analz_bad";
paulson@2072
    61
paulson@3443
    62
(*Prove that the agent is uncompromised by the confidentiality of 
paulson@3443
    63
  a component of a message she's said.*)
paulson@3683
    64
fun not_bad_tac s =
paulson@3683
    65
    case_tac ("(" ^ s ^ ") : bad") THEN'
paulson@3443
    66
    SELECT_GOAL 
paulson@3683
    67
      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
paulson@3443
    68
       REPEAT_DETERM (etac MPair_analz 1) THEN
paulson@3443
    69
       THEN_BEST_FIRST 
paulson@3683
    70
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
paulson@3443
    71
         (has_fewer_prems 1, size_of_thm)
paulson@3443
    72
         (Step_tac 1));
paulson@1934
    73
paulson@2516
    74
paulson@2516
    75
(** Fresh keys never clash with long-term shared keys **)
paulson@2516
    76
paulson@3683
    77
(*Agents see their own shared keys!*)
paulson@5076
    78
Goal "Key (shrK A) : initState A";
paulson@3683
    79
by (induct_tac "A" 1);
paulson@4477
    80
by Auto_tac;
paulson@3683
    81
qed "shrK_in_initState";
paulson@3683
    82
AddIffs [shrK_in_initState];
paulson@3683
    83
paulson@5076
    84
Goal "Key (shrK A) : used evs";
wenzelm@4423
    85
by (rtac initState_into_used 1);
paulson@3121
    86
by (Blast_tac 1);
paulson@2516
    87
qed "shrK_in_used";
paulson@2516
    88
AddIffs [shrK_in_used];
paulson@2516
    89
paulson@3121
    90
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@2516
    91
  from long-term shared keys*)
paulson@5114
    92
Goal "Key K ~: used evs ==> K ~: range shrK";
paulson@3121
    93
by (Blast_tac 1);
paulson@2516
    94
qed "Key_not_used";
paulson@2516
    95
paulson@5114
    96
Goal "Key K ~: used evs ==> shrK B ~= K";
paulson@2891
    97
by (Blast_tac 1);
paulson@2516
    98
qed "shrK_neq";
paulson@2516
    99
paulson@2516
   100
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
paulson@3961
   101
paulson@2516
   102
paulson@3512
   103
(*** Fresh nonces ***)
paulson@2516
   104
paulson@5076
   105
Goal "Nonce N ~: parts (initState B)";
paulson@3667
   106
by (induct_tac "B" 1);
paulson@4477
   107
by Auto_tac;
paulson@3512
   108
qed "Nonce_notin_initState";
paulson@3512
   109
AddIffs [Nonce_notin_initState];
paulson@2516
   110
paulson@5076
   111
Goal "Nonce N ~: used []";
wenzelm@4091
   112
by (simp_tac (simpset() addsimps [used_Nil]) 1);
paulson@3512
   113
qed "Nonce_notin_used_empty";
paulson@3512
   114
Addsimps [Nonce_notin_used_empty];
paulson@2516
   115
paulson@2516
   116
paulson@2516
   117
(*** Supply fresh nonces for possibility theorems. ***)
paulson@2516
   118
paulson@3512
   119
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
paulson@5076
   120
Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs";
paulson@3667
   121
by (induct_tac "evs" 1);
paulson@2516
   122
by (res_inst_tac [("x","0")] exI 1);
paulson@3683
   123
by (ALLGOALS (asm_simp_tac
wenzelm@4091
   124
	      (simpset() addsimps [used_Cons]
nipkow@4686
   125
			addsplits [expand_event_case])));
paulson@3730
   126
by Safe_tac;
paulson@3512
   127
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
wenzelm@4091
   128
by (ALLGOALS (blast_tac (claset() addSEs [add_leE])));
paulson@2516
   129
val lemma = result();
paulson@2516
   130
paulson@5076
   131
Goal "EX N. Nonce N ~: used evs";
paulson@2516
   132
by (rtac (lemma RS exE) 1);
paulson@2891
   133
by (Blast_tac 1);
paulson@2516
   134
qed "Nonce_supply1";
paulson@2516
   135
paulson@5076
   136
Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
paulson@2516
   137
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   138
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@3708
   139
by (Clarify_tac 1);
paulson@2516
   140
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   141
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
wenzelm@4091
   142
by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   143
				     le_add2, le_add1, 
paulson@2516
   144
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   145
qed "Nonce_supply2";
paulson@2516
   146
paulson@5076
   147
Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
paulson@2516
   148
\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
paulson@2516
   149
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   150
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   151
by (cut_inst_tac [("evs","evs''")] lemma 1);
paulson@3708
   152
by (Clarify_tac 1);
paulson@2516
   153
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   154
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   155
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
wenzelm@4091
   156
by (asm_simp_tac (simpset() addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   157
				     le_add2, le_add1, 
paulson@2516
   158
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   159
qed "Nonce_supply3";
paulson@2516
   160
paulson@5076
   161
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
paulson@2516
   162
by (rtac (lemma RS exE) 1);
paulson@2516
   163
by (rtac selectI 1);
paulson@2891
   164
by (Blast_tac 1);
paulson@2516
   165
qed "Nonce_supply";
paulson@2516
   166
paulson@2516
   167
(*** Supply fresh keys for possibility theorems. ***)
paulson@2516
   168
paulson@5076
   169
Goal "EX K. Key K ~: used evs";
nipkow@3414
   170
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
paulson@2891
   171
by (Blast_tac 1);
paulson@2516
   172
qed "Key_supply1";
paulson@2516
   173
paulson@5076
   174
Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'";
nipkow@3414
   175
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
paulson@2516
   176
by (etac exE 1);
paulson@2516
   177
by (cut_inst_tac [("evs","evs'")] 
nipkow@3414
   178
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
oheimb@4633
   179
by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *)
paulson@2516
   180
qed "Key_supply2";
paulson@2516
   181
paulson@5076
   182
Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
paulson@2516
   183
\                      Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''";
nipkow@3414
   184
by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1);
paulson@2516
   185
by (etac exE 1);
paulson@4156
   186
(*Blast_tac requires instantiation of the keys for some reason*)
paulson@4156
   187
by (cut_inst_tac [("evs","evs'"), ("a1","K")] 
nipkow@3414
   188
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   189
by (etac exE 1);
paulson@4156
   190
by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] 
nipkow@3414
   191
    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
paulson@4156
   192
by (Blast_tac 1);
paulson@2516
   193
qed "Key_supply3";
paulson@2516
   194
paulson@5076
   195
Goal "Key (@ K. Key K ~: used evs) ~: used evs";
nipkow@3414
   196
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
paulson@2516
   197
by (rtac selectI 1);
paulson@2891
   198
by (Blast_tac 1);
paulson@2516
   199
qed "Key_supply";
paulson@2516
   200
paulson@2516
   201
(*** Tactics for possibility theorems ***)
paulson@2516
   202
paulson@3673
   203
(*Omitting used_Says makes the tactic much faster: it leaves expressions
paulson@3673
   204
    such as  Nonce ?N ~: used evs that match Nonce_supply*)
paulson@3542
   205
fun possibility_tac st = st |>
paulson@3673
   206
   (REPEAT 
wenzelm@4091
   207
    (ALLGOALS (simp_tac (simpset() delsimps [used_Says] setSolver safe_solver))
paulson@2516
   208
     THEN
paulson@2516
   209
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@3542
   210
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
paulson@2516
   211
paulson@2516
   212
(*For harder protocols (such as Recur) where we have to set up some
paulson@2516
   213
  nonces and keys initially*)
paulson@3542
   214
fun basic_possibility_tac st = st |>
paulson@2516
   215
    REPEAT 
wenzelm@4091
   216
    (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
paulson@2516
   217
     THEN
paulson@2516
   218
     REPEAT_FIRST (resolve_tac [refl, conjI]));
paulson@2516
   219
paulson@2516
   220
paulson@3472
   221
(*** Specialized rewriting for analz_insert_freshK ***)
paulson@2320
   222
paulson@5114
   223
Goal "A <= Compl (range shrK) ==> shrK x ~: A";
paulson@2891
   224
by (Blast_tac 1);
paulson@2516
   225
qed "subset_Compl_range";
paulson@2045
   226
paulson@5076
   227
Goal "insert (Key K) H = Key `` {K} Un H";
paulson@2891
   228
by (Blast_tac 1);
paulson@2516
   229
qed "insert_Key_singleton";
paulson@2516
   230
paulson@5076
   231
Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
paulson@2891
   232
by (Blast_tac 1);
paulson@2891
   233
qed "insert_Key_image";
paulson@2516
   234
paulson@3451
   235
(*Reverse the normal simplification of "image" to build up (not break down)
paulson@3451
   236
  the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@3451
   237
  erase occurrences of forwarded message components (X).*)
paulson@2516
   238
val analz_image_freshK_ss = 
wenzelm@4091
   239
     simpset() addcongs [if_weak_cong]
paulson@3673
   240
	      delsimps [image_insert, image_Un]
paulson@3680
   241
              delsimps [imp_disjL]    (*reduces blow-up*)
paulson@3479
   242
              addsimps ([image_insert RS sym, image_Un RS sym,
paulson@3479
   243
                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
paulson@2516
   244
                         insert_Key_singleton, subset_Compl_range,
paulson@3479
   245
                         Key_not_used, insert_Key_image, Un_assoc RS sym]
nipkow@4686
   246
                        @disj_comms);
paulson@2045
   247
paulson@2045
   248
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@5278
   249
Goal "(Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
paulson@2045
   250
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
wenzelm@4091
   251
by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
paulson@2516
   252
qed "analz_image_freshK_lemma";