equal
deleted
inserted
replaced
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
17 |
17 |
18 |
18 |
19 (*A "possibility property": there are traces that reach the end*) |
19 (*A "possibility property": there are traces that reach the end*) |
20 Goal "B \\<noteq> Server \ |
20 Goal "B \\<noteq> Server \ |
21 \ ==> \\<exists>K. \\<exists>NA. \\<exists>evs \\<in> otway. \ |
21 \ ==> \\<exists>K. \\<exists>evs \\<in> otway. \ |
22 \ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ |
22 \ Says B A (Crypt (shrK A) {|Nonce NA, Agent A, Agent B, Key K|}) \ |
23 \ \\<in> set evs"; |
23 \ \\<in> set evs"; |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
25 by (rtac (otway.Nil RS |
25 by (rtac (otway.Nil RS |
26 otway.OR1 RS otway.Reception RS |
26 otway.OR1 RS otway.Reception RS |