equal
deleted
inserted
replaced
101 theorem Spy_not_see_NA: |
101 theorem Spy_not_see_NA: |
102 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
102 "\<lbrakk>Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
103 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
103 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
104 \<Longrightarrow> Nonce NA \<notin> analz (spies evs)" |
104 \<Longrightarrow> Nonce NA \<notin> analz (spies evs)" |
105 apply (erule rev_mp) |
105 apply (erule rev_mp) |
106 apply (erule ns_public.induct, simp_all) |
106 apply (erule ns_public.induct, simp_all, spy_analz) |
107 apply spy_analz |
|
108 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
107 apply (blast dest: unique_NA intro: no_nonce_NS1_NS2)+ |
109 done |
108 done |
110 |
109 |
111 |
110 |
112 (*Authentication for A: if she receives message 2 and has used NA |
111 (*Authentication for A: if she receives message 2 and has used NA |
164 theorem Spy_not_see_NB [dest]: |
163 theorem Spy_not_see_NB [dest]: |
165 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
164 "\<lbrakk>Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>) \<in> set evs; |
166 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
165 A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
167 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
166 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
168 apply (erule rev_mp) |
167 apply (erule rev_mp) |
169 apply (erule ns_public.induct, simp_all) |
168 apply (erule ns_public.induct, simp_all, spy_analz) |
170 apply spy_analz |
|
171 apply (blast intro: no_nonce_NS1_NS2)+ |
169 apply (blast intro: no_nonce_NS1_NS2)+ |
172 done |
170 done |
173 |
171 |
174 |
172 |
175 (*Authentication for B: if he receives message 3 and has used NB |
173 (*Authentication for B: if he receives message 3 and has used NB |