80 declare analz_into_parts [dest] |
80 declare analz_into_parts [dest] |
81 declare Fake_parts_insert_in_Un [dest] |
81 declare Fake_parts_insert_in_Un [dest] |
82 |
82 |
83 |
83 |
84 (*A "possibility property": there are traces that reach the end*) |
84 (*A "possibility property": there are traces that reach the end*) |
85 lemma "B \<noteq> Server |
85 lemma "[| B \<noteq> Server; Key K \<notin> used [] |] |
86 ==> \<exists>K. \<exists>evs \<in> otway. |
86 ==> \<exists>evs \<in> otway. |
87 Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) |
87 Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) |
88 \<in> set evs" |
88 \<in> set evs" |
89 apply (intro exI bexI) |
89 apply (intro exI bexI) |
90 apply (rule_tac [2] otway.Nil |
90 apply (rule_tac [2] otway.Nil |
91 [THEN otway.OR1, THEN otway.Reception, |
91 [THEN otway.OR1, THEN otway.Reception, |
92 THEN otway.OR2, THEN otway.Reception, |
92 THEN otway.OR2, THEN otway.Reception, |
93 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4], possibility) |
93 THEN otway.OR3, THEN otway.Reception, THEN otway.OR4]) |
|
94 apply (possibility, simp add: used_Cons) |
94 done |
95 done |
95 |
96 |
96 lemma Gets_imp_Says [dest!]: |
97 lemma Gets_imp_Says [dest!]: |
97 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
98 "[| Gets B X \<in> set evs; evs \<in> otway |] ==> \<exists>A. Says A B X \<in> set evs" |
98 by (erule rev_mp, erule otway.induct, auto) |
99 by (erule rev_mp, erule otway.induct, auto) |