55 |
55 |
56 lemma |
56 lemma |
57 assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" |
57 assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" |
58 assumes "evs = |
58 assumes "evs = |
59 [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), |
59 [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), |
60 Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), |
60 Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>), |
61 Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), |
61 Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>), |
62 Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") |
62 Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>)]" (is "_ = [?e3, ?e2, ?e1, ?e0]") |
63 shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" |
63 shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" |
64 proof - |
64 proof - |
65 from assms show "A \<noteq> Spy" by auto |
65 from assms show "A \<noteq> Spy" by auto |
66 from assms show "B \<noteq> Spy" by auto |
66 from assms show "B \<noteq> Spy" by auto |
67 have "[] : ns_public" by (rule Nil) |
67 have "[] : ns_public" by (rule Nil) |
69 proof (rule NS1) |
69 proof (rule NS1) |
70 show "Nonce 0 ~: used []" by eval |
70 show "Nonce 0 ~: used []" by eval |
71 qed |
71 qed |
72 then have "[?e1, ?e0] : ns_public" |
72 then have "[?e1, ?e0] : ns_public" |
73 proof (rule Fake) |
73 proof (rule Fake) |
74 show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))" |
74 show "Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace> : synth (analz (knows Spy [?e0]))" |
75 by (intro synth.intros(2,3,4,1)) eval+ |
75 by (intro synth.intros(2,3,4,1)) eval+ |
76 qed |
76 qed |
77 then have "[?e2, ?e1, ?e0] : ns_public" |
77 then have "[?e2, ?e1, ?e0] : ns_public" |
78 proof (rule NS2) |
78 proof (rule NS2) |
79 show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp |
79 show "Says Spy Bob (Crypt (pubEK Bob) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e1, ?e0]" by simp |
80 show " Nonce 1 ~: used [?e1, ?e0]" by eval |
80 show " Nonce 1 ~: used [?e1, ?e0]" by eval |
81 qed |
81 qed |
82 then show "evs : ns_public" |
82 then show "evs : ns_public" |
83 unfolding assms |
83 unfolding assms |
84 proof (rule NS3) |
84 proof (rule NS3) |
85 show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp |
85 show " Says Alice Spy (Crypt (pubEK Spy) \<lbrace>Nonce 0, Agent Alice\<rbrace>) \<in> set [?e2, ?e1, ?e0]" by simp |
86 show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp |
86 show "Says Bob Alice (Crypt (pubEK Alice) \<lbrace>Nonce 0, Nonce 1\<rbrace>) : set [?e2, ?e1, ?e0]" by simp |
87 qed |
87 qed |
88 from assms show "Nonce NB : analz (knows Spy evs)" |
88 from assms show "Nonce NB : analz (knows Spy evs)" |
89 apply simp |
89 apply simp |
90 apply (rule analz.intros(4)) |
90 apply (rule analz.intros(4)) |
91 apply (rule analz.intros(1)) |
91 apply (rule analz.intros(1)) |