src/HOL/Auth/Shared.ML
author paulson
Wed, 21 Aug 1996 13:25:27 +0200
changeset 1934 58573e7041b4
child 1943 20574dca5a3e
permissions -rw-r--r--
Separation of theory Event into two parts: Shared for general shared-key material NS_Shared for the Needham-Schroeder shared-key protocol
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1934
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Auth/Message
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     2
    ID:         $Id$
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     4
    Copyright   1996  University of Cambridge
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     5
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     6
Theory of Shared Keys (common to all symmetric-key protocols)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     7
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     8
Server keys; initial states of agents; new nonces and keys; function "sees" 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
     9
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    10
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    11
*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    12
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    13
Addsimps [parts_cut_eq];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    14
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    15
proof_timing:=true;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    16
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    17
(*IN SET.ML*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    18
goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    19
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    20
qed "mem_if";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    21
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    22
(*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    23
goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    24
by (fast_tac (!claset addEs [equalityE]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    25
val subset_range_iff = result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    26
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    27
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    28
open Shared;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    29
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    30
Addsimps [Un_insert_left, Un_insert_right];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    31
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    32
(*By default only o_apply is built-in.  But in the presence of eta-expansion
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    33
  this means that some terms displayed as (f o g) will be rewritten, and others
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    34
  will not!*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    35
Addsimps [o_def];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    36
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    37
(*** Basic properties of serverKey and newK ***)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    38
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    39
(* invKey (serverKey A) = serverKey A *)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    40
bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    41
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    42
(* invKey (newK evs) = newK evs *)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    43
bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    44
Addsimps [invKey_serverKey, invKey_newK];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    45
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    46
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    47
(*New keys and nonces are fresh*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    48
val serverKey_inject = inj_serverKey RS injD;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    49
val newN_inject = inj_newN RS injD
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    50
and newK_inject = inj_newK RS injD;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    51
AddSEs [serverKey_inject, newN_inject, newK_inject,
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    52
	fresh_newK RS notE, fresh_newN RS notE];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    53
Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    54
Addsimps [fresh_newN, fresh_newK];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    55
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    56
(** Rewrites should not refer to  initState(Friend i) 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    57
    -- not in normal form! **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    58
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    59
goal thy "newK evs ~= serverKey B";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    60
by (subgoal_tac "newK evs = serverKey B --> \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    61
\                Key (newK evs) : parts (initState B)" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    62
by (Fast_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    63
by (agent.induct_tac "B" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    64
by (auto_tac (!claset addIs [range_eqI], !simpset));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    65
qed "newK_neq_serverKey";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    66
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    67
Addsimps [newK_neq_serverKey, newK_neq_serverKey RS not_sym];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    68
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    69
(*Good for talking about Server's initial state*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    70
goal thy "!!H. H <= Key``E ==> parts H = H";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    71
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    72
be parts.induct 1;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    73
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    74
qed "parts_image_subset";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    75
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    76
bind_thm ("parts_image_Key", subset_refl RS parts_image_subset);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    77
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    78
goal thy "!!H. H <= Key``E ==> analz H = H";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    79
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    80
be analz.induct 1;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    81
by (ALLGOALS (fast_tac (!claset addss (!simpset))));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    82
qed "analz_image_subset";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    83
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    84
bind_thm ("analz_image_Key", subset_refl RS analz_image_subset);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    85
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    86
Addsimps [parts_image_Key, analz_image_Key];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    87
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    88
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    89
by (agent.induct_tac "C" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    90
by (auto_tac (!claset addIs [range_eqI] delrules partsEs, !simpset));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    91
qed "keysFor_parts_initState";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    92
Addsimps [keysFor_parts_initState];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    93
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    94
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    95
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    96
qed "keysFor_image_Key";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    97
Addsimps [keysFor_image_Key];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    98
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
    99
goal thy "serverKey A ~: newK``E";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   100
by (agent.induct_tac "A" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   101
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   102
qed "serverKey_notin_image_newK";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   103
Addsimps [serverKey_notin_image_newK];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   104
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   105
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   106
(*Agents see their own serverKeys!*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   107
goal thy "Key (serverKey A) : analz (sees A evs)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   108
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   109
by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   110
by (agent.induct_tac "A" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   111
by (auto_tac (!claset addIs [range_eqI], !simpset));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   112
qed "analz_own_serverKey";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   113
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   114
bind_thm ("parts_own_serverKey",
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   115
	  [analz_subset_parts, analz_own_serverKey] MRS subsetD);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   116
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   117
Addsimps [analz_own_serverKey, parts_own_serverKey];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   118
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   119
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   120
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   121
(** Specialized rewrite rules for (sees A (Says...#evs)) **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   122
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   123
goal thy "sees A (Says A B X # evs) = insert X (sees A evs)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   124
by (Simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   125
qed "sees_own";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   126
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   127
goal thy "!!A. Server ~= A ==> \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   128
\              sees Server (Says A B X # evs) = sees Server evs";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   129
by (Asm_simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   130
qed "sees_Server";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   131
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   132
goal thy "!!A. Friend i ~= A ==> \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   133
\              sees (Friend i) (Says A B X # evs) = sees (Friend i) evs";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   134
by (Asm_simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   135
qed "sees_Friend";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   136
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   137
goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   138
by (Simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   139
qed "sees_Enemy";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   140
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   141
goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   142
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   143
by (Fast_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   144
qed "sees_Says_subset_insert";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   145
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   146
goal thy "sees A evs <= sees A (Says A' B X # evs)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   147
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   148
by (Fast_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   149
qed "sees_subset_sees_Says";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   150
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   151
(*Pushing Unions into parts; one of the A's equals B, and thus sees Y*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   152
goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   153
\         parts {Y} Un (UN A. parts (sees A evs))";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   154
by (Step_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   155
be rev_mp 1;	(*for some reason, split_tac does not work on assumptions*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   156
val ss = (!simpset addsimps [parts_Un, sees_Cons] 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   157
	           setloop split_tac [expand_if]);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   158
by (ALLGOALS (fast_tac (!claset addss ss)));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   159
qed "UN_parts_sees_Says";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   160
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   161
goal thy "Says A B X : set_of_list evs --> X : sees Enemy evs";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   162
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   163
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   164
qed_spec_mp "Says_imp_sees_Enemy";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   165
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   166
Addsimps [Says_imp_sees_Enemy];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   167
AddIs    [Says_imp_sees_Enemy];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   168
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   169
goal thy "initState C <= Key `` range serverKey";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   170
by (agent.induct_tac "C" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   171
by (Auto_tac ());
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   172
qed "initState_subset";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   173
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   174
goal thy "X : sees C evs --> \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   175
\          (EX A B. Says A B X : set_of_list evs) | \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   176
\          (EX A. Notes A X : set_of_list evs) | \
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   177
\          (EX A. X = Key (serverKey A))";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   178
by (list.induct_tac "evs" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   179
by (ALLGOALS Asm_simp_tac);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   180
by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   181
br conjI 1;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   182
by (Fast_tac 2);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   183
by (event.induct_tac "a" 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   184
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   185
by (ALLGOALS Fast_tac);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   186
qed_spec_mp "seesD";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   187
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   188
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   189
Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   190
Delsimps [sees_Cons];	(**** NOTE REMOVAL -- laws above are cleaner ****)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   191
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   192
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   193
goal thy "!!K. newK evs = invKey K ==> newK evs = K";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   194
br (invKey_eq RS iffD1) 1;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   195
by (Simp_tac 1);
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   196
val newK_invKey = result();
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   197
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   198
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   199
(** Rewrites to push in Key and Crypt messages, so that other messages can
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   200
    be pulled out using the analz_insert rules **)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   201
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   202
fun insComm x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   203
                      insert_commute;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   204
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   205
val pushKeys = map (insComm "Key ?K") 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   206
                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   207
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   208
val pushCrypts = map (insComm "Crypt ?X ?K") 
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   209
                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   210
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   211
(*Cannot be added with Addsimps -- we don't always want to re-order messages*)
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   212
val pushes = pushKeys@pushCrypts;
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   213
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   214
val pushKey_newK = insComm "Key (newK ?evs)"  "Key (serverKey ?C)";
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   215
58573e7041b4 Separation of theory Event into two parts:
paulson
parents:
diff changeset
   216