src/HOL/SET-Protocol/Purchase.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/Purchase
     2     Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
     3 *)
     4 
     5 header{*Purchase Phase of SET*}
     6 
     7 theory Purchase imports PublicSET begin
     8 
     9 text{*
    10 Note: nonces seem to consist of 20 bytes.  That includes both freshness
    11 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)
    12 
    13 This version omits @{text LID_C} but retains @{text LID_M}. At first glance
    14 (Programmer's Guide page 267) it seems that both numbers are just introduced
    15 for the respective convenience of the Cardholder's and Merchant's
    16 system. However, omitting both of them would create a problem of
    17 identification: how can the Merchant's system know what transaction is it
    18 supposed to process?
    19 
    20 Further reading (Programmer's guide page 309) suggest that there is an outside
    21 bootstrapping message (SET initiation message) which is used by the Merchant
    22 and the Cardholder to agree on the actual transaction. This bootstrapping
    23 message is described in the SET External Interface Guide and ought to generate
    24 @{text LID_M}. According SET Extern Interface Guide, this number might be a
    25 cookie, an invoice number etc. The Programmer's Guide on page 310, states that
    26 in absence of @{text LID_M} the protocol must somehow ("outside SET") identify
    27 the transaction from OrderDesc, which is assumed to be a searchable text only
    28 field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed
    29 out-of-bad on the value of @{text LID_M} (for instance a cookie in a web
    30 transaction etc.). This out-of-band agreement is expressed with a preliminary
    31 start action in which the merchant and the Cardholder agree on the appropriate
    32 values. Agreed values are stored with a suitable notes action.
    33 
    34 "XID is a transaction ID that is usually generated by the Merchant system,
    35 unless there is no PInitRes, in which case it is generated by the Cardholder
    36 system. It is a randomly generated 20 byte variable that is globally unique
    37 (statistically). Merchant and Cardholder systems shall use appropriate random
    38 number generators to ensure the global uniqueness of XID."
    39 --Programmer's Guide, page 267.
    40 
    41 PI (Payment Instruction) is the most central and sensitive data structure in
    42 SET. It is used to pass the data required to authorize a payment card payment
    43 from the Cardholder to the Payment Gateway, which will use the data to
    44 initiate a payment card transaction through the traditional payment card
    45 financial network. The data is encrypted by the Cardholder and sent via the
    46 Merchant, such that the data is hidden from the Merchant unless the Acquirer
    47 passes the data back to the Merchant.
    48 --Programmer's Guide, page 271.*}
    49 
    50 consts
    51 
    52     CardSecret :: "nat => nat"
    53      --{*Maps Cardholders to CardSecrets.
    54          A CardSecret of 0 means no cerificate, must use unsigned format.*}
    55 
    56     PANSecret :: "nat => nat"
    57      --{*Maps Cardholders to PANSecrets.*}
    58 
    59 inductive_set
    60   set_pur :: "event list set"
    61 where
    62 
    63   Nil:   --{*Initial trace is empty*}
    64 	 "[] \<in> set_pur"
    65 
    66 | Fake:  --{*The spy MAY say anything he CAN say.*}
    67 	 "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]
    68 	  ==> Says Spy B X  # evsf \<in> set_pur"
    69 
    70 
    71 | Reception: --{*If A sends a message X to B, then B might receive it*}
    72 	     "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]
    73 	      ==> Gets B X  # evsr \<in> set_pur"
    74 
    75 | Start: 
    76       --{*Added start event which is out-of-band for SET: the Cardholder and
    77 	  the merchant agree on the amounts and uses @{text LID_M} as an
    78           identifier.
    79 	  This is suggested by the External Interface Guide. The Programmer's
    80 	  Guide, in absence of @{text LID_M}, states that the merchant uniquely
    81 	  identifies the order out of some data contained in OrderDesc.*}
    82    "[|evsStart \<in> set_pur;
    83       Number LID_M \<notin> used evsStart;
    84       C = Cardholder k; M = Merchant i; P = PG j;
    85       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    86       LID_M \<notin> range CardSecret;
    87       LID_M \<notin> range PANSecret |]
    88      ==> Notes C {|Number LID_M, Transaction|}
    89        # Notes M {|Number LID_M, Agent P, Transaction|}
    90        # evsStart \<in> set_pur"
    91 
    92 | PInitReq:
    93      --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
    94    "[|evsPIReq \<in> set_pur;
    95       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    96       Nonce Chall_C \<notin> used evsPIReq;
    97       Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;
    98       Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
    99     ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
   100 
   101 | PInitRes:
   102      --{*Merchant replies with his own label XID and the encryption
   103 	 key certificate of his chosen Payment Gateway. Page 74 of Formal
   104          Protocol Desc. We use @{text LID_M} to identify Cardholder*}
   105    "[|evsPIRes \<in> set_pur;
   106       Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;
   107       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   108       Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;
   109       Nonce Chall_M \<notin> used evsPIRes;
   110       Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;
   111       Number XID \<notin> used evsPIRes;
   112       XID \<notin> range CardSecret; XID \<notin> range PANSecret|]
   113     ==> Says M C (sign (priSK M)
   114 		       {|Number LID_M, Number XID,
   115 			 Nonce Chall_C, Nonce Chall_M,
   116 			 cert P (pubEK P) onlyEnc (priSK RCA)|})
   117           # evsPIRes \<in> set_pur"
   118 
   119 | PReqUns:
   120       --{*UNSIGNED Purchase request (CardSecret = 0).
   121 	Page 79 of Formal Protocol Desc.
   122 	Merchant never sees the amount in clear. This holds of the real
   123 	protocol, where XID identifies the transaction. We omit
   124 	Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
   125 	the CardSecret is 0 and because AuthReq treated the unsigned case
   126 	very differently from the signed one anyway.*}
   127    "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
   128     [|evsPReqU \<in> set_pur;
   129       C = Cardholder k; CardSecret k = 0;
   130       Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
   131       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   132       HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   133       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};
   134       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
   135       Gets C (sign (priSK M)
   136 		   {|Number LID_M, Number XID,
   137 		     Nonce Chall_C, Nonce Chall_M,
   138 		     cert P EKj onlyEnc (priSK RCA)|})
   139 	\<in> set evsPReqU;
   140       Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;
   141       Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]
   142     ==> Says C M
   143 	     {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
   144 	       OIData, Hash{|PIHead, Pan (pan C)|} |}
   145 	  # Notes C {|Key KC1, Agent M|}
   146 	  # evsPReqU \<in> set_pur"
   147 
   148 | PReqS:
   149       --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
   150           We could specify the equation
   151 	  @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
   152 	  Formal Desc. gives PIHead the same format in the unsigned case.
   153 	  However, there's little point, as P treats the signed and 
   154           unsigned cases differently.*}
   155    "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData
   156       OIDualSigned OrderDesc P PANData PIData PIDualSigned
   157       PIHead PurchAmt Transaction XID evsPReqS k.
   158     [|evsPReqS \<in> set_pur;
   159       C = Cardholder k;
   160       CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
   161       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   162       HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   163       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};
   164       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
   165 		  Hash{|Number XID, Nonce (CardSecret k)|}|};
   166       PANData = {|Pan (pan C), Nonce (PANSecret k)|};
   167       PIData = {|PIHead, PANData|};
   168       PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},
   169 		       EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};
   170       OIDualSigned = {|OIData, Hash PIData|};
   171       Gets C (sign (priSK M)
   172 		   {|Number LID_M, Number XID,
   173 		     Nonce Chall_C, Nonce Chall_M,
   174 		     cert P EKj onlyEnc (priSK RCA)|})
   175 	\<in> set evsPReqS;
   176       Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;
   177       Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]
   178     ==> Says C M {|PIDualSigned, OIDualSigned|}
   179 	  # Notes C {|Key KC2, Agent M|}
   180 	  # evsPReqS \<in> set_pur"
   181 
   182   --{*Authorization Request.  Page 92 of Formal Protocol Desc.
   183     Sent in response to Purchase Request.*}
   184 | AuthReq:
   185    "[| evsAReq \<in> set_pur;
   186        Key KM \<notin> used evsAReq;  KM \<in> symKeys;
   187        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   188        HOD = Hash{|Number OrderDesc, Number PurchAmt|};
   189        OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,
   190 		  Nonce Chall_M|};
   191        CardSecret k \<noteq> 0 -->
   192 	 P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
   193        Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;
   194        Says M C (sign (priSK M) {|Number LID_M, Number XID,
   195 				  Nonce Chall_C, Nonce Chall_M,
   196 				  cert P EKj onlyEnc (priSK RCA)|})
   197 	 \<in> set evsAReq;
   198 	Notes M {|Number LID_M, Agent P, Transaction|}
   199 	   \<in> set evsAReq |]
   200     ==> Says M P
   201 	     (EncB (priSK M) KM (pubEK P)
   202 	       {|Number LID_M, Number XID, Hash OIData, HOD|}	P_I)
   203 	  # evsAReq \<in> set_pur"
   204 
   205   --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.
   206     Page 99 of Formal Protocol Desc.
   207     PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and
   208     HOIData occur independently in @{text P_I} and in M's message.
   209     The authCode in AuthRes represents the baggage of EncB, which in the
   210     full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
   211     optional items for split shipments, recurring payments, etc.*}
   212 
   213 | AuthResUns:
   214     --{*Authorization Response, UNSIGNED*}
   215    "[| evsAResU \<in> set_pur;
   216        C = Cardholder k; M = Merchant i;
   217        Key KP \<notin> used evsAResU;  KP \<in> symKeys;
   218        CardSecret k = 0;  KC1 \<in> symKeys;  KM \<in> symKeys;
   219        PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};
   220        P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));
   221        Gets P (EncB (priSK M) KM (pubEK P)
   222 	       {|Number LID_M, Number XID, HOIData, HOD|} P_I)
   223 	   \<in> set evsAResU |]
   224    ==> Says P M
   225 	    (EncB (priSK P) KP (pubEK M)
   226 	      {|Number LID_M, Number XID, Number PurchAmt|}
   227 	      authCode)
   228        # evsAResU \<in> set_pur"
   229 
   230 | AuthResS:
   231     --{*Authorization Response, SIGNED*}
   232    "[| evsAResS \<in> set_pur;
   233        C = Cardholder k;
   234        Key KP \<notin> used evsAResS;  KP \<in> symKeys;
   235        CardSecret k \<noteq> 0;  KC2 \<in> symKeys;  KM \<in> symKeys;
   236        P_I = {|sign (priSK C) {|Hash PIData, HOIData|},
   237 	       EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};
   238        PANData = {|Pan (pan C), Nonce (PANSecret k)|};
   239        PIData = {|PIHead, PANData|};
   240        PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
   241 		  Hash{|Number XID, Nonce (CardSecret k)|}|};
   242        Gets P (EncB (priSK M) KM (pubEK P)
   243 		{|Number LID_M, Number XID, HOIData, HOD|}
   244 	       P_I)
   245 	   \<in> set evsAResS |]
   246    ==> Says P M
   247 	    (EncB (priSK P) KP (pubEK M)
   248 	      {|Number LID_M, Number XID, Number PurchAmt|}
   249 	      authCode)
   250        # evsAResS \<in> set_pur"
   251 
   252 | PRes:
   253     --{*Purchase response.*}
   254    "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
   255        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   256        Gets M (EncB (priSK P) KP (pubEK M)
   257 	      {|Number LID_M, Number XID, Number PurchAmt|}
   258 	      authCode)
   259 	  \<in> set evsPRes;
   260        Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;
   261        Says M P
   262 	    (EncB (priSK M) KM (pubEK P)
   263 	      {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
   264 	 \<in> set evsPRes;
   265        Notes M {|Number LID_M, Agent P, Transaction|}
   266 	  \<in> set evsPRes
   267       |]
   268    ==> Says M C
   269 	 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
   270 			   Hash (Number PurchAmt)|})
   271 	 # evsPRes \<in> set_pur"
   272 
   273 
   274 specification (CardSecret PANSecret)
   275   inj_CardSecret:  "inj CardSecret"
   276   inj_PANSecret:   "inj PANSecret"
   277   CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
   278     --{*No CardSecret equals any PANSecret*}
   279   apply (rule_tac x="curry nat2_to_nat 0" in exI)
   280   apply (rule_tac x="curry nat2_to_nat 1" in exI)
   281   apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
   282   done
   283 
   284 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
   285 declare parts.Body [dest]
   286 declare analz_into_parts [dest]
   287 declare Fake_parts_insert_in_Un [dest]
   288 
   289 declare CardSecret_neq_PANSecret [iff] 
   290         CardSecret_neq_PANSecret [THEN not_sym, iff]
   291 declare inj_CardSecret [THEN inj_eq, iff] 
   292         inj_PANSecret [THEN inj_eq, iff]
   293 
   294 
   295 subsection{*Possibility Properties*}
   296 
   297 lemma Says_to_Gets:
   298      "Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"
   299 by (rule set_pur.Reception, auto)
   300 
   301 text{*Possibility for UNSIGNED purchases. Note that we need to ensure
   302 that XID differs from OrderDesc and PurchAmt, since it is supposed to be
   303 a unique number!*}
   304 lemma possibility_Uns:
   305     "[| CardSecret k = 0;
   306         C = Cardholder k;  M = Merchant i;
   307 	Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
   308 	KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
   309 	KC < KM; KM < KP;
   310 	Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
   311         Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
   312 	Chall_C < Chall_M; 
   313         Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
   314         Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
   315         LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 
   316    ==> \<exists>evs \<in> set_pur.
   317           Says M C
   318                (sign (priSK M)
   319                     {|Number LID_M, Number XID, Nonce Chall_C, 
   320                       Hash (Number PurchAmt)|})
   321                   \<in> set evs" 
   322 apply (intro exI bexI)
   323 apply (rule_tac [2]
   324 	set_pur.Nil
   325          [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
   326 	  THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
   327           THEN Says_to_Gets, 
   328 	  THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
   329           THEN Says_to_Gets,
   330 	  THEN set_pur.PReqUns [of concl: C M KC],
   331           THEN Says_to_Gets, 
   332 	  THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
   333           THEN Says_to_Gets, 
   334 	  THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],
   335           THEN Says_to_Gets, 
   336 	  THEN set_pur.PRes]) 
   337 apply basic_possibility
   338 apply (simp_all add: used_Cons symKeys_neq_imp_neq) 
   339 done
   340 
   341 lemma possibility_S:
   342     "[| CardSecret k \<noteq> 0;
   343         C = Cardholder k;  M = Merchant i;
   344 	Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
   345 	KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
   346 	KC < KM; KM < KP;
   347 	Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;
   348         Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;
   349 	Chall_C < Chall_M; 
   350         Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;
   351         Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;
   352         LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 
   353    ==>  \<exists>evs \<in> set_pur.
   354             Says M C
   355                  (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, 
   356                                    Hash (Number PurchAmt)|})
   357                \<in> set evs"
   358 apply (intro exI bexI)
   359 apply (rule_tac [2]
   360 	set_pur.Nil
   361          [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
   362 	  THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],
   363           THEN Says_to_Gets, 
   364 	  THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
   365           THEN Says_to_Gets,
   366 	  THEN set_pur.PReqS [of concl: C M _ _ KC],
   367           THEN Says_to_Gets, 
   368 	  THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
   369           THEN Says_to_Gets, 
   370 	  THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],
   371           THEN Says_to_Gets, 
   372 	  THEN set_pur.PRes]) 
   373 apply basic_possibility
   374 apply (auto simp add: used_Cons symKeys_neq_imp_neq) 
   375 done
   376 
   377 text{*General facts about message reception*}
   378 lemma Gets_imp_Says:
   379      "[| Gets B X \<in> set evs; evs \<in> set_pur |]
   380    ==> \<exists>A. Says A B X \<in> set evs"
   381 apply (erule rev_mp)
   382 apply (erule set_pur.induct, auto)
   383 done
   384 
   385 lemma Gets_imp_knows_Spy:
   386      "[| Gets B X \<in> set evs; evs \<in> set_pur |]  ==> X \<in> knows Spy evs"
   387 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   388 
   389 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]
   390 
   391 text{*Forwarding lemmas, to aid simplification*}
   392 
   393 lemma AuthReq_msg_in_parts_spies:
   394      "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
   395         evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"
   396 by auto
   397 
   398 lemma AuthReq_msg_in_analz_spies:
   399      "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;
   400         evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"
   401 by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])
   402 
   403 
   404 subsection{*Proofs on Asymmetric Keys*}
   405 
   406 text{*Private Keys are Secret*}
   407 
   408 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}
   409 lemma Spy_see_private_Key [simp]:
   410      "evs \<in> set_pur
   411       ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"
   412 apply (erule set_pur.induct)
   413 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   414 apply auto
   415 done
   416 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]
   417 
   418 lemma Spy_analz_private_Key [simp]:
   419      "evs \<in> set_pur ==>
   420      (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"
   421 by auto
   422 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]
   423 
   424 text{*rewriting rule for priEK's*}
   425 lemma parts_image_priEK:
   426      "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));
   427         evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"
   428 by auto
   429 
   430 text{*trivial proof because @{term"priEK C"} never appears even in
   431   @{term "parts evs"}. *}
   432 lemma analz_image_priEK:
   433      "evs \<in> set_pur ==>
   434           (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =
   435           (priEK C \<in> KK | C \<in> bad)"
   436 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])
   437 
   438 
   439 subsection{*Public Keys in Certificates are Correct*}
   440 
   441 lemma Crypt_valid_pubEK [dest!]:
   442      "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}
   443            \<in> parts (knows Spy evs);
   444          evs \<in> set_pur |] ==> EKi = pubEK C"
   445 by (erule rev_mp, erule set_pur.induct, auto)
   446 
   447 lemma Crypt_valid_pubSK [dest!]:
   448      "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}
   449            \<in> parts (knows Spy evs);
   450          evs \<in> set_pur |] ==> SKi = pubSK C"
   451 by (erule rev_mp, erule set_pur.induct, auto)
   452 
   453 lemma certificate_valid_pubEK:
   454     "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);
   455         evs \<in> set_pur |]
   456      ==> EKi = pubEK C"
   457 by (unfold cert_def signCert_def, auto)
   458 
   459 lemma certificate_valid_pubSK:
   460     "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);
   461         evs \<in> set_pur |] ==> SKi = pubSK C"
   462 by (unfold cert_def signCert_def, auto)
   463 
   464 lemma Says_certificate_valid [simp]:
   465      "[| Says A B (sign SK {|lid, xid, cc, cm,
   466                            cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
   467          evs \<in> set_pur |]
   468       ==> EK = pubEK C"
   469 by (unfold sign_def, auto)
   470 
   471 lemma Gets_certificate_valid [simp]:
   472      "[| Gets A (sign SK {|lid, xid, cc, cm,
   473                            cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;
   474          evs \<in> set_pur |]
   475       ==> EK = pubEK C"
   476 by (frule Gets_imp_Says, auto)
   477 
   478 method_setup valid_certificate_tac = {*
   479   Args.goal_spec >> (fn quant =>
   480     K (SIMPLE_METHOD'' quant (fn i =>
   481       EVERY [ftac @{thm Gets_certificate_valid} i,
   482              assume_tac i, REPEAT (hyp_subst_tac i)])))
   483 *} ""
   484 
   485 
   486 subsection{*Proofs on Symmetric Keys*}
   487 
   488 text{*Nobody can have used non-existent keys!*}
   489 lemma new_keys_not_used [rule_format,simp]:
   490      "evs \<in> set_pur
   491       ==> Key K \<notin> used evs --> K \<in> symKeys -->
   492           K \<notin> keysFor (parts (knows Spy evs))"
   493 apply (erule set_pur.induct)
   494 apply (valid_certificate_tac [8]) --{*PReqS*}
   495 apply (valid_certificate_tac [7]) --{*PReqUns*}
   496 apply auto
   497 apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
   498 done
   499 
   500 lemma new_keys_not_analzd:
   501      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   502       ==> K \<notin> keysFor (analz (knows Spy evs))"
   503 by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used)
   504 
   505 lemma Crypt_parts_imp_used:
   506      "[|Crypt K X \<in> parts (knows Spy evs);
   507         K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
   508 apply (rule ccontr)
   509 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)
   510 done
   511 
   512 lemma Crypt_analz_imp_used:
   513      "[|Crypt K X \<in> analz (knows Spy evs);
   514         K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"
   515 by (blast intro: Crypt_parts_imp_used)
   516 
   517 text{*New versions: as above, but generalized to have the KK argument*}
   518 
   519 lemma gen_new_keys_not_used:
   520      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   521       ==> Key K \<notin> used evs --> K \<in> symKeys -->
   522           K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"
   523 by auto
   524 
   525 lemma gen_new_keys_not_analzd:
   526      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   527       ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"
   528 by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used)
   529 
   530 lemma analz_Key_image_insert_eq:
   531      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]
   532       ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =
   533           insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"
   534 by (simp add: gen_new_keys_not_analzd)
   535 
   536 
   537 subsection{*Secrecy of Symmetric Keys*}
   538 
   539 lemma Key_analz_image_Key_lemma:
   540      "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)
   541       ==>
   542       P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"
   543 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   544 
   545 
   546 lemma symKey_compromise:
   547      "evs \<in> set_pur \<Longrightarrow>
   548       (\<forall>SK KK. SK \<in> symKeys \<longrightarrow>
   549         (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow>
   550                (Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) =
   551                (SK \<in> KK \<or> Key SK \<in> analz (knows Spy evs)))"
   552 apply (erule set_pur.induct)
   553 apply (rule_tac [!] allI)+
   554 apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+
   555 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   556 apply (valid_certificate_tac [8]) --{*PReqS*}
   557 apply (valid_certificate_tac [7]) --{*PReqUns*}
   558 apply (simp_all
   559          del: image_insert image_Un imp_disjL
   560          add: analz_image_keys_simps disj_simps
   561               analz_Key_image_insert_eq notin_image_iff
   562               analz_insert_simps analz_image_priEK)
   563   --{*8 seconds on a 1.6GHz machine*}
   564 apply spy_analz --{*Fake*}
   565 apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}
   566 done
   567 
   568 
   569 
   570 subsection{*Secrecy of Nonces*}
   571 
   572 text{*As usual: we express the property as a logical equivalence*}
   573 lemma Nonce_analz_image_Key_lemma:
   574      "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)
   575       ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"
   576 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   577 
   578 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   579   the quantifier and allows the simprule's condition to itself be simplified.*}
   580 lemma Nonce_compromise [rule_format (no_asm)]:
   581      "evs \<in> set_pur ==>
   582       (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C))   -->
   583               (Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) =
   584               (Nonce N \<in> analz (knows Spy evs)))"
   585 apply (erule set_pur.induct)
   586 apply (rule_tac [!] allI)+
   587 apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+
   588 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   589 apply (valid_certificate_tac [8]) --{*PReqS*}
   590 apply (valid_certificate_tac [7]) --{*PReqUns*}
   591 apply (simp_all
   592          del: image_insert image_Un imp_disjL
   593          add: analz_image_keys_simps disj_simps symKey_compromise
   594               analz_Key_image_insert_eq notin_image_iff
   595               analz_insert_simps analz_image_priEK)
   596   --{*8 seconds on a 1.6GHz machine*}
   597 apply spy_analz --{*Fake*}
   598 apply (blast elim!: ballE) --{*PReqS*}
   599 done
   600 
   601 lemma PANSecret_notin_spies:
   602      "[|Nonce (PANSecret k) \<in> analz (knows Spy evs);  evs \<in> set_pur|]
   603       ==> 
   604        (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.
   605           Says (Cardholder k) M
   606                {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
   607                  V|}  \<in>  set evs)"
   608 apply (erule rev_mp)
   609 apply (erule set_pur.induct)
   610 apply (frule_tac [9] AuthReq_msg_in_analz_spies)
   611 apply (valid_certificate_tac [8]) --{*PReqS*}
   612 apply (simp_all
   613          del: image_insert image_Un imp_disjL
   614          add: analz_image_keys_simps disj_simps
   615               symKey_compromise pushes sign_def Nonce_compromise
   616               analz_Key_image_insert_eq notin_image_iff
   617               analz_insert_simps analz_image_priEK)
   618   --{*2.5 seconds on a 1.6GHz machine*}
   619 apply spy_analz
   620 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
   621 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
   622                    Gets_imp_knows_Spy [THEN analz.Inj])
   623 apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*}
   624 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 
   625                    Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*}
   626 done
   627 
   628 text{*This theorem is a bit silly, in that many CardSecrets are 0!
   629   But then we don't care.  NOT USED*}
   630 lemma CardSecret_notin_spies:
   631      "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"
   632 by (erule set_pur.induct, auto)
   633 
   634 
   635 subsection{*Confidentiality of PAN*}
   636 
   637 lemma analz_image_pan_lemma:
   638      "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>
   639       (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"
   640 by (blast intro: analz_mono [THEN [2] rev_subsetD])
   641 
   642 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   643   the quantifier and allows the simprule's condition to itself be simplified.*}
   644 lemma analz_image_pan [rule_format (no_asm)]:
   645      "evs \<in> set_pur ==>
   646        \<forall>KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->
   647             (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =
   648             (Pan P \<in> analz (knows Spy evs))"
   649 apply (erule set_pur.induct)
   650 apply (rule_tac [!] allI impI)+
   651 apply (rule_tac [!] analz_image_pan_lemma)+
   652 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   653 apply (valid_certificate_tac [8]) --{*PReqS*}
   654 apply (valid_certificate_tac [7]) --{*PReqUns*}
   655 apply (simp_all
   656          del: image_insert image_Un imp_disjL
   657          add: analz_image_keys_simps
   658               symKey_compromise pushes sign_def
   659               analz_Key_image_insert_eq notin_image_iff
   660               analz_insert_simps analz_image_priEK)
   661   --{*7 seconds on a 1.6GHz machine*}
   662 apply spy_analz --{*Fake*}
   663 apply auto
   664 done
   665 
   666 lemma analz_insert_pan:
   667      "[| evs \<in> set_pur;  K \<notin> range(\<lambda>C. priEK C) |] ==>
   668           (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =
   669           (Pan P \<in> analz (knows Spy evs))"
   670 by (simp del: image_insert image_Un
   671          add: analz_image_keys_simps analz_image_pan)
   672 
   673 text{*Confidentiality of the PAN, unsigned case.*}
   674 theorem pan_confidentiality_unsigned:
   675      "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
   676          CardSecret k = 0;  evs \<in> set_pur|]
   677     ==> \<exists>P M KC1 K X Y.
   678      Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
   679           \<in> set evs  &
   680      P \<in> bad"
   681 apply (erule rev_mp)
   682 apply (erule set_pur.induct)
   683 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   684 apply (valid_certificate_tac [8]) --{*PReqS*}
   685 apply (valid_certificate_tac [7]) --{*PReqUns*}
   686 apply (simp_all
   687          del: image_insert image_Un imp_disjL
   688          add: analz_image_keys_simps analz_insert_pan analz_image_pan
   689               notin_image_iff
   690               analz_insert_simps analz_image_priEK)
   691   --{*3 seconds on a 1.6GHz machine*}
   692 apply spy_analz --{*Fake*}
   693 apply blast --{*PReqUns: unsigned*}
   694 apply force --{*PReqS: signed*}
   695 done
   696 
   697 text{*Confidentiality of the PAN, signed case.*}
   698 theorem pan_confidentiality_signed:
   699  "[|Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
   700     CardSecret k \<noteq> 0;  evs \<in> set_pur|]
   701   ==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.
   702       Says C M {|{|PIDualSign_1, 
   703                    EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, 
   704        OIDualSign|} \<in> set evs  &  P \<in> bad"
   705 apply (erule rev_mp)
   706 apply (erule set_pur.induct)
   707 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
   708 apply (valid_certificate_tac [8]) --{*PReqS*}
   709 apply (valid_certificate_tac [7]) --{*PReqUns*}
   710 apply (simp_all
   711          del: image_insert image_Un imp_disjL
   712          add: analz_image_keys_simps analz_insert_pan analz_image_pan
   713               notin_image_iff
   714               analz_insert_simps analz_image_priEK)
   715   --{*3 seconds on a 1.6GHz machine*}
   716 apply spy_analz --{*Fake*}
   717 apply force --{*PReqUns: unsigned*}
   718 apply blast --{*PReqS: signed*}
   719 done
   720 
   721 text{*General goal: that C, M and PG agree on those details of the transaction
   722      that they are allowed to know about.  PG knows about price and account
   723      details.  M knows about the order description and price.  C knows both.*}
   724 
   725 
   726 subsection{*Proofs Common to Signed and Unsigned Versions*}
   727 
   728 lemma M_Notes_PG:
   729      "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;
   730         evs \<in> set_pur|] ==> \<exists>j. P = PG j"
   731 by (erule rev_mp, erule set_pur.induct, simp_all)
   732 
   733 text{*If we trust M, then @{term LID_M} determines his choice of P
   734       (Payment Gateway)*}
   735 lemma goodM_gives_correct_PG:
   736      "[| MsgPInitRes = 
   737             {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
   738          Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
   739          evs \<in> set_pur; M \<notin> bad |]
   740       ==> \<exists>j trans.
   741             P = PG j &
   742             Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"
   743 apply clarify
   744 apply (erule rev_mp)
   745 apply (erule set_pur.induct)
   746 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   747 apply simp_all
   748 apply (blast intro: M_Notes_PG)+
   749 done
   750 
   751 lemma C_gets_correct_PG:
   752      "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,
   753                               cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;
   754          evs \<in> set_pur;  M \<notin> bad|]
   755       ==> \<exists>j trans.
   756             P = PG j &
   757             Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   758             EKj = pubEK P"
   759 by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)
   760 
   761 text{*When C receives PInitRes, he learns M's choice of P*}
   762 lemma C_verifies_PInitRes:
   763  "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,
   764 	   cert P EKj onlyEnc (priSK RCA)|};
   765      Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);
   766      evs \<in> set_pur;  M \<notin> bad|]
   767   ==> \<exists>j trans.
   768          Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   769          P = PG j &
   770          EKj = pubEK P"
   771 apply clarify
   772 apply (erule rev_mp)
   773 apply (erule set_pur.induct)
   774 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   775 apply simp_all
   776 apply (blast intro: M_Notes_PG)+
   777 done
   778 
   779 text{*Corollary of previous one*}
   780 lemma Says_C_PInitRes:
   781      "[|Says A C (sign (priSK M)
   782                       {|Number LID_M, Number XID,
   783                         Nonce Chall_C, Nonce Chall_M,
   784                         cert P EKj onlyEnc (priSK RCA)|})
   785            \<in> set evs;  M \<notin> bad;  evs \<in> set_pur|]
   786       ==> \<exists>j trans.
   787            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &
   788            P = PG j &
   789            EKj = pubEK (PG j)"
   790 apply (frule Says_certificate_valid)
   791 apply (auto simp add: sign_def)
   792 apply (blast dest: refl [THEN goodM_gives_correct_PG])
   793 apply (blast dest: refl [THEN C_verifies_PInitRes])
   794 done
   795 
   796 text{*When P receives an AuthReq, he knows that the signed part originated 
   797       with M. PIRes also has a signed message from M....*}
   798 lemma P_verifies_AuthReq:
   799      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
   800          Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})
   801            \<in> parts (knows Spy evs);
   802          evs \<in> set_pur;  M \<notin> bad|]
   803       ==> \<exists>j trans KM OIData HPIData.
   804             Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
   805             Gets M {|P_I, OIData, HPIData|} \<in> set evs &
   806             Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
   807               \<in> set evs"
   808 apply clarify
   809 apply (erule rev_mp)
   810 apply (erule set_pur.induct, simp_all)
   811 apply (frule_tac [4] M_Notes_PG, auto)
   812 done
   813 
   814 text{*When M receives AuthRes, he knows that P signed it, including
   815   the identifying tags and the purchase amount, which he can verify.
   816   (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
   817    send the same message to M.)  The conclusion is weak: M is existentially
   818   quantified! That is because Authorization Response does not refer to M, while
   819   the digital envelope weakens the link between @{term MsgAuthRes} and
   820   @{term"priSK M"}.  Changing the precondition to refer to 
   821   @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since
   822   otherwise the Spy could create that message.*}
   823 theorem M_verifies_AuthRes:
   824   "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 
   825                      Hash authCode|};
   826       Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
   827       PG j \<notin> bad;  evs \<in> set_pur|]
   828    ==> \<exists>M KM KP HOIData HOD P_I.
   829 	Gets (PG j)
   830 	   (EncB (priSK M) KM (pubEK (PG j))
   831 		    {|Number LID_M, Number XID, HOIData, HOD|}
   832 		    P_I) \<in> set evs &
   833 	Says (PG j) M
   834 	     (EncB (priSK (PG j)) KP (pubEK M)
   835 	      {|Number LID_M, Number XID, Number PurchAmt|}
   836 	      authCode) \<in> set evs"
   837 apply clarify
   838 apply (erule rev_mp)
   839 apply (erule set_pur.induct)
   840 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   841 apply simp_all
   842 apply blast+
   843 done
   844 
   845 
   846 subsection{*Proofs for Unsigned Purchases*}
   847 
   848 text{*What we can derive from the ASSUMPTION that C issued a purchase request.
   849    In the unsigned case, we must trust "C": there's no authentication.*}
   850 lemma C_determines_EKj:
   851      "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),
   852                     OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;
   853          PIHead = {|Number LID_M, Trans_details|};
   854          evs \<in> set_pur;  C = Cardholder k;  M \<notin> bad|]
   855   ==> \<exists>trans j.
   856                Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
   857                EKj = pubEK (PG j)"
   858 apply clarify
   859 apply (erule rev_mp)
   860 apply (erule set_pur.induct, simp_all)
   861 apply (valid_certificate_tac [2]) --{*PReqUns*}
   862 apply auto
   863 apply (blast dest: Gets_imp_Says Says_C_PInitRes)
   864 done
   865 
   866 
   867 text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}
   868 lemma unique_LID_M:
   869      "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;
   870         Notes C {|Number LID_M, Agent M, Agent C, Number OD,
   871              Number PA|} \<in> set evs;
   872         evs \<in> set_pur|]
   873       ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"
   874 apply (erule rev_mp)
   875 apply (erule rev_mp)
   876 apply (erule set_pur.induct, simp_all)
   877 apply (force dest!: Notes_imp_parts_subset_used)
   878 done
   879 
   880 text{*Unicity of @{term LID_M}, for two Merchant Notes events*}
   881 lemma unique_LID_M2:
   882      "[|Notes M {|Number LID_M, Trans|} \<in> set evs;
   883         Notes M {|Number LID_M, Trans'|} \<in> set evs;
   884         evs \<in> set_pur|] ==> Trans' = Trans"
   885 apply (erule rev_mp)
   886 apply (erule rev_mp)
   887 apply (erule set_pur.induct, simp_all)
   888 apply (force dest!: Notes_imp_parts_subset_used)
   889 done
   890 
   891 text{*Lemma needed below: for the case that
   892   if PRes is present, then @{term LID_M} has been used.*}
   893 lemma signed_imp_used:
   894      "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);
   895          M \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
   896 apply (erule rev_mp)
   897 apply (erule set_pur.induct)
   898 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   899 apply simp_all
   900 apply safe
   901 apply blast+
   902 done
   903 
   904 text{*Similar, with nested Hash*}
   905 lemma signed_Hash_imp_used:
   906      "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);
   907          C \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"
   908 apply (erule rev_mp)
   909 apply (erule set_pur.induct)
   910 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   911 apply simp_all
   912 apply safe
   913 apply blast+
   914 done
   915 
   916 text{*Lemma needed below: for the case that
   917   if PRes is present, then @{text LID_M} has been used.*}
   918 lemma PRes_imp_LID_used:
   919      "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);
   920          M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"
   921 by (drule signed_imp_used, auto)
   922 
   923 text{*When C receives PRes, he knows that M and P agreed to the purchase details.
   924   He also knows that P is the same PG as before*}
   925 lemma C_verifies_PRes_lemma:
   926      "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);
   927          Notes C {|Number LID_M, Trans |} \<in> set evs;
   928          Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
   929          MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
   930                 Hash (Number PurchAmt)|};
   931          evs \<in> set_pur;  M \<notin> bad|]
   932   ==> \<exists>j KP.
   933         Notes M {|Number LID_M, Agent (PG j), Trans |}
   934           \<in> set evs &
   935         Gets M (EncB (priSK (PG j)) KP (pubEK M)
   936                 {|Number LID_M, Number XID, Number PurchAmt|}
   937                 authCode)
   938           \<in> set evs &
   939         Says M C (sign (priSK M) MsgPRes) \<in> set evs"
   940 apply clarify
   941 apply (erule rev_mp)
   942 apply (erule rev_mp)
   943 apply (erule set_pur.induct)
   944 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   945 apply simp_all
   946 apply blast
   947 apply blast
   948 apply (blast dest: PRes_imp_LID_used)
   949 apply (frule M_Notes_PG, auto)
   950 apply (blast dest: unique_LID_M)
   951 done
   952 
   953 text{*When the Cardholder receives Purchase Response from an uncompromised
   954 Merchant, he knows that M sent it. He also knows that M received a message signed
   955 by a Payment Gateway chosen by M to authorize the purchase.*}
   956 theorem C_verifies_PRes:
   957      "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
   958                      Hash (Number PurchAmt)|};
   959          Gets C (sign (priSK M) MsgPRes) \<in> set evs;
   960          Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
   961                    Number PurchAmt|} \<in> set evs;
   962          evs \<in> set_pur;  M \<notin> bad|]
   963   ==> \<exists>P KP trans.
   964         Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
   965         Gets M (EncB (priSK P) KP (pubEK M)
   966                 {|Number LID_M, Number XID, Number PurchAmt|}
   967                 authCode)  \<in>  set evs &
   968         Says M C (sign (priSK M) MsgPRes) \<in> set evs"
   969 apply (rule C_verifies_PRes_lemma [THEN exE])
   970 apply (auto simp add: sign_def)
   971 done
   972 
   973 subsection{*Proofs for Signed Purchases*}
   974 
   975 text{*Some Useful Lemmas: the cardholder knows what he is doing*}
   976 
   977 lemma Crypt_imp_Says_Cardholder:
   978      "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
   979            \<in> parts (knows Spy evs);
   980          PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
   981          Key K \<notin> analz (knows Spy evs);
   982          evs \<in> set_pur|]
   983   ==> \<exists>M shash EK HPIData.
   984        Says (Cardholder k) M {|{|shash,
   985           Crypt K
   986             {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},
   987            Crypt EK {|Key K, PANData|}|},
   988           OIData, HPIData|} \<in> set evs"
   989 apply (erule rev_mp)
   990 apply (erule rev_mp)
   991 apply (erule rev_mp)
   992 apply (erule set_pur.induct, analz_mono_contra)
   993 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
   994 apply simp_all
   995 apply auto
   996 done
   997 
   998 lemma Says_PReqS_imp_trans_details_C:
   999      "[| MsgPReqS = {|{|shash,
  1000                  Crypt K
  1001                   {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},
  1002             cryptek|}, data|};
  1003          Says (Cardholder k) M MsgPReqS \<in> set evs;
  1004          evs \<in> set_pur |]
  1005    ==> \<exists>trans.
  1006            Notes (Cardholder k) 
  1007                  {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
  1008             \<in> set evs"
  1009 apply (erule rev_mp)
  1010 apply (erule rev_mp)
  1011 apply (erule set_pur.induct)
  1012 apply (simp_all (no_asm_simp))
  1013 apply auto
  1014 done
  1015 
  1016 text{*Can't happen: only Merchants create this type of Note*}
  1017 lemma Notes_Cardholder_self_False:
  1018      "[|Notes (Cardholder k)
  1019           {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;
  1020         evs \<in> set_pur|] ==> False"
  1021 by (erule rev_mp, erule set_pur.induct, auto)
  1022 
  1023 text{*When M sees a dual signature, he knows that it originated with C.
  1024   Using XID he knows it was intended for him.
  1025   This guarantee isn't useful to P, who never gets OIData.*}
  1026 theorem M_verifies_Signed_PReq:
  1027  "[| MsgDualSign = {|HPIData, Hash OIData|};
  1028      OIData = {|Number LID_M, etc|};
  1029      Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  1030      Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
  1031      M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
  1032   ==> \<exists>PIData PICrypt.
  1033 	HPIData = Hash PIData &
  1034 	Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
  1035 	  \<in> set evs"
  1036 apply clarify
  1037 apply (erule rev_mp)
  1038 apply (erule rev_mp)
  1039 apply (erule set_pur.induct)
  1040 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}
  1041 apply simp_all
  1042 apply blast
  1043 apply (force dest!: signed_Hash_imp_used)
  1044 apply (clarify) --{*speeds next step*}
  1045 apply (blast dest: unique_LID_M)
  1046 apply (blast dest!: Notes_Cardholder_self_False)
  1047 done
  1048 
  1049 text{*When P sees a dual signature, he knows that it originated with C.
  1050   and was intended for M. This guarantee isn't useful to M, who never gets
  1051   PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
  1052   assuming @{term "M \<notin> bad"}.*}
  1053 theorem P_verifies_Signed_PReq:
  1054      "[| MsgDualSign = {|Hash PIData, HOIData|};
  1055          PIData = {|PIHead, PANData|};
  1056          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  1057                     TransStain|};
  1058          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  1059          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
  1060     ==> \<exists>OIData OrderDesc K j trans.
  1061           HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
  1062           HOIData = Hash OIData &
  1063           Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
  1064           Says C M {|{|sign (priSK C) MsgDualSign,
  1065                      EXcrypt K (pubEK (PG j))
  1066                                 {|PIHead, Hash OIData|} PANData|},
  1067                      OIData, Hash PIData|}
  1068             \<in> set evs"
  1069 apply clarify
  1070 apply (erule rev_mp)
  1071 apply (erule set_pur.induct, simp_all)
  1072 apply (auto dest!: C_gets_correct_PG)
  1073 done
  1074 
  1075 lemma C_determines_EKj_signed:
  1076      "[| Says C M {|{|sign (priSK C) text,
  1077                       EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;
  1078          PIHead = {|Number LID_M, Number XID, W|};
  1079          C = Cardholder k;  evs \<in> set_pur;  M \<notin> bad|]
  1080   ==> \<exists> trans j.
  1081          Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &
  1082          EKj = pubEK (PG j)"
  1083 apply clarify
  1084 apply (erule rev_mp)
  1085 apply (erule set_pur.induct, simp_all, auto)
  1086 apply (blast dest: C_gets_correct_PG)
  1087 done
  1088 
  1089 lemma M_Says_AuthReq:
  1090      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
  1091          sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);
  1092          evs \<in> set_pur;  M \<notin> bad|]
  1093    ==> \<exists>j trans KM.
  1094            Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &
  1095              Says M (PG j)
  1096                (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
  1097               \<in> set evs"
  1098 apply (rule refl [THEN P_verifies_AuthReq, THEN exE])
  1099 apply (auto simp add: sign_def)
  1100 done
  1101 
  1102 text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information.
  1103   Even here we cannot be certain about what C sent to M, since a bad
  1104   PG could have replaced the two key fields.  (NOT USED)*}
  1105 lemma Signed_PReq_imp_Says_Cardholder:
  1106      "[| MsgDualSign = {|Hash PIData, Hash OIData|};
  1107          OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};
  1108          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  1109                     TransStain|};
  1110          PIData = {|PIHead, PANData|};
  1111          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
  1112          M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
  1113       ==> \<exists>KC EKj.
  1114             Says C M {|{|sign (priSK C) MsgDualSign,
  1115                        EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
  1116                        OIData, Hash PIData|}
  1117               \<in> set evs"
  1118 apply clarify
  1119 apply (erule rev_mp)
  1120 apply (erule rev_mp)
  1121 apply (erule set_pur.induct, simp_all, auto)
  1122 done
  1123 
  1124 text{*When P receives an AuthReq and a dual signature, he knows that C and M
  1125   agree on the essential details.  PurchAmt however is never sent by M to
  1126   P; instead C and M both send 
  1127      @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}
  1128   and P compares the two copies of HOD.
  1129 
  1130   Agreement can't be proved for some things, including the symmetric keys
  1131   used in the digital envelopes.  On the other hand, M knows the true identity
  1132   of PG (namely j'), and sends AReq there; he can't, however, check that
  1133   the EXcrypt involves the correct PG's key.
  1134 *}
  1135 theorem P_sees_CM_agreement:
  1136      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
  1137          KC \<in> symKeys;
  1138          Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
  1139            \<in> set evs;
  1140          C = Cardholder k;
  1141          PI_sign = sign (priSK C) {|Hash PIData, HOIData|};
  1142          P_I = {|PI_sign,
  1143                  EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};
  1144          PANData = {|Pan (pan C), Nonce (PANSecret k)|};
  1145          PIData = {|PIHead, PANData|};
  1146          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
  1147                     TransStain|};
  1148          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]
  1149   ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.
  1150            HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
  1151            HOIData = Hash OIData &
  1152            Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &
  1153            Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &
  1154            Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
  1155                            AuthReqData P_I'')  \<in>  set evs &
  1156            P_I' = {|PI_sign,
  1157              EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &
  1158            P_I'' = {|PI_sign,
  1159              EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"
  1160 apply clarify
  1161 apply (rule exE)
  1162 apply (rule P_verifies_Signed_PReq [OF refl refl refl])
  1163 apply (simp (no_asm_use) add: sign_def EncB_def, blast)
  1164 apply (assumption+, clarify, simp)
  1165 apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)
  1166 apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2)
  1167 done
  1168 
  1169 end