author  haftmann 
Fri, 17 Jun 2005 16:12:49 +0200  
changeset 16417  9bc16273c2d4 
parent 14207  f20fbb141673 
child 23746  a455e69c31cc 
permissions  rwrr 
3445  1 
(* Title: HOL/Auth/Yahalom2 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

2 
ID: $Id$ 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

5 
*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

6 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

7 
header{*The Yahalom Protocol, Variant 2*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

8 

16417  9 
theory Yahalom2 imports Public begin 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

10 

f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

11 
text{* 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

12 
This version trades encryption of NB for additional explicitness in YM3. 
3432  13 
Also in YM3, care is taken to make the two certificates distinct. 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

14 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

15 
From page 259 of 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

16 
Burrows, Abadi and Needham (1989). A Logic of Authentication. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

17 
Proc. Royal Soc. 426 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

18 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

19 
This theory has the prototypical example of a secrecy relation, KeyCryptNonce. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

20 
*} 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

21 

11251  22 
consts yahalom :: "event list set" 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3481
diff
changeset

23 
inductive "yahalom" 
11251  24 
intros 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

25 
(*Initial trace is empty*) 
11251  26 
Nil: "[] \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

27 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

28 
(*The spy MAY say anything he CAN say. We do not expect him to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

29 
invent new nonces here, but he can also use NS1. Common to 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

30 
all similar protocols.*) 
11251  31 
Fake: "[ evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) ] 
32 
==> Says Spy B X # evsf \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

33 

6335  34 
(*A message that has been sent can be received by the 
35 
intended recipient.*) 

11251  36 
Reception: "[ evsr \<in> yahalom; Says A B X \<in> set evsr ] 
37 
==> Gets B X # evsr \<in> yahalom" 

6335  38 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

39 
(*Alice initiates a protocol run*) 
11251  40 
YM1: "[ evs1 \<in> yahalom; Nonce NA \<notin> used evs1 ] 
41 
==> Says A B {Agent A, Nonce NA} # evs1 \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

42 

6335  43 
(*Bob's response to Alice's message.*) 
11251  44 
YM2: "[ evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
45 
Gets B {Agent A, Nonce NA} \<in> set evs2 ] 

46 
==> Says B Server 

3432  47 
{Agent B, Nonce NB, Crypt (shrK B) {Agent A, Nonce NA}} 
11251  48 
# evs2 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

49 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

50 
(*The Server receives Bob's message. He responds by sending a 
3659
eddedfe2f3f8
Renamed "evs" to "evs1", "evs2", etc. in protocol inductive definition
paulson
parents:
3519
diff
changeset

51 
new session key to Alice, with a certificate for forwarding to Bob. 
5066
30271d90644f
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
paulson
parents:
4537
diff
changeset

52 
Both agents are quoted in the 2nd certificate to prevent attacks!*) 
11251  53 
YM3: "[ evs3 \<in> yahalom; Key KAB \<notin> used evs3; 
6335  54 
Gets Server {Agent B, Nonce NB, 
55 
Crypt (shrK B) {Agent A, Nonce NA}} 

11251  56 
\<in> set evs3 ] 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

57 
==> Says Server A 
11251  58 
{Nonce NB, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

59 
Crypt (shrK A) {Agent B, Key KAB, Nonce NA}, 
5066
30271d90644f
Changed format of Bob's certificate from Nb,K,A to A,B,K,Nb.
paulson
parents:
4537
diff
changeset

60 
Crypt (shrK B) {Agent A, Agent B, Key KAB, Nonce NB}} 
11251  61 
# evs3 \<in> yahalom" 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

62 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

63 
(*Alice receives the Server's (?) message, checks her Nonce, and 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

64 
uses the new session key to send Bob his Nonce.*) 
11251  65 
YM4: "[ evs4 \<in> yahalom; 
6335  66 
Gets A {Nonce NB, Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
11251  67 
X} \<in> set evs4; 
68 
Says A B {Agent A, Nonce NA} \<in> set evs4 ] 

69 
==> Says A B {X, Crypt K (Nonce NB)} # evs4 \<in> yahalom" 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

70 

2155  71 
(*This message models possible leaks of session keys. The nonces 
72 
identify the protocol run. Quoting Server here ensures they are 

73 
correct. *) 

11251  74 
Oops: "[ evso \<in> yahalom; 
75 
Says Server A {Nonce NB, 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2155
diff
changeset

76 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 
11251  77 
X} \<in> set evso ] 
78 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso \<in> yahalom" 

79 

80 

81 
declare Says_imp_knows_Spy [THEN analz.Inj, dest] 

82 
declare parts.Body [dest] 

83 
declare Fake_parts_insert_in_Un [dest] 

84 
declare analz_into_parts [dest] 

85 

13907  86 
text{*A "possibility property": there are traces that reach the end*} 
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

87 
lemma "Key K \<notin> used [] 
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

88 
==> \<exists>X NB. \<exists>evs \<in> yahalom. 
11251  89 
Says A B {X, Crypt K (Nonce NB)} \<in> set evs" 
90 
apply (intro exI bexI) 

91 
apply (rule_tac [2] yahalom.Nil 

92 
[THEN yahalom.YM1, THEN yahalom.Reception, 

93 
THEN yahalom.YM2, THEN yahalom.Reception, 

94 
THEN yahalom.YM3, THEN yahalom.Reception, 

14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset

95 
THEN yahalom.YM4]) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

96 
apply (possibility, simp add: used_Cons) 
11251  97 
done 
98 

99 
lemma Gets_imp_Says: 

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

101 
by (erule rev_mp, erule yahalom.induct, auto) 

102 

13907  103 
text{*Must be proved separately for each protocol*} 
11251  104 
lemma Gets_imp_knows_Spy: 
105 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> X \<in> knows Spy evs" 

106 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

107 

108 
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 

109 

110 

13907  111 
subsection{*Inductive Proofs*} 
11251  112 

13907  113 
text{*Result for reasoning about the encrypted portion of messages. 
114 
Lets us treat YM4 using a similar argument as for the Fake case.*} 

11251  115 
lemma YM4_analz_knows_Spy: 
116 
"[ Gets A {NB, Crypt (shrK A) Y, X} \<in> set evs; evs \<in> yahalom ] 

117 
==> X \<in> analz (knows Spy evs)" 

118 
by blast 

119 

120 
lemmas YM4_parts_knows_Spy = 

121 
YM4_analz_knows_Spy [THEN analz_into_parts, standard] 

122 

123 

124 
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY 

125 
sends messages containing X! **) 

126 

13907  127 
text{*Spy never sees a good agent's shared key!*} 
11251  128 
lemma Spy_see_shrK [simp]: 
129 
"evs \<in> yahalom ==> (Key (shrK A) \<in> parts (knows Spy evs)) = (A \<in> bad)" 

13907  130 
by (erule yahalom.induct, force, 
131 
drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 

11251  132 

133 
lemma Spy_analz_shrK [simp]: 

134 
"evs \<in> yahalom ==> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)" 

135 
by auto 

136 

137 
lemma Spy_see_shrK_D [dest!]: 

138 
"[Key (shrK A) \<in> parts (knows Spy evs); evs \<in> yahalom] ==> A \<in> bad" 

139 
by (blast dest: Spy_see_shrK) 

140 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

141 
text{*Nobody can have used nonexistent keys! 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

142 
Needed to apply @{text analz_insert_Key}*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

143 
lemma new_keys_not_used [simp]: 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

144 
"[Key K \<notin> used evs; K \<in> symKeys; evs \<in> yahalom] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

145 
==> K \<notin> keysFor (parts (spies evs))" 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

146 
apply (erule rev_mp) 
11251  147 
apply (erule yahalom.induct, force, 
148 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

13926  149 
txt{*Fake*} 
150 
apply (force dest!: keysFor_parts_insert) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

151 
txt{*YM3*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

152 
apply blast 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

153 
txt{*YM4*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

154 
apply auto 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

155 
apply (blast dest!: Gets_imp_knows_Spy [THEN parts.Inj]) 
11251  156 
done 
157 

158 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

159 
text{*Describes the form of K when the Server sends this message. Useful for 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

160 
Oops as well as main secrecy property.*} 
11251  161 
lemma Says_Server_message_form: 
162 
"[ Says Server A {nb', Crypt (shrK A) {Agent B, Key K, na}, X} 

163 
\<in> set evs; evs \<in> yahalom ] 

164 
==> K \<notin> range shrK" 

165 
by (erule rev_mp, erule yahalom.induct, simp_all) 

166 

167 

168 
(**** 

169 
The following is to prove theorems of the form 

170 

171 
Key K \<in> analz (insert (Key KAB) (knows Spy evs)) ==> 

172 
Key K \<in> analz (knows Spy evs) 

173 

174 
A more general formula must be proved inductively. 

175 
****) 

176 

177 
(** Session keys are not used to encrypt other session keys **) 

178 

179 
lemma analz_image_freshK [rule_format]: 

180 
"evs \<in> yahalom ==> 

181 
\<forall>K KK. KK <=  (range shrK) > 

182 
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = 

183 
(K \<in> KK  Key K \<in> analz (knows Spy evs))" 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

184 
apply (erule yahalom.induct) 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

185 
apply (frule_tac [8] Says_Server_message_form) 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

186 
apply (drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
11251  187 
done 
188 

189 
lemma analz_insert_freshK: 

190 
"[ evs \<in> yahalom; KAB \<notin> range shrK ] ==> 

11655  191 
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  192 
(K = KAB  Key K \<in> analz (knows Spy evs))" 
193 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

194 

195 

13907  196 
text{*The Key K uniquely identifies the Server's message*} 
11251  197 
lemma unique_session_keys: 
198 
"[ Says Server A 

199 
{nb, Crypt (shrK A) {Agent B, Key K, na}, X} \<in> set evs; 

200 
Says Server A' 

201 
{nb', Crypt (shrK A') {Agent B', Key K, na'}, X'} \<in> set evs; 

202 
evs \<in> yahalom ] 

203 
==> A=A' & B=B' & na=na' & nb=nb'" 

204 
apply (erule rev_mp, erule rev_mp) 

205 
apply (erule yahalom.induct, simp_all) 

13907  206 
txt{*YM3, by freshness*} 
11251  207 
apply blast 
208 
done 

209 

210 

13907  211 
subsection{*Crucial Secrecy Property: Spy Does Not See Key @{term KAB}*} 
11251  212 

213 
lemma secrecy_lemma: 

214 
"[ A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

215 
==> Says Server A 

216 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

217 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

218 
\<in> set evs > 

219 
Notes Spy {na, nb, Key K} \<notin> set evs > 

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

221 
apply (erule yahalom.induct, force, frule_tac [7] Says_Server_message_form, 

222 
drule_tac [6] YM4_analz_knows_Spy) 

13907  223 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) 
11251  224 
apply (blast dest: unique_session_keys)+ (*YM3, Oops*) 
225 
done 

226 

227 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

228 
text{*Final version*} 
11251  229 
lemma Spy_not_see_encrypted_key: 
230 
"[ Says Server A 

231 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

232 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

233 
\<in> set evs; 

234 
Notes Spy {na, nb, Key K} \<notin> set evs; 

235 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

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

237 
by (blast dest: secrecy_lemma Says_Server_message_form) 

238 

239 

13907  240 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

241 
text{*This form is an immediate consequence of the previous result. It is 
13907  242 
similar to the assertions established by other methods. It is equivalent 
243 
to the previous result in that the Spy already has @{term analz} and 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

244 
@{term synth} at his disposal. However, the conclusion 
13907  245 
@{term "Key K \<notin> knows Spy evs"} appears not to be inductive: all the cases 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

246 
other than Fake are trivial, while Fake requires 
13907  247 
@{term "Key K \<notin> analz (knows Spy evs)"}. *} 
248 
lemma Spy_not_know_encrypted_key: 

249 
"[ Says Server A 

250 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

251 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

252 
\<in> set evs; 

253 
Notes Spy {na, nb, Key K} \<notin> set evs; 

254 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

255 
==> Key K \<notin> knows Spy evs" 

256 
by (blast dest: Spy_not_see_encrypted_key) 

257 

258 

259 
subsection{*Security Guarantee for A upon receiving YM3*} 

11251  260 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

261 
text{*If the encrypted message appears then it originated with the Server. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

262 
May now apply @{text Spy_not_see_encrypted_key}, subject to its conditions.*} 
11251  263 
lemma A_trusts_YM3: 
264 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> parts (knows Spy evs); 

265 
A \<notin> bad; evs \<in> yahalom ] 

266 
==> \<exists>nb. Says Server A 

267 
{nb, Crypt (shrK A) {Agent B, Key K, na}, 

268 
Crypt (shrK B) {Agent A, Agent B, Key K, nb}} 

269 
\<in> set evs" 

270 
apply (erule rev_mp) 

271 
apply (erule yahalom.induct, force, 

272 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

13907  273 
txt{*Fake, YM3*} 
11251  274 
apply blast+ 
275 
done 

276 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

277 
text{*The obvious combination of @{text A_trusts_YM3} with 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

278 
@{text Spy_not_see_encrypted_key}*} 
13907  279 
theorem A_gets_good_key: 
11251  280 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> parts (knows Spy evs); 
281 
\<forall>nb. Notes Spy {na, nb, Key K} \<notin> set evs; 

282 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

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

284 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 

285 

286 

13907  287 
subsection{*Security Guarantee for B upon receiving YM4*} 
11251  288 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

289 
text{*B knows, by the first part of A's message, that the Server distributed 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

290 
the key for A and B, and has associated it with NB.*} 
11251  291 
lemma B_trusts_YM4_shrK: 
292 
"[ Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB} 

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

294 
B \<notin> bad; evs \<in> yahalom ] 

295 
==> \<exists>NA. Says Server A 

296 
{Nonce NB, 

297 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 

298 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}} 

299 
\<in> set evs" 

300 
apply (erule rev_mp) 

301 
apply (erule yahalom.induct, force, 

302 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

303 
txt{*Fake, YM3*} 
11251  304 
apply blast+ 
305 
done 

306 

307 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

308 
text{*With this protocol variant, we don't need the 2nd part of YM4 at all: 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

309 
Nonce NB is available in the first part.*} 
11251  310 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

311 
text{*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

312 
because we do not have to show that NB is secret. *} 
11251  313 
lemma B_trusts_YM4: 
314 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, X} 

315 
\<in> set evs; 

316 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

317 
==> \<exists>NA. Says Server A 

318 
{Nonce NB, 

319 
Crypt (shrK A) {Agent B, Key K, Nonce NA}, 

320 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}} 

321 
\<in> set evs" 

322 
by (blast dest!: B_trusts_YM4_shrK) 

323 

324 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

325 
text{*The obvious combination of @{text B_trusts_YM4} with 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

326 
@{text Spy_not_see_encrypted_key}*} 
13907  327 
theorem B_gets_good_key: 
11251  328 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, X} 
329 
\<in> set evs; 

330 
\<forall>na. Notes Spy {na, Nonce NB, Key K} \<notin> set evs; 

331 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

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

333 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 

334 

335 

13907  336 
subsection{*Authenticating B to A*} 
11251  337 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

338 
text{*The encryption in message YM2 tells us it cannot be faked.*} 
11251  339 
lemma B_Said_YM2: 
340 
"[ Crypt (shrK B) {Agent A, Nonce NA} \<in> parts (knows Spy evs); 

341 
B \<notin> bad; evs \<in> yahalom ] 

342 
==> \<exists>NB. Says B Server {Agent B, Nonce NB, 

343 
Crypt (shrK B) {Agent A, Nonce NA}} 

344 
\<in> set evs" 

345 
apply (erule rev_mp) 

346 
apply (erule yahalom.induct, force, 

347 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

348 
txt{*Fake, YM2*} 
11251  349 
apply blast+ 
350 
done 

351 

352 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

353 
text{*If the server sends YM3 then B sent YM2, perhaps with a different NB*} 
11251  354 
lemma YM3_auth_B_to_A_lemma: 
355 
"[ Says Server A {nb, Crypt (shrK A) {Agent B, Key K, Nonce NA}, X} 

356 
\<in> set evs; 

357 
B \<notin> bad; evs \<in> yahalom ] 

358 
==> \<exists>nb'. Says B Server {Agent B, nb', 

359 
Crypt (shrK B) {Agent A, Nonce NA}} 

360 
\<in> set evs" 

361 
apply (erule rev_mp) 

362 
apply (erule yahalom.induct, simp_all) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

363 
txt{*Fake, YM2, YM3*} 
11251  364 
apply (blast dest!: B_Said_YM2)+ 
365 
done 

366 

13907  367 
text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*} 
368 
theorem YM3_auth_B_to_A: 

11251  369 
"[ Gets A {nb, Crypt (shrK A) {Agent B, Key K, Nonce NA}, X} 
370 
\<in> set evs; 

371 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 

372 
==> \<exists>nb'. Says B Server 

373 
{Agent B, nb', Crypt (shrK B) {Agent A, Nonce NA}} 

374 
\<in> set evs" 

375 
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 

376 

377 

13907  378 
subsection{*Authenticating A to B*} 
11251  379 

13907  380 
text{*using the certificate @{term "Crypt K (Nonce NB)"}*} 
11251  381 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

382 
text{*Assuming the session key is secure, if both certificates are present then 
11251  383 
A has said NB. We can't be sure about the rest of A's message, but only 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

384 
NB matters for freshness. Note that @{term "Key K \<notin> analz (knows Spy evs)"} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

385 
must be the FIRST antecedent of the induction formula.*} 
11251  386 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

387 
text{*This lemma allows a use of @{text unique_session_keys} in the next proof, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

388 
which otherwise is extremely slow.*} 
11251  389 
lemma secure_unique_session_keys: 
390 
"[ Crypt (shrK A) {Agent B, Key K, na} \<in> analz (spies evs); 

391 
Crypt (shrK A') {Agent B', Key K, na'} \<in> analz (spies evs); 

392 
Key K \<notin> analz (knows Spy evs); evs \<in> yahalom ] 

393 
==> A=A' & B=B'" 

394 
by (blast dest!: A_trusts_YM3 dest: unique_session_keys Crypt_Spy_analz_bad) 

395 

396 

397 
lemma Auth_A_to_B_lemma [rule_format]: 

398 
"evs \<in> yahalom 

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

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

400 
K \<in> symKeys > 
11251  401 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 
402 
Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB} 

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

404 
B \<notin> bad > 

405 
(\<exists>X. Says A B {X, Crypt K (Nonce NB)} \<in> set evs)" 

406 
apply (erule yahalom.induct, force, 

407 
frule_tac [6] YM4_parts_knows_Spy) 

408 
apply (analz_mono_contra, simp_all) 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

409 
txt{*Fake*} 
11251  410 
apply blast 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

411 
txt{*YM3: by @{text new_keys_not_used}, the message 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

412 
@{term "Crypt K (Nonce NB)"} could not exist*} 
11251  413 
apply (force dest!: Crypt_imp_keysFor) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

414 
txt{*YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If so, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

415 
apply unicity of session keys; if not, use the induction hypothesis*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

416 
apply (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys) 
11251  417 
done 
418 

419 

13907  420 
text{*If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  421 
Moreover, A associates K with NB (thus is talking about the same run). 
13907  422 
Other premises guarantee secrecy of K.*} 
423 
theorem YM4_imp_A_Said_YM3 [rule_format]: 

11251  424 
"[ Gets B {Crypt (shrK B) {Agent A, Agent B, Key K, Nonce NB}, 
425 
Crypt K (Nonce NB)} \<in> set evs; 

426 
(\<forall>NA. Notes Spy {Nonce NA, Nonce NB, Key K} \<notin> set evs); 

14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

427 
K \<in> symKeys; A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
11251  428 
==> \<exists>X. Says A B {X, Crypt K (Nonce NB)} \<in> set evs" 
429 
by (blast intro: Auth_A_to_B_lemma 

430 
dest: Spy_not_see_encrypted_key B_trusts_YM4_shrK) 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

431 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

432 
end 