author | wenzelm |
Sat, 05 Jun 2004 13:07:04 +0200 | |
changeset 14872 | 3f2144aebd76 |
parent 14261 | 6c418d139f74 |
child 15032 | 02aed07e01bf |
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 |
||
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset
|
6 |
Theory of Public Keys (common to all public-key protocols) |
2318 | 7 |
|
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3478
diff
changeset
|
8 |
Private and public keys; initial states of agents |
2318 | 9 |
*) |
10 |
||
13922 | 11 |
theory Public = Event: |
12 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
lemma invKey_K: "K \<in> symKeys ==> invKey K = K" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
14 |
by (simp add: symKeys_def) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
15 |
|
13922 | 16 |
subsection{*Asymmetric Keys*} |
2318 | 17 |
|
18 |
consts |
|
13922 | 19 |
(*the bool is TRUE if a signing key*) |
20 |
publicKey :: "[bool,agent] => key" |
|
2318 | 21 |
|
22 |
syntax |
|
13922 | 23 |
pubEK :: "agent => key" |
24 |
pubSK :: "agent => key" |
|
25 |
||
26 |
privateKey :: "[bool,agent] => key" |
|
27 |
priEK :: "agent => key" |
|
28 |
priSK :: "agent => key" |
|
29 |
||
30 |
translations |
|
31 |
"pubEK" == "publicKey False" |
|
32 |
"pubSK" == "publicKey True" |
|
33 |
||
34 |
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
|
35 |
"privateKey b A" == "invKey (publicKey b A)" |
|
36 |
"priEK A" == "privateKey False A" |
|
37 |
"priSK A" == "privateKey True A" |
|
38 |
||
39 |
||
40 |
text{*These translations give backward compatibility. They represent the |
|
41 |
simple situation where the signature and encryption keys are the same.*} |
|
42 |
syntax |
|
43 |
pubK :: "agent => key" |
|
44 |
priK :: "agent => key" |
|
45 |
||
46 |
translations |
|
47 |
"pubK A" == "pubEK A" |
|
48 |
"priK A" == "invKey (pubEK A)" |
|
49 |
||
50 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
51 |
text{*By freeness of agents, no two agents have the same key. Since |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
52 |
@{term "True\<noteq>False"}, no agent has identical signing and encryption keys*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
53 |
specification (publicKey) |
13922 | 54 |
injective_publicKey: |
55 |
"publicKey b A = publicKey c A' ==> b=c & A=A'" |
|
14261 | 56 |
apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"]) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
57 |
apply (auto simp add: inj_on_def split: agent.split, presburger+) |
14133 | 58 |
(*faster would be this: |
14261 | 59 |
apply (simp split: agent.split, auto) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
60 |
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
14133 | 61 |
*) |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
62 |
done |
13922 | 63 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
64 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
65 |
axioms |
13922 | 66 |
(*No private key equals any public key (essential to ensure that private |
67 |
keys are private!) *) |
|
68 |
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'" |
|
69 |
||
13926 | 70 |
declare privateKey_neq_publicKey [THEN not_sym, iff] |
13922 | 71 |
|
72 |
||
13926 | 73 |
subsection{*Basic properties of @{term pubK} and @{term priK}*} |
13922 | 74 |
|
75 |
lemma [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')" |
|
76 |
by (blast dest!: injective_publicKey) |
|
77 |
||
78 |
lemma not_symKeys_pubK [iff]: "publicKey b A \<notin> symKeys" |
|
13926 | 79 |
by (simp add: symKeys_def) |
13922 | 80 |
|
81 |
lemma not_symKeys_priK [iff]: "privateKey b A \<notin> symKeys" |
|
13926 | 82 |
by (simp add: symKeys_def) |
13922 | 83 |
|
84 |
lemma symKey_neq_priEK: "K \<in> symKeys ==> K \<noteq> priEK A" |
|
85 |
by auto |
|
86 |
||
87 |
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) ==> K \<noteq> K'" |
|
13926 | 88 |
by blast |
13922 | 89 |
|
90 |
lemma symKeys_invKey_iff [iff]: "(invKey K \<in> symKeys) = (K \<in> symKeys)" |
|
13926 | 91 |
by (unfold symKeys_def, auto) |
2318 | 92 |
|
13922 | 93 |
lemma analz_symKeys_Decrypt: |
94 |
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] |
|
95 |
==> X \<in> analz H" |
|
96 |
by (auto simp add: symKeys_def) |
|
97 |
||
98 |
||
99 |
||
100 |
subsection{*"Image" equations that hold for injective functions*} |
|
101 |
||
102 |
lemma invKey_image_eq [simp]: "(invKey x \<in> invKey`A) = (x \<in> A)" |
|
13926 | 103 |
by auto |
13922 | 104 |
|
105 |
(*holds because invKey is injective*) |
|
106 |
lemma publicKey_image_eq [simp]: |
|
107 |
"(publicKey b x \<in> publicKey c ` AA) = (b=c & x \<in> AA)" |
|
108 |
by auto |
|
109 |
||
110 |
lemma privateKey_notin_image_publicKey [simp]: "privateKey b x \<notin> publicKey c ` AA" |
|
13926 | 111 |
by auto |
13922 | 112 |
|
113 |
lemma privateKey_image_eq [simp]: |
|
114 |
"(privateKey b A \<in> invKey ` publicKey c ` AS) = (b=c & A\<in>AS)" |
|
115 |
by auto |
|
116 |
||
117 |
lemma publicKey_notin_image_privateKey [simp]: "publicKey b A \<notin> invKey ` publicKey c ` AS" |
|
13926 | 118 |
by auto |
13922 | 119 |
|
120 |
||
121 |
subsection{*Symmetric Keys*} |
|
122 |
||
123 |
text{*For some protocols, it is convenient to equip agents with symmetric as |
|
124 |
well as asymmetric keys. The theory @{text Shared} assumes that all keys |
|
125 |
are symmetric.*} |
|
126 |
||
127 |
consts |
|
128 |
shrK :: "agent => key" --{*long-term shared keys*} |
|
129 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
130 |
specification (shrK) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
131 |
inj_shrK: "inj shrK" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
132 |
--{*No two agents have the same long-term key*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
133 |
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
|
134 |
apply (simp add: inj_on_def split: agent.split) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
135 |
done |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
136 |
|
13922 | 137 |
axioms |
138 |
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*} |
|
139 |
||
140 |
(*Injectiveness: Agents' long-term keys are distinct.*) |
|
141 |
declare inj_shrK [THEN inj_eq, iff] |
|
142 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
143 |
lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
144 |
by (simp add: invKey_K) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
145 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
146 |
lemma analz_shrK_Decrypt: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
147 |
"[| Crypt (shrK A) X \<in> analz H; Key(shrK A) \<in> analz H |] ==> X \<in> analz H" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
148 |
by auto |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
149 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
150 |
lemma analz_Decrypt': |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
151 |
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] ==> X \<in> analz H" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
152 |
by (auto simp add: invKey_K) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
153 |
|
13922 | 154 |
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C" |
13926 | 155 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 156 |
|
157 |
declare priK_neq_shrK [THEN not_sym, simp] |
|
158 |
||
159 |
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C" |
|
13926 | 160 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 161 |
|
162 |
declare pubK_neq_shrK [THEN not_sym, simp] |
|
163 |
||
164 |
lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" |
|
165 |
by auto |
|
166 |
||
167 |
lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA" |
|
168 |
by auto |
|
169 |
||
170 |
lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA" |
|
171 |
by auto |
|
172 |
||
173 |
lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA" |
|
174 |
by auto |
|
175 |
||
176 |
lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" |
|
177 |
by auto |
|
178 |
||
179 |
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)" |
|
180 |
by auto |
|
181 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
182 |
text{*For some reason, moving this up can make some proofs loop!*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
183 |
declare invKey_K [simp] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
184 |
|
13922 | 185 |
|
186 |
subsection{*Initial States of Agents*} |
|
187 |
||
188 |
text{*Note: for all practical purposes, all that matters is the initial |
|
189 |
knowledge of the Spy. All other agents are automata, merely following the |
|
190 |
protocol.*} |
|
2318 | 191 |
|
5183 | 192 |
primrec |
2318 | 193 |
(*Agents know their private key and all public keys*) |
13922 | 194 |
initState_Server: |
195 |
"initState Server = |
|
196 |
{Key (priEK Server), Key (priSK Server)} \<union> |
|
197 |
(Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)" |
|
198 |
||
199 |
initState_Friend: |
|
200 |
"initState (Friend i) = |
|
201 |
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> |
|
202 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
203 |
||
204 |
initState_Spy: |
|
205 |
"initState Spy = |
|
206 |
(Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> |
|
207 |
(Key ` shrK ` bad) \<union> |
|
208 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
209 |
||
210 |
||
211 |
text{*These lemmas allow reasoning about @{term "used evs"} rather than |
|
13935 | 212 |
@{term "knows Spy evs"}, which is useful when there are private Notes. |
213 |
Because they depend upon the definition of @{term initState}, they cannot |
|
214 |
be moved up.*} |
|
13922 | 215 |
|
216 |
lemma used_parts_subset_parts [rule_format]: |
|
217 |
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs" |
|
218 |
apply (induct evs) |
|
219 |
prefer 2 |
|
220 |
apply (simp add: used_Cons) |
|
221 |
apply (rule ballI) |
|
13935 | 222 |
apply (case_tac a, auto) |
223 |
apply (auto dest!: parts_cut) |
|
13922 | 224 |
txt{*Base case*} |
13935 | 225 |
apply (simp add: used_Nil) |
13922 | 226 |
done |
227 |
||
228 |
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H" |
|
229 |
by (drule used_parts_subset_parts, simp, blast) |
|
230 |
||
231 |
lemma MPair_used [elim!]: |
|
232 |
"[| {|X,Y|} \<in> used H; |
|
233 |
[| X \<in> used H; Y \<in> used H |] ==> P |] |
|
234 |
==> P" |
|
235 |
by (blast dest: MPair_used_D) |
|
236 |
||
237 |
||
238 |
text{*Rewrites should not refer to @{term "initState(Friend i)"} because |
|
239 |
that expression is not in normal form.*} |
|
240 |
||
241 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
242 |
apply (unfold keysFor_def) |
|
243 |
apply (induct_tac "C") |
|
244 |
apply (auto intro: range_eqI) |
|
245 |
done |
|
246 |
||
247 |
lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)" |
|
248 |
by (induct B, auto) |
|
249 |
||
13935 | 250 |
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []" |
251 |
by (simp add: Crypt_notin_initState used_Nil) |
|
252 |
||
13922 | 253 |
(*** Basic properties of shrK ***) |
254 |
||
255 |
(*Agents see their own shared keys!*) |
|
256 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" |
|
13926 | 257 |
by (induct_tac "A", auto) |
13922 | 258 |
|
259 |
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs" |
|
260 |
by (simp add: initState_subset_knows [THEN subsetD]) |
|
261 |
||
262 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" |
|
13926 | 263 |
by (rule initState_into_used, blast) |
13922 | 264 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
265 |
|
13922 | 266 |
(** Fresh keys never clash with long-term shared keys **) |
267 |
||
268 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
269 |
from long-term shared keys*) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
270 |
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" |
13926 | 271 |
by blast |
13922 | 272 |
|
273 |
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K" |
|
13926 | 274 |
by blast |
13922 | 275 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
276 |
declare shrK_neq [THEN not_sym, simp] |
2318 | 277 |
|
278 |
||
13922 | 279 |
subsection{*Function @{term spies} *} |
280 |
||
281 |
text{*Agents see their own private keys!*} |
|
282 |
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A" |
|
13926 | 283 |
by (induct_tac "A", auto) |
13922 | 284 |
|
285 |
text{*Agents see all public keys!*} |
|
286 |
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B" |
|
13926 | 287 |
by (case_tac "B", auto) |
13922 | 288 |
|
289 |
text{*All public keys are visible*} |
|
290 |
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs" |
|
291 |
apply (induct_tac "evs") |
|
292 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
293 |
done |
|
294 |
||
295 |
declare spies_pubK [THEN analz.Inj, iff] |
|
296 |
||
297 |
text{*Spy sees private keys of bad agents!*} |
|
298 |
lemma Spy_spies_bad_privateKey [intro!]: |
|
299 |
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs" |
|
300 |
apply (induct_tac "evs") |
|
301 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
302 |
done |
|
303 |
||
304 |
text{*Spy sees long-term shared keys of bad agents!*} |
|
305 |
lemma Spy_spies_bad_shrK [intro!]: |
|
306 |
"A \<in> bad ==> Key (shrK A) \<in> spies evs" |
|
307 |
apply (induct_tac "evs") |
|
308 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
309 |
done |
|
310 |
||
311 |
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs" |
|
312 |
apply (rule initState_into_used) |
|
313 |
apply (rule publicKey_in_initState [THEN parts.Inj]) |
|
314 |
done |
|
315 |
||
316 |
lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs" |
|
317 |
apply(rule initState_into_used) |
|
318 |
apply(rule priK_in_initState [THEN parts.Inj]) |
|
319 |
done |
|
320 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
321 |
(*For case analysis on whether or not an agent is compromised*) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
322 |
lemma Crypt_Spy_analz_bad: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
323 |
"[| Crypt (shrK A) X \<in> analz (knows Spy evs); A \<in> bad |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
324 |
==> X \<in> analz (knows Spy evs)" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
325 |
by force |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
326 |
|
13922 | 327 |
|
328 |
subsection{*Fresh Nonces*} |
|
329 |
||
330 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
13926 | 331 |
by (induct_tac "B", auto) |
13922 | 332 |
|
333 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
13926 | 334 |
by (simp add: used_Nil) |
13922 | 335 |
|
11104 | 336 |
|
13922 | 337 |
subsection{*Supply fresh nonces for possibility theorems*} |
338 |
||
339 |
text{*In any trace, there is an upper bound N on the greatest nonce in use*} |
|
340 |
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
|
341 |
apply (induct_tac "evs") |
|
13926 | 342 |
apply (rule_tac x = 0 in exI) |
13922 | 343 |
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
344 |
apply safe |
|
345 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
|
346 |
done |
|
347 |
||
348 |
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |
|
13926 | 349 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
13922 | 350 |
|
351 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
|
352 |
apply (rule Nonce_supply_lemma [THEN exE]) |
|
13926 | 353 |
apply (rule someI, fast) |
13922 | 354 |
done |
355 |
||
13956 | 356 |
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |
13922 | 357 |
|
358 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" |
|
13926 | 359 |
by blast |
11104 | 360 |
|
13922 | 361 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C" |
13926 | 362 |
by blast |
13922 | 363 |
|
364 |
ML |
|
365 |
{* |
|
366 |
val Key_not_used = thm "Key_not_used"; |
|
367 |
val insert_Key_singleton = thm "insert_Key_singleton"; |
|
368 |
val insert_Key_image = thm "insert_Key_image"; |
|
369 |
*} |
|
370 |
||
371 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
372 |
lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H" |
13926 | 373 |
by (drule Crypt_imp_invKey_keysFor, simp) |
13922 | 374 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
375 |
text{*Lemma for the trivial direction of the if-and-only-if of the |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
376 |
Session Key Compromise Theorem*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
377 |
lemma analz_image_freshK_lemma: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
378 |
"(Key K \<in> analz (Key`nE \<union> H)) --> (K \<in> nE | Key K \<in> analz H) ==> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
379 |
(Key K \<in> analz (Key`nE \<union> H)) = (K \<in> nE | Key K \<in> analz H)" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
380 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
381 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
382 |
lemmas analz_image_freshK_simps = |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
383 |
simp_thms mem_simps --{*these two allow its use with @{text "only:"}*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
384 |
disj_comms |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
385 |
image_insert [THEN sym] image_Un [THEN sym] empty_subsetI insert_subset |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
386 |
analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
387 |
insert_Key_singleton |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
388 |
Key_not_used insert_Key_image Un_assoc [THEN sym] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
389 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
390 |
ML |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
391 |
{* |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
392 |
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma"; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
393 |
val analz_image_freshK_simps = thms "analz_image_freshK_simps"; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
394 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
395 |
val analz_image_freshK_ss = |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
396 |
simpset() delsimps [image_insert, image_Un] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
397 |
delsimps [imp_disjL] (*reduces blow-up*) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
398 |
addsimps thms "analz_image_freshK_simps" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
399 |
*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
400 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
401 |
method_setup analz_freshK = {* |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
402 |
Method.no_args |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
403 |
(Method.METHOD |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
404 |
(fn facts => EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]), |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
405 |
REPEAT_FIRST (rtac analz_image_freshK_lemma), |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
406 |
ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
407 |
"for proving the Session Key Compromise theorem" |
13922 | 408 |
|
409 |
subsection{*Specialized Methods for Possibility Theorems*} |
|
410 |
||
411 |
ML |
|
412 |
{* |
|
413 |
val Nonce_supply = thm "Nonce_supply"; |
|
414 |
||
415 |
(*Tactic for possibility theorems (Isar interface)*) |
|
416 |
fun gen_possibility_tac ss state = state |> |
|
417 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
|
418 |
(ALLGOALS (simp_tac (ss delsimps [used_Says])) |
|
419 |
THEN |
|
420 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
421 |
resolve_tac [refl, conjI, Nonce_supply])) |
|
422 |
||
423 |
(*Tactic for possibility theorems (ML script version)*) |
|
424 |
fun possibility_tac state = gen_possibility_tac (simpset()) state |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
425 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
426 |
(*For harder protocols (such as Recur) where we have to set up some |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
427 |
nonces and keys initially*) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
428 |
fun basic_possibility_tac st = st |> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
429 |
REPEAT |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
430 |
(ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
431 |
THEN |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
432 |
REPEAT_FIRST (resolve_tac [refl, conjI])) |
13922 | 433 |
*} |
11104 | 434 |
|
435 |
method_setup possibility = {* |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
436 |
Method.ctxt_args (fn ctxt => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
437 |
Method.METHOD (fn facts => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
438 |
gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *} |
11104 | 439 |
"for proving possibility theorems" |
2318 | 440 |
|
441 |
end |