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