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/Cardholder_Registration.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 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

5 
Author: Piero Tramontano 
14199  6 
*) 
7 

8 
header{*The SET Cardholder Registration Protocol*} 

9 

33028  10 
theory Cardholder_Registration 
11 
imports Public_SET 

12 
begin 

14199  13 

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

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

16 
*} 

17 

18 
text{*Simplifications involving @{text analz_image_keys_simps} appear to 

19 
have become much slower. The cause is unclear. However, there is a big blowup 

20 
and the rewriting is very sensitive to the set of rewrite rules given.*} 

21 

22 
subsection{*Predicate Formalizing the Encryption Association between Keys *} 

23 

39758  24 
primrec KeyCryptKey :: "[key, key, event list] => bool" 
25 
where 

26 
KeyCryptKey_Nil: 

27 
"KeyCryptKey DK K [] = False" 

28 
 KeyCryptKey_Cons: 

14199  29 
{*Says is the only important case. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

30 
1st case: CR5, where KC3 encrypts KC2. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

31 
2nd case: any use of priEK C. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

32 
Revision 1.12 has a more complicated version with separate treatment of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

33 
the dependency of KC1, KC2 and KC3 on priEK (CA i.) Not needed since 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

34 
priEK C is never sent (and so can't be lost except at the start). *} 
39758  35 
"KeyCryptKey DK K (ev # evs) = 
36 
(KeyCryptKey DK K evs  

37 
(case ev of 

38 
Says A B Z => 

39 
((\<exists>N X Y. A \<noteq> Spy & 

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

40 
DK \<in> symKeys & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

41 
Z = {Crypt DK {Agent A, Nonce N, Key K, X}, Y})  
39758  42 
(\<exists>C. DK = priEK C)) 
43 
 Gets A' X => False 

44 
 Notes A' X => False))" 

14199  45 

46 

47 
subsection{*Predicate formalizing the association between keys and nonces *} 

48 

39758  49 
primrec KeyCryptNonce :: "[key, key, event list] => bool" 
50 
where 

51 
KeyCryptNonce_Nil: 

52 
"KeyCryptNonce EK K [] = False" 

53 
 KeyCryptNonce_Cons: 

14199  54 
{*Says is the only important case. 
55 
1st case: CR3, where KC1 encrypts NC2 (distinct from CR5 due to EXH); 

56 
2nd case: CR5, where KC3 encrypts NC3; 

57 
3rd case: CR6, where KC2 encrypts NC3; 

58 
4th case: CR6, where KC2 encrypts NonceCCA; 

59 
5th case: any use of @{term "priEK C"} (including CardSecret). 

60 
NB the only Nonces we need to keep secret are CardSecret and NonceCCA. 

61 
But we can't prove @{text Nonce_compromise} unless the relation covers ALL 

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

62 
nonces that the protocol keeps secret. 
14199  63 
*} 
64 
"KeyCryptNonce DK N (ev # evs) = 

65 
(KeyCryptNonce DK N evs  

66 
(case ev of 

67 
Says A B Z => 

68 
A \<noteq> Spy & 

69 
((\<exists>X Y. DK \<in> symKeys & 

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

70 
Z = (EXHcrypt DK X {Agent A, Nonce N} Y))  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

71 
(\<exists>X Y. DK \<in> symKeys & 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

72 
Z = {Crypt DK {Agent A, Nonce N, X}, Y})  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

73 
(\<exists>K i X Y. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

74 
K \<in> symKeys & 
14199  75 
Z = Crypt K {sign (priSK (CA i)) {Agent B, Nonce N, X}, Y} & 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

76 
(DK=K  KeyCryptKey DK K evs))  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

77 
(\<exists>K C NC3 Y. 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

78 
K \<in> symKeys & 
14199  79 
Z = Crypt K 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

80 
{sign (priSK C) {Agent B, Nonce NC3, Agent C, Nonce N}, 
14199  81 
Y} & 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

82 
(DK=K  KeyCryptKey DK K evs))  
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

83 
(\<exists>C. DK = priEK C)) 
14199  84 
 Gets A' X => False 
85 
 Notes A' X => False))" 

86 

87 

88 
subsection{*Formal protocol definition *} 

89 

23755  90 
inductive_set 
91 
set_cr :: "event list set" 

92 
where 

14199  93 

94 
Nil: {*Initial trace is empty*} 

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

95 
"[] \<in> set_cr" 
14199  96 

23755  97 
 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

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

99 
==> Says Spy B X # evsf \<in> set_cr" 
14199  100 

23755  101 
 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

102 
"[ evsr \<in> set_cr; Says A B X \<in> set evsr ] 
14199  103 
==> Gets B X # evsr \<in> set_cr" 
104 

23755  105 
 SET_CR1: {*CardCInitReq: C initiates a run, sending a nonce to CCA*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

106 
"[ evs1 \<in> set_cr; C = Cardholder k; Nonce NC1 \<notin> used evs1 ] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

107 
==> Says C (CA i) {Agent C, Nonce NC1} # evs1 \<in> set_cr" 
14199  108 

23755  109 
 SET_CR2: {*CardCInitRes: CA responds sending NC1 and its certificates*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

110 
"[ evs2 \<in> set_cr; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

111 
Gets (CA i) {Agent C, Nonce NC1} \<in> set evs2 ] 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

112 
==> Says (CA i) C 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

113 
{sign (priSK (CA i)) {Agent C, Nonce NC1}, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

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

116 
# evs2 \<in> set_cr" 
14199  117 

23755  118 
 SET_CR3: 
14199  119 
{*RegFormReq: C sends his PAN and a new nonce to CA. 
120 
C verifies that 

121 
 nonce received is the same as that sent; 

122 
 certificates are signed by RCA; 

123 
 certificates are an encryption certificate (flag is onlyEnc) and a 

124 
signature certificate (flag is onlySig); 

125 
 certificates pertain to the CA that C contacted (this is done by 

126 
checking the signature). 

127 
C generates a fresh symmetric key KC1. 

128 
The point of encrypting @{term "{Agent C, Nonce NC2, Hash (Pan(pan C))}"} 

129 
is not clear. *} 

130 
"[ evs3 \<in> set_cr; C = Cardholder k; 

131 
Nonce NC2 \<notin> used evs3; 

132 
Key KC1 \<notin> used evs3; KC1 \<in> symKeys; 

133 
Gets C {sign (invKey SKi) {Agent X, Nonce NC1}, 

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

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

135 
cert (CA i) SKi onlySig (priSK RCA)} 
14199  136 
\<in> set evs3; 
137 
Says C (CA i) {Agent C, Nonce NC1} \<in> set evs3] 

138 
==> Says C (CA i) (EXHcrypt KC1 EKi {Agent C, Nonce NC2} (Pan(pan C))) 

139 
# Notes C {Key KC1, Agent (CA i)} 

140 
# evs3 \<in> set_cr" 

141 

23755  142 
 SET_CR4: 
14199  143 
{*RegFormRes: 
144 
CA responds sending NC2 back with a new nonce NCA, after checking that 

145 
 the digital envelope is correctly encrypted by @{term "pubEK (CA i)"} 

146 
 the entire message is encrypted with the same key found inside the 

147 
envelope (here, KC1) *} 

148 
"[ evs4 \<in> set_cr; 

149 
Nonce NCA \<notin> used evs4; KC1 \<in> symKeys; 

150 
Gets (CA i) (EXHcrypt KC1 EKi {Agent C, Nonce NC2} (Pan(pan X))) 

151 
\<in> set evs4 ] 

152 
==> Says (CA i) C 

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

153 
{sign (priSK (CA i)) {Agent C, Nonce NC2, Nonce NCA}, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

155 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)} 
14199  156 
# evs4 \<in> set_cr" 
157 

23755  158 
 SET_CR5: 
14199  159 
{*CertReq: C sends his PAN, a new nonce, its proposed public signature key 
160 
and its half of the secret value to CA. 

161 
We now assume that C has a fixed key pair, and he submits (pubSK C). 

162 
The protocol does not require this key to be fresh. 

163 
The encryption below is actually EncX.*} 

164 
"[ evs5 \<in> set_cr; C = Cardholder k; 

165 
Nonce NC3 \<notin> used evs5; Nonce CardSecret \<notin> used evs5; NC3\<noteq>CardSecret; 

166 
Key KC2 \<notin> used evs5; KC2 \<in> symKeys; 

167 
Key KC3 \<notin> used evs5; KC3 \<in> symKeys; KC2\<noteq>KC3; 

168 
Gets C {sign (invKey SKi) {Agent C, Nonce NC2, Nonce NCA}, 

169 
cert (CA i) EKi onlyEnc (priSK RCA), 

170 
cert (CA i) SKi onlySig (priSK RCA) } 

171 
\<in> set evs5; 

172 
Says C (CA i) (EXHcrypt KC1 EKi {Agent C, Nonce NC2} (Pan(pan C))) 

173 
\<in> set evs5 ] 

174 
==> Says C (CA i) 

175 
{Crypt KC3 

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

176 
{Agent C, Nonce NC3, Key KC2, Key (pubSK C), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

177 
Crypt (priSK C) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

178 
(Hash {Agent C, Nonce NC3, Key KC2, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

179 
Key (pubSK C), Pan (pan C), Nonce CardSecret})}, 
14199  180 
Crypt EKi {Key KC3, Pan (pan C), Nonce CardSecret} } 
181 
# Notes C {Key KC2, Agent (CA i)} 

182 
# Notes C {Key KC3, Agent (CA i)} 

183 
# evs5 \<in> set_cr" 

184 

185 

186 
{* CertRes: CA responds sending NC3 back with its half of the secret value, 

187 
its signature certificate and the new cardholder signature 

188 
certificate. CA checks to have never certified the key proposed by C. 

189 
NOTE: In Merchant Registration, the corresponding rule (4) 

190 
uses the "sign" primitive. The encryption below is actually @{term EncK}, 

191 
which is just @{term "Crypt K (sign SK X)"}. 

192 
*} 

193 

23755  194 
 SET_CR6: 
14199  195 
"[ evs6 \<in> set_cr; 
196 
Nonce NonceCCA \<notin> used evs6; 

197 
KC2 \<in> symKeys; KC3 \<in> symKeys; cardSK \<notin> symKeys; 

198 
Notes (CA i) (Key cardSK) \<notin> set evs6; 

199 
Gets (CA i) 

200 
{Crypt KC3 {Agent C, Nonce NC3, Key KC2, Key cardSK, 

201 
Crypt (invKey cardSK) 

202 
(Hash {Agent C, Nonce NC3, Key KC2, 

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

203 
Key cardSK, Pan (pan C), Nonce CardSecret})}, 
14199  204 
Crypt (pubEK (CA i)) {Key KC3, Pan (pan C), Nonce CardSecret} } 
205 
\<in> set evs6 ] 

206 
==> Says (CA i) C 

207 
(Crypt KC2 

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

208 
{sign (priSK (CA i)) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

209 
{Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA}, 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

210 
certC (pan C) cardSK (XOR(CardSecret,NonceCCA)) onlySig (priSK (CA i)), 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

211 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)}) 
14199  212 
# Notes (CA i) (Key cardSK) 
213 
# evs6 \<in> set_cr" 

214 

215 

216 
declare Says_imp_knows_Spy [THEN parts.Inj, dest] 

217 
declare parts.Body [dest] 

218 
declare analz_into_parts [dest] 

219 
declare Fake_parts_insert_in_Un [dest] 

220 

221 
text{*A "possibility property": there are traces that reach the end. 

222 
An unconstrained proof with many subgoals.*} 

223 

224 
lemma Says_to_Gets: 

225 
"Says A B X # evs \<in> set_cr ==> Gets B X # Says A B X # evs \<in> set_cr" 

226 
by (rule set_cr.Reception, auto) 

227 

228 
text{*The many nonces and keys generated, some simultaneously, force us to 

229 
introduce them explicitly as shown below.*} 

230 
lemma possibility_CR6: 

231 
"[NC1 < (NC2::nat); NC2 < NC3; NC3 < NCA ; 

232 
NCA < NonceCCA; NonceCCA < CardSecret; 

233 
KC1 < (KC2::key); KC2 < KC3; 

234 
KC1 \<in> symKeys; Key KC1 \<notin> used []; 

235 
KC2 \<in> symKeys; Key KC2 \<notin> used []; 

236 
KC3 \<in> symKeys; Key KC3 \<notin> used []; 

237 
C = Cardholder k] 

238 
==> \<exists>evs \<in> set_cr. 

239 
Says (CA i) C 

240 
(Crypt KC2 

241 
{sign (priSK (CA i)) 

242 
{Agent C, Nonce NC3, Agent(CA i), Nonce NonceCCA}, 

243 
certC (pan C) (pubSK (Cardholder k)) (XOR(CardSecret,NonceCCA)) 

244 
onlySig (priSK (CA i)), 

245 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)}) 

246 
\<in> set evs" 

247 
apply (intro exI bexI) 

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

248 
apply (rule_tac [2] 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

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

250 
[THEN set_cr.SET_CR1 [of concl: C i NC1], 
77bf175f5145
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
paulson
parents:
14199
diff
changeset

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

252 
THEN set_cr.SET_CR2 [of concl: i C NC1], 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

254 
THEN set_cr.SET_CR3 [of concl: C i KC1 _ NC2], 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

256 
THEN set_cr.SET_CR4 [of concl: i C NC2 NCA], 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

258 
THEN set_cr.SET_CR5 [of concl: C i KC3 NC3 KC2 CardSecret], 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32404
diff
changeset

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

260 
THEN set_cr.SET_CR6 [of concl: i C KC2]]) 
30607
c3d1590debd8
eliminated global SIMPSET, CLASET etc.  refer to explicit context;
wenzelm
parents:
30549
diff
changeset

261 
apply basic_possibility 
14199  262 
apply (simp_all (no_asm_simp) add: symKeys_neq_imp_neq) 
263 
done 

264 

265 
text{*General facts about message reception*} 

266 
lemma Gets_imp_Says: 

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

268 
apply (erule rev_mp) 

269 
apply (erule set_cr.induct, auto) 

270 
done 

271 

272 
lemma Gets_imp_knows_Spy: 

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

274 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

275 
declare Gets_imp_knows_Spy [THEN parts.Inj, dest] 

276 

277 

278 
subsection{*Proofs on keys *} 

279 

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

281 

282 
lemma Spy_see_private_Key [simp]: 

283 
"evs \<in> set_cr 

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

285 
by (erule set_cr.induct, auto) 

286 

287 
lemma Spy_analz_private_Key [simp]: 

288 
"evs \<in> set_cr ==> 

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

290 
by auto 

291 

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

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

294 

295 

296 
subsection{*Begin Piero's Theorems on Certificates*} 

297 
text{*Trivial in the current model, where certificates by RCA are secure *} 

298 

299 
lemma Crypt_valid_pubEK: 

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

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

302 
evs \<in> set_cr ] ==> EKi = pubEK C" 

303 
apply (erule rev_mp) 

304 
apply (erule set_cr.induct, auto) 

305 
done 

306 

307 
lemma certificate_valid_pubEK: 

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

309 
evs \<in> set_cr ] 

310 
==> EKi = pubEK C" 

311 
apply (unfold cert_def signCert_def) 

312 
apply (blast dest!: Crypt_valid_pubEK) 

313 
done 

314 

315 
lemma Crypt_valid_pubSK: 

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

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

318 
evs \<in> set_cr ] ==> SKi = pubSK C" 

319 
apply (erule rev_mp) 

320 
apply (erule set_cr.induct, auto) 

321 
done 

322 

323 
lemma certificate_valid_pubSK: 

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

325 
evs \<in> set_cr ] ==> SKi = pubSK C" 

326 
apply (unfold cert_def signCert_def) 

327 
apply (blast dest!: Crypt_valid_pubSK) 

328 
done 

329 

330 
lemma Gets_certificate_valid: 

331 
"[ Gets A { X, cert C EKi onlyEnc (priSK RCA), 

332 
cert C SKi onlySig (priSK RCA)} \<in> set evs; 

333 
evs \<in> set_cr ] 

334 
==> EKi = pubEK C & SKi = pubSK C" 

335 
by (blast dest: certificate_valid_pubEK certificate_valid_pubSK) 

336 

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

338 
lemma new_keys_not_used: 

339 
"[K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr] 

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

341 
apply (erule rev_mp) 

342 
apply (erule rev_mp) 

343 
apply (erule set_cr.induct) 

344 
apply (frule_tac [8] Gets_certificate_valid) 

345 
apply (frule_tac [6] Gets_certificate_valid, simp_all) 

14218  346 
apply (force dest!: usedI keysFor_parts_insert) {*Fake*} 
347 
apply (blast,auto) {*Others*} 

14199  348 
done 
349 

350 

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

352 

353 
lemma gen_new_keys_not_used: 

354 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr ] 

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

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

357 
by (auto simp add: new_keys_not_used) 

358 

359 
lemma gen_new_keys_not_analzd: 

360 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> set_cr ] 

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

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

363 
dest: gen_new_keys_not_used) 

364 

365 
lemma analz_Key_image_insert_eq: 

366 
"[K \<in> symKeys; Key K \<notin> used evs; evs \<in> set_cr ] 

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

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

369 
by (simp add: gen_new_keys_not_analzd) 

370 

371 
lemma Crypt_parts_imp_used: 

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

373 
K \<in> symKeys; evs \<in> set_cr ] ==> Key K \<in> used evs" 

374 
apply (rule ccontr) 

375 
apply (force dest: new_keys_not_used Crypt_imp_invKey_keysFor) 

376 
done 

377 

378 
lemma Crypt_analz_imp_used: 

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

380 
K \<in> symKeys; evs \<in> set_cr ] ==> Key K \<in> used evs" 

381 
by (blast intro: Crypt_parts_imp_used) 

382 

383 

14218  384 
(*<*) 
14199  385 
subsection{*Messages signed by CA*} 
386 

387 
text{*Message @{text SET_CR2}: C can check CA's signature if he has received 

388 
CA's certificate.*} 

389 
lemma CA_Says_2_lemma: 

390 
"[ Crypt (priSK (CA i)) (Hash{Agent C, Nonce NC1}) 

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

392 
evs \<in> set_cr; (CA i) \<notin> bad ] 

393 
==> \<exists>Y. Says (CA i) C {sign (priSK (CA i)) {Agent C, Nonce NC1}, Y} 

394 
\<in> set evs" 

395 
apply (erule rev_mp) 

396 
apply (erule set_cr.induct, auto) 

397 
done 

398 

399 
text{*Ever used?*} 

400 
lemma CA_Says_2: 

401 
"[ Crypt (invKey SK) (Hash{Agent C, Nonce NC1}) 

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

403 
cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs); 

404 
evs \<in> set_cr; (CA i) \<notin> bad ] 

405 
==> \<exists>Y. Says (CA i) C {sign (priSK (CA i)) {Agent C, Nonce NC1}, Y} 

406 
\<in> set evs" 

407 
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_2_lemma) 

408 

409 

410 
text{*Message @{text SET_CR4}: C can check CA's signature if he has received 

411 
CA's certificate.*} 

412 
lemma CA_Says_4_lemma: 

413 
"[ Crypt (priSK (CA i)) (Hash{Agent C, Nonce NC2, Nonce NCA}) 

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

415 
evs \<in> set_cr; (CA i) \<notin> bad ] 

416 
==> \<exists>Y. Says (CA i) C {sign (priSK (CA i)) 

417 
{Agent C, Nonce NC2, Nonce NCA}, Y} \<in> set evs" 

418 
apply (erule rev_mp) 

419 
apply (erule set_cr.induct, auto) 

420 
done 

421 

422 
text{*NEVER USED*} 

423 
lemma CA_Says_4: 

424 
"[ Crypt (invKey SK) (Hash{Agent C, Nonce NC2, Nonce NCA}) 

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

426 
cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs); 

427 
evs \<in> set_cr; (CA i) \<notin> bad ] 

428 
==> \<exists>Y. Says (CA i) C {sign (priSK (CA i)) 

429 
{Agent C, Nonce NC2, Nonce NCA}, Y} \<in> set evs" 

430 
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_4_lemma) 

431 

432 

433 
text{*Message @{text SET_CR6}: C can check CA's signature if he has 

434 
received CA's certificate.*} 

435 
lemma CA_Says_6_lemma: 

436 
"[ Crypt (priSK (CA i)) 

437 
(Hash{Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA}) 

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

439 
evs \<in> set_cr; (CA i) \<notin> bad ] 

440 
==> \<exists>Y K. Says (CA i) C (Crypt K {sign (priSK (CA i)) 

441 
{Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA}, Y}) \<in> set evs" 

442 
apply (erule rev_mp) 

443 
apply (erule set_cr.induct, auto) 

444 
done 

445 

446 
text{*NEVER USED*} 

447 
lemma CA_Says_6: 

448 
"[ Crypt (invKey SK) (Hash{Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA}) 

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

450 
cert (CA i) SK onlySig (priSK RCA) \<in> parts (knows Spy evs); 

451 
evs \<in> set_cr; (CA i) \<notin> bad ] 

452 
==> \<exists>Y K. Says (CA i) C (Crypt K {sign (priSK (CA i)) 

453 
{Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA}, Y}) \<in> set evs" 

454 
by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma) 

14218  455 
(*>*) 
14199  456 

457 

458 
subsection{*Useful lemmas *} 

459 

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

461 
for other keys aren't needed.*} 

462 

463 
lemma parts_image_priEK: 

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

465 
evs \<in> set_cr] ==> priEK C \<in> KK  C \<in> bad" 

466 
by auto 

467 

468 
text{*trivial proof because (priEK C) never appears even in (parts evs)*} 

469 
lemma analz_image_priEK: 

470 
"evs \<in> set_cr ==> 

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

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

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

474 

475 

476 
subsection{*Secrecy of Session Keys *} 

477 

478 
subsubsection{*Lemmas about the predicate KeyCryptKey *} 

479 

480 
text{*A fresh DK cannot be associated with any other 

481 
(with respect to a given trace). *} 

482 
lemma DK_fresh_not_KeyCryptKey: 

483 
"[ Key DK \<notin> used evs; evs \<in> set_cr ] ==> ~ KeyCryptKey DK K evs" 

484 
apply (erule rev_mp) 

485 
apply (erule set_cr.induct) 

486 
apply (simp_all (no_asm_simp)) 

487 
apply (blast dest: Crypt_analz_imp_used)+ 

488 
done 

489 

490 
text{*A fresh K cannot be associated with any other. The assumption that 

491 
DK isn't a private encryption key may be an artifact of the particular 

492 
definition of KeyCryptKey.*} 

493 
lemma K_fresh_not_KeyCryptKey: 

494 
"[\<forall>C. DK \<noteq> priEK C; Key K \<notin> used evs] ==> ~ KeyCryptKey DK K evs" 

495 
apply (induct evs) 

496 
apply (auto simp add: parts_insert2 split add: event.split) 

497 
done 

498 

499 

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

501 
be known to the Spy, by @{term Spy_see_private_Key}*} 

502 
lemma cardSK_neq_priEK: 

503 
"[Key cardSK \<notin> analz (knows Spy evs); 

504 
Key cardSK : parts (knows Spy evs); 

505 
evs \<in> set_cr] ==> cardSK \<noteq> priEK C" 

506 
by blast 

507 

508 
lemma not_KeyCryptKey_cardSK [rule_format (no_asm)]: 

509 
"[cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr] ==> 

510 
Key cardSK \<notin> analz (knows Spy evs) > ~ KeyCryptKey cardSK K evs" 

511 
by (erule set_cr.induct, analz_mono_contra, auto) 

512 

513 
text{*Lemma for message 5: pubSK C is never used to encrypt Keys.*} 

514 
lemma pubSK_not_KeyCryptKey [simp]: "~ KeyCryptKey (pubSK C) K evs" 

515 
apply (induct_tac "evs") 

516 
apply (auto simp add: parts_insert2 split add: event.split) 

517 
done 

518 

519 
text{*Lemma for message 6: either cardSK is compromised (when we don't care) 

520 
or else cardSK hasn't been used to encrypt K. Previously we treated 

521 
message 5 in the same way, but the current model assumes that rule 

522 
@{text SET_CR5} is executed only by honest agents.*} 

523 
lemma msg6_KeyCryptKey_disj: 

524 
"[Gets B {Crypt KC3 {Agent C, Nonce N, Key KC2, Key cardSK, X}, Y} 

525 
\<in> set evs; 

526 
cardSK \<notin> symKeys; evs \<in> set_cr] 

527 
==> Key cardSK \<in> analz (knows Spy evs)  

528 
(\<forall>K. ~ KeyCryptKey cardSK K evs)" 

529 
by (blast dest: not_KeyCryptKey_cardSK intro: cardSK_neq_priEK) 

530 

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

532 
lemma Key_analz_image_Key_lemma: 

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

534 
==> 

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

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

537 

24123  538 
method_setup valid_certificate_tac = {* 
30549  539 
Args.goal_spec >> (fn quant => K (SIMPLE_METHOD'' quant 
540 
(fn i => 

541 
EVERY [ftac @{thm Gets_certificate_valid} i, 

542 
assume_tac i, 

543 
etac conjE i, REPEAT (hyp_subst_tac i)]))) 

42814  544 
*} 
14199  545 

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

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

548 
lemma symKey_compromise [rule_format (no_asm)]: 

549 
"evs \<in> set_cr ==> 

550 
(\<forall>SK KK. SK \<in> symKeys \<longrightarrow> (\<forall>K \<in> KK. ~ KeyCryptKey K SK evs) > 

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

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

553 
apply (erule set_cr.induct) 

554 
apply (rule_tac [!] allI) + 

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

24123  556 
apply (valid_certificate_tac [8]) {*for message 5*} 
557 
apply (valid_certificate_tac [6]) {*for message 5*} 

14199  558 
apply (erule_tac [9] msg6_KeyCryptKey_disj [THEN disjE]) 
559 
apply (simp_all 

560 
del: image_insert image_Un imp_disjL 

561 
add: analz_image_keys_simps analz_knows_absorb 

562 
analz_Key_image_insert_eq notin_image_iff 

563 
K_fresh_not_KeyCryptKey 

564 
DK_fresh_not_KeyCryptKey ball_conj_distrib 

565 
analz_image_priEK disj_simps) 

24123  566 
{*9 seconds on a 1.6GHz machine*} 
14199  567 
apply spy_analz 
14218  568 
apply blast {*3*} 
569 
apply blast {*5*} 

14199  570 
done 
571 

572 
text{*The remaining quantifiers seem to be essential. 

573 
NO NEED to assume the cardholder's OK: bad cardholders don't do anything 

574 
wrong!!*} 

575 
lemma symKey_secrecy [rule_format]: 

576 
"[CA i \<notin> bad; K \<in> symKeys; evs \<in> set_cr] 

577 
==> \<forall>X c. Says (Cardholder c) (CA i) X \<in> set evs > 

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

579 
Cardholder c \<notin> bad > 

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

581 
apply (erule set_cr.induct) 

582 
apply (frule_tac [8] Gets_certificate_valid) {*for message 5*} 

583 
apply (frule_tac [6] Gets_certificate_valid) {*for message 3*} 

584 
apply (erule_tac [11] msg6_KeyCryptKey_disj [THEN disjE]) 

585 
apply (simp_all del: image_insert image_Un imp_disjL 

586 
add: symKey_compromise fresh_notin_analz_knows_Spy 

587 
analz_image_keys_simps analz_knows_absorb 

588 
analz_Key_image_insert_eq notin_image_iff 

589 
K_fresh_not_KeyCryptKey 

590 
DK_fresh_not_KeyCryptKey 

591 
analz_image_priEK) 

24123  592 
{*2.5 seconds on a 1.6GHz machine*} 
14218  593 
apply spy_analz {*Fake*} 
14199  594 
apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used) 
595 
done 

596 

597 

598 
subsection{*Primary Goals of Cardholder Registration *} 

599 

600 
text{*The cardholder's certificate really was created by the CA, provided the 

601 
CA is uncompromised *} 

602 

603 
text{*Lemma concerning the actual signed message digest*} 

604 
lemma cert_valid_lemma: 

605 
"[Crypt (priSK (CA i)) {Hash {Nonce N, Pan(pan C)}, Key cardSK, N1} 

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

607 
CA i \<notin> bad; evs \<in> set_cr] 

608 
==> \<exists>KC2 X Y. Says (CA i) C 

609 
(Crypt KC2 

610 
{X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y}) 

611 
\<in> set evs" 

612 
apply (erule rev_mp) 

613 
apply (erule set_cr.induct) 

614 
apply (simp_all (no_asm_simp)) 

615 
apply auto 

616 
done 

617 

618 
text{*Prepackaged version for cardholder. We don't try to confirm the values 

619 
of KC2, X and Y, since they are not important.*} 

620 
lemma certificate_valid_cardSK: 

621 
"[Gets C (Crypt KC2 {X, certC (pan C) cardSK N onlySig (invKey SKi), 

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

623 
CA i \<notin> bad; evs \<in> set_cr] 

624 
==> \<exists>KC2 X Y. Says (CA i) C 

625 
(Crypt KC2 

626 
{X, certC (pan C) cardSK N onlySig (priSK (CA i)), Y}) 

627 
\<in> set evs" 

628 
by (force dest!: Gets_imp_knows_Spy [THEN parts.Inj, THEN parts.Body] 

629 
certificate_valid_pubSK cert_valid_lemma) 

630 

631 

632 
lemma Hash_imp_parts [rule_format]: 

633 
"evs \<in> set_cr 

634 
==> Hash{X, Nonce N} \<in> parts (knows Spy evs) > 

635 
Nonce N \<in> parts (knows Spy evs)" 

636 
apply (erule set_cr.induct, force) 

637 
apply (simp_all (no_asm_simp)) 

638 
apply (blast intro: parts_mono [THEN [2] rev_subsetD]) 

639 
done 

640 

641 
lemma Hash_imp_parts2 [rule_format]: 

642 
"evs \<in> set_cr 

643 
==> Hash{X, Nonce M, Y, Nonce N} \<in> parts (knows Spy evs) > 

644 
Nonce M \<in> parts (knows Spy evs) & Nonce N \<in> parts (knows Spy evs)" 

645 
apply (erule set_cr.induct, force) 

646 
apply (simp_all (no_asm_simp)) 

647 
apply (blast intro: parts_mono [THEN [2] rev_subsetD]) 

648 
done 

649 

650 

651 
subsection{*Secrecy of Nonces*} 

652 

653 
subsubsection{*Lemmas about the predicate KeyCryptNonce *} 

654 

655 
text{*A fresh DK cannot be associated with any other 

656 
(with respect to a given trace). *} 

657 
lemma DK_fresh_not_KeyCryptNonce: 

658 
"[ DK \<in> symKeys; Key DK \<notin> used evs; evs \<in> set_cr ] 

659 
==> ~ KeyCryptNonce DK K evs" 

660 
apply (erule rev_mp) 

661 
apply (erule rev_mp) 

662 
apply (erule set_cr.induct) 

663 
apply (simp_all (no_asm_simp)) 

664 
apply blast 

665 
apply blast 

666 
apply (auto simp add: DK_fresh_not_KeyCryptKey) 

667 
done 

668 

669 
text{*A fresh N cannot be associated with any other 

670 
(with respect to a given trace). *} 

671 
lemma N_fresh_not_KeyCryptNonce: 

672 
"\<forall>C. DK \<noteq> priEK C ==> Nonce N \<notin> used evs > ~ KeyCryptNonce DK N evs" 

673 
apply (induct_tac "evs") 

674 
apply (case_tac [2] "a") 

675 
apply (auto simp add: parts_insert2) 

676 
done 

677 

678 
lemma not_KeyCryptNonce_cardSK [rule_format (no_asm)]: 

679 
"[cardSK \<notin> symKeys; \<forall>C. cardSK \<noteq> priEK C; evs \<in> set_cr] ==> 

680 
Key cardSK \<notin> analz (knows Spy evs) > ~ KeyCryptNonce cardSK N evs" 

681 
apply (erule set_cr.induct, analz_mono_contra, simp_all) 

14218  682 
apply (blast dest: not_KeyCryptKey_cardSK) {*6*} 
14199  683 
done 
684 

685 
subsubsection{*Lemmas for message 5 and 6: 

686 
either cardSK is compromised (when we don't care) 

687 
or else cardSK hasn't been used to encrypt K. *} 

688 

689 
text{*Lemma for message 5: pubSK C is never used to encrypt Nonces.*} 

690 
lemma pubSK_not_KeyCryptNonce [simp]: "~ KeyCryptNonce (pubSK C) N evs" 

691 
apply (induct_tac "evs") 

692 
apply (auto simp add: parts_insert2 split add: event.split) 

693 
done 

694 

695 
text{*Lemma for message 6: either cardSK is compromised (when we don't care) 

696 
or else cardSK hasn't been used to encrypt K.*} 

697 
lemma msg6_KeyCryptNonce_disj: 

698 
"[Gets B {Crypt KC3 {Agent C, Nonce N, Key KC2, Key cardSK, X}, Y} 

699 
\<in> set evs; 

700 
cardSK \<notin> symKeys; evs \<in> set_cr] 

701 
==> Key cardSK \<in> analz (knows Spy evs)  

702 
((\<forall>K. ~ KeyCryptKey cardSK K evs) & 

703 
(\<forall>N. ~ KeyCryptNonce cardSK N evs))" 

704 
by (blast dest: not_KeyCryptKey_cardSK not_KeyCryptNonce_cardSK 

705 
intro: cardSK_neq_priEK) 

706 

707 

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

709 
lemma Nonce_analz_image_Key_lemma: 

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

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

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

713 

32404  714 

14199  715 
text{*The @{text "(no_asm)"} attribute is essential, since it retains 
716 
the quantifier and allows the simprule's condition to itself be simplified.*} 

717 
lemma Nonce_compromise [rule_format (no_asm)]: 

718 
"evs \<in> set_cr ==> 

719 
(\<forall>N KK. (\<forall>K \<in> KK. ~ KeyCryptNonce K N evs) > 

720 
(Nonce N \<in> analz (Key`KK Un (knows Spy evs))) = 

721 
(Nonce N \<in> analz (knows Spy evs)))" 

722 
apply (erule set_cr.induct) 

723 
apply (rule_tac [!] allI)+ 

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

725 
apply (frule_tac [8] Gets_certificate_valid) {*for message 5*} 

726 
apply (frule_tac [6] Gets_certificate_valid) {*for message 3*} 

727 
apply (frule_tac [11] msg6_KeyCryptNonce_disj) 

728 
apply (erule_tac [13] disjE) 

729 
apply (simp_all del: image_insert image_Un 

730 
add: symKey_compromise 

731 
analz_image_keys_simps analz_knows_absorb 

732 
analz_Key_image_insert_eq notin_image_iff 

733 
N_fresh_not_KeyCryptNonce 

734 
DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey 

735 
ball_conj_distrib analz_image_priEK) 

24123  736 
{*14 seconds on a 1.6GHz machine*} 
14218  737 
apply spy_analz {*Fake*} 
738 
apply blast {*3*} 

739 
apply blast {*5*} 

740 
txt{*Message 6*} 

32404  741 
apply (metis symKey_compromise) 
14218  742 
{*cardSK compromised*} 
14199  743 
txt{*Simplify againnecessary because the previous simplification introduces 
32404  744 
some logical connectives*} 
745 
apply (force simp del: image_insert image_Un imp_disjL 

14199  746 
simp add: analz_image_keys_simps symKey_compromise) 
14218  747 
done 
14199  748 

749 

750 
subsection{*Secrecy of CardSecret: the Cardholder's secret*} 

751 

752 
lemma NC2_not_CardSecret: 

753 
"[Crypt EKj {Key K, Pan p, Hash {Agent D, Nonce N}} 

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

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

756 
Nonce N \<notin> analz (knows Spy evs); 

757 
evs \<in> set_cr] 

758 
==> Crypt EKi {Key K', Pan p', Nonce N} \<notin> parts (knows Spy evs)" 

759 
apply (erule rev_mp) 

760 
apply (erule rev_mp) 

761 
apply (erule rev_mp) 

762 
apply (erule set_cr.induct, analz_mono_contra, simp_all) 

763 
apply (blast dest: Hash_imp_parts)+ 

764 
done 

765 

766 
lemma KC2_secure_lemma [rule_format]: 

767 
"[U = Crypt KC3 {Agent C, Nonce N, Key KC2, X}; 

768 
U \<in> parts (knows Spy evs); 

769 
evs \<in> set_cr] 

770 
==> Nonce N \<notin> analz (knows Spy evs) > 

771 
(\<exists>k i W. Says (Cardholder k) (CA i) {U,W} \<in> set evs & 

772 
Cardholder k \<notin> bad & CA i \<notin> bad)" 

773 
apply (erule_tac P = "U \<in> ?H" in rev_mp) 

774 
apply (erule set_cr.induct) 

24123  775 
apply (valid_certificate_tac [8]) {*for message 5*} 
14199  776 
apply (simp_all del: image_insert image_Un imp_disjL 
777 
add: analz_image_keys_simps analz_knows_absorb 

778 
analz_knows_absorb2 notin_image_iff) 

24123  779 
{*4 seconds on a 1.6GHz machine*} 
14199  780 
apply (simp_all (no_asm_simp)) {*leaves 4 subgoals*} 
781 
apply (blast intro!: analz_insertI)+ 

782 
done 

783 

784 
lemma KC2_secrecy: 

785 
"[Gets B {Crypt K {Agent C, Nonce N, Key KC2, X}, Y} \<in> set evs; 

786 
Nonce N \<notin> analz (knows Spy evs); KC2 \<in> symKeys; 

787 
evs \<in> set_cr] 

788 
==> Key KC2 \<notin> analz (knows Spy evs)" 

789 
by (force dest!: refl [THEN KC2_secure_lemma] symKey_secrecy) 

790 

791 

792 
text{*Inductive version*} 

793 
lemma CardSecret_secrecy_lemma [rule_format]: 

794 
"[CA i \<notin> bad; evs \<in> set_cr] 

795 
==> Key K \<notin> analz (knows Spy evs) > 

796 
Crypt (pubEK (CA i)) {Key K, Pan p, Nonce CardSecret} 

797 
\<in> parts (knows Spy evs) > 

798 
Nonce CardSecret \<notin> analz (knows Spy evs)" 

799 
apply (erule set_cr.induct, analz_mono_contra) 

24123  800 
apply (valid_certificate_tac [8]) {*for message 5*} 
801 
apply (valid_certificate_tac [6]) {*for message 5*} 

14199  802 
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE]) 
803 
apply (simp_all 

804 
del: image_insert image_Un imp_disjL 

805 
add: analz_image_keys_simps analz_knows_absorb 

806 
analz_Key_image_insert_eq notin_image_iff 

807 
EXHcrypt_def Crypt_notin_image_Key 

808 
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce 

809 
ball_conj_distrib Nonce_compromise symKey_compromise 

810 
analz_image_priEK) 

24123  811 
{*2.5 seconds on a 1.6GHz machine*} 
14218  812 
apply spy_analz {*Fake*} 
14199  813 
apply (simp_all (no_asm_simp)) 
14218  814 
apply blast {*1*} 
815 
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) {*2*} 

816 
apply blast {*3*} 

817 
apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt) {*4*} 

818 
apply blast {*5*} 

819 
apply (blast dest: KC2_secrecy)+ {*Message 6: two cases*} 

14199  820 
done 
821 

822 

823 
text{*Packaged version for cardholder*} 

824 
lemma CardSecret_secrecy: 

825 
"[Cardholder k \<notin> bad; CA i \<notin> bad; 

826 
Says (Cardholder k) (CA i) 

827 
{X, Crypt EKi {Key KC3, Pan p, Nonce CardSecret}} \<in> set evs; 

828 
Gets A {Z, cert (CA i) EKi onlyEnc (priSK RCA), 

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

830 
KC3 \<in> symKeys; evs \<in> set_cr] 

831 
==> Nonce CardSecret \<notin> analz (knows Spy evs)" 

832 
apply (frule Gets_certificate_valid, assumption) 

833 
apply (subgoal_tac "Key KC3 \<notin> analz (knows Spy evs) ") 

834 
apply (blast dest: CardSecret_secrecy_lemma) 

835 
apply (rule symKey_secrecy) 

836 
apply (auto simp add: parts_insert2) 

837 
done 

838 

839 

840 
subsection{*Secrecy of NonceCCA [the CA's secret] *} 

841 

842 
lemma NC2_not_NonceCCA: 

843 
"[Hash {Agent C', Nonce N', Agent C, Nonce N} 

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

845 
Nonce N \<notin> analz (knows Spy evs); 

846 
evs \<in> set_cr] 

847 
==> Crypt KC1 {{Agent B, Nonce N}, Hash p} \<notin> parts (knows Spy evs)" 

848 
apply (erule rev_mp) 

849 
apply (erule rev_mp) 

850 
apply (erule set_cr.induct, analz_mono_contra, simp_all) 

851 
apply (blast dest: Hash_imp_parts2)+ 

852 
done 

853 

854 

855 
text{*Inductive version*} 

856 
lemma NonceCCA_secrecy_lemma [rule_format]: 

857 
"[CA i \<notin> bad; evs \<in> set_cr] 

858 
==> Key K \<notin> analz (knows Spy evs) > 

859 
Crypt K 

860 
{sign (priSK (CA i)) 

861 
{Agent C, Nonce N, Agent(CA i), Nonce NonceCCA}, 

862 
X, Y} 

863 
\<in> parts (knows Spy evs) > 

864 
Nonce NonceCCA \<notin> analz (knows Spy evs)" 

865 
apply (erule set_cr.induct, analz_mono_contra) 

24123  866 
apply (valid_certificate_tac [8]) {*for message 5*} 
867 
apply (valid_certificate_tac [6]) {*for message 5*} 

14199  868 
apply (frule_tac [9] msg6_KeyCryptNonce_disj [THEN disjE]) 
869 
apply (simp_all 

870 
del: image_insert image_Un imp_disjL 

871 
add: analz_image_keys_simps analz_knows_absorb sign_def 

872 
analz_Key_image_insert_eq notin_image_iff 

873 
EXHcrypt_def Crypt_notin_image_Key 

874 
N_fresh_not_KeyCryptNonce DK_fresh_not_KeyCryptNonce 

875 
ball_conj_distrib Nonce_compromise symKey_compromise 

876 
analz_image_priEK) 

24123  877 
{*3 seconds on a 1.6GHz machine*} 
14218  878 
apply spy_analz {*Fake*} 
879 
apply blast {*1*} 

880 
apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj]) {*2*} 

881 
apply blast {*3*} 

882 
apply (blast dest: NC2_not_NonceCCA) {*4*} 

883 
apply blast {*5*} 

884 
apply (blast dest: KC2_secrecy)+ {*Message 6: two cases*} 

14199  885 
done 
886 

887 

888 
text{*Packaged version for cardholder*} 

889 
lemma NonceCCA_secrecy: 

890 
"[Cardholder k \<notin> bad; CA i \<notin> bad; 

891 
Gets (Cardholder k) 

892 
(Crypt KC2 

893 
{sign (priSK (CA i)) {Agent C, Nonce N, Agent(CA i), Nonce NonceCCA}, 

894 
X, Y}) \<in> set evs; 

895 
Says (Cardholder k) (CA i) 

896 
{Crypt KC3 {Agent C, Nonce NC3, Key KC2, X'}, Y'} \<in> set evs; 

897 
Gets A {Z, cert (CA i) EKi onlyEnc (priSK RCA), 

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

899 
KC2 \<in> symKeys; evs \<in> set_cr] 

900 
==> Nonce NonceCCA \<notin> analz (knows Spy evs)" 

901 
apply (frule Gets_certificate_valid, assumption) 

902 
apply (subgoal_tac "Key KC2 \<notin> analz (knows Spy evs) ") 

903 
apply (blast dest: NonceCCA_secrecy_lemma) 

904 
apply (rule symKey_secrecy) 

905 
apply (auto simp add: parts_insert2) 

906 
done 

907 

908 
text{*We don't bother to prove guarantees for the CA. He doesn't care about 

909 
the PANSecret: it isn't his credit card!*} 

910 

911 

912 
subsection{*Rewriting Rule for PANs*} 

913 

914 
text{*Lemma for message 6: either cardSK isn't a CA's private encryption key, 

915 
or if it is then (because it appears in traffic) that CA is bad, 

916 
and so the Spy knows that key already. Either way, we can simplify 

917 
the expression @{term "analz (insert (Key cardSK) X)"}.*} 

918 
lemma msg6_cardSK_disj: 

919 
"[Gets A {Crypt K {c, n, k', Key cardSK, X}, Y} 

920 
\<in> set evs; evs \<in> set_cr ] 

921 
==> cardSK \<notin> range(invKey o pubEK o CA)  Key cardSK \<in> knows Spy evs" 

922 
by auto 

923 

924 
lemma analz_image_pan_lemma: 

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

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

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

928 

929 
lemma analz_image_pan [rule_format]: 

930 
"evs \<in> set_cr ==> 

931 
\<forall>KK. KK <=  invKey ` pubEK ` range CA > 

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

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

934 
apply (erule set_cr.induct) 

935 
apply (rule_tac [!] allI impI)+ 

936 
apply (rule_tac [!] analz_image_pan_lemma) 

24123  937 
apply (valid_certificate_tac [8]) {*for message 5*} 
938 
apply (valid_certificate_tac [6]) {*for message 5*} 

14199  939 
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE]) 
940 
apply (simp_all 

941 
del: image_insert image_Un 

942 
add: analz_image_keys_simps disjoint_image_iff 

943 
notin_image_iff analz_image_priEK) 

24123  944 
{*6 seconds on a 1.6GHz machine*} 
14199  945 
apply spy_analz 
14218  946 
apply (simp add: insert_absorb) {*6*} 
14199  947 
done 
948 

949 
lemma analz_insert_pan: 

950 
"[ evs \<in> set_cr; K \<notin> invKey ` pubEK ` range CA ] ==> 

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

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

953 
by (simp del: image_insert image_Un 

954 
add: analz_image_keys_simps analz_image_pan) 

955 

956 

957 
text{*Confidentiality of the PAN\@. Maybe we could combine the statements of 

958 
this theorem with @{term analz_image_pan}, requiring a single induction but 

959 
a much more difficult proof.*} 

960 
lemma pan_confidentiality: 

961 
"[ Pan (pan C) \<in> analz(knows Spy evs); C \<noteq>Spy; evs :set_cr] 

962 
==> \<exists>i X K HN. 

963 
Says C (CA i) {X, Crypt (pubEK (CA i)) {Key K, Pan (pan C), HN} } 

964 
\<in> set evs 

965 
& (CA i) \<in> bad" 

966 
apply (erule rev_mp) 

967 
apply (erule set_cr.induct) 

24123  968 
apply (valid_certificate_tac [8]) {*for message 5*} 
969 
apply (valid_certificate_tac [6]) {*for message 5*} 

14199  970 
apply (erule_tac [9] msg6_cardSK_disj [THEN disjE]) 
971 
apply (simp_all 

972 
del: image_insert image_Un 

973 
add: analz_image_keys_simps analz_insert_pan analz_image_pan 

974 
notin_image_iff analz_image_priEK) 

24123  975 
{*3.5 seconds on a 1.6GHz machine*} 
14218  976 
apply spy_analz {*fake*} 
977 
apply blast {*3*} 

978 
apply blast {*5*} 

979 
apply (simp (no_asm_simp) add: insert_absorb) {*6*} 

14199  980 
done 
981 

982 

983 
subsection{*Unicity*} 

984 

985 
lemma CR6_Says_imp_Notes: 

986 
"[Says (CA i) C (Crypt KC2 

987 
{sign (priSK (CA i)) {Agent C, Nonce NC3, Agent (CA i), Nonce Y}, 

988 
certC (pan C) cardSK X onlySig (priSK (CA i)), 

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

990 
evs \<in> set_cr ] 

991 
==> Notes (CA i) (Key cardSK) \<in> set evs" 

992 
apply (erule rev_mp) 

993 
apply (erule set_cr.induct) 

994 
apply (simp_all (no_asm_simp)) 

995 
done 

996 

997 
text{*Unicity of cardSK: it uniquely identifies the other components. 

998 
This holds because a CA accepts a cardSK at most once.*} 

999 
lemma cardholder_key_unicity: 

1000 
"[Says (CA i) C (Crypt KC2 

1001 
{sign (priSK (CA i)) {Agent C, Nonce NC3, Agent (CA i), Nonce Y}, 

1002 
certC (pan C) cardSK X onlySig (priSK (CA i)), 

1003 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)}) 

1004 
\<in> set evs; 

1005 
Says (CA i) C' (Crypt KC2' 

1006 
{sign (priSK (CA i)) {Agent C', Nonce NC3', Agent (CA i), Nonce Y'}, 

1007 
certC (pan C') cardSK X' onlySig (priSK (CA i)), 

1008 
cert (CA i) (pubSK (CA i)) onlySig (priSK RCA)}) 

1009 
\<in> set evs; 

1010 
evs \<in> set_cr ] ==> C=C' & NC3=NC3' & X=X' & KC2=KC2' & Y=Y'" 

1011 
apply (erule rev_mp) 

1012 
apply (erule rev_mp) 

1013 
apply (erule set_cr.induct) 

1014 
apply (simp_all (no_asm_simp)) 

1015 
apply (blast dest!: CR6_Says_imp_Notes) 

1016 
done 

1017 

1018 

14218  1019 
(*<*) 
14199  1020 
text{*UNUSED unicity result*} 
1021 
lemma unique_KC1: 

1022 
"[Says C B {Crypt KC1 X, Crypt EK {Key KC1, Y}} 

1023 
\<in> set evs; 

1024 
Says C B' {Crypt KC1 X', Crypt EK' {Key KC1, Y'}} 

1025 
\<in> set evs; 

1026 
C \<notin> bad; evs \<in> set_cr] ==> B'=B & Y'=Y" 

1027 
apply (erule rev_mp) 

1028 
apply (erule rev_mp) 

1029 
apply (erule set_cr.induct, auto) 

1030 
done 

1031 

1032 
text{*UNUSED unicity result*} 

1033 
lemma unique_KC2: 

1034 
"[Says C B {Crypt K {Agent C, nn, Key KC2, X}, Y} \<in> set evs; 

1035 
Says C B' {Crypt K' {Agent C, nn', Key KC2, X'}, Y'} \<in> set evs; 

1036 
C \<notin> bad; evs \<in> set_cr] ==> B'=B & X'=X" 

1037 
apply (erule rev_mp) 

1038 
apply (erule rev_mp) 

1039 
apply (erule set_cr.induct, auto) 

1040 
done 

14218  1041 
(*>*) 
1042 

14199  1043 

1044 
text{*Cannot show cardSK to be secret because it isn't assumed to be fresh 

1045 
it could be a previously compromised cardSK [e.g. involving a bad CA]*} 

1046 

1047 

1048 
end 