104 theorem Spy_not_see_NA: |
104 theorem Spy_not_see_NA: |
105 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
105 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
106 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
106 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
107 \<Longrightarrow> Nonce NA \<notin> analz (spies evs)" |
107 \<Longrightarrow> Nonce NA \<notin> analz (spies evs)" |
108 apply (erule rev_mp) |
108 apply (erule rev_mp) |
109 apply (erule ns_public.induct, simp_all) |
109 apply (erule ns_public.induct, simp_all, spy_analz) |
110 apply spy_analz |
|
111 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
110 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
112 done |
111 done |
113 |
112 |
114 |
113 |
115 (*Authentication for A: if she receives message 2 and has used NA |
114 (*Authentication for A: if she receives message 2 and has used NA |
165 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
164 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
166 \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs; |
165 \<forall>C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set evs; |
167 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
166 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
168 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
167 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
169 apply (erule rev_mp, erule rev_mp) |
168 apply (erule rev_mp, erule rev_mp) |
170 apply (erule ns_public.induct, simp_all) |
169 apply (erule ns_public.induct, simp_all, spy_analz) |
171 apply spy_analz |
|
172 apply (simp_all add: all_conj_distrib) (*speeds up the next step*) |
170 apply (simp_all add: all_conj_distrib) (*speeds up the next step*) |
173 apply (blast intro: no_nonce_NS1_NS2)+ |
171 apply (blast intro: no_nonce_NS1_NS2)+ |
174 done |
172 done |
175 |
173 |
176 |
174 |
195 |
193 |
196 (*Can we strengthen the secrecy theorem Spy_not_see_NB? NO*) |
194 (*Can we strengthen the secrecy theorem Spy_not_see_NB? NO*) |
197 lemma "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
195 lemma "\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
198 \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs |
196 \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs |
199 \<longrightarrow> Nonce NB \<notin> analz (spies evs)" |
197 \<longrightarrow> Nonce NB \<notin> analz (spies evs)" |
200 apply (erule ns_public.induct, simp_all) |
198 apply (erule ns_public.induct, simp_all, spy_analz) |
201 apply spy_analz |
|
202 (*NS1: by freshness*) |
199 (*NS1: by freshness*) |
203 apply blast |
200 apply blast |
204 (*NS2: by freshness and unicity of NB*) |
201 (*NS2: by freshness and unicity of NB*) |
205 apply (blast intro: no_nonce_NS1_NS2) |
202 apply (blast intro: no_nonce_NS1_NS2) |
206 (*NS3: unicity of NB identifies A and NA, but not B*) |
203 (*NS3: unicity of NB identifies A and NA, but not B*) |
207 apply clarify |
204 apply clarify |
208 apply (frule_tac A' = "A" in |
205 apply (frule_tac A' = A in |
209 Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB]) |
206 Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto) |
210 apply auto |
|
211 apply (rename_tac C B' evs3) |
207 apply (rename_tac C B' evs3) |
212 oops |
208 oops |
213 |
209 |
214 (* |
210 (* |
215 THIS IS THE ATTACK! |
211 THIS IS THE ATTACK! |