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