author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 67443 | 3abf6a722518 |
child 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
33028 | 1 |
(* Title: HOL/SET_Protocol/Merchant_Registration.thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
2 |
Author: Giampaolo Bella |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
3 |
Author: Fabio Massacci |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
4 |
Author: Lawrence C Paulson |
14199 | 5 |
*) |
6 |
||
63167 | 7 |
section\<open>The SET Merchant Registration Protocol\<close> |
14199 | 8 |
|
33028 | 9 |
theory Merchant_Registration |
10 |
imports Public_SET |
|
11 |
begin |
|
14199 | 12 |
|
63167 | 13 |
text\<open>Copmpared with Cardholder Reigstration, \<open>KeyCryptKey\<close> is not |
14199 | 14 |
needed: no session key encrypts another. Instead we |
15 |
prove the "key compromise" theorems for sets KK that contain no private |
|
63167 | 16 |
encryption keys (@{term "priEK C"}).\<close> |
14199 | 17 |
|
18 |
||
23755 | 19 |
inductive_set |
20 |
set_mr :: "event list set" |
|
21 |
where |
|
14199 | 22 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
23 |
Nil: \<comment> \<open>Initial trace is empty\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
24 |
"[] \<in> set_mr" |
14199 | 25 |
|
26 |
||
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
27 |
| Fake: \<comment> \<open>The spy MAY say anything he CAN say.\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
28 |
"[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
29 |
==> Says Spy B X # evsf \<in> set_mr" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
30 |
|
14199 | 31 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
32 |
| Reception: \<comment> \<open>If A sends a message X to B, then B might receive it\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
33 |
"[| evsr \<in> set_mr; Says A B X \<in> set evsr |] |
14199 | 34 |
==> Gets B X # evsr \<in> set_mr" |
35 |
||
36 |
||
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
37 |
| SET_MR1: \<comment> \<open>RegFormReq: M requires a registration form to a CA\<close> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
38 |
"[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |] |
61984 | 39 |
==> Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> # evs1 \<in> set_mr" |
14199 | 40 |
|
41 |
||
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
42 |
| SET_MR2: \<comment> \<open>RegFormRes: CA replies with the registration form and the |
63167 | 43 |
certificates for her keys\<close> |
14199 | 44 |
"[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2; |
61984 | 45 |
Gets (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<in> set evs2 |] |
46 |
==> Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM1, Nonce NCA\<rbrace>, |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
47 |
cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA), |
61984 | 48 |
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) \<rbrace> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
49 |
# evs2 \<in> set_mr" |
14199 | 50 |
|
23755 | 51 |
| SET_MR3: |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
52 |
\<comment> \<open>CertReq: M submits the key pair to be certified. The Notes |
14199 | 53 |
event allows KM1 to be lost if M is compromised. Piero remarks |
54 |
that the agent mentioned inside the signature is not verified to |
|
55 |
correspond to M. As in CR, each Merchant has fixed key pairs. M |
|
56 |
is only optionally required to send NCA back, so M doesn't do so |
|
63167 | 57 |
in the model\<close> |
14199 | 58 |
"[| evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3; |
59 |
Key KM1 \<notin> used evs3; KM1 \<in> symKeys; |
|
61984 | 60 |
Gets M \<lbrace>sign (invKey SKi) \<lbrace>Agent X, Nonce NM1, Nonce NCA\<rbrace>, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
61 |
cert (CA i) EKi onlyEnc (priSK RCA), |
61984 | 62 |
cert (CA i) SKi onlySig (priSK RCA) \<rbrace> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
63 |
\<in> set evs3; |
61984 | 64 |
Says M (CA i) \<lbrace>Agent M, Nonce NM1\<rbrace> \<in> set evs3 |] |
14199 | 65 |
==> Says M (CA i) |
61984 | 66 |
\<lbrace>Crypt KM1 (sign (priSK M) \<lbrace>Agent M, Nonce NM2, |
67 |
Key (pubSK M), Key (pubEK M)\<rbrace>), |
|
68 |
Crypt EKi (Key KM1)\<rbrace> |
|
69 |
# Notes M \<lbrace>Key KM1, Agent (CA i)\<rbrace> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
70 |
# evs3 \<in> set_mr" |
14199 | 71 |
|
23755 | 72 |
| SET_MR4: |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
73 |
\<comment> \<open>CertRes: CA issues the certificates for merSK and merEK, |
14199 | 74 |
while checking never to have certified the m even |
75 |
separately. NOTE: In Cardholder Registration the |
|
76 |
corresponding rule (6) doesn't use the "sign" primitive. "The |
|
77 |
CertRes shall be signed but not encrypted if the EE is a Merchant |
|
63167 | 78 |
or Payment Gateway."-- Programmer's Guide, page 191.\<close> |
14199 | 79 |
"[| evs4 \<in> set_mr; M = Merchant k; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
80 |
merSK \<notin> symKeys; merEK \<notin> symKeys; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
81 |
Notes (CA i) (Key merSK) \<notin> set evs4; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
82 |
Notes (CA i) (Key merEK) \<notin> set evs4; |
61984 | 83 |
Gets (CA i) \<lbrace>Crypt KM1 (sign (invKey merSK) |
84 |
\<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), |
|
85 |
Crypt (pubEK (CA i)) (Key KM1) \<rbrace> |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
86 |
\<in> set evs4 |] |
61984 | 87 |
==> Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent(CA i)\<rbrace>, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
88 |
cert M merSK onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
89 |
cert M merEK onlyEnc (priSK (CA i)), |
61984 | 90 |
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
91 |
# Notes (CA i) (Key merSK) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
92 |
# Notes (CA i) (Key merEK) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
93 |
# evs4 \<in> set_mr" |
14199 | 94 |
|
95 |
||
63167 | 96 |
text\<open>Note possibility proofs are missing.\<close> |
14199 | 97 |
|
98 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
|
99 |
declare parts.Body [dest] |
|
100 |
declare analz_into_parts [dest] |
|
101 |
declare Fake_parts_insert_in_Un [dest] |
|
102 |
||
63167 | 103 |
text\<open>General facts about message reception\<close> |
14199 | 104 |
lemma Gets_imp_Says: |
105 |
"[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> \<exists>A. Says A B X \<in> set evs" |
|
106 |
apply (erule rev_mp) |
|
107 |
apply (erule set_mr.induct, auto) |
|
108 |
done |
|
109 |
||
110 |
lemma Gets_imp_knows_Spy: |
|
111 |
"[| Gets B X \<in> set evs; evs \<in> set_mr |] ==> X \<in> knows Spy evs" |
|
112 |
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) |
|
113 |
||
114 |
||
115 |
declare Gets_imp_knows_Spy [THEN parts.Inj, dest] |
|
116 |
||
63167 | 117 |
subsubsection\<open>Proofs on keys\<close> |
14199 | 118 |
|
63167 | 119 |
text\<open>Spy never sees an agent's private keys! (unless it's bad at start)\<close> |
14199 | 120 |
lemma Spy_see_private_Key [simp]: |
121 |
"evs \<in> set_mr |
|
122 |
==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)" |
|
123 |
apply (erule set_mr.induct) |
|
124 |
apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj]) |
|
125 |
done |
|
126 |
||
127 |
lemma Spy_analz_private_Key [simp]: |
|
128 |
"evs \<in> set_mr ==> |
|
129 |
(Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)" |
|
130 |
by auto |
|
131 |
||
132 |
declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!] |
|
133 |
declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!] |
|
134 |
||
135 |
(*This is to state that the signed keys received in step 4 |
|
136 |
are into parts - rather than installing sign_def each time. |
|
137 |
Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK |
|
138 |
Goal "[|Gets C \<lbrace>Crypt KM1 |
|
139 |
(sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace> |
|
140 |
\<in> set evs; evs \<in> set_mr |] |
|
141 |
==> Key merSK \<in> parts (knows Spy evs) \<and> |
|
142 |
Key merEK \<in> parts (knows Spy evs)" |
|
143 |
by (fast_tac (claset() addss (simpset())) 1); |
|
144 |
qed "signed_keys_in_parts"; |
|
145 |
???*) |
|
146 |
||
63167 | 147 |
text\<open>Proofs on certificates - |
148 |
they hold, as in CR, because RCA's keys are secure\<close> |
|
14199 | 149 |
|
150 |
lemma Crypt_valid_pubEK: |
|
61984 | 151 |
"[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key EKi, onlyEnc\<rbrace> |
14199 | 152 |
\<in> parts (knows Spy evs); |
153 |
evs \<in> set_mr |] ==> EKi = pubEK (CA i)" |
|
154 |
apply (erule rev_mp) |
|
155 |
apply (erule set_mr.induct, auto) |
|
156 |
done |
|
157 |
||
158 |
lemma certificate_valid_pubEK: |
|
159 |
"[| cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs); |
|
160 |
evs \<in> set_mr |] |
|
161 |
==> EKi = pubEK (CA i)" |
|
162 |
apply (unfold cert_def signCert_def) |
|
163 |
apply (blast dest!: Crypt_valid_pubEK) |
|
164 |
done |
|
165 |
||
166 |
lemma Crypt_valid_pubSK: |
|
61984 | 167 |
"[| Crypt (priSK RCA) \<lbrace>Agent (CA i), Key SKi, onlySig\<rbrace> |
14199 | 168 |
\<in> parts (knows Spy evs); |
169 |
evs \<in> set_mr |] ==> SKi = pubSK (CA i)" |
|
170 |
apply (erule rev_mp) |
|
171 |
apply (erule set_mr.induct, auto) |
|
172 |
done |
|
173 |
||
174 |
lemma certificate_valid_pubSK: |
|
175 |
"[| cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs); |
|
176 |
evs \<in> set_mr |] ==> SKi = pubSK (CA i)" |
|
177 |
apply (unfold cert_def signCert_def) |
|
178 |
apply (blast dest!: Crypt_valid_pubSK) |
|
179 |
done |
|
180 |
||
181 |
lemma Gets_certificate_valid: |
|
61984 | 182 |
"[| Gets A \<lbrace> X, cert (CA i) EKi onlyEnc (priSK RCA), |
183 |
cert (CA i) SKi onlySig (priSK RCA)\<rbrace> \<in> set evs; |
|
14199 | 184 |
evs \<in> set_mr |] |
67613 | 185 |
==> EKi = pubEK (CA i) \<and> SKi = pubSK (CA i)" |
14199 | 186 |
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK) |
187 |
||
188 |
||
63167 | 189 |
text\<open>Nobody can have used non-existent keys!\<close> |
14199 | 190 |
lemma new_keys_not_used [rule_format,simp]: |
191 |
"evs \<in> set_mr |
|
67613 | 192 |
==> Key K \<notin> used evs \<longrightarrow> K \<in> symKeys \<longrightarrow> |
14199 | 193 |
K \<notin> keysFor (parts (knows Spy evs))" |
194 |
apply (erule set_mr.induct, simp_all) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
195 |
apply (force dest!: usedI keysFor_parts_insert) \<comment> \<open>Fake\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
196 |
apply force \<comment> \<open>Message 2\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
197 |
apply (blast dest: Gets_certificate_valid) \<comment> \<open>Message 3\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
198 |
apply force \<comment> \<open>Message 4\<close> |
14199 | 199 |
done |
200 |
||
201 |
||
63167 | 202 |
subsubsection\<open>New Versions: As Above, but Generalized with the Kk Argument\<close> |
14199 | 203 |
|
204 |
lemma gen_new_keys_not_used [rule_format]: |
|
205 |
"evs \<in> set_mr |
|
67613 | 206 |
==> Key K \<notin> used evs \<longrightarrow> K \<in> symKeys \<longrightarrow> |
207 |
K \<notin> keysFor (parts (Key`KK \<union> knows Spy evs))" |
|
14199 | 208 |
by auto |
209 |
||
210 |
lemma gen_new_keys_not_analzd: |
|
211 |
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |] |
|
67613 | 212 |
==> K \<notin> keysFor (analz (Key`KK \<union> knows Spy evs))" |
14199 | 213 |
by (blast intro: keysFor_mono [THEN [2] rev_subsetD] |
214 |
dest: gen_new_keys_not_used) |
|
215 |
||
216 |
lemma analz_Key_image_insert_eq: |
|
217 |
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr |] |
|
218 |
==> analz (Key ` (insert K KK) \<union> knows Spy evs) = |
|
219 |
insert (Key K) (analz (Key ` KK \<union> knows Spy evs))" |
|
220 |
by (simp add: gen_new_keys_not_analzd) |
|
221 |
||
222 |
||
223 |
lemma Crypt_parts_imp_used: |
|
224 |
"[|Crypt K X \<in> parts (knows Spy evs); |
|
225 |
K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs" |
|
226 |
apply (rule ccontr) |
|
227 |
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor) |
|
228 |
done |
|
229 |
||
230 |
lemma Crypt_analz_imp_used: |
|
231 |
"[|Crypt K X \<in> analz (knows Spy evs); |
|
232 |
K \<in> symKeys; evs \<in> set_mr |] ==> Key K \<in> used evs" |
|
233 |
by (blast intro: Crypt_parts_imp_used) |
|
234 |
||
63167 | 235 |
text\<open>Rewriting rule for private encryption keys. Analogous rewriting rules |
236 |
for other keys aren't needed.\<close> |
|
14199 | 237 |
|
238 |
lemma parts_image_priEK: |
|
67613 | 239 |
"[|Key (priEK (CA i)) \<in> parts (Key`KK \<union> (knows Spy evs)); |
14199 | 240 |
evs \<in> set_mr|] ==> priEK (CA i) \<in> KK | CA i \<in> bad" |
241 |
by auto |
|
242 |
||
63167 | 243 |
text\<open>trivial proof because (priEK (CA i)) never appears even in (parts evs)\<close> |
14199 | 244 |
lemma analz_image_priEK: |
245 |
"evs \<in> set_mr ==> |
|
67613 | 246 |
(Key (priEK (CA i)) \<in> analz (Key`KK \<union> (knows Spy evs))) = |
14199 | 247 |
(priEK (CA i) \<in> KK | CA i \<in> bad)" |
248 |
by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD]) |
|
249 |
||
250 |
||
63167 | 251 |
subsection\<open>Secrecy of Session Keys\<close> |
14199 | 252 |
|
63167 | 253 |
text\<open>This holds because if (priEK (CA i)) appears in any traffic then it must |
254 |
be known to the Spy, by \<open>Spy_see_private_Key\<close>\<close> |
|
14199 | 255 |
lemma merK_neq_priEK: |
256 |
"[|Key merK \<notin> analz (knows Spy evs); |
|
257 |
Key merK \<in> parts (knows Spy evs); |
|
258 |
evs \<in> set_mr|] ==> merK \<noteq> priEK C" |
|
259 |
by blast |
|
260 |
||
63167 | 261 |
text\<open>Lemma for message 4: either merK is compromised (when we don't care) |
262 |
or else merK hasn't been used to encrypt K.\<close> |
|
14199 | 263 |
lemma msg4_priEK_disj: |
61984 | 264 |
"[|Gets B \<lbrace>Crypt KM1 |
265 |
(sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), |
|
266 |
Y\<rbrace> \<in> set evs; |
|
14199 | 267 |
evs \<in> set_mr|] |
268 |
==> (Key merSK \<in> analz (knows Spy evs) | merSK \<notin> range(\<lambda>C. priEK C)) |
|
67613 | 269 |
\<and> (Key merEK \<in> analz (knows Spy evs) | merEK \<notin> range(\<lambda>C. priEK C))" |
14199 | 270 |
apply (unfold sign_def) |
271 |
apply (blast dest: merK_neq_priEK) |
|
272 |
done |
|
273 |
||
274 |
||
275 |
lemma Key_analz_image_Key_lemma: |
|
67613 | 276 |
"P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) \<longrightarrow> (K\<in>KK | Key K \<in> analz H) |
14199 | 277 |
==> |
67613 | 278 |
P \<longrightarrow> (Key K \<in> analz (Key`KK \<union> H)) = (K\<in>KK | Key K \<in> analz H)" |
14199 | 279 |
by (blast intro: analz_mono [THEN [2] rev_subsetD]) |
280 |
||
281 |
lemma symKey_compromise: |
|
282 |
"evs \<in> set_mr ==> |
|
67613 | 283 |
(\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow> |
284 |
(Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) = |
|
14199 | 285 |
(SK \<in> KK | Key SK \<in> analz (knows Spy evs)))" |
286 |
apply (erule set_mr.induct) |
|
287 |
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI]) |
|
288 |
apply (drule_tac [7] msg4_priEK_disj) |
|
289 |
apply (frule_tac [6] Gets_certificate_valid) |
|
290 |
apply (safe del: impI) |
|
291 |
apply (simp_all del: image_insert image_Un imp_disjL |
|
292 |
add: analz_image_keys_simps abbrev_simps analz_knows_absorb |
|
293 |
analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff |
|
294 |
Spy_analz_private_Key analz_image_priEK) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
295 |
\<comment> \<open>5 seconds on a 1.6GHz machine\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
296 |
apply spy_analz \<comment> \<open>Fake\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
297 |
apply auto \<comment> \<open>Message 3\<close> |
14199 | 298 |
done |
299 |
||
300 |
lemma symKey_secrecy [rule_format]: |
|
301 |
"[|CA i \<notin> bad; K \<in> symKeys; evs \<in> set_mr|] |
|
67613 | 302 |
==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs \<longrightarrow> |
303 |
Key K \<in> parts{X} \<longrightarrow> |
|
304 |
Merchant m \<notin> bad \<longrightarrow> |
|
14199 | 305 |
Key K \<notin> analz (knows Spy evs)" |
306 |
apply (erule set_mr.induct) |
|
307 |
apply (drule_tac [7] msg4_priEK_disj) |
|
308 |
apply (frule_tac [6] Gets_certificate_valid) |
|
309 |
apply (safe del: impI) |
|
310 |
apply (simp_all del: image_insert image_Un imp_disjL |
|
311 |
add: analz_image_keys_simps abbrev_simps analz_knows_absorb |
|
312 |
analz_knows_absorb2 analz_Key_image_insert_eq |
|
313 |
symKey_compromise notin_image_iff Spy_analz_private_Key |
|
314 |
analz_image_priEK) |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
315 |
apply spy_analz \<comment> \<open>Fake\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
316 |
apply force \<comment> \<open>Message 1\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
63167
diff
changeset
|
317 |
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) \<comment> \<open>Message 3\<close> |
14199 | 318 |
done |
319 |
||
63167 | 320 |
subsection\<open>Unicity\<close> |
14199 | 321 |
|
322 |
lemma msg4_Says_imp_Notes: |
|
61984 | 323 |
"[|Says (CA i) M \<lbrace>sign (priSK (CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
324 |
cert M merSK onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
325 |
cert M merEK onlyEnc (priSK (CA i)), |
61984 | 326 |
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs; |
14199 | 327 |
evs \<in> set_mr |] |
328 |
==> Notes (CA i) (Key merSK) \<in> set evs |
|
67613 | 329 |
\<and> Notes (CA i) (Key merEK) \<in> set evs" |
14199 | 330 |
apply (erule rev_mp) |
331 |
apply (erule set_mr.induct) |
|
332 |
apply (simp_all (no_asm_simp)) |
|
333 |
done |
|
334 |
||
63167 | 335 |
text\<open>Unicity of merSK wrt a given CA: |
336 |
merSK uniquely identifies the other components, including merEK\<close> |
|
14199 | 337 |
lemma merSK_unicity: |
61984 | 338 |
"[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
339 |
cert M merSK onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
340 |
cert M merEK onlyEnc (priSK (CA i)), |
61984 | 341 |
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs; |
342 |
Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>, |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
343 |
cert M' merSK onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
344 |
cert M' merEK' onlyEnc (priSK (CA i)), |
61984 | 345 |
cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs; |
67613 | 346 |
evs \<in> set_mr |] ==> M=M' \<and> NM2=NM2' \<and> merEK=merEK'" |
14199 | 347 |
apply (erule rev_mp) |
348 |
apply (erule rev_mp) |
|
349 |
apply (erule set_mr.induct) |
|
350 |
apply (simp_all (no_asm_simp)) |
|
351 |
apply (blast dest!: msg4_Says_imp_Notes) |
|
352 |
done |
|
353 |
||
63167 | 354 |
text\<open>Unicity of merEK wrt a given CA: |
355 |
merEK uniquely identifies the other components, including merSK\<close> |
|
14199 | 356 |
lemma merEK_unicity: |
61984 | 357 |
"[|Says (CA i) M \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M, Nonce NM2, Agent (CA i)\<rbrace>, |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
358 |
cert M merSK onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
359 |
cert M merEK onlyEnc (priSK (CA i)), |
61984 | 360 |
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs; |
361 |
Says (CA i) M' \<lbrace>sign (priSK(CA i)) \<lbrace>Agent M', Nonce NM2', Agent (CA i)\<rbrace>, |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
362 |
cert M' merSK' onlySig (priSK (CA i)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
24123
diff
changeset
|
363 |
cert M' merEK onlyEnc (priSK (CA i)), |
61984 | 364 |
cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)\<rbrace> \<in> set evs; |
14199 | 365 |
evs \<in> set_mr |] |
67613 | 366 |
==> M=M' \<and> NM2=NM2' \<and> merSK=merSK'" |
14199 | 367 |
apply (erule rev_mp) |
368 |
apply (erule rev_mp) |
|
369 |
apply (erule set_mr.induct) |
|
370 |
apply (simp_all (no_asm_simp)) |
|
371 |
apply (blast dest!: msg4_Says_imp_Notes) |
|
372 |
done |
|
373 |
||
374 |
||
63167 | 375 |
text\<open>-No interest on secrecy of nonces: they appear to be used |
14199 | 376 |
only for freshness. |
377 |
-No interest on secrecy of merSK or merEK, as in CR. |
|
63167 | 378 |
-There's no equivalent of the PAN\<close> |
14199 | 379 |
|
380 |
||
63167 | 381 |
subsection\<open>Primary Goals of Merchant Registration\<close> |
14199 | 382 |
|
63167 | 383 |
subsubsection\<open>The merchant's certificates really were created by the CA, |
384 |
provided the CA is uncompromised\<close> |
|
14199 | 385 |
|
63167 | 386 |
text\<open>The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses |
387 |
certificates of the same form.\<close> |
|
14199 | 388 |
lemma certificate_merSK_valid_lemma [intro]: |
61984 | 389 |
"[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merSK, onlySig\<rbrace> |
14199 | 390 |
\<in> parts (knows Spy evs); |
391 |
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|] |
|
392 |
==> \<exists>X Y Z. Says (CA i) M |
|
61984 | 393 |
\<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs" |
14199 | 394 |
apply (erule rev_mp) |
395 |
apply (erule set_mr.induct) |
|
396 |
apply (simp_all (no_asm_simp)) |
|
397 |
apply auto |
|
398 |
done |
|
399 |
||
400 |
lemma certificate_merSK_valid: |
|
401 |
"[| cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs); |
|
402 |
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|] |
|
403 |
==> \<exists>X Y Z. Says (CA i) M |
|
61984 | 404 |
\<lbrace>X, cert M merSK onlySig (priSK (CA i)), Y, Z\<rbrace> \<in> set evs" |
14199 | 405 |
by auto |
406 |
||
407 |
lemma certificate_merEK_valid_lemma [intro]: |
|
61984 | 408 |
"[|Crypt (priSK (CA i)) \<lbrace>Agent M, Key merEK, onlyEnc\<rbrace> |
14199 | 409 |
\<in> parts (knows Spy evs); |
410 |
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|] |
|
411 |
==> \<exists>X Y Z. Says (CA i) M |
|
61984 | 412 |
\<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs" |
14199 | 413 |
apply (erule rev_mp) |
414 |
apply (erule set_mr.induct) |
|
415 |
apply (simp_all (no_asm_simp)) |
|
416 |
apply auto |
|
417 |
done |
|
418 |
||
419 |
lemma certificate_merEK_valid: |
|
420 |
"[| cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs); |
|
421 |
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr|] |
|
422 |
==> \<exists>X Y Z. Says (CA i) M |
|
61984 | 423 |
\<lbrace>X, Y, cert M merEK onlyEnc (priSK (CA i)), Z\<rbrace> \<in> set evs" |
14199 | 424 |
by auto |
425 |
||
63167 | 426 |
text\<open>The two certificates - for merSK and for merEK - cannot be proved to |
427 |
have originated together\<close> |
|
14199 | 428 |
|
429 |
end |