1236 prefer 2 |
1236 prefer 2 |
1237 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) |
1237 apply (blast dest: Says_Kas_message_form Says_Tgs_message_form intro: less_SucI) |
1238 txt{*K5. Not clear how this step could be integrated with the main |
1238 txt{*K5. Not clear how this step could be integrated with the main |
1239 simplification step. Done in KerberosV.thy*} |
1239 simplification step. Done in KerberosV.thy*} |
1240 apply clarify |
1240 apply clarify |
1241 apply (erule_tac V = "Says Aa Tgs ?X \<in> set ?evs" in thin_rl) |
1241 apply (erule_tac V = "Says Aa Tgs X \<in> set evs" for X evs in thin_rl) |
1242 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD]) |
1242 apply (frule Gets_imp_knows_Spy [THEN parts.Inj, THEN servK_notin_authKeysD]) |
1243 apply (assumption, assumption, blast, assumption) |
1243 apply (assumption, assumption, blast, assumption) |
1244 apply (simp add: analz_insert_freshK2) |
1244 apply (simp add: analz_insert_freshK2) |
1245 by (blast dest: Says_imp_spies [THEN parts.Inj] Key_unique_SesKey intro: less_SucI) |
1245 apply (blast dest: Key_unique_SesKey intro: less_SucI) |
|
1246 done |
1246 |
1247 |
1247 |
1248 |
1248 text{* In the real world Tgs can't check wheter authK is secure! *} |
1249 text{* In the real world Tgs can't check wheter authK is secure! *} |
1249 lemma Confidentiality_Tgs: |
1250 lemma Confidentiality_Tgs: |
1250 "\<lbrakk> Says Tgs A |
1251 "\<lbrakk> Says Tgs A |