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