author  haftmann 
Mon, 01 Mar 2010 13:40:23 +0100  
changeset 35416  d8d7d1b785af 
parent 32960  69916a850301 
child 37936  1e4c5015a72e 
permissions  rwrr 
1995  1 
(* Title: HOL/Auth/Yahalom 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
ID: $Id$ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

6 

13956  7 
header{*The Yahalom Protocol*} 
8 

16417  9 
theory Yahalom 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{*From page 257 of 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

13 
Proc. Royal Soc. 426 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

14 

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

15 
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

16 
*} 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

17 

23746  18 
inductive_set yahalom :: "event list set" 
19 
where 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

20 
(*Initial trace is empty*) 
11251  21 
Nil: "[] \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

22 

2032  23 
(*The spy MAY say anything he CAN say. We do not expect him to 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

24 
invent new nonces here, but he can also use NS1. Common to 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

25 
all similar protocols.*) 
23746  26 
 Fake: "[ evsf \<in> yahalom; X \<in> synth (analz (knows Spy evsf)) ] 
11251  27 
==> Says Spy B X # evsf \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

28 

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

23746  31 
 Reception: "[ evsr \<in> yahalom; Says A B X \<in> set evsr ] 
11251  32 
==> Gets B X # evsr \<in> yahalom" 
6335  33 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

34 
(*Alice initiates a protocol run*) 
23746  35 
 YM1: "[ evs1 \<in> yahalom; Nonce NA \<notin> used evs1 ] 
11251  36 
==> Says A B {Agent A, Nonce NA} # evs1 \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

37 

6335  38 
(*Bob's response to Alice's message.*) 
23746  39 
 YM2: "[ evs2 \<in> yahalom; Nonce NB \<notin> used evs2; 
11251  40 
Gets B {Agent A, Nonce NA} \<in> set evs2 ] 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

41 
==> Says B Server 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

42 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
11251  43 
# evs2 \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

45 
(*The Server receives Bob's message. He responds by sending a 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

46 
new session key to Alice, with a packet for forwarding to Bob.*) 
23746  47 
 YM3: "[ evs3 \<in> yahalom; Key KAB \<notin> used evs3; KAB \<in> symKeys; 
6335  48 
Gets Server 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

49 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
11251  50 
\<in> set evs3 ] 
1995  51 
==> Says Server A 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

52 
{Crypt (shrK A) {Agent B, Key KAB, Nonce NA, Nonce NB}, 
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

53 
Crypt (shrK B) {Agent A, Key KAB}} 
11251  54 
# evs3 \<in> yahalom" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

55 

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

57 
{*Alice receives the Server's (?) message, checks her Nonce, and 
3961  58 
uses the new session key to send Bob his Nonce. The premise 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

59 
@{term "A \<noteq> Server"} is needed for @{text Says_Server_not_range}. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

60 
Alice can check that K is symmetric by its length.*} 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32377
diff
changeset

61 
"[ evs4 \<in> yahalom; A \<noteq> Server; K \<in> symKeys; 
6335  62 
Gets A {Crypt(shrK A) {Agent B, Key K, Nonce NA, Nonce NB}, X} 
11251  63 
\<in> set evs4; 
64 
Says A B {Agent A, Nonce NA} \<in> set evs4 ] 

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

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

66 

2110  67 
(*This message models possible leaks of session keys. The Nonces 
2156  68 
identify the protocol run. Quoting Server here ensures they are 
69 
correct.*) 

23746  70 
 Oops: "[ evso \<in> yahalom; 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

71 
Says Server A {Crypt (shrK A) 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2156
diff
changeset

72 
{Agent B, Key K, Nonce NA, Nonce NB}, 
11251  73 
X} \<in> set evso ] 
74 
==> Notes Spy {Nonce NA, Nonce NB, Key K} # evso \<in> yahalom" 

2110  75 

3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

76 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset

77 
definition KeyWithNonce :: "[key, nat, event list] => bool" where 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

78 
"KeyWithNonce K NB evs == 
11251  79 
\<exists>A B na X. 
3447
c7c8c0db05b9
Defines KeyWithNonce, which is used to prove the secrecy of NB
paulson
parents:
2516
diff
changeset

80 
Says Server A {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} 
11251  81 
\<in> set evs" 
82 

83 

18570  84 
declare Says_imp_analz_Spy [dest] 
11251  85 
declare parts.Body [dest] 
86 
declare Fake_parts_insert_in_Un [dest] 

87 
declare analz_into_parts [dest] 

88 

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

89 
text{*A "possibility property": there are traces that reach the end*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

90 
lemma "[ A \<noteq> Server; K \<in> symKeys; Key K \<notin> used [] ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

94 
apply (rule_tac [2] yahalom.Nil 

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

95 
[THEN yahalom.YM1, THEN yahalom.Reception, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

96 
THEN yahalom.YM2, THEN yahalom.Reception, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

97 
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

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

99 
apply (possibility, simp add: used_Cons) 
11251  100 
done 
101 

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

102 

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

103 
subsection{*Regularity Lemmas for Yahalom*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

104 

11251  105 
lemma Gets_imp_Says: 
106 
"[ Gets B X \<in> set evs; evs \<in> yahalom ] ==> \<exists>A. Says A B X \<in> set evs" 

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

108 

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

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

112 
by (blast dest!: Gets_imp_Says Says_imp_knows_Spy) 

113 

18570  114 
lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj] 
115 
declare Gets_imp_analz_Spy [dest] 

11251  116 

117 

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

118 
text{*Lets us treat YM4 using a similar argument as for the Fake case.*} 
11251  119 
lemma YM4_analz_knows_Spy: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

120 
"[ Gets A {Crypt (shrK A) Y, X} \<in> set evs; evs \<in> yahalom ] 
11251  121 
==> X \<in> analz (knows Spy evs)" 
122 
by blast 

123 

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

124 
lemmas YM4_parts_knows_Spy = 
11251  125 
YM4_analz_knows_Spy [THEN analz_into_parts, standard] 
126 

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

127 
text{*For Oops*} 
11251  128 
lemma YM4_Key_parts_knows_Spy: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

129 
"Says Server A {Crypt (shrK A) {B,K,NA,NB}, X} \<in> set evs 
11251  130 
==> K \<in> parts (knows Spy evs)" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

131 
by (metis parts.Body parts.Fst parts.Snd Says_imp_knows_Spy parts.Inj) 
11251  132 

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

133 
text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

134 
that NOBODY sends messages containing X! *} 
11251  135 

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

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

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

139 
by (erule yahalom.induct, force, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

140 
drule_tac [6] YM4_parts_knows_Spy, simp_all, blast+) 
11251  141 

142 
lemma Spy_analz_shrK [simp]: 

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

144 
by auto 

145 

146 
lemma Spy_see_shrK_D [dest!]: 

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

148 
by (blast dest: Spy_see_shrK) 

149 

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

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

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

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

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

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

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

156 
apply (erule yahalom.induct, force, 
11251  157 
frule_tac [6] YM4_parts_knows_Spy, simp_all) 
13926  158 
txt{*Fake*} 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

159 
apply (force dest!: keysFor_parts_insert, auto) 
11251  160 
done 
161 

162 

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

163 
text{*Earlier, all protocol proofs declared this theorem. 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

164 
But only a few proofs need it, e.g. Yahalom and Kerberos IV.*} 
11251  165 
lemma new_keys_not_analzd: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

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

168 
by (blast dest: new_keys_not_used intro: keysFor_mono [THEN subsetD]) 
11251  169 

170 

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

171 
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

172 
Oops as well as main secrecy property.*} 
11251  173 
lemma Says_Server_not_range [simp]: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

174 
"[ Says Server A {Crypt (shrK A) {Agent B, Key K, na, nb}, X} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

175 
\<in> set evs; evs \<in> yahalom ] 
11251  176 
==> K \<notin> range shrK" 
17778  177 
by (erule rev_mp, erule yahalom.induct, simp_all) 
11251  178 

179 

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

180 
subsection{*Secrecy Theorems*} 
11251  181 

182 
(**** 

183 
The following is to prove theorems of the form 

184 

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

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

187 

188 
A more general formula must be proved inductively. 

189 
****) 

190 

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

191 
text{* Session keys are not used to encrypt other session keys *} 
11251  192 

193 
lemma analz_image_freshK [rule_format]: 

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

194 
"evs \<in> yahalom ==> 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

195 
\<forall>K KK. KK <=  (range shrK) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

196 
(Key K \<in> analz (Key`KK Un (knows Spy evs))) = 
11251  197 
(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

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

199 
drule_tac [7] YM4_analz_knows_Spy, analz_freshK, spy_analz, blast) 
11251  200 
apply (simp only: Says_Server_not_range analz_image_freshK_simps) 
201 
done 

202 

203 
lemma analz_insert_freshK: 

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

204 
"[ evs \<in> yahalom; KAB \<notin> range shrK ] ==> 
11655  205 
(Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  206 
(K = KAB  Key K \<in> analz (knows Spy evs))" 
207 
by (simp only: analz_image_freshK analz_image_freshK_simps) 

208 

209 

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

210 
text{*The Key K uniquely identifies the Server's message.*} 
11251  211 
lemma unique_session_keys: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

212 
"[ Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

213 
{Crypt (shrK A) {Agent B, Key K, na, nb}, X} \<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

214 
Says Server A' 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

215 
{Crypt (shrK A') {Agent B', Key K, na', nb'}, X'} \<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

216 
evs \<in> yahalom ] 
11251  217 
==> A=A' & B=B' & na=na' & nb=nb'" 
218 
apply (erule rev_mp, erule rev_mp) 

219 
apply (erule yahalom.induct, simp_all) 

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

220 
txt{*YM3, by freshness, and YM4*} 
11251  221 
apply blast+ 
222 
done 

223 

224 

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

225 
text{*Crucial secrecy property: Spy does not see the keys sent in msg YM3*} 
11251  226 
lemma secrecy_lemma: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

227 
"[ A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

228 
==> Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

229 
{Crypt (shrK A) {Agent B, Key K, na, nb}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

230 
Crypt (shrK B) {Agent A, Key K}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

231 
\<in> set evs > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

232 
Notes Spy {na, nb, Key K} \<notin> set evs > 
11251  233 
Key K \<notin> analz (knows Spy evs)" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

234 
apply (erule yahalom.induct, force, 
11251  235 
drule_tac [6] YM4_analz_knows_Spy) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

236 
apply (simp_all add: pushes analz_insert_eq analz_insert_freshK, spy_analz) {*Fake*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

237 
apply (blast dest: unique_session_keys)+ {*YM3, Oops*} 
11251  238 
done 
239 

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

240 
text{*Final version*} 
11251  241 
lemma Spy_not_see_encrypted_key: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

242 
"[ Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

243 
{Crypt (shrK A) {Agent B, Key K, na, nb}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

244 
Crypt (shrK B) {Agent A, Key K}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

245 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

246 
Notes Spy {na, nb, Key K} \<notin> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

247 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
11251  248 
==> Key K \<notin> analz (knows Spy evs)" 
249 
by (blast dest: secrecy_lemma) 

250 

251 

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

252 
subsubsection{* Security Guarantee for A upon receiving YM3 *} 
11251  253 

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

254 
text{*If the encrypted message appears then it originated with the Server*} 
11251  255 
lemma A_trusts_YM3: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

256 
"[ Crypt (shrK A) {Agent B, Key K, na, nb} \<in> parts (knows Spy evs); 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

257 
A \<notin> bad; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

258 
==> Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

259 
{Crypt (shrK A) {Agent B, Key K, na, nb}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

260 
Crypt (shrK B) {Agent A, Key K}} 
11251  261 
\<in> set evs" 
262 
apply (erule rev_mp) 

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

263 
apply (erule yahalom.induct, force, 
11251  264 
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

265 
txt{*Fake, YM3*} 
11251  266 
apply blast+ 
267 
done 

268 

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

269 
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

270 
@{text Spy_not_see_encrypted_key}*} 
11251  271 
lemma A_gets_good_key: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

272 
"[ Crypt (shrK A) {Agent B, Key K, na, nb} \<in> parts (knows Spy evs); 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

273 
Notes Spy {na, nb, Key K} \<notin> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

274 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
11251  275 
==> Key K \<notin> analz (knows Spy evs)" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

276 
by (metis A_trusts_YM3 secrecy_lemma) 
11251  277 

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

278 

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

279 
subsubsection{* Security Guarantees for B upon receiving YM4 *} 
11251  280 

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

281 
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

282 
the key for A and B. But this part says nothing about nonces.*} 
11251  283 
lemma B_trusts_YM4_shrK: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

284 
"[ Crypt (shrK B) {Agent A, Key K} \<in> parts (knows Spy evs); 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

285 
B \<notin> bad; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

286 
==> \<exists>NA NB. Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

287 
{Crypt (shrK A) {Agent B, Key K, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

288 
Nonce NA, Nonce NB}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

289 
Crypt (shrK B) {Agent A, Key K}} 
11251  290 
\<in> set evs" 
291 
apply (erule rev_mp) 

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

292 
apply (erule yahalom.induct, force, 
11251  293 
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

294 
txt{*Fake, YM3*} 
11251  295 
apply blast+ 
296 
done 

297 

17411  298 
text{*B knows, by the second part of A's message, that the Server 
299 
distributed the key quoting nonce NB. This part says nothing about 

300 
agent names. Secrecy of NB is crucial. Note that @{term "Nonce NB 

301 
\<notin> analz(knows Spy evs)"} must be the FIRST antecedent of the 

302 
induction formula.*} 

303 

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

304 
lemma B_trusts_YM4_newK [rule_format]: 
11251  305 
"[Crypt K (Nonce NB) \<in> parts (knows Spy evs); 
306 
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom] 

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

307 
==> \<exists>A B NA. Says Server A 
11251  308 
{Crypt (shrK A) {Agent B, Key K, Nonce NA, Nonce NB}, 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

309 
Crypt (shrK B) {Agent A, Key K}} 
11251  310 
\<in> set evs" 
311 
apply (erule rev_mp, erule rev_mp) 

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

312 
apply (erule yahalom.induct, force, 
11251  313 
frule_tac [6] YM4_parts_knows_Spy) 
314 
apply (analz_mono_contra, simp_all) 

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

315 
txt{*Fake, YM3*} 
11251  316 
apply blast 
317 
apply blast 

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

318 
txt{*YM4. A is uncompromised because NB is secure 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

319 
A's certificate guarantees the existence of the Server message*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

320 
apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

321 
dest: Says_imp_spies 
11251  322 
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3]) 
323 
done 

324 

325 

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

326 
subsubsection{* Towards proving secrecy of Nonce NB *} 
11251  327 

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

328 
text{*Lemmas about the predicate KeyWithNonce*} 
11251  329 

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

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

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

332 
{Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} 
11251  333 
\<in> set evs ==> KeyWithNonce K NB evs" 
334 
by (unfold KeyWithNonce_def, blast) 

335 

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

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

337 
"KeyWithNonce K NB (Says S A X # evs) = 
11251  338 
(Server = S & 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

339 
(\<exists>B n X'. X = {Crypt (shrK A) {Agent B, Key K, n, Nonce NB}, X'}) 
11251  340 
 KeyWithNonce K NB evs)" 
341 
by (simp add: KeyWithNonce_def, blast) 

342 

343 

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

344 
lemma KeyWithNonce_Notes [simp]: 
11251  345 
"KeyWithNonce K NB (Notes A X # evs) = KeyWithNonce K NB evs" 
346 
by (simp add: KeyWithNonce_def) 

347 

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

348 
lemma KeyWithNonce_Gets [simp]: 
11251  349 
"KeyWithNonce K NB (Gets A X # evs) = KeyWithNonce K NB evs" 
350 
by (simp add: KeyWithNonce_def) 

351 

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

352 
text{*A fresh key cannot be associated with any nonce 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

353 
(with respect to a given trace). *} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

355 
"Key K \<notin> used evs ==> ~ KeyWithNonce K NB evs" 
11251  356 
by (unfold KeyWithNonce_def, blast) 
357 

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

358 
text{*The Server message associates K with NB' and therefore not with any 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

359 
other nonce NB.*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

361 
"[ Says Server A {Crypt (shrK A) {Agent B, Key K, na, Nonce NB'}, X} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

362 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

363 
NB \<noteq> NB'; evs \<in> yahalom ] 
11251  364 
==> ~ KeyWithNonce K NB evs" 
365 
by (unfold KeyWithNonce_def, blast dest: unique_session_keys) 

366 

367 

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

368 
text{*The only nonces that can be found with the help of session keys are 
11251  369 
those distributed as nonce NB by the Server. The form of the theorem 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

370 
recalls @{text analz_image_freshK}, but it is much more complicated.*} 
11251  371 

372 

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

373 
text{*As with @{text analz_image_freshK}, we take some pains to express the 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

374 
property as a logical equivalence so that the simplifier can apply it.*} 
11251  375 
lemma Nonce_secrecy_lemma: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

376 
"P > (X \<in> analz (G Un H)) > (X \<in> analz H) ==> 
11251  377 
P > (X \<in> analz (G Un H)) = (X \<in> analz H)" 
378 
by (blast intro: analz_mono [THEN subsetD]) 

379 

380 
lemma Nonce_secrecy: 

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

381 
"evs \<in> yahalom ==> 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

382 
(\<forall>KK. KK <=  (range shrK) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

383 
(\<forall>K \<in> KK. K \<in> symKeys > ~ KeyWithNonce K NB evs) > 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

384 
(Nonce NB \<in> analz (Key`KK Un (knows Spy evs))) = 
11251  385 
(Nonce NB \<in> analz (knows Spy evs)))" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

387 
frule_tac [7] YM4_analz_knows_Spy) 
11251  388 
apply (safe del: allI impI intro!: Nonce_secrecy_lemma [THEN impI, THEN allI]) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

389 
apply (simp_all del: image_insert image_Un 
11251  390 
add: analz_image_freshK_simps split_ifs 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

391 
all_conj_distrib ball_conj_distrib 
11251  392 
analz_image_freshK fresh_not_KeyWithNonce 
393 
imp_disj_not1 (*Moves NBa\<noteq>NB to the front*) 

394 
Says_Server_KeyWithNonce) 

17411  395 
txt{*For Oops, simplification proves @{prop "NBa\<noteq>NB"}. By 
396 
@{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB 

397 
evs"}; then simplification can apply the induction hypothesis with 

398 
@{term "KK = {K}"}.*} 

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

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

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

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

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

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

405 
txt{*YM4*} 
13507  406 
apply (erule_tac V = "\<forall>KK. ?P KK" in thin_rl, clarify) 
17411  407 
txt{*If @{prop "A \<in> bad"} then @{term NBa} is known, therefore 
408 
@{prop "NBa \<noteq> NB"}. Previous two steps make the next step 

409 
faster.*} 

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

410 
apply (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def 
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

411 
Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj) 
11251  412 
done 
413 

414 

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

415 
text{*Version required below: if NB can be decrypted using a session key then 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

416 
it was distributed with that key. The more general form above is required 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

417 
for the induction to carry through.*} 
11251  418 
lemma single_Nonce_secrecy: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

419 
"[ Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

420 
{Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

421 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

422 
NB \<noteq> NB'; KAB \<notin> range shrK; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

423 
==> (Nonce NB \<in> analz (insert (Key KAB) (knows Spy evs))) = 
11251  424 
(Nonce NB \<in> analz (knows Spy evs))" 
425 
by (simp_all del: image_insert image_Un imp_disjL 

426 
add: analz_image_freshK_simps split_ifs 

13507  427 
Nonce_secrecy Says_Server_KeyWithNonce) 
11251  428 

429 

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

430 
subsubsection{* The Nonce NB uniquely identifies B's message. *} 
11251  431 

432 
lemma unique_NB: 

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

433 
"[ Crypt (shrK B) {Agent A, Nonce NA, nb} \<in> parts (knows Spy evs); 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

434 
Crypt (shrK B') {Agent A', Nonce NA', nb} \<in> parts (knows Spy evs); 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

435 
evs \<in> yahalom; B \<notin> bad; B' \<notin> bad ] 
11251  436 
==> NA' = NA & A' = A & B' = B" 
437 
apply (erule rev_mp, erule rev_mp) 

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

438 
apply (erule yahalom.induct, force, 
11251  439 
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

440 
txt{*Fake, and YM2 by freshness*} 
11251  441 
apply blast+ 
442 
done 

443 

444 

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

445 
text{*Variant useful for proving secrecy of NB. Because nb is assumed to be 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

446 
secret, we no longer must assume B, B' not bad.*} 
11251  447 
lemma Says_unique_NB: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

448 
"[ Says C S {X, Crypt (shrK B) {Agent A, Nonce NA, nb}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

449 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

450 
Gets S' {X', Crypt (shrK B') {Agent A', Nonce NA', nb}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

451 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

452 
nb \<notin> analz (knows Spy evs); evs \<in> yahalom ] 
11251  453 
==> NA' = NA & A' = A & B' = B" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

454 
by (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad 
11251  455 
dest: Says_imp_spies unique_NB parts.Inj analz.Inj) 
456 

457 

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

458 
subsubsection{* A nonce value is never used both as NA and as NB *} 
11251  459 

460 
lemma no_nonce_YM1_YM2: 

461 
"[Crypt (shrK B') {Agent A', Nonce NB, nb'} \<in> parts(knows Spy evs); 

462 
Nonce NB \<notin> analz (knows Spy evs); evs \<in> yahalom] 

463 
==> Crypt (shrK B) {Agent A, na, Nonce NB} \<notin> parts(knows Spy evs)" 

464 
apply (erule rev_mp, erule rev_mp) 

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

465 
apply (erule yahalom.induct, force, 
11251  466 
frule_tac [6] YM4_parts_knows_Spy) 
467 
apply (analz_mono_contra, simp_all) 

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

468 
txt{*Fake, YM2*} 
11251  469 
apply blast+ 
470 
done 

471 

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

472 
text{*The Server sends YM3 only in response to YM2.*} 
11251  473 
lemma Says_Server_imp_YM2: 
474 
"[ Says Server A {Crypt (shrK A) {Agent B, k, na, nb}, X} \<in> set evs; 

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

475 
evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

476 
==> Gets Server { Agent B, Crypt (shrK B) {Agent A, na, nb} } 
11251  477 
\<in> set evs" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

478 
by (erule rev_mp, erule yahalom.induct, auto) 
11251  479 

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

480 
text{*A vital theorem for B, that nonce NB remains secure from the Spy.*} 
11251  481 
lemma Spy_not_see_NB : 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

482 
"[ Says B Server 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32377
diff
changeset

483 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32377
diff
changeset

484 
\<in> set evs; 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32377
diff
changeset

485 
(\<forall>k. Notes Spy {Nonce NA, Nonce NB, k} \<notin> set evs); 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

486 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
11251  487 
==> Nonce NB \<notin> analz (knows Spy evs)" 
488 
apply (erule rev_mp, erule rev_mp) 

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

489 
apply (erule yahalom.induct, force, 
11251  490 
frule_tac [6] YM4_analz_knows_Spy) 
491 
apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq 

492 
analz_insert_freshK) 

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

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

495 
txt{*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*} 
11251  496 
apply blast 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

499 
txt{*Prove YM3 by showing that no NB can also be an NA*} 
11251  500 
apply (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

501 
txt{*LEVEL 7: YM4 and Oops remain*} 
11251  502 
apply (clarify, simp add: all_conj_distrib) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

503 
txt{*YM4: key K is visible to Spy, contradicting session key secrecy theorem*} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

504 
txt{*Case analysis on Aa:bad; PROOF FAILED problems 
17411  505 
use @{text Says_unique_NB} to identify message components: @{term "Aa=A"}, @{term "Ba=B"}*} 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

506 
apply (blast dest!: Says_unique_NB analz_shrK_Decrypt 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

507 
parts.Inj [THEN parts.Fst, THEN A_trusts_YM3] 
11251  508 
dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2 
509 
Spy_not_see_encrypted_key) 

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

510 
txt{*Oops case: if the nonce is betrayed now, show that the Oops event is 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

511 
covered by the quantified Oops assumption.*} 
11251  512 
apply (clarify, simp add: all_conj_distrib) 
513 
apply (frule Says_Server_imp_YM2, assumption) 

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

514 
apply (metis Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1)) 
11251  515 
done 
516 

517 

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

518 
text{*B's session key guarantee from YM4. The two certificates contribute to a 
11251  519 
single conclusion about the Server's message. Note that the "Notes Spy" 
17411  520 
assumption must quantify over @{text \<forall>} POSSIBLE keys instead of our particular K. 
11251  521 
If this run is broken and the spy substitutes a certificate containing an 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

522 
old key, B has no means of telling.*} 
11251  523 
lemma B_trusts_YM4: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

524 
"[ Gets B {Crypt (shrK B) {Agent A, Key K}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

525 
Crypt K (Nonce NB)} \<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

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

527 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

528 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

529 
\<forall>k. Notes Spy {Nonce NA, Nonce NB, k} \<notin> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

530 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

531 
==> Says Server A 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

532 
{Crypt (shrK A) {Agent B, Key K, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

533 
Nonce NA, Nonce NB}, 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

534 
Crypt (shrK B) {Agent A, Key K}} 
11251  535 
\<in> set evs" 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

536 
by (blast dest: Spy_not_see_NB Says_unique_NB 
11251  537 
Says_Server_imp_YM2 B_trusts_YM4_newK) 
538 

539 

540 

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

541 
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

542 
@{text Spy_not_see_encrypted_key}*} 
11251  543 
lemma B_gets_good_key: 
544 
"[ Gets B {Crypt (shrK B) {Agent A, Key K}, 

545 
Crypt K (Nonce NB)} \<in> set evs; 

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

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

547 
{Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

548 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

549 
\<forall>k. Notes Spy {Nonce NA, Nonce NB, k} \<notin> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

550 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
11251  551 
==> Key K \<notin> analz (knows Spy evs)" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

552 
by (metis B_trusts_YM4 Spy_not_see_encrypted_key) 
11251  553 

554 

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

555 
subsection{*Authenticating B to A*} 
11251  556 

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

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

560 
evs \<in> yahalom] 

561 
==> B \<notin> bad > 

562 
Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} 

563 
\<in> set evs" 

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

564 
apply (erule rev_mp, erule yahalom.induct, force, 
11251  565 
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

566 
txt{*Fake*} 
11251  567 
apply blast 
568 
done 

569 

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

570 
text{*If the server sends YM3 then B sent YM2*} 
11251  571 
lemma YM3_auth_B_to_A_lemma: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

572 
"[Says Server A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} 
11251  573 
\<in> set evs; evs \<in> yahalom] 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

574 
==> B \<notin> bad > 
11251  575 
Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} 
576 
\<in> set evs" 

577 
apply (erule rev_mp, erule yahalom.induct, simp_all) 

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

578 
txt{*YM3, YM4*} 
11251  579 
apply (blast dest!: B_Said_YM2)+ 
580 
done 

581 

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

582 
text{*If A receives YM3 then B has used nonce NA (and therefore is alive)*} 
11251  583 
lemma YM3_auth_B_to_A: 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

584 
"[ Gets A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

585 
\<in> set evs; 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

586 
A \<notin> bad; B \<notin> bad; evs \<in> yahalom ] 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

587 
==> Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} 
11251  588 
\<in> set evs" 
32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

589 
by (metis A_trusts_YM3 Gets_imp_analz_Spy YM3_auth_B_to_A_lemma analz.Fst 
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

590 
not_parts_not_analz) 
11251  591 

592 

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

593 
subsection{*Authenticating A to B using the certificate 
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

594 
@{term "Crypt K (Nonce NB)"}*} 
11251  595 

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

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

598 
NB matters for freshness.*} 
11251  599 
lemma A_Said_YM3_lemma [rule_format]: 
600 
"evs \<in> yahalom 

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

602 
Crypt K (Nonce NB) \<in> parts (knows Spy evs) > 

603 
Crypt (shrK B) {Agent A, Key K} \<in> parts (knows Spy evs) > 

604 
B \<notin> bad > 

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

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

606 
apply (erule yahalom.induct, force, 
11251  607 
frule_tac [6] YM4_parts_knows_Spy) 
608 
apply (analz_mono_contra, simp_all) 

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

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

611 
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

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

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

615 
If not, use the induction hypothesis*} 
11251  616 
apply (simp add: ex_disj_distrib) 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

617 
txt{*yes: apply unicity of session keys*} 
11251  618 
apply (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

619 
Crypt_Spy_analz_bad 
11251  620 
dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys) 
621 
done 

622 

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

623 
text{*If B receives YM4 then A has used nonce NB (and therefore is alive). 
11251  624 
Moreover, A associates K with NB (thus is talking about the same run). 
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset

625 
Other premises guarantee secrecy of K.*} 
11251  626 
lemma YM4_imp_A_Said_YM3 [rule_format]: 
627 
"[ Gets B {Crypt (shrK B) {Agent A, Key K}, 

628 
Crypt K (Nonce NB)} \<in> set evs; 

629 
Says B Server 

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

631 
\<in> set evs; 

632 
(\<forall>NA k. Notes Spy {Nonce NA, Nonce NB, k} \<notin> set evs); 

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

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

32367
a508148f7c25
Removal of redundant settings of unification trace and search bounds.
paulson
parents:
23746
diff
changeset

635 
by (metis A_Said_YM3_lemma B_gets_good_key Gets_imp_analz_Spy YM4_parts_knows_Spy analz.Fst not_parts_not_analz) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

636 
end 