src/HOL/Auth/Public.ML
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2637 e9b203f854ae
child 3121 cbb6c0c1c58a
permissions -rw-r--r--
Dep. on Provers/nat_transitive
paulson@2318
     1
(*  Title:      HOL/Auth/Public
paulson@2318
     2
    ID:         $Id$
paulson@2318
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@2318
     4
    Copyright   1996  University of Cambridge
paulson@2318
     5
paulson@2318
     6
Theory of Public Keys (common to all symmetric-key protocols)
paulson@2318
     7
paulson@2318
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
paulson@2318
     9
*)
paulson@2318
    10
paulson@2318
    11
paulson@2318
    12
open Public;
paulson@2318
    13
paulson@2497
    14
(*Injectiveness of new nonces*)
paulson@2497
    15
AddIffs [inj_newN RS inj_eq];
paulson@2497
    16
paulson@2318
    17
(*Holds because Friend is injective: thus cannot prove for all f*)
paulson@2318
    18
goal thy "(Friend x : Friend``A) = (x:A)";
paulson@2318
    19
by (Auto_tac());
paulson@2318
    20
qed "Friend_image_eq";
paulson@2318
    21
Addsimps [Friend_image_eq];
paulson@2318
    22
paulson@2318
    23
Addsimps [Un_insert_left, Un_insert_right];
paulson@2318
    24
paulson@2318
    25
(*By default only o_apply is built-in.  But in the presence of eta-expansion
paulson@2318
    26
  this means that some terms displayed as (f o g) will be rewritten, and others
paulson@2318
    27
  will not!*)
paulson@2318
    28
Addsimps [o_def];
paulson@2318
    29
paulson@2318
    30
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
paulson@2318
    31
by (agent.induct_tac "C" 1);
paulson@2318
    32
by (auto_tac (!claset addIs [range_eqI], !simpset));
paulson@2318
    33
qed "keysFor_parts_initState";
paulson@2318
    34
Addsimps [keysFor_parts_initState];
paulson@2318
    35
paulson@2318
    36
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
paulson@2318
    37
by (Auto_tac ());
paulson@2318
    38
qed "keysFor_image_Key";
paulson@2318
    39
Addsimps [keysFor_image_Key];
paulson@2318
    40
paulson@2318
    41
paulson@2318
    42
(*** Function "sees" ***)
paulson@2318
    43
paulson@2318
    44
goal thy
paulson@2318
    45
    "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
paulson@2318
    46
by (list.induct_tac "evs" 1);
paulson@2318
    47
by (agent.induct_tac "A" 1);
paulson@2318
    48
by (event.induct_tac "a" 2);
paulson@2318
    49
by (Auto_tac ());
paulson@2318
    50
qed "sees_mono";
paulson@2318
    51
paulson@2497
    52
(*** Basic properties of pubK & priK ***)
paulson@2497
    53
paulson@2497
    54
AddIffs [inj_pubK RS inj_eq];
paulson@2497
    55
Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
paulson@2497
    56
paulson@2318
    57
(*Agents see their own private keys!*)
paulson@2318
    58
goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
paulson@2318
    59
by (list.induct_tac "evs" 1);
paulson@2318
    60
by (agent.induct_tac "A" 1);
paulson@2318
    61
by (Auto_tac ());
paulson@2318
    62
qed_spec_mp "sees_own_priK";
paulson@2318
    63
paulson@2318
    64
(*All public keys are visible*)
paulson@2318
    65
goal thy "Key (pubK A) : sees lost A evs";
paulson@2318
    66
by (list.induct_tac "evs" 1);
paulson@2318
    67
by (agent.induct_tac "A" 1);
paulson@2318
    68
by (Auto_tac ());
paulson@2318
    69
qed_spec_mp "sees_pubK";
paulson@2318
    70
paulson@2318
    71
(*Spy sees private keys of lost agents!*)
paulson@2318
    72
goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs";
paulson@2318
    73
by (list.induct_tac "evs" 1);
paulson@2318
    74
by (Auto_tac());
paulson@2318
    75
qed "Spy_sees_lost";
paulson@2318
    76
paulson@2318
    77
AddIffs [sees_pubK];
paulson@2318
    78
AddSIs  [sees_own_priK, Spy_sees_lost];
paulson@2318
    79
paulson@2318
    80
(*Added for Yahalom/lost_tac*)
paulson@2318
    81
goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs);  A: lost |] \
paulson@2318
    82
\              ==> X : analz (sees lost Spy evs)";
paulson@2318
    83
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
paulson@2318
    84
qed "Crypt_Spy_analz_lost";
paulson@2318
    85
paulson@2318
    86
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
paulson@2318
    87
paulson@2318
    88
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
paulson@2318
    89
by (Simp_tac 1);
paulson@2318
    90
qed "sees_own";
paulson@2318
    91
paulson@2318
    92
goal thy "!!A. Server ~= B ==> \
paulson@2318
    93
\          sees lost Server (Says A B X # evs) = sees lost Server evs";
paulson@2318
    94
by (Asm_simp_tac 1);
paulson@2318
    95
qed "sees_Server";
paulson@2318
    96
paulson@2318
    97
goal thy "!!A. Friend i ~= B ==> \
paulson@2318
    98
\          sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
paulson@2318
    99
by (Asm_simp_tac 1);
paulson@2318
   100
qed "sees_Friend";
paulson@2318
   101
paulson@2318
   102
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
paulson@2318
   103
by (Simp_tac 1);
paulson@2318
   104
qed "sees_Spy";
paulson@2318
   105
paulson@2318
   106
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
paulson@2318
   107
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2318
   108
by (Fast_tac 1);
paulson@2318
   109
qed "sees_Says_subset_insert";
paulson@2318
   110
paulson@2318
   111
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
paulson@2318
   112
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
paulson@2318
   113
by (Fast_tac 1);
paulson@2318
   114
qed "sees_subset_sees_Says";
paulson@2318
   115
paulson@2318
   116
(*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
paulson@2318
   117
  Once used to prove new_keys_not_seen; now obsolete.*)
paulson@2318
   118
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
paulson@2318
   119
\         parts {Y} Un (UN A. parts (sees lost A evs))";
paulson@2318
   120
by (Step_tac 1);
paulson@2318
   121
by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
paulson@2318
   122
by (ALLGOALS
paulson@2318
   123
    (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] 
paulson@2318
   124
                       setloop split_tac [expand_if]))));
paulson@2318
   125
qed "UN_parts_sees_Says";
paulson@2318
   126
paulson@2318
   127
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
paulson@2318
   128
by (list.induct_tac "evs" 1);
paulson@2318
   129
by (Auto_tac ());
paulson@2318
   130
qed_spec_mp "Says_imp_sees_Spy";
paulson@2318
   131
paulson@2537
   132
(*Use with addSEs to derive contradictions from old Says events containing
paulson@2537
   133
  items known to be fresh*)
paulson@2537
   134
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs;
paulson@2537
   135
paulson@2318
   136
goal thy  
paulson@2318
   137
 "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;  C : lost |] \
paulson@2318
   138
\        ==> X : analz (sees lost Spy evs)";
paulson@2318
   139
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
paulson@2318
   140
                      addss (!simpset)) 1);
paulson@2318
   141
qed "Says_Crypt_lost";
paulson@2318
   142
paulson@2318
   143
goal thy  
paulson@2318
   144
 "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs;        \
paulson@2318
   145
\           X ~: analz (sees lost Spy evs) |]                     \
paulson@2318
   146
\        ==> C ~: lost";
paulson@2318
   147
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
paulson@2318
   148
                      addss (!simpset)) 1);
paulson@2318
   149
qed "Says_Crypt_not_lost";
paulson@2318
   150
paulson@2318
   151
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
paulson@2318
   152
Delsimps [sees_Cons];   (**** NOTE REMOVAL -- laws above are cleaner ****)
paulson@2318
   153
paulson@2318
   154
paulson@2497
   155
(*** Fresh nonces ***)
paulson@2497
   156
paulson@2497
   157
goal thy "Nonce N ~: parts (initState lost B)";
paulson@2497
   158
by (agent.induct_tac "B" 1);
paulson@2497
   159
by (Auto_tac ());
paulson@2497
   160
qed "Nonce_notin_initState";
paulson@2497
   161
paulson@2497
   162
AddIffs [Nonce_notin_initState];
paulson@2497
   163
paulson@2497
   164
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
paulson@2516
   165
by (etac (impOfSubs parts_mono) 1);
paulson@2497
   166
by (Fast_tac 1);
paulson@2497
   167
qed "usedI";
paulson@2497
   168
paulson@2497
   169
AddIs [usedI];
paulson@2497
   170
paulson@2516
   171
(** A supply of fresh nonces for possibility theorems. **)
paulson@2516
   172
paulson@2497
   173
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
paulson@2497
   174
by (list.induct_tac "evs" 1);
paulson@2497
   175
by (res_inst_tac [("x","0")] exI 1);
paulson@2497
   176
by (Step_tac 1);
paulson@2497
   177
by (Full_simp_tac 1);
paulson@2516
   178
(*Inductive step*)
paulson@2497
   179
by (event.induct_tac "a" 1);
paulson@2497
   180
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
paulson@2497
   181
by (msg.induct_tac "msg" 1);
paulson@2497
   182
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
paulson@2497
   183
by (Step_tac 1);
paulson@2497
   184
(*MPair case*)
paulson@2497
   185
by (res_inst_tac [("x","Na+Nb")] exI 2);
paulson@2497
   186
by (fast_tac (!claset addSEs [add_leE]) 2);
paulson@2497
   187
(*Nonce case*)
paulson@2497
   188
by (res_inst_tac [("x","N + Suc nat")] exI 1);
oheimb@2637
   189
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
paulson@2497
   190
val lemma = result();
paulson@2497
   191
paulson@2497
   192
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
paulson@2516
   193
by (rtac (lemma RS exE) 1);
paulson@2516
   194
by (rtac selectI 1);
paulson@2497
   195
by (Fast_tac 1);
paulson@2497
   196
qed "Nonce_supply";
paulson@2497
   197
paulson@2516
   198
(*Tactic for possibility theorems*)
paulson@2516
   199
val possibility_tac =
paulson@2516
   200
    REPEAT 
oheimb@2637
   201
    (ALLGOALS (simp_tac (!simpset setSolver safe_solver))
paulson@2516
   202
     THEN
paulson@2516
   203
     REPEAT_FIRST (eq_assume_tac ORELSE' 
paulson@2516
   204
                   resolve_tac [refl, conjI, Nonce_supply]));
paulson@2497
   205
paulson@2318
   206
(** Power of the Spy **)
paulson@2318
   207
paulson@2318
   208
(*The Spy can see more than anybody else, except for their initial state*)
paulson@2318
   209
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
paulson@2318
   210
by (list.induct_tac "evs" 1);
paulson@2318
   211
by (event.induct_tac "a" 2);
paulson@2318
   212
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] 
paulson@2318
   213
                                addss (!simpset))));
paulson@2318
   214
qed "sees_agent_subset_sees_Spy";
paulson@2318
   215
paulson@2318
   216
(*The Spy can see more than anybody else who's lost their key!*)
paulson@2318
   217
goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
paulson@2318
   218
by (list.induct_tac "evs" 1);
paulson@2318
   219
by (event.induct_tac "a" 2);
paulson@2318
   220
by (agent.induct_tac "A" 1);
paulson@2318
   221
by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
paulson@2318
   222
qed_spec_mp "sees_lost_agent_subset_sees_Spy";
paulson@2318
   223
paulson@2318
   224
paulson@2318
   225
(** Simplifying   parts (insert X (sees lost A evs))
paulson@2318
   226
      = parts {X} Un parts (sees lost A evs) -- since general case loops*)
paulson@2318
   227
paulson@2318
   228
val parts_insert_sees = 
paulson@2318
   229
    parts_insert |> read_instantiate_sg (sign_of thy)
paulson@2318
   230
                                        [("H", "sees lost A evs")]
paulson@2318
   231
                 |> standard;