54 (simpset() addsimps [imageI, knows_Cons] |
54 (simpset() addsimps [imageI, knows_Cons] |
55 addsplits [expand_event_case]))); |
55 addsplits [expand_event_case]))); |
56 qed "Spy_knows_Spy_bad"; |
56 qed "Spy_knows_Spy_bad"; |
57 AddSIs [Spy_knows_Spy_bad]; |
57 AddSIs [Spy_knows_Spy_bad]; |
58 |
58 |
59 (*For not_bad_tac*) |
59 (*For case analysis on whether or not an agent is compromised*) |
60 Goal "[| Crypt (shrK A) X : analz (knows Spy evs); A: bad |] \ |
60 Goal "[| Crypt (shrK A) X : analz (knows Spy evs); A: bad |] \ |
61 \ ==> X : analz (knows Spy evs)"; |
61 \ ==> X : analz (knows Spy evs)"; |
62 by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1); |
62 by (force_tac (claset() addSDs [analz.Decrypt], simpset()) 1); |
63 qed "Crypt_Spy_analz_bad"; |
63 qed "Crypt_Spy_analz_bad"; |
64 |
|
65 (*Prove that the agent is uncompromised by the confidentiality of |
|
66 a component of a message she's said.*) |
|
67 fun not_bad_tac s = |
|
68 case_tac ("(" ^ s ^ ") : bad") THEN' |
|
69 SELECT_GOAL |
|
70 (REPEAT_DETERM (etac exE 1) THEN |
|
71 REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN |
|
72 REPEAT_DETERM (etac MPair_analz 1) THEN |
|
73 THEN_BEST_FIRST |
|
74 (dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) |
|
75 (has_fewer_prems 1, size_of_thm) |
|
76 (Step_tac 1)); |
|
77 |
64 |
78 |
65 |
79 (** Fresh keys never clash with long-term shared keys **) |
66 (** Fresh keys never clash with long-term shared keys **) |
80 |
67 |
81 (*Agents see their own shared keys!*) |
68 (*Agents see their own shared keys!*) |