2318
|
1 |
(* Title: HOL/Auth/Public
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1996 University of Cambridge
|
|
5 |
|
|
6 |
Theory of Public Keys (common to all symmetric-key protocols)
|
|
7 |
|
|
8 |
Server keys; initial states of agents; new nonces and keys; function "sees"
|
|
9 |
*)
|
|
10 |
|
|
11 |
|
|
12 |
open Public;
|
|
13 |
|
2497
|
14 |
(*Injectiveness of new nonces*)
|
|
15 |
AddIffs [inj_newN RS inj_eq];
|
|
16 |
|
2318
|
17 |
(*Holds because Friend is injective: thus cannot prove for all f*)
|
|
18 |
goal thy "(Friend x : Friend``A) = (x:A)";
|
|
19 |
by (Auto_tac());
|
|
20 |
qed "Friend_image_eq";
|
|
21 |
Addsimps [Friend_image_eq];
|
|
22 |
|
|
23 |
Addsimps [Un_insert_left, Un_insert_right];
|
|
24 |
|
|
25 |
(*By default only o_apply is built-in. But in the presence of eta-expansion
|
|
26 |
this means that some terms displayed as (f o g) will be rewritten, and others
|
|
27 |
will not!*)
|
|
28 |
Addsimps [o_def];
|
|
29 |
|
|
30 |
goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}";
|
|
31 |
by (agent.induct_tac "C" 1);
|
|
32 |
by (auto_tac (!claset addIs [range_eqI], !simpset));
|
|
33 |
qed "keysFor_parts_initState";
|
|
34 |
Addsimps [keysFor_parts_initState];
|
|
35 |
|
|
36 |
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
|
|
37 |
by (Auto_tac ());
|
|
38 |
qed "keysFor_image_Key";
|
|
39 |
Addsimps [keysFor_image_Key];
|
|
40 |
|
|
41 |
|
|
42 |
(*** Function "sees" ***)
|
|
43 |
|
|
44 |
goal thy
|
|
45 |
"!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs";
|
|
46 |
by (list.induct_tac "evs" 1);
|
|
47 |
by (agent.induct_tac "A" 1);
|
|
48 |
by (event.induct_tac "a" 2);
|
|
49 |
by (Auto_tac ());
|
|
50 |
qed "sees_mono";
|
|
51 |
|
2497
|
52 |
(*** Basic properties of pubK & priK ***)
|
|
53 |
|
|
54 |
AddIffs [inj_pubK RS inj_eq];
|
|
55 |
Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym];
|
|
56 |
|
2318
|
57 |
(*Agents see their own private keys!*)
|
|
58 |
goal thy "A ~= Spy --> Key (priK A) : sees lost A evs";
|
|
59 |
by (list.induct_tac "evs" 1);
|
|
60 |
by (agent.induct_tac "A" 1);
|
|
61 |
by (Auto_tac ());
|
|
62 |
qed_spec_mp "sees_own_priK";
|
|
63 |
|
|
64 |
(*All public keys are visible*)
|
|
65 |
goal thy "Key (pubK A) : sees lost A evs";
|
|
66 |
by (list.induct_tac "evs" 1);
|
|
67 |
by (agent.induct_tac "A" 1);
|
|
68 |
by (Auto_tac ());
|
|
69 |
qed_spec_mp "sees_pubK";
|
|
70 |
|
|
71 |
(*Spy sees private keys of lost agents!*)
|
|
72 |
goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs";
|
|
73 |
by (list.induct_tac "evs" 1);
|
|
74 |
by (Auto_tac());
|
|
75 |
qed "Spy_sees_lost";
|
|
76 |
|
|
77 |
AddIffs [sees_pubK];
|
|
78 |
AddSIs [sees_own_priK, Spy_sees_lost];
|
|
79 |
|
|
80 |
(*Added for Yahalom/lost_tac*)
|
|
81 |
goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \
|
|
82 |
\ ==> X : analz (sees lost Spy evs)";
|
|
83 |
by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1);
|
|
84 |
qed "Crypt_Spy_analz_lost";
|
|
85 |
|
|
86 |
(** Specialized rewrite rules for (sees lost A (Says...#evs)) **)
|
|
87 |
|
|
88 |
goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)";
|
|
89 |
by (Simp_tac 1);
|
|
90 |
qed "sees_own";
|
|
91 |
|
|
92 |
goal thy "!!A. Server ~= B ==> \
|
|
93 |
\ sees lost Server (Says A B X # evs) = sees lost Server evs";
|
|
94 |
by (Asm_simp_tac 1);
|
|
95 |
qed "sees_Server";
|
|
96 |
|
|
97 |
goal thy "!!A. Friend i ~= B ==> \
|
|
98 |
\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs";
|
|
99 |
by (Asm_simp_tac 1);
|
|
100 |
qed "sees_Friend";
|
|
101 |
|
|
102 |
goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)";
|
|
103 |
by (Simp_tac 1);
|
|
104 |
qed "sees_Spy";
|
|
105 |
|
|
106 |
goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
|
|
107 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
|
|
108 |
by (Fast_tac 1);
|
|
109 |
qed "sees_Says_subset_insert";
|
|
110 |
|
|
111 |
goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
|
|
112 |
by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
|
|
113 |
by (Fast_tac 1);
|
|
114 |
qed "sees_subset_sees_Says";
|
|
115 |
|
|
116 |
(*Pushing Unions into parts. One of the agents A is B, and thus sees Y.
|
|
117 |
Once used to prove new_keys_not_seen; now obsolete.*)
|
|
118 |
goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \
|
|
119 |
\ parts {Y} Un (UN A. parts (sees lost A evs))";
|
|
120 |
by (Step_tac 1);
|
|
121 |
by (etac rev_mp 1); (*split_tac does not work on assumptions*)
|
|
122 |
by (ALLGOALS
|
|
123 |
(fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons]
|
|
124 |
setloop split_tac [expand_if]))));
|
|
125 |
qed "UN_parts_sees_Says";
|
|
126 |
|
|
127 |
goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
|
|
128 |
by (list.induct_tac "evs" 1);
|
|
129 |
by (Auto_tac ());
|
|
130 |
qed_spec_mp "Says_imp_sees_Spy";
|
|
131 |
|
|
132 |
goal thy
|
|
133 |
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; C : lost |] \
|
|
134 |
\ ==> X : analz (sees lost Spy evs)";
|
|
135 |
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
|
|
136 |
addss (!simpset)) 1);
|
|
137 |
qed "Says_Crypt_lost";
|
|
138 |
|
|
139 |
goal thy
|
|
140 |
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \
|
|
141 |
\ X ~: analz (sees lost Spy evs) |] \
|
|
142 |
\ ==> C ~: lost";
|
|
143 |
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]
|
|
144 |
addss (!simpset)) 1);
|
|
145 |
qed "Says_Crypt_not_lost";
|
|
146 |
|
|
147 |
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
|
|
148 |
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****)
|
|
149 |
|
|
150 |
|
2497
|
151 |
(*** Fresh nonces ***)
|
|
152 |
|
|
153 |
goal thy "Nonce N ~: parts (initState lost B)";
|
|
154 |
by (agent.induct_tac "B" 1);
|
|
155 |
by (Auto_tac ());
|
|
156 |
qed "Nonce_notin_initState";
|
|
157 |
|
|
158 |
AddIffs [Nonce_notin_initState];
|
|
159 |
|
|
160 |
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
|
|
161 |
be (impOfSubs parts_mono) 1;
|
|
162 |
by (Fast_tac 1);
|
|
163 |
qed "usedI";
|
|
164 |
|
|
165 |
AddIs [usedI];
|
|
166 |
|
|
167 |
(*Yields a supply of fresh nonces for possibility theorems.*)
|
|
168 |
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs";
|
|
169 |
by (list.induct_tac "evs" 1);
|
|
170 |
by (res_inst_tac [("x","0")] exI 1);
|
|
171 |
by (Step_tac 1);
|
|
172 |
by (Full_simp_tac 1);
|
|
173 |
by (event.induct_tac "a" 1);
|
|
174 |
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1);
|
|
175 |
by (msg.induct_tac "msg" 1);
|
|
176 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
|
|
177 |
by (Step_tac 1);
|
|
178 |
(*MPair case*)
|
|
179 |
by (res_inst_tac [("x","Na+Nb")] exI 2);
|
|
180 |
by (fast_tac (!claset addSEs [add_leE]) 2);
|
|
181 |
(*Nonce case*)
|
|
182 |
by (res_inst_tac [("x","N + Suc nat")] exI 1);
|
|
183 |
by (fast_tac (!claset addSEs [add_leE] addafter (TRYALL trans_tac)) 1);
|
|
184 |
val lemma = result();
|
|
185 |
|
|
186 |
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
|
|
187 |
br (lemma RS exE) 1;
|
|
188 |
br selectI 1;
|
|
189 |
by (Fast_tac 1);
|
|
190 |
qed "Nonce_supply";
|
|
191 |
|
|
192 |
|
2318
|
193 |
(** Power of the Spy **)
|
|
194 |
|
|
195 |
(*The Spy can see more than anybody else, except for their initial state*)
|
|
196 |
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs";
|
|
197 |
by (list.induct_tac "evs" 1);
|
|
198 |
by (event.induct_tac "a" 2);
|
|
199 |
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD]
|
|
200 |
addss (!simpset))));
|
|
201 |
qed "sees_agent_subset_sees_Spy";
|
|
202 |
|
|
203 |
(*The Spy can see more than anybody else who's lost their key!*)
|
|
204 |
goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs";
|
|
205 |
by (list.induct_tac "evs" 1);
|
|
206 |
by (event.induct_tac "a" 2);
|
|
207 |
by (agent.induct_tac "A" 1);
|
|
208 |
by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset)));
|
|
209 |
qed_spec_mp "sees_lost_agent_subset_sees_Spy";
|
|
210 |
|
|
211 |
|
|
212 |
(** Simplifying parts (insert X (sees lost A evs))
|
|
213 |
= parts {X} Un parts (sees lost A evs) -- since general case loops*)
|
|
214 |
|
|
215 |
val parts_insert_sees =
|
|
216 |
parts_insert |> read_instantiate_sg (sign_of thy)
|
|
217 |
[("H", "sees lost A evs")]
|
|
218 |
|> standard;
|