author  berghofe 
Wed, 11 Jul 2007 11:14:51 +0200  
changeset 23746  a455e69c31cc 
parent 16417  9bc16273c2d4 
child 32960  69916a850301 
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 

23746  22 
inductive_set yahalom :: "event list set" 
23 
where 

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

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

26 

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

27 
(*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

28 
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

29 
all similar protocols.*) 
23746  30 
 Fake: "[ evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) ] 
11251  31 
==> 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

32 

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

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

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

38 
(*Alice initiates a protocol run*) 
23746  39 
 YM1: "[ evs1 \<in> yahalom; Nonce NA \<notin> used evs1 ] 
11251  40 
==> 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

41 

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

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

48 

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

49 
(*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

50 
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

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

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

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

58 
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

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

61 

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

62 
(*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

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

68 
==> 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

69 

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

72 
correct. *) 

23746  73 
 Oops: "[ evso \<in> yahalom; 
11251  74 
Says Server A {Nonce NB, 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2155
diff
changeset

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

78 

79 

80 
declare Says_imp_knows_Spy [THEN analz.Inj, dest] 

81 
declare parts.Body [dest] 

82 
declare Fake_parts_insert_in_Un [dest] 

83 
declare analz_into_parts [dest] 

84 

13907  85 
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

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

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

90 
apply (rule_tac [2] yahalom.Nil 

91 
[THEN yahalom.YM1, THEN yahalom.Reception, 

92 
THEN yahalom.YM2, THEN yahalom.Reception, 

93 
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

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

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

98 
lemma Gets_imp_Says: 

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

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

101 

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

105 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

106 

107 
declare Gets_imp_knows_Spy [THEN analz.Inj, dest] 

108 

109 

13907  110 
subsection{*Inductive Proofs*} 
11251  111 

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

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

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

117 
by blast 

118 

119 
lemmas YM4_parts_knows_Spy = 

120 
YM4_analz_knows_Spy [THEN analz_into_parts, standard] 

121 

122 

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

124 
sends messages containing X! **) 

125 

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

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

11251  131 

132 
lemma Spy_analz_shrK [simp]: 

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

134 
by auto 

135 

136 
lemma Spy_see_shrK_D [dest!]: 

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

138 
by (blast dest: Spy_see_shrK) 

139 

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

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

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

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

143 
"[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

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

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

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

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

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

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

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

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

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

157 

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

158 
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

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

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

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

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

165 

166 

167 
(**** 

168 
The following is to prove theorems of the form 

169 

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

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

172 

173 
A more general formula must be proved inductively. 

174 
****) 

175 

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

177 

178 
lemma analz_image_freshK [rule_format]: 

179 
"evs \<in> yahalom ==> 

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

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

182 
(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

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

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

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

188 
lemma analz_insert_freshK: 

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

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

193 

194 

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

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

199 
Says Server A' 

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

201 
evs \<in> yahalom ] 

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

203 
apply (erule rev_mp, erule rev_mp) 

204 
apply (erule yahalom.induct, simp_all) 

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

208 

209 

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

212 
lemma secrecy_lemma: 

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

214 
==> Says Server A 

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

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

217 
\<in> set evs > 

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

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

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

221 
drule_tac [6] YM4_analz_knows_Spy) 

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

225 

226 

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

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

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

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

232 
\<in> set evs; 

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

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

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

236 
by (blast dest: secrecy_lemma Says_Server_message_form) 

237 

238 

13907  239 

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

240 
text{*This form is an immediate consequence of the previous result. It is 
13907  241 
similar to the assertions established by other methods. It is equivalent 
242 
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

243 
@{term synth} at his disposal. However, the conclusion 
13907  244 
@{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

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

248 
"[ Says Server A 

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

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

251 
\<in> set evs; 

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

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

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

255 
by (blast dest: Spy_not_see_encrypted_key) 

256 

257 

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

11251  259 

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

260 
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

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

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

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

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

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

268 
\<in> set evs" 

269 
apply (erule rev_mp) 

270 
apply (erule yahalom.induct, force, 

271 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 

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

275 

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

276 
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

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

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

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

283 
by (blast dest!: A_trusts_YM3 Spy_not_see_encrypted_key) 

284 

285 

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

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

288 
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

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

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

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

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

295 
{Nonce NB, 

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

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

298 
\<in> set evs" 

299 
apply (erule rev_mp) 

300 
apply (erule yahalom.induct, force, 

301 
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

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

305 

306 

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

307 
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

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

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

310 
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

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

314 
\<in> set evs; 

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

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

317 
{Nonce NB, 

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

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

320 
\<in> set evs" 

321 
by (blast dest!: B_trusts_YM4_shrK) 

322 

323 

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

324 
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

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

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

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

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

332 
by (blast dest!: B_trusts_YM4 Spy_not_see_encrypted_key) 

333 

334 

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

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

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

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

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

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

343 
\<in> set evs" 

344 
apply (erule rev_mp) 

345 
apply (erule yahalom.induct, force, 

346 
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

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

350 

351 

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

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

355 
\<in> set evs; 

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

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

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

359 
\<in> set evs" 

360 
apply (erule rev_mp) 

361 
apply (erule yahalom.induct, simp_all) 

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

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

365 

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

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

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

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

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

373 
\<in> set evs" 

374 
by (blast dest!: A_trusts_YM3 YM3_auth_B_to_A_lemma) 

375 

376 

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

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

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

381 
text{*Assuming the session key is secure, if both certificates are present then 
11251  382 
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

383 
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

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

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

386 
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

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

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

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

392 
==> A=A' & B=B'" 

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

394 

395 

396 
lemma Auth_A_to_B_lemma [rule_format]: 

397 
"evs \<in> yahalom 

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

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

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

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

403 
B \<notin> bad > 

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

405 
apply (erule yahalom.induct, force, 

406 
frule_tac [6] YM4_parts_knows_Spy) 

407 
apply (analz_mono_contra, simp_all) 

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

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

410 
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

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

413 
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

414 
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

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

418 

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

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

425 
(\<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

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

429 
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

430 

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

431 
end 