equal
deleted
inserted
replaced
50 |
50 |
51 (*A "possibility property": there are traces that reach the end*) |
51 (*A "possibility property": there are traces that reach the end*) |
52 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" |
52 lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" |
53 apply (intro exI bexI) |
53 apply (intro exI bexI) |
54 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |
54 apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, |
55 THEN ns_public.NS3]) |
55 THEN ns_public.NS3], possibility) |
56 apply possibility |
|
57 done |
56 done |
58 |
57 |
59 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
58 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
60 sends messages containing X! **) |
59 sends messages containing X! **) |
61 |
60 |