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