src/HOL/Auth/Shared.ML
author paulson
Fri Sep 19 18:27:31 1997 +0200 (1997-09-19)
changeset 3686 4b484805b4c4
parent 3683 aafe719dff14
child 3708 56facaebf3e3
permissions -rw-r--r--
First working version with Oops event for session keys
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@3121
    27
by (Auto_tac ());
paulson@1934
    28
qed "keysFor_parts_initState";
paulson@1934
    29
Addsimps [keysFor_parts_initState];
paulson@1934
    30
paulson@2032
    31
paulson@3683
    32
(*** Function "spies" ***)
paulson@1934
    33
paulson@3519
    34
(*Spy sees shared keys of agents!*)
paulson@3683
    35
goal thy "!!A. A: bad ==> Key (shrK A) : spies evs";
paulson@3667
    36
by (induct_tac "evs" 1);
paulson@3683
    37
by (ALLGOALS (asm_simp_tac
paulson@3683
    38
	      (!simpset addsimps [imageI, spies_Cons]
paulson@3683
    39
	                setloop split_tac [expand_event_case, expand_if])));
paulson@3683
    40
qed "Spy_spies_bad";
paulson@1934
    41
paulson@3683
    42
AddSIs [Spy_spies_bad];
paulson@2032
    43
paulson@3683
    44
(*For not_bad_tac*)
paulson@3683
    45
goal thy "!!A. [| Crypt (shrK A) X : analz (spies evs);  A: bad |] \
paulson@3683
    46
\              ==> X : analz (spies evs)";
paulson@3443
    47
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
paulson@3683
    48
qed "Crypt_Spy_analz_bad";
paulson@2072
    49
paulson@3443
    50
(*Prove that the agent is uncompromised by the confidentiality of 
paulson@3443
    51
  a component of a message she's said.*)
paulson@3683
    52
fun not_bad_tac s =
paulson@3683
    53
    case_tac ("(" ^ s ^ ") : bad") THEN'
paulson@3443
    54
    SELECT_GOAL 
paulson@3683
    55
      (REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN
paulson@3443
    56
       REPEAT_DETERM (etac MPair_analz 1) THEN
paulson@3443
    57
       THEN_BEST_FIRST 
paulson@3683
    58
         (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1)
paulson@3443
    59
         (has_fewer_prems 1, size_of_thm)
paulson@3443
    60
         (Step_tac 1));
paulson@1934
    61
paulson@2516
    62
paulson@2516
    63
(** Fresh keys never clash with long-term shared keys **)
paulson@2516
    64
paulson@3683
    65
(*Agents see their own shared keys!*)
paulson@3683
    66
goal thy "Key (shrK A) : initState A";
paulson@3683
    67
by (induct_tac "A" 1);
paulson@3683
    68
by (Auto_tac());
paulson@3683
    69
qed "shrK_in_initState";
paulson@3683
    70
AddIffs [shrK_in_initState];
paulson@3683
    71
paulson@2516
    72
goal thy "Key (shrK A) : used evs";
paulson@3683
    73
br initState_into_used 1;
paulson@3121
    74
by (Blast_tac 1);
paulson@2516
    75
qed "shrK_in_used";
paulson@2516
    76
AddIffs [shrK_in_used];
paulson@2516
    77
paulson@3121
    78
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys
paulson@2516
    79
  from long-term shared keys*)
paulson@2516
    80
goal thy "!!K. Key K ~: used evs ==> K ~: range shrK";
paulson@3121
    81
by (Blast_tac 1);
paulson@2516
    82
qed "Key_not_used";
paulson@2516
    83
paulson@2516
    84
(*A session key cannot clash with a long-term shared key*)
paulson@2516
    85
goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
paulson@2891
    86
by (Blast_tac 1);
paulson@2516
    87
qed "shrK_neq";
paulson@2516
    88
paulson@2516
    89
Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
paulson@2516
    90
paulson@2516
    91
paulson@3512
    92
(*** Fresh nonces ***)
paulson@2516
    93
paulson@3519
    94
goal thy "Nonce N ~: parts (initState B)";
paulson@3667
    95
by (induct_tac "B" 1);
paulson@3512
    96
by (Auto_tac ());
paulson@3512
    97
qed "Nonce_notin_initState";
paulson@3512
    98
AddIffs [Nonce_notin_initState];
paulson@2516
    99
paulson@3512
   100
goal thy "Nonce N ~: used []";
paulson@3683
   101
by (simp_tac (!simpset addsimps [used_Nil]) 1);
paulson@3512
   102
qed "Nonce_notin_used_empty";
paulson@3512
   103
Addsimps [Nonce_notin_used_empty];
paulson@2516
   104
paulson@2516
   105
paulson@2516
   106
(*** Supply fresh nonces for possibility theorems. ***)
paulson@2516
   107
paulson@3512
   108
(*In any trace, there is an upper bound N on the greatest nonce in use.*)
paulson@3683
   109
goal thy "EX N. ALL n. N<=n --> Nonce n ~: used evs";
paulson@3667
   110
by (induct_tac "evs" 1);
paulson@2516
   111
by (res_inst_tac [("x","0")] exI 1);
paulson@3683
   112
by (ALLGOALS (asm_simp_tac
paulson@3683
   113
	      (!simpset addsimps [used_Cons]
paulson@3683
   114
			setloop split_tac [expand_event_case, expand_if])));
paulson@2516
   115
by (Step_tac 1);
paulson@3512
   116
by (ALLGOALS (rtac (msg_Nonce_supply RS exE)));
paulson@3512
   117
by (ALLGOALS (blast_tac (!claset addSEs [add_leE])));
paulson@2516
   118
val lemma = result();
paulson@2516
   119
paulson@2516
   120
goal thy "EX N. Nonce N ~: used evs";
paulson@2516
   121
by (rtac (lemma RS exE) 1);
paulson@2891
   122
by (Blast_tac 1);
paulson@2516
   123
qed "Nonce_supply1";
paulson@2516
   124
paulson@2516
   125
goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
paulson@2516
   126
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   127
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   128
by (Step_tac 1);
paulson@2516
   129
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   130
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   131
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   132
				     le_add2, le_add1, 
paulson@2516
   133
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   134
qed "Nonce_supply2";
paulson@2516
   135
paulson@2516
   136
goal thy "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \
paulson@2516
   137
\                   Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''";
paulson@2516
   138
by (cut_inst_tac [("evs","evs")] lemma 1);
paulson@2516
   139
by (cut_inst_tac [("evs","evs'")] lemma 1);
paulson@2516
   140
by (cut_inst_tac [("evs","evs''")] lemma 1);
paulson@2516
   141
by (Step_tac 1);
paulson@2516
   142
by (res_inst_tac [("x","N")] exI 1);
paulson@2516
   143
by (res_inst_tac [("x","Suc (N+Na)")] exI 1);
paulson@2516
   144
by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1);
paulson@2516
   145
by (asm_simp_tac (!simpset addsimps [less_not_refl2 RS not_sym, 
paulson@2516
   146
				     le_add2, le_add1, 
paulson@2516
   147
				     le_eq_less_Suc RS sym]) 1);
paulson@2516
   148
by (rtac (less_trans RS less_not_refl2 RS not_sym) 1);
paulson@2516
   149
by (stac (le_eq_less_Suc RS sym) 1);
paulson@2516
   150
by (asm_simp_tac (!simpset addsimps [le_eq_less_Suc RS sym]) 2);
paulson@2516
   151
by (REPEAT (rtac le_add1 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@2516
   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@2516
   179
by (cut_inst_tac [("evs","evs'")] 
nipkow@3414
   180
    (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   181
by (etac exE 1);
paulson@2516
   182
by (cut_inst_tac [("evs","evs''")] 
nipkow@3414
   183
    (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1);
paulson@2516
   184
by (Step_tac 1);
paulson@2516
   185
by (Full_simp_tac 1);
paulson@2516
   186
by (fast_tac (!claset addSEs [allE]) 1);
paulson@2516
   187
qed "Key_supply3";
paulson@2516
   188
paulson@2516
   189
goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
nipkow@3414
   190
by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1);
paulson@2516
   191
by (rtac selectI 1);
paulson@2891
   192
by (Blast_tac 1);
paulson@2516
   193
qed "Key_supply";
paulson@2516
   194
paulson@2516
   195
(*** Tactics for possibility theorems ***)
paulson@2516
   196
paulson@3673
   197
(*Omitting used_Says makes the tactic much faster: it leaves expressions
paulson@3673
   198
    such as  Nonce ?N ~: used evs that match Nonce_supply*)
paulson@3542
   199
fun possibility_tac st = st |>
paulson@3673
   200
   (REPEAT 
paulson@3512
   201
    (ALLGOALS (simp_tac (!simpset delsimps [used_Says] setSolver safe_solver))
paulson@2516
   202
     THEN
paulson@2516
   203
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@3542
   204
                   resolve_tac [refl, conjI, Nonce_supply, Key_supply])));
paulson@2516
   205
paulson@2516
   206
(*For harder protocols (such as Recur) where we have to set up some
paulson@2516
   207
  nonces and keys initially*)
paulson@3542
   208
fun basic_possibility_tac st = st |>
paulson@2516
   209
    REPEAT 
oheimb@2637
   210
    (ALLGOALS (asm_simp_tac (!simpset setSolver safe_solver))
paulson@2516
   211
     THEN
paulson@2516
   212
     REPEAT_FIRST (resolve_tac [refl, conjI]));
paulson@2516
   213
paulson@2516
   214
paulson@3472
   215
(*** Specialized rewriting for analz_insert_freshK ***)
paulson@2320
   216
paulson@2516
   217
goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
paulson@2891
   218
by (Blast_tac 1);
paulson@2516
   219
qed "subset_Compl_range";
paulson@2045
   220
paulson@2516
   221
goal thy "insert (Key K) H = Key `` {K} Un H";
paulson@2891
   222
by (Blast_tac 1);
paulson@2516
   223
qed "insert_Key_singleton";
paulson@2516
   224
paulson@2516
   225
goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
paulson@2891
   226
by (Blast_tac 1);
paulson@2891
   227
qed "insert_Key_image";
paulson@2516
   228
paulson@3451
   229
(*Reverse the normal simplification of "image" to build up (not break down)
paulson@3451
   230
  the set of keys.  Use analz_insert_eq with (Un_upper2 RS analz_mono) to
paulson@3451
   231
  erase occurrences of forwarded message components (X).*)
paulson@2516
   232
val analz_image_freshK_ss = 
paulson@3673
   233
     !simpset addcongs [if_weak_cong]
paulson@3673
   234
	      delsimps [image_insert, image_Un]
paulson@3680
   235
              delsimps [imp_disjL]    (*reduces blow-up*)
paulson@3479
   236
              addsimps ([image_insert RS sym, image_Un RS sym,
paulson@3479
   237
                         analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono),
paulson@2516
   238
                         insert_Key_singleton, subset_Compl_range,
paulson@3479
   239
                         Key_not_used, insert_Key_image, Un_assoc RS sym]
paulson@2516
   240
                        @disj_comms)
paulson@2516
   241
              setloop split_tac [expand_if];
paulson@2045
   242
paulson@2045
   243
(*Lemma for the trivial direction of the if-and-only-if*)
paulson@2045
   244
goal thy  
paulson@2045
   245
 "!!evs. (Key K : analz (Key``nE Un H)) --> (K : nE | Key K : analz H)  ==> \
paulson@2045
   246
\        (Key K : analz (Key``nE Un H)) = (K : nE | Key K : analz H)";
paulson@2922
   247
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1);
paulson@2516
   248
qed "analz_image_freshK_lemma";