14 AddDs [impOfSubs analz_subset_parts]; |
14 AddDs [impOfSubs analz_subset_parts]; |
15 AddDs [impOfSubs Fake_parts_insert]; |
15 AddDs [impOfSubs Fake_parts_insert]; |
16 |
16 |
17 |
17 |
18 (*A "possibility property": there are traces that reach the end*) |
18 (*A "possibility property": there are traces that reach the end*) |
19 Goal "[| A ~= B; A ~= Server; B ~= Server |] \ |
19 Goal "EX NB. EX evs: woolam. \ |
20 \ ==> EX NB. EX evs: woolam. \ |
|
21 \ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs"; |
20 \ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) : set evs"; |
22 by (REPEAT (resolve_tac [exI,bexI] 1)); |
21 by (REPEAT (resolve_tac [exI,bexI] 1)); |
23 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS |
22 by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS |
24 woolam.WL4 RS woolam.WL5) 2); |
23 woolam.WL4 RS woolam.WL5) 2); |
25 by possibility_tac; |
24 by possibility_tac; |
26 result(); |
25 result(); |
27 |
26 |
28 |
27 |
29 (**** Inductive proofs about woolam ****) |
28 (**** Inductive proofs about woolam ****) |
30 |
|
31 (*Nobody sends themselves messages*) |
|
32 Goal "evs : woolam ==> ALL X. Says A A X ~: set evs"; |
|
33 by (etac woolam.induct 1); |
|
34 by Auto_tac; |
|
35 qed_spec_mp "not_Says_to_self"; |
|
36 Addsimps [not_Says_to_self]; |
|
37 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
38 |
|
39 |
29 |
40 (** For reasoning about the encrypted portion of messages **) |
30 (** For reasoning about the encrypted portion of messages **) |
41 |
31 |
42 Goal "Says A' B X : set evs ==> X : analz (spies evs)"; |
32 Goal "Says A' B X : set evs ==> X : analz (spies evs)"; |
43 by (etac (Says_imp_spies RS analz.Inj) 1); |
33 by (etac (Says_imp_spies RS analz.Inj) 1); |