18 By induction on a list of agents (no repetitions) |
18 By induction on a list of agents (no repetitions) |
19 **) |
19 **) |
20 |
20 |
21 |
21 |
22 (*Simplest case: Alice goes directly to the server*) |
22 (*Simplest case: Alice goes directly to the server*) |
23 Goal "EX K NA. EX evs: recur. \ |
23 Goal "\\<exists>K NA. \\<exists>evs \\<in> recur. \ |
24 \ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ |
24 \ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \ |
25 \ END|} : set evs"; |
25 \ END|} \\<in> set evs"; |
26 by (REPEAT (resolve_tac [exI,bexI] 1)); |
26 by (REPEAT (resolve_tac [exI,bexI] 1)); |
27 by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2); |
27 by (rtac (recur.Nil RS recur.RA1 RS (respond.One RSN (3,recur.RA3))) 2); |
28 by possibility_tac; |
28 by possibility_tac; |
29 result(); |
29 result(); |
30 |
30 |
31 |
31 |
32 (*Case two: Alice, Bob and the server*) |
32 (*Case two: Alice, Bob and the server*) |
33 Goal "EX K. EX NA. EX evs: recur. \ |
33 Goal "\\<exists>K. \\<exists>NA. \\<exists>evs \\<in> recur. \ |
34 \ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ |
34 \ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ |
35 \ END|} : set evs"; |
35 \ END|} \\<in> set evs"; |
36 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); |
36 by (cut_facts_tac [Nonce_supply2, Key_supply2] 1); |
37 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
37 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
38 by (REPEAT (resolve_tac [exI,bexI] 1)); |
38 by (REPEAT (resolve_tac [exI,bexI] 1)); |
39 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS |
39 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS |
40 (respond.One RS respond.Cons RSN (3,recur.RA3)) RS |
40 (respond.One RS respond.Cons RSN (3,recur.RA3)) RS |
44 result(); |
44 result(); |
45 |
45 |
46 |
46 |
47 (*Case three: Alice, Bob, Charlie and the server |
47 (*Case three: Alice, Bob, Charlie and the server |
48 TOO SLOW to run every time! |
48 TOO SLOW to run every time! |
49 Goal "EX K. EX NA. EX evs: recur. \ |
49 Goal "\\<exists>K. \\<exists>NA. \\<exists>evs \\<in> recur. \ |
50 \ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ |
50 \ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \ |
51 \ END|} : set evs"; |
51 \ END|} \\<in> set evs"; |
52 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); |
52 by (cut_facts_tac [Nonce_supply3, Key_supply3] 1); |
53 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
53 by (REPEAT (eresolve_tac [exE, conjE] 1)); |
54 by (REPEAT (resolve_tac [exI,bexI] 1)); |
54 by (REPEAT (resolve_tac [exI,bexI] 1)); |
55 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS |
55 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS |
56 (respond.One RS respond.Cons RS respond.Cons RSN |
56 (respond.One RS respond.Cons RS respond.Cons RSN |
57 (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); |
57 (3,recur.RA3)) RS recur.RA4 RS recur.RA4) 2); |
58 (*SLOW: 33 seconds*) |
|
59 by basic_possibility_tac; |
58 by basic_possibility_tac; |
60 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 |
59 by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1 |
61 ORELSE |
60 ORELSE |
62 eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); |
61 eresolve_tac [asm_rl, less_not_refl2, less_not_refl3] 1)); |
63 result(); |
62 result(); |
64 ****************) |
63 ****************) |
65 |
64 |
66 (**** Inductive proofs about recur ****) |
65 (**** Inductive proofs about recur ****) |
67 |
66 |
68 |
67 Goal "(PA,RB,KAB) \\<in> respond evs ==> Key KAB \\<notin> used evs"; |
69 Goal "(PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}"; |
|
70 by (etac respond.induct 1); |
|
71 by (ALLGOALS Simp_tac); |
|
72 qed "respond_Key_in_parts"; |
|
73 |
|
74 Goal "(PA,RB,KAB) : respond evs ==> Key KAB ~: used evs"; |
|
75 by (etac respond.induct 1); |
68 by (etac respond.induct 1); |
76 by (REPEAT (assume_tac 1)); |
69 by (REPEAT (assume_tac 1)); |
77 qed "respond_imp_not_used"; |
70 qed "respond_imp_not_used"; |
78 |
71 |
79 Goal "[| Key K : parts {RB}; (PB,RB,K') : respond evs |] \ |
72 Goal "[| Key K \\<in> parts {RB}; (PB,RB,K') \\<in> respond evs |] ==> Key K \\<notin> used evs"; |
80 \ ==> Key K ~: used evs"; |
|
81 by (etac rev_mp 1); |
73 by (etac rev_mp 1); |
82 by (etac respond.induct 1); |
74 by (etac respond.induct 1); |
83 by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used], |
75 by (auto_tac(claset() addDs [Key_not_used, respond_imp_not_used], |
84 simpset())); |
76 simpset())); |
85 qed_spec_mp "Key_in_parts_respond"; |
77 qed_spec_mp "Key_in_parts_respond"; |
86 |
78 |
87 (*Simple inductive reasoning about responses*) |
79 (*Simple inductive reasoning about responses*) |
88 Goal "(PA,RB,KAB) : respond evs ==> RB : responses evs"; |
80 Goal "(PA,RB,KAB) \\<in> respond evs ==> RB \\<in> responses evs"; |
89 by (etac respond.induct 1); |
81 by (etac respond.induct 1); |
90 by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); |
82 by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1)); |
91 qed "respond_imp_responses"; |
83 qed "respond_imp_responses"; |
92 |
84 |
93 |
85 |
94 (** For reasoning about the encrypted portion of messages **) |
86 (** For reasoning about the encrypted portion of messages **) |
95 |
87 |
96 val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; |
88 val RA2_analz_spies = Says_imp_spies RS analz.Inj |> standard; |
97 |
89 |
98 Goal "Says C' B {|Crypt K X, X', RA|} : set evs ==> RA : analz (spies evs)"; |
90 Goal "Says C' B {|Crypt K X, X', RA|} \\<in> set evs ==> RA \\<in> analz (spies evs)"; |
99 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
91 by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); |
100 qed "RA4_analz_spies"; |
92 qed "RA4_analz_spies"; |
101 |
93 |
102 (*RA2_analz... and RA4_analz... let us treat those cases using the same |
94 (*RA2_analz... and RA4_analz... let us treat those cases using the same |
103 argument as for the Fake case. This is possible for most, but not all, |
95 argument as for the Fake case. This is possible for most, but not all, |
107 bind_thm ("RA2_parts_spies", |
99 bind_thm ("RA2_parts_spies", |
108 RA2_analz_spies RS (impOfSubs analz_subset_parts)); |
100 RA2_analz_spies RS (impOfSubs analz_subset_parts)); |
109 bind_thm ("RA4_parts_spies", |
101 bind_thm ("RA4_parts_spies", |
110 RA4_analz_spies RS (impOfSubs analz_subset_parts)); |
102 RA4_analz_spies RS (impOfSubs analz_subset_parts)); |
111 |
103 |
112 (*For proving the easier theorems about X ~: parts (spies evs).*) |
104 (*For proving the easier theorems about X \\<notin> parts (spies evs).*) |
113 fun parts_induct_tac i = |
105 fun parts_induct_tac i = |
114 EVERY [etac recur.induct i, |
106 EVERY [etac recur.induct i, |
115 ftac RA4_parts_spies (i+5), |
107 ftac RA4_parts_spies (i+5), |
116 ftac respond_imp_responses (i+4), |
108 ftac respond_imp_responses (i+4), |
117 ftac RA2_parts_spies (i+3), |
109 ftac RA2_parts_spies (i+3), |
118 prove_simple_subgoals_tac i]; |
110 prove_simple_subgoals_tac i]; |
119 |
111 |
120 |
112 |
121 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
113 (** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY |
122 sends messages containing X! **) |
114 sends messages containing X! **) |
123 |
115 |
124 |
116 |
125 (** Spy never sees another agent's shared key! (unless it's bad at start) **) |
117 (** Spy never sees another agent's shared key! (unless it's bad at start) **) |
126 |
118 |
127 Goal "evs : recur ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
119 Goal "evs \\<in> recur ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; |
128 by (parts_induct_tac 1); |
120 by (parts_induct_tac 1); |
129 by Auto_tac; |
121 by Auto_tac; |
130 (*RA3*) |
122 (*RA3*) |
131 by (auto_tac (claset() addDs [Key_in_parts_respond], |
123 by (auto_tac (claset() addDs [Key_in_parts_respond], |
132 simpset() addsimps [parts_insert_spies])); |
124 simpset() addsimps [parts_insert_spies])); |
133 qed "Spy_see_shrK"; |
125 qed "Spy_see_shrK"; |
134 Addsimps [Spy_see_shrK]; |
126 Addsimps [Spy_see_shrK]; |
135 |
127 |
136 Goal "evs : recur ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
128 Goal "evs \\<in> recur ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; |
137 by Auto_tac; |
129 by Auto_tac; |
138 qed "Spy_analz_shrK"; |
130 qed "Spy_analz_shrK"; |
139 Addsimps [Spy_analz_shrK]; |
131 Addsimps [Spy_analz_shrK]; |
140 |
132 |
141 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
133 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
143 |
135 |
144 |
136 |
145 (** Nobody can have used non-existent keys! **) |
137 (** Nobody can have used non-existent keys! **) |
146 |
138 |
147 (*The special case of H={} has the same proof*) |
139 (*The special case of H={} has the same proof*) |
148 Goal "[| K : keysFor (parts (insert RB H)); RB : responses evs |] \ |
140 Goal "[| K \\<in> keysFor (parts (insert RB H)); RB \\<in> responses evs |] \ |
149 \ ==> K : range shrK | K : keysFor (parts H)"; |
141 \ ==> K \\<in> range shrK | K \\<in> keysFor (parts H)"; |
150 by (etac rev_mp 1); |
142 by (etac rev_mp 1); |
151 by (etac responses.induct 1); |
143 by (etac responses.induct 1); |
152 by Auto_tac; |
144 by Auto_tac; |
153 qed_spec_mp "Key_in_keysFor_parts"; |
145 qed_spec_mp "Key_in_keysFor_parts"; |
154 |
146 |
155 |
147 |
156 Goal "evs : recur ==> Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
148 Goal "evs \\<in> recur ==> Key K \\<notin> used evs --> K \\<notin> keysFor (parts (spies evs))"; |
157 by (parts_induct_tac 1); |
149 by (parts_induct_tac 1); |
158 (*RA3*) |
150 (*RA3*) |
159 by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); |
151 by (blast_tac (claset() addSDs [Key_in_keysFor_parts]) 2); |
160 (*Fake*) |
152 (*Fake*) |
161 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
153 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
162 qed_spec_mp "new_keys_not_used"; |
154 qed_spec_mp "new_keys_not_used"; |
163 |
155 Addsimps [new_keys_not_used]; |
164 |
|
165 bind_thm ("new_keys_not_analzd", |
|
166 [analz_subset_parts RS keysFor_mono, |
|
167 new_keys_not_used] MRS contra_subsetD); |
|
168 |
|
169 Addsimps [new_keys_not_used, new_keys_not_analzd]; |
|
170 |
156 |
171 |
157 |
172 |
158 |
173 (*** Proofs involving analz ***) |
159 (*** Proofs involving analz ***) |
174 |
160 |
175 (*For proofs involving analz.*) |
161 (*For proofs involving analz.*) |
176 val analz_spies_tac = |
162 val analz_spies_tac = |
177 dtac RA2_analz_spies 4 THEN |
163 dtac RA2_analz_spies 4 THEN |
178 ftac respond_imp_responses 5 THEN |
164 ftac respond_imp_responses 5 THEN |
179 dtac RA4_analz_spies 6; |
165 dtac RA4_analz_spies 6; |
180 |
166 |
181 |
167 |
182 (** Session keys are not used to encrypt other session keys **) |
168 (** Session keys are not used to encrypt other session keys **) |
183 |
169 |
184 (*Version for "responses" relation. Handles case RA3 in the theorem below. |
170 (*Version for "responses" relation. Handles case RA3 in the theorem below. |
185 Note that it holds for *any* set H (not just "spies evs") |
171 Note that it holds for *any* set H (not just "spies evs") |
186 satisfying the inductive hypothesis.*) |
172 satisfying the inductive hypothesis.*) |
187 Goal "[| RB : responses evs; \ |
173 Goal "[| RB \\<in> responses evs; \ |
188 \ ALL K KK. KK <= - (range shrK) --> \ |
174 \ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \ |
189 \ (Key K : analz (Key`KK Un H)) = \ |
175 \ (Key K \\<in> analz (Key`KK Un H)) = \ |
190 \ (K : KK | Key K : analz H) |] \ |
176 \ (K \\<in> KK | Key K \\<in> analz H) |] \ |
191 \ ==> ALL K KK. KK <= - (range shrK) --> \ |
177 \ ==> \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \ |
192 \ (Key K : analz (insert RB (Key`KK Un H))) = \ |
178 \ (Key K \\<in> analz (insert RB (Key`KK Un H))) = \ |
193 \ (K : KK | Key K : analz (insert RB H))"; |
179 \ (K \\<in> KK | Key K \\<in> analz (insert RB H))"; |
194 by (etac responses.induct 1); |
180 by (etac responses.induct 1); |
195 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
181 by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); |
196 qed "resp_analz_image_freshK_lemma"; |
182 qed "resp_analz_image_freshK_lemma"; |
197 |
183 |
198 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) |
184 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*) |
199 Goal "evs : recur ==> \ |
185 Goal "evs \\<in> recur ==> \ |
200 \ ALL K KK. KK <= - (range shrK) --> \ |
186 \ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \ |
201 \ (Key K : analz (Key`KK Un (spies evs))) = \ |
187 \ (Key K \\<in> analz (Key`KK Un (spies evs))) = \ |
202 \ (K : KK | Key K : analz (spies evs))"; |
188 \ (K \\<in> KK | Key K \\<in> analz (spies evs))"; |
203 by (etac recur.induct 1); |
189 by (etac recur.induct 1); |
204 by analz_spies_tac; |
190 by analz_spies_tac; |
205 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
191 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
206 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
192 by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); |
207 by (ALLGOALS |
193 by (ALLGOALS |
212 val raw_analz_image_freshK = result(); |
198 val raw_analz_image_freshK = result(); |
213 qed_spec_mp "analz_image_freshK"; |
199 qed_spec_mp "analz_image_freshK"; |
214 |
200 |
215 |
201 |
216 (*Instance of the lemma with H replaced by (spies evs): |
202 (*Instance of the lemma with H replaced by (spies evs): |
217 [| RB : responses evs; evs : recur; |] |
203 [| RB \\<in> responses evs; evs \\<in> recur; |] |
218 ==> KK <= - (range shrK) --> |
204 ==> KK \\<subseteq> - (range shrK) --> |
219 Key K : analz (insert RB (Key`KK Un spies evs)) = |
205 Key K \\<in> analz (insert RB (Key`KK Un spies evs)) = |
220 (K : KK | Key K : analz (insert RB (spies evs))) |
206 (K \\<in> KK | Key K \\<in> analz (insert RB (spies evs))) |
221 *) |
207 *) |
222 bind_thm ("resp_analz_image_freshK", |
208 bind_thm ("resp_analz_image_freshK", |
223 raw_analz_image_freshK RSN |
209 raw_analz_image_freshK RSN |
224 (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); |
210 (2, resp_analz_image_freshK_lemma) RS spec RS spec RS mp); |
225 |
211 |
226 Goal "[| evs : recur; KAB ~: range shrK |] ==> \ |
212 Goal "[| evs \\<in> recur; KAB \\<notin> range shrK |] ==> \ |
227 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
213 \ Key K \\<in> analz (insert (Key KAB) (spies evs)) = \ |
228 \ (K = KAB | Key K : analz (spies evs))"; |
214 \ (K = KAB | Key K \\<in> analz (spies evs))"; |
229 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
215 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
230 qed "analz_insert_freshK"; |
216 qed "analz_insert_freshK"; |
231 |
217 |
232 |
218 |
233 (*Everything that's hashed is already in past traffic. *) |
219 (*Everything that's hashed is already in past traffic. *) |
234 Goal "[| Hash {|Key(shrK A), X|} : parts (spies evs); \ |
220 Goal "[| Hash {|Key(shrK A), X|} \\<in> parts (spies evs); \ |
235 \ evs : recur; A ~: bad |] ==> X : parts (spies evs)"; |
221 \ evs \\<in> recur; A \\<notin> bad |] ==> X \\<in> parts (spies evs)"; |
236 by (etac rev_mp 1); |
222 by (etac rev_mp 1); |
237 by (parts_induct_tac 1); |
223 by (parts_induct_tac 1); |
238 (*RA3 requires a further induction*) |
224 (*RA3 requires a further induction*) |
239 by (etac responses.induct 2); |
225 by (etac responses.induct 2); |
240 by (ALLGOALS Asm_simp_tac); |
226 by (ALLGOALS Asm_simp_tac); |
247 This theorem applies to steps RA1 and RA2! |
233 This theorem applies to steps RA1 and RA2! |
248 |
234 |
249 Unicity is not used in other proofs but is desirable in its own right. |
235 Unicity is not used in other proofs but is desirable in its own right. |
250 **) |
236 **) |
251 |
237 |
252 Goal "[| evs : recur; A ~: bad |] \ |
238 Goal |
253 \ ==> EX B' P'. ALL B P. \ |
239 "[| Hash {|Key(shrK A), Agent A, B, NA, P|} \\<in> parts (spies evs); \ |
254 \ Hash {|Key(shrK A), Agent A, B, NA, P|} : parts (spies evs) \ |
240 \ Hash {|Key(shrK A), Agent A, B',NA, P'|} \\<in> parts (spies evs); \ |
255 \ --> B=B' & P=P'"; |
241 \ evs \\<in> recur; A \\<notin> bad |] \ |
|
242 \ ==> B=B' & P=P'"; |
|
243 by (etac rev_mp 1); |
|
244 by (etac rev_mp 1); |
256 by (parts_induct_tac 1); |
245 by (parts_induct_tac 1); |
257 by (Blast_tac 1); |
246 by (Blast_tac 1); |
258 by (etac responses.induct 3); |
247 by (etac responses.induct 3); |
259 by (ALLGOALS (simp_tac (simpset() addsimps [all_conj_distrib]))); |
248 by (Asm_full_simp_tac 4); |
260 by (clarify_tac (claset() addSEs partsEs) 1); |
249 (*RA1,2: creation of new Nonce*) |
261 (*RA1,2: creation of new Nonce. Move assertion into global context*) |
|
262 by (ALLGOALS (expand_case_tac "NA = ?y")); |
|
263 by (REPEAT_FIRST (ares_tac [exI])); |
|
264 by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1)); |
250 by (REPEAT (blast_tac (claset() addSDs [Hash_imp_body]) 1)); |
265 val lemma = result(); |
|
266 |
|
267 Goalw [HPair_def] |
|
268 "[| Hash[Key(shrK A)] {|Agent A, B,NA,P|} : parts (spies evs); \ |
|
269 \ Hash[Key(shrK A)] {|Agent A, B',NA,P'|} : parts (spies evs); \ |
|
270 \ evs : recur; A ~: bad |] \ |
|
271 \ ==> B=B' & P=P'"; |
|
272 by (REPEAT (eresolve_tac partsEs 1)); |
|
273 by (prove_unique_tac lemma 1); |
|
274 qed "unique_NA"; |
251 qed "unique_NA"; |
275 |
252 |
276 |
253 |
277 (*** Lemmas concerning the Server's response |
254 (*** Lemmas concerning the Server's response |
278 (relations "respond" and "responses") |
255 (relations "respond" and "responses") |
279 ***) |
256 ***) |
280 |
257 |
281 Goal "[| RB : responses evs; evs : recur |] \ |
258 Goal "[| RB \\<in> responses evs; evs \\<in> recur |] \ |
282 \ ==> (Key (shrK B) : analz (insert RB (spies evs))) = (B:bad)"; |
259 \ ==> (Key (shrK B) \\<in> analz (insert RB (spies evs))) = (B:bad)"; |
283 by (etac responses.induct 1); |
260 by (etac responses.induct 1); |
284 by (ALLGOALS |
261 by (ALLGOALS |
285 (asm_simp_tac |
262 (asm_simp_tac |
286 (analz_image_freshK_ss addsimps [Spy_analz_shrK, |
263 (analz_image_freshK_ss addsimps [Spy_analz_shrK, |
287 resp_analz_image_freshK]))); |
264 resp_analz_image_freshK]))); |
288 qed "shrK_in_analz_respond"; |
265 qed "shrK_in_analz_respond"; |
289 Addsimps [shrK_in_analz_respond]; |
266 Addsimps [shrK_in_analz_respond]; |
290 |
267 |
291 |
268 |
292 Goal "[| RB : responses evs; \ |
269 Goal "[| RB \\<in> responses evs; \ |
293 \ ALL K KK. KK <= - (range shrK) --> \ |
270 \ \\<forall>K KK. KK \\<subseteq> - (range shrK) --> \ |
294 \ (Key K : analz (Key`KK Un H)) = \ |
271 \ (Key K \\<in> analz (Key`KK Un H)) = \ |
295 \ (K : KK | Key K : analz H) |] \ |
272 \ (K \\<in> KK | Key K \\<in> analz H) |] \ |
296 \ ==> (Key K : analz (insert RB H)) --> \ |
273 \ ==> (Key K \\<in> analz (insert RB H)) --> \ |
297 \ (Key K : parts{RB} | Key K : analz H)"; |
274 \ (Key K \\<in> parts{RB} | Key K \\<in> analz H)"; |
298 by (etac responses.induct 1); |
275 by (etac responses.induct 1); |
299 by (ALLGOALS |
276 by (ALLGOALS |
300 (asm_simp_tac |
277 (asm_simp_tac |
301 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
278 (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma]))); |
302 (*Simplification using two distinct treatments of "image"*) |
279 (*Simplification using two distinct treatments of "image"*) |
308 raw_analz_image_freshK RSN |
285 raw_analz_image_freshK RSN |
309 (2, resp_analz_insert_lemma) RSN(2, rev_mp)); |
286 (2, resp_analz_insert_lemma) RSN(2, rev_mp)); |
310 |
287 |
311 |
288 |
312 (*The last key returned by respond indeed appears in a certificate*) |
289 (*The last key returned by respond indeed appears in a certificate*) |
313 Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \ |
290 Goal "(Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) \\<in> respond evs \ |
314 \ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}"; |
291 \ ==> Crypt (shrK A) {|Key K, B, NA|} \\<in> parts {RA}"; |
315 by (etac respond.elim 1); |
292 by (etac respond.elim 1); |
316 by (ALLGOALS Asm_full_simp_tac); |
293 by (ALLGOALS Asm_full_simp_tac); |
317 qed "respond_certificate"; |
294 qed "respond_certificate"; |
318 |
295 |
319 |
296 (*This unicity proof differs from all the others in the HOL/Auth directory. |
320 Goal "(PB,RB,KXY) : respond evs \ |
297 The conclusion isn't quite unicity but duplicity, in that there are two |
321 \ ==> EX A' B'. ALL A B N. \ |
298 possibilities. Also, the presence of two different matching messages in |
322 \ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \ |
299 the inductive step complicates the case analysis. Unusually for such proofs, |
323 \ --> (A'=A & B'=B) | (A'=B & B'=A)"; |
300 the quantifiers appear to be necessary.*) |
|
301 Goal "(PB,RB,KXY) \\<in> respond evs ==> \ |
|
302 \ \\<forall>A B N. Crypt (shrK A) {|Key K, Agent B, N|} \\<in> parts {RB} --> \ |
|
303 \ (\\<forall>A' B' N'. Crypt (shrK A') {|Key K, Agent B', N'|} \\<in> parts {RB} --> \ |
|
304 \ (A'=A & B'=B) | (A'=B & B'=A))"; |
324 by (etac respond.induct 1); |
305 by (etac respond.induct 1); |
325 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); |
306 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [all_conj_distrib]))); |
326 (*Base case*) |
307 by (blast_tac (claset() addDs [respond_certificate]) 1); |
327 by (Blast_tac 1); |
308 qed_spec_mp "unique_lemma"; |
328 by Safe_tac; |
309 |
329 by (expand_case_tac "K = KBC" 1); |
310 Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} \\<in> parts {RB}; \ |
330 by (dtac respond_Key_in_parts 1); |
311 \ Crypt (shrK A') {|Key K, Agent B', N'|} \\<in> parts {RB}; \ |
331 by (blast_tac (claset() addSIs [exI] |
312 \ (PB,RB,KXY) \\<in> respond evs |] \ |
332 addDs [Key_in_parts_respond]) 1); |
|
333 by (expand_case_tac "K = KAB" 1); |
|
334 by (REPEAT (ares_tac [exI] 2)); |
|
335 by (ex_strip_tac 1); |
|
336 by (dtac respond_certificate 1); |
|
337 by (Blast_tac 1); |
|
338 val lemma = result(); |
|
339 |
|
340 Goal "[| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \ |
|
341 \ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \ |
|
342 \ (PB,RB,KXY) : respond evs |] \ |
|
343 \ ==> (A'=A & B'=B) | (A'=B & B'=A)"; |
313 \ ==> (A'=A & B'=B) | (A'=B & B'=A)"; |
344 by (prove_unique_tac lemma 1); |
314 by (rtac unique_lemma 1); |
|
315 by Auto_tac; |
345 qed "unique_session_keys"; |
316 qed "unique_session_keys"; |
346 |
317 |
347 |
318 |
348 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3 |
319 (** Crucial secrecy property: Spy does not see the keys sent in msg RA3 |
349 Does not in itself guarantee security: an attack could violate |
320 Does not in itself guarantee security: an attack could violate |
350 the premises, e.g. by having A=Spy **) |
321 the premises, e.g. by having A=Spy **) |
351 |
322 |
352 Goal "[| (PB,RB,KAB) : respond evs; evs : recur |] \ |
323 Goal "[| (PB,RB,KAB) \\<in> respond evs; evs \\<in> recur |] \ |
353 \ ==> ALL A A' N. A ~: bad & A' ~: bad --> \ |
324 \ ==> \\<forall>A A' N. A \\<notin> bad & A' \\<notin> bad --> \ |
354 \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ |
325 \ Crypt (shrK A) {|Key K, Agent A', N|} \\<in> parts{RB} --> \ |
355 \ Key K ~: analz (insert RB (spies evs))"; |
326 \ Key K \\<notin> analz (insert RB (spies evs))"; |
356 by (etac respond.induct 1); |
327 by (etac respond.induct 1); |
357 by (ftac respond_imp_responses 2); |
328 by (ftac respond_imp_responses 2); |
358 by (ftac respond_imp_not_used 2); |
329 by (ftac respond_imp_not_used 2); |
359 by (ALLGOALS (*6 seconds*) |
330 by (ALLGOALS (*6 seconds*) |
360 (asm_simp_tac |
331 (asm_simp_tac |
365 by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); |
336 by (ALLGOALS (simp_tac (simpset() addsimps [ex_disj_distrib]))); |
366 (** LEVEL 5 **) |
337 (** LEVEL 5 **) |
367 by (Blast_tac 1); |
338 by (Blast_tac 1); |
368 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); |
339 by (REPEAT_FIRST (resolve_tac [allI, conjI, impI])); |
369 by (ALLGOALS Clarify_tac); |
340 by (ALLGOALS Clarify_tac); |
370 by (blast_tac (claset() addSDs [resp_analz_insert] |
341 by (blast_tac (claset() addSDs [resp_analz_insert]) 3); |
371 addIs [impOfSubs analz_subset_parts]) 3); |
|
372 by (blast_tac (claset() addSDs [respond_certificate]) 2); |
342 by (blast_tac (claset() addSDs [respond_certificate]) 2); |
373 by (Asm_full_simp_tac 1); |
343 by (Asm_full_simp_tac 1); |
374 (*by unicity, either B=Aa or B=A', a contradiction if B: bad*) |
344 (*by unicity, either B=Aa or B=A', a contradiction if B \\<in> bad*) |
375 by (blast_tac |
345 by (blast_tac |
376 (claset() addSEs [MPair_parts] |
346 (claset() addSEs [MPair_parts] |
377 addDs [parts.Body, |
347 addDs [parts.Body, |
378 respond_certificate RSN (2, unique_session_keys)]) 1); |
348 respond_certificate RSN (2, unique_session_keys)]) 1); |
379 qed_spec_mp "respond_Spy_not_see_session_key"; |
349 qed_spec_mp "respond_Spy_not_see_session_key"; |
380 |
350 |
381 |
351 |
382 Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} : parts (spies evs); \ |
352 Goal "[| Crypt (shrK A) {|Key K, Agent A', N|} \\<in> parts (spies evs); \ |
383 \ A ~: bad; A' ~: bad; evs : recur |] \ |
353 \ A \\<notin> bad; A' \\<notin> bad; evs \\<in> recur |] \ |
384 \ ==> Key K ~: analz (spies evs)"; |
354 \ ==> Key K \\<notin> analz (spies evs)"; |
385 by (etac rev_mp 1); |
355 by (etac rev_mp 1); |
386 by (etac recur.induct 1); |
356 by (etac recur.induct 1); |
387 by analz_spies_tac; |
357 by analz_spies_tac; |
388 by (ALLGOALS |
358 by (ALLGOALS |
389 (asm_simp_tac |
359 (asm_simp_tac |
390 (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK]))); |
360 (simpset() addsimps split_ifs @ [analz_insert_eq, analz_insert_freshK]))); |
391 (*RA4*) |
361 (*RA4*) |
392 by (spy_analz_tac 5); |
362 by (Blast_tac 5); |
393 (*RA2*) |
363 (*RA2*) |
394 by (spy_analz_tac 3); |
364 by (Blast_tac 3); |
395 (*Fake*) |
365 (*Fake*) |
396 by (spy_analz_tac 2); |
366 by (spy_analz_tac 2); |
397 (*Base*) |
367 (*Base*) |
398 by (Force_tac 1); |
368 by (Force_tac 1); |
399 (*RA3 remains*) |
369 (*RA3 remains*) |
409 qed "Spy_not_see_session_key"; |
379 qed "Spy_not_see_session_key"; |
410 |
380 |
411 (**** Authenticity properties for Agents ****) |
381 (**** Authenticity properties for Agents ****) |
412 |
382 |
413 (*The response never contains Hashes*) |
383 (*The response never contains Hashes*) |
414 Goal "[| Hash {|Key (shrK B), M|} : parts (insert RB H); \ |
384 Goal "[| Hash {|Key (shrK B), M|} \\<in> parts (insert RB H); \ |
415 \ (PB,RB,K) : respond evs |] \ |
385 \ (PB,RB,K) \\<in> respond evs |] \ |
416 \ ==> Hash {|Key (shrK B), M|} : parts H"; |
386 \ ==> Hash {|Key (shrK B), M|} \\<in> parts H"; |
417 by (etac rev_mp 1); |
387 by (etac rev_mp 1); |
418 by (etac (respond_imp_responses RS responses.induct) 1); |
388 by (etac (respond_imp_responses RS responses.induct) 1); |
419 by Auto_tac; |
389 by Auto_tac; |
420 qed "Hash_in_parts_respond"; |
390 qed "Hash_in_parts_respond"; |
421 |
391 |
422 (*Only RA1 or RA2 can have caused such a part of a message to appear. |
392 (*Only RA1 or RA2 can have caused such a part of a message to appear. |
423 This result is of no use to B, who cannot verify the Hash. Moreover, |
393 This result is of no use to B, who cannot verify the Hash. Moreover, |
424 it can say nothing about how recent A's message is. It might later be |
394 it can say nothing about how recent A's message is. It might later be |
425 used to prove B's presence to A at the run's conclusion.*) |
395 used to prove B's presence to A at the run's conclusion.*) |
426 Goalw [HPair_def] |
396 Goalw [HPair_def] |
427 "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} : parts(spies evs); \ |
397 "[| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \\<in> parts(spies evs); \ |
428 \ A ~: bad; evs : recur |] \ |
398 \ A \\<notin> bad; evs \\<in> recur |] \ |
429 \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) : set evs"; |
399 \ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \\<in> set evs"; |
430 by (etac rev_mp 1); |
400 by (etac rev_mp 1); |
431 by (parts_induct_tac 1); |
401 by (parts_induct_tac 1); |
432 by (Blast_tac 1); |
402 by (Blast_tac 1); |
433 (*RA3*) |
403 (*RA3*) |
434 by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1); |
404 by (blast_tac (claset() addSDs [Hash_in_parts_respond]) 1); |