author | paulson |
Thu, 04 Sep 2003 11:08:24 +0200 | |
changeset 14181 | 942db403d4bb |
parent 14126 | 28824746d046 |
child 14200 | d8598e24f8fa |
permissions | -rw-r--r-- |
1934 | 1 |
(* Title: HOL/Auth/Shared |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Theory of Shared Keys (common to all symmetric-key protocols) |
|
7 |
||
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3472
diff
changeset
|
8 |
Shared, long-term keys; initial states of agents |
1934 | 9 |
*) |
10 |
||
13926 | 11 |
theory Shared = Event: |
1934 | 12 |
|
13 |
consts |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
14 |
shrK :: "agent => key" (*symmetric keys*); |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
15 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
16 |
specification (shrK) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
17 |
inj_shrK: "inj shrK" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
18 |
--{*No two agents have the same long-term key*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
19 |
apply (rule exI [of _ "agent_case 0 (\<lambda>n. n + 2) 1"]) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
20 |
apply (simp add: inj_on_def split: agent.split) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
21 |
done |
1967 | 22 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
23 |
text{*All keys are symmetric*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
24 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
25 |
defs all_symmetric_def: "all_symmetric == True" |
1934 | 26 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
27 |
lemma isSym_keys: "K \<in> symKeys" |
14181 | 28 |
by (simp add: symKeys_def all_symmetric_def invKey_symmetric) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
29 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
30 |
text{*Server knows all long-term keys; other agents know only their own*} |
5183 | 31 |
primrec |
11104 | 32 |
initState_Server: "initState Server = Key ` range shrK" |
33 |
initState_Friend: "initState (Friend i) = {Key (shrK (Friend i))}" |
|
34 |
initState_Spy: "initState Spy = Key`shrK`bad" |
|
2032 | 35 |
|
1934 | 36 |
|
13926 | 37 |
subsection{*Basic properties of shrK*} |
38 |
||
39 |
(*Injectiveness: Agents' long-term keys are distinct.*) |
|
40 |
declare inj_shrK [THEN inj_eq, iff] |
|
41 |
||
42 |
lemma invKey_K [simp]: "invKey K = K" |
|
43 |
apply (insert isSym_keys) |
|
44 |
apply (simp add: symKeys_def) |
|
45 |
done |
|
46 |
||
47 |
||
48 |
lemma analz_Decrypt' [dest]: |
|
49 |
"[| Crypt K X \<in> analz H; Key K \<in> analz H |] ==> X \<in> analz H" |
|
50 |
by auto |
|
51 |
||
52 |
text{*Now cancel the @{text dest} attribute given to |
|
53 |
@{text analz.Decrypt} in its declaration.*} |
|
54 |
ML |
|
55 |
{* |
|
56 |
Delrules [analz.Decrypt]; |
|
57 |
*} |
|
58 |
||
59 |
text{*Rewrites should not refer to @{term "initState(Friend i)"} because |
|
60 |
that expression is not in normal form.*} |
|
61 |
||
62 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
63 |
apply (unfold keysFor_def) |
|
64 |
apply (induct_tac "C", auto) |
|
65 |
done |
|
66 |
||
67 |
(*Specialized to shared-key model: no @{term invKey}*) |
|
68 |
lemma keysFor_parts_insert: |
|
69 |
"[| K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) |] \ |
|
70 |
\ ==> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"; |
|
71 |
by (force dest: Event.keysFor_parts_insert) |
|
72 |
||
73 |
lemma Crypt_imp_keysFor: "Crypt K X \<in> H ==> K \<in> keysFor H" |
|
74 |
by (drule Crypt_imp_invKey_keysFor, simp) |
|
75 |
||
76 |
||
77 |
subsection{*Function "knows"*} |
|
78 |
||
79 |
(*Spy sees shared keys of agents!*) |
|
80 |
lemma Spy_knows_Spy_bad [intro!]: "A: bad ==> Key (shrK A) \<in> knows Spy evs" |
|
81 |
apply (induct_tac "evs") |
|
82 |
apply (simp_all (no_asm_simp) add: imageI knows_Cons split add: event.split) |
|
83 |
done |
|
84 |
||
85 |
(*For case analysis on whether or not an agent is compromised*) |
|
86 |
lemma Crypt_Spy_analz_bad: "[| Crypt (shrK A) X \<in> analz (knows Spy evs); A: bad |] |
|
87 |
==> X \<in> analz (knows Spy evs)" |
|
88 |
apply (force dest!: analz.Decrypt) |
|
89 |
done |
|
90 |
||
91 |
||
92 |
(** Fresh keys never clash with long-term shared keys **) |
|
93 |
||
94 |
(*Agents see their own shared keys!*) |
|
95 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" |
|
96 |
by (induct_tac "A", auto) |
|
97 |
||
98 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" |
|
99 |
by (rule initState_into_used, blast) |
|
100 |
||
101 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
102 |
from long-term shared keys*) |
|
103 |
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" |
|
104 |
by blast |
|
105 |
||
106 |
lemma shrK_neq [simp]: "Key K \<notin> used evs ==> shrK B \<noteq> K" |
|
107 |
by blast |
|
108 |
||
109 |
declare shrK_neq [THEN not_sym, simp] |
|
110 |
||
111 |
||
112 |
subsection{*Fresh nonces*} |
|
113 |
||
114 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
115 |
by (induct_tac "B", auto) |
|
116 |
||
117 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
118 |
apply (simp (no_asm) add: used_Nil) |
|
119 |
done |
|
120 |
||
121 |
||
122 |
subsection{*Supply fresh nonces for possibility theorems.*} |
|
123 |
||
124 |
(*In any trace, there is an upper bound N on the greatest nonce in use.*) |
|
125 |
lemma Nonce_supply_lemma: "\<exists>N. ALL n. N<=n --> Nonce n \<notin> used evs" |
|
126 |
apply (induct_tac "evs") |
|
127 |
apply (rule_tac x = 0 in exI) |
|
128 |
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
|
129 |
apply safe |
|
130 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
|
131 |
done |
|
132 |
||
133 |
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs" |
|
134 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
|
135 |
||
136 |
lemma Nonce_supply2: "\<exists>N N'. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & N \<noteq> N'" |
|
137 |
apply (cut_tac evs = evs in Nonce_supply_lemma) |
|
138 |
apply (cut_tac evs = "evs'" in Nonce_supply_lemma, clarify) |
|
139 |
apply (rule_tac x = N in exI) |
|
140 |
apply (rule_tac x = "Suc (N+Na) " in exI) |
|
141 |
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
|
142 |
done |
|
143 |
||
144 |
lemma Nonce_supply3: "\<exists>N N' N''. Nonce N \<notin> used evs & Nonce N' \<notin> used evs' & |
|
145 |
Nonce N'' \<notin> used evs'' & N \<noteq> N' & N' \<noteq> N'' & N \<noteq> N''" |
|
146 |
apply (cut_tac evs = evs in Nonce_supply_lemma) |
|
147 |
apply (cut_tac evs = "evs'" in Nonce_supply_lemma) |
|
148 |
apply (cut_tac evs = "evs''" in Nonce_supply_lemma, clarify) |
|
149 |
apply (rule_tac x = N in exI) |
|
150 |
apply (rule_tac x = "Suc (N+Na) " in exI) |
|
151 |
apply (rule_tac x = "Suc (Suc (N+Na+Nb))" in exI) |
|
152 |
apply (simp (no_asm_simp) add: less_not_refl3 le_add1 le_add2 less_Suc_eq_le) |
|
153 |
done |
|
154 |
||
155 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
|
156 |
apply (rule Nonce_supply_lemma [THEN exE]) |
|
157 |
apply (rule someI, blast) |
|
158 |
done |
|
159 |
||
160 |
subsection{*Supply fresh keys for possibility theorems.*} |
|
161 |
||
11104 | 162 |
axioms |
13926 | 163 |
Key_supply_ax: "finite KK ==> \<exists>K. K \<notin> KK & Key K \<notin> used evs" |
164 |
--{*Unlike the corresponding property of nonces, this cannot be proved. |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
165 |
We have infinitely many agents and there is nothing to stop their |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
166 |
long-term keys from exhausting all the natural numbers. The axiom |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
167 |
assumes that their keys are dispersed so as to leave room for infinitely |
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
168 |
many fresh session keys. We could, alternatively, restrict agents to |
13926 | 169 |
an unspecified finite number. We could however replace @{term"used evs"} |
170 |
by @{term "used []"}.*} |
|
171 |
||
172 |
lemma Key_supply1: "\<exists>K. Key K \<notin> used evs" |
|
173 |
by (rule Finites.emptyI [THEN Key_supply_ax, THEN exE], blast) |
|
174 |
||
175 |
lemma Key_supply2: "\<exists>K K'. Key K \<notin> used evs & Key K' \<notin> used evs' & K \<noteq> K'" |
|
176 |
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) |
|
177 |
apply (erule exE) |
|
178 |
apply (cut_tac evs="evs'" in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax], auto) |
|
179 |
done |
|
180 |
||
181 |
lemma Key_supply3: "\<exists>K K' K''. Key K \<notin> used evs & Key K' \<notin> used evs' & |
|
182 |
Key K'' \<notin> used evs'' & K \<noteq> K' & K' \<noteq> K'' & K \<noteq> K''" |
|
183 |
apply (cut_tac evs = evs in Finites.emptyI [THEN Key_supply_ax]) |
|
184 |
apply (erule exE) |
|
185 |
(*Blast_tac requires instantiation of the keys for some reason*) |
|
186 |
apply (cut_tac evs="evs'" and a1 = K in Finites.emptyI [THEN Finites.insertI, THEN Key_supply_ax]) |
|
187 |
apply (erule exE) |
|
188 |
apply (cut_tac evs = "evs''" and a1 = Ka and a2 = K |
|
189 |
in Finites.emptyI [THEN Finites.insertI, THEN Finites.insertI, THEN Key_supply_ax], blast) |
|
190 |
done |
|
191 |
||
192 |
lemma Key_supply: "Key (@ K. Key K \<notin> used evs) \<notin> used evs" |
|
193 |
apply (rule Finites.emptyI [THEN Key_supply_ax, THEN exE]) |
|
194 |
apply (rule someI, blast) |
|
195 |
done |
|
196 |
||
197 |
subsection{*Tactics for possibility theorems*} |
|
198 |
||
199 |
ML |
|
200 |
{* |
|
201 |
val inj_shrK = thm "inj_shrK"; |
|
202 |
val isSym_keys = thm "isSym_keys"; |
|
203 |
val Key_supply_ax = thm "Key_supply_ax"; |
|
204 |
val Key_supply = thm "Key_supply"; |
|
205 |
val Nonce_supply = thm "Nonce_supply"; |
|
206 |
val invKey_K = thm "invKey_K"; |
|
207 |
val analz_Decrypt' = thm "analz_Decrypt'"; |
|
208 |
val keysFor_parts_initState = thm "keysFor_parts_initState"; |
|
209 |
val keysFor_parts_insert = thm "keysFor_parts_insert"; |
|
210 |
val Crypt_imp_keysFor = thm "Crypt_imp_keysFor"; |
|
211 |
val Spy_knows_Spy_bad = thm "Spy_knows_Spy_bad"; |
|
212 |
val Crypt_Spy_analz_bad = thm "Crypt_Spy_analz_bad"; |
|
213 |
val shrK_in_initState = thm "shrK_in_initState"; |
|
214 |
val shrK_in_used = thm "shrK_in_used"; |
|
215 |
val Key_not_used = thm "Key_not_used"; |
|
216 |
val shrK_neq = thm "shrK_neq"; |
|
217 |
val Nonce_notin_initState = thm "Nonce_notin_initState"; |
|
218 |
val Nonce_notin_used_empty = thm "Nonce_notin_used_empty"; |
|
219 |
val Nonce_supply_lemma = thm "Nonce_supply_lemma"; |
|
220 |
val Nonce_supply1 = thm "Nonce_supply1"; |
|
221 |
val Nonce_supply2 = thm "Nonce_supply2"; |
|
222 |
val Nonce_supply3 = thm "Nonce_supply3"; |
|
223 |
val Nonce_supply = thm "Nonce_supply"; |
|
224 |
val Key_supply1 = thm "Key_supply1"; |
|
225 |
val Key_supply2 = thm "Key_supply2"; |
|
226 |
val Key_supply3 = thm "Key_supply3"; |
|
227 |
val Key_supply = thm "Key_supply"; |
|
228 |
*} |
|
229 |
||
11104 | 230 |
|
13926 | 231 |
ML |
232 |
{* |
|
233 |
(*Omitting used_Says makes the tactic much faster: it leaves expressions |
|
234 |
such as Nonce ?N \<notin> used evs that match Nonce_supply*) |
|
235 |
fun gen_possibility_tac ss state = state |> |
|
236 |
(REPEAT |
|
237 |
(ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets] |
|
238 |
setSolver safe_solver)) |
|
239 |
THEN |
|
240 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
241 |
resolve_tac [refl, conjI, Nonce_supply, Key_supply]))) |
|
242 |
||
243 |
(*Tactic for possibility theorems (ML script version)*) |
|
244 |
fun possibility_tac state = gen_possibility_tac (simpset()) state |
|
245 |
||
246 |
(*For harder protocols (such as Recur) where we have to set up some |
|
247 |
nonces and keys initially*) |
|
248 |
fun basic_possibility_tac st = st |> |
|
249 |
REPEAT |
|
250 |
(ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) |
|
251 |
THEN |
|
252 |
REPEAT_FIRST (resolve_tac [refl, conjI])) |
|
253 |
*} |
|
254 |
||
13956 | 255 |
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |
13926 | 256 |
|
257 |
lemma subset_Compl_range: "A <= - (range shrK) ==> shrK x \<notin> A" |
|
258 |
by blast |
|
259 |
||
260 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H" |
|
261 |
by blast |
|
262 |
||
13956 | 263 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key`(insert K KK) \<union> C" |
13926 | 264 |
by blast |
265 |
||
266 |
(** Reverse the normal simplification of "image" to build up (not break down) |
|
267 |
the set of keys. Use analz_insert_eq with (Un_upper2 RS analz_mono) to |
|
268 |
erase occurrences of forwarded message components (X). **) |
|
269 |
||
270 |
lemmas analz_image_freshK_simps = |
|
271 |
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*} |
|
272 |
disj_comms |
|
273 |
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset |
|
274 |
analz_insert_eq Un_upper2 [THEN analz_mono, THEN [2] rev_subsetD] |
|
275 |
insert_Key_singleton subset_Compl_range |
|
276 |
Key_not_used insert_Key_image Un_assoc [THEN sym] |
|
277 |
||
278 |
(*Lemma for the trivial direction of the if-and-only-if*) |
|
279 |
lemma analz_image_freshK_lemma: |
|
280 |
"(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==> |
|
281 |
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)" |
|
282 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
|
283 |
||
284 |
ML |
|
285 |
{* |
|
286 |
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; |
|
287 |
||
288 |
val analz_image_freshK_ss = |
|
289 |
simpset() delsimps [image_insert, image_Un] |
|
290 |
delsimps [imp_disjL] (*reduces blow-up*) |
|
291 |
addsimps thms "analz_image_freshK_simps" |
|
292 |
*} |
|
293 |
||
294 |
||
11104 | 295 |
|
296 |
(*Lets blast_tac perform this step without needing the simplifier*) |
|
297 |
lemma invKey_shrK_iff [iff]: |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
298 |
"(Key (invKey K) \<in> X) = (Key K \<in> X)" |
13507 | 299 |
by auto |
11104 | 300 |
|
301 |
(*Specialized methods*) |
|
302 |
||
303 |
method_setup analz_freshK = {* |
|
304 |
Method.no_args |
|
305 |
(Method.METHOD |
|
13907 | 306 |
(fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
11104 | 307 |
REPEAT_FIRST (rtac analz_image_freshK_lemma), |
308 |
ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} |
|
309 |
"for proving the Session Key Compromise theorem" |
|
310 |
||
311 |
method_setup possibility = {* |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
312 |
Method.ctxt_args (fn ctxt => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
313 |
Method.METHOD (fn facts => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11230
diff
changeset
|
314 |
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
11104 | 315 |
"for proving possibility theorems" |
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
316 |
|
12415
74977582a585
Slightly generalized the agents' knowledge theorems
paulson
parents:
11270
diff
changeset
|
317 |
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)" |
74977582a585
Slightly generalized the agents' knowledge theorems
paulson
parents:
11270
diff
changeset
|
318 |
by (induct e, auto simp: knows_Cons) |
74977582a585
Slightly generalized the agents' knowledge theorems
paulson
parents:
11270
diff
changeset
|
319 |
|
1934 | 320 |
end |