src/HOL/SET-Protocol/Purchase.thy

eliminated duplicate fold1 -- beware of argument order!

(*  Title:      HOL/SET-Protocol/Purchase.thy
    Author:     Giampaolo Bella
    Author:     Fabio Massacci
    Author:     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.*}

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 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 \<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 =>
    K (SIMPLE_METHOD'' quant (fn i =>
      EVERY [ftac @{thm 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 \<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 (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