12 AddDs [impOfSubs Fake_parts_insert]; |
12 AddDs [impOfSubs Fake_parts_insert]; |
13 |
13 |
14 AddIffs [Spy_in_bad]; |
14 AddIffs [Spy_in_bad]; |
15 |
15 |
16 (*A "possibility property": there are traces that reach the end*) |
16 (*A "possibility property": there are traces that reach the end*) |
17 Goal "A ~= B ==> EX NB. EX evs: ns_public. \ |
17 Goal |
18 \ Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
18 "EX NB. EX evs: ns_public. Says A B (Crypt (pubK B) (Nonce NB)) : set evs"; |
19 by (REPEAT (resolve_tac [exI,bexI] 1)); |
19 by (REPEAT (resolve_tac [exI,bexI] 1)); |
20 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
20 by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); |
21 by possibility_tac; |
21 by possibility_tac; |
22 result(); |
22 result(); |
23 |
23 |
24 |
24 |
25 (**** Inductive proofs about ns_public ****) |
25 (**** Inductive proofs about ns_public ****) |
26 |
|
27 (*Nobody sends themselves messages*) |
|
28 Goal "evs : ns_public ==> ALL X. Says A A X ~: set evs"; |
|
29 by (etac ns_public.induct 1); |
|
30 by Auto_tac; |
|
31 qed_spec_mp "not_Says_to_self"; |
|
32 Addsimps [not_Says_to_self]; |
|
33 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
34 |
|
35 |
26 |
36 (*Induction for regularity theorems. If induction formula has the form |
27 (*Induction for regularity theorems. If induction formula has the form |
37 X ~: analz (spies evs) --> ... then it shortens the proof by discarding |
28 X ~: analz (spies evs) --> ... then it shortens the proof by discarding |
38 needless information about analz (insert X (spies evs)) *) |
29 needless information about analz (insert X (spies evs)) *) |
39 fun parts_induct_tac i = |
30 fun parts_induct_tac i = |