(*  Title:      HOL/SET_Protocol/Purchase.thy

     Author:     Giampaolo Bella

     Author:     Fabio Massacci

     Author:     Lawrence C Paulson

 *)

 header{*Purchase Phase of SET*}

 theory Purchase

 imports Public_SET

 begin

 text{*

 Note: nonces seem to consist of 20 bytes.  That includes both freshness

 challenges (Chall-EE, etc.) and important secrets (CardSecret, PANsecret)

 This version omits @{text LID_C} but retains @{text LID_M}. At first glance

 (Programmer's Guide page 267) it seems that both numbers are just introduced

 for the respective convenience of the Cardholder's and Merchant's

 system. However, omitting both of them would create a problem of

 identification: how can the Merchant's system know what transaction is it

 supposed to process?

 Further reading (Programmer's guide page 309) suggest that there is an outside

 bootstrapping message (SET initiation message) which is used by the Merchant

 and the Cardholder to agree on the actual transaction. This bootstrapping

 message is described in the SET External Interface Guide and ought to generate

 @{text LID_M}. According SET Extern Interface Guide, this number might be a

 cookie, an invoice number etc. The Programmer's Guide on page 310, states that

 in absence of @{text LID_M} the protocol must somehow ("outside SET") identify

 the transaction from OrderDesc, which is assumed to be a searchable text only

 field. Thus, it is assumed that the Merchant or the Cardholder somehow agreed

 out-of-bad on the value of @{text LID_M} (for instance a cookie in a web

 transaction etc.). This out-of-band agreement is expressed with a preliminary

 start action in which the merchant and the Cardholder agree on the appropriate

 values. Agreed values are stored with a suitable notes action.

 "XID is a transaction ID that is usually generated by the Merchant system,

 unless there is no PInitRes, in which case it is generated by the Cardholder

 system. It is a randomly generated 20 byte variable that is globally unique

 (statistically). Merchant and Cardholder systems shall use appropriate random

 number generators to ensure the global uniqueness of XID."

 --Programmer's Guide, page 267.

 PI (Payment Instruction) is the most central and sensitive data structure in

 SET. It is used to pass the data required to authorize a payment card payment

 from the Cardholder to the Payment Gateway, which will use the data to

 initiate a payment card transaction through the traditional payment card

 financial network. The data is encrypted by the Cardholder and sent via the

 Merchant, such that the data is hidden from the Merchant unless the Acquirer

 passes the data back to the Merchant.

 --Programmer's Guide, page 271.*}

 consts

     CardSecret :: "nat => nat"

      --{*Maps Cardholders to CardSecrets.

          A CardSecret of 0 means no cerificate, must use unsigned format.*}

     PANSecret :: "nat => nat"

      --{*Maps Cardholders to PANSecrets.*}

 inductive_set

   set_pur :: "event list set"

 where

   Nil:   --{*Initial trace is empty*}

          "[] \<in> set_pur"

 | Fake:  --{*The spy MAY say anything he CAN say.*}

          "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]

           ==> Says Spy B X  # evsf \<in> set_pur"

 | Reception: --{*If A sends a message X to B, then B might receive it*}

              "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]

               ==> Gets B X  # evsr \<in> set_pur"

 | Start: 

       --{*Added start event which is out-of-band for SET: the Cardholder and

           the merchant agree on the amounts and uses @{text LID_M} as an

           identifier.

           This is suggested by the External Interface Guide. The Programmer's

           Guide, in absence of @{text LID_M}, states that the merchant uniquely

           identifies the order out of some data contained in OrderDesc.*}

    "[|evsStart \<in> set_pur;

       Number LID_M \<notin> used evsStart;

       C = Cardholder k; M = Merchant i; P = PG j;

       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

       LID_M \<notin> range CardSecret;

       LID_M \<notin> range PANSecret |]

      ==> Notes C {|Number LID_M, Transaction|}

        # Notes M {|Number LID_M, Agent P, Transaction|}

        # evsStart \<in> set_pur"

 | PInitReq:

      --{*Purchase initialization, page 72 of Formal Protocol Desc.*}

    "[|evsPIReq \<in> set_pur;

       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

       Nonce Chall_C \<notin> used evsPIReq;

       Chall_C \<notin> range CardSecret; Chall_C \<notin> range PANSecret;

       Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]

     ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"

 | PInitRes:

      --{*Merchant replies with his own label XID and the encryption

          key certificate of his chosen Payment Gateway. Page 74 of Formal

          Protocol Desc. We use @{text LID_M} to identify Cardholder*}

    "[|evsPIRes \<in> set_pur;

       Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPIRes;

       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

       Notes M {|Number LID_M, Agent P, Transaction|} \<in> set evsPIRes;

       Nonce Chall_M \<notin> used evsPIRes;

       Chall_M \<notin> range CardSecret; Chall_M \<notin> range PANSecret;

       Number XID \<notin> used evsPIRes;

       XID \<notin> range CardSecret; XID \<notin> range PANSecret|]

     ==> Says M C (sign (priSK M)

                        {|Number LID_M, Number XID,

                          Nonce Chall_C, Nonce Chall_M,

                          cert P (pubEK P) onlyEnc (priSK RCA)|})

           # evsPIRes \<in> set_pur"

 | PReqUns:

       --{*UNSIGNED Purchase request (CardSecret = 0).

         Page 79 of Formal Protocol Desc.

         Merchant never sees the amount in clear. This holds of the real

         protocol, where XID identifies the transaction. We omit

         Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because

         the CardSecret is 0 and because AuthReq treated the unsigned case

         very differently from the signed one anyway.*}

    "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.

     [|evsPReqU \<in> set_pur;

       C = Cardholder k; CardSecret k = 0;

       Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;

       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

       HOD = Hash{|Number OrderDesc, Number PurchAmt|};

       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,Nonce Chall_M|};

       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};

       Gets C (sign (priSK M)

                    {|Number LID_M, Number XID,

                      Nonce Chall_C, Nonce Chall_M,

                      cert P EKj onlyEnc (priSK RCA)|})

         \<in> set evsPReqU;

       Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqU;

       Notes C {|Number LID_M, Transaction|} \<in> set evsPReqU |]

     ==> Says C M

              {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),

                OIData, Hash{|PIHead, Pan (pan C)|} |}

           # Notes C {|Key KC1, Agent M|}

           # evsPReqU \<in> set_pur"

 | PReqS:

       --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.

           We could specify the equation

           @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the

           Formal Desc. gives PIHead the same format in the unsigned case.

           However, there's little point, as P treats the signed and 

           unsigned cases differently.*}

    "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData

       OIDualSigned OrderDesc P PANData PIData PIDualSigned

       PIHead PurchAmt Transaction XID evsPReqS k.

     [|evsPReqS \<in> set_pur;

       C = Cardholder k;

       CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;

       Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

       HOD = Hash{|Number OrderDesc, Number PurchAmt|};

       OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, Nonce Chall_M|};

       PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,

                   Hash{|Number XID, Nonce (CardSecret k)|}|};

       PANData = {|Pan (pan C), Nonce (PANSecret k)|};

       PIData = {|PIHead, PANData|};

       PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|},

                        EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|};

       OIDualSigned = {|OIData, Hash PIData|};

       Gets C (sign (priSK M)

                    {|Number LID_M, Number XID,

                      Nonce Chall_C, Nonce Chall_M,

                      cert P EKj onlyEnc (priSK RCA)|})

         \<in> set evsPReqS;

       Says C M {|Number LID_M, Nonce Chall_C|} \<in> set evsPReqS;

       Notes C {|Number LID_M, Transaction|} \<in> set evsPReqS |]

     ==> Says C M {|PIDualSigned, OIDualSigned|}

           # Notes C {|Key KC2, Agent M|}

           # evsPReqS \<in> set_pur"

   --{*Authorization Request.  Page 92 of Formal Protocol Desc.

     Sent in response to Purchase Request.*}

 | AuthReq:

    "[| evsAReq \<in> set_pur;

        Key KM \<notin> used evsAReq;  KM \<in> symKeys;

        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

        HOD = Hash{|Number OrderDesc, Number PurchAmt|};

        OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD,

                   Nonce Chall_M|};

        CardSecret k \<noteq> 0 -->

          P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};

        Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq;

        Says M C (sign (priSK M) {|Number LID_M, Number XID,

                                   Nonce Chall_C, Nonce Chall_M,

                                   cert P EKj onlyEnc (priSK RCA)|})

          \<in> set evsAReq;

         Notes M {|Number LID_M, Agent P, Transaction|}

            \<in> set evsAReq |]

     ==> Says M P

              (EncB (priSK M) KM (pubEK P)

                {|Number LID_M, Number XID, Hash OIData, HOD|}   P_I)

           # evsAReq \<in> set_pur"

   --{*Authorization Response has two forms: for UNSIGNED and SIGNED PIs.

     Page 99 of Formal Protocol Desc.

     PI is a keyword (product!), so we call it @{text P_I}. The hashes HOD and

     HOIData occur independently in @{text P_I} and in M's message.

     The authCode in AuthRes represents the baggage of EncB, which in the

     full protocol is [CapToken], [AcqCardMsg], [AuthToken]:

     optional items for split shipments, recurring payments, etc.*}

 | AuthResUns:

     --{*Authorization Response, UNSIGNED*}

    "[| evsAResU \<in> set_pur;

        C = Cardholder k; M = Merchant i;

        Key KP \<notin> used evsAResU;  KP \<in> symKeys;

        CardSecret k = 0;  KC1 \<in> symKeys;  KM \<in> symKeys;

        PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M|};

        P_I = EXHcrypt KC1 EKj {|PIHead, HOIData|} (Pan (pan C));

        Gets P (EncB (priSK M) KM (pubEK P)

                {|Number LID_M, Number XID, HOIData, HOD|} P_I)

            \<in> set evsAResU |]

    ==> Says P M

             (EncB (priSK P) KP (pubEK M)

               {|Number LID_M, Number XID, Number PurchAmt|}

               authCode)

        # evsAResU \<in> set_pur"

 | AuthResS:

     --{*Authorization Response, SIGNED*}

    "[| evsAResS \<in> set_pur;

        C = Cardholder k;

        Key KP \<notin> used evsAResS;  KP \<in> symKeys;

        CardSecret k \<noteq> 0;  KC2 \<in> symKeys;  KM \<in> symKeys;

        P_I = {|sign (priSK C) {|Hash PIData, HOIData|},

                EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|};

        PANData = {|Pan (pan C), Nonce (PANSecret k)|};

        PIData = {|PIHead, PANData|};

        PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,

                   Hash{|Number XID, Nonce (CardSecret k)|}|};

        Gets P (EncB (priSK M) KM (pubEK P)

                 {|Number LID_M, Number XID, HOIData, HOD|}

                P_I)

            \<in> set evsAResS |]

    ==> Says P M

             (EncB (priSK P) KP (pubEK M)

               {|Number LID_M, Number XID, Number PurchAmt|}

               authCode)

        # evsAResS \<in> set_pur"

 | PRes:

     --{*Purchase response.*}

    "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;

        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};

        Gets M (EncB (priSK P) KP (pubEK M)

               {|Number LID_M, Number XID, Number PurchAmt|}

               authCode)

           \<in> set evsPRes;

        Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes;

        Says M P

             (EncB (priSK M) KM (pubEK P)

               {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)

          \<in> set evsPRes;

        Notes M {|Number LID_M, Agent P, Transaction|}

           \<in> set evsPRes

       |]

    ==> Says M C

          (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,

                            Hash (Number PurchAmt)|})

          # evsPRes \<in> set_pur"

 specification (CardSecret PANSecret)

   inj_CardSecret:  "inj CardSecret"

   inj_PANSecret:   "inj PANSecret"

   CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"

     --{*No CardSecret equals any PANSecret*}

   apply (rule_tac x="curry prod_encode 0" in exI)

   apply (rule_tac x="curry prod_encode 1" in exI)

   apply (simp add: prod_encode_eq inj_on_def)

   done

 declare Says_imp_knows_Spy [THEN parts.Inj, dest]

 declare parts.Body [dest]

 declare analz_into_parts [dest]

 declare Fake_parts_insert_in_Un [dest]

 declare CardSecret_neq_PANSecret [iff] 

         CardSecret_neq_PANSecret [THEN not_sym, iff]

 declare inj_CardSecret [THEN inj_eq, iff] 

         inj_PANSecret [THEN inj_eq, iff]

 subsection{*Possibility Properties*}

 lemma Says_to_Gets:

      "Says A B X # evs \<in> set_pur ==> Gets B X # Says A B X # evs \<in> set_pur"

 by (rule set_pur.Reception, auto)

 text{*Possibility for UNSIGNED purchases. Note that we need to ensure

 that XID differs from OrderDesc and PurchAmt, since it is supposed to be

 a unique number!*}

 lemma possibility_Uns:

     "[| CardSecret k = 0;

         C = Cardholder k;  M = Merchant i;

         Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 

         KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 

         KC < KM; KM < KP;

         Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;

         Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;

         Chall_C < Chall_M; 

         Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;

         Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;

         LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 

    ==> \<exists>evs \<in> set_pur.

           Says M C

                (sign (priSK M)

                     {|Number LID_M, Number XID, Nonce Chall_C, 

                       Hash (Number PurchAmt)|})

                   \<in> set evs" 

 apply (intro exI bexI)

 apply (rule_tac [2]

         set_pur.Nil

          [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 

           THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],

           THEN Says_to_Gets, 

           THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 

           THEN Says_to_Gets,

           THEN set_pur.PReqUns [of concl: C M KC],

           THEN Says_to_Gets, 

           THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 

           THEN Says_to_Gets, 

           THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID],

           THEN Says_to_Gets, 

           THEN set_pur.PRes]) 

 apply basic_possibility

 apply (simp_all add: used_Cons symKeys_neq_imp_neq) 

 done

 lemma possibility_S:

     "[| CardSecret k \<noteq> 0;

         C = Cardholder k;  M = Merchant i;

         Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 

         KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 

         KC < KM; KM < KP;

         Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret;

         Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret;

         Chall_C < Chall_M; 

         Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret;

         Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret;

         LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] 

    ==>  \<exists>evs \<in> set_pur.

             Says M C

                  (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, 

                                    Hash (Number PurchAmt)|})

                \<in> set evs"

 apply (intro exI bexI)

 apply (rule_tac [2]

         set_pur.Nil

          [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 

           THEN set_pur.PInitReq [of concl: C M LID_M Chall_C],

           THEN Says_to_Gets, 

           THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 

           THEN Says_to_Gets,

           THEN set_pur.PReqS [of concl: C M _ _ KC],

           THEN Says_to_Gets, 

           THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 

           THEN Says_to_Gets, 

           THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID],

           THEN Says_to_Gets, 

           THEN set_pur.PRes]) 

 apply basic_possibility

 apply (auto simp add: used_Cons symKeys_neq_imp_neq) 

 done

 text{*General facts about message reception*}

 lemma Gets_imp_Says:

      "[| Gets B X \<in> set evs; evs \<in> set_pur |]

    ==> \<exists>A. Says A B X \<in> set evs"

 apply (erule rev_mp)

 apply (erule set_pur.induct, auto)

 done

 lemma Gets_imp_knows_Spy:

      "[| Gets B X \<in> set evs; evs \<in> set_pur |]  ==> X \<in> knows Spy evs"

 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)

 declare Gets_imp_knows_Spy [THEN parts.Inj, dest]

 text{*Forwarding lemmas, to aid simplification*}

 lemma AuthReq_msg_in_parts_spies:

      "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;

         evs \<in> set_pur|] ==> P_I \<in> parts (knows Spy evs)"

 by auto

 lemma AuthReq_msg_in_analz_spies:

      "[|Gets M {|P_I, OIData, HPIData|} \<in> set evs;

         evs \<in> set_pur|] ==> P_I \<in> analz (knows Spy evs)"

 by (blast dest: Gets_imp_knows_Spy [THEN analz.Inj])

 subsection{*Proofs on Asymmetric Keys*}

 text{*Private Keys are Secret*}

 text{*Spy never sees an agent's private keys! (unless it's bad at start)*}

 lemma Spy_see_private_Key [simp]:

      "evs \<in> set_pur

       ==> (Key(invKey (publicKey b A)) \<in> parts(knows Spy evs)) = (A \<in> bad)"

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply auto

 done

 declare Spy_see_private_Key [THEN [2] rev_iffD1, dest!]

 lemma Spy_analz_private_Key [simp]:

      "evs \<in> set_pur ==>

      (Key(invKey (publicKey b A)) \<in> analz(knows Spy evs)) = (A \<in> bad)"

 by auto

 declare Spy_analz_private_Key [THEN [2] rev_iffD1, dest!]

 text{*rewriting rule for priEK's*}

 lemma parts_image_priEK:

      "[|Key (priEK C) \<in> parts (Key`KK Un (knows Spy evs));

         evs \<in> set_pur|] ==> priEK C \<in> KK | C \<in> bad"

 by auto

 text{*trivial proof because @{term"priEK C"} never appears even in

   @{term "parts evs"}. *}

 lemma analz_image_priEK:

      "evs \<in> set_pur ==>

           (Key (priEK C) \<in> analz (Key`KK Un (knows Spy evs))) =

           (priEK C \<in> KK | C \<in> bad)"

 by (blast dest!: parts_image_priEK intro: analz_mono [THEN [2] rev_subsetD])

 subsection{*Public Keys in Certificates are Correct*}

 lemma Crypt_valid_pubEK [dest!]:

      "[| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|}

            \<in> parts (knows Spy evs);

          evs \<in> set_pur |] ==> EKi = pubEK C"

 by (erule rev_mp, erule set_pur.induct, auto)

 lemma Crypt_valid_pubSK [dest!]:

      "[| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|}

            \<in> parts (knows Spy evs);

          evs \<in> set_pur |] ==> SKi = pubSK C"

 by (erule rev_mp, erule set_pur.induct, auto)

 lemma certificate_valid_pubEK:

     "[| cert C EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs);

         evs \<in> set_pur |]

      ==> EKi = pubEK C"

 by (unfold cert_def signCert_def, auto)

 lemma certificate_valid_pubSK:

     "[| cert C SKi onlySig (priSK RCA) \<in> parts (knows Spy evs);

         evs \<in> set_pur |] ==> SKi = pubSK C"

 by (unfold cert_def signCert_def, auto)

 lemma Says_certificate_valid [simp]:

      "[| Says A B (sign SK {|lid, xid, cc, cm,

                            cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;

          evs \<in> set_pur |]

       ==> EK = pubEK C"

 by (unfold sign_def, auto)

 lemma Gets_certificate_valid [simp]:

      "[| Gets A (sign SK {|lid, xid, cc, cm,

                            cert C EK onlyEnc (priSK RCA)|}) \<in> set evs;

          evs \<in> set_pur |]

       ==> EK = pubEK C"

 by (frule Gets_imp_Says, auto)

 method_setup valid_certificate_tac = {*

   Args.goal_spec >> (fn quant =>

     fn ctxt => SIMPLE_METHOD'' quant (fn i =>

       EVERY [ftac @{thm Gets_certificate_valid} i,

              assume_tac i, REPEAT (hyp_subst_tac ctxt i)]))

 *}

 subsection{*Proofs on Symmetric Keys*}

 text{*Nobody can have used non-existent keys!*}

 lemma new_keys_not_used [rule_format,simp]:

      "evs \<in> set_pur

       ==> Key K \<notin> used evs --> K \<in> symKeys -->

           K \<notin> keysFor (parts (knows Spy evs))"

 apply (erule set_pur.induct)

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply auto

 apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}

 done

 lemma new_keys_not_analzd:

      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]

       ==> K \<notin> keysFor (analz (knows Spy evs))"

 by (blast intro: keysFor_mono [THEN [2] rev_subsetD] dest: new_keys_not_used)

 lemma Crypt_parts_imp_used:

      "[|Crypt K X \<in> parts (knows Spy evs);

         K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"

 apply (rule ccontr)

 apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor)

 done

 lemma Crypt_analz_imp_used:

      "[|Crypt K X \<in> analz (knows Spy evs);

         K \<in> symKeys; evs \<in> set_pur |] ==> Key K \<in> used evs"

 by (blast intro: Crypt_parts_imp_used)

 text{*New versions: as above, but generalized to have the KK argument*}

 lemma gen_new_keys_not_used:

      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]

       ==> Key K \<notin> used evs --> K \<in> symKeys -->

           K \<notin> keysFor (parts (Key`KK Un knows Spy evs))"

 by auto

 lemma gen_new_keys_not_analzd:

      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]

       ==> K \<notin> keysFor (analz (Key`KK Un knows Spy evs))"

 by (blast intro: keysFor_mono [THEN subsetD] dest: gen_new_keys_not_used)

 lemma analz_Key_image_insert_eq:

      "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_pur |]

       ==> analz (Key ` (insert K KK) \<union> knows Spy evs) =

           insert (Key K) (analz (Key ` KK \<union> knows Spy evs))"

 by (simp add: gen_new_keys_not_analzd)

 subsection{*Secrecy of Symmetric Keys*}

 lemma Key_analz_image_Key_lemma:

      "P --> (Key K \<in> analz (Key`KK Un H)) --> (K\<in>KK | Key K \<in> analz H)

       ==>

       P --> (Key K \<in> analz (Key`KK Un H)) = (K\<in>KK | Key K \<in> analz H)"

 by (blast intro: analz_mono [THEN [2] rev_subsetD])

 lemma symKey_compromise:

      "evs \<in> set_pur \<Longrightarrow>

       (\<forall>SK KK. SK \<in> symKeys \<longrightarrow>

         (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow>

                (Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) =

                (SK \<in> KK \<or> Key SK \<in> analz (knows Spy evs)))"

 apply (erule set_pur.induct)

 apply (rule_tac [!] allI)+

 apply (rule_tac [!] impI [THEN Key_analz_image_Key_lemma, THEN impI])+

 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps disj_simps

               analz_Key_image_insert_eq notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*8 seconds on a 1.6GHz machine*}

 apply spy_analz --{*Fake*}

 apply (blast elim!: ballE)+ --{*PReq: unsigned and signed*}

 done

 subsection{*Secrecy of Nonces*}

 text{*As usual: we express the property as a logical equivalence*}

 lemma Nonce_analz_image_Key_lemma:

      "P --> (Nonce N \<in> analz (Key`KK Un H)) --> (Nonce N \<in> analz H)

       ==> P --> (Nonce N \<in> analz (Key`KK Un H)) = (Nonce N \<in> analz H)"

 by (blast intro: analz_mono [THEN [2] rev_subsetD])

 text{*The @{text "(no_asm)"} attribute is essential, since it retains

   the quantifier and allows the simprule's condition to itself be simplified.*}

 lemma Nonce_compromise [rule_format (no_asm)]:

      "evs \<in> set_pur ==>

       (\<forall>N KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C))   -->

               (Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) =

               (Nonce N \<in> analz (knows Spy evs)))"

 apply (erule set_pur.induct)

 apply (rule_tac [!] allI)+

 apply (rule_tac [!] impI [THEN Nonce_analz_image_Key_lemma])+

 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps disj_simps symKey_compromise

               analz_Key_image_insert_eq notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*8 seconds on a 1.6GHz machine*}

 apply spy_analz --{*Fake*}

 apply (blast elim!: ballE) --{*PReqS*}

 done

 lemma PANSecret_notin_spies:

      "[|Nonce (PANSecret k) \<in> analz (knows Spy evs);  evs \<in> set_pur|]

       ==> 

        (\<exists>V W X Y KC2 M. \<exists>P \<in> bad.

           Says (Cardholder k) M

                {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},

                  V|}  \<in>  set evs)"

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_analz_spies)

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps disj_simps

               symKey_compromise pushes sign_def Nonce_compromise

               analz_Key_image_insert_eq notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*2.5 seconds on a 1.6GHz machine*}

 apply spy_analz

 apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])

 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 

                    Gets_imp_knows_Spy [THEN analz.Inj])

 apply (blast dest: Gets_imp_knows_Spy [THEN analz.Inj]) --{*PReqS*}

 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] 

                    Gets_imp_knows_Spy [THEN analz.Inj]) --{*PRes*}

 done

 text{*This theorem is a bit silly, in that many CardSecrets are 0!

   But then we don't care.  NOT USED*}

 lemma CardSecret_notin_spies:

      "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"

 by (erule set_pur.induct, auto)

 subsection{*Confidentiality of PAN*}

 lemma analz_image_pan_lemma:

      "(Pan P \<in> analz (Key`nE Un H)) --> (Pan P \<in> analz H)  ==>

       (Pan P \<in> analz (Key`nE Un H)) =   (Pan P \<in> analz H)"

 by (blast intro: analz_mono [THEN [2] rev_subsetD])

 text{*The @{text "(no_asm)"} attribute is essential, since it retains

   the quantifier and allows the simprule's condition to itself be simplified.*}

 lemma analz_image_pan [rule_format (no_asm)]:

      "evs \<in> set_pur ==>

        \<forall>KK. (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) -->

             (Pan P \<in> analz (Key`KK Un (knows Spy evs))) =

             (Pan P \<in> analz (knows Spy evs))"

 apply (erule set_pur.induct)

 apply (rule_tac [!] allI impI)+

 apply (rule_tac [!] analz_image_pan_lemma)+

 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps

               symKey_compromise pushes sign_def

               analz_Key_image_insert_eq notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*7 seconds on a 1.6GHz machine*}

 apply spy_analz --{*Fake*}

 apply auto

 done

 lemma analz_insert_pan:

      "[| evs \<in> set_pur;  K \<notin> range(\<lambda>C. priEK C) |] ==>

           (Pan P \<in> analz (insert (Key K) (knows Spy evs))) =

           (Pan P \<in> analz (knows Spy evs))"

 by (simp del: image_insert image_Un

          add: analz_image_keys_simps analz_image_pan)

 text{*Confidentiality of the PAN, unsigned case.*}

 theorem pan_confidentiality_unsigned:

      "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;

          CardSecret k = 0;  evs \<in> set_pur|]

     ==> \<exists>P M KC1 K X Y.

      Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}

           \<in> set evs  &

      P \<in> bad"

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps analz_insert_pan analz_image_pan

               notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*3 seconds on a 1.6GHz machine*}

 apply spy_analz --{*Fake*}

 apply blast --{*PReqUns: unsigned*}

 apply force --{*PReqS: signed*}

 done

 text{*Confidentiality of the PAN, signed case.*}

 theorem pan_confidentiality_signed:

  "[|Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;

     CardSecret k \<noteq> 0;  evs \<in> set_pur|]

   ==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.

       Says C M {|{|PIDualSign_1, 

                    EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, 

        OIDualSign|} \<in> set evs  &  P \<in> bad"

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}

 apply (valid_certificate_tac [8]) --{*PReqS*}

 apply (valid_certificate_tac [7]) --{*PReqUns*}

 apply (simp_all

          del: image_insert image_Un imp_disjL

          add: analz_image_keys_simps analz_insert_pan analz_image_pan

               notin_image_iff

               analz_insert_simps analz_image_priEK)

   --{*3 seconds on a 1.6GHz machine*}

 apply spy_analz --{*Fake*}

 apply force --{*PReqUns: unsigned*}

 apply blast --{*PReqS: signed*}

 done

 text{*General goal: that C, M and PG agree on those details of the transaction

      that they are allowed to know about.  PG knows about price and account

      details.  M knows about the order description and price.  C knows both.*}

 subsection{*Proofs Common to Signed and Unsigned Versions*}

 lemma M_Notes_PG:

      "[|Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} \<in> set evs;

         evs \<in> set_pur|] ==> \<exists>j. P = PG j"

 by (erule rev_mp, erule set_pur.induct, simp_all)

 text{*If we trust M, then @{term LID_M} determines his choice of P

       (Payment Gateway)*}

 lemma goodM_gives_correct_PG:

      "[| MsgPInitRes = 

             {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};

          Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);

          evs \<in> set_pur; M \<notin> bad |]

       ==> \<exists>j trans.

             P = PG j &

             Notes M {|Number LID_M, Agent P, trans|} \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply (blast intro: M_Notes_PG)+

 done

 lemma C_gets_correct_PG:

      "[| Gets A (sign (priSK M) {|Number LID_M, xid, cc, cm,

                               cert P EKj onlyEnc (priSK RCA)|}) \<in> set evs;

          evs \<in> set_pur;  M \<notin> bad|]

       ==> \<exists>j trans.

             P = PG j &

             Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &

             EKj = pubEK P"

 by (rule refl [THEN goodM_gives_correct_PG, THEN exE], auto)

 text{*When C receives PInitRes, he learns M's choice of P*}

 lemma C_verifies_PInitRes:

  "[| MsgPInitRes = {|Number LID_M, Number XID, Nonce Chall_C, Nonce Chall_M,

            cert P EKj onlyEnc (priSK RCA)|};

      Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs);

      evs \<in> set_pur;  M \<notin> bad|]

   ==> \<exists>j trans.

          Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &

          P = PG j &

          EKj = pubEK P"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply (blast intro: M_Notes_PG)+

 done

 text{*Corollary of previous one*}

 lemma Says_C_PInitRes:

      "[|Says A C (sign (priSK M)

                       {|Number LID_M, Number XID,

                         Nonce Chall_C, Nonce Chall_M,

                         cert P EKj onlyEnc (priSK RCA)|})

            \<in> set evs;  M \<notin> bad;  evs \<in> set_pur|]

       ==> \<exists>j trans.

            Notes M {|Number LID_M, Agent P, trans|} \<in> set evs &

            P = PG j &

            EKj = pubEK (PG j)"

 apply (frule Says_certificate_valid)

 apply (auto simp add: sign_def)

 apply (blast dest: refl [THEN goodM_gives_correct_PG])

 apply (blast dest: refl [THEN C_verifies_PInitRes])

 done

 text{*When P receives an AuthReq, he knows that the signed part originated 

       with M. PIRes also has a signed message from M....*}

 lemma P_verifies_AuthReq:

      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};

          Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|})

            \<in> parts (knows Spy evs);

          evs \<in> set_pur;  M \<notin> bad|]

       ==> \<exists>j trans KM OIData HPIData.

             Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &

             Gets M {|P_I, OIData, HPIData|} \<in> set evs &

             Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)

               \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)

 apply (frule_tac [4] M_Notes_PG, auto)

 done

 text{*When M receives AuthRes, he knows that P signed it, including

   the identifying tags and the purchase amount, which he can verify.

   (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they

    send the same message to M.)  The conclusion is weak: M is existentially

   quantified! That is because Authorization Response does not refer to M, while

   the digital envelope weakens the link between @{term MsgAuthRes} and

   @{term"priSK M"}.  Changing the precondition to refer to 

   @{term "Crypt K (sign SK M)"} requires assuming @{term K} to be secure, since

   otherwise the Spy could create that message.*}

 theorem M_verifies_AuthRes:

   "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, 

                      Hash authCode|};

       Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);

       PG j \<notin> bad;  evs \<in> set_pur|]

    ==> \<exists>M KM KP HOIData HOD P_I.

         Gets (PG j)

            (EncB (priSK M) KM (pubEK (PG j))

                     {|Number LID_M, Number XID, HOIData, HOD|}

                     P_I) \<in> set evs &

         Says (PG j) M

              (EncB (priSK (PG j)) KP (pubEK M)

               {|Number LID_M, Number XID, Number PurchAmt|}

               authCode) \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply blast+

 done

 subsection{*Proofs for Unsigned Purchases*}

 text{*What we can derive from the ASSUMPTION that C issued a purchase request.

    In the unsigned case, we must trust "C": there's no authentication.*}

 lemma C_determines_EKj:

      "[| Says C M {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)),

                     OIData, Hash{|PIHead, Pan (pan C)|} |} \<in> set evs;

          PIHead = {|Number LID_M, Trans_details|};

          evs \<in> set_pur;  C = Cardholder k;  M \<notin> bad|]

   ==> \<exists>trans j.

                Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &

                EKj = pubEK (PG j)"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)

 apply (valid_certificate_tac [2]) --{*PReqUns*}

 apply auto

 apply (blast dest: Gets_imp_Says Says_C_PInitRes)

 done

 text{*Unicity of @{term LID_M} between Merchant and Cardholder notes*}

 lemma unique_LID_M:

      "[|Notes (Merchant i) {|Number LID_M, Agent P, Trans|} \<in> set evs;

         Notes C {|Number LID_M, Agent M, Agent C, Number OD,

              Number PA|} \<in> set evs;

         evs \<in> set_pur|]

       ==> M = Merchant i & Trans = {|Agent M, Agent C, Number OD, Number PA|}"

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)

 apply (force dest!: Notes_imp_parts_subset_used)

 done

 text{*Unicity of @{term LID_M}, for two Merchant Notes events*}

 lemma unique_LID_M2:

      "[|Notes M {|Number LID_M, Trans|} \<in> set evs;

         Notes M {|Number LID_M, Trans'|} \<in> set evs;

         evs \<in> set_pur|] ==> Trans' = Trans"

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)

 apply (force dest!: Notes_imp_parts_subset_used)

 done

 text{*Lemma needed below: for the case that

   if PRes is present, then @{term LID_M} has been used.*}

 lemma signed_imp_used:

      "[| Crypt (priSK M) (Hash X) \<in> parts (knows Spy evs);

          M \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply safe

 apply blast+

 done

 text{*Similar, with nested Hash*}

 lemma signed_Hash_imp_used:

      "[| Crypt (priSK C) (Hash {|H, Hash X|}) \<in> parts (knows Spy evs);

          C \<notin> bad;  evs \<in> set_pur|] ==> parts {X} \<subseteq> used evs"

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply safe

 apply blast+

 done

 text{*Lemma needed below: for the case that

   if PRes is present, then @{text LID_M} has been used.*}

 lemma PRes_imp_LID_used:

      "[| Crypt (priSK M) (Hash {|N, X|}) \<in> parts (knows Spy evs);

          M \<notin> bad;  evs \<in> set_pur|] ==> N \<in> used evs"

 by (drule signed_imp_used, auto)

 text{*When C receives PRes, he knows that M and P agreed to the purchase details.

   He also knows that P is the same PG as before*}

 lemma C_verifies_PRes_lemma:

      "[| Crypt (priSK M) (Hash MsgPRes) \<in> parts (knows Spy evs);

          Notes C {|Number LID_M, Trans |} \<in> set evs;

          Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};

          MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,

                 Hash (Number PurchAmt)|};

          evs \<in> set_pur;  M \<notin> bad|]

   ==> \<exists>j KP.

         Notes M {|Number LID_M, Agent (PG j), Trans |}

           \<in> set evs &

         Gets M (EncB (priSK (PG j)) KP (pubEK M)

                 {|Number LID_M, Number XID, Number PurchAmt|}

                 authCode)

           \<in> set evs &

         Says M C (sign (priSK M) MsgPRes) \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply blast

 apply blast

 apply (blast dest: PRes_imp_LID_used)

 apply (frule M_Notes_PG, auto)

 apply (blast dest: unique_LID_M)

 done

 text{*When the Cardholder receives Purchase Response from an uncompromised

 Merchant, he knows that M sent it. He also knows that M received a message signed

 by a Payment Gateway chosen by M to authorize the purchase.*}

 theorem C_verifies_PRes:

      "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,

                      Hash (Number PurchAmt)|};

          Gets C (sign (priSK M) MsgPRes) \<in> set evs;

          Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,

                    Number PurchAmt|} \<in> set evs;

          evs \<in> set_pur;  M \<notin> bad|]

   ==> \<exists>P KP trans.

         Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &

         Gets M (EncB (priSK P) KP (pubEK M)

                 {|Number LID_M, Number XID, Number PurchAmt|}

                 authCode)  \<in>  set evs &

         Says M C (sign (priSK M) MsgPRes) \<in> set evs"

 apply (rule C_verifies_PRes_lemma [THEN exE])

 apply (auto simp add: sign_def)

 done

 subsection{*Proofs for Signed Purchases*}

 text{*Some Useful Lemmas: the cardholder knows what he is doing*}

 lemma Crypt_imp_Says_Cardholder:

      "[| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}

            \<in> parts (knows Spy evs);

          PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};

          Key K \<notin> analz (knows Spy evs);

          evs \<in> set_pur|]

   ==> \<exists>M shash EK HPIData.

        Says (Cardholder k) M {|{|shash,

           Crypt K

             {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|},

            Crypt EK {|Key K, PANData|}|},

           OIData, HPIData|} \<in> set evs"

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct, analz_mono_contra)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply auto

 done

 lemma Says_PReqS_imp_trans_details_C:

      "[| MsgPReqS = {|{|shash,

                  Crypt K

                   {|{|{|Number LID_M, PIrest|}, Hash OIData|}, hashpd|},

             cryptek|}, data|};

          Says (Cardholder k) M MsgPReqS \<in> set evs;

          evs \<in> set_pur |]

    ==> \<exists>trans.

            Notes (Cardholder k) 

                  {|Number LID_M, Agent M, Agent (Cardholder k), trans|}

             \<in> set evs"

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (simp_all (no_asm_simp))

 apply auto

 done

 text{*Can't happen: only Merchants create this type of Note*}

 lemma Notes_Cardholder_self_False:

      "[|Notes (Cardholder k)

           {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|} \<in> set evs;

         evs \<in> set_pur|] ==> False"

 by (erule rev_mp, erule set_pur.induct, auto)

 text{*When M sees a dual signature, he knows that it originated with C.

   Using XID he knows it was intended for him.

   This guarantee isn't useful to P, who never gets OIData.*}

 theorem M_verifies_Signed_PReq:

  "[| MsgDualSign = {|HPIData, Hash OIData|};

      OIData = {|Number LID_M, etc|};

      Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);

      Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;

      M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]

   ==> \<exists>PIData PICrypt.

         HPIData = Hash PIData &

         Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}

           \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct)

 apply (frule_tac [9] AuthReq_msg_in_parts_spies) --{*AuthReq*}

 apply simp_all

 apply blast

 apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used)

 apply (metis unique_LID_M)

 apply (blast dest!: Notes_Cardholder_self_False)

 done

 text{*When P sees a dual signature, he knows that it originated with C.

   and was intended for M. This guarantee isn't useful to M, who never gets

   PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without

   assuming @{term "M \<notin> bad"}.*}

 theorem P_verifies_Signed_PReq:

      "[| MsgDualSign = {|Hash PIData, HOIData|};

          PIData = {|PIHead, PANData|};

          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,

                     TransStain|};

          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);

          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]

     ==> \<exists>OIData OrderDesc K j trans.

           HOD = Hash{|Number OrderDesc, Number PurchAmt|} &

           HOIData = Hash OIData &

           Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &

           Says C M {|{|sign (priSK C) MsgDualSign,

                      EXcrypt K (pubEK (PG j))

                                 {|PIHead, Hash OIData|} PANData|},

                      OIData, Hash PIData|}

             \<in> set evs"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all)

 apply (auto dest!: C_gets_correct_PG)

 done

 lemma C_determines_EKj_signed:

      "[| Says C M {|{|sign (priSK C) text,

                       EXcrypt K EKj {|PIHead, X|} Y|}, Z|} \<in> set evs;

          PIHead = {|Number LID_M, Number XID, W|};

          C = Cardholder k;  evs \<in> set_pur;  M \<notin> bad|]

   ==> \<exists> trans j.

          Notes M {|Number LID_M, Agent (PG j), trans|} \<in> set evs &

          EKj = pubEK (PG j)"

 apply clarify

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all, auto)

 apply (blast dest: C_gets_correct_PG)

 done

 lemma M_Says_AuthReq:

      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};

          sign (priSK M) {|AuthReqData, Hash P_I|} \<in> parts (knows Spy evs);

          evs \<in> set_pur;  M \<notin> bad|]

    ==> \<exists>j trans KM.

            Notes M {|Number LID_M, Agent (PG j), trans |} \<in> set evs &

              Says M (PG j)

                (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)

               \<in> set evs"

 apply (rule refl [THEN P_verifies_AuthReq, THEN exE])

 apply (auto simp add: sign_def)

 done

 text{*A variant of @{text M_verifies_Signed_PReq} with explicit PI information.

   Even here we cannot be certain about what C sent to M, since a bad

   PG could have replaced the two key fields.  (NOT USED)*}

 lemma Signed_PReq_imp_Says_Cardholder:

      "[| MsgDualSign = {|Hash PIData, Hash OIData|};

          OIData = {|Number LID_M, Number XID, Nonce Chall_C, HOD, etc|};

          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,

                     TransStain|};

          PIData = {|PIHead, PANData|};

          Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);

          M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]

       ==> \<exists>KC EKj.

             Says C M {|{|sign (priSK C) MsgDualSign,

                        EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},

                        OIData, Hash PIData|}

               \<in> set evs"

 apply clarify

 apply hypsubst_thin

 apply (erule rev_mp)

 apply (erule rev_mp)

 apply (erule set_pur.induct, simp_all, auto)

 done

 text{*When P receives an AuthReq and a dual signature, he knows that C and M

   agree on the essential details.  PurchAmt however is never sent by M to

   P; instead C and M both send 

      @{term "HOD = Hash{|Number OrderDesc, Number PurchAmt|}"}

   and P compares the two copies of HOD.

   Agreement can't be proved for some things, including the symmetric keys

   used in the digital envelopes.  On the other hand, M knows the true identity

   of PG (namely j'), and sends AReq there; he can't, however, check that

   the EXcrypt involves the correct PG's key.

 *}

 theorem P_sees_CM_agreement:

      "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};

          KC \<in> symKeys;

          Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)

            \<in> set evs;

          C = Cardholder k;

          PI_sign = sign (priSK C) {|Hash PIData, HOIData|};

          P_I = {|PI_sign,

                  EXcrypt KC (pubEK (PG j)) {|PIHead, HOIData|} PANData|};

          PANData = {|Pan (pan C), Nonce (PANSecret k)|};

          PIData = {|PIHead, PANData|};

          PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,

                     TransStain|};

          evs \<in> set_pur;  C \<notin> bad;  M \<notin> bad|]

   ==> \<exists>OIData OrderDesc KM' trans j' KC' KC'' P_I' P_I''.

            HOD = Hash{|Number OrderDesc, Number PurchAmt|} &

            HOIData = Hash OIData &

            Notes M {|Number LID_M, Agent (PG j'), trans|} \<in> set evs &

            Says C M {|P_I', OIData, Hash PIData|} \<in> set evs &

            Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))

                            AuthReqData P_I'')  \<in>  set evs &

            P_I' = {|PI_sign,

              EXcrypt KC' (pubEK (PG j')) {|PIHead, Hash OIData|} PANData|} &

            P_I'' = {|PI_sign,

              EXcrypt KC'' (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|}"

 apply clarify

 apply (rule exE)

 apply (rule P_verifies_Signed_PReq [OF refl refl refl])

 apply (simp (no_asm_use) add: sign_def EncB_def, blast)

 apply (assumption+, clarify, simp)

 apply (drule Gets_imp_knows_Spy [THEN parts.Inj], assumption)

 apply (blast elim: EncB_partsE dest: refl [THEN M_Says_AuthReq] unique_LID_M2)

 done

 end