11 needed: no session key encrypts another. Instead we |
11 needed: no session key encrypts another. Instead we |
12 prove the "key compromise" theorems for sets KK that contain no private |
12 prove the "key compromise" theorems for sets KK that contain no private |
13 encryption keys (@{term "priEK C"}). *} |
13 encryption keys (@{term "priEK C"}). *} |
14 |
14 |
15 |
15 |
16 consts set_mr :: "event list set" |
16 inductive_set |
17 inductive set_mr |
17 set_mr :: "event list set" |
18 intros |
18 where |
19 |
19 |
20 Nil: --{*Initial trace is empty*} |
20 Nil: --{*Initial trace is empty*} |
21 "[] \<in> set_mr" |
21 "[] \<in> set_mr" |
22 |
22 |
23 |
23 |
24 Fake: --{*The spy MAY say anything he CAN say.*} |
24 | Fake: --{*The spy MAY say anything he CAN say.*} |
25 "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |] |
25 "[| evsf \<in> set_mr; X \<in> synth (analz (knows Spy evsf)) |] |
26 ==> Says Spy B X # evsf \<in> set_mr" |
26 ==> Says Spy B X # evsf \<in> set_mr" |
27 |
27 |
28 |
28 |
29 Reception: --{*If A sends a message X to B, then B might receive it*} |
29 | Reception: --{*If A sends a message X to B, then B might receive it*} |
30 "[| evsr \<in> set_mr; Says A B X \<in> set evsr |] |
30 "[| evsr \<in> set_mr; Says A B X \<in> set evsr |] |
31 ==> Gets B X # evsr \<in> set_mr" |
31 ==> Gets B X # evsr \<in> set_mr" |
32 |
32 |
33 |
33 |
34 SET_MR1: --{*RegFormReq: M requires a registration form to a CA*} |
34 | SET_MR1: --{*RegFormReq: M requires a registration form to a CA*} |
35 "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |] |
35 "[| evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 |] |
36 ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr" |
36 ==> Says M (CA i) {|Agent M, Nonce NM1|} # evs1 \<in> set_mr" |
37 |
37 |
38 |
38 |
39 SET_MR2: --{*RegFormRes: CA replies with the registration form and the |
39 | SET_MR2: --{*RegFormRes: CA replies with the registration form and the |
40 certificates for her keys*} |
40 certificates for her keys*} |
41 "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2; |
41 "[| evs2 \<in> set_mr; Nonce NCA \<notin> used evs2; |
42 Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |] |
42 Gets (CA i) {|Agent M, Nonce NM1|} \<in> set evs2 |] |
43 ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|}, |
43 ==> Says (CA i) M {|sign (priSK (CA i)) {|Agent M, Nonce NM1, Nonce NCA|}, |
44 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA), |
44 cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA), |
45 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |} |
45 cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) |} |
46 # evs2 \<in> set_mr" |
46 # evs2 \<in> set_mr" |
47 |
47 |
48 SET_MR3: |
48 | SET_MR3: |
49 --{*CertReq: M submits the key pair to be certified. The Notes |
49 --{*CertReq: M submits the key pair to be certified. The Notes |
50 event allows KM1 to be lost if M is compromised. Piero remarks |
50 event allows KM1 to be lost if M is compromised. Piero remarks |
51 that the agent mentioned inside the signature is not verified to |
51 that the agent mentioned inside the signature is not verified to |
52 correspond to M. As in CR, each Merchant has fixed key pairs. M |
52 correspond to M. As in CR, each Merchant has fixed key pairs. M |
53 is only optionally required to send NCA back, so M doesn't do so |
53 is only optionally required to send NCA back, so M doesn't do so |
64 Key (pubSK M), Key (pubEK M)|}), |
64 Key (pubSK M), Key (pubEK M)|}), |
65 Crypt EKi (Key KM1)|} |
65 Crypt EKi (Key KM1)|} |
66 # Notes M {|Key KM1, Agent (CA i)|} |
66 # Notes M {|Key KM1, Agent (CA i)|} |
67 # evs3 \<in> set_mr" |
67 # evs3 \<in> set_mr" |
68 |
68 |
69 SET_MR4: |
69 | SET_MR4: |
70 --{*CertRes: CA issues the certificates for merSK and merEK, |
70 --{*CertRes: CA issues the certificates for merSK and merEK, |
71 while checking never to have certified the m even |
71 while checking never to have certified the m even |
72 separately. NOTE: In Cardholder Registration the |
72 separately. NOTE: In Cardholder Registration the |
73 corresponding rule (6) doesn't use the "sign" primitive. "The |
73 corresponding rule (6) doesn't use the "sign" primitive. "The |
74 CertRes shall be signed but not encrypted if the EE is a Merchant |
74 CertRes shall be signed but not encrypted if the EE is a Merchant |