author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 33028  9aa8bfb1649d 
child 58889  5b7a9633cfa8 
permissions  rwrr 
33028  1 
(* Title: HOL/SET_Protocol/Merchant_Registration.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

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

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

4 
Author: Lawrence C Paulson 
14199  5 
*) 
6 

7 
header{*The SET Merchant Registration Protocol*} 

8 

33028  9 
theory Merchant_Registration 
10 
imports Public_SET 

11 
begin 

14199  12 

13 
text{*Copmpared with Cardholder Reigstration, @{text KeyCryptKey} is not 

14 
needed: no session key encrypts another. Instead we 

15 
prove the "key compromise" theorems for sets KK that contain no private 

16 
encryption keys (@{term "priEK C"}). *} 

17 

18 

23755  19 
inductive_set 
20 
set_mr :: "event list set" 

21 
where 

14199  22 

23 
Nil: {*Initial trace is empty*} 

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

24 
"[] \<in> set_mr" 
14199  25 

26 

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

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

29 
==> Says Spy B X # evsf \<in> set_mr" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

30 

14199  31 

23755  32 
 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:
24123
diff
changeset

33 
"[ evsr \<in> set_mr; Says A B X \<in> set evsr ] 
14199  34 
==> Gets B X # evsr \<in> set_mr" 
35 

36 

23755  37 
 SET_MR1: {*RegFormReq: M requires a registration form to a CA*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

38 
"[ evs1 \<in> set_mr; M = Merchant k; Nonce NM1 \<notin> used evs1 ] 
14199  39 
==> Says M (CA i) {Agent M, Nonce NM1} # evs1 \<in> set_mr" 
40 

41 

23755  42 
 SET_MR2: {*RegFormRes: CA replies with the registration form and the 
14199  43 
certificates for her keys*} 
44 
"[ evs2 \<in> set_mr; Nonce NCA \<notin> used evs2; 

45 
Gets (CA i) {Agent M, Nonce NM1} \<in> set evs2 ] 

46 
==> Says (CA i) M {sign (priSK (CA i)) {Agent M, Nonce NM1, Nonce NCA}, 

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

47 
cert (CA i) (pubEK (CA i)) onlyEnc (priSK RCA), 
14199  48 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA) } 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

49 
# evs2 \<in> set_mr" 
14199  50 

23755  51 
 SET_MR3: 
14199  52 
{*CertReq: M submits the key pair to be certified. The Notes 
53 
event allows KM1 to be lost if M is compromised. Piero remarks 

54 
that the agent mentioned inside the signature is not verified to 

55 
correspond to M. As in CR, each Merchant has fixed key pairs. M 

56 
is only optionally required to send NCA back, so M doesn't do so 

57 
in the model*} 

58 
"[ evs3 \<in> set_mr; M = Merchant k; Nonce NM2 \<notin> used evs3; 

59 
Key KM1 \<notin> used evs3; KM1 \<in> symKeys; 

60 
Gets M {sign (invKey SKi) {Agent X, Nonce NM1, Nonce NCA}, 

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

61 
cert (CA i) EKi onlyEnc (priSK RCA), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

62 
cert (CA i) SKi onlySig (priSK RCA) } 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

63 
\<in> set evs3; 
14199  64 
Says M (CA i) {Agent M, Nonce NM1} \<in> set evs3 ] 
65 
==> Says M (CA i) 

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

66 
{Crypt KM1 (sign (priSK M) {Agent M, Nonce NM2, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

67 
Key (pubSK M), Key (pubEK M)}), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

68 
Crypt EKi (Key KM1)} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

69 
# Notes M {Key KM1, Agent (CA i)} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

70 
# evs3 \<in> set_mr" 
14199  71 

23755  72 
 SET_MR4: 
14199  73 
{*CertRes: CA issues the certificates for merSK and merEK, 
74 
while checking never to have certified the m even 

75 
separately. NOTE: In Cardholder Registration the 

76 
corresponding rule (6) doesn't use the "sign" primitive. "The 

77 
CertRes shall be signed but not encrypted if the EE is a Merchant 

78 
or Payment Gateway." Programmer's Guide, page 191.*} 

79 
"[ evs4 \<in> set_mr; M = Merchant k; 

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

80 
merSK \<notin> symKeys; merEK \<notin> symKeys; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

81 
Notes (CA i) (Key merSK) \<notin> set evs4; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

82 
Notes (CA i) (Key merEK) \<notin> set evs4; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

83 
Gets (CA i) {Crypt KM1 (sign (invKey merSK) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

84 
{Agent M, Nonce NM2, Key merSK, Key merEK}), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

85 
Crypt (pubEK (CA i)) (Key KM1) } 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

86 
\<in> set evs4 ] 
14199  87 
==> Says (CA i) M {sign (priSK(CA i)) {Agent M, Nonce NM2, Agent(CA i)}, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

88 
cert M merSK onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

89 
cert M merEK onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

90 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

91 
# Notes (CA i) (Key merSK) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

92 
# Notes (CA i) (Key merEK) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

93 
# evs4 \<in> set_mr" 
14199  94 

95 

96 
text{*Note possibility proofs are missing.*} 

97 

98 
declare Says_imp_knows_Spy [THEN parts.Inj, dest] 

99 
declare parts.Body [dest] 

100 
declare analz_into_parts [dest] 

101 
declare Fake_parts_insert_in_Un [dest] 

102 

103 
text{*General facts about message reception*} 

104 
lemma Gets_imp_Says: 

105 
"[ Gets B X \<in> set evs; evs \<in> set_mr ] ==> \<exists>A. Says A B X \<in> set evs" 

106 
apply (erule rev_mp) 

107 
apply (erule set_mr.induct, auto) 

108 
done 

109 

110 
lemma Gets_imp_knows_Spy: 

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

112 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

113 

114 

115 
declare Gets_imp_knows_Spy [THEN parts.Inj, dest] 

116 

117 
subsubsection{*Proofs on keys *} 

118 

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

120 
lemma Spy_see_private_Key [simp]: 

121 
"evs \<in> set_mr 

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

123 
apply (erule set_mr.induct) 

124 
apply (auto dest!: Gets_imp_knows_Spy [THEN parts.Inj]) 

125 
done 

126 

127 
lemma Spy_analz_private_Key [simp]: 

128 
"evs \<in> set_mr ==> 

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

130 
by auto 

131 

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

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

134 

135 
(*This is to state that the signed keys received in step 4 

136 
are into parts  rather than installing sign_def each time. 

137 
Needed in Spy_see_priSK_RCA, Spy_see_priEK and in Spy_see_priSK 

138 
Goal "[Gets C \<lbrace>Crypt KM1 

139 
(sign K \<lbrace>Agent M, Nonce NM2, Key merSK, Key merEK\<rbrace>), X\<rbrace> 

140 
\<in> set evs; evs \<in> set_mr ] 

141 
==> Key merSK \<in> parts (knows Spy evs) \<and> 

142 
Key merEK \<in> parts (knows Spy evs)" 

143 
by (fast_tac (claset() addss (simpset())) 1); 

144 
qed "signed_keys_in_parts"; 

145 
???*) 

146 

147 
text{*Proofs on certificates  

148 
they hold, as in CR, because RCA's keys are secure*} 

149 

150 
lemma Crypt_valid_pubEK: 

151 
"[ Crypt (priSK RCA) {Agent (CA i), Key EKi, onlyEnc} 

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

153 
evs \<in> set_mr ] ==> EKi = pubEK (CA i)" 

154 
apply (erule rev_mp) 

155 
apply (erule set_mr.induct, auto) 

156 
done 

157 

158 
lemma certificate_valid_pubEK: 

159 
"[ cert (CA i) EKi onlyEnc (priSK RCA) \<in> parts (knows Spy evs); 

160 
evs \<in> set_mr ] 

161 
==> EKi = pubEK (CA i)" 

162 
apply (unfold cert_def signCert_def) 

163 
apply (blast dest!: Crypt_valid_pubEK) 

164 
done 

165 

166 
lemma Crypt_valid_pubSK: 

167 
"[ Crypt (priSK RCA) {Agent (CA i), Key SKi, onlySig} 

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

169 
evs \<in> set_mr ] ==> SKi = pubSK (CA i)" 

170 
apply (erule rev_mp) 

171 
apply (erule set_mr.induct, auto) 

172 
done 

173 

174 
lemma certificate_valid_pubSK: 

175 
"[ cert (CA i) SKi onlySig (priSK RCA) \<in> parts (knows Spy evs); 

176 
evs \<in> set_mr ] ==> SKi = pubSK (CA i)" 

177 
apply (unfold cert_def signCert_def) 

178 
apply (blast dest!: Crypt_valid_pubSK) 

179 
done 

180 

181 
lemma Gets_certificate_valid: 

182 
"[ Gets A { X, cert (CA i) EKi onlyEnc (priSK RCA), 

183 
cert (CA i) SKi onlySig (priSK RCA)} \<in> set evs; 

184 
evs \<in> set_mr ] 

185 
==> EKi = pubEK (CA i) & SKi = pubSK (CA i)" 

186 
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK) 

187 

188 

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

190 
lemma new_keys_not_used [rule_format,simp]: 

191 
"evs \<in> set_mr 

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

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

194 
apply (erule set_mr.induct, simp_all) 

14218  195 
apply (force dest!: usedI keysFor_parts_insert) {*Fake*} 
196 
apply force {*Message 2*} 

197 
apply (blast dest: Gets_certificate_valid) {*Message 3*} 

198 
apply force {*Message 4*} 

14199  199 
done 
200 

201 

202 
subsubsection{*New Versions: As Above, but Generalized with the Kk Argument*} 

203 

204 
lemma gen_new_keys_not_used [rule_format]: 

205 
"evs \<in> set_mr 

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

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

208 
by auto 

209 

210 
lemma gen_new_keys_not_analzd: 

211 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr ] 

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

213 
by (blast intro: keysFor_mono [THEN [2] rev_subsetD] 

214 
dest: gen_new_keys_not_used) 

215 

216 
lemma analz_Key_image_insert_eq: 

217 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_mr ] 

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

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

220 
by (simp add: gen_new_keys_not_analzd) 

221 

222 

223 
lemma Crypt_parts_imp_used: 

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

225 
K \<in> symKeys; evs \<in> set_mr ] ==> Key K \<in> used evs" 

226 
apply (rule ccontr) 

227 
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor) 

228 
done 

229 

230 
lemma Crypt_analz_imp_used: 

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

232 
K \<in> symKeys; evs \<in> set_mr ] ==> Key K \<in> used evs" 

233 
by (blast intro: Crypt_parts_imp_used) 

234 

235 
text{*Rewriting rule for private encryption keys. Analogous rewriting rules 

236 
for other keys aren't needed.*} 

237 

238 
lemma parts_image_priEK: 

239 
"[Key (priEK (CA i)) \<in> parts (Key`KK Un (knows Spy evs)); 

240 
evs \<in> set_mr] ==> priEK (CA i) \<in> KK  CA i \<in> bad" 

241 
by auto 

242 

243 
text{*trivial proof because (priEK (CA i)) never appears even in (parts evs)*} 

244 
lemma analz_image_priEK: 

245 
"evs \<in> set_mr ==> 

246 
(Key (priEK (CA i)) \<in> analz (Key`KK Un (knows Spy evs))) = 

247 
(priEK (CA i) \<in> KK  CA i \<in> bad)" 

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

249 

250 

251 
subsection{*Secrecy of Session Keys*} 

252 

253 
text{*This holds because if (priEK (CA i)) appears in any traffic then it must 

254 
be known to the Spy, by @{text Spy_see_private_Key}*} 

255 
lemma merK_neq_priEK: 

256 
"[Key merK \<notin> analz (knows Spy evs); 

257 
Key merK \<in> parts (knows Spy evs); 

258 
evs \<in> set_mr] ==> merK \<noteq> priEK C" 

259 
by blast 

260 

261 
text{*Lemma for message 4: either merK is compromised (when we don't care) 

262 
or else merK hasn't been used to encrypt K.*} 

263 
lemma msg4_priEK_disj: 

264 
"[Gets B {Crypt KM1 

265 
(sign K {Agent M, Nonce NM2, Key merSK, Key merEK}), 

266 
Y} \<in> set evs; 

267 
evs \<in> set_mr] 

268 
==> (Key merSK \<in> analz (knows Spy evs)  merSK \<notin> range(\<lambda>C. priEK C)) 

269 
& (Key merEK \<in> analz (knows Spy evs)  merEK \<notin> range(\<lambda>C. priEK C))" 

270 
apply (unfold sign_def) 

271 
apply (blast dest: merK_neq_priEK) 

272 
done 

273 

274 

275 
lemma Key_analz_image_Key_lemma: 

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

277 
==> 

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

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

280 

281 
lemma symKey_compromise: 

282 
"evs \<in> set_mr ==> 

283 
(\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. K \<notin> range(\<lambda>C. priEK C)) > 

284 
(Key SK \<in> analz (Key`KK Un (knows Spy evs))) = 

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

286 
apply (erule set_mr.induct) 

287 
apply (safe del: impI intro!: Key_analz_image_Key_lemma [THEN impI]) 

288 
apply (drule_tac [7] msg4_priEK_disj) 

289 
apply (frule_tac [6] Gets_certificate_valid) 

290 
apply (safe del: impI) 

291 
apply (simp_all del: image_insert image_Un imp_disjL 

292 
add: analz_image_keys_simps abbrev_simps analz_knows_absorb 

293 
analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff 

294 
Spy_analz_private_Key analz_image_priEK) 

24123  295 
{*5 seconds on a 1.6GHz machine*} 
14218  296 
apply spy_analz {*Fake*} 
297 
apply auto {*Message 3*} 

14199  298 
done 
299 

300 
lemma symKey_secrecy [rule_format]: 

301 
"[CA i \<notin> bad; K \<in> symKeys; evs \<in> set_mr] 

302 
==> \<forall>X m. Says (Merchant m) (CA i) X \<in> set evs > 

303 
Key K \<in> parts{X} > 

304 
Merchant m \<notin> bad > 

305 
Key K \<notin> analz (knows Spy evs)" 

306 
apply (erule set_mr.induct) 

307 
apply (drule_tac [7] msg4_priEK_disj) 

308 
apply (frule_tac [6] Gets_certificate_valid) 

309 
apply (safe del: impI) 

310 
apply (simp_all del: image_insert image_Un imp_disjL 

311 
add: analz_image_keys_simps abbrev_simps analz_knows_absorb 

312 
analz_knows_absorb2 analz_Key_image_insert_eq 

313 
symKey_compromise notin_image_iff Spy_analz_private_Key 

314 
analz_image_priEK) 

14218  315 
apply spy_analz {*Fake*} 
316 
apply force {*Message 1*} 

317 
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) {*Message 3*} 

14199  318 
done 
319 

320 
subsection{*Unicity *} 

321 

322 
lemma msg4_Says_imp_Notes: 

323 
"[Says (CA i) M {sign (priSK (CA i)) {Agent M, Nonce NM2, Agent (CA i)}, 

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

324 
cert M merSK onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

325 
cert M merEK onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

326 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)} \<in> set evs; 
14199  327 
evs \<in> set_mr ] 
328 
==> Notes (CA i) (Key merSK) \<in> set evs 

329 
& Notes (CA i) (Key merEK) \<in> set evs" 

330 
apply (erule rev_mp) 

331 
apply (erule set_mr.induct) 

332 
apply (simp_all (no_asm_simp)) 

333 
done 

334 

335 
text{*Unicity of merSK wrt a given CA: 

336 
merSK uniquely identifies the other components, including merEK*} 

337 
lemma merSK_unicity: 

338 
"[Says (CA i) M {sign (priSK(CA i)) {Agent M, Nonce NM2, Agent (CA i)}, 

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

339 
cert M merSK onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

340 
cert M merEK onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

341 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)} \<in> set evs; 
14199  342 
Says (CA i) M' {sign (priSK(CA i)) {Agent M', Nonce NM2', Agent (CA i)}, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

343 
cert M' merSK onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

344 
cert M' merEK' onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

345 
cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)} \<in> set evs; 
14199  346 
evs \<in> set_mr ] ==> M=M' & NM2=NM2' & merEK=merEK'" 
347 
apply (erule rev_mp) 

348 
apply (erule rev_mp) 

349 
apply (erule set_mr.induct) 

350 
apply (simp_all (no_asm_simp)) 

351 
apply (blast dest!: msg4_Says_imp_Notes) 

352 
done 

353 

354 
text{*Unicity of merEK wrt a given CA: 

355 
merEK uniquely identifies the other components, including merSK*} 

356 
lemma merEK_unicity: 

357 
"[Says (CA i) M {sign (priSK(CA i)) {Agent M, Nonce NM2, Agent (CA i)}, 

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

358 
cert M merSK onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

359 
cert M merEK onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

360 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)} \<in> set evs; 
14199  361 
Says (CA i) M' {sign (priSK(CA i)) {Agent M', Nonce NM2', Agent (CA i)}, 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

362 
cert M' merSK' onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

363 
cert M' merEK onlyEnc (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
24123
diff
changeset

364 
cert (CA i) (pubSK(CA i)) onlySig (priSK RCA)} \<in> set evs; 
14199  365 
evs \<in> set_mr ] 
366 
==> M=M' & NM2=NM2' & merSK=merSK'" 

367 
apply (erule rev_mp) 

368 
apply (erule rev_mp) 

369 
apply (erule set_mr.induct) 

370 
apply (simp_all (no_asm_simp)) 

371 
apply (blast dest!: msg4_Says_imp_Notes) 

372 
done 

373 

374 

375 
text{* No interest on secrecy of nonces: they appear to be used 

376 
only for freshness. 

377 
No interest on secrecy of merSK or merEK, as in CR. 

378 
There's no equivalent of the PAN*} 

379 

380 

381 
subsection{*Primary Goals of Merchant Registration *} 

382 

383 
subsubsection{*The merchant's certificates really were created by the CA, 

384 
provided the CA is uncompromised *} 

385 

386 
text{*The assumption @{term "CA i \<noteq> RCA"} is required: step 2 uses 

387 
certificates of the same form.*} 

388 
lemma certificate_merSK_valid_lemma [intro]: 

389 
"[Crypt (priSK (CA i)) {Agent M, Key merSK, onlySig} 

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

391 
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr] 

392 
==> \<exists>X Y Z. Says (CA i) M 

393 
{X, cert M merSK onlySig (priSK (CA i)), Y, Z} \<in> set evs" 

394 
apply (erule rev_mp) 

395 
apply (erule set_mr.induct) 

396 
apply (simp_all (no_asm_simp)) 

397 
apply auto 

398 
done 

399 

400 
lemma certificate_merSK_valid: 

401 
"[ cert M merSK onlySig (priSK (CA i)) \<in> parts (knows Spy evs); 

402 
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr] 

403 
==> \<exists>X Y Z. Says (CA i) M 

404 
{X, cert M merSK onlySig (priSK (CA i)), Y, Z} \<in> set evs" 

405 
by auto 

406 

407 
lemma certificate_merEK_valid_lemma [intro]: 

408 
"[Crypt (priSK (CA i)) {Agent M, Key merEK, onlyEnc} 

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

410 
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr] 

411 
==> \<exists>X Y Z. Says (CA i) M 

412 
{X, Y, cert M merEK onlyEnc (priSK (CA i)), Z} \<in> set evs" 

413 
apply (erule rev_mp) 

414 
apply (erule set_mr.induct) 

415 
apply (simp_all (no_asm_simp)) 

416 
apply auto 

417 
done 

418 

419 
lemma certificate_merEK_valid: 

420 
"[ cert M merEK onlyEnc (priSK (CA i)) \<in> parts (knows Spy evs); 

421 
CA i \<notin> bad; CA i \<noteq> RCA; evs \<in> set_mr] 

422 
==> \<exists>X Y Z. Says (CA i) M 

423 
{X, Y, cert M merEK onlyEnc (priSK (CA i)), Z} \<in> set evs" 

424 
by auto 

425 

426 
text{*The two certificates  for merSK and for merEK  cannot be proved to 

427 
have originated together*} 

428 

429 
end 