src/HOL/SET_Protocol/Cardholder_Registration.thy
author wenzelm
Sat Jul 18 22:58:50 2015 +0200 (2015-07-18)
changeset 60758 d8d85a8172b5
parent 60754 02924903a6fd
child 61984 cdea44c775fa
permissions -rw-r--r--
isabelle update_cartouches;
     1 (*  Title:      HOL/SET_Protocol/Cardholder_Registration.thy
     2     Author:     Giampaolo Bella
     3     Author:     Fabio Massacci
     4     Author:     Lawrence C Paulson
     5     Author:     Piero Tramontano
     6 *)
     7 
     8 section{*The SET Cardholder Registration Protocol*}
     9 
    10 theory Cardholder_Registration
    11 imports Public_SET
    12 begin
    13 
    14 text{*Note: nonces seem to consist of 20 bytes.  That includes both freshness
    15 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
    16 *}
    17 
    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.*}
    21 
    22 subsection{*Predicate Formalizing the Encryption Association between Keys *}
    23 
    24 primrec KeyCryptKey :: "[key, key, event list] => bool"
    25 where
    26   KeyCryptKey_Nil:
    27     "KeyCryptKey DK K [] = False"
    28 | KeyCryptKey_Cons:
    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 |
    37       (case ev of
    38         Says A B Z =>
    39          ((\<exists>N X Y. A \<noteq> Spy &
    40                  DK \<in> symKeys &
    41                  Z = {|Crypt DK {|Agent A, Nonce N, Key K, X|}, Y|}) |
    42           (\<exists>C. DK = priEK C))
    43       | Gets A' X => False
    44       | Notes A' X => False))"
    45 
    46 
    47 subsection{*Predicate formalizing the association between keys and nonces *}
    48 
    49 primrec KeyCryptNonce :: "[key, key, event list] => bool"
    50 where
    51   KeyCryptNonce_Nil:
    52     "KeyCryptNonce EK K [] = False"
    53 | KeyCryptNonce_Cons:
    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.
    63   *}
    64   "KeyCryptNonce DK N (ev # evs) =
    65    (KeyCryptNonce DK N evs |
    66     (case ev of
    67       Says A B Z =>
    68        A \<noteq> Spy &
    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|}) |
    73         (\<exists>K i X Y.
    74           K \<in> symKeys &
    75           Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
    76           (DK=K | KeyCryptKey DK K evs)) |
    77         (\<exists>K C NC3 Y.
    78           K \<in> symKeys &
    79           Z = Crypt K
    80                 {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
    81                   Y|} &
    82           (DK=K | KeyCryptKey DK K evs)) |
    83         (\<exists>C. DK = priEK C))
    84     | Gets A' X => False
    85     | Notes A' X => False))"
    86 
    87 
    88 subsection{*Formal protocol definition *}
    89 
    90 inductive_set
    91   set_cr :: "event list set"
    92 where
    93 
    94   Nil:    --{*Initial trace is empty*}
    95           "[] \<in> set_cr"
    96 
    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"
   100 
   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"
   104 
   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"
   108 
   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 |]
   112               ==> Says (CA i) C
   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)|}
   116                     # evs2 \<in> set_cr"
   117 
   118 | SET_CR3:
   119    --{*RegFormReq: C sends his PAN and a new nonce to CA.
   120    C verifies that
   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))|}"}
   129    is not clear. *}
   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)|}
   136        \<in> set evs3;
   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)|}
   140        # evs3 \<in> set_cr"
   141 
   142 | SET_CR4:
   143     --{*RegFormRes:
   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)))
   151        \<in> set evs4 |]
   152   ==> Says (CA i) C
   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)|}
   156        # evs4 \<in> set_cr"
   157 
   158 | SET_CR5:
   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) |}
   171         \<in> set evs5;
   172     Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
   173          \<in> set evs5 |]
   174 ==> Says C (CA i)
   175          {|Crypt KC3
   176              {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
   177                Crypt (priSK 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)|}
   183     # evs5 \<in> set_cr"
   184 
   185 
   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)"}.
   192 *}
   193 
   194 | SET_CR6:
   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;
   199     Gets (CA i)
   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|} |}
   205       \<in> set evs6 |]
   206 ==> Says (CA i) C
   207          (Crypt KC2
   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)
   213       # evs6 \<in> set_cr"
   214 
   215 
   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]
   220 
   221 text{*A "possibility property": there are traces that reach the end.
   222       An unconstrained proof with many subgoals.*}
   223 
   224 lemma Says_to_Gets:
   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)
   227 
   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 [];
   237         C = Cardholder k|]
   238    ==> \<exists>evs \<in> set_cr.
   239        Says (CA i) C
   240             (Crypt KC2
   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)|})
   246           \<in> set evs"
   247 apply (intro exI bexI)
   248 apply (rule_tac [2] 
   249        set_cr.Nil 
   250         [THEN set_cr.SET_CR1 [of concl: C i NC1], 
   251          THEN Says_to_Gets, 
   252          THEN set_cr.SET_CR2 [of concl: i C NC1], 
   253          THEN Says_to_Gets,  
   254          THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2], 
   255          THEN Says_to_Gets,  
   256          THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], 
   257          THEN Says_to_Gets,  
   258          THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
   259          THEN Says_to_Gets,  
   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)
   263 done
   264 
   265 text{*General facts about message reception*}
   266 lemma Gets_imp_Says:
   267      "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
   268 apply (erule rev_mp)
   269 apply (erule set_cr.induct, auto)
   270 done
   271 
   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]
   276 
   277 
   278 subsection{*Proofs on keys *}
   279 
   280 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   281 
   282 lemma Spy_see_private_Key [simp]:
   283      "evs \<in> set_cr
   284       ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   285 by (erule set_cr.induct, auto)
   286 
   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)"
   290 by auto
   291 
   292 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   293 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   294 
   295 
   296 subsection{*Begin Piero's Theorems on Certificates*}
   297 text{*Trivial in the current model, where certificates by RCA are secure *}
   298 
   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"
   303 apply (erule rev_mp)
   304 apply (erule set_cr.induct, auto)
   305 done
   306 
   307 lemma certificate_valid_pubEK:
   308     "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   309         evs \<in> set_cr |]
   310      ==> EKi = pubEK C"
   311 apply (unfold cert_def signCert_def)
   312 apply (blast dest!: Crypt_valid_pubEK)
   313 done
   314 
   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"
   319 apply (erule rev_mp)
   320 apply (erule set_cr.induct, auto)
   321 done
   322 
   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)
   328 done
   329 
   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;
   333          evs \<in> set_cr |]
   334       ==> EKi = pubEK C & SKi = pubSK C"
   335 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
   336 
   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))"
   341 apply (erule rev_mp)
   342 apply (erule rev_mp)
   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*}
   348 done
   349 
   350 
   351 subsection{*New versions: as above, but generalized to have the KK argument *}
   352 
   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)
   358 
   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)
   364 
   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)
   370 
   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"
   374 apply (rule ccontr)
   375 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   376 done
   377 
   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)
   382 
   383 
   384 (*<*) 
   385 subsection{*Messages signed by CA*}
   386 
   387 text{*Message @{text SET_CR2}: C can check CA's signature if he has received
   388      CA's certificate.*}
   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|}
   394                  \<in> set evs"
   395 apply (erule rev_mp)
   396 apply (erule set_cr.induct, auto)
   397 done
   398 
   399 text{*Ever used?*}
   400 lemma CA_Says_2:
   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|}
   406                   \<in> set evs"
   407 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
   408 
   409 
   410 text{*Message @{text SET_CR4}: C can check CA's signature if he has received
   411       CA's certificate.*}
   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"
   418 apply (erule rev_mp)
   419 apply (erule set_cr.induct, auto)
   420 done
   421 
   422 text{*NEVER USED*}
   423 lemma CA_Says_4:
   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)
   431 
   432 
   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"
   442 apply (erule rev_mp)
   443 apply (erule set_cr.induct, auto)
   444 done
   445 
   446 text{*NEVER USED*}
   447 lemma CA_Says_6:
   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)
   455 (*>*)
   456 
   457 
   458 subsection{*Useful lemmas *}
   459 
   460 text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
   461 for other keys aren't needed.*}
   462 
   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"
   466 by auto
   467 
   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])
   474 
   475 
   476 subsection{*Secrecy of Session Keys *}
   477 
   478 subsubsection{*Lemmas about the predicate KeyCryptKey *}
   479 
   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"
   484 apply (erule rev_mp)
   485 apply (erule set_cr.induct)
   486 apply (simp_all (no_asm_simp))
   487 apply (blast dest: Crypt_analz_imp_used)+
   488 done
   489 
   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"
   495 apply (induct evs)
   496 apply (auto simp add: parts_insert2 split add: event.split)
   497 done
   498 
   499 
   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"
   506 by blast
   507 
   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)
   512 
   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)
   517 done
   518 
   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|}
   525           \<in> set evs;
   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)
   530 
   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)
   534       ==>
   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])
   537 
   538 method_setup valid_certificate_tac = {*
   539   Args.goal_spec >> (fn quant => fn ctxt => SIMPLE_METHOD'' quant
   540     (fn i =>
   541       EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i,
   542              assume_tac ctxt i,
   543              eresolve_tac ctxt [conjE] i, REPEAT (hyp_subst_tac ctxt i)]))
   544 *}
   545 
   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])
   559 apply (simp_all
   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*}
   567 apply spy_analz
   568 apply blast  --{*3*}
   569 apply blast  --{*5*}
   570 done
   571 
   572 text{*The remaining quantifiers seem to be essential.
   573   NO NEED to assume the cardholder's OK: bad cardholders don't do anything
   574   wrong!!*}
   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
   591               analz_image_priEK)
   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)
   595 done
   596 
   597 
   598 subsection{*Primary Goals of Cardholder Registration *}
   599 
   600 text{*The cardholder's certificate really was created by the CA, provided the
   601     CA is uncompromised *}
   602 
   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
   609                      (Crypt KC2 
   610                        {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   611                   \<in> set evs"
   612 apply (erule rev_mp)
   613 apply (erule set_cr.induct)
   614 apply (simp_all (no_asm_simp))
   615 apply auto
   616 done
   617 
   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
   625                      (Crypt KC2 
   626                        {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   627                    \<in> set evs"
   628 by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
   629                     certificate_valid_pubSK cert_valid_lemma)
   630 
   631 
   632 lemma Hash_imp_parts [rule_format]:
   633      "evs \<in> set_cr
   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])
   639 done
   640 
   641 lemma Hash_imp_parts2 [rule_format]:
   642      "evs \<in> set_cr
   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])
   648 done
   649 
   650 
   651 subsection{*Secrecy of Nonces*}
   652 
   653 subsubsection{*Lemmas about the predicate KeyCryptNonce *}
   654 
   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"
   660 apply (erule rev_mp)
   661 apply (erule rev_mp)
   662 apply (erule set_cr.induct)
   663 apply (simp_all (no_asm_simp))
   664 apply blast
   665 apply blast
   666 apply (auto simp add: DK_fresh_not_KeyCryptKey)
   667 done
   668 
   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 (rename_tac [2] a evs')
   675 apply (case_tac [2] "a")
   676 apply (auto simp add: parts_insert2)
   677 done
   678 
   679 lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
   680      "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
   681       Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
   682 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   683 apply (blast dest: not_KeyCryptKey_cardSK)  --{*6*}
   684 done
   685 
   686 subsubsection{*Lemmas for message 5 and 6:
   687   either cardSK is compromised (when we don't care)
   688   or else cardSK hasn't been used to encrypt K. *}
   689 
   690 text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
   691 lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
   692 apply (induct_tac "evs")
   693 apply (auto simp add: parts_insert2 split add: event.split)
   694 done
   695 
   696 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   697   or else cardSK hasn't been used to encrypt K.*}
   698 lemma msg6_KeyCryptNonce_disj:
   699      "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
   700           \<in> set evs;
   701         cardSK \<notin> symKeys;  evs \<in> set_cr|]
   702       ==> Key cardSK \<in> analz (knows Spy evs) |
   703           ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
   704            (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
   705 by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
   706           intro: cardSK_neq_priEK)
   707 
   708 
   709 text{*As usual: we express the property as a logical equivalence*}
   710 lemma Nonce_analz_image_Key_lemma:
   711      "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
   712       ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
   713 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   714 
   715 
   716 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   717   the quantifier and allows the simprule's condition to itself be simplified.*}
   718 lemma Nonce_compromise [rule_format (no_asm)]:
   719      "evs \<in> set_cr ==>
   720       (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs)   -->
   721                (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
   722                (Nonce N \<in> analz (knows Spy evs)))"
   723 apply (erule set_cr.induct)
   724 apply (rule_tac [!] allI)+
   725 apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
   726 apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
   727 apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
   728 apply (frule_tac [11] msg6_KeyCryptNonce_disj)
   729 apply (erule_tac [13] disjE)
   730 apply (simp_all del: image_insert image_Un
   731          add: symKey_compromise
   732               analz_image_keys_simps analz_knows_absorb
   733               analz_Key_image_insert_eq notin_image_iff
   734               N_fresh_not_KeyCryptNonce
   735               DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
   736               ball_conj_distrib analz_image_priEK)
   737   --{*14 seconds on a 1.6GHz machine*}
   738 apply spy_analz  --{*Fake*}
   739 apply blast  --{*3*}
   740 apply blast  --{*5*}
   741 txt{*Message 6*}
   742 apply (metis symKey_compromise)
   743   --{*cardSK compromised*}
   744 txt{*Simplify again--necessary because the previous simplification introduces
   745   some logical connectives*} 
   746 apply (force simp del: image_insert image_Un imp_disjL
   747           simp add: analz_image_keys_simps symKey_compromise)
   748 done
   749 
   750 
   751 subsection{*Secrecy of CardSecret: the Cardholder's secret*}
   752 
   753 lemma NC2_not_CardSecret:
   754      "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
   755           \<in> parts (knows Spy evs);
   756         Key K \<notin> analz (knows Spy evs);
   757         Nonce N \<notin> analz (knows Spy evs);
   758        evs \<in> set_cr|]
   759       ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
   760 apply (erule rev_mp)
   761 apply (erule rev_mp)
   762 apply (erule rev_mp)
   763 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   764 apply (blast dest: Hash_imp_parts)+
   765 done
   766 
   767 lemma KC2_secure_lemma [rule_format]:
   768      "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
   769         U \<in> parts (knows Spy evs);
   770         evs \<in> set_cr|]
   771   ==> Nonce N \<notin> analz (knows Spy evs) -->
   772       (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
   773                Cardholder k \<notin> bad & CA i \<notin> bad)"
   774 apply (erule_tac P = "U \<in> H" for H in rev_mp)
   775 apply (erule set_cr.induct)
   776 apply (valid_certificate_tac [8])  --{*for message 5*}
   777 apply (simp_all del: image_insert image_Un imp_disjL
   778          add: analz_image_keys_simps analz_knows_absorb
   779               analz_knows_absorb2 notin_image_iff)
   780   --{*4 seconds on a 1.6GHz machine*}
   781 apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
   782 apply (blast intro!: analz_insertI)+
   783 done
   784 
   785 lemma KC2_secrecy:
   786      "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
   787         Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
   788         evs \<in> set_cr|]
   789        ==> Key KC2 \<notin> analz (knows Spy evs)"
   790 by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
   791 
   792 
   793 text{*Inductive version*}
   794 lemma CardSecret_secrecy_lemma [rule_format]:
   795      "[|CA i \<notin> bad;  evs \<in> set_cr|]
   796       ==> Key K \<notin> analz (knows Spy evs) -->
   797           Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
   798              \<in> parts (knows Spy evs) -->
   799           Nonce CardSecret \<notin> analz (knows Spy evs)"
   800 apply (erule set_cr.induct, analz_mono_contra)
   801 apply (valid_certificate_tac [8]) --{*for message 5*}
   802 apply (valid_certificate_tac [6]) --{*for message 5*}
   803 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   804 apply (simp_all
   805          del: image_insert image_Un imp_disjL
   806          add: analz_image_keys_simps analz_knows_absorb
   807               analz_Key_image_insert_eq notin_image_iff
   808               EXHcrypt_def Crypt_notin_image_Key
   809               N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   810               ball_conj_distrib Nonce_compromise symKey_compromise
   811               analz_image_priEK)
   812   --{*2.5 seconds on a 1.6GHz machine*}
   813 apply spy_analz  --{*Fake*}
   814 apply (simp_all (no_asm_simp))
   815 apply blast  --{*1*}
   816 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
   817 apply blast  --{*3*}
   818 apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)  --{*4*}
   819 apply blast  --{*5*}
   820 apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
   821 done
   822 
   823 
   824 text{*Packaged version for cardholder*}
   825 lemma CardSecret_secrecy:
   826      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   827         Says (Cardholder k) (CA i)
   828            {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
   829         Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   830                     cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   831         KC3 \<in> symKeys;  evs \<in> set_cr|]
   832       ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
   833 apply (frule Gets_certificate_valid, assumption)
   834 apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
   835 apply (blast dest: CardSecret_secrecy_lemma)
   836 apply (rule symKey_secrecy)
   837 apply (auto simp add: parts_insert2)
   838 done
   839 
   840 
   841 subsection{*Secrecy of NonceCCA [the CA's secret] *}
   842 
   843 lemma NC2_not_NonceCCA:
   844      "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
   845           \<in> parts (knows Spy evs);
   846         Nonce N \<notin> analz (knows Spy evs);
   847        evs \<in> set_cr|]
   848       ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
   849 apply (erule rev_mp)
   850 apply (erule rev_mp)
   851 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   852 apply (blast dest: Hash_imp_parts2)+
   853 done
   854 
   855 
   856 text{*Inductive version*}
   857 lemma NonceCCA_secrecy_lemma [rule_format]:
   858      "[|CA i \<notin> bad;  evs \<in> set_cr|]
   859       ==> Key K \<notin> analz (knows Spy evs) -->
   860           Crypt K
   861             {|sign (priSK (CA i))
   862                    {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   863               X, Y|}
   864              \<in> parts (knows Spy evs) -->
   865           Nonce NonceCCA \<notin> analz (knows Spy evs)"
   866 apply (erule set_cr.induct, analz_mono_contra)
   867 apply (valid_certificate_tac [8]) --{*for message 5*}
   868 apply (valid_certificate_tac [6]) --{*for message 5*}
   869 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   870 apply (simp_all
   871          del: image_insert image_Un imp_disjL
   872          add: analz_image_keys_simps analz_knows_absorb sign_def
   873               analz_Key_image_insert_eq notin_image_iff
   874               EXHcrypt_def Crypt_notin_image_Key
   875               N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   876               ball_conj_distrib Nonce_compromise symKey_compromise
   877               analz_image_priEK)
   878   --{*3 seconds on a 1.6GHz machine*}
   879 apply spy_analz  --{*Fake*}
   880 apply blast  --{*1*}
   881 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
   882 apply blast  --{*3*}
   883 apply (blast dest: NC2_not_NonceCCA)  --{*4*}
   884 apply blast  --{*5*}
   885 apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
   886 done
   887 
   888 
   889 text{*Packaged version for cardholder*}
   890 lemma NonceCCA_secrecy:
   891      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   892         Gets (Cardholder k)
   893            (Crypt KC2
   894             {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   895               X, Y|}) \<in> set evs;
   896         Says (Cardholder k) (CA i)
   897            {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
   898         Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   899                     cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   900         KC2 \<in> symKeys;  evs \<in> set_cr|]
   901       ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
   902 apply (frule Gets_certificate_valid, assumption)
   903 apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
   904 apply (blast dest: NonceCCA_secrecy_lemma)
   905 apply (rule symKey_secrecy)
   906 apply (auto simp add: parts_insert2)
   907 done
   908 
   909 text{*We don't bother to prove guarantees for the CA.  He doesn't care about
   910   the PANSecret: it isn't his credit card!*}
   911 
   912 
   913 subsection{*Rewriting Rule for PANs*}
   914 
   915 text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
   916   or if it is then (because it appears in traffic) that CA is bad,
   917   and so the Spy knows that key already.  Either way, we can simplify
   918   the expression @{term "analz (insert (Key cardSK) X)"}.*}
   919 lemma msg6_cardSK_disj:
   920      "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
   921           \<in> set evs;  evs \<in> set_cr |]
   922       ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
   923 by auto
   924 
   925 lemma analz_image_pan_lemma:
   926      "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
   927       (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
   928 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   929 
   930 lemma analz_image_pan [rule_format]:
   931      "evs \<in> set_cr ==>
   932        \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
   933             (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
   934             (Pan P \<in> analz (knows Spy evs))"
   935 apply (erule set_cr.induct)
   936 apply (rule_tac [!] allI impI)+
   937 apply (rule_tac [!] analz_image_pan_lemma)
   938 apply (valid_certificate_tac [8]) --{*for message 5*}
   939 apply (valid_certificate_tac [6]) --{*for message 5*}
   940 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
   941 apply (simp_all
   942          del: image_insert image_Un
   943          add: analz_image_keys_simps disjoint_image_iff
   944               notin_image_iff analz_image_priEK)
   945   --{*6 seconds on a 1.6GHz machine*}
   946 apply spy_analz
   947 apply (simp add: insert_absorb)  --{*6*}
   948 done
   949 
   950 lemma analz_insert_pan:
   951      "[| evs \<in> set_cr;  K \<notin> invKey ` pubEK ` range CA |] ==>
   952           (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
   953           (Pan P \<in> analz (knows Spy evs))"
   954 by (simp del: image_insert image_Un
   955          add: analz_image_keys_simps analz_image_pan)
   956 
   957 
   958 text{*Confidentiality of the PAN\@.  Maybe we could combine the statements of
   959   this theorem with @{term analz_image_pan}, requiring a single induction but
   960   a much more difficult proof.*}
   961 lemma pan_confidentiality:
   962      "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
   963     ==> \<exists>i X K HN.
   964         Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
   965            \<in> set evs
   966       & (CA i) \<in> bad"
   967 apply (erule rev_mp)
   968 apply (erule set_cr.induct)
   969 apply (valid_certificate_tac [8]) --{*for message 5*}
   970 apply (valid_certificate_tac [6]) --{*for message 5*}
   971 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
   972 apply (simp_all
   973          del: image_insert image_Un
   974          add: analz_image_keys_simps analz_insert_pan analz_image_pan
   975               notin_image_iff analz_image_priEK)
   976   --{*3.5 seconds on a 1.6GHz machine*}
   977 apply spy_analz  --{*fake*}
   978 apply blast  --{*3*}
   979 apply blast  --{*5*}
   980 apply (simp (no_asm_simp) add: insert_absorb)  --{*6*}
   981 done
   982 
   983 
   984 subsection{*Unicity*}
   985 
   986 lemma CR6_Says_imp_Notes:
   987      "[|Says (CA i) C (Crypt KC2
   988           {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
   989             certC (pan C) cardSK X onlySig (priSK (CA i)),
   990             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
   991         evs \<in> set_cr |]
   992       ==> Notes (CA i) (Key cardSK) \<in> set evs"
   993 apply (erule rev_mp)
   994 apply (erule set_cr.induct)
   995 apply (simp_all (no_asm_simp))
   996 done
   997 
   998 text{*Unicity of cardSK: it uniquely identifies the other components.  
   999       This holds because a CA accepts a cardSK at most once.*}
  1000 lemma cardholder_key_unicity:
  1001      "[|Says (CA i) C (Crypt KC2
  1002           {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
  1003             certC (pan C) cardSK X onlySig (priSK (CA i)),
  1004             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  1005           \<in> set evs;
  1006         Says (CA i) C' (Crypt KC2'
  1007           {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
  1008             certC (pan C') cardSK X' onlySig (priSK (CA i)),
  1009             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  1010           \<in> set evs;
  1011         evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
  1012 apply (erule rev_mp)
  1013 apply (erule rev_mp)
  1014 apply (erule set_cr.induct)
  1015 apply (simp_all (no_asm_simp))
  1016 apply (blast dest!: CR6_Says_imp_Notes)
  1017 done
  1018 
  1019 
  1020 (*<*)
  1021 text{*UNUSED unicity result*}
  1022 lemma unique_KC1:
  1023      "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
  1024           \<in> set evs;
  1025         Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
  1026           \<in> set evs;
  1027         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
  1028 apply (erule rev_mp)
  1029 apply (erule rev_mp)
  1030 apply (erule set_cr.induct, auto)
  1031 done
  1032 
  1033 text{*UNUSED unicity result*}
  1034 lemma unique_KC2:
  1035      "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
  1036         Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
  1037         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
  1038 apply (erule rev_mp)
  1039 apply (erule rev_mp)
  1040 apply (erule set_cr.induct, auto)
  1041 done
  1042 (*>*)
  1043 
  1044 
  1045 text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
  1046   it could be a previously compromised cardSK [e.g. involving a bad CA]*}
  1047 
  1048 
  1049 end