src/HOL/SET-Protocol/Purchase.thy
changeset 23755 1c4672d130b1
parent 16474 c3c0208988c0
child 24123 a0fc58900606
     1.1 --- a/src/HOL/SET-Protocol/Purchase.thy	Wed Jul 11 11:27:46 2007 +0200
     1.2 +++ b/src/HOL/SET-Protocol/Purchase.thy	Wed Jul 11 11:28:13 2007 +0200
     1.3 @@ -57,24 +57,23 @@
     1.4      PANSecret :: "nat => nat"
     1.5       --{*Maps Cardholders to PANSecrets.*}
     1.6  
     1.7 -    set_pur  :: "event list set"
     1.8 -
     1.9 -inductive set_pur
    1.10 - intros
    1.11 +inductive_set
    1.12 +  set_pur :: "event list set"
    1.13 +where
    1.14  
    1.15    Nil:   --{*Initial trace is empty*}
    1.16  	 "[] \<in> set_pur"
    1.17  
    1.18 -  Fake:  --{*The spy MAY say anything he CAN say.*}
    1.19 +| Fake:  --{*The spy MAY say anything he CAN say.*}
    1.20  	 "[| evsf \<in> set_pur;  X \<in> synth(analz(knows Spy evsf)) |]
    1.21  	  ==> Says Spy B X  # evsf \<in> set_pur"
    1.22  
    1.23  
    1.24 -  Reception: --{*If A sends a message X to B, then B might receive it*}
    1.25 +| Reception: --{*If A sends a message X to B, then B might receive it*}
    1.26  	     "[| evsr \<in> set_pur;  Says A B X \<in> set evsr |]
    1.27  	      ==> Gets B X  # evsr \<in> set_pur"
    1.28  
    1.29 -  Start: 
    1.30 +| Start: 
    1.31        --{*Added start event which is out-of-band for SET: the Cardholder and
    1.32  	  the merchant agree on the amounts and uses @{text LID_M} as an
    1.33            identifier.
    1.34 @@ -91,7 +90,7 @@
    1.35         # Notes M {|Number LID_M, Agent P, Transaction|}
    1.36         # evsStart \<in> set_pur"
    1.37  
    1.38 -  PInitReq:
    1.39 +| PInitReq:
    1.40       --{*Purchase initialization, page 72 of Formal Protocol Desc.*}
    1.41     "[|evsPIReq \<in> set_pur;
    1.42        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    1.43 @@ -100,7 +99,7 @@
    1.44        Notes C {|Number LID_M, Transaction |} \<in> set evsPIReq |]
    1.45      ==> Says C M {|Number LID_M, Nonce Chall_C|} # evsPIReq \<in> set_pur"
    1.46  
    1.47 -  PInitRes:
    1.48 +| PInitRes:
    1.49       --{*Merchant replies with his own label XID and the encryption
    1.50  	 key certificate of his chosen Payment Gateway. Page 74 of Formal
    1.51           Protocol Desc. We use @{text LID_M} to identify Cardholder*}
    1.52 @@ -118,7 +117,7 @@
    1.53  			 cert P (pubEK P) onlyEnc (priSK RCA)|})
    1.54            # evsPIRes \<in> set_pur"
    1.55  
    1.56 -  PReqUns:
    1.57 +| PReqUns:
    1.58        --{*UNSIGNED Purchase request (CardSecret = 0).
    1.59  	Page 79 of Formal Protocol Desc.
    1.60  	Merchant never sees the amount in clear. This holds of the real
    1.61 @@ -126,7 +125,8 @@
    1.62  	Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because
    1.63  	the CardSecret is 0 and because AuthReq treated the unsigned case
    1.64  	very differently from the signed one anyway.*}
    1.65 -   "[|evsPReqU \<in> set_pur;
    1.66 +   "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU.
    1.67 +    [|evsPReqU \<in> set_pur;
    1.68        C = Cardholder k; CardSecret k = 0;
    1.69        Key KC1 \<notin> used evsPReqU;  KC1 \<in> symKeys;
    1.70        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    1.71 @@ -146,14 +146,17 @@
    1.72  	  # Notes C {|Key KC1, Agent M|}
    1.73  	  # evsPReqU \<in> set_pur"
    1.74  
    1.75 -  PReqS:
    1.76 +| PReqS:
    1.77        --{*SIGNED Purchase request.  Page 77 of Formal Protocol Desc.
    1.78            We could specify the equation
    1.79  	  @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the
    1.80  	  Formal Desc. gives PIHead the same format in the unsigned case.
    1.81  	  However, there's little point, as P treats the signed and 
    1.82            unsigned cases differently.*}
    1.83 -   "[|evsPReqS \<in> set_pur;
    1.84 +   "!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData
    1.85 +      OIDualSigned OrderDesc P PANData PIData PIDualSigned
    1.86 +      PIHead PurchAmt Transaction XID evsPReqS k.
    1.87 +    [|evsPReqS \<in> set_pur;
    1.88        C = Cardholder k;
    1.89        CardSecret k \<noteq> 0;  Key KC2 \<notin> used evsPReqS;  KC2 \<in> symKeys;
    1.90        Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
    1.91 @@ -179,7 +182,7 @@
    1.92  
    1.93    --{*Authorization Request.  Page 92 of Formal Protocol Desc.
    1.94      Sent in response to Purchase Request.*}
    1.95 -  AuthReq:
    1.96 +| AuthReq:
    1.97     "[| evsAReq \<in> set_pur;
    1.98         Key KM \<notin> used evsAReq;  KM \<in> symKeys;
    1.99         Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};
   1.100 @@ -208,7 +211,7 @@
   1.101      full protocol is [CapToken], [AcqCardMsg], [AuthToken]:
   1.102      optional items for split shipments, recurring payments, etc.*}
   1.103  
   1.104 -  AuthResUns:
   1.105 +| AuthResUns:
   1.106      --{*Authorization Response, UNSIGNED*}
   1.107     "[| evsAResU \<in> set_pur;
   1.108         C = Cardholder k; M = Merchant i;
   1.109 @@ -225,7 +228,7 @@
   1.110  	      authCode)
   1.111         # evsAResU \<in> set_pur"
   1.112  
   1.113 -  AuthResS:
   1.114 +| AuthResS:
   1.115      --{*Authorization Response, SIGNED*}
   1.116     "[| evsAResS \<in> set_pur;
   1.117         C = Cardholder k;
   1.118 @@ -247,7 +250,7 @@
   1.119  	      authCode)
   1.120         # evsAResS \<in> set_pur"
   1.121  
   1.122 -  PRes:
   1.123 +| PRes:
   1.124      --{*Purchase response.*}
   1.125     "[| evsPRes \<in> set_pur;  KP \<in> symKeys;  M = Merchant i;
   1.126         Transaction = {|Agent M, Agent C, Number OrderDesc, Number PurchAmt|};