author | urbanc |
Wed, 08 Mar 2006 18:00:00 +0100 | |
changeset 19218 | 47b05ebe106b |
parent 18749 | 31c2af8b0c60 |
child 20048 | a7964311f1fb |
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 |
||
16417 | 11 |
theory Public imports Event begin |
13922 | 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 |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
18 |
datatype keymode = Signature | Encryption |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
19 |
|
2318 | 20 |
consts |
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
21 |
publicKey :: "[keymode,agent] => key" |
2318 | 22 |
|
23 |
syntax |
|
13922 | 24 |
pubEK :: "agent => key" |
25 |
pubSK :: "agent => key" |
|
26 |
||
27 |
privateKey :: "[bool,agent] => key" |
|
28 |
priEK :: "agent => key" |
|
29 |
priSK :: "agent => key" |
|
30 |
||
31 |
translations |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
32 |
"pubEK" == "publicKey Encryption" |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
33 |
"pubSK" == "publicKey Signature" |
13922 | 34 |
|
35 |
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
|
36 |
"privateKey b A" == "invKey (publicKey b A)" |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
37 |
"priEK A" == "privateKey Encryption A" |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
38 |
"priSK A" == "privateKey Signature A" |
13922 | 39 |
|
40 |
||
41 |
text{*These translations give backward compatibility. They represent the |
|
42 |
simple situation where the signature and encryption keys are the same.*} |
|
43 |
syntax |
|
44 |
pubK :: "agent => key" |
|
45 |
priK :: "agent => key" |
|
46 |
||
47 |
translations |
|
48 |
"pubK A" == "pubEK A" |
|
49 |
"priK A" == "invKey (pubEK A)" |
|
50 |
||
51 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
52 |
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
|
53 |
@{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
|
54 |
specification (publicKey) |
13922 | 55 |
injective_publicKey: |
56 |
"publicKey b A = publicKey c A' ==> b=c & A=A'" |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
57 |
apply (rule exI [of _ |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
58 |
"%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + keymode_case 0 1 b"]) |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
59 |
apply (auto simp add: inj_on_def split: agent.split keymode.split) |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
60 |
apply presburger+ |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
61 |
done |
13922 | 62 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
63 |
|
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13956
diff
changeset
|
64 |
axioms |
13922 | 65 |
(*No private key equals any public key (essential to ensure that private |
66 |
keys are private!) *) |
|
67 |
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'" |
|
68 |
||
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
69 |
lemmas publicKey_neq_privateKey = privateKey_neq_publicKey [THEN not_sym] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
70 |
declare publicKey_neq_privateKey [iff] |
13922 | 71 |
|
72 |
||
13926 | 73 |
subsection{*Basic properties of @{term pubK} and @{term priK}*} |
13922 | 74 |
|
18570 | 75 |
lemma publicKey_inject [iff]: "(publicKey b A = publicKey c A') = (b=c & A=A')" |
13922 | 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 |
||
18570 | 140 |
text{*Injectiveness: Agents' long-term keys are distinct.*} |
141 |
lemmas shrK_injective = inj_shrK [THEN inj_eq] |
|
142 |
declare shrK_injective [iff] |
|
13922 | 143 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
144 |
lemma invKey_shrK [simp]: "invKey (shrK A) = shrK A" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
145 |
by (simp add: invKey_K) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
146 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
147 |
lemma analz_shrK_Decrypt: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
148 |
"[| 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
|
149 |
by auto |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
150 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
151 |
lemma analz_Decrypt': |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
152 |
"[| 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
|
153 |
by (auto simp add: invKey_K) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
154 |
|
13922 | 155 |
lemma priK_neq_shrK [iff]: "shrK A \<noteq> privateKey b C" |
13926 | 156 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 157 |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
158 |
lemmas shrK_neq_priK = priK_neq_shrK [THEN not_sym] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
159 |
declare shrK_neq_priK [simp] |
13922 | 160 |
|
161 |
lemma pubK_neq_shrK [iff]: "shrK A \<noteq> publicKey b C" |
|
13926 | 162 |
by (simp add: symKeys_neq_imp_neq) |
13922 | 163 |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
164 |
lemmas shrK_neq_pubK = pubK_neq_shrK [THEN not_sym] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
165 |
declare shrK_neq_pubK [simp] |
13922 | 166 |
|
167 |
lemma priEK_noteq_shrK [simp]: "priEK A \<noteq> shrK B" |
|
168 |
by auto |
|
169 |
||
170 |
lemma publicKey_notin_image_shrK [simp]: "publicKey b x \<notin> shrK ` AA" |
|
171 |
by auto |
|
172 |
||
173 |
lemma privateKey_notin_image_shrK [simp]: "privateKey b x \<notin> shrK ` AA" |
|
174 |
by auto |
|
175 |
||
176 |
lemma shrK_notin_image_publicKey [simp]: "shrK x \<notin> publicKey b ` AA" |
|
177 |
by auto |
|
178 |
||
179 |
lemma shrK_notin_image_privateKey [simp]: "shrK x \<notin> invKey ` publicKey b ` AA" |
|
180 |
by auto |
|
181 |
||
182 |
lemma shrK_image_eq [simp]: "(shrK x \<in> shrK ` AA) = (x \<in> AA)" |
|
183 |
by auto |
|
184 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
185 |
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
|
186 |
declare invKey_K [simp] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
187 |
|
13922 | 188 |
|
189 |
subsection{*Initial States of Agents*} |
|
190 |
||
191 |
text{*Note: for all practical purposes, all that matters is the initial |
|
192 |
knowledge of the Spy. All other agents are automata, merely following the |
|
193 |
protocol.*} |
|
2318 | 194 |
|
5183 | 195 |
primrec |
2318 | 196 |
(*Agents know their private key and all public keys*) |
13922 | 197 |
initState_Server: |
198 |
"initState Server = |
|
199 |
{Key (priEK Server), Key (priSK Server)} \<union> |
|
200 |
(Key ` range pubEK) \<union> (Key ` range pubSK) \<union> (Key ` range shrK)" |
|
201 |
||
202 |
initState_Friend: |
|
203 |
"initState (Friend i) = |
|
204 |
{Key (priEK(Friend i)), Key (priSK(Friend i)), Key (shrK(Friend i))} \<union> |
|
205 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
206 |
||
207 |
initState_Spy: |
|
208 |
"initState Spy = |
|
209 |
(Key ` invKey ` pubEK ` bad) \<union> (Key ` invKey ` pubSK ` bad) \<union> |
|
210 |
(Key ` shrK ` bad) \<union> |
|
211 |
(Key ` range pubEK) \<union> (Key ` range pubSK)" |
|
212 |
||
213 |
||
214 |
text{*These lemmas allow reasoning about @{term "used evs"} rather than |
|
13935 | 215 |
@{term "knows Spy evs"}, which is useful when there are private Notes. |
216 |
Because they depend upon the definition of @{term initState}, they cannot |
|
217 |
be moved up.*} |
|
13922 | 218 |
|
219 |
lemma used_parts_subset_parts [rule_format]: |
|
220 |
"\<forall>X \<in> used evs. parts {X} \<subseteq> used evs" |
|
221 |
apply (induct evs) |
|
222 |
prefer 2 |
|
223 |
apply (simp add: used_Cons) |
|
224 |
apply (rule ballI) |
|
13935 | 225 |
apply (case_tac a, auto) |
226 |
apply (auto dest!: parts_cut) |
|
13922 | 227 |
txt{*Base case*} |
13935 | 228 |
apply (simp add: used_Nil) |
13922 | 229 |
done |
230 |
||
231 |
lemma MPair_used_D: "{|X,Y|} \<in> used H ==> X \<in> used H & Y \<in> used H" |
|
232 |
by (drule used_parts_subset_parts, simp, blast) |
|
233 |
||
17990 | 234 |
text{*There was a similar theorem in Event.thy, so perhaps this one can |
235 |
be moved up if proved directly by induction.*} |
|
13922 | 236 |
lemma MPair_used [elim!]: |
237 |
"[| {|X,Y|} \<in> used H; |
|
238 |
[| X \<in> used H; Y \<in> used H |] ==> P |] |
|
239 |
==> P" |
|
240 |
by (blast dest: MPair_used_D) |
|
241 |
||
242 |
||
243 |
text{*Rewrites should not refer to @{term "initState(Friend i)"} because |
|
244 |
that expression is not in normal form.*} |
|
245 |
||
246 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
247 |
apply (unfold keysFor_def) |
|
248 |
apply (induct_tac "C") |
|
249 |
apply (auto intro: range_eqI) |
|
250 |
done |
|
251 |
||
252 |
lemma Crypt_notin_initState: "Crypt K X \<notin> parts (initState B)" |
|
253 |
by (induct B, auto) |
|
254 |
||
13935 | 255 |
lemma Crypt_notin_used_empty [simp]: "Crypt K X \<notin> used []" |
256 |
by (simp add: Crypt_notin_initState used_Nil) |
|
257 |
||
13922 | 258 |
(*** Basic properties of shrK ***) |
259 |
||
260 |
(*Agents see their own shared keys!*) |
|
261 |
lemma shrK_in_initState [iff]: "Key (shrK A) \<in> initState A" |
|
13926 | 262 |
by (induct_tac "A", auto) |
13922 | 263 |
|
264 |
lemma shrK_in_knows [iff]: "Key (shrK A) \<in> knows A evs" |
|
265 |
by (simp add: initState_subset_knows [THEN subsetD]) |
|
266 |
||
267 |
lemma shrK_in_used [iff]: "Key (shrK A) \<in> used evs" |
|
13926 | 268 |
by (rule initState_into_used, blast) |
13922 | 269 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
270 |
|
13922 | 271 |
(** Fresh keys never clash with long-term shared keys **) |
272 |
||
273 |
(*Used in parts_induct_tac and analz_Fake_tac to distinguish session keys |
|
274 |
from long-term shared keys*) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
275 |
lemma Key_not_used [simp]: "Key K \<notin> used evs ==> K \<notin> range shrK" |
13926 | 276 |
by blast |
13922 | 277 |
|
278 |
lemma shrK_neq: "Key K \<notin> used evs ==> shrK B \<noteq> K" |
|
13926 | 279 |
by blast |
13922 | 280 |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
281 |
lemmas neq_shrK = shrK_neq [THEN not_sym] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
282 |
declare neq_shrK [simp] |
2318 | 283 |
|
284 |
||
13922 | 285 |
subsection{*Function @{term spies} *} |
286 |
||
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
287 |
lemma not_SignatureE [elim!]: "b \<noteq> Signature \<Longrightarrow> b = Encryption" |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
288 |
by (cases b, auto) |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
289 |
|
13922 | 290 |
text{*Agents see their own private keys!*} |
291 |
lemma priK_in_initState [iff]: "Key (privateKey b A) \<in> initState A" |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
292 |
by (cases A, auto) |
13922 | 293 |
|
294 |
text{*Agents see all public keys!*} |
|
295 |
lemma publicKey_in_initState [iff]: "Key (publicKey b A) \<in> initState B" |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
296 |
by (cases B, auto) |
13922 | 297 |
|
298 |
text{*All public keys are visible*} |
|
299 |
lemma spies_pubK [iff]: "Key (publicKey b A) \<in> spies evs" |
|
300 |
apply (induct_tac "evs") |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
301 |
apply (auto simp add: imageI knows_Cons split add: event.split) |
13922 | 302 |
done |
303 |
||
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
304 |
lemmas analz_spies_pubK = spies_pubK [THEN analz.Inj] |
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
305 |
declare analz_spies_pubK [iff] |
13922 | 306 |
|
307 |
text{*Spy sees private keys of bad agents!*} |
|
308 |
lemma Spy_spies_bad_privateKey [intro!]: |
|
309 |
"A \<in> bad ==> Key (privateKey b A) \<in> spies evs" |
|
310 |
apply (induct_tac "evs") |
|
18749
31c2af8b0c60
replacement of bool by a datatype (making problems first-order). More lemma names
paulson
parents:
18570
diff
changeset
|
311 |
apply (auto simp add: imageI knows_Cons split add: event.split) |
13922 | 312 |
done |
313 |
||
314 |
text{*Spy sees long-term shared keys of bad agents!*} |
|
315 |
lemma Spy_spies_bad_shrK [intro!]: |
|
316 |
"A \<in> bad ==> Key (shrK A) \<in> spies evs" |
|
317 |
apply (induct_tac "evs") |
|
318 |
apply (simp_all add: imageI knows_Cons split add: event.split) |
|
319 |
done |
|
320 |
||
321 |
lemma publicKey_into_used [iff] :"Key (publicKey b A) \<in> used evs" |
|
322 |
apply (rule initState_into_used) |
|
323 |
apply (rule publicKey_in_initState [THEN parts.Inj]) |
|
324 |
done |
|
325 |
||
326 |
lemma privateKey_into_used [iff]: "Key (privateKey b A) \<in> used evs" |
|
327 |
apply(rule initState_into_used) |
|
328 |
apply(rule priK_in_initState [THEN parts.Inj]) |
|
329 |
done |
|
330 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
331 |
(*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
|
332 |
lemma Crypt_Spy_analz_bad: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
333 |
"[| 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
|
334 |
==> X \<in> analz (knows Spy evs)" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
335 |
by force |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
336 |
|
13922 | 337 |
|
338 |
subsection{*Fresh Nonces*} |
|
339 |
||
340 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
13926 | 341 |
by (induct_tac "B", auto) |
13922 | 342 |
|
343 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
13926 | 344 |
by (simp add: used_Nil) |
13922 | 345 |
|
11104 | 346 |
|
13922 | 347 |
subsection{*Supply fresh nonces for possibility theorems*} |
348 |
||
349 |
text{*In any trace, there is an upper bound N on the greatest nonce in use*} |
|
350 |
lemma Nonce_supply_lemma: "EX N. ALL n. N<=n --> Nonce n \<notin> used evs" |
|
351 |
apply (induct_tac "evs") |
|
13926 | 352 |
apply (rule_tac x = 0 in exI) |
13922 | 353 |
apply (simp_all (no_asm_simp) add: used_Cons split add: event.split) |
354 |
apply safe |
|
355 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
|
356 |
done |
|
357 |
||
358 |
lemma Nonce_supply1: "EX N. Nonce N \<notin> used evs" |
|
13926 | 359 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
13922 | 360 |
|
361 |
lemma Nonce_supply: "Nonce (@ N. Nonce N \<notin> used evs) \<notin> used evs" |
|
362 |
apply (rule Nonce_supply_lemma [THEN exE]) |
|
13926 | 363 |
apply (rule someI, fast) |
13922 | 364 |
done |
365 |
||
13956 | 366 |
subsection{*Specialized Rewriting for Theorems About @{term analz} and Image*} |
13922 | 367 |
|
368 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} Un H" |
|
13926 | 369 |
by blast |
11104 | 370 |
|
13922 | 371 |
lemma insert_Key_image: "insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C" |
13926 | 372 |
by blast |
13922 | 373 |
|
374 |
ML |
|
375 |
{* |
|
376 |
val Key_not_used = thm "Key_not_used"; |
|
377 |
val insert_Key_singleton = thm "insert_Key_singleton"; |
|
378 |
val insert_Key_image = thm "insert_Key_image"; |
|
379 |
*} |
|
380 |
||
381 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
382 |
lemma Crypt_imp_keysFor :"[|Crypt K X \<in> H; K \<in> symKeys|] ==> K \<in> keysFor H" |
13926 | 383 |
by (drule Crypt_imp_invKey_keysFor, simp) |
13922 | 384 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
385 |
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
|
386 |
Session Key Compromise Theorem*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
387 |
lemma analz_image_freshK_lemma: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
388 |
"(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
|
389 |
(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
|
390 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
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 |
lemmas analz_image_freshK_simps = |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
393 |
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
|
394 |
disj_comms |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
395 |
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
|
396 |
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
|
397 |
insert_Key_singleton |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
398 |
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
|
399 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
400 |
ML |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
401 |
{* |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
402 |
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
|
403 |
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
|
404 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
405 |
val analz_image_freshK_ss = |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
406 |
simpset() delsimps [image_insert, image_Un] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
407 |
delsimps [imp_disjL] (*reduces blow-up*) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
408 |
addsimps thms "analz_image_freshK_simps" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
409 |
*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
410 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
411 |
method_setup analz_freshK = {* |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
412 |
Method.no_args |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
413 |
(Method.METHOD |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
414 |
(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
|
415 |
REPEAT_FIRST (rtac analz_image_freshK_lemma), |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
416 |
ALLGOALS (asm_simp_tac analz_image_freshK_ss)])) *} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
417 |
"for proving the Session Key Compromise theorem" |
13922 | 418 |
|
419 |
subsection{*Specialized Methods for Possibility Theorems*} |
|
420 |
||
421 |
ML |
|
422 |
{* |
|
423 |
val Nonce_supply = thm "Nonce_supply"; |
|
424 |
||
425 |
(*Tactic for possibility theorems (Isar interface)*) |
|
426 |
fun gen_possibility_tac ss state = state |> |
|
427 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
|
428 |
(ALLGOALS (simp_tac (ss delsimps [used_Says])) |
|
429 |
THEN |
|
430 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
431 |
resolve_tac [refl, conjI, Nonce_supply])) |
|
432 |
||
433 |
(*Tactic for possibility theorems (ML script version)*) |
|
434 |
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
|
435 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
436 |
(*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
|
437 |
nonces and keys initially*) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
438 |
fun basic_possibility_tac st = st |> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
439 |
REPEAT |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
440 |
(ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver)) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
441 |
THEN |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
442 |
REPEAT_FIRST (resolve_tac [refl, conjI])) |
13922 | 443 |
*} |
11104 | 444 |
|
445 |
method_setup possibility = {* |
|
11270
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
446 |
Method.ctxt_args (fn ctxt => |
a315a3862bb4
better treatment of methods: uses Method.ctxt_args to refer to current
paulson
parents:
11104
diff
changeset
|
447 |
Method.METHOD (fn facts => |
15032 | 448 |
gen_possibility_tac (local_simpset_of ctxt))) *} |
11104 | 449 |
"for proving possibility theorems" |
2318 | 450 |
|
451 |
end |