35 AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; |
35 AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; |
36 |
36 |
37 (** Rewrites should not refer to initState(Friend i) |
37 (** Rewrites should not refer to initState(Friend i) |
38 -- not in normal form! **) |
38 -- not in normal form! **) |
39 |
39 |
40 goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; |
40 goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; |
41 by (agent.induct_tac "C" 1); |
41 by (agent.induct_tac "C" 1); |
42 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
42 by (auto_tac (!claset addIs [range_eqI], !simpset)); |
43 qed "keysFor_parts_initState"; |
43 qed "keysFor_parts_initState"; |
44 Addsimps [keysFor_parts_initState]; |
44 Addsimps [keysFor_parts_initState]; |
45 |
45 |
46 |
46 |
47 (*** Function "sees" ***) |
47 (*** Function "sees" ***) |
48 |
48 |
49 (*Agents see their own private keys!*) |
49 (*Agents see their own private keys!*) |
50 goal thy "A ~= Spy --> Key (priK A) : sees lost A evs"; |
50 goal thy "A ~= Spy --> Key (priK A) : sees A evs"; |
51 by (list.induct_tac "evs" 1); |
51 by (list.induct_tac "evs" 1); |
52 by (agent.induct_tac "A" 1); |
52 by (agent.induct_tac "A" 1); |
53 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
53 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
54 qed_spec_mp "sees_own_priK"; |
54 qed_spec_mp "sees_own_priK"; |
55 |
55 |
56 (*All public keys are visible to all*) |
56 (*All public keys are visible to all*) |
57 goal thy "Key (pubK A) : sees lost B evs"; |
57 goal thy "Key (pubK A) : sees B evs"; |
58 by (list.induct_tac "evs" 1); |
58 by (list.induct_tac "evs" 1); |
59 by (agent.induct_tac "B" 1); |
59 by (agent.induct_tac "B" 1); |
60 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
60 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
61 by (Auto_tac ()); |
61 by (Auto_tac ()); |
62 qed_spec_mp "sees_pubK"; |
62 qed_spec_mp "sees_pubK"; |
63 |
63 |
64 (*Spy sees private keys of lost agents!*) |
64 (*Spy sees private keys of agents!*) |
65 goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs"; |
65 goal thy "!!A. A: lost ==> Key (priK A) : sees Spy evs"; |
66 by (list.induct_tac "evs" 1); |
66 by (list.induct_tac "evs" 1); |
67 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
67 by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); |
68 by (Blast_tac 1); |
68 by (Blast_tac 1); |
69 qed "Spy_sees_lost"; |
69 qed "Spy_sees_lost"; |
70 |
70 |
71 AddIffs [sees_pubK, sees_pubK RS analz.Inj]; |
71 AddIffs [sees_pubK, sees_pubK RS analz.Inj]; |
72 AddSIs [sees_own_priK, Spy_sees_lost]; |
72 AddSIs [sees_own_priK, Spy_sees_lost]; |
73 |
73 |
74 |
74 |
75 (*For not_lost_tac*) |
75 (*For not_lost_tac*) |
76 goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \ |
76 goal thy "!!A. [| Crypt (pubK A) X : analz (sees Spy evs); A: lost |] \ |
77 \ ==> X : analz (sees lost Spy evs)"; |
77 \ ==> X : analz (sees Spy evs)"; |
78 by (blast_tac (!claset addSDs [analz.Decrypt]) 1); |
78 by (blast_tac (!claset addSDs [analz.Decrypt]) 1); |
79 qed "Crypt_Spy_analz_lost"; |
79 qed "Crypt_Spy_analz_lost"; |
80 |
80 |
81 (*Prove that the agent is uncompromised by the confidentiality of |
81 (*Prove that the agent is uncompromised by the confidentiality of |
82 a component of a message she's said.*) |
82 a component of a message she's said.*) |