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