# Theory Purchase

Up to index of Isabelle/HOL/SET-Protocol

theory Purchase
imports PublicSET
begin

    (*  Title:      HOL/Auth/SET/Purchase
        ID:         $Id: Purchase.thy,v 1.8 2005/06/20 13:54:39 paulson Exp $
        Authors:    Giampaolo Bella, Fabio Massacci, Lawrence C Paulson
    *)

    header{*Purchase Phase of SET*}

    theory Purchase imports PublicSET 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.*}

        set_pur  :: "event list set"

    inductive set_pur
     intros

      Nil:   --{*Initial trace is empty*}
             "[] ∈ set_pur"

      Fake:  --{*The spy MAY say anything he CAN say.*}
             "[| evsf ∈ set_pur;  X ∈ synth(analz(knows Spy evsf)) |]
              ==> Says Spy B X  # evsf ∈ set_pur"

      Reception: --{*If A sends a message X to B, then B might receive it*}
                 "[| evsr ∈ set_pur;  Says A B X ∈ set evsr |]
                  ==> Gets B X  # evsr ∈ 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 ∈ set_pur;
          Number LID_M ∉ used evsStart;
          C = Cardholder k; M = Merchant i; P = PG j;
          Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
          LID_M ∉ range CardSecret;
          LID_M ∉ range PANSecret |]
         ==> Notes C {|Number LID_M, Transaction|}
           # Notes M {|Number LID_M, Agent P, Transaction|}
           # evsStart ∈ set_pur"

      PInitReq:
         --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
       "[|evsPIReq ∈ set_pur;
          Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
          Nonce Chall_C ∉ used evsPIReq;
          Chall_C ∉ range CardSecret; Chall_C ∉ range PANSecret;
          Notes C {|Number LID_M, Transaction |} ∈ set evsPIReq |]
        ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq ∈ 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 ∈ set_pur;
          Gets M {|Number LID_M, Nonce Chall_C|} ∈ set evsPIRes;
          Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
          Notes M {|Number LID_M, Agent P, Transaction|} ∈ set evsPIRes;
          Nonce Chall_M ∉ used evsPIRes;
          Chall_M ∉ range CardSecret; Chall_M ∉ range PANSecret;
          Number XID ∉ used evsPIRes;
          XID ∉ range CardSecret; XID ∉ 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 ∈ 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.*}
       "[|evsPReqU ∈ set_pur;
          C = Cardholder k; CardSecret k = 0;
          Key KC1 ∉ used evsPReqU;  KC1 ∈ 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)|})
            ∈ set evsPReqU;
          Says C M {|Number LID_M, Nonce Chall_C|} ∈ set evsPReqU;
          Notes C {|Number LID_M, Transaction|} ∈ 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 ∈ 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.*}
       "[|evsPReqS ∈ set_pur;
          C = Cardholder k;
          CardSecret k ≠ 0;  Key KC2 ∉ used evsPReqS;  KC2 ∈ 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)|})
            ∈ set evsPReqS;
          Says C M {|Number LID_M, Nonce Chall_C|} ∈ set evsPReqS;
          Notes C {|Number LID_M, Transaction|} ∈ set evsPReqS |]
        ==> Says C M {|PIDualSigned, OIDualSigned|}
              # Notes C {|Key KC2, Agent M|}
              # evsPReqS ∈ set_pur"

      --{*Authorization Request.  Page 92 of Formal Protocol Desc.
        Sent in response to Purchase Request.*}
      AuthReq:
       "[| evsAReq ∈ set_pur;
           Key KM ∉ used evsAReq;  KM ∈ 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 ≠ 0 -->
             P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|};
           Gets M {|P_I, OIData, HPIData|} ∈ 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)|})
             ∈ set evsAReq;
            Notes M {|Number LID_M, Agent P, Transaction|}
               ∈ set evsAReq |]
        ==> Says M P
                 (EncB (priSK M) KM (pubEK P)
                   {|Number LID_M, Number XID, Hash OIData, HOD|}   P_I)
              # evsAReq ∈ 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 ∈ set_pur;
           C = Cardholder k; M = Merchant i;
           Key KP ∉ used evsAResU;  KP ∈ symKeys;
           CardSecret k = 0;  KC1 ∈ symKeys;  KM ∈ 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)
               ∈ set evsAResU |]
       ==> Says P M
                (EncB (priSK P) KP (pubEK M)
                  {|Number LID_M, Number XID, Number PurchAmt|}
                  authCode)
           # evsAResU ∈ set_pur"

      AuthResS:
        --{*Authorization Response, SIGNED*}
       "[| evsAResS ∈ set_pur;
           C = Cardholder k;
           Key KP ∉ used evsAResS;  KP ∈ symKeys;
           CardSecret k ≠ 0;  KC2 ∈ symKeys;  KM ∈ 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)
               ∈ set evsAResS |]
       ==> Says P M
                (EncB (priSK P) KP (pubEK M)
                  {|Number LID_M, Number XID, Number PurchAmt|}
                  authCode)
           # evsAResS ∈ set_pur"

      PRes:
        --{*Purchase response.*}
       "[| evsPRes ∈ set_pur;  KP ∈ 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)
              ∈ set evsPRes;
           Gets M {|Number LID_M, Nonce Chall_C|} ∈ set evsPRes;
           Says M P
                (EncB (priSK M) KM (pubEK P)
                  {|Number LID_M, Number XID, Hash OIData, HOD|} P_I)
             ∈ set evsPRes;
           Notes M {|Number LID_M, Agent P, Transaction|}
              ∈ set evsPRes
          |]
       ==> Says M C
             (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
                               Hash (Number PurchAmt)|})
             # evsPRes ∈ set_pur"

    specification (CardSecret PANSecret)
      inj_CardSecret:  "inj CardSecret"
      inj_PANSecret:   "inj PANSecret"
      CardSecret_neq_PANSecret: "CardSecret k ≠ PANSecret k'"
        --{*No CardSecret equals any PANSecret*}
      apply (rule_tac x="curry nat2_to_nat 0" in exI)
      apply (rule_tac x="curry nat2_to_nat 1" in exI)
      apply (simp add: nat2_to_nat_inj [THEN inj_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 ∈ set_pur ==> Gets B X # Says A B X # evs ∈ 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 ∉ used []; Key KM ∉ used []; Key KP ∉ used [];
            KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys;
            KC < KM; KM < KP;
            Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret;
            Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret;
            Chall_C < Chall_M;
            Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret;
            Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret;
            LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |]
       ==> ∃evs ∈ set_pur.
              Says M C
                   (sign (priSK M)
                        {|Number LID_M, Number XID, Nonce Chall_C,
                          Hash (Number PurchAmt)|})
                      ∈ 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 (tactic "basic_possibility_tac")
    apply (simp_all add: used_Cons symKeys_neq_imp_neq)
    done

    lemma possibility_S:
        "[| CardSecret k ≠ 0;
            C = Cardholder k;  M = Merchant i;
            Key KC ∉ used []; Key KM ∉ used []; Key KP ∉ used [];
            KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys;
            KC < KM; KM < KP;
            Nonce Chall_C ∉ used []; Chall_C ∉ range CardSecret ∪ range PANSecret;
            Nonce Chall_M ∉ used []; Chall_M ∉ range CardSecret ∪ range PANSecret;
            Chall_C < Chall_M;
            Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret;
            Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret;
            LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |]
       ==>  ∃evs ∈ set_pur.
                Says M C
                     (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C,
                                       Hash (Number PurchAmt)|})
                   ∈ 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 (tactic "basic_possibility_tac")
    apply (auto simp add: used_Cons symKeys_neq_imp_neq)
    done

    text{*General facts about message reception*}
    lemma Gets_imp_Says:
         "[| Gets B X ∈ set evs; evs ∈ set_pur |]
       ==> ∃A. Says A B X ∈ set evs"
    apply (erule rev_mp)
    apply (erule set_pur.induct, auto)
    done

    lemma Gets_imp_knows_Spy:
         "[| Gets B X ∈ set evs; evs ∈ set_pur |]  ==> X ∈ 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|} ∈ set evs;
            evs ∈ set_pur|] ==> P_I ∈ parts (knows Spy evs)"
    by auto

    lemma AuthReq_msg_in_analz_spies:
         "[|Gets M {|P_I, OIData, HPIData|} ∈ set evs;
            evs ∈ set_pur|] ==> P_I ∈ 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 ∈ set_pur
          ==> (Key(invKey (publicKey b A)) ∈ parts(knows Spy evs)) = (A ∈ 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 ∈ set_pur ==>
         (Key(invKey (publicKey b A)) ∈ analz(knows Spy evs)) = (A ∈ 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) ∈ parts (Key`KK Un (knows Spy evs));
            evs ∈ set_pur|] ==> priEK C ∈ KK | C ∈ bad"
    by auto

    text{*trivial proof because @{term"priEK C"} never appears even in
      @{term "parts evs"}. *}
    lemma analz_image_priEK:
         "evs ∈ set_pur ==>
              (Key (priEK C) ∈ analz (Key`KK Un (knows Spy evs))) =
              (priEK C ∈ KK | C ∈ 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|}
               ∈ parts (knows Spy evs);
             evs ∈ 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|}
               ∈ parts (knows Spy evs);
             evs ∈ set_pur |] ==> SKi = pubSK C"
    by (erule rev_mp, erule set_pur.induct, auto)

    lemma certificate_valid_pubEK:
        "[| cert C EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs);
            evs ∈ set_pur |]
         ==> EKi = pubEK C"
    by (unfold cert_def signCert_def, auto)

    lemma certificate_valid_pubSK:
        "[| cert C SKi onlySig (priSK RCA) ∈ parts (knows Spy evs);
            evs ∈ 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)|}) ∈ set evs;
             evs ∈ 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)|}) ∈ set evs;
             evs ∈ set_pur |]
          ==> EK = pubEK C"
    by (frule Gets_imp_Says, auto)

    ML
    {*
    val Gets_certificate_valid = thm "Gets_certificate_valid";

    fun valid_certificate_tac i =
        EVERY [ftac Gets_certificate_valid i,
               assume_tac i, REPEAT (hyp_subst_tac i)];
    *}

    subsection{*Proofs on Symmetric Keys*}

    text{*Nobody can have used non-existent keys!*}
    lemma new_keys_not_used [rule_format,simp]:
         "evs ∈ set_pur
          ==> Key K ∉ used evs --> K ∈ symKeys -->
              K ∉ keysFor (parts (knows Spy evs))"
    apply (erule set_pur.induct)
    apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*valid_certificate_tac 7*}) --{*PReqUns*}
    apply auto
    apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
    done

    lemma new_keys_not_analzd:
         "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
          ==> K ∉ 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 ∈ parts (knows Spy evs);
            K ∈ symKeys; evs ∈ set_pur |] ==> Key K ∈ 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 ∈ analz (knows Spy evs);
            K ∈ symKeys; evs ∈ set_pur |] ==> Key K ∈ 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 ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
          ==> Key K ∉ used evs --> K ∈ symKeys -->
              K ∉ keysFor (parts (Key`KK Un knows Spy evs))"
    by auto

    lemma gen_new_keys_not_analzd:
         "[|Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
          ==> K ∉ 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 ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
          ==> analz (Key ` (insert K KK) ∪ knows Spy evs) =
              insert (Key K) (analz (Key ` KK ∪ 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 ∈ analz (Key`KK Un H)) --> (K∈KK | Key K ∈ analz H)
          ==>
          P --> (Key K ∈ analz (Key`KK Un H)) = (K∈KK | Key K ∈ analz H)"
    by (blast intro: analz_mono [THEN [2] rev_subsetD])

    lemma symKey_compromise:
         "evs ∈ set_pur ==>
          (∀SK KK. SK ∈ symKeys -->
            (∀K ∈ KK. K ∉ range(λC. priEK C)) -->
                   (Key SK ∈ analz (Key`KK ∪ (knows Spy evs))) =
                   (SK ∈ KK ∨ Key SK ∈ 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 (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*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)
      --{*35 seconds on a 1.8GHz 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 ∈ analz (Key`KK Un H)) --> (Nonce N ∈ analz H)
          ==> P --> (Nonce N ∈ analz (Key`KK Un H)) = (Nonce N ∈ 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 ∈ set_pur ==>
          (∀N KK. (∀K ∈ KK. K ∉ range(λC. priEK C))   -->
                  (Nonce N ∈ analz (Key`KK ∪ (knows Spy evs))) =
                  (Nonce N ∈ 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 (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*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)
      --{*35 seconds on a 1.8GHz machine*}
    apply spy_analz --{*Fake*}
    apply (blast elim!: ballE) --{*PReqS*}
    done

    lemma PANSecret_notin_spies:
         "[|Nonce (PANSecret k) ∈ analz (knows Spy evs);  evs ∈ set_pur|]
          ==>
           (∃V W X Y KC2 M. ∃P ∈ bad.
              Says (Cardholder k) M
                   {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|},
                     V|}  ∈  set evs)"
    apply (erule rev_mp)
    apply (erule set_pur.induct)
    apply (frule_tac [9] AuthReq_msg_in_analz_spies)
    apply (tactic{*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)
      --{*13 seconds on a 1.8GHz 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 ∈ set_pur ==> Nonce (CardSecret i) ∉ parts (knows Spy evs)"
    by (erule set_pur.induct, auto)

    subsection{*Confidentiality of PAN*}

    lemma analz_image_pan_lemma:
         "(Pan P ∈ analz (Key`nE Un H)) --> (Pan P ∈ analz H)  ==>
          (Pan P ∈ analz (Key`nE Un H)) =   (Pan P ∈ 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 ∈ set_pur ==>
           ∀KK. (∀K ∈ KK. K ∉ range(λC. priEK C)) -->
                (Pan P ∈ analz (Key`KK Un (knows Spy evs))) =
                (Pan P ∈ 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 (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*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)
      --{*32 seconds on a 1.8GHz machine*}
    apply spy_analz --{*Fake*}
    apply auto
    done

    lemma analz_insert_pan:
         "[| evs ∈ set_pur;  K ∉ range(λC. priEK C) |] ==>
              (Pan P ∈ analz (insert (Key K) (knows Spy evs))) =
              (Pan P ∈ 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) ∈ analz(knows Spy evs);  C = Cardholder k;
             CardSecret k = 0;  evs ∈ set_pur|]
        ==> ∃P M KC1 K X Y.
         Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|}
              ∈ set evs  &
         P ∈ bad"
    apply (erule rev_mp)
    apply (erule set_pur.induct)
    apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
    apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*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)
      --{*15 seconds on a 1.8GHz 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) ∈ analz(knows Spy evs);  C = Cardholder k;
        CardSecret k ≠ 0;  evs ∈ set_pur|]
      ==> ∃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|} ∈ set evs  &  P ∈ bad"
    apply (erule rev_mp)
    apply (erule set_pur.induct)
    apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
    apply (tactic{*valid_certificate_tac 8*}) --{*PReqS*}
    apply (tactic{*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)
      --{*17 seconds on a 1.8GHz 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|} ∈ set evs;
            evs ∈ set_pur|] ==> ∃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) ∈ parts (knows Spy evs);
             evs ∈ set_pur; M ∉ bad |]
          ==> ∃j trans.
                P = PG j &
                Notes M {|Number LID_M, Agent P, trans|} ∈ 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)|}) ∈ set evs;
             evs ∈ set_pur;  M ∉ bad|]
          ==> ∃j trans.
                P = PG j &
                Notes M {|Number LID_M, Agent P, trans|} ∈ 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) ∈ parts (knows Spy evs);
         evs ∈ set_pur;  M ∉ bad|]
      ==> ∃j trans.
             Notes M {|Number LID_M, Agent P, trans|} ∈ 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)|})
               ∈ set evs;  M ∉ bad;  evs ∈ set_pur|]
          ==> ∃j trans.
               Notes M {|Number LID_M, Agent P, trans|} ∈ 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|})
               ∈ parts (knows Spy evs);
             evs ∈ set_pur;  M ∉ bad|]
          ==> ∃j trans KM OIData HPIData.
                Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs &
                Gets M {|P_I, OIData, HPIData|} ∈ set evs &
                Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
                  ∈ 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) ∈ parts (knows Spy evs);
          PG j ∉ bad;  evs ∈ set_pur|]
       ==> ∃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) ∈ set evs &
            Says (PG j) M
                 (EncB (priSK (PG j)) KP (pubEK M)
                  {|Number LID_M, Number XID, Number PurchAmt|}
                  authCode) ∈ 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)|} |} ∈ set evs;
             PIHead = {|Number LID_M, Trans_details|};
             evs ∈ set_pur;  C = Cardholder k;  M ∉ bad|]
      ==> ∃trans j.
                   Notes M {|Number LID_M, Agent (PG j), trans |} ∈ set evs &
                   EKj = pubEK (PG j)"
    apply clarify
    apply (erule rev_mp)
    apply (erule set_pur.induct, simp_all)
    apply (tactic{*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|} ∈ set evs;
            Notes C {|Number LID_M, Agent M, Agent C, Number OD,
                 Number PA|} ∈ set evs;
            evs ∈ 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|} ∈ set evs;
            Notes M {|Number LID_M, Trans'|} ∈ set evs;
            evs ∈ 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) ∈ parts (knows Spy evs);
             M ∉ bad;  evs ∈ set_pur|] ==> parts {X} ⊆ 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|}) ∈ parts (knows Spy evs);
             C ∉ bad;  evs ∈ set_pur|] ==> parts {X} ⊆ 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|}) ∈ parts (knows Spy evs);
             M ∉ bad;  evs ∈ set_pur|] ==> N ∈ 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) ∈ parts (knows Spy evs);
             Notes C {|Number LID_M, Trans |} ∈ set evs;
             Trans = {| Agent M, Agent C, Number OrderDesc, Number PurchAmt |};
             MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
                    Hash (Number PurchAmt)|};
             evs ∈ set_pur;  M ∉ bad|]
      ==> ∃j KP.
            Notes M {|Number LID_M, Agent (PG j), Trans |}
              ∈ set evs &
            Gets M (EncB (priSK (PG j)) KP (pubEK M)
                    {|Number LID_M, Number XID, Number PurchAmt|}
                    authCode)
              ∈ set evs &
            Says M C (sign (priSK M) MsgPRes) ∈ 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) ∈ set evs;
             Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc,
                       Number PurchAmt|} ∈ set evs;
             evs ∈ set_pur;  M ∉ bad|]
      ==> ∃P KP trans.
            Notes M {|Number LID_M,Agent P, trans|} ∈ set evs &
            Gets M (EncB (priSK P) KP (pubEK M)
                    {|Number LID_M, Number XID, Number PurchAmt|}
                    authCode)  ∈  set evs &
            Says M C (sign (priSK M) MsgPRes) ∈ 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|}
               ∈ parts (knows Spy evs);
             PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
             Key K ∉ analz (knows Spy evs);
             evs ∈ set_pur|]
      ==> ∃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|} ∈ 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 ∈ set evs;
             evs ∈ set_pur |]
       ==> ∃trans.
               Notes (Cardholder k)
                     {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
                ∈ 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|} ∈ set evs;
            evs ∈ 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) ∈ parts (knows Spy evs);
         Notes M {|Number LID_M, Agent P, extras|} ∈ set evs;
         M = Merchant i;  C = Cardholder k;  C ∉ bad;  evs ∈ set_pur|]
      ==> ∃PIData PICrypt.
            HPIData = Hash PIData &
            Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
              ∈ 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 (force dest!: signed_Hash_imp_used)
    apply (clarify) --{*speeds next step*}
    apply (blast dest: 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 ∉ 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) ∈ parts (knows Spy evs);
             evs ∈ set_pur;  C ∉ bad;  M ∉ bad|]
        ==> ∃OIData OrderDesc K j trans.
              HOD = Hash{|Number OrderDesc, Number PurchAmt|} &
              HOIData = Hash OIData &
              Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs &
              Says C M {|{|sign (priSK C) MsgDualSign,
                         EXcrypt K (pubEK (PG j))
                                    {|PIHead, Hash OIData|} PANData|},
                         OIData, Hash PIData|}
                ∈ 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|} ∈ set evs;
             PIHead = {|Number LID_M, Number XID, W|};
             C = Cardholder k;  evs ∈ set_pur;  M ∉ bad|]
      ==> ∃ trans j.
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ 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|} ∈ parts (knows Spy evs);
             evs ∈ set_pur;  M ∉ bad|]
       ==> ∃j trans KM.
               Notes M {|Number LID_M, Agent (PG j), trans |} ∈ set evs &
                 Says M (PG j)
                   (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
                  ∈ 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) ∈ parts (knows Spy evs);
             M = Merchant i;  C = Cardholder k;  C ∉ bad;  evs ∈ set_pur|]
          ==> ∃KC EKj.
                Says C M {|{|sign (priSK C) MsgDualSign,
                           EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
                           OIData, Hash PIData|}
                  ∈ set evs"
    apply clarify
    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 ∈ symKeys;
             Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
               ∈ 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 ∈ set_pur;  C ∉ bad;  M ∉ bad|]
      ==> ∃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|} ∈ set evs &
               Says C M {|P_I', OIData, Hash PIData|} ∈ set evs &
               Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j'))
                               AuthReqData P_I'')  ∈  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

### Possibility Properties

lemma Says_to_Gets:

      Says A B X # evs ∈ set_pur ==> Gets B X # Says A B X # evs ∈ set_pur

lemma possibility_Uns:

      [| CardSecret k = 0; C = Cardholder k; M = Merchant i; Key KC ∉ used [];
         Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys;
         KC < KM; KM < KP; Nonce Chall_C ∉ used [];
         Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used [];
         Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M;
         Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret;
         Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID;
         XID < OrderDesc; OrderDesc < PurchAmt |]
      ==> ∃evs∈set_pur.
             Says M C
              (sign (priSK M)
                {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
             ∈ set evs

lemma possibility_S:

      [| CardSecret k ≠ 0; C = Cardholder k; M = Merchant i; Key KC ∉ used [];
         Key KM ∉ used []; Key KP ∉ used []; KC ∈ symKeys; KM ∈ symKeys; KP ∈ symKeys;
         KC < KM; KM < KP; Nonce Chall_C ∉ used [];
         Chall_C ∉ range CardSecret ∪ range PANSecret; Nonce Chall_M ∉ used [];
         Chall_M ∉ range CardSecret ∪ range PANSecret; Chall_C < Chall_M;
         Number LID_M ∉ used []; LID_M ∉ range CardSecret ∪ range PANSecret;
         Number XID ∉ used []; XID ∉ range CardSecret ∪ range PANSecret; LID_M < XID;
         XID < OrderDesc; OrderDesc < PurchAmt |]
      ==> ∃evs∈set_pur.
             Says M C
              (sign (priSK M)
                {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|})
             ∈ set evs

lemma Gets_imp_Says:

      [| Gets B X ∈ set evs; evs ∈ set_pur |] ==> ∃A. Says A B X ∈ set evs

lemma Gets_imp_knows_Spy:

      [| Gets B X ∈ set evs; evs ∈ set_pur |] ==> X ∈ knows Spy evs

lemma AuthReq_msg_in_parts_spies:

      [| Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur |]
      ==> P_I ∈ parts (knows Spy evs)

lemma AuthReq_msg_in_analz_spies:

      [| Gets M {|P_I, OIData, HPIData|} ∈ set evs; evs ∈ set_pur |]
      ==> P_I ∈ analz (knows Spy evs)

### Proofs on Asymmetric Keys

lemma Spy_see_private_Key:

      evs ∈ set_pur
      ==> (Key (invKey (publicKey b A)) ∈ parts (knows Spy evs)) = (A ∈ bad)

lemma Spy_analz_private_Key:

      evs ∈ set_pur
      ==> (Key (invKey (publicKey b A)) ∈ analz (knows Spy evs)) = (A ∈ bad)

lemma parts_image_priEK:

      [| Key (priEK C) ∈ parts (Key ` KK ∪ knows Spy evs); evs ∈ set_pur |]
      ==> priEK C ∈ KK ∨ C ∈ bad

lemma analz_image_priEK:

      evs ∈ set_pur
      ==> (Key (priEK C) ∈ analz (Key ` KK ∪ knows Spy evs)) =
          (priEK C ∈ KK ∨ C ∈ bad)

### Public Keys in Certificates are Correct

lemma Crypt_valid_pubEK:

      [| Crypt (priSK RCA) {|Agent C, Key EKi, onlyEnc|} ∈ parts (knows Spy evs);
         evs ∈ set_pur |]
      ==> EKi = pubEK C

lemma Crypt_valid_pubSK:

      [| Crypt (priSK RCA) {|Agent C, Key SKi, onlySig|} ∈ parts (knows Spy evs);
         evs ∈ set_pur |]
      ==> SKi = pubSK C

lemma certificate_valid_pubEK:

      [| cert C EKi onlyEnc (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |]
      ==> EKi = pubEK C

lemma certificate_valid_pubSK:

      [| cert C SKi onlySig (priSK RCA) ∈ parts (knows Spy evs); evs ∈ set_pur |]
      ==> SKi = pubSK C

lemma Says_certificate_valid:

      [| Says A B (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|})
         ∈ set evs;
         evs ∈ set_pur |]
      ==> EK = pubEK C

lemma Gets_certificate_valid:

      [| Gets A (sign SK {|lid, xid, cc, cm, cert C EK onlyEnc (priSK RCA)|})
         ∈ set evs;
         evs ∈ set_pur |]
      ==> EK = pubEK C

### Proofs on Symmetric Keys

lemma new_keys_not_used:

      [| evs ∈ set_pur; Key K ∉ used evs; K ∈ symKeys |]
      ==> K ∉ keysFor (parts (knows Spy evs))

lemma new_keys_not_analzd:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
      ==> K ∉ keysFor (analz (knows Spy evs))

lemma Crypt_parts_imp_used:

      [| Crypt K X ∈ parts (knows Spy evs); K ∈ symKeys; evs ∈ set_pur |]
      ==> Key K ∈ used evs

lemma Crypt_analz_imp_used:

      [| Crypt K X ∈ analz (knows Spy evs); K ∈ symKeys; evs ∈ set_pur |]
      ==> Key K ∈ used evs

lemma gen_new_keys_not_used:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
      ==> Key K ∉ used evs -->
          K ∈ symKeys --> K ∉ keysFor (parts (Key ` KK ∪ knows Spy evs))

lemma gen_new_keys_not_analzd:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
      ==> K ∉ keysFor (analz (Key ` KK ∪ knows Spy evs))

lemma analz_Key_image_insert_eq:

      [| Key K ∉ used evs; K ∈ symKeys; evs ∈ set_pur |]
      ==> analz (Key ` insert K KK ∪ knows Spy evs) =
          insert (Key K) (analz (Key ` KK ∪ knows Spy evs))

### Secrecy of Symmetric Keys

lemma Key_analz_image_Key_lemma:

      P --> Key K ∈ analz (Key ` KK ∪ H) --> K ∈ KK ∨ Key K ∈ analz H
      ==> P --> (Key K ∈ analz (Key ` KK ∪ H)) = (K ∈ KK ∨ Key K ∈ analz H)

lemma symKey_compromise:

      evs ∈ set_pur
      ==> ∀SK KK.
             SK ∈ symKeys -->
             (∀K∈KK. K ∉ range (%C. priEK C)) -->
             (Key SK ∈ analz (Key ` KK ∪ knows Spy evs)) =
             (SK ∈ KK ∨ Key SK ∈ analz (knows Spy evs))

### Secrecy of Nonces

lemma Nonce_analz_image_Key_lemma:

      P --> Nonce N ∈ analz (Key ` KK ∪ H) --> Nonce N ∈ analz H
      ==> P --> (Nonce N ∈ analz (Key ` KK ∪ H)) = (Nonce N ∈ analz H)

lemma Nonce_compromise:

      [| evs ∈ set_pur; ∀K∈KK. K ∉ range (%C. priEK C) |]
      ==> (Nonce N ∈ analz (Key ` KK ∪ knows Spy evs)) =
          (Nonce N ∈ analz (knows Spy evs))

lemma PANSecret_notin_spies:

      [| Nonce (PANSecret k) ∈ analz (knows Spy evs); evs ∈ set_pur |]
      ==> ∃V W X Y KC2 M.
             ∃P∈bad.
                Says (Cardholder k) M
                 {|{|W, EXcrypt KC2 (pubEK P) X {|Y, Nonce (PANSecret k)|}|}, V|}
                ∈ set evs

lemma CardSecret_notin_spies:

      evs ∈ set_pur ==> Nonce (CardSecret i) ∉ parts (knows Spy evs)

### Confidentiality of PAN

lemma analz_image_pan_lemma:

      Pan P ∈ analz (Key ` nE ∪ H) --> Pan P ∈ analz H
      ==> (Pan P ∈ analz (Key ` nE ∪ H)) = (Pan P ∈ analz H)

lemma analz_image_pan:

      [| evs ∈ set_pur; ∀K∈KK. K ∉ range (%C. priEK C) |]
      ==> (Pan P ∈ analz (Key ` KK ∪ knows Spy evs)) = (Pan P ∈ analz (knows Spy evs))

lemma analz_insert_pan:

      [| evs ∈ set_pur; K ∉ range (%C. priEK C) |]
      ==> (Pan P ∈ analz (insert (Key K) (knows Spy evs))) =
          (Pan P ∈ analz (knows Spy evs))

theorem pan_confidentiality_unsigned:

      [| Pan (pan C) ∈ analz (knows Spy evs); C = Cardholder k; CardSecret k = 0;
         evs ∈ set_pur |]
      ==> ∃P M KC1 K X Y.
             Says C M {|EXHcrypt KC1 (pubEK P) X (Pan (pan C)), Y|} ∈ set evs ∧
             P ∈ bad

theorem pan_confidentiality_signed:

      [| Pan (pan C) ∈ analz (knows Spy evs); C = Cardholder k; CardSecret k ≠ 0;
         evs ∈ set_pur |]
      ==> ∃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|}
             ∈ set evs ∧
             P ∈ bad

### Proofs Common to Signed and Unsigned Versions

lemma M_Notes_PG:

      [| Notes M {|Number LID_M, Agent P, Agent M, Agent C, etc|} ∈ set evs;
         evs ∈ set_pur |]
      ==> ∃j. P = PG j

lemma goodM_gives_correct_PG:

      [| MsgPInitRes = {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|};
         Crypt (priSK M) (Hash MsgPInitRes) ∈ parts (knows Spy evs); evs ∈ set_pur;
         M ∉ bad |]
      ==> ∃j trans. P = PG j ∧ Notes M {|Number LID_M, Agent P, trans|} ∈ set evs

lemma C_gets_correct_PG:

      [| Gets A
          (sign (priSK M)
            {|Number LID_M, xid, cc, cm, cert P EKj onlyEnc (priSK RCA)|})
         ∈ set evs;
         evs ∈ set_pur; M ∉ bad |]
      ==> ∃j trans.
             P = PG j ∧
             Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧ EKj = pubEK 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) ∈ parts (knows Spy evs); evs ∈ set_pur;
         M ∉ bad |]
      ==> ∃j trans.
             Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧
             P = PG j ∧ EKj = pubEK P

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)|})
         ∈ set evs;
         M ∉ bad; evs ∈ set_pur |]
      ==> ∃j trans.
             Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧
             P = PG j ∧ EKj = pubEK (PG j)

lemma P_verifies_AuthReq:

      [| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
         Crypt (priSK M) (Hash {|AuthReqData, Hash P_I|}) ∈ parts (knows Spy evs);
         evs ∈ set_pur; M ∉ bad |]
      ==> ∃j trans KM OIData HPIData.
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧
             Gets M {|P_I, OIData, HPIData|} ∈ set evs ∧
             Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
             ∈ set evs

theorem M_verifies_AuthRes:

      [| MsgAuthRes =
         {|{|Number LID_M, Number XID, Number PurchAmt|}, Hash authCode|};
         Crypt (priSK (PG j)) (Hash MsgAuthRes) ∈ parts (knows Spy evs); PG j ∉ bad;
         evs ∈ set_pur |]
      ==> ∃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)
             ∈ set evs ∧
             Says (PG j) M
              (EncB (priSK (PG j)) KP (pubEK M)
                {|Number LID_M, Number XID, Number PurchAmt|} authCode)
             ∈ set evs

### Proofs for Unsigned Purchases

lemma C_determines_EKj:

      [| Says C M
          {|EXHcrypt KC1.0 EKj {|PIHead, Hash OIData|} (Pan (pan C)), OIData,
            Hash {|PIHead, Pan (pan C)|}|}
         ∈ set evs;
         PIHead = {|Number LID_M, Trans_details|}; evs ∈ set_pur; C = Cardholder k;
         M ∉ bad |]
      ==> ∃trans j.
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧
             EKj = pubEK (PG j)

lemma unique_LID_M:

      [| Notes (Merchant i) {|Number LID_M, Agent P, Trans|} ∈ set evs;
         Notes C {|Number LID_M, Agent M, Agent C, Number OD, Number PA|} ∈ set evs;
         evs ∈ set_pur |]
      ==> M = Merchant i ∧ Trans = {|Agent M, Agent C, Number OD, Number PA|}

lemma unique_LID_M2:

      [| Notes M {|Number LID_M, Trans|} ∈ set evs;
         Notes M {|Number LID_M, Trans'|} ∈ set evs; evs ∈ set_pur |]
      ==> Trans' = Trans

lemma signed_imp_used:

      [| Crypt (priSK M) (Hash X) ∈ parts (knows Spy evs); M ∉ bad; evs ∈ set_pur |]
      ==> parts {X} ⊆ used evs

lemma signed_Hash_imp_used:

      [| Crypt (priSK C) (Hash {|H, Hash X|}) ∈ parts (knows Spy evs); C ∉ bad;
         evs ∈ set_pur |]
      ==> parts {X} ⊆ used evs

lemma PRes_imp_LID_used:

      [| Crypt (priSK M) (Hash {|N, X|}) ∈ parts (knows Spy evs); M ∉ bad;
         evs ∈ set_pur |]
      ==> N ∈ used evs

lemma C_verifies_PRes_lemma:

      [| Crypt (priSK M) (Hash MsgPRes) ∈ parts (knows Spy evs);
         Notes C {|Number LID_M, Trans|} ∈ set evs;
         Trans = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
         MsgPRes =
         {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|};
         evs ∈ set_pur; M ∉ bad |]
      ==> ∃j KP. Notes M {|Number LID_M, Agent (PG j), Trans|} ∈ set evs ∧
                 Gets M
                  (EncB (priSK (PG j)) KP (pubEK M)
                    {|Number LID_M, Number XID, Number PurchAmt|} authCode)
                 ∈ set evs ∧
                 Says M C (sign (priSK M) MsgPRes) ∈ set evs

theorem C_verifies_PRes:

      [| MsgPRes =
         {|Number LID_M, Number XID, Nonce Chall_C, Hash (Number PurchAmt)|};
         Gets C (sign (priSK M) MsgPRes) ∈ set evs;
         Notes C {|Number LID_M, Agent M, Agent C, Number OrderDesc, Number PurchAmt|}
         ∈ set evs;
         evs ∈ set_pur; M ∉ bad |]
      ==> ∃P KP trans.
             Notes M {|Number LID_M, Agent P, trans|} ∈ set evs ∧
             Gets M
              (EncB (priSK P) KP (pubEK M)
                {|Number LID_M, Number XID, Number PurchAmt|} authCode)
             ∈ set evs ∧
             Says M C (sign (priSK M) MsgPRes) ∈ set evs

### Proofs for Signed Purchases

lemma Crypt_imp_Says_Cardholder:

      [| Crypt K {|{|{|Number LID_M, others|}, Hash OIData|}, Hash PANData|}
         ∈ parts (knows Spy evs);
         PANData = {|Pan (pan (Cardholder k)), Nonce (PANSecret k)|};
         Key K ∉ analz (knows Spy evs); evs ∈ set_pur |]
      ==> ∃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|}
             ∈ set evs

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 ∈ set evs; evs ∈ set_pur |]
      ==> ∃trans.
             Notes (Cardholder k)
              {|Number LID_M, Agent M, Agent (Cardholder k), trans|}
             ∈ set evs

lemma Notes_Cardholder_self_False:

      [| Notes (Cardholder k)
          {|Number n, Agent P, Agent (Cardholder k), Agent C, etc|}
         ∈ set evs;
         evs ∈ set_pur |]
      ==> False

theorem M_verifies_Signed_PReq:

      [| MsgDualSign = {|HPIData, Hash OIData|}; OIData = {|Number LID_M, etc|};
         Crypt (priSK C) (Hash MsgDualSign) ∈ parts (knows Spy evs);
         Notes M {|Number LID_M, Agent P, extras|} ∈ set evs; M = Merchant i;
         C = Cardholder k; C ∉ bad; evs ∈ set_pur |]
      ==> ∃PIData PICrypt.
             HPIData = Hash PIData ∧
             Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
             ∈ set evs

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) ∈ parts (knows Spy evs); evs ∈ set_pur;
         C ∉ bad; M ∉ bad |]
      ==> ∃OIData OrderDesc K j trans.
             HOD = Hash {|Number OrderDesc, Number PurchAmt|} ∧
             HOIData = Hash OIData ∧
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧
             Says C M
              {|{|sign (priSK C) MsgDualSign,
                  EXcrypt K (pubEK (PG j)) {|PIHead, Hash OIData|} PANData|},
                OIData, Hash PIData|}
             ∈ set evs

lemma C_determines_EKj_signed:

      [| Says C M {|{|sign (priSK C) text, EXcrypt K EKj {|PIHead, X|} Y|}, Z|}
         ∈ set evs;
         PIHead = {|Number LID_M, Number XID, W|}; C = Cardholder k; evs ∈ set_pur;
         M ∉ bad |]
      ==> ∃trans j.
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧
             EKj = pubEK (PG j)

lemma M_Says_AuthReq:

      [| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
         sign (priSK M) {|AuthReqData, Hash P_I|} ∈ parts (knows Spy evs);
         evs ∈ set_pur; M ∉ bad |]
      ==> ∃j trans KM.
             Notes M {|Number LID_M, Agent (PG j), trans|} ∈ set evs ∧
             Says M (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)
             ∈ set evs

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) ∈ parts (knows Spy evs); M = Merchant i;
         C = Cardholder k; C ∉ bad; evs ∈ set_pur |]
      ==> ∃KC EKj.
             Says C M
              {|{|sign (priSK C) MsgDualSign,
                  EXcrypt KC EKj {|PIHead, Hash OIData|} PANData|},
                OIData, Hash PIData|}
             ∈ set evs

theorem P_sees_CM_agreement:

      [| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|}; KC ∈ symKeys;
         Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I) ∈ 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 ∈ set_pur; C ∉ bad; M ∉ bad |]
      ==> ∃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|} ∈ set evs ∧
             Says C M {|P_I', OIData, Hash PIData|} ∈ set evs ∧
             Says M (PG j') (EncB (priSK M) KM' (pubEK (PG j')) AuthReqData P_I'')
             ∈ 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|}