equal
deleted
inserted
replaced
156 apply (drule no_Nonce_NS1_NS2, auto) |
156 apply (drule no_Nonce_NS1_NS2, auto) |
157 (* NS3 *) |
157 (* NS3 *) |
158 apply (case_tac "NBa=NB", clarify) |
158 apply (case_tac "NBa=NB", clarify) |
159 apply (drule Guard_Nonce_analz, simp+) |
159 apply (drule Guard_Nonce_analz, simp+) |
160 apply (drule Says_imp_knows_Spy)+ |
160 apply (drule Says_imp_knows_Spy)+ |
161 by (drule_tac A=Aa and A'=A in NB_is_uniq, auto) |
161 apply (drule_tac A=Aa and A'=A in NB_is_uniq) |
|
162 apply auto[1] |
|
163 apply (auto simp add: guard.No_Nonce) |
|
164 done |
162 |
165 |
163 subsection{*Agents' Authentication*} |
166 subsection{*Agents' Authentication*} |
164 |
167 |
165 lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==> |
168 lemma B_trusts_NS1: "[| evs:nsp; A ~:bad; B ~:bad |] ==> |
166 Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) |
169 Crypt (pubK B) {|Nonce NA, Agent A|}:parts (spies evs) |