author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
33028 | 1 |
(* Title: HOL/SET_Protocol/Public_SET.thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
2 |
Author: Giampaolo Bella |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
3 |
Author: Fabio Massacci |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
4 |
Author: Lawrence C Paulson |
14199 | 5 |
*) |
6 |
||
63167 | 7 |
section\<open>The Public-Key Theory, Modified for SET\<close> |
14199 | 8 |
|
33028 | 9 |
theory Public_SET |
10 |
imports Event_SET |
|
11 |
begin |
|
14199 | 12 |
|
63167 | 13 |
subsection\<open>Symmetric and Asymmetric Keys\<close> |
14199 | 14 |
|
63167 | 15 |
text\<open>definitions influenced by the wish to assign asymmetric keys |
14199 | 16 |
- since the beginning - only to RCA and CAs, namely we need a partial |
63167 | 17 |
function on type Agent\<close> |
14199 | 18 |
|
19 |
||
63167 | 20 |
text\<open>The SET specs mention two signature keys for CAs - we only have one\<close> |
14199 | 21 |
|
22 |
consts |
|
67613 | 23 |
publicKey :: "[bool, agent] \<Rightarrow> key" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
24 |
\<comment> \<open>the boolean is TRUE if a signing key\<close> |
14199 | 25 |
|
35068 | 26 |
abbreviation "pubEK == publicKey False" |
27 |
abbreviation "pubSK == publicKey True" |
|
14199 | 28 |
|
35068 | 29 |
(*BEWARE!! priEK, priSK DON'T WORK with inj, range, image, etc.*) |
30 |
abbreviation "priEK A == invKey (pubEK A)" |
|
31 |
abbreviation "priSK A == invKey (pubSK A)" |
|
14199 | 32 |
|
63167 | 33 |
text\<open>By freeness of agents, no two agents have the same key. Since |
69597 | 34 |
\<^term>\<open>True\<noteq>False\<close>, no agent has the same signing and encryption keys.\<close> |
14199 | 35 |
|
36 |
specification (publicKey) |
|
37 |
injective_publicKey: |
|
67613 | 38 |
"publicKey b A = publicKey c A' \<Longrightarrow> b=c \<and> A=A'" |
14218 | 39 |
(*<*) |
14199 | 40 |
apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) |
41 |
apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) |
|
42 |
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+ |
|
43 |
(*or this, but presburger won't abstract out the function applications |
|
44 |
apply presburger+ |
|
45 |
*) |
|
46 |
done |
|
14218 | 47 |
(*>*) |
14199 | 48 |
|
45827 | 49 |
axiomatization where |
14199 | 50 |
(*No private key equals any public key (essential to ensure that private |
51 |
keys are private!) *) |
|
52 |
privateKey_neq_publicKey [iff]: |
|
53 |
"invKey (publicKey b A) \<noteq> publicKey b' A'" |
|
54 |
||
55 |
declare privateKey_neq_publicKey [THEN not_sym, iff] |
|
56 |
||
57 |
||
63167 | 58 |
subsection\<open>Initial Knowledge\<close> |
14199 | 59 |
|
63167 | 60 |
text\<open>This information is not necessary. Each protocol distributes any needed |
14199 | 61 |
certificates, and anyway our proofs require a formalization of the Spy's |
62 |
knowledge only. However, the initial knowledge is as follows: |
|
63 |
All agents know RCA's public keys; |
|
64 |
RCA and CAs know their own respective keys; |
|
65 |
RCA (has already certified and therefore) knows all CAs public keys; |
|
63167 | 66 |
Spy knows all keys of all bad agents.\<close> |
39758 | 67 |
|
68 |
overloading initState \<equiv> "initState" |
|
69 |
begin |
|
70 |
||
71 |
primrec initState where |
|
14218 | 72 |
(*<*) |
14199 | 73 |
initState_CA: |
74 |
"initState (CA i) = |
|
67613 | 75 |
(if i=0 then Key ` ({priEK RCA, priSK RCA} \<union> |
76 |
pubEK ` (range CA) \<union> pubSK ` (range CA)) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
77 |
else {Key (priEK (CA i)), Key (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
78 |
Key (pubEK (CA i)), Key (pubSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
79 |
Key (pubEK RCA), Key (pubSK RCA)})" |
14199 | 80 |
|
39758 | 81 |
| initState_Cardholder: |
14199 | 82 |
"initState (Cardholder i) = |
83 |
{Key (priEK (Cardholder i)), Key (priSK (Cardholder i)), |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
84 |
Key (pubEK (Cardholder i)), Key (pubSK (Cardholder i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
85 |
Key (pubEK RCA), Key (pubSK RCA)}" |
14199 | 86 |
|
39758 | 87 |
| initState_Merchant: |
14199 | 88 |
"initState (Merchant i) = |
89 |
{Key (priEK (Merchant i)), Key (priSK (Merchant i)), |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
90 |
Key (pubEK (Merchant i)), Key (pubSK (Merchant i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
91 |
Key (pubEK RCA), Key (pubSK RCA)}" |
14199 | 92 |
|
39758 | 93 |
| initState_PG: |
14199 | 94 |
"initState (PG i) = |
95 |
{Key (priEK (PG i)), Key (priSK (PG i)), |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
96 |
Key (pubEK (PG i)), Key (pubSK (PG i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
97 |
Key (pubEK RCA), Key (pubSK RCA)}" |
14218 | 98 |
(*>*) |
39758 | 99 |
| initState_Spy: |
67613 | 100 |
"initState Spy = Key ` (invKey ` pubEK ` bad \<union> |
101 |
invKey ` pubSK ` bad \<union> |
|
102 |
range pubEK \<union> range pubSK)" |
|
14199 | 103 |
|
39758 | 104 |
end |
105 |
||
14199 | 106 |
|
63167 | 107 |
text\<open>Injective mapping from agents to PANs: an agent can have only one card\<close> |
14199 | 108 |
|
67613 | 109 |
consts pan :: "agent \<Rightarrow> nat" |
14199 | 110 |
|
111 |
specification (pan) |
|
112 |
inj_pan: "inj pan" |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
113 |
\<comment> \<open>No two agents have the same PAN\<close> |
14218 | 114 |
(*<*) |
14199 | 115 |
apply (rule exI [of _ "nat_of_agent"]) |
116 |
apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) |
|
117 |
done |
|
14218 | 118 |
(*>*) |
14199 | 119 |
|
120 |
declare inj_pan [THEN inj_eq, iff] |
|
121 |
||
122 |
consts |
|
67613 | 123 |
XOR :: "nat*nat \<Rightarrow> nat" \<comment> \<open>no properties are assumed of exclusive-or\<close> |
14199 | 124 |
|
125 |
||
63167 | 126 |
subsection\<open>Signature Primitives\<close> |
14199 | 127 |
|
36866 | 128 |
definition |
14199 | 129 |
(* Signature = Message + signed Digest *) |
67613 | 130 |
sign :: "[key, msg]\<Rightarrow>msg" |
61984 | 131 |
where "sign K X = \<lbrace>X, Crypt K (Hash X) \<rbrace>" |
14199 | 132 |
|
36866 | 133 |
definition |
14199 | 134 |
(* Signature Only = signed Digest Only *) |
67613 | 135 |
signOnly :: "[key, msg]\<Rightarrow>msg" |
36866 | 136 |
where "signOnly K X = Crypt K (Hash X)" |
14199 | 137 |
|
36866 | 138 |
definition |
14199 | 139 |
(* Signature for Certificates = Message + signed Message *) |
67613 | 140 |
signCert :: "[key, msg]\<Rightarrow>msg" |
61984 | 141 |
where "signCert K X = \<lbrace>X, Crypt K X \<rbrace>" |
14199 | 142 |
|
36866 | 143 |
definition |
14199 | 144 |
(* Certification Authority's Certificate. |
145 |
Contains agent name, a key, a number specifying the key's target use, |
|
146 |
a key to sign the entire certificate. |
|
147 |
||
148 |
Should prove if signK=priSK RCA and C=CA i, |
|
149 |
then Ka=pubEK i or pubSK i depending on T ?? |
|
150 |
*) |
|
67613 | 151 |
cert :: "[agent, key, msg, key] \<Rightarrow> msg" |
61984 | 152 |
where "cert A Ka T signK = signCert signK \<lbrace>Agent A, Key Ka, T\<rbrace>" |
14199 | 153 |
|
36866 | 154 |
definition |
14199 | 155 |
(* Cardholder's Certificate. |
156 |
Contains a PAN, the certified key Ka, the PANSecret PS, |
|
157 |
a number specifying the target use for Ka, the signing key signK. |
|
158 |
*) |
|
67613 | 159 |
certC :: "[nat, key, nat, msg, key] \<Rightarrow> msg" |
36866 | 160 |
where "certC PAN Ka PS T signK = |
61984 | 161 |
signCert signK \<lbrace>Hash \<lbrace>Nonce PS, Pan PAN\<rbrace>, Key Ka, T\<rbrace>" |
14199 | 162 |
|
35068 | 163 |
(*cert and certA have no repeated elements, so they could be abbreviations, |
164 |
but that's tricky and makes proofs slower*) |
|
14199 | 165 |
|
35068 | 166 |
abbreviation "onlyEnc == Number 0" |
167 |
abbreviation "onlySig == Number (Suc 0)" |
|
168 |
abbreviation "authCode == Number (Suc (Suc 0))" |
|
14199 | 169 |
|
63167 | 170 |
subsection\<open>Encryption Primitives\<close> |
14199 | 171 |
|
67613 | 172 |
definition EXcrypt :: "[key,key,msg,msg] \<Rightarrow> msg" where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
173 |
\<comment> \<open>Extra Encryption\<close> |
14199 | 174 |
(*K: the symmetric key EK: the public encryption key*) |
36866 | 175 |
"EXcrypt K EK M m = |
61984 | 176 |
\<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m\<rbrace>\<rbrace>" |
14199 | 177 |
|
67613 | 178 |
definition EXHcrypt :: "[key,key,msg,msg] \<Rightarrow> msg" where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
179 |
\<comment> \<open>Extra Encryption with Hashing\<close> |
14199 | 180 |
(*K: the symmetric key EK: the public encryption key*) |
36866 | 181 |
"EXHcrypt K EK M m = |
61984 | 182 |
\<lbrace>Crypt K \<lbrace>M, Hash m\<rbrace>, Crypt EK \<lbrace>Key K, m, Hash M\<rbrace>\<rbrace>" |
14199 | 183 |
|
67613 | 184 |
definition Enc :: "[key,key,key,msg] \<Rightarrow> msg" where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
185 |
\<comment> \<open>Simple Encapsulation with SIGNATURE\<close> |
14199 | 186 |
(*SK: the sender's signing key |
187 |
K: the symmetric key |
|
188 |
EK: the public encryption key*) |
|
36866 | 189 |
"Enc SK K EK M = |
61984 | 190 |
\<lbrace>Crypt K (sign SK M), Crypt EK (Key K)\<rbrace>" |
14199 | 191 |
|
67613 | 192 |
definition EncB :: "[key,key,key,msg,msg] \<Rightarrow> msg" where |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
193 |
\<comment> \<open>Encapsulation with Baggage. Keys as above, and baggage b.\<close> |
36866 | 194 |
"EncB SK K EK M b = |
61984 | 195 |
\<lbrace>Enc SK K EK \<lbrace>M, Hash b\<rbrace>, b\<rbrace>" |
14199 | 196 |
|
197 |
||
63167 | 198 |
subsection\<open>Basic Properties of pubEK, pubSK, priEK and priSK\<close> |
14199 | 199 |
|
200 |
lemma publicKey_eq_iff [iff]: |
|
67613 | 201 |
"(publicKey b A = publicKey b' A') = (b=b' \<and> A=A')" |
14199 | 202 |
by (blast dest: injective_publicKey) |
203 |
||
204 |
lemma privateKey_eq_iff [iff]: |
|
67613 | 205 |
"(invKey (publicKey b A) = invKey (publicKey b' A')) = (b=b' \<and> A=A')" |
14199 | 206 |
by auto |
207 |
||
208 |
lemma not_symKeys_publicKey [iff]: "publicKey b A \<notin> symKeys" |
|
209 |
by (simp add: symKeys_def) |
|
210 |
||
211 |
lemma not_symKeys_privateKey [iff]: "invKey (publicKey b A) \<notin> symKeys" |
|
212 |
by (simp add: symKeys_def) |
|
213 |
||
67613 | 214 |
lemma symKeys_invKey_eq [simp]: "K \<in> symKeys \<Longrightarrow> invKey K = K" |
14199 | 215 |
by (simp add: symKeys_def) |
216 |
||
217 |
lemma symKeys_invKey_iff [simp]: "(invKey K \<in> symKeys) = (K \<in> symKeys)" |
|
218 |
by (unfold symKeys_def, auto) |
|
219 |
||
63167 | 220 |
text\<open>Can be slow (or even loop) as a simprule\<close> |
67613 | 221 |
lemma symKeys_neq_imp_neq: "(K \<in> symKeys) \<noteq> (K' \<in> symKeys) \<Longrightarrow> K \<noteq> K'" |
14199 | 222 |
by blast |
223 |
||
63167 | 224 |
text\<open>These alternatives to \<open>symKeys_neq_imp_neq\<close> don't seem any better |
225 |
in practice.\<close> |
|
67613 | 226 |
lemma publicKey_neq_symKey: "K \<in> symKeys \<Longrightarrow> publicKey b A \<noteq> K" |
14199 | 227 |
by blast |
228 |
||
67613 | 229 |
lemma symKey_neq_publicKey: "K \<in> symKeys \<Longrightarrow> K \<noteq> publicKey b A" |
14199 | 230 |
by blast |
231 |
||
67613 | 232 |
lemma privateKey_neq_symKey: "K \<in> symKeys \<Longrightarrow> invKey (publicKey b A) \<noteq> K" |
14199 | 233 |
by blast |
234 |
||
67613 | 235 |
lemma symKey_neq_privateKey: "K \<in> symKeys \<Longrightarrow> K \<noteq> invKey (publicKey b A)" |
14199 | 236 |
by blast |
237 |
||
238 |
lemma analz_symKeys_Decrypt: |
|
239 |
"[| Crypt K X \<in> analz H; K \<in> symKeys; Key K \<in> analz H |] |
|
240 |
==> X \<in> analz H" |
|
241 |
by auto |
|
242 |
||
243 |
||
63167 | 244 |
subsection\<open>"Image" Equations That Hold for Injective Functions\<close> |
14199 | 245 |
|
246 |
lemma invKey_image_eq [iff]: "(invKey x \<in> invKey`A) = (x\<in>A)" |
|
247 |
by auto |
|
248 |
||
63167 | 249 |
text\<open>holds because invKey is injective\<close> |
14199 | 250 |
lemma publicKey_image_eq [iff]: |
67613 | 251 |
"(publicKey b A \<in> publicKey c ` AS) = (b=c \<and> A\<in>AS)" |
14199 | 252 |
by auto |
253 |
||
254 |
lemma privateKey_image_eq [iff]: |
|
67613 | 255 |
"(invKey (publicKey b A) \<in> invKey ` publicKey c ` AS) = (b=c \<and> A\<in>AS)" |
14199 | 256 |
by auto |
257 |
||
258 |
lemma privateKey_notin_image_publicKey [iff]: |
|
259 |
"invKey (publicKey b A) \<notin> publicKey c ` AS" |
|
260 |
by auto |
|
261 |
||
262 |
lemma publicKey_notin_image_privateKey [iff]: |
|
263 |
"publicKey b A \<notin> invKey ` publicKey c ` AS" |
|
264 |
by auto |
|
265 |
||
266 |
lemma keysFor_parts_initState [simp]: "keysFor (parts (initState C)) = {}" |
|
267 |
apply (simp add: keysFor_def) |
|
268 |
apply (induct_tac "C") |
|
269 |
apply (auto intro: range_eqI) |
|
270 |
done |
|
271 |
||
63167 | 272 |
text\<open>for proving \<open>new_keys_not_used\<close>\<close> |
14199 | 273 |
lemma keysFor_parts_insert: |
274 |
"[| K \<in> keysFor (parts (insert X H)); X \<in> synth (analz H) |] |
|
275 |
==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H" |
|
14218 | 276 |
by (force dest!: |
14199 | 277 |
parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD] |
278 |
analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] |
|
279 |
intro: analz_into_parts) |
|
280 |
||
281 |
lemma Crypt_imp_keysFor [intro]: |
|
282 |
"[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H" |
|
283 |
by (drule Crypt_imp_invKey_keysFor, simp) |
|
284 |
||
63167 | 285 |
text\<open>Agents see their own private keys!\<close> |
14199 | 286 |
lemma privateKey_in_initStateCA [iff]: |
287 |
"Key (invKey (publicKey b A)) \<in> initState A" |
|
288 |
by (case_tac "A", auto) |
|
289 |
||
63167 | 290 |
text\<open>Agents see their own public keys!\<close> |
14199 | 291 |
lemma publicKey_in_initStateCA [iff]: "Key (publicKey b A) \<in> initState A" |
292 |
by (case_tac "A", auto) |
|
293 |
||
63167 | 294 |
text\<open>RCA sees CAs' public keys!\<close> |
14199 | 295 |
lemma pubK_CA_in_initState_RCA [iff]: |
296 |
"Key (publicKey b (CA i)) \<in> initState RCA" |
|
297 |
by auto |
|
298 |
||
299 |
||
63167 | 300 |
text\<open>Spy knows all public keys\<close> |
14199 | 301 |
lemma knows_Spy_pubEK_i [iff]: "Key (publicKey b A) \<in> knows Spy evs" |
302 |
apply (induct_tac "evs") |
|
63648 | 303 |
apply (simp_all add: imageI knows_Cons split: event.split) |
14199 | 304 |
done |
305 |
||
306 |
declare knows_Spy_pubEK_i [THEN analz.Inj, iff] |
|
307 |
(*needed????*) |
|
308 |
||
63167 | 309 |
text\<open>Spy sees private keys of bad agents! [and obviously public keys too]\<close> |
14199 | 310 |
lemma knows_Spy_bad_privateKey [intro!]: |
67613 | 311 |
"A \<in> bad \<Longrightarrow> Key (invKey (publicKey b A)) \<in> knows Spy evs" |
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset
|
312 |
by (rule initState_subset_knows [THEN subsetD], simp) |
14199 | 313 |
|
314 |
||
63167 | 315 |
subsection\<open>Fresh Nonces for Possibility Theorems\<close> |
14199 | 316 |
|
317 |
lemma Nonce_notin_initState [iff]: "Nonce N \<notin> parts (initState B)" |
|
318 |
by (induct_tac "B", auto) |
|
319 |
||
320 |
lemma Nonce_notin_used_empty [simp]: "Nonce N \<notin> used []" |
|
321 |
by (simp add: used_Nil) |
|
322 |
||
63167 | 323 |
text\<open>In any trace, there is an upper bound N on the greatest nonce in use.\<close> |
67613 | 324 |
lemma Nonce_supply_lemma: "\<exists>N. \<forall>n. N\<le>n \<longrightarrow> Nonce n \<notin> used evs" |
14199 | 325 |
apply (induct_tac "evs") |
326 |
apply (rule_tac x = 0 in exI) |
|
63648 | 327 |
apply (simp_all add: used_Cons split: event.split, safe) |
14199 | 328 |
apply (rule msg_Nonce_supply [THEN exE], blast elim!: add_leE)+ |
329 |
done |
|
330 |
||
331 |
lemma Nonce_supply1: "\<exists>N. Nonce N \<notin> used evs" |
|
332 |
by (rule Nonce_supply_lemma [THEN exE], blast) |
|
333 |
||
67613 | 334 |
lemma Nonce_supply: "Nonce (SOME N. Nonce N \<notin> used evs) \<notin> used evs" |
14199 | 335 |
apply (rule Nonce_supply_lemma [THEN exE]) |
336 |
apply (rule someI, fast) |
|
337 |
done |
|
338 |
||
339 |
||
63167 | 340 |
subsection\<open>Specialized Methods for Possibility Theorems\<close> |
14199 | 341 |
|
342 |
ML |
|
63167 | 343 |
\<open> |
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30549
diff
changeset
|
344 |
(*Tactic for possibility theorems*) |
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30549
diff
changeset
|
345 |
fun possibility_tac ctxt = |
14199 | 346 |
REPEAT (*omit used_Says so that Nonces start from different traces!*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45827
diff
changeset
|
347 |
(ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}, @{thm used_Notes}])) |
14199 | 348 |
THEN |
349 |
REPEAT_FIRST (eq_assume_tac ORELSE' |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
350 |
resolve_tac ctxt [refl, conjI, @{thm Nonce_supply}])) |
14199 | 351 |
|
352 |
(*For harder protocols (such as SET_CR!), where we have to set up some |
|
353 |
nonces and keys initially*) |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30549
diff
changeset
|
354 |
fun basic_possibility_tac ctxt = |
14199 | 355 |
REPEAT |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
45827
diff
changeset
|
356 |
(ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver)) |
14199 | 357 |
THEN |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58889
diff
changeset
|
358 |
REPEAT_FIRST (resolve_tac ctxt [refl, conjI])) |
63167 | 359 |
\<close> |
14199 | 360 |
|
63167 | 361 |
method_setup possibility = \<open> |
362 |
Scan.succeed (SIMPLE_METHOD o possibility_tac)\<close> |
|
14199 | 363 |
"for proving possibility theorems" |
364 |
||
63167 | 365 |
method_setup basic_possibility = \<open> |
366 |
Scan.succeed (SIMPLE_METHOD o basic_possibility_tac)\<close> |
|
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents:
30549
diff
changeset
|
367 |
"for proving possibility theorems" |
14199 | 368 |
|
369 |
||
69597 | 370 |
subsection\<open>Specialized Rewriting for Theorems About \<^term>\<open>analz\<close> and Image\<close> |
14199 | 371 |
|
67613 | 372 |
lemma insert_Key_singleton: "insert (Key K) H = Key ` {K} \<union> H" |
14199 | 373 |
by blast |
374 |
||
375 |
lemma insert_Key_image: |
|
67613 | 376 |
"insert (Key K) (Key`KK \<union> C) = Key ` (insert K KK) \<union> C" |
14199 | 377 |
by blast |
378 |
||
63167 | 379 |
text\<open>Needed for \<open>DK_fresh_not_KeyCryptKey\<close>\<close> |
14199 | 380 |
lemma publicKey_in_used [iff]: "Key (publicKey b A) \<in> used evs" |
381 |
by auto |
|
382 |
||
383 |
lemma privateKey_in_used [iff]: "Key (invKey (publicKey b A)) \<in> used evs" |
|
384 |
by (blast intro!: initState_into_used) |
|
385 |
||
63167 | 386 |
text\<open>Reverse the normal simplification of "image" to build up (not break down) |
387 |
the set of keys. Based on \<open>analz_image_freshK_ss\<close>, but simpler.\<close> |
|
14199 | 388 |
lemmas analz_image_keys_simps = |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63648
diff
changeset
|
389 |
simp_thms mem_simps \<comment> \<open>these two allow its use with \<open>only:\<close>\<close> |
14199 | 390 |
image_insert [THEN sym] image_Un [THEN sym] |
391 |
rangeI symKeys_neq_imp_neq |
|
392 |
insert_Key_singleton insert_Key_image Un_assoc [THEN sym] |
|
393 |
||
394 |
||
395 |
(*General lemmas proved by Larry*) |
|
396 |
||
63167 | 397 |
subsection\<open>Controlled Unfolding of Abbreviations\<close> |
14199 | 398 |
|
63167 | 399 |
text\<open>A set is expanded only if a relation is applied to it\<close> |
14199 | 400 |
lemma def_abbrev_simp_relation: |
67613 | 401 |
"A = B \<Longrightarrow> (A \<in> X) = (B \<in> X) \<and> |
402 |
(u = A) = (u = B) \<and> |
|
14199 | 403 |
(A = u) = (B = u)" |
404 |
by auto |
|
405 |
||
63167 | 406 |
text\<open>A set is expanded only if one of the given functions is applied to it\<close> |
14199 | 407 |
lemma def_abbrev_simp_function: |
36866 | 408 |
"A = B |
67613 | 409 |
\<Longrightarrow> parts (insert A X) = parts (insert B X) \<and> |
410 |
analz (insert A X) = analz (insert B X) \<and> |
|
14199 | 411 |
keysFor (insert A X) = keysFor (insert B X)" |
412 |
by auto |
|
413 |
||
69597 | 414 |
subsubsection\<open>Special Simplification Rules for \<^term>\<open>signCert\<close>\<close> |
14199 | 415 |
|
63167 | 416 |
text\<open>Avoids duplicating X and its components!\<close> |
14199 | 417 |
lemma parts_insert_signCert: |
418 |
"parts (insert (signCert K X) H) = |
|
61984 | 419 |
insert \<lbrace>X, Crypt K X\<rbrace> (parts (insert (Crypt K X) H))" |
14199 | 420 |
by (simp add: signCert_def insert_commute [of X]) |
421 |
||
63167 | 422 |
text\<open>Avoids a case split! [X is always available]\<close> |
14199 | 423 |
lemma analz_insert_signCert: |
424 |
"analz (insert (signCert K X) H) = |
|
61984 | 425 |
insert \<lbrace>X, Crypt K X\<rbrace> (insert (Crypt K X) (analz (insert X H)))" |
14199 | 426 |
by (simp add: signCert_def insert_commute [of X]) |
427 |
||
428 |
lemma keysFor_insert_signCert: "keysFor (insert (signCert K X) H) = keysFor H" |
|
429 |
by (simp add: signCert_def) |
|
430 |
||
69597 | 431 |
text\<open>Controlled rewrite rules for \<^term>\<open>signCert\<close>, just the definitions |
14199 | 432 |
of the others. Encryption primitives are just expanded, despite their huge |
63167 | 433 |
redundancy!\<close> |
14199 | 434 |
lemmas abbrev_simps [simp] = |
435 |
parts_insert_signCert analz_insert_signCert keysFor_insert_signCert |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
436 |
sign_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
437 |
sign_def [THEN def_abbrev_simp_function] |
14199 | 438 |
signCert_def [THEN def_abbrev_simp_relation] |
439 |
signCert_def [THEN def_abbrev_simp_function] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
440 |
certC_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
441 |
certC_def [THEN def_abbrev_simp_function] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
442 |
cert_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
443 |
cert_def [THEN def_abbrev_simp_function] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
444 |
EXcrypt_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
445 |
EXcrypt_def [THEN def_abbrev_simp_function] |
14199 | 446 |
EXHcrypt_def [THEN def_abbrev_simp_relation] |
447 |
EXHcrypt_def [THEN def_abbrev_simp_function] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
448 |
Enc_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
449 |
Enc_def [THEN def_abbrev_simp_function] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
450 |
EncB_def [THEN def_abbrev_simp_relation] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
451 |
EncB_def [THEN def_abbrev_simp_function] |
14199 | 452 |
|
453 |
||
63167 | 454 |
subsubsection\<open>Elimination Rules for Controlled Rewriting\<close> |
14199 | 455 |
|
456 |
lemma Enc_partsE: |
|
457 |
"!!R. [|Enc SK K EK M \<in> parts H; |
|
458 |
[|Crypt K (sign SK M) \<in> parts H; |
|
459 |
Crypt EK (Key K) \<in> parts H|] ==> R|] |
|
460 |
==> R" |
|
461 |
||
462 |
by (unfold Enc_def, blast) |
|
463 |
||
464 |
lemma EncB_partsE: |
|
465 |
"!!R. [|EncB SK K EK M b \<in> parts H; |
|
61984 | 466 |
[|Crypt K (sign SK \<lbrace>M, Hash b\<rbrace>) \<in> parts H; |
14199 | 467 |
Crypt EK (Key K) \<in> parts H; |
468 |
b \<in> parts H|] ==> R|] |
|
469 |
==> R" |
|
470 |
by (unfold EncB_def Enc_def, blast) |
|
471 |
||
472 |
lemma EXcrypt_partsE: |
|
473 |
"!!R. [|EXcrypt K EK M m \<in> parts H; |
|
61984 | 474 |
[|Crypt K \<lbrace>M, Hash m\<rbrace> \<in> parts H; |
475 |
Crypt EK \<lbrace>Key K, m\<rbrace> \<in> parts H|] ==> R|] |
|
14199 | 476 |
==> R" |
477 |
by (unfold EXcrypt_def, blast) |
|
478 |
||
479 |
||
69597 | 480 |
subsection\<open>Lemmas to Simplify Expressions Involving \<^term>\<open>analz\<close>\<close> |
14199 | 481 |
|
482 |
lemma analz_knows_absorb: |
|
483 |
"Key K \<in> analz (knows Spy evs) |
|
484 |
==> analz (Key ` (insert K H) \<union> knows Spy evs) = |
|
485 |
analz (Key ` H \<union> knows Spy evs)" |
|
486 |
by (simp add: analz_insert_eq Un_upper2 [THEN analz_mono, THEN subsetD]) |
|
487 |
||
488 |
lemma analz_knows_absorb2: |
|
489 |
"Key K \<in> analz (knows Spy evs) |
|
490 |
==> analz (Key ` (insert X (insert K H)) \<union> knows Spy evs) = |
|
491 |
analz (Key ` (insert X H) \<union> knows Spy evs)" |
|
492 |
apply (subst insert_commute) |
|
493 |
apply (erule analz_knows_absorb) |
|
494 |
done |
|
495 |
||
496 |
lemma analz_insert_subset_eq: |
|
497 |
"[|X \<in> analz (knows Spy evs); knows Spy evs \<subseteq> H|] |
|
498 |
==> analz (insert X H) = analz H" |
|
499 |
apply (rule analz_insert_eq) |
|
500 |
apply (blast intro: analz_mono [THEN [2] rev_subsetD]) |
|
501 |
done |
|
502 |
||
503 |
lemmas analz_insert_simps = |
|
504 |
analz_insert_subset_eq Un_upper2 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
505 |
subset_insertI [THEN [2] subset_trans] |
14199 | 506 |
|
507 |
||
63167 | 508 |
subsection\<open>Freshness Lemmas\<close> |
14199 | 509 |
|
510 |
lemma in_parts_Says_imp_used: |
|
511 |
"[|Key K \<in> parts {X}; Says A B X \<in> set evs|] ==> Key K \<in> used evs" |
|
512 |
by (blast intro: parts_trans dest!: Says_imp_knows_Spy [THEN parts.Inj]) |
|
513 |
||
69597 | 514 |
text\<open>A useful rewrite rule with \<^term>\<open>analz_image_keys_simps\<close>\<close> |
14199 | 515 |
lemma Crypt_notin_image_Key: "Crypt K X \<notin> Key ` KK" |
516 |
by auto |
|
517 |
||
518 |
lemma fresh_notin_analz_knows_Spy: |
|
67613 | 519 |
"Key K \<notin> used evs \<Longrightarrow> Key K \<notin> analz (knows Spy evs)" |
14199 | 520 |
by (auto dest: analz_into_parts) |
521 |
||
522 |
end |