|
1 (* Title: HOL/Auth/Shared |
|
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 Shared, long-term keys; initial states of agents |
|
9 *) |
|
10 |
|
11 val inj_shrK = thm "inj_shrK"; |
|
12 val isSym_keys = thm "isSym_keys"; |
|
13 val Key_supply_ax = thm "Key_supply_ax"; |
|
14 |
|
15 (*** Basic properties of shrK ***) |
|
16 |
|
17 (*Injectiveness: Agents' long-term keys are distinct.*) |
|
18 AddIffs [inj_shrK RS inj_eq]; |
|
19 |
|
20 (* invKey(shrK A) = shrK A *) |
|
21 Addsimps [rewrite_rule [isSymKey_def] isSym_keys]; |
|
22 |
|
23 (** Rewrites should not refer to initState(Friend i) |
|
24 -- not in normal form! **) |
|
25 |
|
26 Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; |
|
27 by (induct_tac "C" 1); |
|
28 by Auto_tac; |
|
29 qed "keysFor_parts_initState"; |
|
30 Addsimps [keysFor_parts_initState]; |
|
31 |
|
32 (*Specialized to shared-key model: no need for addss in protocol proofs*) |
|
33 Goal "[| K: keysFor (parts (insert X H)); X : synth (analz H) |] \ |
|
34 \ ==> K : keysFor (parts H) | Key K : parts H"; |
|
35 by (force_tac |
|
36 (claset() addSDs [impOfSubs (parts_insert_subset_Un RS keysFor_mono), |
|
37 impOfSubs (analz_subset_parts RS keysFor_mono)] |
|
38 addIs [impOfSubs analz_subset_parts], |
|
39 simpset()) 1); |
|
40 qed "keysFor_parts_insert"; |
|
41 |
|
42 Goal "Crypt K X : H ==> K : keysFor H"; |
|
43 by (dtac Crypt_imp_invKey_keysFor 1); |
|
44 by (Asm_full_simp_tac 1); |
|
45 qed "Crypt_imp_keysFor"; |
|
46 |
|
47 |
|
48 (*** Function "knows" ***) |
|
49 |
|
50 (*Spy sees shared keys of agents!*) |
|
51 Goal "A: bad ==> Key (shrK A) : knows Spy evs"; |
|
52 by (induct_tac "evs" 1); |
|
53 by (ALLGOALS (asm_simp_tac |
|
54 (simpset() addsimps [imageI, knows_Cons] |
|
55 addsplits [expand_event_case]))); |
|
56 qed "Spy_knows_Spy_bad"; |
|
57 AddSIs [Spy_knows_Spy_bad]; |
|
58 |
|
59 (*For not_bad_tac*) |
|
60 Goal "[| Crypt (shrK A) X : analz (knows Spy evs); A: bad |] \ |
|
61 \ ==> X : analz (knows Spy evs)"; |
|
62 by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1); |
|
63 qed "Crypt_Spy_analz_bad"; |
|
64 |
|
65 (*Prove that the agent is uncompromised by the confidentiality of |
|
66 a component of a message she's said.*) |
|
67 fun not_bad_tac s = |
|
68 case_tac ("(" ^ s ^ ") : bad") THEN' |
|
69 SELECT_GOAL |
|
70 (REPEAT_DETERM (etac exE 1) THEN |
|
71 REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN |
|
72 REPEAT_DETERM (etac MPair_analz 1) THEN |
|
73 THEN_BEST_FIRST |
|
74 (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) |
|
75 (has_fewer_prems 1, size_of_thm) |
|
76 (Step_tac 1)); |
|
77 |
|
78 |
|
79 (** Fresh keys never clash with long-term shared keys **) |
|
80 |
|
81 (*Agents see their own shared keys!*) |
|
82 Goal "Key (shrK A) : initState A"; |
|
83 by (induct_tac "A" 1); |
|
84 by Auto_tac; |
|
85 qed "shrK_in_initState"; |
|
86 AddIffs [shrK_in_initState]; |
|
87 |
|
88 Goal "Key (shrK A) : used evs"; |
|
89 by (rtac initState_into_used 1); |
|
90 by (Blast_tac 1); |
|
91 qed "shrK_in_used"; |
|
92 AddIffs [shrK_in_used]; |
|
93 |
|
94 (*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
95 from long-term shared keys*) |
|
96 Goal "Key K ~: used evs ==> K ~: range shrK"; |
|
97 by (Blast_tac 1); |
|
98 qed "Key_not_used"; |
|
99 |
|
100 Goal "Key K ~: used evs ==> shrK B ~= K"; |
|
101 by (Blast_tac 1); |
|
102 qed "shrK_neq"; |
|
103 |
|
104 Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym]; |
|
105 |
|
106 |
|
107 (*** Fresh nonces ***) |
|
108 |
|
109 Goal "Nonce N ~: parts (initState B)"; |
|
110 by (induct_tac "B" 1); |
|
111 by Auto_tac; |
|
112 qed "Nonce_notin_initState"; |
|
113 AddIffs [Nonce_notin_initState]; |
|
114 |
|
115 Goal "Nonce N ~: used []"; |
|
116 by (simp_tac (simpset() addsimps [used_Nil]) 1); |
|
117 qed "Nonce_notin_used_empty"; |
|
118 Addsimps [Nonce_notin_used_empty]; |
|
119 |
|
120 |
|
121 (*** Supply fresh nonces for possibility theorems. ***) |
|
122 |
|
123 (*In any trace, there is an upper bound N on the greatest nonce in use.*) |
|
124 Goal "EX N. ALL n. N<=n --> Nonce n ~: used evs"; |
|
125 by (induct_tac "evs" 1); |
|
126 by (res_inst_tac [("x","0")] exI 1); |
|
127 by (ALLGOALS (asm_simp_tac |
|
128 (simpset() addsimps [used_Cons] |
|
129 addsplits [expand_event_case]))); |
|
130 by Safe_tac; |
|
131 by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); |
|
132 by (ALLGOALS (blast_tac (claset() addSEs [add_leE]))); |
|
133 val lemma = result(); |
|
134 |
|
135 Goal "EX N. Nonce N ~: used evs"; |
|
136 by (rtac (lemma RS exE) 1); |
|
137 by (Blast_tac 1); |
|
138 qed "Nonce_supply1"; |
|
139 |
|
140 Goal "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'"; |
|
141 by (cut_inst_tac [("evs","evs")] lemma 1); |
|
142 by (cut_inst_tac [("evs","evs'")] lemma 1); |
|
143 by (Clarify_tac 1); |
|
144 by (res_inst_tac [("x","N")] exI 1); |
|
145 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
|
146 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, |
|
147 less_Suc_eq_le]) 1); |
|
148 qed "Nonce_supply2"; |
|
149 |
|
150 Goal "EX N N' N''. Nonce N ~: used evs & Nonce N' ~: used evs' & \ |
|
151 \ Nonce N'' ~: used evs'' & N ~= N' & N' ~= N'' & N ~= N''"; |
|
152 by (cut_inst_tac [("evs","evs")] lemma 1); |
|
153 by (cut_inst_tac [("evs","evs'")] lemma 1); |
|
154 by (cut_inst_tac [("evs","evs''")] lemma 1); |
|
155 by (Clarify_tac 1); |
|
156 by (res_inst_tac [("x","N")] exI 1); |
|
157 by (res_inst_tac [("x","Suc (N+Na)")] exI 1); |
|
158 by (res_inst_tac [("x","Suc (Suc (N+Na+Nb))")] exI 1); |
|
159 by (asm_simp_tac (simpset() addsimps [less_not_refl3, le_add1, le_add2, |
|
160 less_Suc_eq_le]) 1); |
|
161 qed "Nonce_supply3"; |
|
162 |
|
163 Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
|
164 by (rtac (lemma RS exE) 1); |
|
165 by (rtac someI 1); |
|
166 by (Blast_tac 1); |
|
167 qed "Nonce_supply"; |
|
168 |
|
169 (*** Supply fresh keys for possibility theorems. ***) |
|
170 |
|
171 Goal "EX K. Key K ~: used evs"; |
|
172 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1); |
|
173 by (Blast_tac 1); |
|
174 qed "Key_supply1"; |
|
175 |
|
176 Goal "EX K K'. Key K ~: used evs & Key K' ~: used evs' & K ~= K'"; |
|
177 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1); |
|
178 by (etac exE 1); |
|
179 by (cut_inst_tac [("evs","evs'")] |
|
180 (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1); |
|
181 by (Asm_full_simp_tac 1 THEN depth_tac (claset()) 2 1); (* replaces Auto_tac *) |
|
182 qed "Key_supply2"; |
|
183 |
|
184 Goal "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \ |
|
185 \ Key K'' ~: used evs'' & K ~= K' & K' ~= K'' & K ~= K''"; |
|
186 by (cut_inst_tac [("evs","evs")] (Finites.emptyI RS Key_supply_ax) 1); |
|
187 by (etac exE 1); |
|
188 (*Blast_tac requires instantiation of the keys for some reason*) |
|
189 by (cut_inst_tac [("evs","evs'"), ("a1","K")] |
|
190 (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1); |
|
191 by (etac exE 1); |
|
192 by (cut_inst_tac [("evs","evs''"), ("a1","Ka"), ("a2","K")] |
|
193 (Finites.emptyI RS Finites.insertI RS Finites.insertI RS Key_supply_ax) 1); |
|
194 by (Blast_tac 1); |
|
195 qed "Key_supply3"; |
|
196 |
|
197 Goal "Key (@ K. Key K ~: used evs) ~: used evs"; |
|
198 by (rtac (Finites.emptyI RS Key_supply_ax RS exE) 1); |
|
199 by (rtac someI 1); |
|
200 by (Blast_tac 1); |
|
201 qed "Key_supply"; |
|
202 |
|
203 (*** Tactics for possibility theorems ***) |
|
204 |
|
205 (*Omitting used_Says makes the tactic much faster: it leaves expressions |
|
206 such as Nonce ?N ~: used evs that match Nonce_supply*) |
|
207 fun possibility_tac st = st |> |
|
208 (REPEAT |
|
209 (ALLGOALS (simp_tac (simpset() delsimps [used_Says, used_Notes, used_Gets] |
|
210 setSolver safe_solver)) |
|
211 THEN |
|
212 REPEAT_FIRST (eq_assume_tac ORELSE' |
|
213 resolve_tac [refl, conjI, Nonce_supply, Key_supply]))); |
|
214 |
|
215 (*For harder protocols (such as Recur) where we have to set up some |
|
216 nonces and keys initially*) |
|
217 fun basic_possibility_tac st = st |> |
|
218 REPEAT |
|
219 (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) |
|
220 THEN |
|
221 REPEAT_FIRST (resolve_tac [refl, conjI])); |
|
222 |
|
223 |
|
224 (*** Specialized rewriting for analz_insert_freshK ***) |
|
225 |
|
226 Goal "A <= - (range shrK) ==> shrK x ~: A"; |
|
227 by (Blast_tac 1); |
|
228 qed "subset_Compl_range"; |
|
229 |
|
230 Goal "insert (Key K) H = Key ` {K} Un H"; |
|
231 by (Blast_tac 1); |
|
232 qed "insert_Key_singleton"; |
|
233 |
|
234 Goal "insert (Key K) (Key`KK Un C) = Key ` (insert K KK) Un C"; |
|
235 by (Blast_tac 1); |
|
236 qed "insert_Key_image"; |
|
237 |
|
238 (** Reverse the normal simplification of "image" to build up (not break down) |
|
239 the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to |
|
240 erase occurrences of forwarded message components (X). **) |
|
241 |
|
242 bind_thms ("analz_image_freshK_simps", |
|
243 simp_thms @ mem_simps @ (*these two allow its use with only:*) |
|
244 disj_comms @ |
|
245 [image_insert RS sym, image_Un RS sym, empty_subsetI, insert_subset, |
|
246 analz_insert_eq, impOfSubs (Un_upper2 RS analz_mono), |
|
247 insert_Key_singleton, subset_Compl_range, |
|
248 Key_not_used, insert_Key_image, Un_assoc RS sym]); |
|
249 |
|
250 val analz_image_freshK_ss = |
|
251 simpset() delsimps [image_insert, image_Un] |
|
252 delsimps [imp_disjL] (*reduces blow-up*) |
|
253 addsimps analz_image_freshK_simps; |
|
254 |
|
255 (*Lemma for the trivial direction of the if-and-only-if*) |
|
256 Goal "(Key K : analz (Key`nE Un H)) --> (K : nE | Key K : analz H) ==> \ |
|
257 \ (Key K : analz (Key`nE Un H)) = (K : nE | Key K : analz H)"; |
|
258 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
|
259 qed "analz_image_freshK_lemma"; |
|
260 |