equal
deleted
inserted
replaced
90 |
90 |
91 (*<*) |
91 (*<*) |
92 declare knows_Spy_partsEs [elim] |
92 declare knows_Spy_partsEs [elim] |
93 declare analz_subset_parts [THEN subsetD, dest] |
93 declare analz_subset_parts [THEN subsetD, dest] |
94 declare Fake_parts_insert [THEN subsetD, dest] |
94 declare Fake_parts_insert [THEN subsetD, dest] |
95 declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
|
96 |
95 |
97 (*A "possibility property": there are traces that reach the end*) |
96 (*A "possibility property": there are traces that reach the end*) |
98 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
97 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set evs" |
99 apply (intro exI bexI) |
98 apply (intro exI bexI) |
100 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |
99 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |