author | paulson |
Fri, 11 Apr 1997 15:21:36 +0200 | |
changeset 2935 | 998cb95fdd43 |
parent 2637 | e9b203f854ae |
child 3121 | cbb6c0c1c58a |
permissions | -rw-r--r-- |
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 |
||
2537 | 132 |
(*Use with addSEs to derive contradictions from old Says events containing |
133 |
items known to be fresh*) |
|
134 |
val sees_Spy_partsEs = make_elim (Says_imp_sees_Spy RS parts.Inj):: partsEs; |
|
135 |
||
2318 | 136 |
goal thy |
137 |
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; C : lost |] \ |
|
138 |
\ ==> X : analz (sees lost Spy evs)"; |
|
139 |
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
|
140 |
addss (!simpset)) 1); |
|
141 |
qed "Says_Crypt_lost"; |
|
142 |
||
143 |
goal thy |
|
144 |
"!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \ |
|
145 |
\ X ~: analz (sees lost Spy evs) |] \ |
|
146 |
\ ==> C ~: lost"; |
|
147 |
by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] |
|
148 |
addss (!simpset)) 1); |
|
149 |
qed "Says_Crypt_not_lost"; |
|
150 |
||
151 |
Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; |
|
152 |
Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) |
|
153 |
||
154 |
||
2497 | 155 |
(*** Fresh nonces ***) |
156 |
||
157 |
goal thy "Nonce N ~: parts (initState lost B)"; |
|
158 |
by (agent.induct_tac "B" 1); |
|
159 |
by (Auto_tac ()); |
|
160 |
qed "Nonce_notin_initState"; |
|
161 |
||
162 |
AddIffs [Nonce_notin_initState]; |
|
163 |
||
164 |
goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs"; |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
165 |
by (etac (impOfSubs parts_mono) 1); |
2497 | 166 |
by (Fast_tac 1); |
167 |
qed "usedI"; |
|
168 |
||
169 |
AddIs [usedI]; |
|
170 |
||
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
171 |
(** A supply of fresh nonces for possibility theorems. **) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
172 |
|
2497 | 173 |
goalw thy [used_def] "EX N. ALL n. N<=n --> Nonce n ~: used evs"; |
174 |
by (list.induct_tac "evs" 1); |
|
175 |
by (res_inst_tac [("x","0")] exI 1); |
|
176 |
by (Step_tac 1); |
|
177 |
by (Full_simp_tac 1); |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
178 |
(*Inductive step*) |
2497 | 179 |
by (event.induct_tac "a" 1); |
180 |
by (full_simp_tac (!simpset addsimps [UN_parts_sees_Says]) 1); |
|
181 |
by (msg.induct_tac "msg" 1); |
|
182 |
by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2]))); |
|
183 |
by (Step_tac 1); |
|
184 |
(*MPair case*) |
|
185 |
by (res_inst_tac [("x","Na+Nb")] exI 2); |
|
186 |
by (fast_tac (!claset addSEs [add_leE]) 2); |
|
187 |
(*Nonce case*) |
|
188 |
by (res_inst_tac [("x","N + Suc nat")] exI 1); |
|
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2537
diff
changeset
|
189 |
by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1); |
2497 | 190 |
val lemma = result(); |
191 |
||
192 |
goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
193 |
by (rtac (lemma RS exE) 1); |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
194 |
by (rtac selectI 1); |
2497 | 195 |
by (Fast_tac 1); |
196 |
qed "Nonce_supply"; |
|
197 |
||
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
198 |
(*Tactic for possibility theorems*) |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
199 |
val possibility_tac = |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
200 |
REPEAT |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2537
diff
changeset
|
201 |
(ALLGOALS (simp_tac (!simpset setSolver safe_solver)) |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
202 |
THEN |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
203 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset
|
204 |
resolve_tac [refl, conjI, Nonce_supply])); |
2497 | 205 |
|
2318 | 206 |
(** Power of the Spy **) |
207 |
||
208 |
(*The Spy can see more than anybody else, except for their initial state*) |
|
209 |
goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs"; |
|
210 |
by (list.induct_tac "evs" 1); |
|
211 |
by (event.induct_tac "a" 2); |
|
212 |
by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] |
|
213 |
addss (!simpset)))); |
|
214 |
qed "sees_agent_subset_sees_Spy"; |
|
215 |
||
216 |
(*The Spy can see more than anybody else who's lost their key!*) |
|
217 |
goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs"; |
|
218 |
by (list.induct_tac "evs" 1); |
|
219 |
by (event.induct_tac "a" 2); |
|
220 |
by (agent.induct_tac "A" 1); |
|
221 |
by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset))); |
|
222 |
qed_spec_mp "sees_lost_agent_subset_sees_Spy"; |
|
223 |
||
224 |
||
225 |
(** Simplifying parts (insert X (sees lost A evs)) |
|
226 |
= parts {X} Un parts (sees lost A evs) -- since general case loops*) |
|
227 |
||
228 |
val parts_insert_sees = |
|
229 |
parts_insert |> read_instantiate_sg (sign_of thy) |
|
230 |
[("H", "sees lost A evs")] |
|
231 |
|> standard; |