96 \<in> set evs" |
96 \<in> set evs" |
97 apply (intro exI bexI) |
97 apply (intro exI bexI) |
98 apply (rule_tac [2] otway.Nil |
98 apply (rule_tac [2] otway.Nil |
99 [THEN otway.OR1, THEN otway.Reception, |
99 [THEN otway.OR1, THEN otway.Reception, |
100 THEN otway.OR2, THEN otway.Reception, |
100 THEN otway.OR2, THEN otway.Reception, |
101 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
101 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility) |
102 apply possibility |
|
103 done |
102 done |
104 |
103 |
105 lemma Gets_imp_Says [dest!]: |
104 lemma Gets_imp_Says [dest!]: |
106 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
105 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
107 apply (erule rev_mp) |
106 apply (erule rev_mp) |
108 apply (erule otway.induct) |
107 apply (erule otway.induct, auto) |
109 apply auto |
|
110 done |
108 done |
111 |
109 |
112 |
110 |
113 (**** Inductive proofs about otway ****) |
111 (**** Inductive proofs about otway ****) |
114 |
112 |
139 |
137 |
140 (*Spy never sees a good agent's shared key!*) |
138 (*Spy never sees a good agent's shared key!*) |
141 lemma Spy_see_shrK [simp]: |
139 lemma Spy_see_shrK [simp]: |
142 "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
140 "evs \<in> otway ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" |
143 apply (erule otway.induct, force, |
141 apply (erule otway.induct, force, |
144 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
142 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
145 apply blast+ |
|
146 done |
143 done |
147 |
144 |
148 lemma Spy_analz_shrK [simp]: |
145 lemma Spy_analz_shrK [simp]: |
149 "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
146 "evs \<in> otway ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" |
150 by auto |
147 by auto |
160 for Oops case.*) |
157 for Oops case.*) |
161 lemma Says_Server_message_form: |
158 lemma Says_Server_message_form: |
162 "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
159 "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} \<in> set evs; |
163 evs \<in> otway |] |
160 evs \<in> otway |] |
164 ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
161 ==> K \<notin> range shrK & (\<exists>i. NA = Nonce i) & (\<exists>j. NB = Nonce j)" |
165 apply (erule rev_mp, erule otway.induct, simp_all) |
162 apply (erule rev_mp, erule otway.induct, simp_all, blast) |
166 apply blast |
|
167 done |
163 done |
168 |
164 |
169 |
165 |
170 (**** |
166 (**** |
171 The following is to prove theorems of the form |
167 The following is to prove theorems of the form |
186 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
182 (Key K \<in> analz (Key`KK Un (knows Spy evs))) = |
187 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
183 (K \<in> KK | Key K \<in> analz (knows Spy evs))" |
188 apply (erule otway.induct, force) |
184 apply (erule otway.induct, force) |
189 apply (frule_tac [7] Says_Server_message_form) |
185 apply (frule_tac [7] Says_Server_message_form) |
190 apply (drule_tac [6] OR4_analz_knows_Spy) |
186 apply (drule_tac [6] OR4_analz_knows_Spy) |
191 apply (drule_tac [4] OR2_analz_knows_Spy) |
187 apply (drule_tac [4] OR2_analz_knows_Spy, analz_freshK, spy_analz) |
192 apply analz_freshK |
|
193 apply spy_analz |
|
194 done |
188 done |
195 |
189 |
196 |
190 |
197 lemma analz_insert_freshK: |
191 lemma analz_insert_freshK: |
198 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
192 "[| evs \<in> otway; KAB \<notin> range shrK |] ==> |
223 ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) --> |
217 ==> Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs) --> |
224 Says A B {|NA, Agent A, Agent B, |
218 Says A B {|NA, Agent A, Agent B, |
225 Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
219 Crypt (shrK A) {|NA, Agent A, Agent B|}|} |
226 \<in> set evs" |
220 \<in> set evs" |
227 apply (erule otway.induct, force, |
221 apply (erule otway.induct, force, |
228 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
222 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
229 apply blast+ |
|
230 done |
223 done |
231 |
224 |
232 lemma Crypt_imp_OR1_Gets: |
225 lemma Crypt_imp_OR1_Gets: |
233 "[| Gets B {|NA, Agent A, Agent B, |
226 "[| Gets B {|NA, Agent A, Agent B, |
234 Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
227 Crypt (shrK A) {|NA, Agent A, Agent B|}|} \<in> set evs; |
246 Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs); |
239 Crypt (shrK A) {|NA, Agent A, Agent C|} \<in> parts (knows Spy evs); |
247 evs \<in> otway; A \<notin> bad |] |
240 evs \<in> otway; A \<notin> bad |] |
248 ==> B = C" |
241 ==> B = C" |
249 apply (erule rev_mp, erule rev_mp) |
242 apply (erule rev_mp, erule rev_mp) |
250 apply (erule otway.induct, force, |
243 apply (erule otway.induct, force, |
251 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
244 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
252 apply blast+ |
|
253 done |
245 done |
254 |
246 |
255 |
247 |
256 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
248 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
257 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
249 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
260 "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs); |
252 "[| Crypt (shrK A) {|NA, Agent A, Agent B|} \<in> parts (knows Spy evs); |
261 A \<notin> bad; evs \<in> otway |] |
253 A \<notin> bad; evs \<in> otway |] |
262 ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)" |
254 ==> Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \<notin> parts (knows Spy evs)" |
263 apply (erule rev_mp) |
255 apply (erule rev_mp) |
264 apply (erule otway.induct, force, |
256 apply (erule otway.induct, force, |
265 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
257 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
266 apply blast+ |
|
267 done |
258 done |
268 |
259 |
269 (*Crucial property: If the encrypted message appears, and A has used NA |
260 (*Crucial property: If the encrypted message appears, and A has used NA |
270 to start a run, then it originated with the Server!*) |
261 to start a run, then it originated with the Server!*) |
271 lemma NA_Crypt_imp_Server_msg [rule_format]: |
262 lemma NA_Crypt_imp_Server_msg [rule_format]: |
276 --> (\<exists>NB. Says Server B |
267 --> (\<exists>NB. Says Server B |
277 {|NA, |
268 {|NA, |
278 Crypt (shrK A) {|NA, Key K|}, |
269 Crypt (shrK A) {|NA, Key K|}, |
279 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)" |
270 Crypt (shrK B) {|NB, Key K|}|} \<in> set evs)" |
280 apply (erule otway.induct, force, |
271 apply (erule otway.induct, force, |
281 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
272 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) |
282 apply blast |
|
283 (*OR1: it cannot be a new Nonce, contradiction.*) |
273 (*OR1: it cannot be a new Nonce, contradiction.*) |
284 apply blast |
274 apply blast |
285 (*OR3*) |
275 (*OR3*) |
286 apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) |
276 apply (blast dest!: no_nonce_OR1_OR2 intro: unique_NA) |
287 (*OR4*) |
277 (*OR4*) |
319 Key K \<notin> analz (knows Spy evs)" |
309 Key K \<notin> analz (knows Spy evs)" |
320 apply (erule otway.induct, force) |
310 apply (erule otway.induct, force) |
321 apply (frule_tac [7] Says_Server_message_form) |
311 apply (frule_tac [7] Says_Server_message_form) |
322 apply (drule_tac [6] OR4_analz_knows_Spy) |
312 apply (drule_tac [6] OR4_analz_knows_Spy) |
323 apply (drule_tac [4] OR2_analz_knows_Spy) |
313 apply (drule_tac [4] OR2_analz_knows_Spy) |
324 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes) |
314 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes, spy_analz) (*Fake*) |
325 apply spy_analz (*Fake*) |
|
326 (*OR3, OR4, Oops*) |
315 (*OR3, OR4, Oops*) |
327 apply (blast dest: unique_session_keys)+ |
316 apply (blast dest: unique_session_keys)+ |
328 done |
317 done |
329 |
318 |
330 lemma Spy_not_see_encrypted_key: |
319 lemma Spy_not_see_encrypted_key: |
361 {|NA, Agent A, Agent B, X, |
350 {|NA, Agent A, Agent B, X, |
362 Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} |
351 Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} |
363 \<in> set evs" |
352 \<in> set evs" |
364 apply (erule rev_mp) |
353 apply (erule rev_mp) |
365 apply (erule otway.induct, force, |
354 apply (erule otway.induct, force, |
366 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
355 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast+) |
367 apply blast+ |
|
368 done |
356 done |
369 |
357 |
370 |
358 |
371 (** The Nonce NB uniquely identifies B's message. **) |
359 (** The Nonce NB uniquely identifies B's message. **) |
372 |
360 |
395 {|NA, Crypt (shrK A) {|NA, Key K|}, |
383 {|NA, Crypt (shrK A) {|NA, Key K|}, |
396 Crypt (shrK B) {|NB, Key K|}|} |
384 Crypt (shrK B) {|NB, Key K|}|} |
397 \<in> set evs)" |
385 \<in> set evs)" |
398 apply simp |
386 apply simp |
399 apply (erule otway.induct, force, |
387 apply (erule otway.induct, force, |
400 drule_tac [4] OR2_parts_knows_Spy, simp_all) |
388 drule_tac [4] OR2_parts_knows_Spy, simp_all, blast) |
401 apply blast |
|
402 (*OR1: it cannot be a new Nonce, contradiction.*) |
389 (*OR1: it cannot be a new Nonce, contradiction.*) |
403 (*OR2*) |
390 (*OR2*) |
404 apply blast |
391 apply blast |
405 (*OR3: needs elim: MPair_parts or it takes forever!*) |
392 (*OR3: needs elim: MPair_parts or it takes forever!*) |
406 apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) |
393 apply (blast dest: unique_NB dest!: no_nonce_OR1_OR2) |