41 "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] |
41 "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] |
42 ==> Says Spy B X # evsf \<in> certified_mail" |
42 ==> Says Spy B X # evsf \<in> certified_mail" |
43 |
43 |
44 | FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent |
44 | FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent |
45 equipped with the necessary credentials to serve as an SSL server.*} |
45 equipped with the necessary credentials to serve as an SSL server.*} |
46 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|] |
46 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|] |
47 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail" |
47 ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail" |
48 |
48 |
49 | CM1: --{*The sender approaches the recipient. The message is a number.*} |
49 | CM1: --{*The sender approaches the recipient. The message is a number.*} |
50 "[|evs1 \<in> certified_mail; |
50 "[|evs1 \<in> certified_mail; |
51 Key K \<notin> used evs1; |
51 Key K \<notin> used evs1; |
52 K \<in> symKeys; |
52 K \<in> symKeys; |
53 Nonce q \<notin> used evs1; |
53 Nonce q \<notin> used evs1; |
54 hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|}; |
54 hs = Hash{|Number cleartext, Nonce q, response S R q, Crypt K (Number m)|}; |
55 S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|] |
55 S2TTP = Crypt(pubEK TTP) {|Agent S, Number BothAuth, Key K, Agent R, hs|}|] |
56 ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, |
56 ==> Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number BothAuth, |
57 Number cleartext, Nonce q, S2TTP|} # evs1 |
57 Number cleartext, Nonce q, S2TTP|} # evs1 |
58 \<in> certified_mail" |
58 \<in> certified_mail" |
59 |
59 |
60 | CM2: --{*The recipient records @{term S2TTP} while transmitting it and her |
60 | CM2: --{*The recipient records @{term S2TTP} while transmitting it and her |
61 password to @{term TTP} over an SSL channel.*} |
61 password to @{term TTP} over an SSL channel.*} |
62 "[|evs2 \<in> certified_mail; |
62 "[|evs2 \<in> certified_mail; |
63 Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, |
63 Gets R {|Agent S, Agent TTP, em, Number BothAuth, Number cleartext, |
64 Nonce q, S2TTP|} \<in> set evs2; |
64 Nonce q, S2TTP|} \<in> set evs2; |
65 TTP \<noteq> R; |
65 TTP \<noteq> R; |
66 hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |] |
66 hr = Hash {|Number cleartext, Nonce q, response S R q, em|} |] |
67 ==> |
67 ==> |
68 Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2 |
68 Notes TTP {|Agent R, Agent TTP, S2TTP, Key(RPwd R), hr|} # evs2 |
69 \<in> certified_mail" |
69 \<in> certified_mail" |
287 isn't inductive: message 3 case can't be proved *) |
287 isn't inductive: message 3 case can't be proved *) |
288 lemma S2TTP_sender_lemma [rule_format]: |
288 lemma S2TTP_sender_lemma [rule_format]: |
289 "evs \<in> certified_mail ==> |
289 "evs \<in> certified_mail ==> |
290 Key K \<notin> analz (spies evs) --> |
290 Key K \<notin> analz (spies evs) --> |
291 (\<forall>AO. Crypt (pubEK TTP) |
291 (\<forall>AO. Crypt (pubEK TTP) |
292 {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs --> |
292 {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs --> |
293 (\<exists>m ctxt q. |
293 (\<exists>m ctxt q. |
294 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
294 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
295 Says S R |
295 Says S R |
296 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
296 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
297 Number ctxt, Nonce q, |
297 Number ctxt, Nonce q, |
298 Crypt (pubEK TTP) |
298 Crypt (pubEK TTP) |
299 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" |
299 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs))" |
300 apply (erule certified_mail.induct, analz_mono_contra) |
300 apply (erule certified_mail.induct, analz_mono_contra) |
301 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp) |
301 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp) |
302 apply (simp add: used_Nil Crypt_notin_initState, simp_all) |
302 apply (simp add: used_Nil Crypt_notin_initState, simp_all) |
303 txt{*Fake*} |
303 txt{*Fake*} |
304 apply (blast dest: Fake_parts_sing [THEN subsetD] |
304 apply (blast dest: Fake_parts_sing [THEN subsetD] |
320 "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs; |
320 "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs; |
321 Key K \<notin> analz (spies evs); |
321 Key K \<notin> analz (spies evs); |
322 evs \<in> certified_mail|] |
322 evs \<in> certified_mail|] |
323 ==> \<exists>m ctxt q. |
323 ==> \<exists>m ctxt q. |
324 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
324 hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} & |
325 Says S R |
325 Says S R |
326 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
326 {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
327 Number ctxt, Nonce q, |
327 Number ctxt, Nonce q, |
328 Crypt (pubEK TTP) |
328 Crypt (pubEK TTP) |
329 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" |
329 {|Agent S, Number AO, Key K, Agent R, hs |}|} \<in> set evs" |
330 by (blast intro: S2TTP_sender_lemma) |
330 by (blast intro: S2TTP_sender_lemma) |
331 |
331 |
332 |
332 |
333 text{*Nobody can have used non-existent keys!*} |
333 text{*Nobody can have used non-existent keys!*} |
334 lemma new_keys_not_used [simp]: |
334 lemma new_keys_not_used [simp]: |
399 theorem S_fairness_bad_R: |
399 theorem S_fairness_bad_R: |
400 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
400 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
401 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
401 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
402 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
402 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
403 Key K \<in> analz (spies evs); |
403 Key K \<in> analz (spies evs); |
404 evs \<in> certified_mail; |
404 evs \<in> certified_mail; |
405 S\<noteq>Spy|] |
405 S\<noteq>Spy|] |
406 ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" |
406 ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" |
407 apply (erule rev_mp) |
407 apply (erule rev_mp) |
408 apply (erule ssubst) |
408 apply (erule ssubst) |
409 apply (erule rev_mp) |
409 apply (erule rev_mp) |
426 text{*Confidentially for the symmetric key*} |
426 text{*Confidentially for the symmetric key*} |
427 theorem Spy_not_see_encrypted_key: |
427 theorem Spy_not_see_encrypted_key: |
428 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
428 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
429 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
429 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
430 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
430 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
431 evs \<in> certified_mail; |
431 evs \<in> certified_mail; |
432 S\<noteq>Spy; R \<notin> bad|] |
432 S\<noteq>Spy; R \<notin> bad|] |
433 ==> Key K \<notin> analz(spies evs)" |
433 ==> Key K \<notin> analz(spies evs)" |
434 by (blast dest: S_fairness_bad_R) |
434 by (blast dest: S_fairness_bad_R) |
435 |
435 |
436 |
436 |
437 text{*Agent @{term R}, who may be the Spy, doesn't receive the key |
437 text{*Agent @{term R}, who may be the Spy, doesn't receive the key |
438 until @{term S} has access to the return receipt.*} |
438 until @{term S} has access to the return receipt.*} |
439 theorem S_guarantee: |
439 theorem S_guarantee: |
440 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
440 "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, |
441 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
441 Number cleartext, Nonce q, S2TTP|} \<in> set evs; |
442 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
442 S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|}; |
443 Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs; |
443 Notes R {|Agent TTP, Agent R, Key K, hs|} \<in> set evs; |
444 S\<noteq>Spy; evs \<in> certified_mail|] |
444 S\<noteq>Spy; evs \<in> certified_mail|] |
445 ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" |
445 ==> Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs" |
446 apply (erule rev_mp) |
446 apply (erule rev_mp) |
447 apply (erule ssubst) |
447 apply (erule ssubst) |
448 apply (erule rev_mp) |
448 apply (erule rev_mp) |
449 apply (erule certified_mail.induct, simp_all) |
449 apply (erule certified_mail.induct, simp_all) |