1 (* Title: HOL/SET_Protocol/Cardholder_Registration.thy
2 Author: Giampaolo Bella
4 Author: Lawrence C Paulson
5 Author: Piero Tramontano
8 header{*The SET Cardholder Registration Protocol*}
10 theory Cardholder_Registration
14 text{*Note: nonces seem to consist of 20 bytes. That includes both freshness
15 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
18 text{*Simplifications involving @{text analz_image_keys_simps} appear to
19 have become much slower. The cause is unclear. However, there is a big blow-up
20 and the rewriting is very sensitive to the set of rewrite rules given.*}
22 subsection{*Predicate Formalizing the Encryption Association between Keys *}
24 primrec KeyCryptKey :: "[key, key, event list] => bool"
27 "KeyCryptKey DK K [] = False"
29 --{*Says is the only important case.
30 1st case: CR5, where KC3 encrypts KC2.
31 2nd case: any use of priEK C.
32 Revision 1.12 has a more complicated version with separate treatment of
33 the dependency of KC1, KC2 and KC3 on priEK (CA i.) Not needed since
34 priEK C is never sent (and so can't be lost except at the start). *}
35 "KeyCryptKey DK K (ev # evs) =
36 (KeyCryptKey DK K evs |
39 ((\<exists>N X Y. A \<noteq> Spy &
41 Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
42 (\<exists>C. DK = priEK C))
44 | Notes A' X => False))"
47 subsection{*Predicate formalizing the association between keys and nonces *}
49 primrec KeyCryptNonce :: "[key, key, event list] => bool"
52 "KeyCryptNonce EK K [] = False"
54 --{*Says is the only important case.
55 1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
56 2nd case: CR5, where KC3 encrypts NC3;
57 3rd case: CR6, where KC2 encrypts NC3;
58 4th case: CR6, where KC2 encrypts NonceCCA;
59 5th case: any use of @{term "priEK C"} (including CardSecret).
60 NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
61 But we can't prove @{text Nonce_compromise} unless the relation covers ALL
62 nonces that the protocol keeps secret.
64 "KeyCryptNonce DK N (ev # evs) =
65 (KeyCryptNonce DK N evs |
69 ((\<exists>X Y. DK \<in> symKeys &
70 Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
71 (\<exists>X Y. DK \<in> symKeys &
72 Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
75 Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
76 (DK=K | KeyCryptKey DK K evs)) |
80 {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
82 (DK=K | KeyCryptKey DK K evs)) |
83 (\<exists>C. DK = priEK C))
85 | Notes A' X => False))"
88 subsection{*Formal protocol definition *}
91 set_cr :: "event list set"
94 Nil: --{*Initial trace is empty*}
97 | Fake: --{*The spy MAY say anything he CAN say.*}
98 "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
99 ==> Says Spy B X # evsf \<in> set_cr"
101 | Reception: --{*If A sends a message X to B, then B might receive it*}
102 "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
103 ==> Gets B X # evsr \<in> set_cr"
105 | SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
106 "[| evs1 \<in> set_cr; C = Cardholder k; Nonce NC1 \<notin> used evs1 |]
107 ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
109 | SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
110 "[| evs2 \<in> set_cr;
111 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
113 {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
114 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
115 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
119 --{*RegFormReq: C sends his PAN and a new nonce to CA.
121 - nonce received is the same as that sent;
122 - certificates are signed by RCA;
123 - certificates are an encryption certificate (flag is onlyEnc) and a
124 signature certificate (flag is onlySig);
125 - certificates pertain to the CA that C contacted (this is done by
126 checking the signature).
127 C generates a fresh symmetric key KC1.
128 The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
130 "[| evs3 \<in> set_cr; C = Cardholder k;
131 Nonce NC2 \<notin> used evs3;
132 Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
133 Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
134 cert (CA i) EKi onlyEnc (priSK RCA),
135 cert (CA i) SKi onlySig (priSK RCA)|}
137 Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
138 ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
139 # Notes C {|Key KC1, Agent (CA i)|}
144 CA responds sending NC2 back with a new nonce NCA, after checking that
145 - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
146 - the entire message is encrypted with the same key found inside the
147 envelope (here, KC1) *}
148 "[| evs4 \<in> set_cr;
149 Nonce NCA \<notin> used evs4; KC1 \<in> symKeys;
150 Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
153 {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
154 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
155 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
159 --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
160 and its half of the secret value to CA.
161 We now assume that C has a fixed key pair, and he submits (pubSK C).
162 The protocol does not require this key to be fresh.
163 The encryption below is actually EncX.*}
164 "[| evs5 \<in> set_cr; C = Cardholder k;
165 Nonce NC3 \<notin> used evs5; Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
166 Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
167 Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
168 Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
169 cert (CA i) EKi onlyEnc (priSK RCA),
170 cert (CA i) SKi onlySig (priSK RCA) |}
172 Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
176 {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
178 (Hash {|Agent C, Nonce NC3, Key KC2,
179 Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
180 Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
181 # Notes C {|Key KC2, Agent (CA i)|}
182 # Notes C {|Key KC3, Agent (CA i)|}
186 --{* CertRes: CA responds sending NC3 back with its half of the secret value,
187 its signature certificate and the new cardholder signature
188 certificate. CA checks to have never certified the key proposed by C.
189 NOTE: In Merchant Registration, the corresponding rule (4)
190 uses the "sign" primitive. The encryption below is actually @{term EncK},
191 which is just @{term "Crypt K (sign SK X)"}.
195 "[| evs6 \<in> set_cr;
196 Nonce NonceCCA \<notin> used evs6;
197 KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys;
198 Notes (CA i) (Key cardSK) \<notin> set evs6;
200 {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
201 Crypt (invKey cardSK)
202 (Hash {|Agent C, Nonce NC3, Key KC2,
203 Key cardSK, Pan (pan C), Nonce CardSecret|})|},
204 Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
208 {|sign (priSK (CA i))
209 {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
210 certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
211 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
212 # Notes (CA i) (Key cardSK)
216 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
217 declare parts.Body [dest]
218 declare analz_into_parts [dest]
219 declare Fake_parts_insert_in_Un [dest]
221 text{*A "possibility property": there are traces that reach the end.
222 An unconstrained proof with many subgoals.*}
225 "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
226 by (rule set_cr.Reception, auto)
228 text{*The many nonces and keys generated, some simultaneously, force us to
229 introduce them explicitly as shown below.*}
230 lemma possibility_CR6:
231 "[|NC1 < (NC2::nat); NC2 < NC3; NC3 < NCA ;
232 NCA < NonceCCA; NonceCCA < CardSecret;
233 KC1 < (KC2::key); KC2 < KC3;
234 KC1 \<in> symKeys; Key KC1 \<notin> used [];
235 KC2 \<in> symKeys; Key KC2 \<notin> used [];
236 KC3 \<in> symKeys; Key KC3 \<notin> used [];
238 ==> \<exists>evs \<in> set_cr.
241 {|sign (priSK (CA i))
242 {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
243 certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
244 onlySig (priSK (CA i)),
245 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
247 apply (intro exI bexI)
250 [THEN set_cr.SET_CR1 [of concl: C i NC1],
252 THEN set_cr.SET_CR2 [of concl: i C NC1],
254 THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2],
256 THEN set_cr.SET_CR4 [of concl: i C NC2 NCA],
258 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
260 THEN set_cr.SET_CR6 [of concl: i C KC2]])
261 apply basic_possibility
262 apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
265 text{*General facts about message reception*}
267 "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
269 apply (erule set_cr.induct, auto)
272 lemma Gets_imp_knows_Spy:
273 "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> X \<in> knows Spy evs"
274 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
275 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
278 subsection{*Proofs on keys *}
280 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
282 lemma Spy_see_private_Key [simp]:
284 ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
285 by (erule set_cr.induct, auto)
287 lemma Spy_analz_private_Key [simp]:
288 "evs \<in> set_cr ==>
289 (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
292 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
293 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
296 subsection{*Begin Piero's Theorems on Certificates*}
297 text{*Trivial in the current model, where certificates by RCA are secure *}
299 lemma Crypt_valid_pubEK:
300 "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
301 \<in> parts (knows Spy evs);
302 evs \<in> set_cr |] ==> EKi = pubEK C"
304 apply (erule set_cr.induct, auto)
307 lemma certificate_valid_pubEK:
308 "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
311 apply (unfold cert_def signCert_def)
312 apply (blast dest!: Crypt_valid_pubEK)
315 lemma Crypt_valid_pubSK:
316 "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
317 \<in> parts (knows Spy evs);
318 evs \<in> set_cr |] ==> SKi = pubSK C"
320 apply (erule set_cr.induct, auto)
323 lemma certificate_valid_pubSK:
324 "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
325 evs \<in> set_cr |] ==> SKi = pubSK C"
326 apply (unfold cert_def signCert_def)
327 apply (blast dest!: Crypt_valid_pubSK)
330 lemma Gets_certificate_valid:
331 "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
332 cert C SKi onlySig (priSK RCA)|} \<in> set evs;
334 ==> EKi = pubEK C & SKi = pubSK C"
335 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
337 text{*Nobody can have used non-existent keys!*}
338 lemma new_keys_not_used:
339 "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
340 ==> K \<notin> keysFor (parts (knows Spy evs))"
343 apply (erule set_cr.induct)
344 apply (frule_tac [8] Gets_certificate_valid)
345 apply (frule_tac [6] Gets_certificate_valid, simp_all)
346 apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
347 apply (blast,auto) --{*Others*}
351 subsection{*New versions: as above, but generalized to have the KK argument *}
353 lemma gen_new_keys_not_used:
354 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
355 ==> Key K \<notin> used evs --> K \<in> symKeys -->
356 K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
357 by (auto simp add: new_keys_not_used)
359 lemma gen_new_keys_not_analzd:
360 "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
361 ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
362 by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
363 dest: gen_new_keys_not_used)
365 lemma analz_Key_image_insert_eq:
366 "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
367 ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
368 insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
369 by (simp add: gen_new_keys_not_analzd)
371 lemma Crypt_parts_imp_used:
372 "[|Crypt K X \<in> parts (knows Spy evs);
373 K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
375 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
378 lemma Crypt_analz_imp_used:
379 "[|Crypt K X \<in> analz (knows Spy evs);
380 K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
381 by (blast intro: Crypt_parts_imp_used)
385 subsection{*Messages signed by CA*}
387 text{*Message @{text SET_CR2}: C can check CA's signature if he has received
389 lemma CA_Says_2_lemma:
390 "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
391 \<in> parts (knows Spy evs);
392 evs \<in> set_cr; (CA i) \<notin> bad |]
393 ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
396 apply (erule set_cr.induct, auto)
401 "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
402 \<in> parts (knows Spy evs);
403 cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
404 evs \<in> set_cr; (CA i) \<notin> bad |]
405 ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
407 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
410 text{*Message @{text SET_CR4}: C can check CA's signature if he has received
412 lemma CA_Says_4_lemma:
413 "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
414 \<in> parts (knows Spy evs);
415 evs \<in> set_cr; (CA i) \<notin> bad |]
416 ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
417 {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
419 apply (erule set_cr.induct, auto)
424 "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
425 \<in> parts (knows Spy evs);
426 cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
427 evs \<in> set_cr; (CA i) \<notin> bad |]
428 ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
429 {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
430 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
433 text{*Message @{text SET_CR6}: C can check CA's signature if he has
434 received CA's certificate.*}
435 lemma CA_Says_6_lemma:
436 "[| Crypt (priSK (CA i))
437 (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
438 \<in> parts (knows Spy evs);
439 evs \<in> set_cr; (CA i) \<notin> bad |]
440 ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
441 {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
443 apply (erule set_cr.induct, auto)
448 "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
449 \<in> parts (knows Spy evs);
450 cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
451 evs \<in> set_cr; (CA i) \<notin> bad |]
452 ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
453 {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
454 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
458 subsection{*Useful lemmas *}
460 text{*Rewriting rule for private encryption keys. Analogous rewriting rules
461 for other keys aren't needed.*}
463 lemma parts_image_priEK:
464 "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
465 evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
468 text{*trivial proof because (priEK C) never appears even in (parts evs)*}
469 lemma analz_image_priEK:
470 "evs \<in> set_cr ==>
471 (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
472 (priEK C \<in> KK | C \<in> bad)"
473 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
476 subsection{*Secrecy of Session Keys *}
478 subsubsection{*Lemmas about the predicate KeyCryptKey *}
480 text{*A fresh DK cannot be associated with any other
481 (with respect to a given trace). *}
482 lemma DK_fresh_not_KeyCryptKey:
483 "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
485 apply (erule set_cr.induct)
486 apply (simp_all (no_asm_simp))
487 apply (blast dest: Crypt_analz_imp_used)+
490 text{*A fresh K cannot be associated with any other. The assumption that
491 DK isn't a private encryption key may be an artifact of the particular
492 definition of KeyCryptKey.*}
493 lemma K_fresh_not_KeyCryptKey:
494 "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
496 apply (auto simp add: parts_insert2 split add: event.split)
500 text{*This holds because if (priEK (CA i)) appears in any traffic then it must
501 be known to the Spy, by @{term Spy_see_private_Key}*}
502 lemma cardSK_neq_priEK:
503 "[|Key cardSK \<notin> analz (knows Spy evs);
504 Key cardSK : parts (knows Spy evs);
505 evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
508 lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
509 "[|cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr|] ==>
510 Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
511 by (erule set_cr.induct, analz_mono_contra, auto)
513 text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
514 lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
515 apply (induct_tac "evs")
516 apply (auto simp add: parts_insert2 split add: event.split)
519 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
520 or else cardSK hasn't been used to encrypt K. Previously we treated
521 message 5 in the same way, but the current model assumes that rule
522 @{text SET_CR5} is executed only by honest agents.*}
523 lemma msg6_KeyCryptKey_disj:
524 "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
526 cardSK \<notin> symKeys; evs \<in> set_cr|]
527 ==> Key cardSK \<in> analz (knows Spy evs) |
528 (\<forall>K. ~ KeyCryptKey cardSK K evs)"
529 by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
531 text{*As usual: we express the property as a logical equivalence*}
532 lemma Key_analz_image_Key_lemma:
533 "P --> (Key K \<in> analz (Key`KK Un H)) --> (K \<in> KK | Key K \<in> analz H)
535 P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
536 by (blast intro: analz_mono [THEN [2] rev_subsetD])
538 method_setup valid_certificate_tac = {*
539 Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
541 EVERY [ftac @{thm Gets_certificate_valid} i,
543 etac conjE i, REPEAT (hyp_subst_tac i)])))
546 text{*The @{text "(no_asm)"} attribute is essential, since it retains
547 the quantifier and allows the simprule's condition to itself be simplified.*}
548 lemma symKey_compromise [rule_format (no_asm)]:
549 "evs \<in> set_cr ==>
550 (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) -->
551 (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
552 (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
553 apply (erule set_cr.induct)
554 apply (rule_tac [!] allI) +
555 apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
556 apply (valid_certificate_tac [8]) --{*for message 5*}
557 apply (valid_certificate_tac [6]) --{*for message 5*}
558 apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
560 del: image_insert image_Un imp_disjL
561 add: analz_image_keys_simps analz_knows_absorb
562 analz_Key_image_insert_eq notin_image_iff
563 K_fresh_not_KeyCryptKey
564 DK_fresh_not_KeyCryptKey ball_conj_distrib
565 analz_image_priEK disj_simps)
566 --{*9 seconds on a 1.6GHz machine*}
572 text{*The remaining quantifiers seem to be essential.
573 NO NEED to assume the cardholder's OK: bad cardholders don't do anything
575 lemma symKey_secrecy [rule_format]:
576 "[|CA i \<notin> bad; K \<in> symKeys; evs \<in> set_cr|]
577 ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
578 Key K \<in> parts{X} -->
579 Cardholder c \<notin> bad -->
580 Key K \<notin> analz (knows Spy evs)"
581 apply (erule set_cr.induct)
582 apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
583 apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
584 apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
585 apply (simp_all del: image_insert image_Un imp_disjL
586 add: symKey_compromise fresh_notin_analz_knows_Spy
587 analz_image_keys_simps analz_knows_absorb
588 analz_Key_image_insert_eq notin_image_iff
589 K_fresh_not_KeyCryptKey
590 DK_fresh_not_KeyCryptKey
592 --{*2.5 seconds on a 1.6GHz machine*}
593 apply spy_analz --{*Fake*}
594 apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
598 subsection{*Primary Goals of Cardholder Registration *}
600 text{*The cardholder's certificate really was created by the CA, provided the
601 CA is uncompromised *}
603 text{*Lemma concerning the actual signed message digest*}
604 lemma cert_valid_lemma:
605 "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
606 \<in> parts (knows Spy evs);
607 CA i \<notin> bad; evs \<in> set_cr|]
608 ==> \<exists>KC2 X Y. Says (CA i) C
610 {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
613 apply (erule set_cr.induct)
614 apply (simp_all (no_asm_simp))
618 text{*Pre-packaged version for cardholder. We don't try to confirm the values
619 of KC2, X and Y, since they are not important.*}
620 lemma certificate_valid_cardSK:
621 "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
622 cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
623 CA i \<notin> bad; evs \<in> set_cr|]
624 ==> \<exists>KC2 X Y. Says (CA i) C
626 {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
628 by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
629 certificate_valid_pubSK cert_valid_lemma)
632 lemma Hash_imp_parts [rule_format]:
634 ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
635 Nonce N \<in> parts (knows Spy evs)"
636 apply (erule set_cr.induct, force)
637 apply (simp_all (no_asm_simp))
638 apply (blast intro: parts_mono [THEN [2] rev_subsetD])
641 lemma Hash_imp_parts2 [rule_format]:
643 ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
644 Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
645 apply (erule set_cr.induct, force)
646 apply (simp_all (no_asm_simp))
647 apply (blast intro: parts_mono [THEN [2] rev_subsetD])
651 subsection{*Secrecy of Nonces*}
653 subsubsection{*Lemmas about the predicate KeyCryptNonce *}
655 text{*A fresh DK cannot be associated with any other
656 (with respect to a given trace). *}
657 lemma DK_fresh_not_KeyCryptNonce:
658 "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
659 ==> ~ KeyCryptNonce DK K evs"
662 apply (erule set_cr.induct)
663 apply (simp_all (no_asm_simp))
666 apply (auto simp add: DK_fresh_not_KeyCryptKey)
669 text{*A fresh N cannot be associated with any other
670 (with respect to a given trace). *}
671 lemma N_fresh_not_KeyCryptNonce:
672 "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
673 apply (induct_tac "evs")
674 apply (case_tac [2] "a")
675 apply (auto simp add: parts_insert2)
678 lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
679 "[|cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr|] ==>
680 Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
681 apply (erule set_cr.induct, analz_mono_contra, simp_all)
682 apply (blast dest: not_KeyCryptKey_cardSK) --{*6*}
685 subsubsection{*Lemmas for message 5 and 6:
686 either cardSK is compromised (when we don't care)
687 or else cardSK hasn't been used to encrypt K. *}
689 text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
690 lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
691 apply (induct_tac "evs")
692 apply (auto simp add: parts_insert2 split add: event.split)
695 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
696 or else cardSK hasn't been used to encrypt K.*}
697 lemma msg6_KeyCryptNonce_disj:
698 "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
700 cardSK \<notin> symKeys; evs \<in> set_cr|]
701 ==> Key cardSK \<in> analz (knows Spy evs) |
702 ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
703 (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
704 by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
705 intro: cardSK_neq_priEK)
708 text{*As usual: we express the property as a logical equivalence*}
709 lemma Nonce_analz_image_Key_lemma:
710 "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
711 ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
712 by (blast intro: analz_mono [THEN [2] rev_subsetD])
715 text{*The @{text "(no_asm)"} attribute is essential, since it retains
716 the quantifier and allows the simprule's condition to itself be simplified.*}
717 lemma Nonce_compromise [rule_format (no_asm)]:
718 "evs \<in> set_cr ==>
719 (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs) -->
720 (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
721 (Nonce N \<in> analz (knows Spy evs)))"
722 apply (erule set_cr.induct)
723 apply (rule_tac [!] allI)+
724 apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
725 apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
726 apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
727 apply (frule_tac [11] msg6_KeyCryptNonce_disj)
728 apply (erule_tac [13] disjE)
729 apply (simp_all del: image_insert image_Un
730 add: symKey_compromise
731 analz_image_keys_simps analz_knows_absorb
732 analz_Key_image_insert_eq notin_image_iff
733 N_fresh_not_KeyCryptNonce
734 DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
735 ball_conj_distrib analz_image_priEK)
736 --{*14 seconds on a 1.6GHz machine*}
737 apply spy_analz --{*Fake*}
741 apply (metis symKey_compromise)
742 --{*cardSK compromised*}
743 txt{*Simplify again--necessary because the previous simplification introduces
744 some logical connectives*}
745 apply (force simp del: image_insert image_Un imp_disjL
746 simp add: analz_image_keys_simps symKey_compromise)
750 subsection{*Secrecy of CardSecret: the Cardholder's secret*}
752 lemma NC2_not_CardSecret:
753 "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
754 \<in> parts (knows Spy evs);
755 Key K \<notin> analz (knows Spy evs);
756 Nonce N \<notin> analz (knows Spy evs);
758 ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
762 apply (erule set_cr.induct, analz_mono_contra, simp_all)
763 apply (blast dest: Hash_imp_parts)+
766 lemma KC2_secure_lemma [rule_format]:
767 "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
768 U \<in> parts (knows Spy evs);
770 ==> Nonce N \<notin> analz (knows Spy evs) -->
771 (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs &
772 Cardholder k \<notin> bad & CA i \<notin> bad)"
773 apply (erule_tac P = "U \<in> ?H" in rev_mp)
774 apply (erule set_cr.induct)
775 apply (valid_certificate_tac [8]) --{*for message 5*}
776 apply (simp_all del: image_insert image_Un imp_disjL
777 add: analz_image_keys_simps analz_knows_absorb
778 analz_knows_absorb2 notin_image_iff)
779 --{*4 seconds on a 1.6GHz machine*}
780 apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
781 apply (blast intro!: analz_insertI)+
785 "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
786 Nonce N \<notin> analz (knows Spy evs); KC2 \<in> symKeys;
788 ==> Key KC2 \<notin> analz (knows Spy evs)"
789 by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
792 text{*Inductive version*}
793 lemma CardSecret_secrecy_lemma [rule_format]:
794 "[|CA i \<notin> bad; evs \<in> set_cr|]
795 ==> Key K \<notin> analz (knows Spy evs) -->
796 Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
797 \<in> parts (knows Spy evs) -->
798 Nonce CardSecret \<notin> analz (knows Spy evs)"
799 apply (erule set_cr.induct, analz_mono_contra)
800 apply (valid_certificate_tac [8]) --{*for message 5*}
801 apply (valid_certificate_tac [6]) --{*for message 5*}
802 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
804 del: image_insert image_Un imp_disjL
805 add: analz_image_keys_simps analz_knows_absorb
806 analz_Key_image_insert_eq notin_image_iff
807 EXHcrypt_def Crypt_notin_image_Key
808 N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
809 ball_conj_distrib Nonce_compromise symKey_compromise
811 --{*2.5 seconds on a 1.6GHz machine*}
812 apply spy_analz --{*Fake*}
813 apply (simp_all (no_asm_simp))
815 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*}
817 apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) --{*4*}
819 apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*}
823 text{*Packaged version for cardholder*}
824 lemma CardSecret_secrecy:
825 "[|Cardholder k \<notin> bad; CA i \<notin> bad;
826 Says (Cardholder k) (CA i)
827 {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
828 Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
829 cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
830 KC3 \<in> symKeys; evs \<in> set_cr|]
831 ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
832 apply (frule Gets_certificate_valid, assumption)
833 apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
834 apply (blast dest: CardSecret_secrecy_lemma)
835 apply (rule symKey_secrecy)
836 apply (auto simp add: parts_insert2)
840 subsection{*Secrecy of NonceCCA [the CA's secret] *}
842 lemma NC2_not_NonceCCA:
843 "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
844 \<in> parts (knows Spy evs);
845 Nonce N \<notin> analz (knows Spy evs);
847 ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
850 apply (erule set_cr.induct, analz_mono_contra, simp_all)
851 apply (blast dest: Hash_imp_parts2)+
855 text{*Inductive version*}
856 lemma NonceCCA_secrecy_lemma [rule_format]:
857 "[|CA i \<notin> bad; evs \<in> set_cr|]
858 ==> Key K \<notin> analz (knows Spy evs) -->
860 {|sign (priSK (CA i))
861 {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
863 \<in> parts (knows Spy evs) -->
864 Nonce NonceCCA \<notin> analz (knows Spy evs)"
865 apply (erule set_cr.induct, analz_mono_contra)
866 apply (valid_certificate_tac [8]) --{*for message 5*}
867 apply (valid_certificate_tac [6]) --{*for message 5*}
868 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
870 del: image_insert image_Un imp_disjL
871 add: analz_image_keys_simps analz_knows_absorb sign_def
872 analz_Key_image_insert_eq notin_image_iff
873 EXHcrypt_def Crypt_notin_image_Key
874 N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
875 ball_conj_distrib Nonce_compromise symKey_compromise
877 --{*3 seconds on a 1.6GHz machine*}
878 apply spy_analz --{*Fake*}
880 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) --{*2*}
882 apply (blast dest: NC2_not_NonceCCA) --{*4*}
884 apply (blast dest: KC2_secrecy)+ --{*Message 6: two cases*}
888 text{*Packaged version for cardholder*}
889 lemma NonceCCA_secrecy:
890 "[|Cardholder k \<notin> bad; CA i \<notin> bad;
893 {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
894 X, Y|}) \<in> set evs;
895 Says (Cardholder k) (CA i)
896 {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
897 Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
898 cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
899 KC2 \<in> symKeys; evs \<in> set_cr|]
900 ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
901 apply (frule Gets_certificate_valid, assumption)
902 apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
903 apply (blast dest: NonceCCA_secrecy_lemma)
904 apply (rule symKey_secrecy)
905 apply (auto simp add: parts_insert2)
908 text{*We don't bother to prove guarantees for the CA. He doesn't care about
909 the PANSecret: it isn't his credit card!*}
912 subsection{*Rewriting Rule for PANs*}
914 text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
915 or if it is then (because it appears in traffic) that CA is bad,
916 and so the Spy knows that key already. Either way, we can simplify
917 the expression @{term "analz (insert (Key cardSK) X)"}.*}
918 lemma msg6_cardSK_disj:
919 "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
920 \<in> set evs; evs \<in> set_cr |]
921 ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
924 lemma analz_image_pan_lemma:
925 "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H) ==>
926 (Pan P \<in> analz (Key`nE Un H)) = (Pan P \<in> analz H)"
927 by (blast intro: analz_mono [THEN [2] rev_subsetD])
929 lemma analz_image_pan [rule_format]:
930 "evs \<in> set_cr ==>
931 \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
932 (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
933 (Pan P \<in> analz (knows Spy evs))"
934 apply (erule set_cr.induct)
935 apply (rule_tac [!] allI impI)+
936 apply (rule_tac [!] analz_image_pan_lemma)
937 apply (valid_certificate_tac [8]) --{*for message 5*}
938 apply (valid_certificate_tac [6]) --{*for message 5*}
939 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
941 del: image_insert image_Un
942 add: analz_image_keys_simps disjoint_image_iff
943 notin_image_iff analz_image_priEK)
944 --{*6 seconds on a 1.6GHz machine*}
946 apply (simp add: insert_absorb) --{*6*}
949 lemma analz_insert_pan:
950 "[| evs \<in> set_cr; K \<notin> invKey ` pubEK ` range CA |] ==>
951 (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
952 (Pan P \<in> analz (knows Spy evs))"
953 by (simp del: image_insert image_Un
954 add: analz_image_keys_simps analz_image_pan)
957 text{*Confidentiality of the PAN\@. Maybe we could combine the statements of
958 this theorem with @{term analz_image_pan}, requiring a single induction but
959 a much more difficult proof.*}
960 lemma pan_confidentiality:
961 "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
962 ==> \<exists>i X K HN.
963 Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
967 apply (erule set_cr.induct)
968 apply (valid_certificate_tac [8]) --{*for message 5*}
969 apply (valid_certificate_tac [6]) --{*for message 5*}
970 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
972 del: image_insert image_Un
973 add: analz_image_keys_simps analz_insert_pan analz_image_pan
974 notin_image_iff analz_image_priEK)
975 --{*3.5 seconds on a 1.6GHz machine*}
976 apply spy_analz --{*fake*}
979 apply (simp (no_asm_simp) add: insert_absorb) --{*6*}
983 subsection{*Unicity*}
985 lemma CR6_Says_imp_Notes:
986 "[|Says (CA i) C (Crypt KC2
987 {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
988 certC (pan C) cardSK X onlySig (priSK (CA i)),
989 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}) \<in> set evs;
991 ==> Notes (CA i) (Key cardSK) \<in> set evs"
993 apply (erule set_cr.induct)
994 apply (simp_all (no_asm_simp))
997 text{*Unicity of cardSK: it uniquely identifies the other components.
998 This holds because a CA accepts a cardSK at most once.*}
999 lemma cardholder_key_unicity:
1000 "[|Says (CA i) C (Crypt KC2
1001 {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
1002 certC (pan C) cardSK X onlySig (priSK (CA i)),
1003 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
1005 Says (CA i) C' (Crypt KC2'
1006 {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
1007 certC (pan C') cardSK X' onlySig (priSK (CA i)),
1008 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
1010 evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
1011 apply (erule rev_mp)
1012 apply (erule rev_mp)
1013 apply (erule set_cr.induct)
1014 apply (simp_all (no_asm_simp))
1015 apply (blast dest!: CR6_Says_imp_Notes)
1020 text{*UNUSED unicity result*}
1022 "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
1024 Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
1026 C \<notin> bad; evs \<in> set_cr|] ==> B'=B & Y'=Y"
1027 apply (erule rev_mp)
1028 apply (erule rev_mp)
1029 apply (erule set_cr.induct, auto)
1032 text{*UNUSED unicity result*}
1034 "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
1035 Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
1036 C \<notin> bad; evs \<in> set_cr|] ==> B'=B & X'=X"
1037 apply (erule rev_mp)
1038 apply (erule rev_mp)
1039 apply (erule set_cr.induct, auto)
1044 text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
1045 it could be a previously compromised cardSK [e.g. involving a bad CA]*}