tidying up; identifying the main theorems
authorpaulson
Wed Sep 29 13:58:40 2004 +0200 (2004-09-29)
changeset 15214d3ab9b76ccb7
parent 15213 4aa219600e5e
child 15215 6bd87812537c
tidying up; identifying the main theorems
src/HOL/SET-Protocol/Purchase.thy
     1.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Tue Sep 28 13:56:46 2004 +0200
     1.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Wed Sep 29 13:58:40 2004 +0200
     1.3 @@ -633,6 +633,7 @@
     1.4       "evs \<in> set_pur ==> Nonce (CardSecret i) \<notin> parts (knows Spy evs)"
     1.5  by (erule set_pur.induct, auto)
     1.6  
     1.7 +
     1.8  subsection{*Confidentiality of PAN*}
     1.9  
    1.10  lemma analz_image_pan_lemma:
    1.11 @@ -672,7 +673,7 @@
    1.12           add: analz_image_keys_simps analz_image_pan)
    1.13  
    1.14  text{*Confidentiality of the PAN, unsigned case.*}
    1.15 -lemma pan_confidentiality_unsigned:
    1.16 +theorem pan_confidentiality_unsigned:
    1.17       "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
    1.18           CardSecret k = 0;  evs \<in> set_pur|]
    1.19      ==> \<exists>P M KC1 K X Y.
    1.20 @@ -696,13 +697,13 @@
    1.21  done
    1.22  
    1.23  text{*Confidentiality of the PAN, signed case.*}
    1.24 -lemma pan_confidentiality_signed:
    1.25 -     "[| Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
    1.26 -         CardSecret k \<noteq> 0;  evs \<in> set_pur|]
    1.27 -    ==> \<exists>B M KC2 K ps X Y Z.
    1.28 -     Says C M {|{|X, EXcrypt KC2 (pubEK B) Y {|Pan (pan C), ps|}|}, Z|}
    1.29 -          \<in> set evs  &
    1.30 -     B \<in> bad"
    1.31 +theorem pan_confidentiality_signed:
    1.32 + "[|Pan (pan C) \<in> analz(knows Spy evs);  C = Cardholder k;
    1.33 +    CardSecret k \<noteq> 0;  evs \<in> set_pur|]
    1.34 +  ==> \<exists>P M KC2 PIDualSign_1 PIDualSign_2 other OIDualSign.
    1.35 +      Says C M {|{|PIDualSign_1, 
    1.36 +                   EXcrypt KC2 (pubEK P) PIDualSign_2 {|Pan (pan C), other|}|}, 
    1.37 +       OIDualSign|} \<in> set evs  &  P \<in> bad"
    1.38  apply (erule rev_mp)
    1.39  apply (erule set_pur.induct)
    1.40  apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*}
    1.41 @@ -818,7 +819,7 @@
    1.42    the identifying tages and the purchase amount, which he can verify.
    1.43    (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they
    1.44     send the same message to M.)*}
    1.45 -lemma M_verifies_AuthRes:
    1.46 +theorem M_verifies_AuthRes:
    1.47    "[| MsgAuthRes = {|Number LID_M, Number XID, Number PurchAmt|};
    1.48        Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs);
    1.49        evs \<in> set_pur;  PG j \<notin> bad|]
    1.50 @@ -946,7 +947,10 @@
    1.51  apply (blast dest: unique_LID_M)
    1.52  done
    1.53  
    1.54 -lemma C_verifies_PRes:
    1.55 +text{*When the Cardholder receives Purchase Response from an uncompromised
    1.56 +Merchant, he knows that M sent it. He also knows that M received a message signed
    1.57 +by a Payment Gateway chosen by M to authorize the purchase.*}
    1.58 +theorem C_verifies_PRes:
    1.59       "[| MsgPRes = {|Number LID_M, Number XID, Nonce Chall_C,
    1.60                       Hash (Number PurchAmt)|};
    1.61           Gets C (sign (priSK M) MsgPRes) \<in> set evs;
    1.62 @@ -957,8 +961,7 @@
    1.63          Notes M {|Number LID_M,Agent P, trans|} \<in> set evs &
    1.64          Gets M (EncB (priSK P) KP (pubEK M)
    1.65                  {|Number LID_M, Number XID, Number PurchAmt|}
    1.66 -                authCode)
    1.67 -          \<in> set evs &
    1.68 +                authCode)  \<in>  set evs &
    1.69          Says M C (sign (priSK M) MsgPRes) \<in> set evs"
    1.70  apply (rule C_verifies_PRes_lemma [THEN exE])
    1.71  apply (auto simp add: sign_def)
    1.72 @@ -1019,16 +1022,16 @@
    1.73  text{*When M sees a dual signature, he knows that it originated with C.
    1.74    Using XID he knows it was intended for him.
    1.75    This guarantee isn't useful to P, who never gets OIData.*}
    1.76 -lemma M_verifies_Signed_PReq:
    1.77 -     "[| MsgDualSign = {|HPIData, Hash OIData|};
    1.78 -         OIData = {|Number LID_M, etc|};
    1.79 -         Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
    1.80 -         Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
    1.81 -         M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
    1.82 -      ==> \<exists>PIData PICrypt.
    1.83 -            HPIData = Hash PIData &
    1.84 -            Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
    1.85 -              \<in> set evs"
    1.86 +theorem M_verifies_Signed_PReq:
    1.87 + "[| MsgDualSign = {|HPIData, Hash OIData|};
    1.88 +     OIData = {|Number LID_M, etc|};
    1.89 +     Crypt (priSK C) (Hash MsgDualSign) \<in> parts (knows Spy evs);
    1.90 +     Notes M {|Number LID_M, Agent P, extras|} \<in> set evs;
    1.91 +     M = Merchant i;  C = Cardholder k;  C \<notin> bad;  evs \<in> set_pur|]
    1.92 +  ==> \<exists>PIData PICrypt.
    1.93 +	HPIData = Hash PIData &
    1.94 +	Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|}
    1.95 +	  \<in> set evs"
    1.96  apply clarify
    1.97  apply (erule rev_mp)
    1.98  apply (erule rev_mp)
    1.99 @@ -1046,7 +1049,7 @@
   1.100    and was intended for M. This guarantee isn't useful to M, who never gets
   1.101    PIData. I don't see how to link @{term "PG j"} and @{text LID_M} without
   1.102    assuming @{term "M \<notin> bad"}.*}
   1.103 -lemma P_verifies_Signed_PReq:
   1.104 +theorem P_verifies_Signed_PReq:
   1.105       "[| MsgDualSign = {|Hash PIData, HOIData|};
   1.106           PIData = {|PIHead, PANData|};
   1.107           PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M,
   1.108 @@ -1128,7 +1131,7 @@
   1.109    of PG (namely j'), and sends AReq there; he can't, however, check that
   1.110    the EXcrypt involves the correct PG's key.
   1.111  *}
   1.112 -lemma P_sees_CM_agreement:
   1.113 +theorem P_sees_CM_agreement:
   1.114       "[| AuthReqData = {|Number LID_M, Number XID, HOIData, HOD|};
   1.115           KC \<in> symKeys;
   1.116           Gets (PG j) (EncB (priSK M) KM (pubEK (PG j)) AuthReqData P_I)