|
1 (* Title: HOL/SET_Protocol/Purchase.thy |
|
2 Author: Giampaolo Bella |
|
3 Author: Fabio Massacci |
|
4 Author: Lawrence C Paulson |
|
5 *) |
|
6 |
|
7 header{*Purchase Phase of SET*} |
|
8 |
|
9 theory Purchase |
|
10 imports Public_SET |
|
11 begin |
|
12 |
|
13 text{* |
|
14 Note: nonces seem to consist of 20 bytes. That includes both freshness |
|
15 challenges (Chall-EE, 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 out-of-bad on the value of @{text LID_M} (for instance a cookie in a web |
|
34 transaction etc.). This out-of-band 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" |
|
57 --{*Maps Cardholders to CardSecrets. |
|
58 A CardSecret of 0 means no cerificate, must use unsigned format.*} |
|
59 |
|
60 PANSecret :: "nat => nat" |
|
61 --{*Maps Cardholders to PANSecrets.*} |
|
62 |
|
63 inductive_set |
|
64 set_pur :: "event list set" |
|
65 where |
|
66 |
|
67 Nil: --{*Initial trace is empty*} |
|
68 "[] \<in> set_pur" |
|
69 |
|
70 | Fake: --{*The spy MAY say anything he CAN say.*} |
|
71 "[| evsf \<in> set_pur; X \<in> synth(analz(knows Spy evsf)) |] |
|
72 ==> Says Spy B X # evsf \<in> set_pur" |
|
73 |
|
74 |
|
75 | Reception: --{*If A sends a message X to B, then B might receive it*} |
|
76 "[| evsr \<in> set_pur; Says A B X \<in> set evsr |] |
|
77 ==> Gets B X # evsr \<in> set_pur" |
|
78 |
|
79 | Start: |
|
80 --{*Added start event which is out-of-band for SET: the Cardholder and |
|
81 the merchant agree on the amounts and uses @{text LID_M} as an |
|
82 identifier. |
|
83 This is suggested by the External Interface Guide. The Programmer's |
|
84 Guide, in absence of @{text LID_M}, states that the merchant uniquely |
|
85 identifies the order out of some data contained in OrderDesc.*} |
|
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 |
|
96 | PInitReq: |
|
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 |
|
105 | PInitRes: |
|
106 --{*Merchant replies with his own label XID and the encryption |
|
107 key certificate of his chosen Payment Gateway. Page 74 of Formal |
|
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) |
|
118 {|Number LID_M, Number XID, |
|
119 Nonce Chall_C, Nonce Chall_M, |
|
120 cert P (pubEK P) onlyEnc (priSK RCA)|}) |
|
121 # evsPIRes \<in> set_pur" |
|
122 |
|
123 | PReqUns: |
|
124 --{*UNSIGNED Purchase request (CardSecret = 0). |
|
125 Page 79 of Formal Protocol Desc. |
|
126 Merchant never sees the amount in clear. This holds of the real |
|
127 protocol, where XID identifies the transaction. We omit |
|
128 Hash{|Number XID, Nonce (CardSecret k)|} from PIHead because |
|
129 the CardSecret is 0 and because AuthReq treated the unsigned case |
|
130 very differently from the signed one anyway.*} |
|
131 "!!Chall_C Chall_M OrderDesc P PurchAmt XID evsPReqU. |
|
132 [|evsPReqU \<in> set_pur; |
|
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) |
|
140 {|Number LID_M, Number XID, |
|
141 Nonce Chall_C, Nonce Chall_M, |
|
142 cert P EKj onlyEnc (priSK RCA)|}) |
|
143 \<in> set evsPReqU; |
|
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 |
|
147 {|EXHcrypt KC1 EKj {|PIHead, Hash OIData|} (Pan (pan C)), |
|
148 OIData, Hash{|PIHead, Pan (pan C)|} |} |
|
149 # Notes C {|Key KC1, Agent M|} |
|
150 # evsPReqU \<in> set_pur" |
|
151 |
|
152 | PReqS: |
|
153 --{*SIGNED Purchase request. Page 77 of Formal Protocol Desc. |
|
154 We could specify the equation |
|
155 @{term "PIReqSigned = {| PIDualSigned, OIDualSigned |}"}, since the |
|
156 Formal Desc. gives PIHead the same format in the unsigned case. |
|
157 However, there's little point, as P treats the signed and |
|
158 unsigned cases differently.*} |
|
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; |
|
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, |
|
169 Hash{|Number XID, Nonce (CardSecret k)|}|}; |
|
170 PANData = {|Pan (pan C), Nonce (PANSecret k)|}; |
|
171 PIData = {|PIHead, PANData|}; |
|
172 PIDualSigned = {|sign (priSK C) {|Hash PIData, Hash OIData|}, |
|
173 EXcrypt KC2 EKj {|PIHead, Hash OIData|} PANData|}; |
|
174 OIDualSigned = {|OIData, Hash PIData|}; |
|
175 Gets C (sign (priSK M) |
|
176 {|Number LID_M, Number XID, |
|
177 Nonce Chall_C, Nonce Chall_M, |
|
178 cert P EKj onlyEnc (priSK RCA)|}) |
|
179 \<in> set evsPReqS; |
|
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|} |
|
183 # Notes C {|Key KC2, Agent M|} |
|
184 # evsPReqS \<in> set_pur" |
|
185 |
|
186 --{*Authorization Request. Page 92 of Formal Protocol Desc. |
|
187 Sent in response to Purchase Request.*} |
|
188 | AuthReq: |
|
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, |
|
194 Nonce Chall_M|}; |
|
195 CardSecret k \<noteq> 0 --> |
|
196 P_I = {|sign (priSK C) {|HPIData, Hash OIData|}, encPANData|}; |
|
197 Gets M {|P_I, OIData, HPIData|} \<in> set evsAReq; |
|
198 Says M C (sign (priSK M) {|Number LID_M, Number XID, |
|
199 Nonce Chall_C, Nonce Chall_M, |
|
200 cert P EKj onlyEnc (priSK RCA)|}) |
|
201 \<in> set evsAReq; |
|
202 Notes M {|Number LID_M, Agent P, Transaction|} |
|
203 \<in> set evsAReq |] |
|
204 ==> Says M P |
|
205 (EncB (priSK M) KM (pubEK P) |
|
206 {|Number LID_M, Number XID, Hash OIData, HOD|} P_I) |
|
207 # evsAReq \<in> set_pur" |
|
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 |
|
217 | AuthResUns: |
|
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) |
|
226 {|Number LID_M, Number XID, HOIData, HOD|} P_I) |
|
227 \<in> set evsAResU |] |
|
228 ==> Says P M |
|
229 (EncB (priSK P) KP (pubEK M) |
|
230 {|Number LID_M, Number XID, Number PurchAmt|} |
|
231 authCode) |
|
232 # evsAResU \<in> set_pur" |
|
233 |
|
234 | AuthResS: |
|
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|}, |
|
241 EXcrypt KC2 (pubEK P) {|PIHead, HOIData|} PANData|}; |
|
242 PANData = {|Pan (pan C), Nonce (PANSecret k)|}; |
|
243 PIData = {|PIHead, PANData|}; |
|
244 PIHead = {|Number LID_M, Number XID, HOD, Number PurchAmt, Agent M, |
|
245 Hash{|Number XID, Nonce (CardSecret k)|}|}; |
|
246 Gets P (EncB (priSK M) KM (pubEK P) |
|
247 {|Number LID_M, Number XID, HOIData, HOD|} |
|
248 P_I) |
|
249 \<in> set evsAResS |] |
|
250 ==> Says P M |
|
251 (EncB (priSK P) KP (pubEK M) |
|
252 {|Number LID_M, Number XID, Number PurchAmt|} |
|
253 authCode) |
|
254 # evsAResS \<in> set_pur" |
|
255 |
|
256 | PRes: |
|
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) |
|
261 {|Number LID_M, Number XID, Number PurchAmt|} |
|
262 authCode) |
|
263 \<in> set evsPRes; |
|
264 Gets M {|Number LID_M, Nonce Chall_C|} \<in> set evsPRes; |
|
265 Says M P |
|
266 (EncB (priSK M) KM (pubEK P) |
|
267 {|Number LID_M, Number XID, Hash OIData, HOD|} P_I) |
|
268 \<in> set evsPRes; |
|
269 Notes M {|Number LID_M, Agent P, Transaction|} |
|
270 \<in> set evsPRes |
|
271 |] |
|
272 ==> Says M C |
|
273 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, |
|
274 Hash (Number PurchAmt)|}) |
|
275 # evsPRes \<in> set_pur" |
|
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*} |
|
283 apply (rule_tac x="curry nat2_to_nat 0" in exI) |
|
284 apply (rule_tac x="curry nat2_to_nat 1" in exI) |
|
285 apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def) |
|
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 |
|
305 text{*Possibility for UNSIGNED purchases. Note that we need to ensure |
|
306 that XID differs from OrderDesc and PurchAmt, since it is supposed to be |
|
307 a unique number!*} |
|
308 lemma possibility_Uns: |
|
309 "[| CardSecret k = 0; |
|
310 C = Cardholder k; M = Merchant i; |
|
311 Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; |
|
312 KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; |
|
313 KC < KM; KM < KP; |
|
314 Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret; |
|
315 Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret; |
|
316 Chall_C < Chall_M; |
|
317 Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret; |
|
318 Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret; |
|
319 LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] |
|
320 ==> \<exists>evs \<in> set_pur. |
|
321 Says M C |
|
322 (sign (priSK M) |
|
323 {|Number LID_M, Number XID, Nonce Chall_C, |
|
324 Hash (Number PurchAmt)|}) |
|
325 \<in> set evs" |
|
326 apply (intro exI bexI) |
|
327 apply (rule_tac [2] |
|
328 set_pur.Nil |
|
329 [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], |
|
330 THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], |
|
331 THEN Says_to_Gets, |
|
332 THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], |
|
333 THEN Says_to_Gets, |
|
334 THEN set_pur.PReqUns [of concl: C M KC], |
|
335 THEN Says_to_Gets, |
|
336 THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], |
|
337 THEN Says_to_Gets, |
|
338 THEN set_pur.AuthResUns [of concl: "PG j" M KP LID_M XID], |
|
339 THEN Says_to_Gets, |
|
340 THEN set_pur.PRes]) |
|
341 apply basic_possibility |
|
342 apply (simp_all add: used_Cons symKeys_neq_imp_neq) |
|
343 done |
|
344 |
|
345 lemma possibility_S: |
|
346 "[| CardSecret k \<noteq> 0; |
|
347 C = Cardholder k; M = Merchant i; |
|
348 Key KC \<notin> used []; Key KM \<notin> used []; Key KP \<notin> used []; |
|
349 KC \<in> symKeys; KM \<in> symKeys; KP \<in> symKeys; |
|
350 KC < KM; KM < KP; |
|
351 Nonce Chall_C \<notin> used []; Chall_C \<notin> range CardSecret \<union> range PANSecret; |
|
352 Nonce Chall_M \<notin> used []; Chall_M \<notin> range CardSecret \<union> range PANSecret; |
|
353 Chall_C < Chall_M; |
|
354 Number LID_M \<notin> used []; LID_M \<notin> range CardSecret \<union> range PANSecret; |
|
355 Number XID \<notin> used []; XID \<notin> range CardSecret \<union> range PANSecret; |
|
356 LID_M < XID; XID < OrderDesc; OrderDesc < PurchAmt |] |
|
357 ==> \<exists>evs \<in> set_pur. |
|
358 Says M C |
|
359 (sign (priSK M) {|Number LID_M, Number XID, Nonce Chall_C, |
|
360 Hash (Number PurchAmt)|}) |
|
361 \<in> set evs" |
|
362 apply (intro exI bexI) |
|
363 apply (rule_tac [2] |
|
364 set_pur.Nil |
|
365 [THEN set_pur.Start [of _ LID_M C k M i _ _ _ OrderDesc PurchAmt], |
|
366 THEN set_pur.PInitReq [of concl: C M LID_M Chall_C], |
|
367 THEN Says_to_Gets, |
|
368 THEN set_pur.PInitRes [of concl: M C LID_M XID Chall_C Chall_M], |
|
369 THEN Says_to_Gets, |
|
370 THEN set_pur.PReqS [of concl: C M _ _ KC], |
|
371 THEN Says_to_Gets, |
|
372 THEN set_pur.AuthReq [of concl: M "PG j" KM LID_M XID], |
|
373 THEN Says_to_Gets, |
|
374 THEN set_pur.AuthResS [of concl: "PG j" M KP LID_M XID], |
|
375 THEN Says_to_Gets, |
|
376 THEN set_pur.PRes]) |
|
377 apply basic_possibility |
|
378 apply (auto simp add: used_Cons symKeys_neq_imp_neq) |
|
379 done |
|
380 |
|
381 text{*General facts about message reception*} |
|
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 |
|
434 text{*trivial proof because @{term"priEK C"} never appears even in |
|
435 @{term "parts evs"}. *} |
|
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 |
|
442 |
|
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" |
|
449 by (erule rev_mp, erule set_pur.induct, auto) |
|
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" |
|
455 by (erule rev_mp, erule set_pur.induct, auto) |
|
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 |
|
482 method_setup valid_certificate_tac = {* |
|
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)]))) |
|
487 *} "" |
|
488 |
|
489 |
|
490 subsection{*Proofs on Symmetric Keys*} |
|
491 |
|
492 text{*Nobody can have used non-existent 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) |
|
498 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
499 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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: |
|
551 "evs \<in> set_pur \<Longrightarrow> |
|
552 (\<forall>SK KK. SK \<in> symKeys \<longrightarrow> |
|
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)))" |
|
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*} |
|
560 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
561 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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) |
|
567 --{*8 seconds on a 1.6GHz machine*} |
|
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)) --> |
|
587 (Nonce N \<in> analz (Key`KK \<union> (knows Spy evs))) = |
|
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*} |
|
593 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
594 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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) |
|
600 --{*8 seconds on a 1.6GHz machine*} |
|
601 apply spy_analz --{*Fake*} |
|
602 apply (blast elim!: ballE) --{*PReqS*} |
|
603 done |
|
604 |
|
605 lemma PANSecret_notin_spies: |
|
606 "[|Nonce (PANSecret k) \<in> analz (knows Spy evs); evs \<in> set_pur|] |
|
607 ==> |
|
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)" |
|
612 apply (erule rev_mp) |
|
613 apply (erule set_pur.induct) |
|
614 apply (frule_tac [9] AuthReq_msg_in_analz_spies) |
|
615 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
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) |
|
622 --{*2.5 seconds on a 1.6GHz machine*} |
|
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 |
|
638 |
|
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*} |
|
657 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
658 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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) |
|
665 --{*7 seconds on a 1.6GHz machine*} |
|
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.*} |
|
678 theorem pan_confidentiality_unsigned: |
|
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*} |
|
688 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
689 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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) |
|
695 --{*3 seconds on a 1.6GHz machine*} |
|
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.*} |
|
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" |
|
709 apply (erule rev_mp) |
|
710 apply (erule set_pur.induct) |
|
711 apply (frule_tac [9] AuthReq_msg_in_analz_spies) --{*AReq*} |
|
712 apply (valid_certificate_tac [8]) --{*PReqS*} |
|
713 apply (valid_certificate_tac [7]) --{*PReqUns*} |
|
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) |
|
719 --{*3 seconds on a 1.6GHz machine*} |
|
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" |
|
735 by (erule rev_mp, erule set_pur.induct, simp_all) |
|
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, |
|
768 cert P EKj onlyEnc (priSK RCA)|}; |
|
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 |
|
819 the identifying tags and the purchase amount, which he can verify. |
|
820 (Although the spec has SIGNED and UNSIGNED forms of AuthRes, they |
|
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.*} |
|
827 theorem M_verifies_AuthRes: |
|
828 "[| MsgAuthRes = {|{|Number LID_M, Number XID, Number PurchAmt|}, |
|
829 Hash authCode|}; |
|
830 Crypt (priSK (PG j)) (Hash MsgAuthRes) \<in> parts (knows Spy evs); |
|
831 PG j \<notin> bad; evs \<in> set_pur|] |
|
832 ==> \<exists>M KM KP HOIData HOD P_I. |
|
833 Gets (PG j) |
|
834 (EncB (priSK M) KM (pubEK (PG j)) |
|
835 {|Number LID_M, Number XID, HOIData, HOD|} |
|
836 P_I) \<in> set evs & |
|
837 Says (PG j) M |
|
838 (EncB (priSK (PG j)) KP (pubEK M) |
|
839 {|Number LID_M, Number XID, Number PurchAmt|} |
|
840 authCode) \<in> set evs" |
|
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) |
|
865 apply (valid_certificate_tac [2]) --{*PReqUns*} |
|
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 |
|
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: |
|
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|} |
|
971 authCode) \<in> set evs & |
|
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" |
|
1025 by (erule rev_mp, erule set_pur.induct, auto) |
|
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.*} |
|
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. |
|
1037 HPIData = Hash PIData & |
|
1038 Says C M {|{|sign (priSK C) MsgDualSign, PICrypt|}, OIData, Hash PIData|} |
|
1039 \<in> set evs" |
|
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 |
|
1047 apply (metis subsetD insert_subset parts.Fst parts_increasing signed_Hash_imp_used) |
|
1048 apply (metis unique_LID_M) |
|
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"}.*} |
|
1056 theorem P_verifies_Signed_PReq: |
|
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 *} |
|
1138 theorem P_sees_CM_agreement: |
|
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 |