src/HOL/SET-Protocol/Cardholder_Registration.thy
author wenzelm
Fri Mar 20 15:24:18 2009 +0100 (2009-03-20)
changeset 30607 c3d1590debd8
parent 30549 d2d7874648bd
child 32404 da3ca3c6ec81
permissions -rw-r--r--
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
     1 (*  Title:      HOL/Auth/SET/Cardholder_Registration
     2     Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson,
     3                 Piero Tramontano
     4 *)
     5 
     6 header{*The SET Cardholder Registration Protocol*}
     7 
     8 theory Cardholder_Registration imports PublicSET begin
     9 
    10 text{*Note: nonces seem to consist of 20 bytes.  That includes both freshness
    11 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
    12 *}
    13 
    14 text{*Simplifications involving @{text analz_image_keys_simps} appear to
    15 have become much slower. The cause is unclear. However, there is a big blow-up
    16 and the rewriting is very sensitive to the set of rewrite rules given.*}
    17 
    18 subsection{*Predicate Formalizing the Encryption Association between Keys *}
    19 
    20 consts
    21   KeyCryptKey :: "[key, key, event list] => bool"
    22 
    23 primrec
    24 
    25 KeyCryptKey_Nil:
    26   "KeyCryptKey DK K [] = False"
    27 
    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 consts
    50   KeyCryptNonce :: "[key, key, event list] => bool"
    51 
    52 primrec
    53 
    54 KeyCryptNonce_Nil:
    55   "KeyCryptNonce EK K [] = False"
    56 
    57 KeyCryptNonce_Cons:
    58   --{*Says is the only important case.
    59     1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH);
    60     2nd case: CR5, where KC3 encrypts NC3;
    61     3rd case: CR6, where KC2 encrypts NC3;
    62     4th case: CR6, where KC2 encrypts NonceCCA;
    63     5th case: any use of @{term "priEK C"} (including CardSecret).
    64     NB the only Nonces we need to keep secret are CardSecret and NonceCCA.
    65     But we can't prove @{text Nonce_compromise} unless the relation covers ALL
    66 	nonces that the protocol keeps secret.
    67   *}
    68   "KeyCryptNonce DK N (ev # evs) =
    69    (KeyCryptNonce DK N evs |
    70     (case ev of
    71       Says A B Z =>
    72        A \<noteq> Spy &
    73        ((\<exists>X Y. DK \<in> symKeys &
    74 	       Z = (EXHcrypt DK X {|Agent A, Nonce N|} Y)) |
    75 	(\<exists>X Y. DK \<in> symKeys &
    76 	       Z = {|Crypt DK {|Agent A, Nonce N, X|}, Y|}) |
    77 	(\<exists>K i X Y.
    78 	  K \<in> symKeys &
    79           Z = Crypt K {|sign (priSK (CA i)) {|Agent B, Nonce N, X|}, Y|} &
    80 	  (DK=K | KeyCryptKey DK K evs)) |
    81 	(\<exists>K C NC3 Y.
    82 	  K \<in> symKeys &
    83           Z = Crypt K
    84  	        {|sign (priSK C) {|Agent B, Nonce NC3, Agent C, Nonce N|},
    85                   Y|} &
    86 	  (DK=K | KeyCryptKey DK K evs)) |
    87 	(\<exists>C. DK = priEK C))
    88     | Gets A' X => False
    89     | Notes A' X => False))"
    90 
    91 
    92 subsection{*Formal protocol definition *}
    93 
    94 inductive_set
    95   set_cr :: "event list set"
    96 where
    97 
    98   Nil:    --{*Initial trace is empty*}
    99 	  "[] \<in> set_cr"
   100 
   101 | Fake:    --{*The spy MAY say anything he CAN say.*}
   102 	   "[| evsf \<in> set_cr; X \<in> synth (analz (knows Spy evsf)) |]
   103 	    ==> Says Spy B X  # evsf \<in> set_cr"
   104 
   105 | Reception: --{*If A sends a message X to B, then B might receive it*}
   106 	     "[| evsr \<in> set_cr; Says A B X \<in> set evsr |]
   107               ==> Gets B X  # evsr \<in> set_cr"
   108 
   109 | SET_CR1: --{*CardCInitReq: C initiates a run, sending a nonce to CCA*}
   110 	     "[| evs1 \<in> set_cr;  C = Cardholder k;  Nonce NC1 \<notin> used evs1 |]
   111 	      ==> Says C (CA i) {|Agent C, Nonce NC1|} # evs1 \<in> set_cr"
   112 
   113 | SET_CR2: --{*CardCInitRes: CA responds sending NC1 and its certificates*}
   114 	     "[| evs2 \<in> set_cr;
   115 		 Gets (CA i) {|Agent C, Nonce NC1|} \<in> set evs2 |]
   116 	      ==> Says (CA i) C
   117 		       {|sign (priSK (CA i)) {|Agent C, Nonce NC1|},
   118 			 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
   119 			 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   120 		    # evs2 \<in> set_cr"
   121 
   122 | SET_CR3:
   123    --{*RegFormReq: C sends his PAN and a new nonce to CA.
   124    C verifies that
   125     - nonce received is the same as that sent;
   126     - certificates are signed by RCA;
   127     - certificates are an encryption certificate (flag is onlyEnc) and a
   128       signature certificate (flag is onlySig);
   129     - certificates pertain to the CA that C contacted (this is done by
   130       checking the signature).
   131    C generates a fresh symmetric key KC1.
   132    The point of encrypting @{term "{|Agent C, Nonce NC2, Hash (Pan(pan C))|}"}
   133    is not clear. *}
   134 "[| evs3 \<in> set_cr;  C = Cardholder k;
   135     Nonce NC2 \<notin> used evs3;
   136     Key KC1 \<notin> used evs3; KC1 \<in> symKeys;
   137     Gets C {|sign (invKey SKi) {|Agent X, Nonce NC1|},
   138 	     cert (CA i) EKi onlyEnc (priSK RCA),
   139 	     cert (CA i) SKi onlySig (priSK RCA)|}
   140        \<in> set evs3;
   141     Says C (CA i) {|Agent C, Nonce NC1|} \<in> set evs3|]
   142  ==> Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
   143        # Notes C {|Key KC1, Agent (CA i)|}
   144        # evs3 \<in> set_cr"
   145 
   146 | SET_CR4:
   147     --{*RegFormRes:
   148     CA responds sending NC2 back with a new nonce NCA, after checking that
   149      - the digital envelope is correctly encrypted by @{term "pubEK (CA i)"}
   150      - the entire message is encrypted with the same key found inside the
   151        envelope (here, KC1) *}
   152 "[| evs4 \<in> set_cr;
   153     Nonce NCA \<notin> used evs4;  KC1 \<in> symKeys;
   154     Gets (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan X)))
   155        \<in> set evs4 |]
   156   ==> Says (CA i) C
   157 	  {|sign (priSK (CA i)) {|Agent C, Nonce NC2, Nonce NCA|},
   158 	    cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA),
   159 	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|}
   160        # evs4 \<in> set_cr"
   161 
   162 | SET_CR5:
   163    --{*CertReq: C sends his PAN, a new nonce, its proposed public signature key
   164        and its half of the secret value to CA.
   165        We now assume that C has a fixed key pair, and he submits (pubSK C).
   166        The protocol does not require this key to be fresh.
   167        The encryption below is actually EncX.*}
   168 "[| evs5 \<in> set_cr;  C = Cardholder k;
   169     Nonce NC3 \<notin> used evs5;  Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret;
   170     Key KC2 \<notin> used evs5; KC2 \<in> symKeys;
   171     Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3;
   172     Gets C {|sign (invKey SKi) {|Agent C, Nonce NC2, Nonce NCA|},
   173              cert (CA i) EKi onlyEnc (priSK RCA),
   174              cert (CA i) SKi onlySig (priSK RCA) |}
   175         \<in> set evs5;
   176     Says C (CA i) (EXHcrypt KC1 EKi {|Agent C, Nonce NC2|} (Pan(pan C)))
   177          \<in> set evs5 |]
   178 ==> Says C (CA i)
   179          {|Crypt KC3
   180 	     {|Agent C, Nonce NC3, Key KC2, Key (pubSK C),
   181 	       Crypt (priSK C)
   182 	         (Hash {|Agent C, Nonce NC3, Key KC2,
   183 			 Key (pubSK C), Pan (pan C), Nonce CardSecret|})|},
   184            Crypt EKi {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
   185     # Notes C {|Key KC2, Agent (CA i)|}
   186     # Notes C {|Key KC3, Agent (CA i)|}
   187     # evs5 \<in> set_cr"
   188 
   189 
   190   --{* CertRes: CA responds sending NC3 back with its half of the secret value,
   191    its signature certificate and the new cardholder signature
   192    certificate.  CA checks to have never certified the key proposed by C.
   193    NOTE: In Merchant Registration, the corresponding rule (4)
   194    uses the "sign" primitive. The encryption below is actually @{term EncK}, 
   195    which is just @{term "Crypt K (sign SK X)"}.
   196 *}
   197 
   198 | SET_CR6:
   199 "[| evs6 \<in> set_cr;
   200     Nonce NonceCCA \<notin> used evs6;
   201     KC2 \<in> symKeys;  KC3 \<in> symKeys;  cardSK \<notin> symKeys;
   202     Notes (CA i) (Key cardSK) \<notin> set evs6;
   203     Gets (CA i)
   204       {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, Key cardSK,
   205                     Crypt (invKey cardSK)
   206                       (Hash {|Agent C, Nonce NC3, Key KC2,
   207 			      Key cardSK, Pan (pan C), Nonce CardSecret|})|},
   208         Crypt (pubEK (CA i)) {|Key KC3, Pan (pan C), Nonce CardSecret|} |}
   209       \<in> set evs6 |]
   210 ==> Says (CA i) C
   211          (Crypt KC2
   212 	  {|sign (priSK (CA i))
   213 	         {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
   214 	    certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)),
   215 	    cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
   216       # Notes (CA i) (Key cardSK)
   217       # evs6 \<in> set_cr"
   218 
   219 
   220 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   221 declare parts.Body [dest]
   222 declare analz_into_parts [dest]
   223 declare Fake_parts_insert_in_Un [dest]
   224 
   225 text{*A "possibility property": there are traces that reach the end.
   226       An unconstrained proof with many subgoals.*}
   227 
   228 lemma Says_to_Gets:
   229      "Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr"
   230 by (rule set_cr.Reception, auto)
   231 
   232 text{*The many nonces and keys generated, some simultaneously, force us to
   233   introduce them explicitly as shown below.*}
   234 lemma possibility_CR6:
   235      "[|NC1 < (NC2::nat);  NC2 < NC3;  NC3 < NCA ;
   236         NCA < NonceCCA;  NonceCCA < CardSecret;
   237         KC1 < (KC2::key);  KC2 < KC3;
   238         KC1 \<in> symKeys;  Key KC1 \<notin> used [];
   239         KC2 \<in> symKeys;  Key KC2 \<notin> used [];
   240         KC3 \<in> symKeys;  Key KC3 \<notin> used [];
   241         C = Cardholder k|]
   242    ==> \<exists>evs \<in> set_cr.
   243        Says (CA i) C
   244             (Crypt KC2
   245              {|sign (priSK (CA i))
   246                     {|Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA|},
   247                certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA))
   248                      onlySig (priSK (CA i)),
   249                cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
   250           \<in> set evs"
   251 apply (intro exI bexI)
   252 apply (rule_tac [2] 
   253        set_cr.Nil 
   254         [THEN set_cr.SET_CR1 [of concl: C i NC1], 
   255          THEN Says_to_Gets, 
   256 	 THEN set_cr.SET_CR2 [of concl: i C NC1], 
   257 	 THEN Says_to_Gets,  
   258 	 THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2], 
   259 	 THEN Says_to_Gets,  
   260 	 THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], 
   261 	 THEN Says_to_Gets,  
   262 	 THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret],
   263 	 THEN Says_to_Gets,  
   264 	 THEN set_cr.SET_CR6 [of concl: i C KC2]])
   265 apply basic_possibility
   266 apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq)
   267 done
   268 
   269 text{*General facts about message reception*}
   270 lemma Gets_imp_Says:
   271      "[| Gets B X \<in> set evs; evs \<in> set_cr |] ==> \<exists>A. Says A B X \<in> set evs"
   272 apply (erule rev_mp)
   273 apply (erule set_cr.induct, auto)
   274 done
   275 
   276 lemma Gets_imp_knows_Spy:
   277      "[| Gets B X \<in> set evs; evs \<in> set_cr |]  ==> X \<in> knows Spy evs"
   278 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   279 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   280 
   281 
   282 subsection{*Proofs on keys *}
   283 
   284 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   285 
   286 lemma Spy_see_private_Key [simp]:
   287      "evs \<in> set_cr
   288       ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   289 by (erule set_cr.induct, auto)
   290 
   291 lemma Spy_analz_private_Key [simp]:
   292      "evs \<in> set_cr ==>
   293      (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   294 by auto
   295 
   296 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   297 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   298 
   299 
   300 subsection{*Begin Piero's Theorems on Certificates*}
   301 text{*Trivial in the current model, where certificates by RCA are secure *}
   302 
   303 lemma Crypt_valid_pubEK:
   304      "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
   305            \<in> parts (knows Spy evs);
   306          evs \<in> set_cr |] ==> EKi = pubEK C"
   307 apply (erule rev_mp)
   308 apply (erule set_cr.induct, auto)
   309 done
   310 
   311 lemma certificate_valid_pubEK:
   312     "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   313         evs \<in> set_cr |]
   314      ==> EKi = pubEK C"
   315 apply (unfold cert_def signCert_def)
   316 apply (blast dest!: Crypt_valid_pubEK)
   317 done
   318 
   319 lemma Crypt_valid_pubSK:
   320      "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
   321            \<in> parts (knows Spy evs);
   322          evs \<in> set_cr |] ==> SKi = pubSK C"
   323 apply (erule rev_mp)
   324 apply (erule set_cr.induct, auto)
   325 done
   326 
   327 lemma certificate_valid_pubSK:
   328     "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   329         evs \<in> set_cr |] ==> SKi = pubSK C"
   330 apply (unfold cert_def signCert_def)
   331 apply (blast dest!: Crypt_valid_pubSK)
   332 done
   333 
   334 lemma Gets_certificate_valid:
   335      "[| Gets A {| X, cert C EKi onlyEnc (priSK RCA),
   336                       cert C SKi onlySig (priSK RCA)|} \<in> set evs;
   337          evs \<in> set_cr |]
   338       ==> EKi = pubEK C & SKi = pubSK C"
   339 by (blast dest: certificate_valid_pubEK certificate_valid_pubSK)
   340 
   341 text{*Nobody can have used non-existent keys!*}
   342 lemma new_keys_not_used:
   343      "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr|]
   344       ==> K \<notin> keysFor (parts (knows Spy evs))"
   345 apply (erule rev_mp)
   346 apply (erule rev_mp)
   347 apply (erule set_cr.induct)
   348 apply (frule_tac [8] Gets_certificate_valid)
   349 apply (frule_tac [6] Gets_certificate_valid, simp_all)
   350 apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
   351 apply (blast,auto)  --{*Others*}
   352 done
   353 
   354 
   355 subsection{*New versions: as above, but generalized to have the KK argument *}
   356 
   357 lemma gen_new_keys_not_used:
   358      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
   359       ==> Key K \<notin> used evs --> K \<in> symKeys -->
   360           K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   361 by (auto simp add: new_keys_not_used)
   362 
   363 lemma gen_new_keys_not_analzd:
   364      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr |]
   365       ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   366 by (blast intro: keysFor_mono [THEN [2] rev_subsetD]
   367           dest: gen_new_keys_not_used)
   368 
   369 lemma analz_Key_image_insert_eq:
   370      "[|K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr |]
   371       ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   372           insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   373 by (simp add: gen_new_keys_not_analzd)
   374 
   375 lemma Crypt_parts_imp_used:
   376      "[|Crypt K X \<in> parts (knows Spy evs);
   377         K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
   378 apply (rule ccontr)
   379 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   380 done
   381 
   382 lemma Crypt_analz_imp_used:
   383      "[|Crypt K X \<in> analz (knows Spy evs);
   384         K \<in> symKeys; evs \<in> set_cr |] ==> Key K \<in> used evs"
   385 by (blast intro: Crypt_parts_imp_used)
   386 
   387 
   388 (*<*) 
   389 subsection{*Messages signed by CA*}
   390 
   391 text{*Message @{text SET_CR2}: C can check CA's signature if he has received
   392      CA's certificate.*}
   393 lemma CA_Says_2_lemma:
   394      "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC1|})
   395            \<in> parts (knows Spy evs);
   396          evs \<in> set_cr; (CA i) \<notin> bad |]
   397      ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
   398                  \<in> set evs"
   399 apply (erule rev_mp)
   400 apply (erule set_cr.induct, auto)
   401 done
   402 
   403 text{*Ever used?*}
   404 lemma CA_Says_2:
   405      "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC1|})
   406            \<in> parts (knows Spy evs);
   407          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   408          evs \<in> set_cr; (CA i) \<notin> bad |]
   409       ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i)) {|Agent C, Nonce NC1|}, Y|}
   410                   \<in> set evs"
   411 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma)
   412 
   413 
   414 text{*Message @{text SET_CR4}: C can check CA's signature if he has received
   415       CA's certificate.*}
   416 lemma CA_Says_4_lemma:
   417      "[| Crypt (priSK (CA i)) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
   418            \<in> parts (knows Spy evs);
   419          evs \<in> set_cr; (CA i) \<notin> bad |]
   420       ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
   421                      {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
   422 apply (erule rev_mp)
   423 apply (erule set_cr.induct, auto)
   424 done
   425 
   426 text{*NEVER USED*}
   427 lemma CA_Says_4:
   428      "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC2, Nonce NCA|})
   429            \<in> parts (knows Spy evs);
   430          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   431          evs \<in> set_cr; (CA i) \<notin> bad |]
   432       ==> \<exists>Y. Says (CA i) C {|sign (priSK (CA i))
   433                    {|Agent C, Nonce NC2, Nonce NCA|}, Y|} \<in> set evs"
   434 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma)
   435 
   436 
   437 text{*Message @{text SET_CR6}: C can check CA's signature if he has
   438       received CA's certificate.*}
   439 lemma CA_Says_6_lemma:
   440      "[| Crypt (priSK (CA i)) 
   441                (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
   442            \<in> parts (knows Spy evs);
   443          evs \<in> set_cr; (CA i) \<notin> bad |]
   444       ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
   445       {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
   446 apply (erule rev_mp)
   447 apply (erule set_cr.induct, auto)
   448 done
   449 
   450 text{*NEVER USED*}
   451 lemma CA_Says_6:
   452      "[| Crypt (invKey SK) (Hash{|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|})
   453            \<in> parts (knows Spy evs);
   454          cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs);
   455          evs \<in> set_cr; (CA i) \<notin> bad |]
   456       ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
   457                     {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
   458 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
   459 (*>*)
   460 
   461 
   462 subsection{*Useful lemmas *}
   463 
   464 text{*Rewriting rule for private encryption keys.  Analogous rewriting rules
   465 for other keys aren't needed.*}
   466 
   467 lemma parts_image_priEK:
   468      "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
   469         evs \<in> set_cr|] ==> priEK C \<in> KK | C \<in> bad"
   470 by auto
   471 
   472 text{*trivial proof because (priEK C) never appears even in (parts evs)*}
   473 lemma analz_image_priEK:
   474      "evs \<in> set_cr ==>
   475           (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
   476           (priEK C \<in> KK | C \<in> bad)"
   477 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   478 
   479 
   480 subsection{*Secrecy of Session Keys *}
   481 
   482 subsubsection{*Lemmas about the predicate KeyCryptKey *}
   483 
   484 text{*A fresh DK cannot be associated with any other
   485   (with respect to a given trace). *}
   486 lemma DK_fresh_not_KeyCryptKey:
   487      "[| Key DK \<notin> used evs; evs \<in> set_cr |] ==> ~ KeyCryptKey DK K evs"
   488 apply (erule rev_mp)
   489 apply (erule set_cr.induct)
   490 apply (simp_all (no_asm_simp))
   491 apply (blast dest: Crypt_analz_imp_used)+
   492 done
   493 
   494 text{*A fresh K cannot be associated with any other.  The assumption that
   495   DK isn't a private encryption key may be an artifact of the particular
   496   definition of KeyCryptKey.*}
   497 lemma K_fresh_not_KeyCryptKey:
   498      "[|\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs|] ==> ~ KeyCryptKey DK K evs"
   499 apply (induct evs)
   500 apply (auto simp add: parts_insert2 split add: event.split)
   501 done
   502 
   503 
   504 text{*This holds because if (priEK (CA i)) appears in any traffic then it must
   505   be known to the Spy, by @{term Spy_see_private_Key}*}
   506 lemma cardSK_neq_priEK:
   507      "[|Key cardSK \<notin> analz (knows Spy evs);
   508         Key cardSK : parts (knows Spy evs);
   509         evs \<in> set_cr|] ==> cardSK \<noteq> priEK C"
   510 by blast
   511 
   512 lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]:
   513      "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
   514       Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptKey cardSK K evs"
   515 by (erule set_cr.induct, analz_mono_contra, auto)
   516 
   517 text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*}
   518 lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs"
   519 apply (induct_tac "evs")
   520 apply (auto simp add: parts_insert2 split add: event.split)
   521 done
   522 
   523 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   524   or else cardSK hasn't been used to encrypt K.  Previously we treated
   525   message 5 in the same way, but the current model assumes that rule
   526   @{text SET_CR5} is executed only by honest agents.*}
   527 lemma msg6_KeyCryptKey_disj:
   528      "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
   529           \<in> set evs;
   530         cardSK \<notin> symKeys;  evs \<in> set_cr|]
   531       ==> Key cardSK \<in> analz (knows Spy evs) |
   532           (\<forall>K. ~ KeyCryptKey cardSK K evs)"
   533 by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK)
   534 
   535 text{*As usual: we express the property as a logical equivalence*}
   536 lemma Key_analz_image_Key_lemma:
   537      "P --> (Key K \<in> analz (Key`KK Un H)) --> (K \<in> KK | Key K \<in> analz H)
   538       ==>
   539       P --> (Key K \<in> analz (Key`KK Un H)) = (K \<in> KK | Key K \<in> analz H)"
   540 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   541 
   542 method_setup valid_certificate_tac = {*
   543   Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant
   544     (fn i =>
   545       EVERY [ftac @{thm Gets_certificate_valid} i,
   546              assume_tac i,
   547              etac conjE i, REPEAT (hyp_subst_tac i)])))
   548 *} ""
   549 
   550 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   551   the quantifier and allows the simprule's condition to itself be simplified.*}
   552 lemma symKey_compromise [rule_format (no_asm)]:
   553      "evs \<in> set_cr ==>
   554       (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs)   -->
   555                (Key SK \<in> analz (Key`KK Un (knows Spy evs))) =
   556                (SK \<in> KK | Key SK \<in> analz (knows Spy evs)))"
   557 apply (erule set_cr.induct)
   558 apply (rule_tac [!] allI) +
   559 apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
   560 apply (valid_certificate_tac [8]) --{*for message 5*}
   561 apply (valid_certificate_tac [6]) --{*for message 5*}
   562 apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE])
   563 apply (simp_all
   564          del: image_insert image_Un imp_disjL
   565          add: analz_image_keys_simps analz_knows_absorb
   566               analz_Key_image_insert_eq notin_image_iff
   567               K_fresh_not_KeyCryptKey
   568               DK_fresh_not_KeyCryptKey ball_conj_distrib
   569               analz_image_priEK disj_simps)
   570   --{*9 seconds on a 1.6GHz machine*}
   571 apply spy_analz
   572 apply blast  --{*3*}
   573 apply blast  --{*5*}
   574 done
   575 
   576 text{*The remaining quantifiers seem to be essential.
   577   NO NEED to assume the cardholder's OK: bad cardholders don't do anything
   578   wrong!!*}
   579 lemma symKey_secrecy [rule_format]:
   580      "[|CA i \<notin> bad;  K \<in> symKeys;  evs \<in> set_cr|]
   581       ==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs -->
   582                 Key K \<in> parts{X} -->
   583                 Cardholder c \<notin> bad -->
   584                 Key K \<notin> analz (knows Spy evs)"
   585 apply (erule set_cr.induct)
   586 apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
   587 apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
   588 apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE])
   589 apply (simp_all del: image_insert image_Un imp_disjL
   590          add: symKey_compromise fresh_notin_analz_knows_Spy
   591               analz_image_keys_simps analz_knows_absorb
   592               analz_Key_image_insert_eq notin_image_iff
   593               K_fresh_not_KeyCryptKey
   594               DK_fresh_not_KeyCryptKey
   595               analz_image_priEK)
   596   --{*2.5 seconds on a 1.6GHz machine*}
   597 apply spy_analz  --{*Fake*}
   598 apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
   599 done
   600 
   601 
   602 subsection{*Primary Goals of Cardholder Registration *}
   603 
   604 text{*The cardholder's certificate really was created by the CA, provided the
   605     CA is uncompromised *}
   606 
   607 text{*Lemma concerning the actual signed message digest*}
   608 lemma cert_valid_lemma:
   609      "[|Crypt (priSK (CA i)) {|Hash {|Nonce N, Pan(pan C)|}, Key cardSK, N1|}
   610           \<in> parts (knows Spy evs);
   611         CA i \<notin> bad; evs \<in> set_cr|]
   612   ==> \<exists>KC2 X Y. Says (CA i) C
   613                      (Crypt KC2 
   614                        {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   615                   \<in> set evs"
   616 apply (erule rev_mp)
   617 apply (erule set_cr.induct)
   618 apply (simp_all (no_asm_simp))
   619 apply auto
   620 done
   621 
   622 text{*Pre-packaged version for cardholder.  We don't try to confirm the values
   623   of KC2, X and Y, since they are not important.*}
   624 lemma certificate_valid_cardSK:
   625     "[|Gets C (Crypt KC2 {|X, certC (pan C) cardSK N onlySig (invKey SKi),
   626                               cert (CA i) SKi onlySig (priSK RCA)|}) \<in> set evs;
   627         CA i \<notin> bad; evs \<in> set_cr|]
   628   ==> \<exists>KC2 X Y. Says (CA i) C
   629                      (Crypt KC2 
   630                        {|X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y|})
   631                    \<in> set evs"
   632 by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body]
   633                     certificate_valid_pubSK cert_valid_lemma)
   634 
   635 
   636 lemma Hash_imp_parts [rule_format]:
   637      "evs \<in> set_cr
   638       ==> Hash{|X, Nonce N|} \<in> parts (knows Spy evs) -->
   639           Nonce N \<in> parts (knows Spy evs)"
   640 apply (erule set_cr.induct, force)
   641 apply (simp_all (no_asm_simp))
   642 apply (blast intro: parts_mono [THEN [2] rev_subsetD])
   643 done
   644 
   645 lemma Hash_imp_parts2 [rule_format]:
   646      "evs \<in> set_cr
   647       ==> Hash{|X, Nonce M, Y, Nonce N|} \<in> parts (knows Spy evs) -->
   648           Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)"
   649 apply (erule set_cr.induct, force)
   650 apply (simp_all (no_asm_simp))
   651 apply (blast intro: parts_mono [THEN [2] rev_subsetD])
   652 done
   653 
   654 
   655 subsection{*Secrecy of Nonces*}
   656 
   657 subsubsection{*Lemmas about the predicate KeyCryptNonce *}
   658 
   659 text{*A fresh DK cannot be associated with any other
   660   (with respect to a given trace). *}
   661 lemma DK_fresh_not_KeyCryptNonce:
   662      "[| DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr |]
   663       ==> ~ KeyCryptNonce DK K evs"
   664 apply (erule rev_mp)
   665 apply (erule rev_mp)
   666 apply (erule set_cr.induct)
   667 apply (simp_all (no_asm_simp))
   668 apply blast
   669 apply blast
   670 apply (auto simp add: DK_fresh_not_KeyCryptKey)
   671 done
   672 
   673 text{*A fresh N cannot be associated with any other
   674       (with respect to a given trace). *}
   675 lemma N_fresh_not_KeyCryptNonce:
   676      "\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs --> ~ KeyCryptNonce DK N evs"
   677 apply (induct_tac "evs")
   678 apply (case_tac [2] "a")
   679 apply (auto simp add: parts_insert2)
   680 done
   681 
   682 lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]:
   683      "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
   684       Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
   685 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   686 apply (blast dest: not_KeyCryptKey_cardSK)  --{*6*}
   687 done
   688 
   689 subsubsection{*Lemmas for message 5 and 6:
   690   either cardSK is compromised (when we don't care)
   691   or else cardSK hasn't been used to encrypt K. *}
   692 
   693 text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*}
   694 lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs"
   695 apply (induct_tac "evs")
   696 apply (auto simp add: parts_insert2 split add: event.split)
   697 done
   698 
   699 text{*Lemma for message 6: either cardSK is compromised (when we don't care)
   700   or else cardSK hasn't been used to encrypt K.*}
   701 lemma msg6_KeyCryptNonce_disj:
   702      "[|Gets B {|Crypt KC3 {|Agent C, Nonce N, Key KC2, Key cardSK, X|}, Y|}
   703           \<in> set evs;
   704         cardSK \<notin> symKeys;  evs \<in> set_cr|]
   705       ==> Key cardSK \<in> analz (knows Spy evs) |
   706           ((\<forall>K. ~ KeyCryptKey cardSK K evs) &
   707            (\<forall>N. ~ KeyCryptNonce cardSK N evs))"
   708 by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK
   709           intro: cardSK_neq_priEK)
   710 
   711 
   712 text{*As usual: we express the property as a logical equivalence*}
   713 lemma Nonce_analz_image_Key_lemma:
   714      "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
   715       ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
   716 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   717 
   718 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   719   the quantifier and allows the simprule's condition to itself be simplified.*}
   720 lemma Nonce_compromise [rule_format (no_asm)]:
   721      "evs \<in> set_cr ==>
   722       (\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs)   -->
   723                (Nonce N \<in> analz (Key`KK Un (knows Spy evs))) =
   724                (Nonce N \<in> analz (knows Spy evs)))"
   725 apply (erule set_cr.induct)
   726 apply (rule_tac [!] allI)+
   727 apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
   728 apply (frule_tac [8] Gets_certificate_valid) --{*for message 5*}
   729 apply (frule_tac [6] Gets_certificate_valid) --{*for message 3*}
   730 apply (frule_tac [11] msg6_KeyCryptNonce_disj)
   731 apply (erule_tac [13] disjE)
   732 apply (simp_all del: image_insert image_Un
   733          add: symKey_compromise
   734               analz_image_keys_simps analz_knows_absorb
   735               analz_Key_image_insert_eq notin_image_iff
   736               N_fresh_not_KeyCryptNonce
   737               DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
   738               ball_conj_distrib analz_image_priEK)
   739   --{*14 seconds on a 1.6GHz machine*}
   740 apply spy_analz  --{*Fake*}
   741 apply blast  --{*3*}
   742 apply blast  --{*5*}
   743 txt{*Message 6*}
   744 apply (force del: allE ballE impCE simp add: symKey_compromise)
   745   --{*cardSK compromised*}
   746 txt{*Simplify again--necessary because the previous simplification introduces
   747   some logical connectives*}
   748 apply (force del: allE ballE impCE
   749           simp del: image_insert image_Un imp_disjL
   750           simp add: analz_image_keys_simps symKey_compromise)
   751 done
   752 
   753 
   754 subsection{*Secrecy of CardSecret: the Cardholder's secret*}
   755 
   756 lemma NC2_not_CardSecret:
   757      "[|Crypt EKj {|Key K, Pan p, Hash {|Agent D, Nonce N|}|}
   758           \<in> parts (knows Spy evs);
   759         Key K \<notin> analz (knows Spy evs);
   760         Nonce N \<notin> analz (knows Spy evs);
   761        evs \<in> set_cr|]
   762       ==> Crypt EKi {|Key K', Pan p', Nonce N|} \<notin> parts (knows Spy evs)"
   763 apply (erule rev_mp)
   764 apply (erule rev_mp)
   765 apply (erule rev_mp)
   766 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   767 apply (blast dest: Hash_imp_parts)+
   768 done
   769 
   770 lemma KC2_secure_lemma [rule_format]:
   771      "[|U = Crypt KC3 {|Agent C, Nonce N, Key KC2, X|};
   772         U \<in> parts (knows Spy evs);
   773         evs \<in> set_cr|]
   774   ==> Nonce N \<notin> analz (knows Spy evs) -->
   775       (\<exists>k i W. Says (Cardholder k) (CA i) {|U,W|} \<in> set evs & 
   776                Cardholder k \<notin> bad & CA i \<notin> bad)"
   777 apply (erule_tac P = "U \<in> ?H" in rev_mp)
   778 apply (erule set_cr.induct)
   779 apply (valid_certificate_tac [8])  --{*for message 5*}
   780 apply (simp_all del: image_insert image_Un imp_disjL
   781          add: analz_image_keys_simps analz_knows_absorb
   782               analz_knows_absorb2 notin_image_iff)
   783   --{*4 seconds on a 1.6GHz machine*}
   784 apply (simp_all (no_asm_simp)) --{*leaves 4 subgoals*}
   785 apply (blast intro!: analz_insertI)+
   786 done
   787 
   788 lemma KC2_secrecy:
   789      "[|Gets B {|Crypt K {|Agent C, Nonce N, Key KC2, X|}, Y|} \<in> set evs;
   790         Nonce N \<notin> analz (knows Spy evs);  KC2 \<in> symKeys;
   791         evs \<in> set_cr|]
   792        ==> Key KC2 \<notin> analz (knows Spy evs)"
   793 by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy)
   794 
   795 
   796 text{*Inductive version*}
   797 lemma CardSecret_secrecy_lemma [rule_format]:
   798      "[|CA i \<notin> bad;  evs \<in> set_cr|]
   799       ==> Key K \<notin> analz (knows Spy evs) -->
   800           Crypt (pubEK (CA i)) {|Key K, Pan p, Nonce CardSecret|}
   801              \<in> parts (knows Spy evs) -->
   802           Nonce CardSecret \<notin> analz (knows Spy evs)"
   803 apply (erule set_cr.induct, analz_mono_contra)
   804 apply (valid_certificate_tac [8]) --{*for message 5*}
   805 apply (valid_certificate_tac [6]) --{*for message 5*}
   806 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   807 apply (simp_all
   808          del: image_insert image_Un imp_disjL
   809          add: analz_image_keys_simps analz_knows_absorb
   810               analz_Key_image_insert_eq notin_image_iff
   811               EXHcrypt_def Crypt_notin_image_Key
   812               N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   813               ball_conj_distrib Nonce_compromise symKey_compromise
   814               analz_image_priEK)
   815   --{*2.5 seconds on a 1.6GHz machine*}
   816 apply spy_analz  --{*Fake*}
   817 apply (simp_all (no_asm_simp))
   818 apply blast  --{*1*}
   819 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
   820 apply blast  --{*3*}
   821 apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)  --{*4*}
   822 apply blast  --{*5*}
   823 apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
   824 done
   825 
   826 
   827 text{*Packaged version for cardholder*}
   828 lemma CardSecret_secrecy:
   829      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   830         Says (Cardholder k) (CA i)
   831            {|X, Crypt EKi {|Key KC3, Pan p, Nonce CardSecret|}|} \<in> set evs;
   832         Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   833                     cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   834         KC3 \<in> symKeys;  evs \<in> set_cr|]
   835       ==> Nonce CardSecret \<notin> analz (knows Spy evs)"
   836 apply (frule Gets_certificate_valid, assumption)
   837 apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ")
   838 apply (blast dest: CardSecret_secrecy_lemma)
   839 apply (rule symKey_secrecy)
   840 apply (auto simp add: parts_insert2)
   841 done
   842 
   843 
   844 subsection{*Secrecy of NonceCCA [the CA's secret] *}
   845 
   846 lemma NC2_not_NonceCCA:
   847      "[|Hash {|Agent C', Nonce N', Agent C, Nonce N|}
   848           \<in> parts (knows Spy evs);
   849         Nonce N \<notin> analz (knows Spy evs);
   850        evs \<in> set_cr|]
   851       ==> Crypt KC1 {|{|Agent B, Nonce N|}, Hash p|} \<notin> parts (knows Spy evs)"
   852 apply (erule rev_mp)
   853 apply (erule rev_mp)
   854 apply (erule set_cr.induct, analz_mono_contra, simp_all)
   855 apply (blast dest: Hash_imp_parts2)+
   856 done
   857 
   858 
   859 text{*Inductive version*}
   860 lemma NonceCCA_secrecy_lemma [rule_format]:
   861      "[|CA i \<notin> bad;  evs \<in> set_cr|]
   862       ==> Key K \<notin> analz (knows Spy evs) -->
   863           Crypt K
   864             {|sign (priSK (CA i))
   865                    {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   866               X, Y|}
   867              \<in> parts (knows Spy evs) -->
   868           Nonce NonceCCA \<notin> analz (knows Spy evs)"
   869 apply (erule set_cr.induct, analz_mono_contra)
   870 apply (valid_certificate_tac [8]) --{*for message 5*}
   871 apply (valid_certificate_tac [6]) --{*for message 5*}
   872 apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE])
   873 apply (simp_all
   874          del: image_insert image_Un imp_disjL
   875          add: analz_image_keys_simps analz_knows_absorb sign_def
   876               analz_Key_image_insert_eq notin_image_iff
   877               EXHcrypt_def Crypt_notin_image_Key
   878               N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce
   879               ball_conj_distrib Nonce_compromise symKey_compromise
   880               analz_image_priEK)
   881   --{*3 seconds on a 1.6GHz machine*}
   882 apply spy_analz  --{*Fake*}
   883 apply blast  --{*1*}
   884 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
   885 apply blast  --{*3*}
   886 apply (blast dest: NC2_not_NonceCCA)  --{*4*}
   887 apply blast  --{*5*}
   888 apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
   889 done
   890 
   891 
   892 text{*Packaged version for cardholder*}
   893 lemma NonceCCA_secrecy:
   894      "[|Cardholder k \<notin> bad;  CA i \<notin> bad;
   895         Gets (Cardholder k)
   896            (Crypt KC2
   897             {|sign (priSK (CA i)) {|Agent C, Nonce N, Agent(CA i), Nonce NonceCCA|},
   898               X, Y|}) \<in> set evs;
   899         Says (Cardholder k) (CA i)
   900            {|Crypt KC3 {|Agent C, Nonce NC3, Key KC2, X'|}, Y'|} \<in> set evs;
   901         Gets A {|Z, cert (CA i) EKi onlyEnc (priSK RCA),
   902                     cert (CA i) SKi onlySig (priSK RCA)|} \<in> set evs;
   903         KC2 \<in> symKeys;  evs \<in> set_cr|]
   904       ==> Nonce NonceCCA \<notin> analz (knows Spy evs)"
   905 apply (frule Gets_certificate_valid, assumption)
   906 apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ")
   907 apply (blast dest: NonceCCA_secrecy_lemma)
   908 apply (rule symKey_secrecy)
   909 apply (auto simp add: parts_insert2)
   910 done
   911 
   912 text{*We don't bother to prove guarantees for the CA.  He doesn't care about
   913   the PANSecret: it isn't his credit card!*}
   914 
   915 
   916 subsection{*Rewriting Rule for PANs*}
   917 
   918 text{*Lemma for message 6: either cardSK isn't a CA's private encryption key,
   919   or if it is then (because it appears in traffic) that CA is bad,
   920   and so the Spy knows that key already.  Either way, we can simplify
   921   the expression @{term "analz (insert (Key cardSK) X)"}.*}
   922 lemma msg6_cardSK_disj:
   923      "[|Gets A {|Crypt K {|c, n, k', Key cardSK, X|}, Y|}
   924           \<in> set evs;  evs \<in> set_cr |]
   925       ==> cardSK \<notin> range(invKey o pubEK o CA) | Key cardSK \<in> knows Spy evs"
   926 by auto
   927 
   928 lemma analz_image_pan_lemma:
   929      "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
   930       (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
   931 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   932 
   933 lemma analz_image_pan [rule_format]:
   934      "evs \<in> set_cr ==>
   935        \<forall>KK. KK <= - invKey ` pubEK ` range CA -->
   936             (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
   937             (Pan P \<in> analz (knows Spy evs))"
   938 apply (erule set_cr.induct)
   939 apply (rule_tac [!] allI impI)+
   940 apply (rule_tac [!] analz_image_pan_lemma)
   941 apply (valid_certificate_tac [8]) --{*for message 5*}
   942 apply (valid_certificate_tac [6]) --{*for message 5*}
   943 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
   944 apply (simp_all
   945          del: image_insert image_Un
   946          add: analz_image_keys_simps disjoint_image_iff
   947               notin_image_iff analz_image_priEK)
   948   --{*6 seconds on a 1.6GHz machine*}
   949 apply spy_analz
   950 apply (simp add: insert_absorb)  --{*6*}
   951 done
   952 
   953 lemma analz_insert_pan:
   954      "[| evs \<in> set_cr;  K \<notin> invKey ` pubEK ` range CA |] ==>
   955           (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
   956           (Pan P \<in> analz (knows Spy evs))"
   957 by (simp del: image_insert image_Un
   958          add: analz_image_keys_simps analz_image_pan)
   959 
   960 
   961 text{*Confidentiality of the PAN\@.  Maybe we could combine the statements of
   962   this theorem with @{term analz_image_pan}, requiring a single induction but
   963   a much more difficult proof.*}
   964 lemma pan_confidentiality:
   965      "[| Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr|]
   966     ==> \<exists>i X K HN.
   967         Says C (CA i) {|X, Crypt (pubEK (CA i)) {|Key K, Pan (pan C), HN|} |}
   968            \<in> set evs
   969       & (CA i) \<in> bad"
   970 apply (erule rev_mp)
   971 apply (erule set_cr.induct)
   972 apply (valid_certificate_tac [8]) --{*for message 5*}
   973 apply (valid_certificate_tac [6]) --{*for message 5*}
   974 apply (erule_tac [9] msg6_cardSK_disj [THEN disjE])
   975 apply (simp_all
   976          del: image_insert image_Un
   977          add: analz_image_keys_simps analz_insert_pan analz_image_pan
   978               notin_image_iff analz_image_priEK)
   979   --{*3.5 seconds on a 1.6GHz machine*}
   980 apply spy_analz  --{*fake*}
   981 apply blast  --{*3*}
   982 apply blast  --{*5*}
   983 apply (simp (no_asm_simp) add: insert_absorb)  --{*6*}
   984 done
   985 
   986 
   987 subsection{*Unicity*}
   988 
   989 lemma CR6_Says_imp_Notes:
   990      "[|Says (CA i) C (Crypt KC2
   991           {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
   992             certC (pan C) cardSK X onlySig (priSK (CA i)),
   993             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})  \<in> set evs;
   994         evs \<in> set_cr |]
   995       ==> Notes (CA i) (Key cardSK) \<in> set evs"
   996 apply (erule rev_mp)
   997 apply (erule set_cr.induct)
   998 apply (simp_all (no_asm_simp))
   999 done
  1000 
  1001 text{*Unicity of cardSK: it uniquely identifies the other components.  
  1002       This holds because a CA accepts a cardSK at most once.*}
  1003 lemma cardholder_key_unicity:
  1004      "[|Says (CA i) C (Crypt KC2
  1005           {|sign (priSK (CA i)) {|Agent C, Nonce NC3, Agent (CA i), Nonce Y|},
  1006             certC (pan C) cardSK X onlySig (priSK (CA i)),
  1007             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  1008           \<in> set evs;
  1009         Says (CA i) C' (Crypt KC2'
  1010           {|sign (priSK (CA i)) {|Agent C', Nonce NC3', Agent (CA i), Nonce Y'|},
  1011             certC (pan C') cardSK X' onlySig (priSK (CA i)),
  1012             cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)|})
  1013           \<in> set evs;
  1014         evs \<in> set_cr |] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'"
  1015 apply (erule rev_mp)
  1016 apply (erule rev_mp)
  1017 apply (erule set_cr.induct)
  1018 apply (simp_all (no_asm_simp))
  1019 apply (blast dest!: CR6_Says_imp_Notes)
  1020 done
  1021 
  1022 
  1023 (*<*)
  1024 text{*UNUSED unicity result*}
  1025 lemma unique_KC1:
  1026      "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
  1027           \<in> set evs;
  1028         Says C B' {|Crypt KC1 X', Crypt EK' {|Key KC1, Y'|}|}
  1029           \<in> set evs;
  1030         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & Y'=Y"
  1031 apply (erule rev_mp)
  1032 apply (erule rev_mp)
  1033 apply (erule set_cr.induct, auto)
  1034 done
  1035 
  1036 text{*UNUSED unicity result*}
  1037 lemma unique_KC2:
  1038      "[|Says C B {|Crypt K {|Agent C, nn, Key KC2, X|}, Y|} \<in> set evs;
  1039         Says C B' {|Crypt K' {|Agent C, nn', Key KC2, X'|}, Y'|} \<in> set evs;
  1040         C \<notin> bad;  evs \<in> set_cr|] ==> B'=B & X'=X"
  1041 apply (erule rev_mp)
  1042 apply (erule rev_mp)
  1043 apply (erule set_cr.induct, auto)
  1044 done
  1045 (*>*)
  1046 
  1047 
  1048 text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
  1049   it could be a previously compromised cardSK [e.g. involving a bad CA]*}
  1050 
  1051 
  1052 end