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