author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42814  5af15f1e2ef6 
child 51798  ad3a241def73 
permissions  rwrr 
33028  1 
(* Title: HOL/SET_Protocol/Purchase.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

2 
Author: Giampaolo Bella 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

3 
Author: Fabio Massacci 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

4 
Author: Lawrence C Paulson 
14199  5 
*) 
6 

7 
header{*Purchase Phase of SET*} 

8 

33028  9 
theory Purchase 
10 
imports Public_SET 

11 
begin 

14199  12 

13 
text{* 

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

15 
challenges (ChallEE, etc.) and important secrets (CardSecret, PANsecret) 

16 

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

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

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

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

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

22 
supposed to process? 

23 

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

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

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

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

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

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

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

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

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

33 
outofbad on the value of @{text LID_M} (for instance a cookie in a web 

34 
transaction etc.). This outofband agreement is expressed with a preliminary 

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

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

37 

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

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

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

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

42 
number generators to ensure the global uniqueness of XID." 

43 
Programmer's Guide, page 267. 

44 

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

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

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

48 
initiate a payment card transaction through the traditional payment card 

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

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

51 
passes the data back to the Merchant. 

52 
Programmer's Guide, page 271.*} 

53 

54 
consts 

55 

56 
CardSecret :: "nat => nat" 

15481  57 
{*Maps Cardholders to CardSecrets. 
58 
A CardSecret of 0 means no cerificate, must use unsigned format.*} 

14199  59 

60 
PANSecret :: "nat => nat" 

15481  61 
{*Maps Cardholders to PANSecrets.*} 
14199  62 

23755  63 
inductive_set 
64 
set_pur :: "event list set" 

65 
where 

14199  66 

67 
Nil: {*Initial trace is empty*} 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

68 
"[] \<in> set_pur" 
14199  69 

23755  70 
 Fake: {*The spy MAY say anything he CAN say.*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

71 
"[ evsf \<in> set_pur; X \<in> synth(analz(knows Spy evsf)) ] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

74 

23755  75 
 Reception: {*If A sends a message X to B, then B might receive it*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

76 
"[ evsr \<in> set_pur; Says A B X \<in> set evsr ] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

23755  79 
 Start: 
14199  80 
{*Added start event which is outofband for SET: the Cardholder and 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

81 
the merchant agree on the amounts and uses @{text LID_M} as an 
14199  82 
identifier. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

83 
This is suggested by the External Interface Guide. The Programmer's 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

84 
Guide, in absence of @{text LID_M}, states that the merchant uniquely 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

85 
identifies the order out of some data contained in OrderDesc.*} 
14199  86 
"[evsStart \<in> set_pur; 
87 
Number LID_M \<notin> used evsStart; 

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

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

90 
LID_M \<notin> range CardSecret; 

91 
LID_M \<notin> range PANSecret ] 

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

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

94 
# evsStart \<in> set_pur" 

95 

23755  96 
 PInitReq: 
14199  97 
{*Purchase initialization, page 72 of Formal Protocol Desc.*} 
98 
"[evsPIReq \<in> set_pur; 

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

100 
Nonce Chall_C \<notin> used evsPIReq; 

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

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

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

104 

23755  105 
 PInitRes: 
14199  106 
{*Merchant replies with his own label XID and the encryption 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

107 
key certificate of his chosen Payment Gateway. Page 74 of Formal 
14199  108 
Protocol Desc. We use @{text LID_M} to identify Cardholder*} 
109 
"[evsPIRes \<in> set_pur; 

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

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

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

113 
Nonce Chall_M \<notin> used evsPIRes; 

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

115 
Number XID \<notin> used evsPIRes; 

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

118 
{Number LID_M, Number XID, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

119 
Nonce Chall_C, Nonce Chall_M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

120 
cert P (pubEK P) onlyEnc (priSK RCA)}) 
14199  121 
# evsPIRes \<in> set_pur" 
122 

23755  123 
 PReqUns: 
14199  124 
{*UNSIGNED Purchase request (CardSecret = 0). 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

125 
Page 79 of Formal Protocol Desc. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

126 
Merchant never sees the amount in clear. This holds of the real 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

127 
protocol, where XID identifies the transaction. We omit 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

128 
Hash{Number XID, Nonce (CardSecret k)} from PIHead because 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

129 
the CardSecret is 0 and because AuthReq treated the unsigned case 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

130 
very differently from the signed one anyway.*} 
23755  131 
"!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU. 
132 
[evsPReqU \<in> set_pur; 

14199  133 
C = Cardholder k; CardSecret k = 0; 
134 
Key KC1 \<notin> used evsPReqU; KC1 \<in> symKeys; 

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

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

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

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

139 
Gets C (sign (priSK M) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

140 
{Number LID_M, Number XID, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

141 
Nonce Chall_C, Nonce Chall_M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

142 
cert P EKj onlyEnc (priSK RCA)}) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

143 
\<in> set evsPReqU; 
14199  144 
Says C M {Number LID_M, Nonce Chall_C} \<in> set evsPReqU; 
145 
Notes C {Number LID_M, Transaction} \<in> set evsPReqU ] 

146 
==> Says C M 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

147 
{EXHcrypt KC1 EKj {PIHead, Hash OIData} (Pan (pan C)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

148 
OIData, Hash{PIHead, Pan (pan C)} } 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

149 
# Notes C {Key KC1, Agent M} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

150 
# evsPReqU \<in> set_pur" 
14199  151 

23755  152 
 PReqS: 
14199  153 
{*SIGNED Purchase request. Page 77 of Formal Protocol Desc. 
154 
We could specify the equation 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

155 
@{term "PIReqSigned = { PIDualSigned, OIDualSigned }"}, since the 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

156 
Formal Desc. gives PIHead the same format in the unsigned case. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

157 
However, there's little point, as P treats the signed and 
14199  158 
unsigned cases differently.*} 
23755  159 
"!!C Chall_C Chall_M EKj HOD KC2 LID_M M OIData 
160 
OIDualSigned OrderDesc P PANData PIData PIDualSigned 

161 
PIHead PurchAmt Transaction XID evsPReqS k. 

162 
[evsPReqS \<in> set_pur; 

14199  163 
C = Cardholder k; 
164 
CardSecret k \<noteq> 0; Key KC2 \<notin> used evsPReqS; KC2 \<in> symKeys; 

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

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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

169 
Hash{Number XID, Nonce (CardSecret k)}}; 
14199  170 
PANData = {Pan (pan C), Nonce (PANSecret k)}; 
171 
PIData = {PIHead, PANData}; 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

173 
EXcrypt KC2 EKj {PIHead, Hash OIData} PANData}; 
14199  174 
OIDualSigned = {OIData, Hash PIData}; 
175 
Gets C (sign (priSK M) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

176 
{Number LID_M, Number XID, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

177 
Nonce Chall_C, Nonce Chall_M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

178 
cert P EKj onlyEnc (priSK RCA)}) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

179 
\<in> set evsPReqS; 
14199  180 
Says C M {Number LID_M, Nonce Chall_C} \<in> set evsPReqS; 
181 
Notes C {Number LID_M, Transaction} \<in> set evsPReqS ] 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

183 
# Notes C {Key KC2, Agent M} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

184 
# evsPReqS \<in> set_pur" 
14199  185 

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

187 
Sent in response to Purchase Request.*} 

23755  188 
 AuthReq: 
14199  189 
"[ evsAReq \<in> set_pur; 
190 
Key KM \<notin> used evsAReq; KM \<in> symKeys; 

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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

194 
Nonce Chall_M}; 
14199  195 
CardSecret k \<noteq> 0 > 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

196 
P_I = {sign (priSK C) {HPIData, Hash OIData}, encPANData}; 
14199  197 
Gets M {P_I, OIData, HPIData} \<in> set evsAReq; 
198 
Says M C (sign (priSK M) {Number LID_M, Number XID, 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

199 
Nonce Chall_C, Nonce Chall_M, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

200 
cert P EKj onlyEnc (priSK RCA)}) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

201 
\<in> set evsAReq; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

202 
Notes M {Number LID_M, Agent P, Transaction} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

203 
\<in> set evsAReq ] 
14199  204 
==> Says M P 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

205 
(EncB (priSK M) KM (pubEK P) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

206 
{Number LID_M, Number XID, Hash OIData, HOD} P_I) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

207 
# evsAReq \<in> set_pur" 
14199  208 

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

210 
Page 99 of Formal Protocol Desc. 

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

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

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

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

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

216 

23755  217 
 AuthResUns: 
14199  218 
{*Authorization Response, UNSIGNED*} 
219 
"[ evsAResU \<in> set_pur; 

220 
C = Cardholder k; M = Merchant i; 

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

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

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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

226 
{Number LID_M, Number XID, HOIData, HOD} P_I) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

227 
\<in> set evsAResU ] 
14199  228 
==> Says P M 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

229 
(EncB (priSK P) KP (pubEK M) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

230 
{Number LID_M, Number XID, Number PurchAmt} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

231 
authCode) 
14199  232 
# evsAResU \<in> set_pur" 
233 

23755  234 
 AuthResS: 
14199  235 
{*Authorization Response, SIGNED*} 
236 
"[ evsAResS \<in> set_pur; 

237 
C = Cardholder k; 

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

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

241 
EXcrypt KC2 (pubEK P) {PIHead, HOIData} PANData}; 
14199  242 
PANData = {Pan (pan C), Nonce (PANSecret k)}; 
243 
PIData = {PIHead, PANData}; 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

245 
Hash{Number XID, Nonce (CardSecret k)}}; 
14199  246 
Gets P (EncB (priSK M) KM (pubEK P) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

247 
{Number LID_M, Number XID, HOIData, HOD} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

248 
P_I) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

249 
\<in> set evsAResS ] 
14199  250 
==> Says P M 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

251 
(EncB (priSK P) KP (pubEK M) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

252 
{Number LID_M, Number XID, Number PurchAmt} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

253 
authCode) 
14199  254 
# evsAResS \<in> set_pur" 
255 

23755  256 
 PRes: 
14199  257 
{*Purchase response.*} 
258 
"[ evsPRes \<in> set_pur; KP \<in> symKeys; M = Merchant i; 

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

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

261 
{Number LID_M, Number XID, Number PurchAmt} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

262 
authCode) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

263 
\<in> set evsPRes; 
14199  264 
Gets M {Number LID_M, Nonce Chall_C} \<in> set evsPRes; 
265 
Says M P 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

266 
(EncB (priSK M) KM (pubEK P) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

267 
{Number LID_M, Number XID, Hash OIData, HOD} P_I) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

268 
\<in> set evsPRes; 
14199  269 
Notes M {Number LID_M, Agent P, Transaction} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

270 
\<in> set evsPRes 
14199  271 
] 
272 
==> Says M C 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

273 
(sign (priSK M) {Number LID_M, Number XID, Nonce Chall_C, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

274 
Hash (Number PurchAmt)}) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

275 
# evsPRes \<in> set_pur" 
14199  276 

277 

278 
specification (CardSecret PANSecret) 

279 
inj_CardSecret: "inj CardSecret" 

280 
inj_PANSecret: "inj PANSecret" 

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

282 
{*No CardSecret equals any PANSecret*} 

35703
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
33028
diff
changeset

283 
apply (rule_tac x="curry prod_encode 0" in exI) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
33028
diff
changeset

284 
apply (rule_tac x="curry prod_encode 1" in exI) 
29cb504abbb5
convert SET_Protocol to use Nat_Bijection library
huffman
parents:
33028
diff
changeset

285 
apply (simp add: prod_encode_eq inj_on_def) 
14199  286 
done 
287 

288 
declare Says_imp_knows_Spy [THEN parts.Inj, dest] 

289 
declare parts.Body [dest] 

290 
declare analz_into_parts [dest] 

291 
declare Fake_parts_insert_in_Un [dest] 

292 

293 
declare CardSecret_neq_PANSecret [iff] 

294 
CardSecret_neq_PANSecret [THEN not_sym, iff] 

295 
declare inj_CardSecret [THEN inj_eq, iff] 

296 
inj_PANSecret [THEN inj_eq, iff] 

297 

298 

299 
subsection{*Possibility Properties*} 

300 

301 
lemma Says_to_Gets: 

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

303 
by (rule set_pur.Reception, auto) 

304 

14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

305 
text{*Possibility for UNSIGNED purchases. Note that we need to ensure 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

306 
that XID differs from OrderDesc and PurchAmt, since it is supposed to be 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

307 
a unique number!*} 
14199  308 
lemma possibility_Uns: 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

309 
"[ CardSecret k = 0; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

310 
C = Cardholder k; M = Merchant i; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

311 
Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

312 
KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

313 
KC < KM; KM < KP; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

314 
Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret; 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

315 
Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

316 
Chall_C < Chall_M; 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

317 
Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

318 
Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

319 
LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt ] 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

320 
==> \<exists>evs \<in> set_pur. 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

321 
Says M C 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

322 
(sign (priSK M) 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

323 
{Number LID_M, Number XID, Nonce Chall_C, 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

324 
Hash (Number PurchAmt)}) 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

325 
\<in> set evs" 
14199  326 
apply (intro exI bexI) 
327 
apply (rule_tac [2] 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

328 
set_pur.Nil 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

329 
[THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

330 
THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

331 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

332 
THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

333 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

334 
THEN set_pur.PReqUns [of concl: C M KC], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

335 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

336 
THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

337 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

338 
THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

339 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

340 
THEN set_pur.PRes]) 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

341 
apply basic_possibility 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

342 
apply (simp_all add: used_Cons symKeys_neq_imp_neq) 
14199  343 
done 
344 

345 
lemma possibility_S: 

14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

346 
"[ CardSecret k \<noteq> 0; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

347 
C = Cardholder k; M = Merchant i; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

348 
Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

349 
KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

350 
KC < KM; KM < KP; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

351 
Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret; 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

352 
Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret; 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

353 
Chall_C < Chall_M; 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

354 
Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

355 
Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret; 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

356 
LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt ] 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

357 
==> \<exists>evs \<in> set_pur. 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

358 
Says M C 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

359 
(sign (priSK M) {Number LID_M, Number XID, Nonce Chall_C, 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

360 
Hash (Number PurchAmt)}) 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

361 
\<in> set evs" 
14199  362 
apply (intro exI bexI) 
363 
apply (rule_tac [2] 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

364 
set_pur.Nil 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

365 
[THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

366 
THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

367 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

368 
THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

369 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

370 
THEN set_pur.PReqS [of concl: C M _ _ KC], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

371 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

372 
THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

373 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

374 
THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID], 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

375 
THEN Says_to_Gets, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

376 
THEN set_pur.PRes]) 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

377 
apply basic_possibility 
14206
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

378 
apply (auto simp add: used_Cons symKeys_neq_imp_neq) 
14199  379 
done 
380 

15481  381 
text{*General facts about message reception*} 
14199  382 
lemma Gets_imp_Says: 
383 
"[ Gets B X \<in> set evs; evs \<in> set_pur ] 

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

385 
apply (erule rev_mp) 

386 
apply (erule set_pur.induct, auto) 

387 
done 

388 

389 
lemma Gets_imp_knows_Spy: 

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

391 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

392 

393 
declare Gets_imp_knows_Spy [THEN parts.Inj, dest] 

394 

395 
text{*Forwarding lemmas, to aid simplification*} 

396 

397 
lemma AuthReq_msg_in_parts_spies: 

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

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

400 
by auto 

401 

402 
lemma AuthReq_msg_in_analz_spies: 

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

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

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

406 

407 

408 
subsection{*Proofs on Asymmetric Keys*} 

409 

410 
text{*Private Keys are Secret*} 

411 

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

413 
lemma Spy_see_private_Key [simp]: 

414 
"evs \<in> set_pur 

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

416 
apply (erule set_pur.induct) 

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

418 
apply auto 

419 
done 

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

421 

422 
lemma Spy_analz_private_Key [simp]: 

423 
"evs \<in> set_pur ==> 

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

425 
by auto 

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

427 

428 
text{*rewriting rule for priEK's*} 

429 
lemma parts_image_priEK: 

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

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

432 
by auto 

433 

15481  434 
text{*trivial proof because @{term"priEK C"} never appears even in 
435 
@{term "parts evs"}. *} 

14199  436 
lemma analz_image_priEK: 
437 
"evs \<in> set_pur ==> 

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

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

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

441 

15481  442 

14199  443 
subsection{*Public Keys in Certificates are Correct*} 
444 

445 
lemma Crypt_valid_pubEK [dest!]: 

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

447 
\<in> parts (knows Spy evs); 

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

15481  449 
by (erule rev_mp, erule set_pur.induct, auto) 
14199  450 

451 
lemma Crypt_valid_pubSK [dest!]: 

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

453 
\<in> parts (knows Spy evs); 

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

15481  455 
by (erule rev_mp, erule set_pur.induct, auto) 
14199  456 

457 
lemma certificate_valid_pubEK: 

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

459 
evs \<in> set_pur ] 

460 
==> EKi = pubEK C" 

461 
by (unfold cert_def signCert_def, auto) 

462 

463 
lemma certificate_valid_pubSK: 

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

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

466 
by (unfold cert_def signCert_def, auto) 

467 

468 
lemma Says_certificate_valid [simp]: 

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

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

471 
evs \<in> set_pur ] 

472 
==> EK = pubEK C" 

473 
by (unfold sign_def, auto) 

474 

475 
lemma Gets_certificate_valid [simp]: 

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

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

478 
evs \<in> set_pur ] 

479 
==> EK = pubEK C" 

480 
by (frule Gets_imp_Says, auto) 

481 

24123  482 
method_setup valid_certificate_tac = {* 
30549  483 
Args.goal_spec >> (fn quant => 
484 
K (SIMPLE_METHOD'' quant (fn i => 

485 
EVERY [ftac @{thm Gets_certificate_valid} i, 

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

42814  487 
*} 
14199  488 

489 

490 
subsection{*Proofs on Symmetric Keys*} 

491 

492 
text{*Nobody can have used nonexistent keys!*} 

493 
lemma new_keys_not_used [rule_format,simp]: 

494 
"evs \<in> set_pur 

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

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

497 
apply (erule set_pur.induct) 

24123  498 
apply (valid_certificate_tac [8]) {*PReqS*} 
499 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  500 
apply auto 
501 
apply (force dest!: usedI keysFor_parts_insert) {*Fake*} 

502 
done 

503 

504 
lemma new_keys_not_analzd: 

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

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

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

508 

509 
lemma Crypt_parts_imp_used: 

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

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

512 
apply (rule ccontr) 

513 
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor) 

514 
done 

515 

516 
lemma Crypt_analz_imp_used: 

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

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

519 
by (blast intro: Crypt_parts_imp_used) 

520 

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

522 

523 
lemma gen_new_keys_not_used: 

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

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

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

527 
by auto 

528 

529 
lemma gen_new_keys_not_analzd: 

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

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

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

533 

534 
lemma analz_Key_image_insert_eq: 

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

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

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

538 
by (simp add: gen_new_keys_not_analzd) 

539 

540 

541 
subsection{*Secrecy of Symmetric Keys*} 

542 

543 
lemma Key_analz_image_Key_lemma: 

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

545 
==> 

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

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

548 

549 

550 
lemma symKey_compromise: 

15205  551 
"evs \<in> set_pur \<Longrightarrow> 
14199  552 
(\<forall>SK KK. SK \<in> symKeys \<longrightarrow> 
15205  553 
(\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) \<longrightarrow> 
554 
(Key SK \<in> analz (Key`KK \<union> (knows Spy evs))) = 

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

14199  556 
apply (erule set_pur.induct) 
557 
apply (rule_tac [!] allI)+ 

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

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

24123  560 
apply (valid_certificate_tac [8]) {*PReqS*} 
561 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  562 
apply (simp_all 
563 
del: image_insert image_Un imp_disjL 

564 
add: analz_image_keys_simps disj_simps 

565 
analz_Key_image_insert_eq notin_image_iff 

566 
analz_insert_simps analz_image_priEK) 

24123  567 
{*8 seconds on a 1.6GHz machine*} 
14199  568 
apply spy_analz {*Fake*} 
569 
apply (blast elim!: ballE)+ {*PReq: unsigned and signed*} 

570 
done 

571 

572 

573 

574 
subsection{*Secrecy of Nonces*} 

575 

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

577 
lemma Nonce_analz_image_Key_lemma: 

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

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

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

581 

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

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

584 
lemma Nonce_compromise [rule_format (no_asm)]: 

585 
"evs \<in> set_pur ==> 

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

14256  587 
(Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) = 
14199  588 
(Nonce N \<in> analz (knows Spy evs)))" 
589 
apply (erule set_pur.induct) 

590 
apply (rule_tac [!] allI)+ 

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

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

24123  593 
apply (valid_certificate_tac [8]) {*PReqS*} 
594 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  595 
apply (simp_all 
596 
del: image_insert image_Un imp_disjL 

597 
add: analz_image_keys_simps disj_simps symKey_compromise 

598 
analz_Key_image_insert_eq notin_image_iff 

599 
analz_insert_simps analz_image_priEK) 

24123  600 
{*8 seconds on a 1.6GHz machine*} 
14199  601 
apply spy_analz {*Fake*} 
602 
apply (blast elim!: ballE) {*PReqS*} 

603 
done 

604 

605 
lemma PANSecret_notin_spies: 

14256  606 
"[Nonce (PANSecret k) \<in> analz (knows Spy evs); evs \<in> set_pur] 
607 
==> 

14199  608 
(\<exists>V W X Y KC2 M. \<exists>P \<in> bad. 
609 
Says (Cardholder k) M 

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

611 
V} \<in> set evs)" 

14256  612 
apply (erule rev_mp) 
14199  613 
apply (erule set_pur.induct) 
614 
apply (frule_tac [9] AuthReq_msg_in_analz_spies) 

24123  615 
apply (valid_certificate_tac [8]) {*PReqS*} 
14199  616 
apply (simp_all 
617 
del: image_insert image_Un imp_disjL 

618 
add: analz_image_keys_simps disj_simps 

619 
symKey_compromise pushes sign_def Nonce_compromise 

620 
analz_Key_image_insert_eq notin_image_iff 

621 
analz_insert_simps analz_image_priEK) 

24123  622 
{*2.5 seconds on a 1.6GHz machine*} 
14199  623 
apply spy_analz 
624 
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) 

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

626 
Gets_imp_knows_Spy [THEN analz.Inj]) 

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

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

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

630 
done 

631 

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

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

634 
lemma CardSecret_notin_spies: 

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

636 
by (erule set_pur.induct, auto) 

637 

15214  638 

14199  639 
subsection{*Confidentiality of PAN*} 
640 

641 
lemma analz_image_pan_lemma: 

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

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

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

645 

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

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

648 
lemma analz_image_pan [rule_format (no_asm)]: 

649 
"evs \<in> set_pur ==> 

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

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

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

653 
apply (erule set_pur.induct) 

654 
apply (rule_tac [!] allI impI)+ 

655 
apply (rule_tac [!] analz_image_pan_lemma)+ 

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

24123  657 
apply (valid_certificate_tac [8]) {*PReqS*} 
658 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  659 
apply (simp_all 
660 
del: image_insert image_Un imp_disjL 

661 
add: analz_image_keys_simps 

662 
symKey_compromise pushes sign_def 

663 
analz_Key_image_insert_eq notin_image_iff 

664 
analz_insert_simps analz_image_priEK) 

24123  665 
{*7 seconds on a 1.6GHz machine*} 
14199  666 
apply spy_analz {*Fake*} 
667 
apply auto 

668 
done 

669 

670 
lemma analz_insert_pan: 

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

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

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

674 
by (simp del: image_insert image_Un 

675 
add: analz_image_keys_simps analz_image_pan) 

676 

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

15214  678 
theorem pan_confidentiality_unsigned: 
14199  679 
"[ Pan (pan C) \<in> analz(knows Spy evs); C = Cardholder k; 
680 
CardSecret k = 0; evs \<in> set_pur] 

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

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

683 
\<in> set evs & 

684 
P \<in> bad" 

685 
apply (erule rev_mp) 

686 
apply (erule set_pur.induct) 

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

24123  688 
apply (valid_certificate_tac [8]) {*PReqS*} 
689 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  690 
apply (simp_all 
691 
del: image_insert image_Un imp_disjL 

692 
add: analz_image_keys_simps analz_insert_pan analz_image_pan 

693 
notin_image_iff 

694 
analz_insert_simps analz_image_priEK) 

24123  695 
{*3 seconds on a 1.6GHz machine*} 
14199  696 
apply spy_analz {*Fake*} 
697 
apply blast {*PReqUns: unsigned*} 

698 
apply force {*PReqS: signed*} 

699 
done 

700 

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

15214  702 
theorem pan_confidentiality_signed: 
703 
"[Pan (pan C) \<in> analz(knows Spy evs); C = Cardholder k; 

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

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

706 
Says C M {{PIDualSign_1, 

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

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

14199  709 
apply (erule rev_mp) 
710 
apply (erule set_pur.induct) 

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

24123  712 
apply (valid_certificate_tac [8]) {*PReqS*} 
713 
apply (valid_certificate_tac [7]) {*PReqUns*} 

14199  714 
apply (simp_all 
715 
del: image_insert image_Un imp_disjL 

716 
add: analz_image_keys_simps analz_insert_pan analz_image_pan 

717 
notin_image_iff 

718 
analz_insert_simps analz_image_priEK) 

24123  719 
{*3 seconds on a 1.6GHz machine*} 
14199  720 
apply spy_analz {*Fake*} 
721 
apply force {*PReqUns: unsigned*} 

722 
apply blast {*PReqS: signed*} 

723 
done 

724 

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

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

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

728 

729 

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

731 

732 
lemma M_Notes_PG: 

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

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

15481  735 
by (erule rev_mp, erule set_pur.induct, simp_all) 
14199  736 

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

738 
(Payment Gateway)*} 

739 
lemma goodM_gives_correct_PG: 

740 
"[ MsgPInitRes = 

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

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

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

744 
==> \<exists>j trans. 

745 
P = PG j & 

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

747 
apply clarify 

748 
apply (erule rev_mp) 

749 
apply (erule set_pur.induct) 

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

751 
apply simp_all 

752 
apply (blast intro: M_Notes_PG)+ 

753 
done 

754 

755 
lemma C_gets_correct_PG: 

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

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

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

759 
==> \<exists>j trans. 

760 
P = PG j & 

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

762 
EKj = pubEK P" 

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

764 

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

766 
lemma C_verifies_PInitRes: 

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

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

768 
cert P EKj onlyEnc (priSK RCA)}; 
14199  769 
Crypt (priSK M) (Hash MsgPInitRes) \<in> parts (knows Spy evs); 
770 
evs \<in> set_pur; M \<notin> bad] 

771 
==> \<exists>j trans. 

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

773 
P = PG j & 

774 
EKj = pubEK P" 

775 
apply clarify 

776 
apply (erule rev_mp) 

777 
apply (erule set_pur.induct) 

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

779 
apply simp_all 

780 
apply (blast intro: M_Notes_PG)+ 

781 
done 

782 

783 
text{*Corollary of previous one*} 

784 
lemma Says_C_PInitRes: 

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

786 
{Number LID_M, Number XID, 

787 
Nonce Chall_C, Nonce Chall_M, 

788 
cert P EKj onlyEnc (priSK RCA)}) 

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

790 
==> \<exists>j trans. 

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

792 
P = PG j & 

793 
EKj = pubEK (PG j)" 

794 
apply (frule Says_certificate_valid) 

795 
apply (auto simp add: sign_def) 

796 
apply (blast dest: refl [THEN goodM_gives_correct_PG]) 

797 
apply (blast dest: refl [THEN C_verifies_PInitRes]) 

798 
done 

799 

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

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

802 
lemma P_verifies_AuthReq: 

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

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

805 
\<in> parts (knows Spy evs); 

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

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

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

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

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

811 
\<in> set evs" 

812 
apply clarify 

813 
apply (erule rev_mp) 

814 
apply (erule set_pur.induct, simp_all) 

815 
apply (frule_tac [4] M_Notes_PG, auto) 

816 
done 

817 

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

15481  819 
the identifying tags and the purchase amount, which he can verify. 
14199  820 
(Although the spec has SIGNED and UNSIGNED forms of AuthRes, they 
16474  821 
send the same message to M.) The conclusion is weak: M is existentially 
822 
quantified! That is because Authorization Response does not refer to M, while 

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

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

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

826 
otherwise the Spy could create that message.*} 

15214  827 
theorem M_verifies_AuthRes: 
16474  828 
"[ MsgAuthRes = {{Number LID_M, Number XID, Number PurchAmt}, 
829 
Hash authCode}; 

14199  830 
Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs); 
16474  831 
PG j \<notin> bad; evs \<in> set_pur] 
832 
==> \<exists>M KM KP HOIData HOD P_I. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

833 
Gets (PG j) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

834 
(EncB (priSK M) KM (pubEK (PG j)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

835 
{Number LID_M, Number XID, HOIData, HOD} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

836 
P_I) \<in> set evs & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

837 
Says (PG j) M 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

838 
(EncB (priSK (PG j)) KP (pubEK M) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

839 
{Number LID_M, Number XID, Number PurchAmt} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

840 
authCode) \<in> set evs" 
14199  841 
apply clarify 
842 
apply (erule rev_mp) 

843 
apply (erule set_pur.induct) 

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

845 
apply simp_all 

846 
apply blast+ 

847 
done 

848 

849 

850 
subsection{*Proofs for Unsigned Purchases*} 

851 

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

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

854 
lemma C_determines_EKj: 

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

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

857 
PIHead = {Number LID_M, Trans_details}; 

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

859 
==> \<exists>trans j. 

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

861 
EKj = pubEK (PG j)" 

862 
apply clarify 

863 
apply (erule rev_mp) 

864 
apply (erule set_pur.induct, simp_all) 

24123  865 
apply (valid_certificate_tac [2]) {*PReqUns*} 
14199  866 
apply auto 
867 
apply (blast dest: Gets_imp_Says Says_C_PInitRes) 

868 
done 

869 

870 

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

872 
lemma unique_LID_M: 

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

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

875 
Number PA} \<in> set evs; 

876 
evs \<in> set_pur] 

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

878 
apply (erule rev_mp) 

879 
apply (erule rev_mp) 

880 
apply (erule set_pur.induct, simp_all) 

881 
apply (force dest!: Notes_imp_parts_subset_used) 

882 
done 

883 

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

885 
lemma unique_LID_M2: 

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

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

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

889 
apply (erule rev_mp) 

890 
apply (erule rev_mp) 

891 
apply (erule set_pur.induct, simp_all) 

892 
apply (force dest!: Notes_imp_parts_subset_used) 

893 
done 

894 

895 
text{*Lemma needed below: for the case that 

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

897 
lemma signed_imp_used: 

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

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

900 
apply (erule rev_mp) 

901 
apply (erule set_pur.induct) 

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

903 
apply simp_all 

904 
apply safe 

905 
apply blast+ 

906 
done 

907 

908 
text{*Similar, with nested Hash*} 

909 
lemma signed_Hash_imp_used: 

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

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

912 
apply (erule rev_mp) 

913 
apply (erule set_pur.induct) 

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

915 
apply simp_all 

916 
apply safe 

917 
apply blast+ 

918 
done 

919 

920 
text{*Lemma needed below: for the case that 

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

922 
lemma PRes_imp_LID_used: 

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

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

925 
by (drule signed_imp_used, auto) 

926 

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

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

929 
lemma C_verifies_PRes_lemma: 

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

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

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

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

934 
Hash (Number PurchAmt)}; 

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

936 
==> \<exists>j KP. 

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

938 
\<in> set evs & 

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

940 
{Number LID_M, Number XID, Number PurchAmt} 

941 
authCode) 

942 
\<in> set evs & 

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

944 
apply clarify 

945 
apply (erule rev_mp) 

946 
apply (erule rev_mp) 

947 
apply (erule set_pur.induct) 

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

949 
apply simp_all 

950 
apply blast 

951 
apply blast 

952 
apply (blast dest: PRes_imp_LID_used) 

953 
apply (frule M_Notes_PG, auto) 

954 
apply (blast dest: unique_LID_M) 

955 
done 

956 

15214  957 
text{*When the Cardholder receives Purchase Response from an uncompromised 
958 
Merchant, he knows that M sent it. He also knows that M received a message signed 

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

960 
theorem C_verifies_PRes: 

14199  961 
"[ MsgPRes = {Number LID_M, Number XID, Nonce Chall_C, 
962 
Hash (Number PurchAmt)}; 

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

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

965 
Number PurchAmt} \<in> set evs; 

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

967 
==> \<exists>P KP trans. 

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

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

970 
{Number LID_M, Number XID, Number PurchAmt} 

15214  971 
authCode) \<in> set evs & 
14199  972 
Says M C (sign (priSK M) MsgPRes) \<in> set evs" 
973 
apply (rule C_verifies_PRes_lemma [THEN exE]) 

974 
apply (auto simp add: sign_def) 

975 
done 

976 

977 
subsection{*Proofs for Signed Purchases*} 

978 

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

980 

981 
lemma Crypt_imp_Says_Cardholder: 

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

983 
\<in> parts (knows Spy evs); 

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

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

986 
evs \<in> set_pur] 

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

988 
Says (Cardholder k) M {{shash, 

989 
Crypt K 

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

991 
Crypt EK {Key K, PANData}}, 

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

993 
apply (erule rev_mp) 

994 
apply (erule rev_mp) 

995 
apply (erule rev_mp) 

996 
apply (erule set_pur.induct, analz_mono_contra) 

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

998 
apply simp_all 

999 
apply auto 

1000 
done 

1001 

1002 
lemma Says_PReqS_imp_trans_details_C: 

1003 
"[ MsgPReqS = {{shash, 

1004 
Crypt K 

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

1006 
cryptek}, data}; 

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

1008 
evs \<in> set_pur ] 

1009 
==> \<exists>trans. 

1010 
Notes (Cardholder k) 

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

1012 
\<in> set evs" 

1013 
apply (erule rev_mp) 

1014 
apply (erule rev_mp) 

1015 
apply (erule set_pur.induct) 

1016 
apply (simp_all (no_asm_simp)) 

1017 
apply auto 

1018 
done 

1019 

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

1021 
lemma Notes_Cardholder_self_False: 

1022 
"[Notes (Cardholder k) 

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

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

15481  1025 
by (erule rev_mp, erule set_pur.induct, auto) 
14199  1026 

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

1028 
Using XID he knows it was intended for him. 

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

15214  1030 
theorem M_verifies_Signed_PReq: 
1031 
"[ MsgDualSign = {HPIData, Hash OIData}; 

1032 
OIData = {Number LID_M, etc}; 

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

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

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

1036 
==> \<exists>PIData PICrypt. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

1037 
HPIData = Hash PIData & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

1038 
Says C M {{sign (priSK C) MsgDualSign, PICrypt}, OIData, Hash PIData} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

1039 
\<in> set evs" 
14199  1040 
apply clarify 
1041 
apply (erule rev_mp) 

1042 
apply (erule rev_mp) 

1043 
apply (erule set_pur.induct) 

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

1045 
apply simp_all 

1046 
apply blast 

32404  1047 
apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used) 
1048 
apply (metis unique_LID_M) 

14199  1049 
apply (blast dest!: Notes_Cardholder_self_False) 
1050 
done 

1051 

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

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

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

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

15214  1056 
theorem P_verifies_Signed_PReq: 
14199  1057 
"[ MsgDualSign = {Hash PIData, HOIData}; 
1058 
PIData = {PIHead, PANData}; 

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

1060 
TransStain}; 

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

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

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

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

1065 
HOIData = Hash OIData & 

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

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

1068 
EXcrypt K (pubEK (PG j)) 

1069 
{PIHead, Hash OIData} PANData}, 

1070 
OIData, Hash PIData} 

1071 
\<in> set evs" 

1072 
apply clarify 

1073 
apply (erule rev_mp) 

1074 
apply (erule set_pur.induct, simp_all) 

1075 
apply (auto dest!: C_gets_correct_PG) 

1076 
done 

1077 

1078 
lemma C_determines_EKj_signed: 

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

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

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

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

1083 
==> \<exists> trans j. 

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

1085 
EKj = pubEK (PG j)" 

1086 
apply clarify 

1087 
apply (erule rev_mp) 

1088 
apply (erule set_pur.induct, simp_all, auto) 

1089 
apply (blast dest: C_gets_correct_PG) 

1090 
done 

1091 

1092 
lemma M_Says_AuthReq: 

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

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

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

1096 
==> \<exists>j trans KM. 

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

1098 
Says M (PG j) 

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

1100 
\<in> set evs" 

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

1102 
apply (auto simp add: sign_def) 

1103 
done 

1104 

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

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

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

1108 
lemma Signed_PReq_imp_Says_Cardholder: 

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

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

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

1112 
TransStain}; 

1113 
PIData = {PIHead, PANData}; 

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

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

1116 
==> \<exists>KC EKj. 

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

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

1119 
OIData, Hash PIData} 

1120 
\<in> set evs" 

1121 
apply clarify 

1122 
apply (erule rev_mp) 

1123 
apply (erule rev_mp) 

1124 
apply (erule set_pur.induct, simp_all, auto) 

1125 
done 

1126 

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

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

1129 
P; instead C and M both send 

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

1131 
and P compares the two copies of HOD. 

1132 

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

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

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

1136 
the EXcrypt involves the correct PG's key. 

1137 
*} 

15214  1138 
theorem P_sees_CM_agreement: 
14199  1139 
"[ AuthReqData = {Number LID_M, Number XID, HOIData, HOD}; 
1140 
KC \<in> symKeys; 

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

1142 
\<in> set evs; 

1143 
C = Cardholder k; 

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

1145 
P_I = {PI_sign, 

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

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

1148 
PIData = {PIHead, PANData}; 

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

1150 
TransStain}; 

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

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

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

1154 
HOIData = Hash OIData & 

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

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

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

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

1159 
P_I' = {PI_sign, 

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

1161 
P_I'' = {PI_sign, 

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

1163 
apply clarify 

1164 
apply (rule exE) 

1165 
apply (rule P_verifies_Signed_PReq [OF refl refl refl]) 

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

1167 
apply (assumption+, clarify, simp) 

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

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

1170 
done 

1171 

1172 
end 