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>NA K. \\<exists>evs \\<in> otway. \ |
21 \ ==> \\<exists>K. \\<exists>evs \\<in> otway. \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, 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 |